c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann{-# LANGUAGE FlexibleInstances, FlexibleContexts, TypeSynonymInstances

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann , UndecidableInstances, OverlappingInstances, MultiParamTypeClasses #-}

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann{- |

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuModule : $Header$

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel HausmannDescription : Reduce instance for the AssignmentStore class

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel HausmannCopyright : (c) Ewaryst Schulz, DFKI Bremen 2010

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel HausmannLicense : GPLv2 or higher, see LICENSE.txt

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel HausmannMaintainer : Ewaryst.Schulz@dfki.de

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel HausmannStability : experimental

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel HausmannPortability : non-portable (various glasgow extensions)

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel HausmannReduce as AssignmentStore

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann-}

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmannmodule CSL.ReduceInterpreter where

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmannimport Common.ProverTools (missingExecutableInPath)

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmannimport Common.Utils (getEnvDef, trimLeft)

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmannimport Common.IOS

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmannimport Common.ResultT

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmannimport CSL.Reduce_Interface ( evalString, exportExp, connectCAS, disconnectCAS

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann , lookupRedShellCmd, Session (..), cslReduceDefaultMapping)

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmannimport CSL.AS_BASIC_CSL

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmannimport CSL.Parse_AS_Basic (parseResult)

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmannimport CSL.Transformation

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmannimport CSL.Interpreter

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann-- the process communication interface

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmannimport qualified Interfaces.Process as PC

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann

d024d9de9b6e7a7cfd72ef72d8efb0e57da5a01bChristian Maederimport Control.Monad.Trans (MonadTrans (..), MonadIO (..))

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmannimport Control.Monad.State (MonadState (..))

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmannimport Data.Maybe

f04dbee44fb71ec868f409099d983f7f3771e0d2Daniel Hausmannimport System.IO (Handle)

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmannimport System.Process (ProcessHandle)

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmannimport System.Exit (ExitCode)

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmannimport Prelude hiding (lookup)

d024d9de9b6e7a7cfd72ef72d8efb0e57da5a01bChristian Maeder

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann-- ----------------------------------------------------------------------

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann-- * Reduce Calculator Instances

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann-- ----------------------------------------------------------------------

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmanndata ReduceInterpreter = ReduceInterpreter { inh :: Handle

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann , outh ::Handle

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann , ph :: ProcessHandle

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann , varcounter :: Int }

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann-- | ReduceInterpreter with Translator based on the CommandState

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmanndata RITrans = RITrans { getBMap :: BMap

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann , getRI :: PC.CommandState }

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann-- Types for two alternative reduce interpreter

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann

093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann-- Reds as (Red)uce (s)tandard interface

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmanntype RedsIO = ResultT (IOS ReduceInterpreter)

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann-- Redc as (Red)uce (c)ommand interface (it is built on CommandState)

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmanntype RedcIO = ResultT (IOS RITrans)

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmanninstance AssignmentStore RedsIO where

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann assign = redAssign evalRedsString redsTransS return

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann lookup = redLookup evalRedsString redsTransS

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann eval = redEval evalRedsString return

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann check = redCheck evalRedsString return

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann names = error "ReduceInterpreter as CS: names are unsupported"

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmanninstance VarGen RedsIO where

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann genVar = do

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann s <- get

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann let i = varcounter s

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann put $ s { varcounter =i + 1 }

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann return $ "?" ++ show i

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmanninstance AssignmentStore RedcIO where

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann assign = redAssign evalRedcString redcTransS redcTransE

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann lookup = redLookup evalRedcString redcTransS

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann eval = redEval evalRedcString redcTransE

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann check = redCheck evalRedcString redcTransE

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann names = get >>= return . SMem . getBMap

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann

d024d9de9b6e7a7cfd72ef72d8efb0e57da5a01bChristian Maederinstance VarGen RedcIO where

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann genVar = do

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann s <- get

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann let i = newkey $ getBMap s

093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann put $ s { getBMap = (getBMap s) { newkey = i + 1 } }

093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann return $ "?" ++ show i

093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann

093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann-- ----------------------------------------------------------------------

093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann-- * Reduce syntax functions

093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann-- ----------------------------------------------------------------------

093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann

093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel HausmannprintAssignment :: String -> EXPRESSION -> String

093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel HausmannprintAssignment n e = concat [n, ":=", exportExp e, ";"]

093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann

093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel HausmannprintEvaluation :: EXPRESSION -> String

093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel HausmannprintEvaluation e = exportExp e ++ ";"

093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann

093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel HausmannprintLookup :: String -> String

093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel HausmannprintLookup n = n ++ ";"

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann

093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann-- As reduce does not support boolean expressions as first class citizens

093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann-- we encode them in an if-stmt and transform the numeric response back.

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel HausmannprintBooleanExpr :: EXPRESSION -> String

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel HausmannprintBooleanExpr e = concat [ "on rounded;"

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann , " if "

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann , exportExp e, " then 1 else 0;"

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann , " off rounded;"

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann ]

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel HausmanngetBooleanFromExpr :: EXPRESSION -> Bool

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel HausmanngetBooleanFromExpr (Int 1 _) = True

093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel HausmanngetBooleanFromExpr (Int 0 _) = False

093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel HausmanngetBooleanFromExpr e =

093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann error $ "getBooleanFromExpr: can't translate expression to boolean: "

093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann ++ show e

093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann-- ----------------------------------------------------------------------

093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann-- * Generic Communication Interface

093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann-- ----------------------------------------------------------------------

093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann

c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann{- |

The generic interface abstracts over the concrete evaluation function

-}

redAssign :: (AssignmentStore s, MonadResult s) =>

(String -> s [EXPRESSION])

-> (ConstantName -> s String)

-> (EXPRESSION -> s EXPRESSION)

-> ConstantName -> EXPRESSION -> s ()

redAssign ef trans transE n e = do

e' <- transE e

n' <- trans n

ef $ printAssignment n' e'

return ()

redLookup :: (AssignmentStore s, MonadResult s) =>

(String -> s [EXPRESSION])

-> (ConstantName -> s String)

-> ConstantName -> s (Maybe EXPRESSION)

redLookup ef trans n = do

n' <- trans n

el <- ef $ printLookup n'

return $ listToMaybe el

-- we don't want to return nothing on id-lookup: "x; --> x"

-- if e == mkOp n [] then return Nothing else return $ Just e

redEval :: (AssignmentStore s, MonadResult s) =>

(String -> s [EXPRESSION])

-> (EXPRESSION -> s EXPRESSION)

-> EXPRESSION -> s EXPRESSION

redEval ef trans e = do

e' <- trans e

el <- ef $ printEvaluation e'

if null el

then error $ "redEval: expression " ++ show e' ++ " couldn't be evaluated"

else return $ head el

redCheck :: (AssignmentStore s, MonadResult s) =>

(String -> s [EXPRESSION])

-> (EXPRESSION -> s EXPRESSION)

-> EXPRESSION -> s Bool

redCheck ef trans e = do

e' <- trans e

el <- ef $ printBooleanExpr e'

if null el

then error $ "redCheck: expression " ++ show e' ++ " couldn't be evaluated"

else return $ getBooleanFromExpr $ head el

-- ----------------------------------------------------------------------

-- * The Standard Communication Interface

-- ----------------------------------------------------------------------

instance Session ReduceInterpreter where

inp = inh

outp = outh

proch = Just . ph

redsTransS :: ConstantName -> RedsIO String

redsTransS = return . show

evalRedsString :: String -> RedsIO [EXPRESSION]

evalRedsString s = do

r <- get

liftIO $ evalString r s

redsInit :: IO ReduceInterpreter

redsInit = do

putStr "Connecting CAS.."

reducecmd <- getEnvDef "HETS_REDUCE" "redcsl"

-- check that prog exists

noProg <- missingExecutableInPath reducecmd

if noProg

then error $ "Could not find reduce under " ++ reducecmd

else do

(inpt, out, _, pid) <- connectCAS reducecmd

return

$ ReduceInterpreter { inh = inpt, outh = out, ph = pid, varcounter = 1 }

redsExit :: ReduceInterpreter -> IO ()

redsExit = disconnectCAS

-- ----------------------------------------------------------------------

-- * An alternative Communication Interface

-- ----------------------------------------------------------------------

wrapCommand :: IOS PC.CommandState a -> IOS RITrans a

wrapCommand ios = do

r <- get

let map' x = r { getRI = x }

stmap map' getRI ios

-- | A direct way to communicate with Reduce

redcDirect :: RITrans -> String -> IO String

redcDirect rit s = do

(res, _) <- runIOS (getRI rit) (PC.call 0.5 s)

return res

redcTransE :: EXPRESSION -> RedcIO EXPRESSION

redcTransE e = do

r <- get

let bm = getBMap r

(bm', e') = translateEXPRESSION bm e

put r { getBMap = bm' }

return e'

redcTransS :: ConstantName -> RedcIO String

redcTransS s = do

r <- get

let bm = getBMap r

(bm', s') = lookupOrInsert bm $ Left s

put r { getBMap = bm' }

return s'

evalRedcString :: String -> RedcIO [EXPRESSION]

evalRedcString s = do

-- 0.09 seconds is a critical value for the accepted response time of Reduce

res <- lift $ wrapCommand $ PC.call 0.5 s

r <- get

let bm = getBMap r

trans = revtranslateEXPRESSION bm

-- don't need to skip the reducelinenr here, because the Command-Interface

-- cleans the outpipe before sending (hence removes the reduce line nr)

return $ map trans $ maybeToList $ parseResult $ trimLeft res

-- | init the reduce communication

redcInit :: Int -- ^ Verbosity level

-> IO RITrans

redcInit v = do

rc <- lookupRedShellCmd

case rc of

Left redcmd -> do

cs <- PC.start redcmd v Nothing

(_, cs') <- runIOS cs $ PC.send $ "off nat; load redlog; "

++ "rlset reals; " --on rounded; precision 30;"

return RITrans { getBMap = initWithDefault cslReduceDefaultMapping

, getRI = cs' }

_ -> error "Could not find reduce shell command!"

redcExit :: RITrans -> IO (Maybe ExitCode)

redcExit r = do

(ec, _) <- runIOS (getRI r) $ PC.close $ Just "quit;"

return ec