MapleInterpreter.hs revision 5dad1d101f19a24ec783767c720a9b36640a1222
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder{-# LANGUAGE FlexibleContexts, TypeSynonymInstances #-}
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder{- |
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederModule : $Header$
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederDescription : Maple instance for the AssignmentStore class
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederCopyright : (c) Ewaryst Schulz, DFKI Bremen 2010
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederMaintainer : Ewaryst.Schulz@dfki.de
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederStability : experimental
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederPortability : non-portable (via imports)
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederMaple as AssignmentStore
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder-}
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder
f799084b320209cdd71a29e74fff1be054c1d342Christian Maedermodule CSL.MapleInterpreter where
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder
3ab1e7a18f3fc3eb004464bc54b7df4483f1f060Christian Maederimport Common.ProverTools (missingExecutableInPath)
f799084b320209cdd71a29e74fff1be054c1d342Christian Maederimport Common.Utils (getEnvDef, trimLeft)
f799084b320209cdd71a29e74fff1be054c1d342Christian Maederimport Common.Doc
f799084b320209cdd71a29e74fff1be054c1d342Christian Maederimport Common.DocUtils
f799084b320209cdd71a29e74fff1be054c1d342Christian Maederimport Common.IOS
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder
f799084b320209cdd71a29e74fff1be054c1d342Christian Maederimport CSL.AS_BASIC_CSL
f799084b320209cdd71a29e74fff1be054c1d342Christian Maederimport CSL.Parse_AS_Basic (parseExpression)
f799084b320209cdd71a29e74fff1be054c1d342Christian Maederimport CSL.Interpreter
f799084b320209cdd71a29e74fff1be054c1d342Christian Maederimport CSL.Transformation
f799084b320209cdd71a29e74fff1be054c1d342Christian Maederimport CSL.Verification
f799084b320209cdd71a29e74fff1be054c1d342Christian Maederimport CSL.Reduce_Interface (exportExp)
f799084b320209cdd71a29e74fff1be054c1d342Christian Maederimport CSL.Analysis
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder-- the process communication interface
0015e1756b734b34d4b550318c078f9a0c585611Christian Maederimport qualified Interfaces.Process as PC
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder
0015e1756b734b34d4b550318c078f9a0c585611Christian Maederimport Control.Monad
0015e1756b734b34d4b550318c078f9a0c585611Christian Maederimport Control.Monad.Trans (MonadTrans (..), MonadIO (..))
f799084b320209cdd71a29e74fff1be054c1d342Christian Maederimport Control.Monad.Error (ErrorT(..), MonadError (..))
0015e1756b734b34d4b550318c078f9a0c585611Christian Maederimport Control.Monad.State.Class
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder
0015e1756b734b34d4b550318c078f9a0c585611Christian Maederimport Data.List hiding (lookup)
0015e1756b734b34d4b550318c078f9a0c585611Christian Maederimport qualified Data.Set as Set
0015e1756b734b34d4b550318c078f9a0c585611Christian Maederimport Data.Maybe
0015e1756b734b34d4b550318c078f9a0c585611Christian Maederimport System.Exit (ExitCode)
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder
0015e1756b734b34d4b550318c078f9a0c585611Christian Maederimport Prelude hiding (lookup)
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder-- ----------------------------------------------------------------------
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder-- * Maple Calculator Instances
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder-- ----------------------------------------------------------------------
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder-- | MapleInterpreter with Translator based on the CommandState
0015e1756b734b34d4b550318c078f9a0c585611Christian Maederdata MITrans = MITrans { getBMap :: BMap
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder , getMI :: PC.CommandState
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder , depGraph :: AssignmentDepGraph ()
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder , channelTimeout :: PC.DTime }
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder-- Maple interface, built on CommandState
0015e1756b734b34d4b550318c078f9a0c585611Christian Maedertype MapleIO = ErrorT ASError (IOS MITrans)
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder
0015e1756b734b34d4b550318c078f9a0c585611Christian Maederinstance AssignmentStore MapleIO where
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder assign = mapleAssign (evalMapleString True) mapleTransS mapleTransVarE
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder assigns =
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder mapleAssigns (evalMapleString False []) mapleTransS mapleTransVarE
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder lookup = mapleLookup (evalMapleString True []) mapleTransS
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder eval = mapleEval (evalMapleString True []) mapleTransE
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder check = mapleCheck (evalMapleString True []) mapleTransE
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder names = get >>= return . SMem . getBMap
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder evalRaw s = get >>= liftIO . flip (mapleDirect True) s
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder getUndefinedConstants e = do
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder adg <- gets depGraph
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder let g = isNothing . depGraphLookup adg
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder return $ Set.filter g $ Set.map SimpleConstant $ setOfUserDefined e
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder genNewKey = do
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder mit <- get
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder let (bm, i) = genKey $ getBMap mit
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder put mit { getBMap = bm }
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder return i
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maederinstance VCGenerator MapleIO where
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder getDepGraph = gets depGraph
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder updateConstant n def =
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder let f gr = updateGraph gr n
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder $ DepGraphAnno { annoDef = def
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder , annoVal = () }
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder mf mit = mit { depGraph = f $ depGraph mit }
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder in modify mf
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder addVC ea e =
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder liftIO $ putStrLn $ show $
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder text "VC for" <+> pretty ea <> text ":" $++$ pretty e
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder-- ----------------------------------------------------------------------
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder-- * Maple Transformation Instances
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder-- ----------------------------------------------------------------------
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder-- TODO: Review the vargen facility and the cache-stuff in Transformation
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder-- | Variable generator instance for internal variables on the Hets-side,
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian Maeder-- in contrast to the newvar generation in lookupOrInsert of the BMap, which
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder-- generates variables for the Maple-side. We use nevertheless the same counter.
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maederinstance VarGen MapleIO where
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder genVar = do
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder s <- get
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder let i = newkey $ getBMap s
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder put $ s { getBMap = (getBMap s) { newkey = i + 1 } }
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder return $ "?" ++ show i
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder-- ----------------------------------------------------------------------
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder-- * Maple syntax functions
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder-- ----------------------------------------------------------------------
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintExp :: EXPRESSION -> String
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintExp = exportExp
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder--printExp = show . pretty
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder-- TODO: The mapping should be OPNAME to OPNAME or we should remove the mapping
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder-- just adapt the opinfo-map for pretty printing for each CAS!
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian MaedercslMapleDefaultMapping :: [(OPNAME, String)]
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian MaedercslMapleDefaultMapping =
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder let idmapping = map (\ x -> (x, show x))
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder-- ampmapping = map (\ x -> (x, "&" ++ show x))
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder possibleIntervalOps = [ OP_mult, OP_div, OP_plus, OP_minus, OP_neg
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian Maeder , OP_cos, OP_sin, OP_tan, OP_sqrt, OP_abs
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian Maeder , OP_neq, OP_lt, OP_leq, OP_eq, OP_gt, OP_geq ]
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder logicOps = [ OP_and, OP_or, OP_impl, OP_true, OP_false ]
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian Maeder otherOps = [ OP_factor, OP_maxloc, OP_sign, OP_Pi, OP_min, OP_max
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder , OP_fthrt, OP_reldist, OP_reldistLe]
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian Maeder specialOps = [(OP_pow, "^"), (OP_failure, "FAIL")]
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder-- specialOp = (OP_pow, "&**")
abcb1baa565c878598d732d0aa7724f474c9265cChristian Maeder in specialOps ++ idmapping logicOps ++ idmapping possibleIntervalOps
abcb1baa565c878598d732d0aa7724f474c9265cChristian Maeder ++ idmapping otherOps
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintAssignment :: String -> [String] -> EXPRESSION -> String
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintAssignment n [] e = concat [n, ":= ", printExp e, ":", n, ";"]
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian MaederprintAssignment n l e = concat [ n, ":= proc", args, printExp e
c26ff5708c4a855bf9503b3001bcc19e5fd6286fChristian Maeder , " end proc:", n, args, ";"]
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder where args = concat [ "(", intercalate ", " l, ") " ]
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintEvaluation :: EXPRESSION -> String
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintEvaluation e = printExp e ++ ";"
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintLookup :: String -> String
c26ff5708c4a855bf9503b3001bcc19e5fd6286fChristian MaederprintLookup n = n ++ ";"
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder{-
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederThe evalf makes the decision much faster. As we verify the result formally
f799084b320209cdd71a29e74fff1be054c1d342Christian Maederthis should not be problematic in a formal context!
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder
c26ff5708c4a855bf9503b3001bcc19e5fd6286fChristian MaederIn the following context "is" gives up if we do not use "evalf":
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder
f799084b320209cdd71a29e74fff1be054c1d342Christian Maederx2 := cos(10+cos(10)/sin(10)+cos(10+cos(10)/sin(10))/sin(10+cos(10)/sin(10))
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder + cos(10+cos(10)/sin(10)+cos(10+cos(10)/sin(10))/sin(10+cos(10)/sin(10)))
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder / sin(10+cos(10)/sin(10)+cos(10+cos(10)/sin(10))/sin(10+cos(10)/sin(10))));
f799084b320209cdd71a29e74fff1be054c1d342Christian Maederis(abs(x2)<1.0e-4);
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder-}
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintBooleanExpr :: EXPRESSION -> String
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintBooleanExpr e = concat [ "is(evalf(", printExp e, "));" ]
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder
f799084b320209cdd71a29e74fff1be054c1d342Christian MaedergetBooleanFromExpr :: EXPRESSION -> Either String Bool
f799084b320209cdd71a29e74fff1be054c1d342Christian MaedergetBooleanFromExpr (Op (OpId OP_true) _ _ _) = Right True
f799084b320209cdd71a29e74fff1be054c1d342Christian MaedergetBooleanFromExpr (Op (OpId OP_false) _ _ _) = Right False
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian MaedergetBooleanFromExpr (Op (OpId OP_failure) _ _ _) = Left "Maple FAILURE"
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian MaedergetBooleanFromExpr e = Left $ "Cannot translate expression to boolean: "
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder ++ show e
c26ff5708c4a855bf9503b3001bcc19e5fd6286fChristian Maeder
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian Maeder
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder-- The evalf is mandatory if we use the if-statement for encoding
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder{-
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder-- | As maple does not evaluate boolean expressions we encode them in an
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder-- if-stmt and transform the numeric response back.
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian MaederprintBooleanExpr :: EXPRESSION -> String
abcb1baa565c878598d732d0aa7724f474c9265cChristian MaederprintBooleanExpr e = concat [ "if evalf("
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder , printExp e, ") then 1 else 0 fi;"
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder ]
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder
f799084b320209cdd71a29e74fff1be054c1d342Christian MaedergetBooleanFromExpr :: EXPRESSION -> Bool
f799084b320209cdd71a29e74fff1be054c1d342Christian MaedergetBooleanFromExpr (Int 1 _) = True
f799084b320209cdd71a29e74fff1be054c1d342Christian MaedergetBooleanFromExpr (Int 0 _) = False
f799084b320209cdd71a29e74fff1be054c1d342Christian MaedergetBooleanFromExpr e =
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder error $ "getBooleanFromExpr: can't translate expression to boolean: "
ce944c156ca6b4a56e81e232d7a22e582fbdcf33Christian Maeder ++ show e
ce944c156ca6b4a56e81e232d7a22e582fbdcf33Christian Maeder-}
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder-- ----------------------------------------------------------------------
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder-- * Generic Communication Interface
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder-- ----------------------------------------------------------------------
3ab1e7a18f3fc3eb004464bc54b7df4483f1f060Christian Maeder
3ab1e7a18f3fc3eb004464bc54b7df4483f1f060Christian Maeder{- |
3ab1e7a18f3fc3eb004464bc54b7df4483f1f060Christian Maeder The generic interface abstracts over the concrete evaluation function
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder-}
3ab1e7a18f3fc3eb004464bc54b7df4483f1f060Christian Maeder
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian MaedermapleAssign :: (MonadError ASError s, AssignmentStore s, MonadIO s) =>
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian Maeder ([String] -> String -> s [EXPRESSION])
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian Maeder -> (ConstantName -> s String)
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian Maeder -> ([String] -> EXPRESSION -> s (EXPRESSION, [String]))
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian Maeder -> ConstantName -> AssDefinition -> s EXPRESSION
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian MaedermapleAssign ef trans transE n def = do
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian Maeder let e = getDefiniens def
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian Maeder args = getArguments def
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian Maeder (e', args') <- transE args e
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian Maeder n' <- trans n
abcb1baa565c878598d732d0aa7724f474c9265cChristian Maeder liftIO $ putStrLn $ show e'
2344f16936f5b31c9530d0cafb3838e9df3f3644Christian Maeder el <- ef args $ printAssignment n' args' e'
2344f16936f5b31c9530d0cafb3838e9df3f3644Christian Maeder case el of
2344f16936f5b31c9530d0cafb3838e9df3f3644Christian Maeder [rhs] -> return rhs
2344f16936f5b31c9530d0cafb3838e9df3f3644Christian Maeder l -> throwError $ ASError InterfaceError $
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder "mapleAssign: unparseable result for assignment of "
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder ++ (show $ pretty n) ++ "\n" ++ (show $ pretty l)
2344f16936f5b31c9530d0cafb3838e9df3f3644Christian Maeder
f799084b320209cdd71a29e74fff1be054c1d342Christian MaedermapleAssigns :: (AssignmentStore s) => (String -> s [EXPRESSION])
abcb1baa565c878598d732d0aa7724f474c9265cChristian Maeder -> (ConstantName -> s String)
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder -> ([String] -> EXPRESSION -> s (EXPRESSION, [String]))
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder -> [(ConstantName, AssDefinition)] -> s ()
f799084b320209cdd71a29e74fff1be054c1d342Christian MaedermapleAssigns ef trans transE l =
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder let f (n, def) = do
abcb1baa565c878598d732d0aa7724f474c9265cChristian Maeder let e = getDefiniens def
abcb1baa565c878598d732d0aa7724f474c9265cChristian Maeder args = getArguments def
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian Maeder (e', args') <- transE args e
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian Maeder n' <- trans n
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian Maeder return $ printAssignment n' args' e'
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian Maeder in mapM f l >>= ef . unlines >> return ()
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian Maeder
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian MaedermapleLookup :: (AssignmentStore s) => (String -> s [EXPRESSION])
abcb1baa565c878598d732d0aa7724f474c9265cChristian Maeder -> (ConstantName -> s String)
abcb1baa565c878598d732d0aa7724f474c9265cChristian Maeder -> ConstantName -> s (Maybe EXPRESSION)
abcb1baa565c878598d732d0aa7724f474c9265cChristian MaedermapleLookup ef trans n = do
abcb1baa565c878598d732d0aa7724f474c9265cChristian Maeder n' <- trans n
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder el <- ef $ printLookup n'
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder return $ listToMaybe el
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder-- we don't want to return nothing on id-lookup: "x; --> x"
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder-- if e == mkOp n [] then return Nothing else return $ Just e
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder
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 $ Left 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
return $ if b
then map trans $ maybeToList $ parseExpression $ 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 = initWithDefault cslMapleDefaultMapping
, getMI = cs'
, depGraph = adg
, 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]);
-}