8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster{-# LANGUAGE FlexibleInstances #-}

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster{- |

8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterModule : $Header$

8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterDescription : interface to Reduce CAS

8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterCopyright : (c) Dominik Dietrich, DFKI Bremen, 2010

8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterLicense : GPLv2 or higher, see LICENSE.txt

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster

8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterMaintainer : Dominik.Dietrich@dfki.de

8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterStability : provisional

8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterPortability : non-portable (uses type-expression in class instances)

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster

8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterInterface for Reduce CAS system.

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-}

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster

8af80418ba1ec431c8027fa9668e5678658d3611Allan Fostermodule CSL.Reduce_Interface where

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster

8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterimport Common.AS_Annotation

8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterimport Common.Id

8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterimport Common.ProverTools (missingExecutableInPath)

8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterimport Common.Utils (getEnvDef)

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster

8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterimport Logic.Prover

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster

8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterimport CSL.AS_BASIC_CSL

8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterimport CSL.ASUtils

8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterimport CSL.Parse_AS_Basic

8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterimport CSL.Lemma_Export

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster

8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterimport Control.Monad (replicateM_)

8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterimport Data.Time (midnight)

8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterimport Data.Maybe (maybeToList)

8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterimport Data.List (intercalate)

8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterimport qualified Data.Map as Map

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster

8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterimport System.IO

8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterimport System.Process

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster{- ----------------------------------------------------------------------

8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterConnection handling

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster---------------------------------------------------------------------- -}

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- | A session is a process connection

8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterclass Session a where

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster outp :: a -> Handle

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster inp :: a -> Handle

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster err :: a -> Maybe Handle

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster err = const Nothing

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster proch :: a -> Maybe ProcessHandle

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster proch = const Nothing

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- | The simplest session

8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterinstance Session (Handle, Handle) where

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster inp = fst

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster outp = snd

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- | Better use this session to properly close the connection

8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterinstance Session (Handle, Handle, ProcessHandle) where

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster inp (x, _, _) = x

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster outp (_, x, _) = x

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster proch (_, _, x) = Just x

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- | Left String is success, Right String is failure

8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterlookupRedShellCmd :: IO (Either String String)

8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterlookupRedShellCmd = do

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster reducecmd <- getEnvDef "HETS_REDUCE" "redcsl"

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- check that prog exists

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster noProg <- missingExecutableInPath reducecmd

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster let f = if noProg then Right else Left

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster return $ f reducecmd

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- | connects to the CAS, prepares the streams and sets initial options

8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterconnectCAS :: String -> IO (Handle, Handle, Handle, ProcessHandle)

8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterconnectCAS reducecmd = do

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster putStrLn "succeeded"

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster (inpt, out, errh, pid) <- runInteractiveCommand $ reducecmd ++ " -w"

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster hSetBuffering out NoBuffering

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster hSetBuffering inpt LineBuffering

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster hPutStrLn inpt "off nat;"

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster hPutStrLn inpt "load redlog;"

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster hPutStrLn inpt "rlset reals;"

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- read 7 lines

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster replicateM_ 7 $ hGetLine out

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster putStrLn "done"

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster return (inpt, out, errh, pid)

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- | closes the connection to the CAS

8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterdisconnectCAS :: Session a => a -> IO ()

8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterdisconnectCAS s = do

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster hPutStrLn (inp s) "quit;"

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster case proch s of

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Nothing -> return ()

8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster

{- this is always better, because it closes also the shell-process,

hence use a Session-variant with ProcessHandle! -}

Just ph -> waitForProcess ph >> return ()

putStrLn "CAS disconnected"

return ()

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

sendToReduce sess = hPutStrLn (inp sess)

{- ----------------------------------------------------------------------

Prover specific

---------------------------------------------------------------------- -}

-- | returns the name of the reduce prover

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 n = openProofStatus n reduceS

closedReduceProofStatus :: Ord pt => String -- ^ name of the goal

-> pt -> ProofStatus pt

closedReduceProofStatus goalname proof_tree =

ProofStatus

{ goalName = goalname

, goalStatus = Proved True

, usedAxioms = []

, usedProver = reduceS

, proofTree = proof_tree

, usedTime = midnight

, tacticScript = TacticScript "" }

{-

For Quantifier Elimination:

off nat; -- pretty-printing switch

load redlog;

rlset reals;

rlqe(exp...);

-}

{- ----------------------------------------------------------------------

Reduce Pretty Printing

---------------------------------------------------------------------- -}

exportExps :: [EXPRESSION] -> String

exportExps l = intercalate "," $ map exportExp l

-- | those operators declared as infix in Reduce

infixOps :: [String]

infixOps = [ "+", "-", "/", "**", "^", "=", "<=", ">=", "<", ">", "*", "and"

, "impl", "or"]

-- | Exports an expression to Reduce format

exportExp :: EXPRESSION -> String

exportExp (Var token) = tokStr token

exportExp (Op s _ exps@[e1, e2] _)

| elem (simpleName s) infixOps =

concat ["(", exportExp e1, simpleName s, exportExp e2, ")"]

| otherwise = concat [simpleName s, "(", exportExps exps, ")"]

exportExp (Op s _ [] _) = simpleName s

exportExp (Op s _ exps _) = concat [simpleName s, "(", exportExps exps, ")"]

exportExp (List exps _) = "{" ++ exportExps exps ++ "}"

exportExp (Int i _) = show i

exportExp (Rat d _) = show d

exportExp (Interval l r _) = concat [ "[", show l, ",", show r, "]" ]

-- exportExp e = error $ "exportExp: expression not supported: " ++ show e

-- | exports command to Reduce Format

exportReduce :: Named CMD -> String

exportReduce namedcmd = case sentence namedcmd of

Cmd "simplify" exps -> exportExp $ head exps

Cmd "ask" exps -> exportExp $ head exps

Cmd cmd exps -> cmd ++ "(" ++ exportExps exps ++ ")"

_ -> 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 s = dropWhile (`elem` " \n") $ tail

$ dropWhile (/= ':') s

-- | try to get an EXPRESSION from a Reduce string

redOutputToExpression :: String -> Maybe EXPRESSION

redOutputToExpression = parseExpression () . skipReduceLineNr

{- ----------------------------------------------------------------------

Reduce Commands

---------------------------------------------------------------------- -}

cslReduceDefaultMapping :: [(OPNAME, String)]

cslReduceDefaultMapping =

let idmapping = map (\ x -> (x, show x))

in (OP_pow, "**") :

idmapping (Map.keys $ Map.delete OP_pow 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 out = do

b <- hIsEOF out

if b then return "" else do

c <- hGetChar out

if c == '$' then return [] else do

r <- getNextResultOutput out

return (c : r)

procCmd :: Session a => a -> Named CMD

-> IO (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])

procCmd sess cmd = case cmdstring of

"simplify" -> cassimplify sess cmd

"ask" -> casask sess cmd

"divide" -> casremainder sess cmd

"rlqe" -> casqelim sess cmd

"factorize" -> casfactorExp sess cmd

"int" -> casint sess cmd

"solve" -> cassolve sess cmd

_ -> error "Command not supported"

where Cmd cmdstring _ = sentence cmd

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

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

evalString sess s = do

putStrLn $ "Send CAS cmd " ++ s

hPutStrLn (inp sess) s

res <- getNextResultOutput (outp sess)

putStrLn $ "Result is " ++ res

putStrLn $ "Parsing of --" ++ skipReduceLineNr res ++ "-- yields "

++ show (redOutputToExpression res)

return $ maybeToList $ redOutputToExpression res

-- | wrap evalString into a ProofStatus

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

procString h axname s = do

res <- evalString h s

let f = if null res then openReduceProofStatus else closedReduceProofStatus

return $ f axname res

-- | factors a given expression over the reals

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

[(Named CMD, ProofStatus [EXPRESSION])])

