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)
Safe Haskell	None

CSL.Reduce_Interface

Description

Interface for Reduce CAS system.

Synopsis

Documentation

class Session a where

A session is a process connection

Minimal complete definition

outp, inp

Methods

outp :: a -> Handle

inp :: a -> Handle

err :: a -> Maybe Handle

proch :: a -> Maybe ProcessHandle

Instances

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.

closedReduceProofStatus

Arguments

:: Ord pt
=> String	name of the goal
-> pt
-> ProofStatus pt

exportExps :: [EXPRESSION] -> String

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

cslReduceDefaultMapping :: [(OPNAME, 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;

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

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

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

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

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

generates the lemma for cmd with result ProofStatus

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

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

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

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

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