content: {-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
  {- |
  Module      :  ./CSL/Parse_Test.hs
  Copyright   :  (c) Dominik Dietrich, DFKI Bremen 2010
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  dominik.dietrich@dfki.de
  Stability   :  experimental
  Portability :  portable
  
  -}
  
  module Main where
  
  import CSL.Sign
  import CSL.Analysis
  import CSL.AS_BASIC_CSL
  import CSL.Morphism
  import CSL.Tools
  import CSL.Reduce_Interface
  import CSL.ReduceProve
  import CSL.Keywords
  import CSL.Parse_AS_Basic
  import Common.GlobalAnnotations
  import Text.ParserCombinators.Parsec
  import Common.AnnoState
  import Common.Lexer
  import Common.Parsec
  import Common.Id
  import CSL.Symbol
  import Common.AS_Annotation
  import Common.Utils (getEnvDef)
  import System.IO
  import System.Process
  import Data.Time.Clock
  import Control.Monad.Reader
  -- expression parser
  
  {- ---------------------------------------------------------------------------
  ------------------------------- Parsing -----------------------------------
  --------------------------------------------------------------------------- -}
  
  expression = plusmin
  
  instance OperatorState String where
      lookupOperator _ = lookupOpInfoForParsing operatorInfoMap
      -- FIXME: This probably needs to be implemented!
      lookupBinder _ = error "Not implemented!"
  
  
  res1 = runParser expression (emptyAnnos ()) "" "x+y+y"
  res2 = runParser expression (emptyAnnos ()) "" "x+y*y"
  res3 = runParser expression (emptyAnnos ()) "" "x*y**y"
  res4 = runParser expression (emptyAnnos ()) "" "x**y*y"
  
  -- parser for commands without annotations
  res6 = runParser command (emptyAnnos ()) "" "solve(x^2=1,x)"
  res7 = runParser command (emptyAnnos ()) "" "solve(a*log(sin(x+3))^5 - b, sin(x+3))"
  res8 = runParser command (emptyAnnos ()) "" "solve({x+3y=7,y-x=1},{x,y})"
  res9 = runParser command (emptyAnnos ()) "" "simplify((x+y)*(x+y+z))"
  res10 = runParser command (emptyAnnos ()) "" "remainder(2*x+y,2)"
  res11 = runParser command (emptyAnnos ()) "" "remainder((x+y)*(x+2*y),x+3*y)"
  res12 = runParser command (emptyAnnos ()) "" "gcd(f(x)+g(x)-l1-l2,f(x)-l1)"
  res13 = runParser command (emptyAnnos ()) "" "int(log(x),x)"
  res14 = runParser command (emptyAnnos ()) "" "qelim(all(x, ex(y, x2+xy+b>0 and x+ay2+b<=0)))"
  
  res15 = runParser aFormula (emptyAnnos ()) "" "true"
  res16 = runParser aFormula (emptyAnnos ()) "" "false"
  res17 = runParser aFormula (emptyAnnos ()) "" "2<=3"
  res18 = runParser aFormula (emptyAnnos ()) "" "2<3"
  res19 = runParser aFormula (emptyAnnos ()) "" "2<3 and 2<=3"
  res20 = runParser aFormula (emptyAnnos ()) "" "2<3 or true and false"
  
  -- the basic parser
  res21 = runParser parseBasicItems (emptyAnnos ()) "" "operator f,h"
  res22 = runParser parseBasicItems (emptyAnnos ()) "" ". solve(x^2=1,x)"
  
  res23 = runParser parseOpDecl (emptyAnnos ()) "" "operator f,h"
  res24 = runParser parseAxItems (emptyAnnos ()) "" ". solve(x^2=1,x)"
  
  res25 = runParser basicSpec (emptyAnnos ()) "" "operator f,h . solve(x^2=1,x)"
  
  
  res30 = runParser extparam () "" "I=0"
  res31 = runParser extparam () "" "I < I+1"
  
  res32 = runParser command (emptyAnnos ()) "" "d_4 := 4.0"
  
  res32pure = case res32 of Right a -> a
  -- processCmds [(makeNamed "as" res32pure)]
  
  
  p001 = runParser signednumber () ""
  p002 = runParser scanFloatExt () ""
  p004 = runParser scanMyFloat () ""
  p01 = runParser scanFloatExt1 () ""
  p02 = runParser scanFloatExt2 () ""
  
  checknums :: [String]
  checknums = [ "1.", ".1", "2.e-13", ".2e+13", "-.1", "-.33E-12", "123", "001" ]
  
  
  -- | In addition to scanFloat, also '1.', '.1' and '2.e-13' are recognized
  scanMyFloat :: CharParser st String
  scanMyFloat =
      let -- the 'E' component
          compE = oneOf "eE" <:> getSNumber
          -- the '.' component
          compD n = char '.' <:> n
          -- an optional number
          getNumber' = option "0" getNumber
          checkSign' '+' = []
          checkSign' _ = "-"
          checkSp "-." = "-0."
          checkSp _ = "0."
          getSNumber = withS getNumber
          withS p = optionL (oneOf "+-" >-> checkSign') <++> p
      in -- '1.' or '2.e-13' or '1.213'
        try (getSNumber <++> (optionL (try $ compD getNumber') <++> optionL compE))
        -- everything starting with a dot
        <|> (choice (map string ["+.", "-.", "."]) >-> checkSp) <++> getNumber <++> optionL compE
  
  -- withS (compD getNumber >-> ("0"++)) <++> optionL compE
  
  scanFloatExt1 :: CharParser st String
  scanFloatExt1 =
      let -- the 'E' component
          compE = oneOf "eE" <:> optionL getSign <++> getNumber
          -- the '.' component
          compD n = char '.' <:> n
          -- an optional number
          getNumber' = option "0" getNumber
          eatPlus '+' = ""
          eatPlus _ = "-"
          -- an optional number
          getSign = oneOf "+-" >-> eatPlus
      in -- '1.' or '2.e-13' or '1.213'
        try (getSign <++> getNumber
             <++> (optionL (try $ compD getNumber') <++> optionL compE))
        -- everything starting with a dot
        <|> getSign <++> (compD getNumber >-> ("0" ++)) <++> optionL compE
  
  scanFloatExt2 :: CharParser st String
  scanFloatExt2 =
      let -- the 'E' component
          compE = oneOf "eE" <:> optionL getSign <++> getNumber
          -- the '.' component
          compD n = char '.' <:> n
          -- an optional number
          getNumber' = option "0" getNumber
          eatPlus '+' = ""
          eatPlus _ = "-"
          -- an optional number
          getSign = oneOf "+-" >-> eatPlus
      in -- '1.' or '2.e-13' or '1.213'
        getSign <++>
                ((getNumber <++> optionL (try $ compD getNumber') <++> optionL compE)
                 -- everything starting with a dot
                 <|> (compD getNumber >-> ("0" ++)) <++> optionL compE)
  
  
  -- declares an equation and ask for the result
  castest = do
    reducecmd <- getEnvDef "HETS_REDUCE" "redcsl"
    (inpt, out, _, pid) <- connectCAS reducecmd
    let sess = (inpt, out, pid)
    putStrLn "Send the command "
    casDeclareEquation sess res32pure
    procCmd sess (makeNamed "test" (Cmd "ask" [Var (mkSimpleId "d_4")]))
    {- putStrLn "query term.. "
    hPutStrLn inp "d_4;"
    res <- getNextResultOutput out
    putStrLn ( "Output is " ++ res) -}
    disconnectCAS sess
    return ()
  
  
  resS = runParser basicSpec (emptyAnnos ()) ""
  
  
  -- time measurement, pendant of the time shell command
  time :: MonadIO m => m a -> m a
  time p = do
    t <- liftIO getCurrentTime
    res <- p
    t' <- liftIO getCurrentTime
    liftIO $ print $ diffUTCTime t' t
    return res
  
  
  -- Run e.g.: time $ testBS "Hets-lib/EnCL/antlr/t2.dol" "/tmp/t2.out"
  testBS fpin fpout = do
    putStr "Reading time was "
    s <- time $ do
           s <- readFile fpin
           putStr $ "(File length: " ++ show (length s) ++ ")"
           return s
    putStr "Parsing time was "
    x <- time $ return $ runParser basicSpec (emptyAnnos ()) "" s
    case x of
      Right bs -> do
             putStr "Writing time was "
             time $ writeFile fpout $ show $ pretty bs
      Left e -> putStrLn $ "Error: " ++ show e
  
  {- ---------------------------------------------------------------------------
  ----------------------- test of static analysis... ------------------------
  --------------------------------------------------------------------------- -}
  
  testspec =
      case runParser basicSpec (emptyAnnos ()) "" "operator f,h . solve(x^2=1,x) . solve(x*x=1,x)" of
        Right a -> a
  
  res26 = splitSpec testspec emptySig
  
  res27 = basicCSLAnalysis (testspec, emptySig, [])
  
  {- ---------------------------------------------------------------------------
  ------------------------------- Analysis ----------------------------------
  --------------------------------------------------------------------------- -}
  
  -- getAtomsFromFile fp = readFile fp >>= return . getAtomsFrom
  
  {- getAtomsFrom s =
  case runParser basicSpec (emptyAnnos ()) "" s of
  Right a -> map (\ (x:l) -> (x, 1 + length l)) $ group $ sort $ getBSAtoms a
  _ -> error "no parse" -}
  
  
  {- ---------------------------------------------------------------------------
  ------------------------------- Morphisms ---------------------------------
  --------------------------------------------------------------------------- -}
  
  
  {- ---------------------------------------------------------------------------
  ------------------------------- Signature ---------------------------------
  --------------------------------------------------------------------------- -}
  
  
  {- ---------------------------------------------------------------------------
  ---------------------------- CSL Interface -----------------------------
  --------------------------------------------------------------------------- -}
  