MapleInterpreter.hs revision 5dad1d101f19a24ec783767c720a9b36640a1222
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder{-# LANGUAGE FlexibleContexts, TypeSynonymInstances #-}
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 MaederMaintainer : Ewaryst.Schulz@dfki.de
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederStability : experimental
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederPortability : non-portable (via imports)
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederMaple as AssignmentStore
3ab1e7a18f3fc3eb004464bc54b7df4483f1f060Christian Maederimport Common.ProverTools (missingExecutableInPath)
f799084b320209cdd71a29e74fff1be054c1d342Christian Maederimport Common.Utils (getEnvDef, trimLeft)
f799084b320209cdd71a29e74fff1be054c1d342Christian Maederimport CSL.Parse_AS_Basic (parseExpression)
f799084b320209cdd71a29e74fff1be054c1d342Christian Maederimport CSL.Reduce_Interface (exportExp)
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder-- the process communication interface
0015e1756b734b34d4b550318c078f9a0c585611Christian Maederimport qualified Interfaces.Process as PC
0015e1756b734b34d4b550318c078f9a0c585611Christian Maederimport Control.Monad.Trans (MonadTrans (..), MonadIO (..))
f799084b320209cdd71a29e74fff1be054c1d342Christian Maederimport Control.Monad.Error (ErrorT(..), MonadError (..))
0015e1756b734b34d4b550318c078f9a0c585611Christian Maederimport Data.List hiding (lookup)
0015e1756b734b34d4b550318c078f9a0c585611Christian Maederimport qualified Data.Set as Set
0015e1756b734b34d4b550318c078f9a0c585611Christian Maederimport System.Exit (ExitCode)
0015e1756b734b34d4b550318c078f9a0c585611Christian Maederimport Prelude hiding (lookup)
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder-- ----------------------------------------------------------------------
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder-- * Maple Calculator Instances
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder-- ----------------------------------------------------------------------
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder-- | MapleInterpreter with Translator based on the CommandState
0015e1756b734b34d4b550318c078f9a0c585611Christian Maederdata MITrans = MITrans { getBMap :: BMap
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder , depGraph :: AssignmentDepGraph ()
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder , channelTimeout :: PC.DTime }
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder-- Maple interface, built on CommandState
0015e1756b734b34d4b550318c078f9a0c585611Christian Maedertype MapleIO = ErrorT ASError (IOS MITrans)
0015e1756b734b34d4b550318c078f9a0c585611Christian Maederinstance AssignmentStore MapleIO where
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder assign = mapleAssign (evalMapleString True) mapleTransS mapleTransVarE
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 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 genNewKey = do
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder let (bm, i) = genKey $ getBMap mit
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder put mit { getBMap = bm }
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 liftIO $ putStrLn $ show $
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder text "VC for" <+> pretty ea <> text ":" $++$ pretty e
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder-- ----------------------------------------------------------------------
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder-- * Maple Transformation Instances
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder-- ----------------------------------------------------------------------
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder-- TODO: Review the vargen facility and the cache-stuff in Transformation
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
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder let i = newkey $ getBMap s
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder put $ s { getBMap = (getBMap s) { newkey = i + 1 } }
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder return $ "?" ++ show i
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder-- ----------------------------------------------------------------------
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder-- * Maple syntax functions
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder-- ----------------------------------------------------------------------
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintExp :: EXPRESSION -> String
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintExp = exportExp
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder--printExp = show . pretty
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 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 MaederprintEvaluation :: EXPRESSION -> String
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintEvaluation e = printExp e ++ ";"
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintLookup :: String -> String
c26ff5708c4a855bf9503b3001bcc19e5fd6286fChristian MaederprintLookup n = n ++ ";"
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederThe evalf makes the decision much faster. As we verify the result formally
f799084b320209cdd71a29e74fff1be054c1d342Christian Maederthis should not be problematic in a formal context!
c26ff5708c4a855bf9503b3001bcc19e5fd6286fChristian MaederIn the following context "is" gives up if we do not use "evalf":
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 MaederprintBooleanExpr :: EXPRESSION -> String
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintBooleanExpr e = concat [ "is(evalf(", printExp e, "));" ]
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: "
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder-- The evalf is mandatory if we use the if-statement for encoding
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 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: "
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder-- ----------------------------------------------------------------------
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder-- * Generic Communication Interface
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder-- ----------------------------------------------------------------------
3ab1e7a18f3fc3eb004464bc54b7df4483f1f060Christian Maeder The generic interface abstracts over the concrete evaluation function
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 [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)
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 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
wrapCommand :: IOS PC.CommandState a -> IOS MITrans a
(res, _) <- runIOS (getMI mit) $ PC.call (channelTimeout mit) s
res <- lift $ wrapCommand $ PC.call (channelTimeout mit) s
-> PC.DTime -- ^ timeout for response
cs <- PC.start (maplecmd ++ " -q") v
(_, cs') <- runIOS cs $ PC.call 0.5
fmap fst $ runIOS (getMI rit) (PC.call 0.5 $ "with(" ++ s ++ ");")
(ec, _) <- runIOS (getMI mit) $ PC.close $ Just "quit;"
-> PC.DTime -- ^ timeout for response