Hets - the Heterogeneous Tool Set

Copyright(c) Dominik Dietrich, DFKI Bremen, 2010
LicenseGPLv2 or higher, see LICENSE.txt
Portabilitynon-portable (uses type-expression in class instances)
Safe HaskellNone



Interface for Reduce CAS system.



class Session a where

A session is a process connection

Minimal complete definition

outp, inp


outp :: a -> Handle

inp :: a -> Handle

err :: a -> Maybe Handle

proch :: a -> Maybe ProcessHandle


Session (Handle, Handle)

The simplest session

Session (Handle, Handle, ProcessHandle)

Better use this session to properly close the connection

lookupRedShellCmd :: IO (Either String String)

Left String is success, Right String is failure

connectCAS :: String -> IO (Handle, Handle, Handle, ProcessHandle)

connects to the CAS, prepares the streams and sets initial options

disconnectCAS :: Session a => a -> IO ()

closes the connection to the CAS

sendToReduce :: Session a => a -> String -> IO ()

reduceS :: String

returns the name of the reduce prover

openReduceProofStatus :: String -> [EXPRESSION] -> ProofStatus [EXPRESSION]

returns a basic proof status for conjecture with name n where [EXPRESSION] represents the proof tree.



:: Ord pt 
=> String

name of the goal

-> pt 
-> ProofStatus pt 

infixOps :: [String]

those operators declared as infix in Reduce

exportExp :: EXPRESSION -> String

Exports an expression to Reduce format

exportReduce :: Named CMD -> String

exports command to Reduce Format

skipReduceLineNr :: String -> String

removes the newlines 4: from the beginning of the string

redOutputToExpression :: String -> Maybe EXPRESSION

try to get an EXPRESSION from a Reduce string

getNextResultOutput :: Handle -> IO String

reads characters from the specified output until the next result is complete, indicated by $ when using the maxima mode off nat;

evalString :: Session a => a -> String -> IO [EXPRESSION]

sends the given string to the CAS, reads the result and tries to parse it.

procString :: Session a => a -> String -> String -> IO (ProofStatus [EXPRESSION])

wrap evalString into a ProofStatus

casfactorExp :: Session a => a -> Named CMD -> IO (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])

factors a given expression over the reals

cassolve :: Session a => a -> Named CMD -> IO (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])

solves a single equation over the reals

cassimplify :: Session a => a -> Named CMD -> IO (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])

simplifies a given expression over the reals

casask :: Session a => a -> Named CMD -> IO (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])

asks value of a given expression

casremainder :: Session a => a -> Named CMD -> IO (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])

computes the remainder of a division

casint :: Session a => a -> Named CMD -> IO (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])

integrates the given expression

casqelim :: Session a => a -> Named CMD -> IO (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])

performs quantifier elimination of a given expression

casDeclareOperators :: Session a => a -> [EXPRESSION] -> IO ()

declares an operator, such that it can used infix/prefix in CAS

casDeclareEquation :: Session a => a -> CMD -> IO ()

declares an equation x := exp

exportLemmaFactor :: Named CMD -> ProofStatus [EXPRESSION] -> (Named CMD, ProofStatus [EXPRESSION])

generates the lemma for cmd with result ProofStatus