Hets - the Heterogeneous Tool Set
Copyright(c) Dominik Dietrich DFKI Bremen 2010
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerDominik.Dietrich@dfki.de
Stabilityprovisional
Portabilitynon-portable (uses type-expression in class instances)
Safe HaskellNone

CSL.Reduce_Interface

Description

Interface for Reduce CAS system.

Synopsis

Documentation

class Session a where Source #

A session is a process connection

Minimal complete definition

outp, inp

Methods

outp :: a -> Handle Source #

inp :: a -> Handle Source #

err :: a -> Maybe Handle Source #

proch :: a -> Maybe ProcessHandle Source #

Instances

Instances details
Session (Handle, Handle) Source #

The simplest session

Instance details

Defined in CSL.Reduce_Interface

Methods

outp :: (Handle, Handle) -> Handle Source #

inp :: (Handle, Handle) -> Handle Source #

err :: (Handle, Handle) -> Maybe Handle Source #

proch :: (Handle, Handle) -> Maybe ProcessHandle Source #

Session (Handle, Handle, ProcessHandle) Source #

Better use this session to properly close the connection

Instance details

Defined in CSL.Reduce_Interface

Methods

outp :: (Handle, Handle, ProcessHandle) -> Handle Source #

inp :: (Handle, Handle, ProcessHandle) -> Handle Source #

err :: (Handle, Handle, ProcessHandle) -> Maybe Handle Source #

proch :: (Handle, Handle, ProcessHandle) -> Maybe ProcessHandle Source #

lookupRedShellCmd :: IO (Either String String) Source #

Left String is success, Right String is failure

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

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

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

closes the connection to the CAS

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

reduceS :: String Source #

returns the name of the reduce prover

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

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

closedReduceProofStatus Source #

Arguments

:: Ord pt 
=> String

name of the goal

-> pt 
-> ProofStatus pt 

exportExps :: [EXPRESSION] -> String Source #

infixOps :: [String] Source #

those operators declared as infix in Reduce

exportExp :: EXPRESSION -> String Source #

Exports an expression to Reduce format

exportReduce :: Named CMD -> String Source #

exports command to Reduce Format

skipReduceLineNr :: String -> String Source #

removes the newlines 4: from the beginning of the string

redOutputToExpression :: String -> Maybe EXPRESSION Source #

try to get an EXPRESSION from a Reduce string

cslReduceDefaultMapping :: [(OPNAME, String)] Source #

getNextResultOutput :: Handle -> IO String Source #

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])]) Source #

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

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

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

wrap evalString into a ProofStatus

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

factors a given expression over the reals

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

solves a single equation over the reals

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

simplifies a given expression over the reals

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

asks value of a given expression

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

computes the remainder of a division

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

integrates the given expression

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

performs quantifier elimination of a given expression

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

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

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

declares an equation x := exp

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

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

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

generates the lemma for cmd with result ProofStatus

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

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

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

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

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