{-# LANGUAGE FlexibleInstances #-}
{- |
Module      :  ./CSL/Reduce_Interface.hs
Description :  interface to Reduce CAS
Copyright   :  (c) Dominik Dietrich, DFKI Bremen, 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Dominik.Dietrich@dfki.de
Stability   :  provisional
Portability :  non-portable (uses type-expression in class instances)

Interface for Reduce CAS system.
-}

module CSL.Reduce_Interface where

import Common.AS_Annotation
import Common.Id
import Common.ProverTools (missingExecutableInPath)
import Common.Utils (getEnvDef)

import Logic.Prover

import CSL.AS_BASIC_CSL
import CSL.ASUtils
import CSL.Parse_AS_Basic
import CSL.Lemma_Export

import Control.Monad (replicateM_)
import Data.Time (midnight)
import Data.Maybe (maybeToList)
import Data.List (intercalate)
import qualified Data.Map as Map

import System.IO
import System.Process

{- ----------------------------------------------------------------------
Connection handling
---------------------------------------------------------------------- -}

-- | A session is a process connection
class Session a where
    outp :: a -> Handle
    inp :: a -> Handle
    err :: a -> Maybe Handle
    err = Maybe Handle -> a -> Maybe Handle
forall a b. a -> b -> a
const Maybe Handle
forall a. Maybe a
Nothing
    proch :: a -> Maybe ProcessHandle
    proch = Maybe ProcessHandle -> a -> Maybe ProcessHandle
forall a b. a -> b -> a
const Maybe ProcessHandle
forall a. Maybe a
Nothing

-- | The simplest session
instance Session (Handle, Handle) where
    inp :: (Handle, Handle) -> Handle
inp = (Handle, Handle) -> Handle
forall a b. (a, b) -> a
fst
    outp :: (Handle, Handle) -> Handle
outp = (Handle, Handle) -> Handle
forall a b. (a, b) -> b
snd

-- | Better use this session to properly close the connection
instance Session (Handle, Handle, ProcessHandle) where
    inp :: (Handle, Handle, ProcessHandle) -> Handle
inp (x :: Handle
x, _, _) = Handle
x
    outp :: (Handle, Handle, ProcessHandle) -> Handle
outp (_, x :: Handle
x, _) = Handle
x
    proch :: (Handle, Handle, ProcessHandle) -> Maybe ProcessHandle
proch (_, _, x :: ProcessHandle
x) = ProcessHandle -> Maybe ProcessHandle
forall a. a -> Maybe a
Just ProcessHandle
x


-- | Left String is success, Right String is failure
lookupRedShellCmd :: IO (Either String String)
lookupRedShellCmd :: IO (Either String String)
lookupRedShellCmd = do
  String
reducecmd <- String -> String -> IO String
getEnvDef "HETS_REDUCE" "redcsl"
  -- check that prog exists
  Bool
noProg <- String -> IO Bool
missingExecutableInPath String
reducecmd
  let f :: a -> Either a a
f = if Bool
noProg then a -> Either a a
forall a b. b -> Either a b
Right else a -> Either a a
forall a b. a -> Either a b
Left
  Either String String -> IO (Either String String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String String -> IO (Either String String))
-> Either String String -> IO (Either String String)
forall a b. (a -> b) -> a -> b
$ String -> Either String String
forall a. a -> Either a a
f String
reducecmd


-- | connects to the CAS, prepares the streams and sets initial options
connectCAS :: String -> IO (Handle, Handle, Handle, ProcessHandle)
connectCAS :: String -> IO (Handle, Handle, Handle, ProcessHandle)
connectCAS reducecmd :: String
reducecmd = do
    String -> IO ()
putStrLn "succeeded"
    (inpt :: Handle
inpt, out :: Handle
out, errh :: Handle
errh, pid :: ProcessHandle
pid) <- String -> IO (Handle, Handle, Handle, ProcessHandle)
runInteractiveCommand (String -> IO (Handle, Handle, Handle, ProcessHandle))
-> String -> IO (Handle, Handle, Handle, ProcessHandle)
forall a b. (a -> b) -> a -> b
$ String
reducecmd String -> String -> String
forall a. [a] -> [a] -> [a]
++ " -w"
    Handle -> BufferMode -> IO ()
hSetBuffering Handle
out BufferMode
NoBuffering
    Handle -> BufferMode -> IO ()
hSetBuffering Handle
inpt BufferMode
LineBuffering
    Handle -> String -> IO ()
hPutStrLn Handle
inpt "off nat;"
    Handle -> String -> IO ()
hPutStrLn Handle
inpt "load redlog;"
    Handle -> String -> IO ()
hPutStrLn Handle
inpt "rlset reals;"
    -- read 7 lines
    Int -> IO String -> IO ()
forall (m :: * -> *) a. Applicative m => Int -> m a -> m ()
replicateM_ 7 (IO String -> IO ()) -> IO String -> IO ()
forall a b. (a -> b) -> a -> b
$ Handle -> IO String
hGetLine Handle
out
    String -> IO ()
putStrLn "done"
    (Handle, Handle, Handle, ProcessHandle)
-> IO (Handle, Handle, Handle, ProcessHandle)
forall (m :: * -> *) a. Monad m => a -> m a
return (Handle
inpt, Handle
out, Handle
errh, ProcessHandle
pid)

-- | closes the connection to the CAS
disconnectCAS :: Session a => a -> IO ()
disconnectCAS :: a -> IO ()
disconnectCAS s :: a
s = do
  Handle -> String -> IO ()
hPutStrLn (a -> Handle
forall a. Session a => a -> Handle
inp a
s) "quit;"
  case a -> Maybe ProcessHandle
forall a. Session a => a -> Maybe ProcessHandle
proch a
s of
    Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

    {- this is always better, because it closes also the shell-process,
    hence use a Session-variant with ProcessHandle! -}
    Just ph :: ProcessHandle
ph -> ProcessHandle -> IO ExitCode
waitForProcess ProcessHandle
ph IO ExitCode -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  String -> IO ()
putStrLn "CAS disconnected"
  () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

sendToReduce :: Session a => a -> String -> IO ()
sendToReduce :: a -> String -> IO ()
sendToReduce sess :: a
sess = Handle -> String -> IO ()
hPutStrLn (a -> Handle
forall a. Session a => a -> Handle
inp a
sess)

{- ----------------------------------------------------------------------
Prover specific
---------------------------------------------------------------------- -}

-- | returns the name of the reduce prover
reduceS :: String
reduceS :: String
reduceS = "Reduce"

{- | returns a basic proof status for conjecture with name n
  where [EXPRESSION] represents the proof tree. -}
openReduceProofStatus :: String -> [EXPRESSION] -> ProofStatus [EXPRESSION]
openReduceProofStatus :: String -> [EXPRESSION] -> ProofStatus [EXPRESSION]
openReduceProofStatus n :: String
n = String -> String -> [EXPRESSION] -> ProofStatus [EXPRESSION]
forall pt. Ord pt => String -> String -> pt -> ProofStatus pt
openProofStatus String
n String
reduceS

closedReduceProofStatus :: Ord pt => String -- ^ name of the goal
                -> pt -> ProofStatus pt
closedReduceProofStatus :: String -> pt -> ProofStatus pt
closedReduceProofStatus goalname :: String
goalname proof_tree :: pt
proof_tree =
    ProofStatus :: forall proof_tree.
String
-> GoalStatus
-> [String]
-> String
-> proof_tree
-> TimeOfDay
-> TacticScript
-> [String]
-> ProofStatus proof_tree
ProofStatus
    { goalName :: String
goalName = String
goalname
    , goalStatus :: GoalStatus
goalStatus = Bool -> GoalStatus
Proved Bool
True
    , usedAxioms :: [String]
usedAxioms = []
    , usedProver :: String
usedProver = String
reduceS
    , proofTree :: pt
proofTree = pt
proof_tree
    , usedTime :: TimeOfDay
usedTime = TimeOfDay
midnight
    , tacticScript :: TacticScript
tacticScript = String -> TacticScript
TacticScript ""
    , proofLines :: [String]
proofLines = [] }

{-
For Quantifier Elimination:

off nat; -- pretty-printing switch
load redlog;
rlset reals;

rlqe(exp...);
-}


{- ----------------------------------------------------------------------
Reduce Pretty Printing
---------------------------------------------------------------------- -}

exportExps :: [EXPRESSION] -> String
exportExps :: [EXPRESSION] -> String
exportExps l :: [EXPRESSION]
l = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "," ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (EXPRESSION -> String) -> [EXPRESSION] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map EXPRESSION -> String
exportExp [EXPRESSION]
l


-- | those operators declared as infix in Reduce
infixOps :: [String]
infixOps :: [String]
infixOps = [ "+", "-", "/", "**", "^", "=", "<=", ">=", "<", ">", "*", "and"
           , "impl", "or"]

-- | Exports an expression to Reduce format
exportExp :: EXPRESSION -> String
exportExp :: EXPRESSION -> String
exportExp (Var token :: Token
token) = Token -> String
tokStr Token
token
exportExp (Op s :: OPID
s _ exps :: [EXPRESSION]
exps@[e1 :: EXPRESSION
e1, e2 :: EXPRESSION
e2] _)
    | String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (OPID -> String
simpleName OPID
s) [String]
infixOps =
        [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ["(", EXPRESSION -> String
exportExp EXPRESSION
e1, OPID -> String
simpleName OPID
s, EXPRESSION -> String
exportExp EXPRESSION
e2, ")"]
    | Bool
otherwise = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [OPID -> String
simpleName OPID
s, "(", [EXPRESSION] -> String
exportExps [EXPRESSION]
exps, ")"]
exportExp (Op s :: OPID
s _ [] _) = OPID -> String
simpleName OPID
s
exportExp (Op s :: OPID
s _ exps :: [EXPRESSION]
exps _) = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [OPID -> String
simpleName OPID
s, "(", [EXPRESSION] -> String
exportExps [EXPRESSION]
exps, ")"]
exportExp (List exps :: [EXPRESSION]
exps _) = "{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [EXPRESSION] -> String
exportExps [EXPRESSION]
exps String -> String -> String
forall a. [a] -> [a] -> [a]
++ "}"
exportExp (Int i :: APInt
i _) = APInt -> String
forall a. Show a => a -> String
show APInt
i
exportExp (Rat d :: APFloat
d _) = APFloat -> String
forall a. Show a => a -> String
show APFloat
d
exportExp (Interval l :: Double
l r :: Double
r _) = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ "[", Double -> String
forall a. Show a => a -> String
show Double
l, ",", Double -> String
forall a. Show a => a -> String
show Double
r, "]" ]
-- exportExp e = error $ "exportExp: expression not supported: " ++ show e

-- | exports command to Reduce Format
exportReduce :: Named CMD -> String
exportReduce :: Named CMD -> String
exportReduce namedcmd :: Named CMD
namedcmd = case Named CMD -> CMD
forall s a. SenAttr s a -> s
sentence Named CMD
namedcmd of
  Cmd "simplify" exps :: [EXPRESSION]
exps -> EXPRESSION -> String
exportExp (EXPRESSION -> String) -> EXPRESSION -> String
forall a b. (a -> b) -> a -> b
$ [EXPRESSION] -> EXPRESSION
forall a. [a] -> a
head [EXPRESSION]
exps
  Cmd "ask" exps :: [EXPRESSION]
exps -> EXPRESSION -> String
exportExp (EXPRESSION -> String) -> EXPRESSION -> String
forall a b. (a -> b) -> a -> b
$ [EXPRESSION] -> EXPRESSION
forall a. [a] -> a
head [EXPRESSION]
exps
  Cmd cmd :: String
cmd exps :: [EXPRESSION]
exps -> String
cmd String -> String -> String
forall a. [a] -> [a] -> [a]
++ "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [EXPRESSION] -> String
exportExps [EXPRESSION]
exps String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
  _ -> String -> String
forall a. HasCallStack => String -> a
error "exportReduce: not implemented for this case" -- TODO: implement


{- ----------------------------------------------------------------------
Reduce Parsing
---------------------------------------------------------------------- -}

-- | removes the newlines 4: from the beginning of the string
skipReduceLineNr :: String -> String
skipReduceLineNr :: String -> String
skipReduceLineNr s :: String
s = (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` " \n") (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String
forall a. [a] -> [a]
tail
                     (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= ':') String
s

-- | try to get an EXPRESSION from a Reduce string
redOutputToExpression :: String -> Maybe EXPRESSION
redOutputToExpression :: String -> Maybe EXPRESSION
redOutputToExpression = () -> String -> Maybe EXPRESSION
forall a. OperatorState a => a -> String -> Maybe EXPRESSION
parseExpression () (String -> Maybe EXPRESSION)
-> (String -> String) -> String -> Maybe EXPRESSION
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
skipReduceLineNr


{- ----------------------------------------------------------------------
Reduce Commands
---------------------------------------------------------------------- -}


cslReduceDefaultMapping :: [(OPNAME, String)]
cslReduceDefaultMapping :: [(OPNAME, String)]
cslReduceDefaultMapping =
    let idmapping :: [OPNAME] -> [(OPNAME, String)]
idmapping = (OPNAME -> (OPNAME, String)) -> [OPNAME] -> [(OPNAME, String)]
forall a b. (a -> b) -> [a] -> [b]
map (\ x :: OPNAME
x -> (OPNAME
x, OPNAME -> String
forall a. Show a => a -> String
show OPNAME
x))
    in (OPNAME
OP_pow, "**") (OPNAME, String) -> [(OPNAME, String)] -> [(OPNAME, String)]
forall a. a -> [a] -> [a]
:
           [OPNAME] -> [(OPNAME, String)]
idmapping (Map OPNAME ArityMap -> [OPNAME]
forall k a. Map k a -> [k]
Map.keys (Map OPNAME ArityMap -> [OPNAME])
-> Map OPNAME ArityMap -> [OPNAME]
forall a b. (a -> b) -> a -> b
$ OPNAME -> Map OPNAME ArityMap -> Map OPNAME ArityMap
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete OPNAME
OP_pow Map OPNAME ArityMap
operatorInfoNameMap)

{- | reads characters from the specified output until the next result is
  complete, indicated by $ when using the maxima mode off nat; -}
getNextResultOutput :: Handle -> IO String
getNextResultOutput :: Handle -> IO String
getNextResultOutput out :: Handle
out = do
  Bool
b <- Handle -> IO Bool
hIsEOF Handle
out
  if Bool
b then String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "" else do
                        Char
c <- Handle -> IO Char
hGetChar Handle
out
                        if Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '$' then String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return [] else do
                                                   String
r <- Handle -> IO String
getNextResultOutput Handle
out
                                                   String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (Char
c Char -> String -> String
forall a. a -> [a] -> [a]
: String
r)


procCmd :: Session a => a -> Named CMD
        -> IO (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
procCmd :: a
-> Named CMD
-> IO
     (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
procCmd sess :: a
sess cmd :: Named CMD
cmd = case String
cmdstring of
                     "simplify" -> a
-> Named CMD
-> IO
     (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
forall a.
Session a =>
a
-> Named CMD
-> IO
     (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
cassimplify a
sess Named CMD
cmd
                     "ask" -> a
-> Named CMD
-> IO
     (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
forall a.
Session a =>
a
-> Named CMD
-> IO
     (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
casask a
sess Named CMD
cmd
                     "divide" -> a
-> Named CMD
-> IO
     (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
forall a.
Session a =>
a
-> Named CMD
-> IO
     (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
casremainder a
sess Named CMD
cmd
                     "rlqe" -> a
-> Named CMD
-> IO
     (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
forall a.
Session a =>
a
-> Named CMD
-> IO
     (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
casqelim a
sess Named CMD
cmd
                     "factorize" -> a
-> Named CMD
-> IO
     (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
forall a.
Session a =>
a
-> Named CMD
-> IO
     (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
casfactorExp a
sess Named CMD
cmd
                     "int" -> a
-> Named CMD
-> IO
     (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
forall a.
Session a =>
a
-> Named CMD
-> IO
     (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
casint a
sess Named CMD
cmd
                     "solve" -> a
-> Named CMD
-> IO
     (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
forall a.
Session a =>
a
-> Named CMD
-> IO
     (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
cassolve a
sess Named CMD
cmd
                     _ -> String
-> IO
     (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
forall a. HasCallStack => String -> a
error "Command not supported"
    where Cmd cmdstring :: String
cmdstring _ = Named CMD -> CMD
forall s a. SenAttr s a -> s
sentence Named CMD
cmd

-- | sends the given string to the CAS, reads the result and tries to parse it.
evalString :: Session a => a -> String -> IO [EXPRESSION]
evalString :: a -> String -> IO [EXPRESSION]
evalString sess :: a
sess s :: String
s = do
  String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "Send CAS cmd " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
  Handle -> String -> IO ()
hPutStrLn (a -> Handle
forall a. Session a => a -> Handle
inp a
sess) String
s
  String
res <- Handle -> IO String
getNextResultOutput (a -> Handle
forall a. Session a => a -> Handle
outp a
sess)
  String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "Result is " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
res
  String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "Parsing of --" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
skipReduceLineNr String
res String -> String -> String
forall a. [a] -> [a] -> [a]
++ "-- yields "
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ Maybe EXPRESSION -> String
forall a. Show a => a -> String
show (String -> Maybe EXPRESSION
redOutputToExpression String
res)
  [EXPRESSION] -> IO [EXPRESSION]
forall (m :: * -> *) a. Monad m => a -> m a
return ([EXPRESSION] -> IO [EXPRESSION])
-> [EXPRESSION] -> IO [EXPRESSION]
forall a b. (a -> b) -> a -> b
$ Maybe EXPRESSION -> [EXPRESSION]
forall a. Maybe a -> [a]
maybeToList (Maybe EXPRESSION -> [EXPRESSION])
-> Maybe EXPRESSION -> [EXPRESSION]
forall a b. (a -> b) -> a -> b
$ String -> Maybe EXPRESSION
redOutputToExpression String
res

-- | wrap evalString into a ProofStatus
procString :: Session a => a -> String -> String -> IO (ProofStatus [EXPRESSION])
procString :: a -> String -> String -> IO (ProofStatus [EXPRESSION])
procString h :: a
h axname :: String
axname s :: String
s = do
  [EXPRESSION]
res <- a -> String -> IO [EXPRESSION]
forall a. Session a => a -> String -> IO [EXPRESSION]
evalString a
h String
s
  let f :: String -> [EXPRESSION] -> ProofStatus [EXPRESSION]
f = if [EXPRESSION] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [EXPRESSION]
res then String -> [EXPRESSION] -> ProofStatus [EXPRESSION]
openReduceProofStatus else String -> [EXPRESSION] -> ProofStatus [EXPRESSION]
forall pt. Ord pt => String -> pt -> ProofStatus pt
closedReduceProofStatus
  ProofStatus [EXPRESSION] -> IO (ProofStatus [EXPRESSION])
forall (m :: * -> *) a. Monad m => a -> m a
return (ProofStatus [EXPRESSION] -> IO (ProofStatus [EXPRESSION]))
-> ProofStatus [EXPRESSION] -> IO (ProofStatus [EXPRESSION])
forall a b. (a -> b) -> a -> b
$ String -> [EXPRESSION] -> ProofStatus [EXPRESSION]
f String
axname [EXPRESSION]
res

-- | factors a given expression over the reals
casfactorExp :: Session a => a -> Named CMD -> IO (ProofStatus [EXPRESSION],
                 [(Named CMD, ProofStatus [EXPRESSION])])
casfactorExp :: a
-> Named CMD
-> IO
     (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
casfactorExp sess :: a
sess cmd :: Named CMD
cmd =
  do
    ProofStatus [EXPRESSION]
proofstatus <- a -> String -> String -> IO (ProofStatus [EXPRESSION])
forall a.
Session a =>
a -> String -> String -> IO (ProofStatus [EXPRESSION])
procString a
sess (Named CMD -> String
forall s a. SenAttr s a -> a
senAttr Named CMD
cmd) (String -> IO (ProofStatus [EXPRESSION]))
-> String -> IO (ProofStatus [EXPRESSION])
forall a b. (a -> b) -> a -> b
$ Named CMD -> String
exportReduce Named CMD
cmd String -> String -> String
forall a. [a] -> [a] -> [a]
++ ";"
    (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
-> IO
     (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
forall (m :: * -> *) a. Monad m => a -> m a
return (ProofStatus [EXPRESSION]
proofstatus, [Named CMD
-> ProofStatus [EXPRESSION]
-> (Named CMD, ProofStatus [EXPRESSION])
exportLemmaFactor Named CMD
cmd ProofStatus [EXPRESSION]
proofstatus])

-- | solves a single equation over the reals
cassolve :: Session a => a -> Named CMD -> IO (ProofStatus [EXPRESSION],
             [(Named CMD, ProofStatus [EXPRESSION])])
cassolve :: a
-> Named CMD
-> IO
     (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
cassolve sess :: a
sess cmd :: Named CMD
cmd =
  do
    ProofStatus [EXPRESSION]
proofstatus <- a -> String -> String -> IO (ProofStatus [EXPRESSION])
forall a.
Session a =>
a -> String -> String -> IO (ProofStatus [EXPRESSION])
procString a
sess (Named CMD -> String
forall s a. SenAttr s a -> a
senAttr Named CMD
cmd) (String -> IO (ProofStatus [EXPRESSION]))
-> String -> IO (ProofStatus [EXPRESSION])
forall a b. (a -> b) -> a -> b
$ Named CMD -> String
exportReduce Named CMD
cmd String -> String -> String
forall a. [a] -> [a] -> [a]
++ ";"
    (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
-> IO
     (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
forall (m :: * -> *) a. Monad m => a -> m a
return (ProofStatus [EXPRESSION]
proofstatus, [])


-- | simplifies a given expression over the reals
cassimplify :: Session a => a -> Named CMD -> IO (ProofStatus [EXPRESSION],
                [(Named CMD, ProofStatus [EXPRESSION])])
cassimplify :: a
-> Named CMD
-> IO
     (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
cassimplify sess :: a
sess cmd :: Named CMD
cmd = do
  ProofStatus [EXPRESSION]
proofstatus <- a -> String -> String -> IO (ProofStatus [EXPRESSION])
forall a.
Session a =>
a -> String -> String -> IO (ProofStatus [EXPRESSION])
procString a
sess (Named CMD -> String
forall s a. SenAttr s a -> a
senAttr Named CMD
cmd) (String -> IO (ProofStatus [EXPRESSION]))
-> String -> IO (ProofStatus [EXPRESSION])
forall a b. (a -> b) -> a -> b
$ Named CMD -> String
exportReduce Named CMD
cmd String -> String -> String
forall a. [a] -> [a] -> [a]
++ ";"
  (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
-> IO
     (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
forall (m :: * -> *) a. Monad m => a -> m a
return (ProofStatus [EXPRESSION]
proofstatus, [Named CMD
-> ProofStatus [EXPRESSION]
-> (Named CMD, ProofStatus [EXPRESSION])
exportLemmaSimplify Named CMD
cmd ProofStatus [EXPRESSION]
proofstatus])


-- | asks value of a given expression
casask :: Session a => a -> Named CMD -> IO (ProofStatus [EXPRESSION],
           [(Named CMD, ProofStatus [EXPRESSION])])
casask :: a
-> Named CMD
-> IO
     (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
casask sess :: a
sess cmd :: Named CMD
cmd = do
  ProofStatus [EXPRESSION]
proofstatus <- a -> String -> String -> IO (ProofStatus [EXPRESSION])
forall a.
Session a =>
a -> String -> String -> IO (ProofStatus [EXPRESSION])
procString a
sess (Named CMD -> String
forall s a. SenAttr s a -> a
senAttr Named CMD
cmd) (String -> IO (ProofStatus [EXPRESSION]))
-> String -> IO (ProofStatus [EXPRESSION])
forall a b. (a -> b) -> a -> b
$ Named CMD -> String
exportReduce Named CMD
cmd String -> String -> String
forall a. [a] -> [a] -> [a]
++ ";"
  (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
-> IO
     (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
forall (m :: * -> *) a. Monad m => a -> m a
return (ProofStatus [EXPRESSION]
proofstatus, [Named CMD
-> ProofStatus [EXPRESSION]
-> (Named CMD, ProofStatus [EXPRESSION])
exportLemmaAsk Named CMD
cmd ProofStatus [EXPRESSION]
proofstatus])


-- | computes the remainder of a division
casremainder :: Session a => a -> Named CMD -> IO (ProofStatus [EXPRESSION],
                 [(Named CMD, ProofStatus [EXPRESSION])])
casremainder :: a
-> Named CMD
-> IO
     (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
casremainder sess :: a
sess cmd :: Named CMD
cmd =
  do
    ProofStatus [EXPRESSION]
proofstatus <- a -> String -> String -> IO (ProofStatus [EXPRESSION])
forall a.
Session a =>
a -> String -> String -> IO (ProofStatus [EXPRESSION])
procString a
sess (Named CMD -> String
forall s a. SenAttr s a -> a
senAttr Named CMD
cmd) (String -> IO (ProofStatus [EXPRESSION]))
-> String -> IO (ProofStatus [EXPRESSION])
forall a b. (a -> b) -> a -> b
$ Named CMD -> String
exportReduce
      (String -> CMD -> Named CMD
forall a s. a -> s -> SenAttr s a
makeNamed (Named CMD -> String
forall s a. SenAttr s a -> a
senAttr Named CMD
cmd) (String -> [EXPRESSION] -> CMD
Cmd "divide" [EXPRESSION]
args)) String -> String -> String
forall a. [a] -> [a] -> [a]
++ ";"
    (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
-> IO
     (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
forall (m :: * -> *) a. Monad m => a -> m a
return (ProofStatus [EXPRESSION]
proofstatus, [Named CMD
-> ProofStatus [EXPRESSION]
-> (Named CMD, ProofStatus [EXPRESSION])
exportLemmaRemainder Named CMD
cmd ProofStatus [EXPRESSION]
proofstatus])
  where Cmd _ args :: [EXPRESSION]
args = Named CMD -> CMD
forall s a. SenAttr s a -> s
sentence Named CMD
cmd

-- | integrates the given expression
casint :: Session a => a -> Named CMD -> IO (ProofStatus [EXPRESSION],
           [(Named CMD, ProofStatus [EXPRESSION])])
casint :: a
-> Named CMD
-> IO
     (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
casint sess :: a
sess cmd :: Named CMD
cmd =
  do
    ProofStatus [EXPRESSION]
proofstatus <- a -> String -> String -> IO (ProofStatus [EXPRESSION])
forall a.
Session a =>
a -> String -> String -> IO (ProofStatus [EXPRESSION])
procString a
sess (Named CMD -> String
forall s a. SenAttr s a -> a
senAttr Named CMD
cmd) (String -> IO (ProofStatus [EXPRESSION]))
-> String -> IO (ProofStatus [EXPRESSION])
forall a b. (a -> b) -> a -> b
$ Named CMD -> String
exportReduce Named CMD
cmd String -> String -> String
forall a. [a] -> [a] -> [a]
++ ";"
    (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
-> IO
     (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
forall (m :: * -> *) a. Monad m => a -> m a
return (ProofStatus [EXPRESSION]
proofstatus, [Named CMD
-> ProofStatus [EXPRESSION]
-> (Named CMD, ProofStatus [EXPRESSION])
exportLemmaInt Named CMD
cmd ProofStatus [EXPRESSION]
proofstatus])

-- | performs quantifier elimination of a given expression
casqelim :: Session a => a -> Named CMD -> IO (ProofStatus [EXPRESSION],
 [(Named CMD, ProofStatus [EXPRESSION])])
casqelim :: a
-> Named CMD
-> IO
     (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
casqelim sess :: a
sess cmd :: Named CMD
cmd =
  do
    ProofStatus [EXPRESSION]
proofstatus <- a -> String -> String -> IO (ProofStatus [EXPRESSION])
forall a.
Session a =>
a -> String -> String -> IO (ProofStatus [EXPRESSION])
procString a
sess (Named CMD -> String
forall s a. SenAttr s a -> a
senAttr Named CMD
cmd) (String -> IO (ProofStatus [EXPRESSION]))
-> String -> IO (ProofStatus [EXPRESSION])
forall a b. (a -> b) -> a -> b
$ Named CMD -> String
exportReduce Named CMD
cmd String -> String -> String
forall a. [a] -> [a] -> [a]
++ ";"
    (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
-> IO
     (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
forall (m :: * -> *) a. Monad m => a -> m a
return (ProofStatus [EXPRESSION]
proofstatus, [Named CMD
-> ProofStatus [EXPRESSION]
-> (Named CMD, ProofStatus [EXPRESSION])
exportLemmaQelim Named CMD
cmd ProofStatus [EXPRESSION]
proofstatus])

-- | declares an operator, such that it can used infix/prefix in CAS
casDeclareOperators :: Session a => a -> [EXPRESSION] -> IO ()
casDeclareOperators :: a -> [EXPRESSION] -> IO ()
casDeclareOperators sess :: a
sess varlist :: [EXPRESSION]
varlist = do
  Handle -> String -> IO ()
hPutStrLn (a -> Handle
forall a. Session a => a -> Handle
inp a
sess) (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "operator " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [EXPRESSION] -> String
exportExps [EXPRESSION]
varlist String -> String -> String
forall a. [a] -> [a] -> [a]
++ ";"
  Handle -> IO String
hGetLine (a -> Handle
forall a. Session a => a -> Handle
outp a
sess)
  () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | declares an equation x := exp
casDeclareEquation :: Session a => a -> CMD -> IO ()
casDeclareEquation :: a -> CMD -> IO ()
casDeclareEquation sess :: a
sess (Ass c :: OpDecl
c def :: EXPRESSION
def) =
    do
      let e1 :: String
e1 = EXPRESSION -> String
exportExp (EXPRESSION -> String) -> EXPRESSION -> String
forall a b. (a -> b) -> a -> b
$ OpDecl -> EXPRESSION
opDeclToOp OpDecl
c
          e2 :: String
e2 = EXPRESSION -> String
exportExp EXPRESSION
def
      String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ ":=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
e2
      Handle -> String -> IO ()
hPutStrLn (a -> Handle
forall a. Session a => a -> Handle
inp a
sess) (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ ":=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
e2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ ";"
      String
res <- Handle -> IO String
getNextResultOutput (a -> Handle
forall a. Session a => a -> Handle
outp a
sess)
      String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "Declaration Result: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
res
      () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

casDeclareEquation _ _ =
    String -> IO ()
forall a. HasCallStack => String -> a
error "casDeclareEquation: not implemented for this case" -- TODO: implement


{- ----------------------------------------------------------------------
Reduce Lemma Export
---------------------------------------------------------------------- -}

exportLemmaGeneric :: Named CMD -> ProofStatus [EXPRESSION] ->
                      (Named CMD, ProofStatus [EXPRESSION])
exportLemmaGeneric :: Named CMD
-> ProofStatus [EXPRESSION]
-> (Named CMD, ProofStatus [EXPRESSION])
exportLemmaGeneric namedcmd :: Named CMD
namedcmd ps :: ProofStatus [EXPRESSION]
ps =
  (String -> CMD -> Named CMD
forall a s. a -> s -> SenAttr s a
makeNamed String
lemmaname CMD
lemma, String -> [EXPRESSION] -> ProofStatus [EXPRESSION]
forall pt. Ord pt => String -> pt -> ProofStatus pt
closedReduceProofStatus String
lemmaname [String -> [EXPRESSION] -> EXPRESSION
mkOp "Proof" []])
      where Cmd _ exps :: [EXPRESSION]
exps = Named CMD -> CMD
forall s a. SenAttr s a -> s
sentence Named CMD
namedcmd
            lemma :: CMD
lemma = String -> [EXPRESSION] -> CMD
Cmd "=" [[EXPRESSION] -> EXPRESSION
forall a. [a] -> a
head [EXPRESSION]
exps, [EXPRESSION] -> EXPRESSION
forall a. [a] -> a
head (ProofStatus [EXPRESSION] -> [EXPRESSION]
forall proof_tree. ProofStatus proof_tree -> proof_tree
proofTree ProofStatus [EXPRESSION]
ps)]
            lemmaname :: String
lemmaname = Named CMD -> String
ganame Named CMD
namedcmd

exportLemmaQelim :: Named CMD -> ProofStatus [EXPRESSION] ->
                    (Named CMD, ProofStatus [EXPRESSION])
exportLemmaQelim :: Named CMD
-> ProofStatus [EXPRESSION]
-> (Named CMD, ProofStatus [EXPRESSION])
exportLemmaQelim = Named CMD
-> ProofStatus [EXPRESSION]
-> (Named CMD, ProofStatus [EXPRESSION])
exportLemmaGeneric

-- | generates the lemma for cmd with result ProofStatus
exportLemmaFactor :: Named CMD -> ProofStatus [EXPRESSION] ->
                     (Named CMD, ProofStatus [EXPRESSION])
exportLemmaFactor :: Named CMD
-> ProofStatus [EXPRESSION]
-> (Named CMD, ProofStatus [EXPRESSION])
exportLemmaFactor = Named CMD
-> ProofStatus [EXPRESSION]
-> (Named CMD, ProofStatus [EXPRESSION])
exportLemmaGeneric

exportLemmaSolve :: Named CMD -> ProofStatus [EXPRESSION] ->
                    (Named CMD, ProofStatus [EXPRESSION])
exportLemmaSolve :: Named CMD
-> ProofStatus [EXPRESSION]
-> (Named CMD, ProofStatus [EXPRESSION])
exportLemmaSolve = Named CMD
-> ProofStatus [EXPRESSION]
-> (Named CMD, ProofStatus [EXPRESSION])
exportLemmaGeneric

exportLemmaSimplify :: Named CMD -> ProofStatus [EXPRESSION] ->
                       (Named CMD, ProofStatus [EXPRESSION])
exportLemmaSimplify :: Named CMD
-> ProofStatus [EXPRESSION]
-> (Named CMD, ProofStatus [EXPRESSION])
exportLemmaSimplify = Named CMD
-> ProofStatus [EXPRESSION]
-> (Named CMD, ProofStatus [EXPRESSION])
exportLemmaGeneric

exportLemmaAsk :: Named CMD -> ProofStatus [EXPRESSION] ->
                  (Named CMD, ProofStatus [EXPRESSION])
exportLemmaAsk :: Named CMD
-> ProofStatus [EXPRESSION]
-> (Named CMD, ProofStatus [EXPRESSION])
exportLemmaAsk = Named CMD
-> ProofStatus [EXPRESSION]
-> (Named CMD, ProofStatus [EXPRESSION])
exportLemmaGeneric

exportLemmaRemainder :: Named CMD -> ProofStatus [EXPRESSION] ->
                        (Named CMD, ProofStatus [EXPRESSION])
exportLemmaRemainder :: Named CMD
-> ProofStatus [EXPRESSION]
-> (Named CMD, ProofStatus [EXPRESSION])
exportLemmaRemainder = Named CMD
-> ProofStatus [EXPRESSION]
-> (Named CMD, ProofStatus [EXPRESSION])
exportLemmaGeneric


exportLemmaInt :: Named CMD -> ProofStatus [EXPRESSION] ->
                  (Named CMD, ProofStatus [EXPRESSION])
exportLemmaInt :: Named CMD
-> ProofStatus [EXPRESSION]
-> (Named CMD, ProofStatus [EXPRESSION])
exportLemmaInt = Named CMD
-> ProofStatus [EXPRESSION]
-> (Named CMD, ProofStatus [EXPRESSION])
exportLemmaGeneric