7db058a7846888b8823fca9e8135f395265ef1d8nilgun{-# LANGUAGE FlexibleContexts, TypeSynonymInstances #-}

7db058a7846888b8823fca9e8135f395265ef1d8nilgun{- |

fd9abdda70912b99b24e3bf1a38f26fde908a74cndModule : $Header$

fd9abdda70912b99b24e3bf1a38f26fde908a74cndDescription : Mathematica instance for the AssignmentStore class

fd9abdda70912b99b24e3bf1a38f26fde908a74cndCopyright : (c) Ewaryst Schulz, DFKI Bremen 2010

7db058a7846888b8823fca9e8135f395265ef1d8nilgunLicense : GPLv2 or higher, see LICENSE.txt

7db058a7846888b8823fca9e8135f395265ef1d8nilgun

7db058a7846888b8823fca9e8135f395265ef1d8nilgunMaintainer : Ewaryst.Schulz@dfki.de

7db058a7846888b8823fca9e8135f395265ef1d8nilgunStability : experimental

96ad5d81ee4a2cc66a4ae19893efc8aa6d06fae7jailletcPortability : non-portable (via imports)

7db058a7846888b8823fca9e8135f395265ef1d8nilgun

7db058a7846888b8823fca9e8135f395265ef1d8nilgunMathematica as AssignmentStore based on the Mathlink interface

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen-}

2e545ce2450a9953665f701bb05350f0d3f26275nd

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowenmodule CSL.MathematicaInterpreter where

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen

7db058a7846888b8823fca9e8135f395265ef1d8nilgunimport Common.ProverTools (missingExecutableInPath)

7db058a7846888b8823fca9e8135f395265ef1d8nilgunimport Common.Utils (getEnvDef, trimLeft)

7db058a7846888b8823fca9e8135f395265ef1d8nilgunimport Common.Doc

af33a4994ae2ff15bc67d19ff1a7feb906745bf8rbowenimport Common.DocUtils

3f08db06526d6901aa08c110b5bc7dde6bc39905ndimport Common.IOS

7db058a7846888b8823fca9e8135f395265ef1d8nilgun

7db058a7846888b8823fca9e8135f395265ef1d8nilgunimport CSL.AS_BASIC_CSL

7db058a7846888b8823fca9e8135f395265ef1d8nilgunimport CSL.Parse_AS_Basic (parseExpression)

3f08db06526d6901aa08c110b5bc7dde6bc39905ndimport CSL.Interpreter

7db058a7846888b8823fca9e8135f395265ef1d8nilgunimport CSL.Transformation

7db058a7846888b8823fca9e8135f395265ef1d8nilgunimport CSL.Verification

7db058a7846888b8823fca9e8135f395265ef1d8nilgunimport CSL.Analysis

d3bd91523e4565551991605fb157fea59c3610e2gryzor

f086b4b402fa9a2fefc7dda85de2a3cc1cd0a654rjung-- the process communication interface

7db058a7846888b8823fca9e8135f395265ef1d8nilgunimport qualified Interfaces.Process as PC

50cb7e2b30597f481fee57bac945190f06ebcc58jorton

7db058a7846888b8823fca9e8135f395265ef1d8nilgunimport Control.Monad

7db058a7846888b8823fca9e8135f395265ef1d8nilgun--import Control.Monad.Trans (MonadTrans (..), MonadIO (..))

7db058a7846888b8823fca9e8135f395265ef1d8nilgunimport Control.Monad.Error (ErrorT(..), MonadError (..))

7db058a7846888b8823fca9e8135f395265ef1d8nilgunimport Control.Monad.State.Class

7db058a7846888b8823fca9e8135f395265ef1d8nilgunimport Control.Monad.Reader

7db058a7846888b8823fca9e8135f395265ef1d8nilgun

7db058a7846888b8823fca9e8135f395265ef1d8nilgunimport Data.List hiding (lookup)

50cb7e2b30597f481fee57bac945190f06ebcc58jortonimport qualified Data.Set as Set

50cb7e2b30597f481fee57bac945190f06ebcc58jortonimport Data.Maybe

e10f97d0097170c9843f6cf335dfeef0b44cd83crbowenimport System.Exit (ExitCode)

50cb7e2b30597f481fee57bac945190f06ebcc58jortonimport System.IO

7db058a7846888b8823fca9e8135f395265ef1d8nilgun

c9f4eb2763c1d6ba9a3d26828e1729e476d0bb1epctonyimport Prelude hiding (lookup)

50cb7e2b30597f481fee57bac945190f06ebcc58jorton

c9f4eb2763c1d6ba9a3d26828e1729e476d0bb1epctony

7db058a7846888b8823fca9e8135f395265ef1d8nilgun-- ----------------------------------------------------------------------

7db058a7846888b8823fca9e8135f395265ef1d8nilgun-- * Tests

7db058a7846888b8823fca9e8135f395265ef1d8nilgun-- ----------------------------------------------------------------------

50cb7e2b30597f481fee57bac945190f06ebcc58jorton

7db058a7846888b8823fca9e8135f395265ef1d8nilgun

7db058a7846888b8823fca9e8135f395265ef1d8nilgun

7db058a7846888b8823fca9e8135f395265ef1d8nilgun

50cb7e2b30597f481fee57bac945190f06ebcc58jorton

7db058a7846888b8823fca9e8135f395265ef1d8nilgun-- ----------------------------------------------------------------------

7db058a7846888b8823fca9e8135f395265ef1d8nilgun-- * Mathematica Types and Instances

7db058a7846888b8823fca9e8135f395265ef1d8nilgun-- ----------------------------------------------------------------------

50cb7e2b30597f481fee57bac945190f06ebcc58jorton

7db058a7846888b8823fca9e8135f395265ef1d8nilguntype ConnectInfo = (PC.CommandState, PC.DTime)

7db058a7846888b8823fca9e8135f395265ef1d8nilgun

50cb7e2b30597f481fee57bac945190f06ebcc58jorton-- | MathematicaInterpreter with Translator based on the Mathlink interface

e10f97d0097170c9843f6cf335dfeef0b44cd83crbowentype MathState = ASState ConnectInfo

7db058a7846888b8823fca9e8135f395265ef1d8nilgun

7db058a7846888b8823fca9e8135f395265ef1d8nilgunupdateCS :: PC.CommandState -> ConnectInfo -> ConnectInfo

7db058a7846888b8823fca9e8135f395265ef1d8nilgunupdateCS cs (_, dt) = (cs, dt)

c44eeebd065e2c8cd028016b45c58afb480aaf8fdruggeri

c44eeebd065e2c8cd028016b45c58afb480aaf8fdruggeriupdateDT :: PC.DTime -> ConnectInfo -> ConnectInfo

c44eeebd065e2c8cd028016b45c58afb480aaf8fdruggeriupdateDT dt (cs, _) = (cs, dt)

c44eeebd065e2c8cd028016b45c58afb480aaf8fdruggeri

c44eeebd065e2c8cd028016b45c58afb480aaf8fdruggerigetChannelTimeout :: MathState -> PC.DTime

7db058a7846888b8823fca9e8135f395265ef1d8nilgungetChannelTimeout = snd . getConnectInfo

7db058a7846888b8823fca9e8135f395265ef1d8nilgun

7db058a7846888b8823fca9e8135f395265ef1d8nilgunsetChannelTimeout :: PC.DTime -> MathState -> MathState

7db058a7846888b8823fca9e8135f395265ef1d8nilgunsetChannelTimeout dt = fmap (updateDT dt)

c44eeebd065e2c8cd028016b45c58afb480aaf8fdruggeri

7db058a7846888b8823fca9e8135f395265ef1d8nilgungetMI :: MathState -> PC.CommandState

7db058a7846888b8823fca9e8135f395265ef1d8nilgungetMI = fst . getConnectInfo

7db058a7846888b8823fca9e8135f395265ef1d8nilgun

4aa603e6448b99f9371397d439795c91a93637eandsetMI :: PC.CommandState -> MathState -> MathState

17ade6df5ec233536985eb1c130a906c725dd614humbedoohsetMI cs = fmap (updateCS cs)

17ade6df5ec233536985eb1c130a906c725dd614humbedooh

a99c5d4cc3cab6a62b04d52000dbc22ce1fa2d94coar-- Mathematica interface, built on CommandState

a99c5d4cc3cab6a62b04d52000dbc22ce1fa2d94coartype MathematicaIO = ErrorT ASError (IOS MathState)

a99c5d4cc3cab6a62b04d52000dbc22ce1fa2d94coar

a99c5d4cc3cab6a62b04d52000dbc22ce1fa2d94coarinstance AssignmentStore MathematicaIO where

4aa603e6448b99f9371397d439795c91a93637eand assign = mathematicaAssign (evalMathematicaString True) mathematicaTransS mathematicaTransVarE

e487d6c09669296f94a5190cc34586a98e624a00nd assigns =

17ade6df5ec233536985eb1c130a906c725dd614humbedooh mathematicaAssigns (evalMathematicaString False []) mathematicaTransS mathematicaTransVarE

4aa603e6448b99f9371397d439795c91a93637eand lookup = mathematicaLookup (evalMathematicaString True []) mathematicaTransS

17ade6df5ec233536985eb1c130a906c725dd614humbedooh eval = mathematicaEval (evalMathematicaString True []) mathematicaTransE

17ade6df5ec233536985eb1c130a906c725dd614humbedooh check = mathematicaCheck (evalMathematicaString True []) mathematicaTransE

a99c5d4cc3cab6a62b04d52000dbc22ce1fa2d94coar names = get >>= return . SMem . getBMap

a99c5d4cc3cab6a62b04d52000dbc22ce1fa2d94coar evalRaw s = get >>= liftIO . flip (mathematicaDirect True) s

a99c5d4cc3cab6a62b04d52000dbc22ce1fa2d94coar

a99c5d4cc3cab6a62b04d52000dbc22ce1fa2d94coar getUndefinedConstants e = do

4aa603e6448b99f9371397d439795c91a93637eand adg <- gets depGraph

e487d6c09669296f94a5190cc34586a98e624a00nd let g = isNothing . depGraphLookup adg

7db058a7846888b8823fca9e8135f395265ef1d8nilgun return $ Set.filter g $ Set.map SimpleConstant $ setOfUserDefined e

7db058a7846888b8823fca9e8135f395265ef1d8nilgun

7db058a7846888b8823fca9e8135f395265ef1d8nilgun genNewKey = do

7db058a7846888b8823fca9e8135f395265ef1d8nilgun mit <- get

50cb7e2b30597f481fee57bac945190f06ebcc58jorton let (bm, i) = genKey $ getBMap mit

7153ff43420a22c7f6213937b6b210f25d02c464rbowen put mit { getBMap = bm }

7db058a7846888b8823fca9e8135f395265ef1d8nilgun return i

7db058a7846888b8823fca9e8135f395265ef1d8nilgun

7db058a7846888b8823fca9e8135f395265ef1d8nilgun getDepGraph = gets depGraph

7db058a7846888b8823fca9e8135f395265ef1d8nilgun updateConstant n def =

50cb7e2b30597f481fee57bac945190f06ebcc58jorton let f gr = updateGraph gr n

7db058a7846888b8823fca9e8135f395265ef1d8nilgun $ DepGraphAnno { annoDef = def

c9f4eb2763c1d6ba9a3d26828e1729e476d0bb1epctony , annoVal = () }

7db058a7846888b8823fca9e8135f395265ef1d8nilgun mf mit = mit { depGraph = f $ depGraph mit }

c9f4eb2763c1d6ba9a3d26828e1729e476d0bb1epctony in modify mf

7db058a7846888b8823fca9e8135f395265ef1d8nilgun

50cb7e2b30597f481fee57bac945190f06ebcc58jortoninstance VCGenerator MathematicaIO where

7db058a7846888b8823fca9e8135f395265ef1d8nilgun addVC ea e = do

50cb7e2b30597f481fee57bac945190f06ebcc58jorton let

7db058a7846888b8823fca9e8135f395265ef1d8nilgun s = show

50cb7e2b30597f481fee57bac945190f06ebcc58jorton $ (text "Verification condition for" <+> pretty ea <> text ":")

7db058a7846888b8823fca9e8135f395265ef1d8nilgun $++$ printExpForVC e

7db058a7846888b8823fca9e8135f395265ef1d8nilgun --s = show $ printExpForVC e <> text ";"

1f1b6bf13313fdd14a45e52e553d3ff28689b717coar -- s = (++ "\n\n;\n\n") $ showRaw $ text "VC for" <+> pretty ea <> text ":" $++$ pretty e

1f1b6bf13313fdd14a45e52e553d3ff28689b717coar-- vcHdl = stdout

1f1b6bf13313fdd14a45e52e553d3ff28689b717coar vcHdl <- liftM (fromMaybe stdout) $ gets vericondOut

1f1b6bf13313fdd14a45e52e553d3ff28689b717coar liftIO $ hPutStrLn vcHdl s where

1f1b6bf13313fdd14a45e52e553d3ff28689b717coar

1f1b6bf13313fdd14a45e52e553d3ff28689b717coar

1f1b6bf13313fdd14a45e52e553d3ff28689b717coarinstance StepDebugger MathematicaIO where

1f1b6bf13313fdd14a45e52e553d3ff28689b717coar setDebugMode b = modify mf where mf mit = mit { debugMode = b }

1f1b6bf13313fdd14a45e52e553d3ff28689b717coar getDebugMode = gets debugMode

1f1b6bf13313fdd14a45e52e553d3ff28689b717coar

1f1b6bf13313fdd14a45e52e553d3ff28689b717coarinstance SymbolicEvaluator MathematicaIO where

1f1b6bf13313fdd14a45e52e553d3ff28689b717coar setSymbolicMode b = modify mf where mf mit = mit { symbolicMode = b }

1f1b6bf13313fdd14a45e52e553d3ff28689b717coar getSymbolicMode = gets symbolicMode

1f1b6bf13313fdd14a45e52e553d3ff28689b717coar

1f1b6bf13313fdd14a45e52e553d3ff28689b717coarinstance MessagePrinter MathematicaIO where

1f1b6bf13313fdd14a45e52e553d3ff28689b717coar printMessage = liftIO . putStrLn

1f1b6bf13313fdd14a45e52e553d3ff28689b717coar

1f1b6bf13313fdd14a45e52e553d3ff28689b717coar-- ----------------------------------------------------------------------

1f1b6bf13313fdd14a45e52e553d3ff28689b717coar-- * Mathematica Transformation Instances

1f1b6bf13313fdd14a45e52e553d3ff28689b717coar-- ----------------------------------------------------------------------

1f1b6bf13313fdd14a45e52e553d3ff28689b717coar

1f1b6bf13313fdd14a45e52e553d3ff28689b717coar-- TODO: Review the vargen facility and the cache-stuff in Transformation

1f1b6bf13313fdd14a45e52e553d3ff28689b717coar

1f1b6bf13313fdd14a45e52e553d3ff28689b717coar-- | Variable generator instance for internal variables on the Hets-side,

1f1b6bf13313fdd14a45e52e553d3ff28689b717coar-- in contrast to the newvar generation in lookupOrInsert of the BMap, which

1f1b6bf13313fdd14a45e52e553d3ff28689b717coar-- generates variables for the Mathematica-side. We use nevertheless the same counter.

1f1b6bf13313fdd14a45e52e553d3ff28689b717coarinstance VarGen MathematicaIO where

1f1b6bf13313fdd14a45e52e553d3ff28689b717coar genVar = do

7db058a7846888b8823fca9e8135f395265ef1d8nilgun s <- get

7db058a7846888b8823fca9e8135f395265ef1d8nilgun let i = newkey $ getBMap s

d3bd91523e4565551991605fb157fea59c3610e2gryzor put $ s { getBMap = (getBMap s) { newkey = i + 1 } }

f086b4b402fa9a2fefc7dda85de2a3cc1cd0a654rjung return $ "?" ++ show i

727872d18412fc021f03969b8641810d8896820bhumbedooh

0d0ba3a410038e179b695446bb149cce6264e0abnd

727872d18412fc021f03969b8641810d8896820bhumbedooh-- ----------------------------------------------------------------------

cc7e1025de9ac63bd4db6fe7f71c158b2cf09fe4humbedooh-- * Mathematica syntax functions

0d0ba3a410038e179b695446bb149cce6264e0abnd-- ----------------------------------------------------------------------

cc7e1025de9ac63bd4db6fe7f71c158b2cf09fe4humbedooh

727872d18412fc021f03969b8641810d8896820bhumbedoohprintExp :: EXPRESSION -> String

0d0ba3a410038e179b695446bb149cce6264e0abndprintExp e = show $ runReader (printExpression e) mathematicaOpInfoNameMap

0d0ba3a410038e179b695446bb149cce6264e0abnd--printExp = exportExp

0d0ba3a410038e179b695446bb149cce6264e0abnd--printExp = show . pretty

ac082aefa89416cbdc9a1836eaf3bed9698201c8humbedooh-- :: ExpressionPrinter m => EXPRESSION -> m Doc

0d0ba3a410038e179b695446bb149cce6264e0abnd

0d0ba3a410038e179b695446bb149cce6264e0abnd

0d0ba3a410038e179b695446bb149cce6264e0abnd

727872d18412fc021f03969b8641810d8896820bhumbedoohmathematicaOpInfoMap :: OpInfoMap

0d0ba3a410038e179b695446bb149cce6264e0abndmathematicaOpInfoMap = operatorInfoMap

0d0ba3a410038e179b695446bb149cce6264e0abnd

30471a4650391f57975f60bbb6e4a90be7b284bfhumbedoohmathematicaOpInfoNameMap :: OpInfoNameMap

205f749042ed530040a4f0080dbcb47ceae8a374rjungmathematicaOpInfoNameMap = operatorInfoNameMap

af33a4994ae2ff15bc67d19ff1a7feb906745bf8rbowen

0d0ba3a410038e179b695446bb149cce6264e0abndprintAssignment :: String -> [String] -> EXPRESSION -> String

7fec19672a491661b2fe4b29f685bc7f4efa64d4ndprintAssignment n [] e = concat [n, ":= ", printExp e, ":", n, ";"]

7fec19672a491661b2fe4b29f685bc7f4efa64d4ndprintAssignment n l e = concat [ n, ":= proc", args, printExp e

7fec19672a491661b2fe4b29f685bc7f4efa64d4nd , " end proc:", n, args, ";"]

7db058a7846888b8823fca9e8135f395265ef1d8nilgun where args = concat [ "(", intercalate ", " l, ") " ]

printAssignmentWithEval :: String -> [String] -> EXPRESSION -> String

printAssignmentWithEval n [] e =

-- concat [n, ":= evalf(", printExp e, "):", n, " &+ 0", ";"]

-- concat [n, ":= evalf(", printExp e, "):", n, ";"]

concat [n, ":= evalf(", printExp e, "):g(", n, ")", ";"]

printAssignmentWithEval n l e = concat [ n, ":= proc", args, printExp e

, " end proc:", n, args, ";"]

where args = concat [ "(", intercalate ", " l, ") " ]

printEvaluation :: EXPRESSION -> String

printEvaluation e = printExp e ++ ";"

printEvaluationWithEval :: EXPRESSION -> String

printEvaluationWithEval e = "evalf(" ++ printExp e ++ ");"

printLookup :: String -> String

printLookup n = n ++ ";"

{-

The evalf makes the decision much faster. As we verify the result formally

this should not be problematic in a formal context!

In the following context "is" gives up if we do not use "evalf":

x2 := cos(10+cos(10)/sin(10)+cos(10+cos(10)/sin(10))/sin(10+cos(10)/sin(10))

+ cos(10+cos(10)/sin(10)+cos(10+cos(10)/sin(10))/sin(10+cos(10)/sin(10)))

/ sin(10+cos(10)/sin(10)+cos(10+cos(10)/sin(10))/sin(10+cos(10)/sin(10))));

is(abs(x2)<1.0e-4);

-}

printBooleanExpr :: EXPRESSION -> String

printBooleanExpr e = concat [ "is(evalf(", printExp e, "));" ]

getBooleanFromExpr :: EXPRESSION -> Either String Bool

getBooleanFromExpr (Op (OpId OP_true) _ _ _) = Right True

getBooleanFromExpr (Op (OpId OP_false) _ _ _) = Right False

getBooleanFromExpr (Op (OpId OP_failure) _ _ _) = Left "Mathematica FAILURE"

getBooleanFromExpr e = Left $ "Cannot translate expression to boolean: "

++ show e

-- The evalf is mandatory if we use the if-statement for encoding

{-

-- | As mathematica does not evaluate boolean expressions we encode them in an

-- if-stmt and transform the numeric response back.

printBooleanExpr :: EXPRESSION -> String

printBooleanExpr e = concat [ "if evalf("

, printExp e, ") then 1 else 0 fi;"

]

getBooleanFromExpr :: EXPRESSION -> Bool

getBooleanFromExpr (Int 1 _) = True

getBooleanFromExpr (Int 0 _) = False

getBooleanFromExpr e =

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

++ show e

-}

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

-- * Generic Communication Interface

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

{- |

The generic interface abstracts over the concrete evaluation function

-}

mathematicaAssign :: (MonadError ASError s, MonadIO s, SymbolicEvaluator s) =>

([String] -> String -> s [EXPRESSION])

-> (ConstantName -> s String)

-> ([String] -> EXPRESSION -> s (EXPRESSION, [String]))

-> ConstantName -> AssDefinition -> s EXPRESSION

mathematicaAssign ef trans transE n def = do

let e = getDefiniens def

args = getArguments def

(e', args') <- transE args e

n' <- trans n

-- liftIO $ putStrLn $ show e'

b <- getSymbolicMode

let f = if b then printAssignment else printAssignmentWithEval

el <- ef args $ f n' args' e'

-- el <- ef args $ printAssignment n' args' e'

case el of

[rhs] -> return rhs

l -> throwError $ ASError InterfaceError $

"mathematicaAssign: unparseable result for assignment of "

++ (show $ pretty n) ++ "\n" ++ (show $ pretty l)

mathematicaAssigns :: (AssignmentStore s) => (String -> s [EXPRESSION])

-> (ConstantName -> s String)

-> ([String] -> EXPRESSION -> s (EXPRESSION, [String]))

-> [(ConstantName, AssDefinition)] -> s ()

mathematicaAssigns ef trans transE l =

let f (n, def) = do

let e = getDefiniens def

args = getArguments def

(e', args') <- transE args e

n' <- trans n

return $ printAssignment n' args' e'

in mapM f l >>= ef . unlines >> return ()

mathematicaLookup :: (AssignmentStore s) => (String -> s [EXPRESSION])

-> (ConstantName -> s String)

-> ConstantName -> s (Maybe EXPRESSION)

mathematicaLookup 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

mathematicaEval :: (MonadError ASError s, SymbolicEvaluator s) =>

(String -> s [EXPRESSION])

-> (EXPRESSION -> s EXPRESSION)

-> EXPRESSION -> s EXPRESSION

mathematicaEval ef trans e = do

e' <- trans e

b <- getSymbolicMode

let f = if b then printEvaluation else printEvaluationWithEval

el <- ef $ f e'

if null el

then throwError $ ASError InterfaceError $

"mathematicaEval: expression " ++ show e' ++ " couldn't be evaluated"

else return $ head el

mathematicaCheck :: (MonadError ASError s, AssignmentStore s) =>

(String -> s [EXPRESSION])

-> (EXPRESSION -> s EXPRESSION)

-> EXPRESSION -> s Bool

mathematicaCheck ef trans e = do

e' <- trans e

el <- ef $ printBooleanExpr e'

if null el

then throwError $ ASError CASError

$ "mathematicaCheck: expression " ++ show e' ++ " could not be evaluated"

else case getBooleanFromExpr $ head el of

Right b -> return b

Left s ->

throwError

$ ASError CASError $

concat [ "mathematicaCheck: CAS error for expression "

, show e', "\n", s ]

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

-- * The Communication Interface

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

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

wrapCommand ios = do

r <- get

let map' x = setMI x r

stmap map' getMI ios

-- | A direct way to communicate with Mathematica

mathematicaDirect :: Bool -> MathState -> String -> IO String

mathematicaDirect b mit s = do

(res, _) <- runIOS (getMI mit) $ PC.call (getChannelTimeout mit) s

return $ if b then removeOutputComments res else res

mathematicaTransE :: EXPRESSION -> MathematicaIO EXPRESSION

mathematicaTransE e = do

r <- get

let bm = getBMap r

(bm', e') = translateExpr bm e

put r { getBMap = bm' }

return e'

mathematicaTransVarE :: [String] -> EXPRESSION -> MathematicaIO (EXPRESSION, [String])

mathematicaTransVarE vl e = do

r <- get

let bm = getBMap r

args = translateArgVars bm vl

(bm', e') = translateExprWithVars vl bm e

put r { getBMap = bm' }

return (e', args)

mathematicaTransS :: ConstantName -> MathematicaIO String

mathematicaTransS s = do

r <- get

let bm = getBMap r

(bm', s') = lookupOrInsert bm s

-- outs = [ "lookingUp " ++ show s ++ " in "

-- , show $ pretty bm, "{", show bm, "}" ]

-- liftIO $ putStrLn $ unlines outs

put r { getBMap = bm' }

return s'

-- | Evaluate the given String as mathematica expression and

-- parse the result to an expression list.

evalMathematicaString :: Bool -- ^ Use parser

-> [String] -- ^ Use this argument list for variable trafo

-> String -> MathematicaIO [EXPRESSION]

evalMathematicaString b args s = do

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

mit <- get

res <- lift $ wrapCommand $ PC.call (getChannelTimeout mit) s

let bm = getBMap mit

trans = if null args then revtranslateExpr bm

else revtranslateExprWithVars args bm

-- when b $ liftIO $ putStrLn $ "evalMathematicaString:"

-- when b $ liftIO $ putStrLn $ show $ maybeToList $ parseExpression mathematicaOpInfoMap $ trimLeft

-- $ removeOutputComments res

-- when b $ liftIO $ putStrLn $ show $ map trans $ maybeToList $ parseExpression mathematicaOpInfoMap $ trimLeft

-- $ removeOutputComments res

return $ if b

then map trans $ maybeToList $ parseExpression mathematicaOpInfoMap

$ trimLeft $ removeOutputComments res

else []

-- | init the mathematica communication

mathematicaInit :: AssignmentDepGraph ()

-> Int -- ^ Verbosity level

-> PC.DTime -- ^ timeout for response

-> IO MathState

mathematicaInit adg v to = do

rc <- lookupMathematicaShellCmd

libpath <- getEnvDef "HETS_MATHEMATICALIB"

$ error "mathematicaInit: Environment variable HETS_MATHEMATICALIB not set."

case rc of

Left mathematicacmd -> do

cs <- PC.start (mathematicacmd ++ " -q") v

$ Just PC.defaultConfig { PC.startTimeout = 3 }

(_, cs') <- runIOS cs $ PC.call 0.5

$ concat [ "interface(prettyprint=0); Digits := 10;"

, "libname := \"", libpath, "\", libname;" ]

return ASState { getBMap = initWithOpMap mathematicaOpInfoMap

, getConnectInfo = (cs', to)

, depGraph = adg

, debugMode = False

, symbolicMode = False

, vericondOut = Nothing

}

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

-- | Loads a mathematica module such as intpakX or intCompare

mathematicaLoadModule :: MathState -> String -> IO String

mathematicaLoadModule rit s =

fmap fst $ runIOS (getMI rit) (PC.call 0.5 $ "with(" ++ s ++ ");")

mathematicaExit :: MathState -> IO (Maybe ExitCode)

mathematicaExit mit = do

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

return ec

execWithMathematica :: MathState -> MathematicaIO a -> IO (MathState, a)

execWithMathematica mit m = do

let err s = error $ "execWithMathematica: " ++ s

(res, mit') <- runIOS mit $ runErrorT m

case res of

Left s' -> err $ asErrorMsg s'

Right x -> return (mit', x)

runWithMathematica :: AssignmentDepGraph () -> Int -- ^ Verbosity level

-> PC.DTime -- ^ timeout for response

-> [String] -> MathematicaIO a

-> IO (MathState, a)

runWithMathematica adg i to l m = do

mit <- mathematicaInit adg i to

mapM_ (mathematicaLoadModule mit) l

-- wraps an interval around the number

let debugFun = "g := proc(v) z:=abs(Float(v,1-Digits)):[v-z, v+z] end;"

runIOS (getMI mit) $ PC.call 0.3 debugFun

execWithMathematica mit m

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

-- * The Mathematica system

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

-- | Left String is success, Right String is failure

lookupMathematicaShellCmd :: IO (Either String String)

lookupMathematicaShellCmd = do

cmd <- getEnvDef "HETS_MATHEMATICA" "mathematica"

-- check that prog exists

noProg <- missingExecutableInPath cmd

let f = if noProg then Right else Left

return $ f cmd

-- | Removes lines starting with ">"

removeOutputComments :: String -> String

removeOutputComments =

filter (/= '\\') . concat . filter (not . isPrefixOf ">") . lines