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

Session (Handle, Handle) Source #

The simplest session

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

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

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;

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

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

generates the lemma for cmd with result ProofStatus