21c27810fa966e9253073efaf7f36458715d84bbEwaryst Schulz{-# LANGUAGE FlexibleInstances, TypeSynonymInstances #-}
25ae784bc2e848d6c2d53de84b4236449857e4ccEwaryst SchulzDescription : Maple instance for the AssignmentStore class
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzCopyright : (c) Ewaryst Schulz, DFKI Bremen 2010
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzMaintainer : Ewaryst.Schulz@dfki.de
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzStability : experimental
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst SchulzPortability : portable
25ae784bc2e848d6c2d53de84b4236449857e4ccEwaryst SchulzMaple as AssignmentStore
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulzimport Common.ProverTools (missingExecutableInPath)
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulzimport Common.Utils (getEnvDef, trimLeft)
8c22ca329de452600ec3e6384394890c1b695079Ewaryst Schulzimport CSL.Parse_AS_Basic (parseExpression)
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz-- the process communication interface
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulzimport qualified Interfaces.Process as PC
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- import Control.Monad.Trans (MonadTrans (..), MonadIO (..))
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Control.Monad.Error (ErrorT (..), MonadError (..))
44eca622a16639b4a1a3d4fd088c7c3bfff89b8eEwaryst Schulzimport Data.List hiding (lookup)
0aba0666fda59f604db05c7a70e4790f4d4e47e7Ewaryst Schulzimport qualified Data.Set as Set
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulzimport System.Exit (ExitCode)
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulzimport Prelude hiding (lookup)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- ----------------------------------------------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederMaple Types and Instances
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder---------------------------------------------------------------------- -}
f474203c4cef7d85cb078f15ce5c2cea71e9a030Ewaryst Schulztype ConnectInfo = (PC.CommandState, PC.DTime)
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz-- | MapleInterpreter with Translator based on the CommandState
f474203c4cef7d85cb078f15ce5c2cea71e9a030Ewaryst Schulztype MITrans = ASState ConnectInfo
f474203c4cef7d85cb078f15ce5c2cea71e9a030Ewaryst SchulzupdateCS :: PC.CommandState -> ConnectInfo -> ConnectInfo
f474203c4cef7d85cb078f15ce5c2cea71e9a030Ewaryst SchulzupdateCS cs (_, dt) = (cs, dt)
f474203c4cef7d85cb078f15ce5c2cea71e9a030Ewaryst SchulzupdateDT :: PC.DTime -> ConnectInfo -> ConnectInfo
f474203c4cef7d85cb078f15ce5c2cea71e9a030Ewaryst SchulzupdateDT dt (cs, _) = (cs, dt)
f474203c4cef7d85cb078f15ce5c2cea71e9a030Ewaryst SchulzgetChannelTimeout :: MITrans -> PC.DTime
f474203c4cef7d85cb078f15ce5c2cea71e9a030Ewaryst SchulzgetChannelTimeout = snd . getConnectInfo
f474203c4cef7d85cb078f15ce5c2cea71e9a030Ewaryst SchulzsetChannelTimeout :: PC.DTime -> MITrans -> MITrans
f474203c4cef7d85cb078f15ce5c2cea71e9a030Ewaryst SchulzsetChannelTimeout dt = fmap (updateDT dt)
f474203c4cef7d85cb078f15ce5c2cea71e9a030Ewaryst SchulzgetMI :: MITrans -> PC.CommandState
f474203c4cef7d85cb078f15ce5c2cea71e9a030Ewaryst SchulzgetMI = fst . getConnectInfo
f474203c4cef7d85cb078f15ce5c2cea71e9a030Ewaryst SchulzsetMI :: PC.CommandState -> MITrans -> MITrans
f474203c4cef7d85cb078f15ce5c2cea71e9a030Ewaryst SchulzsetMI cs = fmap (updateCS cs)
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz-- Maple interface, built on CommandState
71dd29e7cfb990182dffa41faace353159c7ab44Ewaryst Schulztype MapleIO = ErrorT ASError (IOS MITrans)
25ae784bc2e848d6c2d53de84b4236449857e4ccEwaryst Schulzinstance AssignmentStore MapleIO where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder assign = genAssign mapleAssignDirect
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst Schulz assigns l = genAssigns mapleAssignsDirect l >> return ()
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst Schulz lookup = genLookup mapleLookupDirect
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst Schulz eval = genEval mapleEvalDirect
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst Schulz check = mapleCheck
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder names = liftM (SMem . getBMap) get
434337161e50b53db671671fad5edb814255830aEwaryst Schulz evalRaw s = get >>= liftIO . flip (mapleDirect True) s
0aba0666fda59f604db05c7a70e4790f4d4e47e7Ewaryst Schulz getUndefinedConstants e = do
0aba0666fda59f604db05c7a70e4790f4d4e47e7Ewaryst Schulz adg <- gets depGraph
0aba0666fda59f604db05c7a70e4790f4d4e47e7Ewaryst Schulz let g = isNothing . depGraphLookup adg
0aba0666fda59f604db05c7a70e4790f4d4e47e7Ewaryst Schulz return $ Set.filter g $ Set.map SimpleConstant $ setOfUserDefined e
0aba0666fda59f604db05c7a70e4790f4d4e47e7Ewaryst Schulz genNewKey = do
0aba0666fda59f604db05c7a70e4790f4d4e47e7Ewaryst Schulz let (bm, i) = genKey $ getBMap mit
0aba0666fda59f604db05c7a70e4790f4d4e47e7Ewaryst Schulz put mit { getBMap = bm }
01c4a854ca10779b54d7ab57ee98e476077f1f15Ewaryst Schulz getDepGraph = gets depGraph
01c4a854ca10779b54d7ab57ee98e476077f1f15Ewaryst Schulz updateConstant n def =
01c4a854ca10779b54d7ab57ee98e476077f1f15Ewaryst Schulz let f gr = updateGraph gr n
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder DepGraphAnno { annoDef = def
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , annoVal = () }
01c4a854ca10779b54d7ab57ee98e476077f1f15Ewaryst Schulz mf mit = mit { depGraph = f $ depGraph mit }
f474203c4cef7d85cb078f15ce5c2cea71e9a030Ewaryst Schulzinstance VCGenerator MapleIO where
a46759a60a40e273585c54c971213d5cd6dc7d00Ewaryst Schulz addVC ea e = do
0f541fef46255a09d1143a9cbf3e2dbafb610923Ewaryst Schulz $ (text "Verification condition for" <+> pretty ea <> text ":")
0f541fef46255a09d1143a9cbf3e2dbafb610923Ewaryst Schulz $++$ printExpForVC e
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder {- s = show $ printExpForVC e <> text ";"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder s = (++ "\n\n;\n\n") $ showRaw $ text "VC for" <+> pretty ea <> text ":" $++$ pretty e
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedervcHdl = stdout -}
a46759a60a40e273585c54c971213d5cd6dc7d00Ewaryst Schulz vcHdl <- liftM (fromMaybe stdout) $ gets vericondOut
a46759a60a40e273585c54c971213d5cd6dc7d00Ewaryst Schulz liftIO $ hPutStrLn vcHdl s where
a46759a60a40e273585c54c971213d5cd6dc7d00Ewaryst Schulzinstance StepDebugger MapleIO where
a46759a60a40e273585c54c971213d5cd6dc7d00Ewaryst Schulz setDebugMode b = modify mf where mf mit = mit { debugMode = b }
a46759a60a40e273585c54c971213d5cd6dc7d00Ewaryst Schulz getDebugMode = gets debugMode
0f541fef46255a09d1143a9cbf3e2dbafb610923Ewaryst Schulzinstance SymbolicEvaluator MapleIO where
0f541fef46255a09d1143a9cbf3e2dbafb610923Ewaryst Schulz setSymbolicMode b = modify mf where mf mit = mit { symbolicMode = b }
0f541fef46255a09d1143a9cbf3e2dbafb610923Ewaryst Schulz getSymbolicMode = gets symbolicMode
105837926c174394ac05c02471215fb6d68a780fEwaryst Schulzinstance MessagePrinter MapleIO where
105837926c174394ac05c02471215fb6d68a780fEwaryst Schulz printMessage = liftIO . putStrLn
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- ----------------------------------------------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederMaple syntax functions
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder---------------------------------------------------------------------- -}
21c27810fa966e9253073efaf7f36458715d84bbEwaryst Schulzdata OfMaple a = OfMaple { mplValue :: a }
21c27810fa966e9253073efaf7f36458715d84bbEwaryst Schulztype MaplePrinter = Reader (OfMaple OpInfoNameMap)
21c27810fa966e9253073efaf7f36458715d84bbEwaryst Schulzinstance ExpressionPrinter MaplePrinter where
21c27810fa966e9253073efaf7f36458715d84bbEwaryst Schulz getOINM = asks mplValue
21c27810fa966e9253073efaf7f36458715d84bbEwaryst Schulz printOpname = return . text . mplShowOPNAME
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederprintMaplePretty :: MaplePrinter Doc -> Doc
21c27810fa966e9253073efaf7f36458715d84bbEwaryst SchulzprintMaplePretty = flip runReader $ OfMaple mapleOpInfoNameMap
21c27810fa966e9253073efaf7f36458715d84bbEwaryst Schulzclass MaplePretty a where
21c27810fa966e9253073efaf7f36458715d84bbEwaryst Schulz mplPretty :: a -> Doc
21c27810fa966e9253073efaf7f36458715d84bbEwaryst Schulzinstance MaplePretty EXPRESSION where
21c27810fa966e9253073efaf7f36458715d84bbEwaryst Schulz mplPretty e = printMaplePretty $ printExpression e
21c27810fa966e9253073efaf7f36458715d84bbEwaryst Schulzinstance MaplePretty AssDefinition where
21c27810fa966e9253073efaf7f36458715d84bbEwaryst Schulz mplPretty def = printMaplePretty $ printAssDefinition def
21c27810fa966e9253073efaf7f36458715d84bbEwaryst Schulzinstance MaplePretty String where
21c27810fa966e9253073efaf7f36458715d84bbEwaryst Schulz mplPretty = text
21c27810fa966e9253073efaf7f36458715d84bbEwaryst Schulzinstance (MaplePretty a, MaplePretty b) => MaplePretty [(a, b)] where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder mplPretty = ppPairlist mplPretty mplPretty braces sepBySemis (<>)
819c43ddaab748a3668c192fb2d1f70070dced59Ewaryst SchulzprintExp :: EXPRESSION -> String
21c27810fa966e9253073efaf7f36458715d84bbEwaryst SchulzprintExp = show . mplPretty
21c27810fa966e9253073efaf7f36458715d84bbEwaryst SchulzmplShowOPNAME :: OPNAME -> String
21c27810fa966e9253073efaf7f36458715d84bbEwaryst SchulzmplShowOPNAME OP_approx = "evalf"
21c27810fa966e9253073efaf7f36458715d84bbEwaryst SchulzmplShowOPNAME x = showOPNAME x
7b4b3c800d82cbdef5ce44d26e3037c714b03c07Ewaryst SchulzmapleOpInfoMap :: OpInfoMap
7b4b3c800d82cbdef5ce44d26e3037c714b03c07Ewaryst SchulzmapleOpInfoMap = operatorInfoMap
ee3bb87ab2da52ee1ad0c6675ea8b699b0af9ddcEwaryst SchulzmapleBindInfoMap :: BindInfoMap
ee3bb87ab2da52ee1ad0c6675ea8b699b0af9ddcEwaryst SchulzmapleBindInfoMap = operatorBindInfoMap
7b4b3c800d82cbdef5ce44d26e3037c714b03c07Ewaryst SchulzmapleOpInfoNameMap :: OpInfoNameMap
7b4b3c800d82cbdef5ce44d26e3037c714b03c07Ewaryst SchulzmapleOpInfoNameMap = operatorInfoNameMap
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst SchulzprintAssignment :: String -> AssDefinition -> String
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst SchulzprintAssignment n (ConstDef e) = concat [n, ":= ", printExp e, ":", n, ";"]
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst SchulzprintAssignment n (FunDef l e) = concat [ n, ":= proc", args, printExp e
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst Schulz , " end proc:", n, args, ";"]
44eca622a16639b4a1a3d4fd088c7c3bfff89b8eEwaryst Schulz where args = concat [ "(", intercalate ", " l, ") " ]
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst SchulzprintAssignmentWithEval :: String -> AssDefinition -> String
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst SchulzprintAssignmentWithEval n (ConstDef e) =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- concat [n, ":= evalf(", printExp e, "):", n, " &+ 0", ";"]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederconcat [n, ":= evalf(", printExp e, "):", n, ";"] -}
d3ea4ab5527bc4bd7381d39ecbc4af2199f54341Ewaryst Schulz concat [n, ":= evalf(", printExp e, "):g(", n, ")", ";"]
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst SchulzprintAssignmentWithEval n (FunDef l e) = concat [ n, ":= proc", args, printExp e
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst Schulz , " end proc:", n, args, ";"]
f14bf11310b51516794b2ad792907c45ebeb73d7Ewaryst Schulz where args = concat [ "(", intercalate ", " l, ") " ]
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzprintEvaluation :: EXPRESSION -> String
819c43ddaab748a3668c192fb2d1f70070dced59Ewaryst SchulzprintEvaluation e = printExp e ++ ";"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- printEvaluationWithEval :: EXPRESSION -> String
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederprintEvaluationWithEval e = "evalf(" ++ printExp e ++ ");" -}
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzprintLookup :: String -> String
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzprintLookup n = n ++ ";"
01c4a854ca10779b54d7ab57ee98e476077f1f15Ewaryst SchulzThe evalf makes the decision much faster. As we verify the result formally
01c4a854ca10779b54d7ab57ee98e476077f1f15Ewaryst Schulzthis should not be problematic in a formal context!
01c4a854ca10779b54d7ab57ee98e476077f1f15Ewaryst SchulzIn the following context "is" gives up if we do not use "evalf":
01c4a854ca10779b54d7ab57ee98e476077f1f15Ewaryst Schulzx2 := cos(10+cos(10)/sin(10)+cos(10+cos(10)/sin(10))/sin(10+cos(10)/sin(10))
01c4a854ca10779b54d7ab57ee98e476077f1f15Ewaryst Schulz + cos(10+cos(10)/sin(10)+cos(10+cos(10)/sin(10))/sin(10+cos(10)/sin(10)))
01c4a854ca10779b54d7ab57ee98e476077f1f15Ewaryst Schulz / sin(10+cos(10)/sin(10)+cos(10+cos(10)/sin(10))/sin(10+cos(10)/sin(10))));
01c4a854ca10779b54d7ab57ee98e476077f1f15Ewaryst Schulzis(abs(x2)<1.0e-4);
01c4a854ca10779b54d7ab57ee98e476077f1f15Ewaryst SchulzprintBooleanExpr :: EXPRESSION -> String
819c43ddaab748a3668c192fb2d1f70070dced59Ewaryst SchulzprintBooleanExpr e = concat [ "is(evalf(", printExp e, "));" ]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- The evalf is mandatory if we use the if-statement for encoding
877770f8a4c927134bf689e17208a897032893f5Ewaryst Schulz-- | As maple does not evaluate boolean expressions we encode them in an
877770f8a4c927134bf689e17208a897032893f5Ewaryst Schulz-- if-stmt and transform the numeric response back.
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzprintBooleanExpr :: EXPRESSION -> String
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzprintBooleanExpr e = concat [ "if evalf("
819c43ddaab748a3668c192fb2d1f70070dced59Ewaryst Schulz , printExp e, ") then 1 else 0 fi;"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- ----------------------------------------------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederMethods for Maple 'AssignmentStore' Interface
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder---------------------------------------------------------------------- -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- | Evaluate the given String as maple expression and
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederparse the result to an maybe expression. If the boolean flag is false
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederthe result will not be parsed. -}
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst SchulzevalMapleString' :: Bool -- ^ Use parser
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst Schulz -> String -- ^ the maple command to evaluate
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst Schulz -> MapleIO (Maybe EXPRESSION)
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst SchulzevalMapleString' b s = do
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst Schulz -- 0.09 seconds is a critical value for the accepted response time of Maple
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst Schulz res <- lift $ wrapCommand $ PC.call (getChannelTimeout mit) s
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst Schulz return $ if b
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -- then parseExpression mapleOpInfoMap $ trimLeft $ removeOutputComments res
ee3bb87ab2da52ee1ad0c6675ea8b699b0af9ddcEwaryst Schulz then parseExpression (mapleOpInfoMap, mapleBindInfoMap) $ trimLeft res
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst Schulz-- | Evaluate the given String as maple expression and skip the result
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst SchulzsendMapleString :: String -- ^ the maple command to evaluate
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst Schulz -> MapleIO ()
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst SchulzsendMapleString s = evalMapleString' False s >> return ()
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- | Evaluate the given String as maple expression and
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederparse the result back to an expression. -}
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst SchulzevalMapleString :: String -- ^ an error message for the failure case
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst Schulz -> String -- ^ the maple command to evaluate
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst Schulz -> MapleIO EXPRESSION
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst SchulzevalMapleString msg s = do
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst Schulz mE <- evalMapleString' True s
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst Schulz Just e -> return e
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst Schulz _ -> throwError $ ASError InterfaceError msg
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst SchulzmapleAssignDirect :: String -> AssDefinition -> MapleIO EXPRESSION
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst SchulzmapleAssignDirect n def = do
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst Schulz sm <- getSymbolicMode
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst Schulz let f = if sm then printAssignment else printAssignmentWithEval
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst Schulz msg = "mapleAssignDirect: unparseable result for assignment of "
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ++ (show (pretty n) <+> pretty def)
21c27810fa966e9253073efaf7f36458715d84bbEwaryst Schulz prettyInfo3 $ mplPretty [(n, def)]
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst Schulz evalMapleString msg $ f n def
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst SchulzmapleAssignsDirect :: [(String, AssDefinition)] -> MapleIO ()
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst SchulzmapleAssignsDirect =
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst Schulz sendMapleString . unlines . map (uncurry printAssignment)
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst SchulzmapleLookupDirect :: String -> MapleIO EXPRESSION
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst SchulzmapleLookupDirect n = evalMapleString msg $ printLookup n where
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst Schulz msg = "mapleLookupDirect: unparseable result for lookup of " ++ n
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst SchulzmapleEvalDirect :: EXPRESSION -> MapleIO EXPRESSION
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst SchulzmapleEvalDirect e = do
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- b <- getSymbolicMode
21c27810fa966e9253073efaf7f36458715d84bbEwaryst Schulz let -- f = if b then printEvaluation else printEvaluationWithEval
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst Schulz msg = "mapleEvalDirect: unparseable result for evaluation of "
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ++ show (pretty e)
21c27810fa966e9253073efaf7f36458715d84bbEwaryst Schulz evalMapleString msg $ printEvaluation e -- f e
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst SchulzmapleCheck :: EXPRESSION -> MapleIO Bool
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst SchulzmapleCheck e = do
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst Schulz let msg = "mapleCheck: unparseable result for evaluation of "
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ++ show (pretty e)
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst Schulz eB <- genCheck (evalMapleString msg . printBooleanExpr) e
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst Schulz Right b -> return b
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst Schulz throwError $ ASError CASError $
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst Schulz concat [ "mapleCheck: CAS error for expression "
6091bd7fb65c7def81e5a5d0359ceeed7a88bb7fEwaryst Schulz , show e, "\n", s ]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- ----------------------------------------------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederThe Communication Interface
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder---------------------------------------------------------------------- -}
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzwrapCommand :: IOS PC.CommandState a -> IOS MITrans a
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzwrapCommand ios = do
f474203c4cef7d85cb078f15ce5c2cea71e9a030Ewaryst Schulz let map' x = setMI x r
f474203c4cef7d85cb078f15ce5c2cea71e9a030Ewaryst Schulz stmap map' getMI ios
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz-- | A direct way to communicate with Maple
552e47c304b69cf5690829e73b002bb7baba919bEwaryst SchulzmapleDirect :: Bool -> MITrans -> String -> IO String
0aba0666fda59f604db05c7a70e4790f4d4e47e7Ewaryst SchulzmapleDirect b mit s = do
f474203c4cef7d85cb078f15ce5c2cea71e9a030Ewaryst Schulz (res, _) <- runIOS (getMI mit) $ PC.call (getChannelTimeout mit) s
552e47c304b69cf5690829e73b002bb7baba919bEwaryst Schulz return $ if b then removeOutputComments res else res
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz-- | init the maple communication
01c4a854ca10779b54d7ab57ee98e476077f1f15Ewaryst SchulzmapleInit :: AssignmentDepGraph ()
01c4a854ca10779b54d7ab57ee98e476077f1f15Ewaryst Schulz -> Int -- ^ Verbosity level
0aba0666fda59f604db05c7a70e4790f4d4e47e7Ewaryst Schulz -> PC.DTime -- ^ timeout for response
01c4a854ca10779b54d7ab57ee98e476077f1f15Ewaryst Schulz -> IO MITrans
0aba0666fda59f604db05c7a70e4790f4d4e47e7Ewaryst SchulzmapleInit adg v to = do
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz rc <- lookupMapleShellCmd
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz libpath <- getEnvDef "HETS_MAPLELIB"
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz $ error "mapleInit: Environment variable HETS_MAPLELIB not set."
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz Left maplecmd -> do
8b6641f92fd899798421ef2b3d3e335da7425030Ewaryst Schulz cs <- PC.start (maplecmd ++ " -q") v
baec30a71697583b5e73008fb17c2563da2830f5Ewaryst Schulz $ Just PC.defaultConfig { PC.startTimeout = 3 }
0aba0666fda59f604db05c7a70e4790f4d4e47e7Ewaryst Schulz (_, cs') <- runIOS cs $ PC.call 0.5
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz $ concat [ "interface(prettyprint=0); Digits := 10;"
931b637f93ac196223b69e414f8c184b91191febEwaryst Schulz , "libname := \"", libpath, "\", libname;" ]
f54cad0338da90c6789bb9baae1caec50d994b3aEwaryst Schulz return $ initASState (cs', to) mapleOpInfoMap adg v
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> error "Could not find maple shell command!"
931b637f93ac196223b69e414f8c184b91191febEwaryst Schulz-- | Loads a maple module such as intpakX or intCompare
931b637f93ac196223b69e414f8c184b91191febEwaryst SchulzmapleLoadModule :: MITrans -> String -> IO String
931b637f93ac196223b69e414f8c184b91191febEwaryst SchulzmapleLoadModule rit s =
931b637f93ac196223b69e414f8c184b91191febEwaryst Schulz fmap fst $ runIOS (getMI rit) (PC.call 0.5 $ "with(" ++ s ++ ");")
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzmapleExit :: MITrans -> IO (Maybe ExitCode)
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzmapleExit mit = do
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz (ec, _) <- runIOS (getMI mit) $ PC.close $ Just "quit;"
44eca622a16639b4a1a3d4fd088c7c3bfff89b8eEwaryst SchulzexecWithMaple :: MITrans -> MapleIO a -> IO (MITrans, a)
71dd29e7cfb990182dffa41faace353159c7ab44Ewaryst SchulzexecWithMaple mit m = do
71dd29e7cfb990182dffa41faace353159c7ab44Ewaryst Schulz let err s = error $ "execWithMaple: " ++ s
71dd29e7cfb990182dffa41faace353159c7ab44Ewaryst Schulz (res, mit') <- runIOS mit $ runErrorT m
71dd29e7cfb990182dffa41faace353159c7ab44Ewaryst Schulz Left s' -> err $ asErrorMsg s'
71dd29e7cfb990182dffa41faace353159c7ab44Ewaryst Schulz Right x -> return (mit', x)
0f541fef46255a09d1143a9cbf3e2dbafb610923Ewaryst SchulzrunWithMaple :: AssignmentDepGraph () -> Int -- ^ Verbosity level
0aba0666fda59f604db05c7a70e4790f4d4e47e7Ewaryst Schulz -> PC.DTime -- ^ timeout for response
0aba0666fda59f604db05c7a70e4790f4d4e47e7Ewaryst Schulz -> [String] -> MapleIO a
0aba0666fda59f604db05c7a70e4790f4d4e47e7Ewaryst Schulz -> IO (MITrans, a)
0aba0666fda59f604db05c7a70e4790f4d4e47e7Ewaryst SchulzrunWithMaple adg i to l m = do
0aba0666fda59f604db05c7a70e4790f4d4e47e7Ewaryst Schulz mit <- mapleInit adg i to
931b637f93ac196223b69e414f8c184b91191febEwaryst Schulz mapM_ (mapleLoadModule mit) l
d3ea4ab5527bc4bd7381d39ecbc4af2199f54341Ewaryst Schulz -- wraps an interval around the number
d3ea4ab5527bc4bd7381d39ecbc4af2199f54341Ewaryst Schulz let debugFun = "g := proc(v) z:=abs(Float(v,1-Digits)):[v-z, v+z] end;"
d3ea4ab5527bc4bd7381d39ecbc4af2199f54341Ewaryst Schulz runIOS (getMI mit) $ PC.call 0.3 debugFun
931b637f93ac196223b69e414f8c184b91191febEwaryst Schulz execWithMaple mit m
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- ----------------------------------------------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederThe Maple system
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder---------------------------------------------------------------------- -}
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz-- | Left String is success, Right String is failure
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzlookupMapleShellCmd :: IO (Either String String)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederlookupMapleShellCmd = do
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz cmd <- getEnvDef "HETS_MAPLE" "maple"
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz -- check that prog exists
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz noProg <- missingExecutableInPath cmd
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz let f = if noProg then Right else Left
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz return $ f cmd
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz-- | Removes lines starting with ">"
f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzremoveOutputComments :: String -> String
0aba0666fda59f604db05c7a70e4790f4d4e47e7Ewaryst SchulzremoveOutputComments =
0aba0666fda59f604db05c7a70e4790f4d4e47e7Ewaryst Schulz filter (/= '\\') . concat . filter (not . isPrefixOf ">") . lines
877770f8a4c927134bf689e17208a897032893f5Ewaryst Schulz{- Some problems with the maximization in Maple:
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder> Maximize(-x^6+t*x^3-3, {t >= -1000, t <= 1000}, x=-2..0);
877770f8a4c927134bf689e17208a897032893f5Ewaryst SchulzError, (in Optimization:-NLPSolve) no improved point could be found
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder> Maximize(-x^t*x^3-3, {t >= -1000, t <= 1000}, x=-2..0);
877770f8a4c927134bf689e17208a897032893f5Ewaryst SchulzError, (in Optimization:-NLPSolve) complex value encountered
819c43ddaab748a3668c192fb2d1f70070dced59Ewaryst Schulz-- works better:
819c43ddaab748a3668c192fb2d1f70070dced59Ewaryst Schulzrhs(maximize(-(tan(x)-1/12)^2 -1, x=-1..1, location)[2,1,1,1]);