4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder{-# LANGUAGE FlexibleContexts, TypeSynonymInstances #-}

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder{- |

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian MaederModule : $Header$

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederDescription : Maple instance for the AssignmentStore class

23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian MaederCopyright : (c) Ewaryst Schulz, DFKI Bremen 2010

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaederLicense : GPLv2 or higher, see LICENSE.txt

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederMaintainer : Ewaryst.Schulz@dfki.de

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederStability : experimental

f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederPortability : non-portable (via imports)

23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian Maeder

23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian MaederMaple as AssignmentStore

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder-}

23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian Maeder

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maedermodule CSL.MapleInterpreter where

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederimport Common.ProverTools (missingExecutableInPath)

fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maederimport Common.Utils (getEnvDef, trimLeft)

23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maederimport Common.Doc

fcb1d8a27670f3206bd4ca28d77d4172619db602Christian Maederimport Common.DocUtils

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maederimport Common.IOS

dc6b48bb46df8e56da3491c98476e6da0d1d5d1dChristian Maeder

fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maederimport CSL.AS_BASIC_CSL

f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maederimport CSL.Parse_AS_Basic (parseExpression)

f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maederimport CSL.Interpreter

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maederimport CSL.Transformation

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederimport CSL.Verification

f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maederimport CSL.Analysis

af621d0066770895fd79562728e93099c8c52060Christian Maeder

7c554e9d4a39b8eb3b0881f20807c95dd8e793aeChristian Maeder-- the process communication interface

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport qualified Interfaces.Process as PC

79d11c2e3ad242ebb241f5d4a5e98a674c0b986fChristian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport Control.Monad

f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maeder--import Control.Monad.Trans (MonadTrans (..), MonadIO (..))

024621f43239cfe9629e35d35a8669fad7acbba2Christian Maederimport Control.Monad.Error (ErrorT(..), MonadError (..))

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederimport Control.Monad.State.Class

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederimport Control.Monad.Reader

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederimport Data.List hiding (lookup)

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederimport qualified Data.Set as Set

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederimport Data.Maybe

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederimport System.Exit (ExitCode)

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederimport System.IO

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederimport Prelude hiding (lookup)

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder-- ----------------------------------------------------------------------

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder-- * Maple Calculator Instances

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder-- ----------------------------------------------------------------------

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder-- | MapleInterpreter with Translator based on the CommandState

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederdata MITrans = MITrans { getBMap :: BMap

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder , getMI :: PC.CommandState

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder , depGraph :: AssignmentDepGraph ()

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder , debugMode :: Bool

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder , symbolicMode :: Bool

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder , vericondOut :: Maybe Handle

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder , channelTimeout :: PC.DTime }

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder-- Maple interface, built on CommandState

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maedertype MapleIO = ErrorT ASError (IOS MITrans)

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederinstance AssignmentStore MapleIO where

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder assign = mapleAssign (evalMapleString True) mapleTransS mapleTransVarE

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder assigns =

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder mapleAssigns (evalMapleString False []) mapleTransS mapleTransVarE

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder lookup = mapleLookup (evalMapleString True []) mapleTransS

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder eval = mapleEval (evalMapleString True []) mapleTransE

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder check = mapleCheck (evalMapleString True []) mapleTransE

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder names = get >>= return . SMem . getBMap

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder evalRaw s = get >>= liftIO . flip (mapleDirect True) s

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder getUndefinedConstants e = do

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder adg <- gets depGraph

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder let g = isNothing . depGraphLookup adg

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder return $ Set.filter g $ Set.map SimpleConstant $ setOfUserDefined e

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder genNewKey = do

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder mit <- get

986e0e9cf8c2358f455460b3fc75ce7c5dcf0973Christian Maeder let (bm, i) = genKey $ getBMap mit

6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder put mit { getBMap = bm }

6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder return i

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maederinstance VCGenerator MapleIO where

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder getDepGraph = gets depGraph

6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder updateConstant n def =

6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder let f gr = updateGraph gr n

6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder $ DepGraphAnno { annoDef = def

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder , annoVal = () }

6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder mf mit = mit { depGraph = f $ depGraph mit }

6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder in modify mf

6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder

6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder addVC ea e = do

6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder let

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder -- s = show $ text "VC for" <+> pretty ea <> text ":" $++$ pretty e

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder s = show $ pretty e <> text ";"

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

89054b2b95a3f92e78324dc852f3d34704e2ca49Christian Maeder-- vcHdl = stdout

89054b2b95a3f92e78324dc852f3d34704e2ca49Christian Maeder vcHdl <- liftM (fromMaybe stdout) $ gets vericondOut

89054b2b95a3f92e78324dc852f3d34704e2ca49Christian Maeder liftIO $ hPutStrLn vcHdl s where

b9eb4099ac3fd619c73f48cd022fc0f3c9b732f0Christian Maeder

b9eb4099ac3fd619c73f48cd022fc0f3c9b732f0Christian Maeder

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maederinstance StepDebugger MapleIO where

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder setDebugMode b = modify mf where mf mit = mit { debugMode = b }

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder getDebugMode = gets debugMode

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder

af621d0066770895fd79562728e93099c8c52060Christian Maeder-- ----------------------------------------------------------------------

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder-- * Maple Transformation Instances

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder-- ----------------------------------------------------------------------

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder

af621d0066770895fd79562728e93099c8c52060Christian Maeder-- TODO: Review the vargen facility and the cache-stuff in Transformation

af621d0066770895fd79562728e93099c8c52060Christian Maeder

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder-- | Variable generator instance for internal variables on the Hets-side,

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder-- in contrast to the newvar generation in lookupOrInsert of the BMap, which

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder-- generates variables for the Maple-side. We use nevertheless the same counter.

89054b2b95a3f92e78324dc852f3d34704e2ca49Christian Maederinstance VarGen MapleIO where

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder genVar = do

f353be6210f67ffd4a46967bba749afc968cee52Christian Maeder s <- get

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder let i = newkey $ getBMap s

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder put $ s { getBMap = (getBMap s) { newkey = i + 1 } }

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder return $ "?" ++ show i

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder

89054b2b95a3f92e78324dc852f3d34704e2ca49Christian Maeder-- ----------------------------------------------------------------------

8485da94b57d8b5135ee685b55c982b037ed4140Christian Maeder-- * Maple syntax functions

8485da94b57d8b5135ee685b55c982b037ed4140Christian Maeder-- ----------------------------------------------------------------------

8485da94b57d8b5135ee685b55c982b037ed4140Christian Maeder

e76e6a43f51438215737d6fc176c89da05bb86daChristian MaederprintExp :: EXPRESSION -> String

8485da94b57d8b5135ee685b55c982b037ed4140Christian MaederprintExp e = show $ runReader (printExpression e) mapleOpInfoNameMap

8485da94b57d8b5135ee685b55c982b037ed4140Christian Maeder--printExp = exportExp

8485da94b57d8b5135ee685b55c982b037ed4140Christian Maeder--printExp = show . pretty

8485da94b57d8b5135ee685b55c982b037ed4140Christian Maeder-- :: ExpressionPrinter m => EXPRESSION -> m Doc

8485da94b57d8b5135ee685b55c982b037ed4140Christian Maeder

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder

0a85c4dc6f4bba88e1994e8f1cd3657b6503b220Christian MaedermapleOpInfoMap :: OpInfoMap

e76e6a43f51438215737d6fc176c89da05bb86daChristian MaedermapleOpInfoMap = operatorInfoMap

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedermapleOpInfoNameMap :: OpInfoNameMap

a94b530fa82bb281caac766a9c0f7b2fcfe7a584Christian MaedermapleOpInfoNameMap = operatorInfoNameMap

997c56f3bc74a703043010978e5013fdb074d659Christian Maeder

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder-- TODO: The mapping should be OPNAME to OPNAME or we should remove the mapping

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder-- just adapt the opinfo-map for pretty printing for each CAS!

dc6b48bb46df8e56da3491c98476e6da0d1d5d1dChristian MaedercslMapleDefaultMapping :: [(OPNAME, String)]

8485da94b57d8b5135ee685b55c982b037ed4140Christian MaedercslMapleDefaultMapping =

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

fcb1d8a27670f3206bd4ca28d77d4172619db602Christian Maeder-- ampmapping = map (\ x -> (x, "&" ++ show x))

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder possibleIntervalOps = [ OP_mult, OP_div, OP_plus, OP_minus, OP_neg

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder , OP_cos, OP_sin, OP_tan, OP_sqrt, OP_abs

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder , OP_neq, OP_lt, OP_leq, OP_eq, OP_gt, OP_geq ]

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder logicOps = [ OP_and, OP_or, OP_impl, OP_true, OP_false ]

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder otherOps = [ OP_factor, OP_maxloc, OP_sign, OP_Pi, OP_min, OP_max

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder , OP_fthrt, OP_reldist, OP_reldistLe]

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder specialOps = [(OP_pow, "^"), (OP_failure, "FAIL")]

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder-- specialOp = (OP_pow, "&**")

8485da94b57d8b5135ee685b55c982b037ed4140Christian Maeder in specialOps ++ idmapping logicOps ++ idmapping possibleIntervalOps

dc6b48bb46df8e56da3491c98476e6da0d1d5d1dChristian Maeder ++ idmapping otherOps

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederprintAssignment :: String -> [String] -> EXPRESSION -> String

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian MaederprintAssignment n [] e = concat [n, ":= ", printExp e, ":", n, ";"]

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

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

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

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian MaederprintAssignmentWithEval :: String -> [String] -> EXPRESSION -> String

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian MaederprintAssignmentWithEval n [] e =

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

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

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

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

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian MaederprintEvaluation :: EXPRESSION -> String

836e72a3c413366ba9801726f3b249c7791cb9caChristian MaederprintEvaluation e = printExp e ++ ";"

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder

9c5b1136299d9052e4e995614a3a36a051a2682fChristian MaederprintLookup :: String -> String

c1031ac42b3f3d7d0fe7d9d6b54423a092d473a0Christian MaederprintLookup n = n ++ ";"

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder{-

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

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maederthis should not be problematic in a formal context!

23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maeder

23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maeder

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

3cafc73a998493f9ed3d5e934c0ab80bcfb465c2Christian Maeder

b5699d97a9e2b4496f98d624f4b0a537986651c3Christian Maederx2 := cos(10+cos(10)/sin(10)+cos(10+cos(10)/sin(10))/sin(10+cos(10)/sin(10))

b5699d97a9e2b4496f98d624f4b0a537986651c3Christian Maeder + cos(10+cos(10)/sin(10)+cos(10+cos(10)/sin(10))/sin(10+cos(10)/sin(10)))

3cafc73a998493f9ed3d5e934c0ab80bcfb465c2Christian Maeder / sin(10+cos(10)/sin(10)+cos(10+cos(10)/sin(10))/sin(10+cos(10)/sin(10))));

7bf6d421b0ea31ae63f1fe04919942b931abda47Christian Maederis(abs(x2)<1.0e-4);

7bf6d421b0ea31ae63f1fe04919942b931abda47Christian Maeder-}

7bf6d421b0ea31ae63f1fe04919942b931abda47Christian MaederprintBooleanExpr :: EXPRESSION -> String

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

7c554e9d4a39b8eb3b0881f20807c95dd8e793aeChristian Maeder

7bf6d421b0ea31ae63f1fe04919942b931abda47Christian MaedergetBooleanFromExpr :: EXPRESSION -> Either String Bool

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian MaedergetBooleanFromExpr (Op (OpId OP_true) _ _ _) = Right True

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian MaedergetBooleanFromExpr (Op (OpId OP_false) _ _ _) = Right False

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian MaedergetBooleanFromExpr (Op (OpId OP_failure) _ _ _) = Left "Maple FAILURE"

7c554e9d4a39b8eb3b0881f20807c95dd8e793aeChristian MaedergetBooleanFromExpr e = Left $ "Cannot translate expression to boolean: "

7bf6d421b0ea31ae63f1fe04919942b931abda47Christian Maeder ++ show e

7bf6d421b0ea31ae63f1fe04919942b931abda47Christian Maeder

7bf6d421b0ea31ae63f1fe04919942b931abda47Christian Maeder

7bf6d421b0ea31ae63f1fe04919942b931abda47Christian Maeder

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

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder{-

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder

3cafc73a998493f9ed3d5e934c0ab80bcfb465c2Christian Maeder-- | As maple does not evaluate boolean expressions we encode them in an

836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder-- if-stmt and transform the numeric response back.

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian MaederprintBooleanExpr :: EXPRESSION -> String

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian MaederprintBooleanExpr e = concat [ "if evalf("

9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder , printExp e, ") then 1 else 0 fi;"

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder ]

bb3bdd4a260606a6184b5f5a5774ca6632ca597aChristian Maeder

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian MaedergetBooleanFromExpr :: EXPRESSION -> Bool

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian MaedergetBooleanFromExpr (Int 1 _) = True

e76e6a43f51438215737d6fc176c89da05bb86daChristian MaedergetBooleanFromExpr (Int 0 _) = False

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian MaedergetBooleanFromExpr e =

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

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder ++ show e

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder-}

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

-- * Generic Communication Interface

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

{- |

The generic interface abstracts over the concrete evaluation function

-}

mapleAssign :: (MonadError ASError s, AssignmentStore s, MonadIO s) =>

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

-> (ConstantName -> s String)

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

-> ConstantName -> AssDefinition -> s EXPRESSION

mapleAssign 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'

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

case el of

[rhs] -> return rhs

l -> throwError $ ASError InterfaceError $

"mapleAssign: unparseable result for assignment of "

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

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

-> (ConstantName -> s String)

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

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

mapleAssigns 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 ()

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

-> (ConstantName -> s String)

-> ConstantName -> s (Maybe EXPRESSION)

mapleLookup 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

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

(String -> s [EXPRESSION])

-> (EXPRESSION -> s EXPRESSION)

-> EXPRESSION -> s EXPRESSION

mapleEval ef trans e = do

e' <- trans e

el <- ef $ printEvaluation e'

if null el

then throwError $ ASError InterfaceError $

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

else return $ head el

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

(String -> s [EXPRESSION])

-> (EXPRESSION -> s EXPRESSION)

-> EXPRESSION -> s Bool

mapleCheck ef trans e = do

e' <- trans e

el <- ef $ printBooleanExpr e'

if null el

then throwError $ ASError CASError

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

else case getBooleanFromExpr $ head el of

Right b -> return b

Left s ->

throwError

$ ASError CASError $

concat [ "mapleCheck: CAS error for expression "

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

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

-- * The Communication Interface

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

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

wrapCommand ios = do

r <- get

let map' x = r { getMI = x }

stmap map' getMI ios

-- | A direct way to communicate with Maple

mapleDirect :: Bool -> MITrans -> String -> IO String

mapleDirect b mit s = do

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

return $ if b then removeOutputComments res else res

mapleTransE :: EXPRESSION -> MapleIO EXPRESSION

mapleTransE e = do

r <- get

let bm = getBMap r

(bm', e') = translateExpr bm e

put r { getBMap = bm' }

return e'

mapleTransVarE :: [String] -> EXPRESSION -> MapleIO (EXPRESSION, [String])

mapleTransVarE 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)

mapleTransS :: ConstantName -> MapleIO String

mapleTransS 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 maple expression and

-- parse the result to an expression list.

evalMapleString :: Bool -- ^ Use parser

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

-> String -> MapleIO [EXPRESSION]

evalMapleString b args s = do

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

mit <- get

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

let bm = getBMap mit

trans = if null args then revtranslateExpr bm

else revtranslateExprWithVars args bm

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

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

-- $ removeOutputComments res

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

-- $ removeOutputComments res

return $ if b

then map trans $ maybeToList $ parseExpression mapleOpInfoMap

$ trimLeft $ removeOutputComments res

else []

-- | init the maple communication

mapleInit :: AssignmentDepGraph ()

-> Int -- ^ Verbosity level

-> PC.DTime -- ^ timeout for response

-> IO MITrans

mapleInit adg v to = do

rc <- lookupMapleShellCmd

libpath <- getEnvDef "HETS_MAPLELIB"

$ error "mapleInit: Environment variable HETS_MAPLELIB not set."

case rc of

Left maplecmd -> do

cs <- PC.start (maplecmd ++ " -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 MITrans { getBMap = initWithOpMap mapleOpInfoMap

, getMI = cs'

, depGraph = adg

, debugMode = False

, symbolicMode = True

, vericondOut = Nothing

, channelTimeout = to

}

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

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

mapleLoadModule :: MITrans -> String -> IO String

mapleLoadModule rit s =

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

mapleExit :: MITrans -> IO (Maybe ExitCode)

mapleExit mit = do

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

return ec

execWithMaple :: MITrans -> MapleIO a -> IO (MITrans, a)

execWithMaple mit m = do

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

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

case res of

Left s' -> err $ asErrorMsg s'

Right x -> return (mit', x)

runWithMaple :: AssignmentDepGraph () -> Int

-> PC.DTime -- ^ timeout for response

-> [String] -> MapleIO a

-> IO (MITrans, a)

runWithMaple adg i to l m = do

mit <- mapleInit adg i to

mapM_ (mapleLoadModule mit) l

execWithMaple mit m

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

-- * The Maple system

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

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

lookupMapleShellCmd :: IO (Either String String)

lookupMapleShellCmd = do

cmd <- getEnvDef "HETS_MAPLE" "maple"

-- 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

{- Some problems with the maximization in Maple:

> Maximize(-x^6+t*x^3-3, {t >= -1000, t <= 1000}, x=-2..0);

Error, (in Optimization:-NLPSolve) no improved point could be found

> Maximize(-x^t*x^3-3, {t >= -1000, t <= 1000}, x=-2..0);

Error, (in Optimization:-NLPSolve) complex value encountered

-- works better:

rhs(maximize(-(tan(x)-1/12)^2 -1, x=-1..1, location)[2,1,1,1]);

-}