casfactorExp sess cmd =

do

proofstatus <- procString sess (senAttr cmd) $ exportReduce cmd ++ ";"

return (proofstatus, [exportLemmaFactor cmd proofstatus])

-- | solves a single equation over the reals

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

[(Named CMD, ProofStatus [EXPRESSION])])

cassolve sess cmd =

do

proofstatus <- procString sess (senAttr cmd) $ exportReduce cmd ++ ";"

return (proofstatus, [])

-- | simplifies a given expression over the reals

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

[(Named CMD, ProofStatus [EXPRESSION])])

cassimplify sess cmd = do

proofstatus <- procString sess (senAttr cmd) $ exportReduce cmd ++ ";"

return (proofstatus, [exportLemmaSimplify cmd proofstatus])

-- | asks value of a given expression

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

[(Named CMD, ProofStatus [EXPRESSION])])

casask sess cmd = do

proofstatus <- procString sess (senAttr cmd) $ exportReduce cmd ++ ";"

return (proofstatus, [exportLemmaAsk cmd proofstatus])

-- | computes the remainder of a division

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

[(Named CMD, ProofStatus [EXPRESSION])])

casremainder sess cmd =

do

proofstatus <- procString sess (senAttr cmd) $ exportReduce

(makeNamed (senAttr cmd) (Cmd "divide" args)) ++ ";"

