MapleInterpreter.hs revision 25ae784bc2e848d6c2d53de84b4236449857e4cc
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maeder{-# LANGUAGE FlexibleInstances, FlexibleContexts, TypeSynonymInstances
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maeder , UndecidableInstances, OverlappingInstances, MultiParamTypeClasses #-}
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederModule : $Header$
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederDescription : Maple instance for the AssignmentStore class
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian MaederCopyright : (c) Ewaryst Schulz, DFKI Bremen 2010
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederLicense : GPLv2 or higher, see LICENSE.txt
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederMaintainer : Ewaryst.Schulz@dfki.de
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian MaederStability : experimental
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederPortability : non-portable (various glasgow extensions)
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian MaederMaple as AssignmentStore
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maederimport Common.ProverTools (missingExecutableInPath)
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maederimport Common.Utils (getEnvDef, trimLeft)
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport CSL.Parse_AS_Basic (parseResult)
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maederimport CSL.Reduce_Interface (exportExp)
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder-- the process communication interface
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maederimport qualified Interfaces.Process as PC
2b9022bd5dfb351d1d80f61680336effeccfa23eChristian Maederimport Control.Monad.Trans (MonadTrans (..))
cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maederimport Control.Monad.State (MonadState (..))
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maederimport System.Exit (ExitCode)
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maederimport Prelude hiding (lookup)
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder-- ----------------------------------------------------------------------
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder-- * Maple Calculator Instances
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder-- ----------------------------------------------------------------------
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder-- | MapleInterpreter with Translator based on the CommandState
04dada28736b4a237745e92063d8bdd49a362debChristian Maederdata MITrans = MITrans { getBMap :: BMap
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder-- Maple interface, built on CommandState
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maedertype MapleIO = ResultT (IOS MITrans)
5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maederinstance AssignmentStore MapleIO where
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maeder assign = mapleAssign evalMapleString mapleTransS mapleTransE
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder lookup = mapleLookup evalMapleString mapleTransS
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder eval = mapleEval evalMapleString mapleTransE
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder check = mapleCheck evalMapleString mapleTransE
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder names = get >>= return . SMem . getBMap
cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder-- ----------------------------------------------------------------------
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder-- * Maple Transformation Instances
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder-- ----------------------------------------------------------------------
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder-- | Variable generator instance for internal variables on the Hets-side,
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder-- in contrast to the newvar generation in lookupOrInsert of the BMap, which
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder-- generates variables for the Maple-side. We use nevertheless the same counter.
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maederinstance VarGen MapleIO where
9ae2df7accdbf35839d56f90e1e8662be7112cdbChristian Maeder let i = newkey $ getBMap s
9ae2df7accdbf35839d56f90e1e8662be7112cdbChristian Maeder put $ s { getBMap = (getBMap s) { newkey = i + 1 } }
ad623ebb0fa505940a039fe967ecff8749719ac9Christian Maeder return $ "?" ++ show i
9ae2df7accdbf35839d56f90e1e8662be7112cdbChristian Maeder-- ----------------------------------------------------------------------
9ae2df7accdbf35839d56f90e1e8662be7112cdbChristian Maeder-- * Maple syntax functions
9ae2df7accdbf35839d56f90e1e8662be7112cdbChristian Maeder-- ----------------------------------------------------------------------
9ae2df7accdbf35839d56f90e1e8662be7112cdbChristian MaedercslMapleDefaultMapping :: [(OPNAME, String)]
9ae2df7accdbf35839d56f90e1e8662be7112cdbChristian MaedercslMapleDefaultMapping =
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder let idmapping = map (\ x -> (x, show x))
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder-- ampmapping = map (\ x -> (x, "&" ++ show x))
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder possibleIntervalOps = [ OP_mult, OP_div, OP_plus, OP_minus, OP_neg
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder , OP_cos, OP_sin, OP_tan, OP_sqrt, OP_abs
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder , OP_neq, OP_lt, OP_leq, OP_eq, OP_gt, OP_geq ]
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder logicOps = [ OP_and, OP_or, OP_impl ]
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder otherOps = [OP_factor, OP_maximize]
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder specialOp = (OP_pow, "^")
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder-- specialOp = (OP_pow, "&**")
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder in specialOp : idmapping logicOps
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder ++ idmapping possibleIntervalOps
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder ++ idmapping otherOps
ab0f35d8b9012e459417e086773049ce33dda2a0Christian MaederprintAssignment :: String -> EXPRESSION -> String
ab0f35d8b9012e459417e086773049ce33dda2a0Christian MaederprintAssignment n e = concat [n, ":= ", exportExp e, ";"]
ab0f35d8b9012e459417e086773049ce33dda2a0Christian MaederprintEvaluation :: EXPRESSION -> String
ab0f35d8b9012e459417e086773049ce33dda2a0Christian MaederprintEvaluation e = exportExp e ++ ";"
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederprintLookup :: String -> String
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederprintLookup n = n ++ ";"
ab0f35d8b9012e459417e086773049ce33dda2a0Christian Maeder-- | As maple does not evaluate boolean expressions we encode them in an
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- if-stmt and transform the numeric response back.
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederprintBooleanExpr :: EXPRESSION -> String
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederprintBooleanExpr e = concat [ "if evalf("
7dec34aee2b609b9535c48d060e0f7baf3536457Christian Maeder , exportExp e, ") then 1 else 0 fi;"
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian MaedergetBooleanFromExpr :: EXPRESSION -> Bool
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian MaedergetBooleanFromExpr (Int 1 _) = True
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian MaedergetBooleanFromExpr (Int 0 _) = False
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian MaedergetBooleanFromExpr e =
0b14ccc700093e203914052bf6aceda3164af730Christian Maeder error $ "getBooleanFromExpr: can't translate expression to boolean: "
9c03fbe72966fb21c99238c449efdb0126dae9deChristian Maeder-- ----------------------------------------------------------------------
9c03fbe72966fb21c99238c449efdb0126dae9deChristian Maeder-- * Generic Communication Interface
9c03fbe72966fb21c99238c449efdb0126dae9deChristian Maeder-- ----------------------------------------------------------------------
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder The generic interface abstracts over the concrete evaluation function
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian MaedermapleAssign :: (AssignmentStore s, MonadResult s) => (String -> s [EXPRESSION])
9c03fbe72966fb21c99238c449efdb0126dae9deChristian Maeder -> (ConstantName -> s String)
9c03fbe72966fb21c99238c449efdb0126dae9deChristian Maeder -> (EXPRESSION -> s EXPRESSION)
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder -> ConstantName -> EXPRESSION -> s ()
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaedermapleAssign ef trans transE n e = do
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder e' <- transE e
d48085f765fca838c1d972d2123601997174583dChristian Maeder n' <- trans n
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder ef $ printAssignment n' e'
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedermapleLookup :: (AssignmentStore s, MonadResult s) => (String -> s [EXPRESSION])
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder -> (ConstantName -> s String)
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder -> ConstantName -> s (Maybe EXPRESSION)
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedermapleLookup ef trans n = do
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder n' <- trans n
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder el <- ef $ printLookup n'
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder return $ listToMaybe el
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder-- we don't want to return nothing on id-lookup: "x; --> x"
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder-- if e == mkOp n [] then return Nothing else return $ Just e
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedermapleEval :: (AssignmentStore s, MonadResult s) => (String -> s [EXPRESSION])
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder -> (EXPRESSION -> s EXPRESSION)
a716971174535184da7713ed308423e355a4aa66Christian Maeder -> EXPRESSION -> s EXPRESSION
a716971174535184da7713ed308423e355a4aa66Christian MaedermapleEval ef trans e = do
a716971174535184da7713ed308423e355a4aa66Christian Maeder e' <- trans e
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder el <- ef $ printEvaluation e'
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder then error $ "mapleEval: expression " ++ show e' ++ " couldn't be evaluated"
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder else return $ head el
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedermapleCheck :: (AssignmentStore s, MonadResult s) => (String -> s [EXPRESSION])
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder -> (EXPRESSION -> s EXPRESSION)
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder -> EXPRESSION -> s Bool
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian MaedermapleCheck ef trans e = do
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder e' <- trans e
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder el <- ef $ printBooleanExpr e'
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder then error $ "mapleCheck: expression " ++ show e' ++ " couldn't be evaluated"
a716971174535184da7713ed308423e355a4aa66Christian Maeder else return $ getBooleanFromExpr $ head el
a716971174535184da7713ed308423e355a4aa66Christian Maeder-- ----------------------------------------------------------------------
a716971174535184da7713ed308423e355a4aa66Christian Maeder-- * The Communication Interface
a716971174535184da7713ed308423e355a4aa66Christian Maeder-- ----------------------------------------------------------------------
793945d4ac7c0f22760589c87af8e71427c76118Christian MaederwrapCommand :: IOS PC.CommandState a -> IOS MITrans a
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian MaederwrapCommand ios = do
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder let map' x = r { getMI = x }
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder stmap map' getMI ios
cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maeder-- | A direct way to communicate with Maple
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaedermapleDirect :: MITrans -> String -> IO String
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian MaedermapleDirect rit s = do
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder (res, _) <- runIOS (getMI rit) (PC.call 0.5 s)
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder return $ removeOutputComments res
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedermapleTransE :: EXPRESSION -> MapleIO EXPRESSION
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedermapleTransE e = do
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder let bm = getBMap r
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder (bm', e') = translateEXPRESSION bm e
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder put r { getBMap = bm' }
0b14ccc700093e203914052bf6aceda3164af730Christian MaedermapleTransS :: ConstantName -> MapleIO String
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedermapleTransS s = do
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder let bm = getBMap r
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder (bm', s') = lookupOrInsert bm $ Left s
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder put r { getBMap = bm' }
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederevalMapleString :: String -> MapleIO [EXPRESSION]
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian MaederevalMapleString s = do
cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maeder -- 0.09 seconds is a critical value for the accepted response time of Maple
ad623ebb0fa505940a039fe967ecff8749719ac9Christian Maeder res <- lift $ wrapCommand $ PC.call 0.7 s
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder let bm = getBMap r
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder trans = revtranslateEXPRESSION bm
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder return $ map trans $ maybeToList $ parseResult $ trimLeft
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder $ removeOutputComments res
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder-- | init the maple communication
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaedermapleInit :: Int -- ^ Verbosity level
ad623ebb0fa505940a039fe967ecff8749719ac9Christian Maeder -> IO MITrans
ad623ebb0fa505940a039fe967ecff8749719ac9Christian MaedermapleInit v = do
ad623ebb0fa505940a039fe967ecff8749719ac9Christian Maeder rc <- lookupMapleShellCmd
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder libpath <- getEnvDef "HETS_MAPLELIB"
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder $ error "mapleInit: Environment variable HETS_MAPLELIB not set."
ad623ebb0fa505940a039fe967ecff8749719ac9Christian Maeder Left maplecmd -> do
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder cs <- PC.start (maplecmd ++ " -q") v
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder $ Just PC.defaultConfig { PC.startTimeout = 3 }
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder (_, cs') <- runIOS cs $ PC.call 1.0
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder $ concat [ "interface(prettyprint=0); Digits := 10;"
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder , "libname := \"", libpath, "\", libname;"
20fe556546c9277cf017931a07d90add61f199d9Christian Maeder , "with(intpakX);with(intCompare);" ]
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder return MITrans { getBMap = initWithDefault cslMapleDefaultMapping
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder , getMI = cs'
c9b711a46e5138b2742727817c8071960e673073Christian Maeder _ -> error "Could not find maple shell command!"
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian MaedermapleExit :: MITrans -> IO (Maybe ExitCode)
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian MaedermapleExit mit = do
59c036af82aff7fbe074455dad50477b7878e2d8Christian Maeder (ec, _) <- runIOS (getMI mit) $ PC.close $ Just "quit;"
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder-- ----------------------------------------------------------------------
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder-- * The Maple system