44N/A{-# LANGUAGE FlexibleContexts, FlexibleInstances, TypeSynonymInstances #-}

44N/A{- |

44N/AModule : $Header$

44N/ADescription : Mathematica instance for the AssignmentStore class

44N/ACopyright : (c) Ewaryst Schulz, DFKI Bremen 2010

44N/ALicense : GPLv2 or higher, see LICENSE.txt

44N/A

44N/AMaintainer : Ewaryst.Schulz@dfki.de

44N/AStability : experimental

44N/APortability : non-portable (via imports)

44N/A

44N/AMathematica as AssignmentStore based on the Mathlink interface

44N/A-}

44N/A

44N/Amodule CSL.MathematicaInterpreter where

44N/A

44N/Aimport Common.Id

44N/Aimport Common.Doc

44N/Aimport Common.DocUtils

44N/A

44N/Aimport Common.MathLink

44N/A

44N/A

44N/Aimport CSL.AS_BASIC_CSL

44N/Aimport CSL.Print_AS

44N/Aimport CSL.Interpreter

44N/Aimport CSL.Verification

44N/Aimport CSL.DependencyGraph

44N/Aimport CSL.GenericInterpreter

44N/A

44N/A

44N/Aimport Control.Monad

44N/A--import Control.Monad.Trans (MonadTrans (..), MonadIO (..))

44N/Aimport Control.Monad.Error

44N/Aimport Control.Monad.State

44N/Aimport Control.Monad.Reader

44N/A

44N/Aimport Data.List hiding (lookup)

44N/Aimport qualified Data.Set as Set

44N/Aimport Data.Maybe

44N/Aimport System.IO

44N/A

44N/A

44N/Aimport Prelude hiding (lookup)

44N/A

44N/A

44N/A

44N/A-- ----------------------------------------------------------------------

44N/A-- * Mathematica Types and Instances

44N/A-- ----------------------------------------------------------------------

44N/A

44N/A-- | MathematicaInterpreter with Translator based on the MathLink interface

44N/Atype MathState = ASState (MLState, Maybe FilePath)

44N/A

44N/A-- Mathematica interface, built on MathLink

44N/Atype MathematicaIO = ErrorT ASError (StateT MathState ML)

44N/A

44N/AgetMLState :: MathState -> MLState

44N/AgetMLState = fst . getConnectInfo

44N/A

44N/AgetMLLogFile :: MathState -> Maybe FilePath

44N/AgetMLLogFile = snd . getConnectInfo

44N/A

44N/A

44N/AliftML :: ML a -> MathematicaIO a

44N/AliftML = lift . lift

44N/A

44N/A

44N/Ainstance AssignmentStore MathematicaIO where

44N/A assign = genAssign mathematicaAssign

44N/A assigns l = genAssigns mathematicaAssigns l >> return ()

44N/A lookup = genLookup mathematicaLookup

44N/A eval = genEval mathematicaEval

44N/A check = mathematicaCheck

44N/A names = get >>= return . SMem . getBMap

44N/A evalRaw s = get >>= liftIO . mathematicaDirect s

44N/A

44N/A getUndefinedConstants e = do

44N/A adg <- gets depGraph

44N/A let g = isNothing . depGraphLookup adg

44N/A return $ Set.filter g $ Set.map SimpleConstant $ setOfUserDefined e

44N/A

44N/A genNewKey = do

44N/A mit <- get

44N/A let (bm, i) = genKey $ getBMap mit

44N/A put mit { getBMap = bm }

44N/A return i

44N/A

44N/A getDepGraph = gets depGraph

44N/A updateConstant n def =

44N/A let f gr = updateGraph gr n

44N/A $ DepGraphAnno { annoDef = def

44N/A , annoVal = () }

44N/A mf mit = mit { depGraph = f $ depGraph mit }

44N/A in modify mf

44N/A

44N/Ainstance VCGenerator MathematicaIO where

44N/A addVC ea e = do

44N/A vcHdl <- liftM (fromMaybe stdout) $ gets vericondOut

44N/A liftIO $ hPutStrLn vcHdl $ show $ printVCForIsabelle ea "lemma1" e

44N/A

44N/Ainstance StepDebugger MathematicaIO where

44N/A setDebugMode b = modify mf where mf mit = mit { debugMode = b }

44N/A getDebugMode = gets debugMode

44N/A

44N/Ainstance SymbolicEvaluator MathematicaIO where

44N/A setSymbolicMode b = modify mf where mf mit = mit { symbolicMode = b }

44N/A getSymbolicMode = gets symbolicMode

44N/A

44N/Ainstance MessagePrinter MathematicaIO where

44N/A printMessage = liftIO . putStrLn

44N/A

44N/A

44N/A-- ----------------------------------------------------------------------

44N/A-- * Mathematica syntax and special terms

44N/A-- ----------------------------------------------------------------------

44N/A

44N/AmmShowOPNAME :: OPNAME -> String

44N/AmmShowOPNAME x =

44N/A case x of

44N/A OP_plus -> "Plus"

44N/A OP_mult -> "Times"

44N/A OP_pow -> "Power"

44N/A OP_div -> "Divide"

44N/A

44N/A

44N/A OP_neq -> "Unequal"

44N/A OP_lt -> "Less"

44N/A OP_leq -> "LessEqual"

44N/A OP_eq -> "Equal"

44N/A OP_gt -> "Greater"

44N/A OP_geq -> "GreaterEqual"

44N/A

44N/A OP_sqrt -> "Sqrt"

44N/A OP_abs -> "Abs"

44N/A OP_sign -> "Sign"

44N/A

44N/A OP_max -> "Max"

44N/A OP_min -> "Min"

44N/A

44N/A OP_sin -> "Sin"

44N/A OP_cos -> "Cos"

44N/A OP_tan -> "Tan"

44N/A OP_cot -> "Cot"

44N/A OP_Pi -> "Pi"

44N/A

44N/A OP_and -> "And"

44N/A OP_not -> "Not"

44N/A OP_or -> "Or"

44N/A OP_impl -> "Implies"

44N/A OP_false -> "False"

44N/A OP_true -> "True"

44N/A

44N/A OP_approx -> "N"

44N/A

44N/A -- these functions have to be defined in a package

44N/A OP_minus -> "minus"

44N/A OP_neg -> "negate"

44N/A

44N/A OP_fthrt -> "fthrt"

44N/A

44N/A OP_maxloc -> "maxloc"

44N/A OP_minloc -> "minloc"

44N/A

44N/A OP_reldist -> "reldist"

44N/A OP_reldistLe -> "reldistLe"

44N/A

44N/A OP_undef -> "undef"

44N/A OP_failure -> "fail"

44N/A _ -> showOPNAME x

44N/A

44N/AmmShowOPID :: OPID -> String

44N/AmmShowOPID (OpId x) = mmShowOPNAME x

44N/AmmShowOPID (OpUser (SimpleConstant s)) = s

44N/AmmShowOPID _ = error "mmShowOpId: unsupported constant"

44N/A

44N/A

44N/AmmFlexFoldOpList :: [OPNAME]

44N/AmmFlexFoldOpList = [ OP_plus, OP_mult, OP_and, OP_or ]

44N/A

44N/AmathematicaOperatorInfo :: [OpInfo]

44N/AmathematicaOperatorInfo = toFlexFold mmFlexFoldOpList operatorInfo

-- | opInfoMap for mathematica's prdefined symbols

mathematicaOpInfoMap :: OpInfoMap

mathematicaOpInfoMap =

getOpInfoMap (mmShowOPNAME . opname) mathematicaOperatorInfo

-- | opInfoNameMap for mathematica's prdefined symbols

mathematicaOpInfoNameMap :: OpInfoNameMap

mathematicaOpInfoNameMap =

getOpInfoNameMap mathematicaOperatorInfo

toFlexFold :: [OPNAME] -> [OpInfo] -> [OpInfo]

toFlexFold nl oil = map f oil where

ns = Set.fromList nl

f oi | Set.member (opname oi) ns = oi { arity = -1, foldNAry = True }

| otherwise = oi

-- | mathematica term "Set"

mtDef :: String -> AssDefinition -> EXPRESSION

mtDef s (ConstDef e) = mkOp "Set" [mkOp s [], e]

mtDef s (FunDef args e) = mkOp "Set" [mkOp s $ map mtVarDecl args, e]

mtVarDecl :: String -> EXPRESSION

mtVarDecl s = mkOp "Pattern" [mkOp s [], mkOp "Blank" []]

mtList :: [EXPRESSION] -> EXPRESSION

mtList = mkOp "List"

mtCompound :: [EXPRESSION] -> EXPRESSION

mtCompound = mkOp "CompoundExpression"

mtIsBlank :: OPID -> Bool

mtIsBlank oi = mmShowOPID oi == "Blank"

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

-- * Mathematica pretty printing

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

data OfMathematica a = OfMathematica { mmValue :: a }

type MathPrinter = Reader (OfMathematica OpInfoNameMap)

instance ExpressionPrinter MathPrinter where

getOINM = asks mmValue

printOpname = return . text . mmShowOPNAME

printArgs = return . brackets . sepByCommas

prefixMode = return True

printVarDecl s = return $ text s <> text "_"

printMathPretty :: (MathPrinter Doc) -> Doc

printMathPretty = flip runReader $ OfMathematica mathematicaOpInfoNameMap

class MathPretty a where

mmPretty :: a -> Doc

instance MathPretty EXPRESSION where

mmPretty e = printMathPretty $ printExpression e

instance MathPretty AssDefinition where

mmPretty def = printMathPretty $ printAssDefinition def

instance MathPretty String where

mmPretty = text

instance (MathPretty a, MathPretty b) => MathPretty [(a, b)] where

mmPretty l = ppPairlist mmPretty mmPretty braces sepBySemis (<>) l

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

-- * Mathematica over ML Interface

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

sendExpressionString :: String -> ML ()

sendExpressionString s = do

mlPutFunction' "ToExpression" 1

mlPutString s

return ()

sendExpression :: Bool -- ^ symbolic mode

-> EXPRESSION -> ML ()

sendExpression sm e =

case e of

Var token -> mlPutSymbol (tokStr token) >> return ()

Op oi _ [] _

-- blanks get extra empty brackets

| mtIsBlank oi -> mlPutFunction' "Blank" 0 >> return ()

| otherwise -> mlPutSymbol (mmShowOPID oi) >> return ()

Op oi _ exps _ -> do

mlPutFunction' (mmShowOPID oi) (length exps)

mapM_ (sendExpression sm) exps

Int i _ -> mlPutInteger'' i >> return ()

Rat r _

| sm -> putRational r

| otherwise -> mlPutFunction' "N" 1 >> putRational r

where putRational r' = do

let (n1, dn2) = toFraction r'

mlPutFunction' "Rational" 2

mlPutInteger'' n1

mlPutInteger'' dn2

return ()

List _ _ -> error "sendExpression: List not supported"

Interval _ _ _ -> error "sendExpression: Interval not supported"

receiveExpression :: ML EXPRESSION

receiveExpression = do

et <- mlGetNext

let mkMLOp s args = mkAndAnalyzeOp mathematicaOpInfoMap s [] args nullRange

pr | et == dfMLTKSYM = liftM (flip mkMLOp []) mlGetSymbol

| et == dfMLTKINT = liftM (flip Int nullRange) mlGetInteger''

| et == dfMLTKREAL = liftM (flip Rat nullRange . toRational) mlGetReal'

| et == dfMLTKFUNC =

do

ac <- mlGetArgCount

if ac == 0 then mlProcError

else do

-- the head is expected to be a symbol

et' <- mlGetNext

s <- if et' == dfMLTKSYM then mlGetSymbol else

error $ "receiveExpression: Expecting symbol at "

++ "function head, but got " ++ show et'

if s == "Rational" then

do

nn <- mlGetInteger''

dn <- mlGetInteger''

return $ Rat (fromFraction nn dn) nullRange

else

liftM (mkMLOp s) $ forM [1..ac] $ const receiveExpression

| et == dfMLTKERROR = mlProcError

| otherwise = mlProcError

pr

receiveString :: ML String

receiveString = do

et <- mlGetNext

if et == dfMLTKSTR then mlGetString

else error $ "receiveString: Got " ++ showTK et

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

-- * Methods for Mathematica 'AssignmentStore' Interface

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

mathematicaSend :: EXPRESSION -> MathematicaIO ()

mathematicaSend e = do

prettyInfo3 $ text "Sending expression" <+> braces (mmPretty e)

sm <- getSymbolicMode

liftML $ sendEvalPacket (sendExpression sm e) >> skipAnswer >> return ()

mathematicaEval :: EXPRESSION -> MathematicaIO EXPRESSION

mathematicaEval e = do

prettyInfo3 $ text "Sending expression for evaluation"

<+> braces (mmPretty e)

sm <- getSymbolicMode

res <- liftML $ sendEvalPacket (sendExpression sm e) >> waitForAnswer

>> receiveExpression

prettyInfo3 $ text "Received expression"

<+> braces (mmPretty res)

return res

mathematicaAssign :: String -> AssDefinition -> MathematicaIO EXPRESSION

mathematicaAssign s def = do

prettyInfo $ text "Assigning" <+> mmPretty s <+> mmPretty def

mathematicaEval $ mtDef s def

mathematicaAssigns :: [(String, AssDefinition)] -> MathematicaIO ()

mathematicaAssigns l = do

prettyInfo $ text "Assigning list" <+> mmPretty l

let l' = map (uncurry mtDef) l

mathematicaSend $ mtCompound l'

mathematicaLookup :: String -> MathematicaIO EXPRESSION

mathematicaLookup s = mathematicaEval $ mkOp s []

mathematicaCheck :: EXPRESSION -> MathematicaIO Bool

mathematicaCheck e = do

prettyInfo $ text "Checking expression" <+> mmPretty e

eB <- genCheck mathematicaEval e

case eB of

Right b -> return b

Left s ->

throwError $ ASError CASError $

concat [ "mathematicaCheck:", show e, "\n", s ]

mathematicaDirect :: String -> MathState -> IO String

mathematicaDirect s st =

liftM snd $ withMathematica st $ liftML

$ sendTextResultPacket s >> waitForAnswer >> receiveString

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

-- * The Mathematica system via MathLink

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

loadMathematicaModule :: FilePath -> MathematicaIO ()

loadMathematicaModule fp =

liftML $ sendTextPacket ("<<" ++ show fp) >> skipAnswer >> return ()

withMathematica :: MathState -> MathematicaIO a -> IO (MathState, a)

withMathematica st mprog = do

let stE = runErrorT mprog -- (:: StateT MathState ML (Either ASError a))

mlE = runStateT stE st -- (:: ML (Either ASError a, MathState))

(eRes, st') <- withLink (getMLState st) (getMLLogFile st) mlE

case eRes of

Left err -> throwASError err

Right res -> return (st', res)

-- | Init the Mathematica communication

mathematicaInit :: AssignmentDepGraph ()

-> Int -- ^ Verbosity level

-> Maybe FilePath -- ^ Log MathLink messages into this file

-> Maybe String -- ^ Connection name

-- (launches a new kernel if not specified)

-> IO MathState

mathematicaInit adg v mFp mN = do

eMLSt <- openLink v mN

case eMLSt of

Left i ->

error $ "mathematicaInit: MathLink connection failure " ++ show i

Right mlSt ->

return $ initASState (mlSt, mFp) mathematicaOpInfoMap adg v

mathematicaExit :: MathState -> IO ()

mathematicaExit = closeLink . getMLState

runWithMathematica :: AssignmentDepGraph () -> Int -- ^ Verbosity level

-> Maybe FilePath -- ^ Log MathLink messages into this file

-> Maybe String -- ^ Connection name

-- (launches a new kernel if not specified)

-> [String] -- ^ mathematica modules to load

-> MathematicaIO a -- ^ the mathematica program to run

-> IO (MathState, a)

runWithMathematica adg i mFp mN mods p = do

mst <- mathematicaInit adg i mFp mN

withMathematica mst $ mapM_ loadMathematicaModule mods >> p