return (proofstatus, [exportLemmaRemainder cmd proofstatus])

where Cmd _ args = sentence cmd

-- | integrates the given expression

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

[(Named CMD, ProofStatus [EXPRESSION])])

casint sess cmd =

do

proofstatus <- procString sess (senAttr cmd) $ exportReduce cmd ++ ";"

return (proofstatus, [exportLemmaInt cmd proofstatus])

-- | performs quantifier elimination of a given expression

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

[(Named CMD, ProofStatus [EXPRESSION])])

casqelim sess cmd =

do

proofstatus <- procString sess (senAttr cmd) $ exportReduce cmd ++ ";"

return (proofstatus, [exportLemmaQelim cmd proofstatus])

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

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

casDeclareOperators sess varlist = do

hPutStrLn (inp sess) $ "operator " ++ exportExps varlist ++ ";"

hGetLine (outp sess)

return ()

-- | declares an equation x := exp

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

casDeclareEquation sess (Ass c def) =

do

let e1 = exportExp $ opDeclToOp c

e2 = exportExp def

putStrLn $ e1 ++ ":=" ++ e2

hPutStrLn (inp sess) $ e1 ++ ":=" ++ e2 ++ ";"

res <- getNextResultOutput (outp sess)

putStrLn $ "Declaration Result: " ++ res

return ()

casDeclareEquation _ _ =

error "casDeclareEquation: not implemented for this case" -- TODO: implement

{- ----------------------------------------------------------------------

Reduce Lemma Export

---------------------------------------------------------------------- -}

exportLemmaGeneric :: Named CMD -> ProofStatus [EXPRESSION] ->

(Named CMD, ProofStatus [EXPRESSION])

exportLemmaGeneric namedcmd ps =

(makeNamed lemmaname lemma, closedReduceProofStatus lemmaname [mkOp "Proof" []])

where Cmd _ exps = sentence namedcmd

lemma = Cmd "=" [head exps, head (proofTree ps)]

lemmaname = ganame namedcmd

exportLemmaQelim :: Named CMD -> ProofStatus [EXPRESSION] ->

(Named CMD, ProofStatus [EXPRESSION])

exportLemmaQelim = exportLemmaGeneric

-- | generates the lemma for cmd with result ProofStatus

exportLemmaFactor :: Named CMD -> ProofStatus [EXPRESSION] ->

(Named CMD, ProofStatus [EXPRESSION])

exportLemmaFactor = exportLemmaGeneric

exportLemmaSolve :: Named CMD -> ProofStatus [EXPRESSION] ->

(Named CMD, ProofStatus [EXPRESSION])

exportLemmaSolve = exportLemmaGeneric

exportLemmaSimplify :: Named CMD -> ProofStatus [EXPRESSION] ->

(Named CMD, ProofStatus [EXPRESSION])

exportLemmaSimplify = exportLemmaGeneric

exportLemmaAsk :: Named CMD -> ProofStatus [EXPRESSION] ->

(Named CMD, ProofStatus [EXPRESSION])

exportLemmaAsk = exportLemmaGeneric

exportLemmaRemainder :: Named CMD -> ProofStatus [EXPRESSION] ->

(Named CMD, ProofStatus [EXPRESSION])

exportLemmaRemainder = exportLemmaGeneric

exportLemmaInt :: Named CMD -> ProofStatus [EXPRESSION] ->

(Named CMD, ProofStatus [EXPRESSION])

exportLemmaInt = exportLemmaGeneric