{-# LANGUAGE FunctionalDependencies, FlexibleInstances, FlexibleContexts
, MultiParamTypeClasses, TypeSynonymInstances, ExistentialQuantification #-}
{- |
Module : ./CSL/Interpreter.hs
Description : Interpreter for CPL programs
Copyright : (c) Ewaryst Schulz, DFKI Bremen 2010
License : GPLv2 or higher, see LICENSE.txt
Maintainer : Ewaryst.Schulz@dfki.de
Stability : experimental
Portability : non-portable (various glasgow extensions)
Defines an interface for Calculators used to evaluate CPL programs
-}
module CSL.Interpreter
( AssignmentStore (..)
, SMem (..)
, isDefined
, evaluate
, evaluateList
, loadAS
, BMap (..)
, CSL.Interpreter.empty
, initWithOpMap
, genKey
, lookupOrInsert
, revlookup
, rolookup
, translateArgVars
, translateExpr
, translateExprWithVars
, revtranslateExpr
, revtranslateExprWithVars
, convergenceTerm
, stepwise
, stepwiseSafe
, interactiveStepper
, readEvalPrintLoop
, EvalAtom (..)
, prettyEvalAtom
, asErrorMsg
, throwASError
, ASState (..)
, initASState
, withLogFile
, ASError (..)
, ErrorSource (..)
, StepDebugger (..)
, SymbolicEvaluator (..)
, MessagePrinter (..)
, verbMsgASSt
, verbMsgASStLn
, prettyInfo
, prettyInfo3
)
where
import Control.Monad
import Control.Monad.State
import Control.Monad.Error (Error (..), MonadError (..))
import Data.Maybe
import qualified Data.Set as Set
import qualified Data.Map as Map
import qualified Data.IntMap as IMap
import Data.List (mapAccumL)
import Prelude hiding (lookup)
import System.IO
import Common.Id
import Common.Doc
import Common.DocUtils
import Common.Utils
import CSL.AS_BASIC_CSL
import CSL.ASUtils
import CSL.DependencyGraph
-- import Common.MonadTrans ()
{- ----------------------------------------------------------------------
Evaluator
---------------------------------------------------------------------- -}
-- ** Some utility classes for abstraction of concrete realizations
-- | Abstraction from lists, sets, etc. for some simple operations
class SimpleMember a b | a -> b where
member :: b -> a -> Bool
count :: a -> Int
toList :: a -> [b]
-- ** Abstraction wrapper for utility classes
data SMem b = forall a . SimpleMember a b => SMem a
-- ** Instances for abstraction wrapper
instance SimpleMember (SMem b) b where
member x (SMem a) = member x a
count (SMem a) = count a
toList (SMem a) = toList a
data ASState a =
ASState
{ getBMap :: BMap
, getConnectInfo :: a
, depGraph :: AssignmentDepGraph ()
, debugMode :: Bool
, symbolicMode :: Bool
, verbosity :: Int
, vericondOut :: Maybe Handle
, logOut :: Handle
, printcount :: Int
}
initASState :: a -> OpInfoMap -> AssignmentDepGraph () -> Int -> ASState a
initASState ci oim adg v =
ASState { getBMap = initWithOpMap oim
, getConnectInfo = ci
, depGraph = adg
, debugMode = False
, symbolicMode = False
, verbosity = v
, vericondOut = Nothing
, logOut = stdout
, printcount = 0
}
-- | Prints a message dependent on the verbosity level
verbMsgASSt :: (MonadState (ASState a) as, MonadIO as) => Int -> String -> as ()
verbMsgASSt lvl msg = do
hdl <- gets logOut
v <- gets verbosity
liftIO $ verbMsg hdl v lvl msg
-- | Prints a message dependent on the verbosity level
verbMsgASStLn :: (MonadState (ASState a) as, MonadIO as) =>
Int -> String -> as ()
verbMsgASStLn lvl msg = do
hdl <- gets logOut
v <- gets verbosity
liftIO $ verbMsgLn hdl v lvl msg
prettyInfo3 :: (MonadState (ASState a) as, MonadIO as) => Doc -> as ()
prettyInfo3 = prettyInfoN 3
prettyInfo :: (MonadState (ASState a) as, MonadIO as) => Doc -> as ()
prettyInfo = prettyInfoN 2
prettyInfoN :: (MonadState (ASState a) as, MonadIO as) => Int -> Doc -> as ()
prettyInfoN n d = do
let mf ass = ass { printcount = printcount ass + 1 }
modify mf
gets printcount >>= verbMsgASSt n . show
verbMsgASSt n ": "
verbMsgASStLn n (show d)
withLogFile :: (MonadState (ASState a) as, MonadIO as) =>
FilePath -> as b -> as b
withLogFile fp prog = do
oldHdl <- gets logOut
let mf hdl ass = ass { logOut = hdl }
newHdl <- liftIO $ openFile fp WriteMode
modify $ mf newHdl
res <- prog
modify $ mf oldHdl
liftIO $ hClose newHdl
return res
instance Functor ASState where
fmap f s = s { getConnectInfo = f $ getConnectInfo s }
-- ** AssignmentStore
{- | Calculation interface, bundles the evaluation engine and the
assignment store -}
class (Monad m) => AssignmentStore m where
assign :: ConstantName -> AssDefinition -> m EXPRESSION
assigns :: [(ConstantName, AssDefinition)] -> m ()
assigns = mapM_ $ uncurry assign
lookup :: ConstantName -> m (Maybe EXPRESSION)
names :: m (SMem ConstantName)
eval :: EXPRESSION -> m EXPRESSION
evalRaw :: String -> m String
check :: EXPRESSION -> m Bool
values :: m [(ConstantName, EXPRESSION)]
values = let f x = do
v <- lookup x
return (x, fromJust v)
in names >>= mapM f . toList
getUndefinedConstants :: EXPRESSION -> m (Set.Set ConstantName)
getUndefinedConstants =
error "AssignmentStore: Unimplemented getUndefinedConstants"
genNewKey :: m Int
getDepGraph :: m (AssignmentDepGraph ())
updateConstant :: ConstantName -> AssDefinition -> m ()
instance AssignmentStore m => AssignmentStore (StateT s m) where
assign s = lift . assign s
assigns = lift . assigns
lookup = lift . lookup
names = lift names
eval = lift . eval
evalRaw = lift . evalRaw
check = lift . check
values = lift values
getUndefinedConstants = lift . getUndefinedConstants
genNewKey = lift genNewKey
getDepGraph = lift getDepGraph
updateConstant c = lift . updateConstant c
-- ** AssignmentStore Extensions
class AssignmentStore m => StepDebugger m where
setDebugMode :: Bool -> m ()
getDebugMode :: m Bool
class AssignmentStore m => SymbolicEvaluator m where
setSymbolicMode :: Bool -> m ()
getSymbolicMode :: m Bool
class AssignmentStore m => MessagePrinter m where
printMessage :: String -> m ()
-- ** Error handling
data ErrorSource = CASError | UserError | InterfaceError deriving Show
data ASError = ASError ErrorSource String deriving Show
asErrorMsg :: ASError -> String
asErrorMsg (ASError _ s) = s
throwASError :: ASError -> a
throwASError = error . asErrorMsg
instance Error ASError where
noMsg = ASError UserError ""
strMsg = ASError UserError
instance Pretty ErrorSource where
pretty es = case es of
CASError -> text "CAS error"
UserError -> text "User error"
InterfaceError -> text "Interface error"
instance Pretty ASError where
pretty (ASError es s) = pretty es <> text ":" <+> text s
-- ** Evaluation, Debugging, Stepping
{- | If the expression list is a variable list the list of the variable names
is returned. -}
toArgList :: [EXPRESSION] -> [String]
toArgList [] = []
toArgList (Var tok : l) = tokStr tok : toArgList l
toArgList (x : _) = error $ "toArgList: unsupported as argument " ++ show (pretty x)
isDefined :: AssignmentStore m => ConstantName -> m Bool
isDefined s = liftM (member s) names
evaluate :: AssignmentStore m => CMD -> m ()
evaluate (Ass (OpDecl n [] l _) e) = do
assign n $ mkDefinition (map varDeclName l) e
return ()
evaluate (Cond l) = do
cl <- filterM (check . fst) l
if null cl
then error "evaluate: non-exhaustive conditional"
else evaluateList $ snd $ head cl
evaluate (Repeat e l) =
let f = do
-- first run of the repeat loop
evaluateList l
b <- check e
-- repeat f until condition holds
unless b f
in f
evaluate (Sequence l) = evaluateList l
evaluate (Cmd c _) = error $ "evaluate: unsupported command " ++ c
evaluate a@(Ass _ _) = error $ "evaluate: unsupported assignment " ++ show a
evaluateList :: AssignmentStore m => [CMD] -> m ()
evaluateList l = forM_ l evaluate
data EvalAtom = AssAtom ConstantName AssDefinition
| CaseAtom EXPRESSION
| RepeatAtom EXPRESSION (Map.Map EXPRESSION Int) EXPRESSION
deriving Show
prettyEvalAtom :: EvalAtom -> Doc
prettyEvalAtom (AssAtom c def) = pretty c <+> pretty def
prettyEvalAtom (RepeatAtom e _ _) = text "Repeat condition:" <+> pretty e
prettyEvalAtom (CaseAtom e) = text "Case condition:" <+> pretty e
instance Pretty EvalAtom where
pretty = prettyEvalAtom
readEvalPrintLoop :: (MonadIO m, AssignmentStore m) =>
Handle -- ^ Input handle
-> Handle -- ^ Output handle
-> String -- ^ Command prompt
-> (String -> Bool) -- ^ Exit command predicate
-> m String
readEvalPrintLoop inp outp cp exitWhen = do
s <- liftIO $ hPutStr outp cp >> hFlush outp >> hGetLine inp
if exitWhen s then return s
else evalRaw s >>= liftIO . hPutStrLn outp
>> readEvalPrintLoop inp outp cp exitWhen
{- | An atom evaluator for 'stepwise' which pauses at each atomic evaluation
position. -}
interactiveStepper :: (MonadIO m, AssignmentStore m) => m () -> EvalAtom
-> m Bool
interactiveStepper prog x = do
liftIO $ putStrLn $ "At step " ++ show (prettyEvalAtom x)
b <- evaluateAtom prog x
readEvalPrintLoop stdin stdout "next>" null
return b
-- | The most primitive atom evaluator as expected by 'stepwise'.
evaluateAtom :: AssignmentStore m => m () -> EvalAtom -> m Bool
evaluateAtom _ (AssAtom n def) = assign n def >> return True
evaluateAtom _ (CaseAtom e) = check e
evaluateAtom prog (RepeatAtom _ _ e') = prog >> check e'
{- | It is assumed that the given function respects the evaluation semantics,
i.e., that for the assignment atom an assignment takes place and for the
repeat atom the passed program is evaluated and afterwards the condition is
checked and for the case atom the condition is checked. See 'evaluateAtom'
for an example.
-}
stepwiseSafe :: (MonadError ASError m, MessagePrinter m) =>
(m () -> EvalAtom -> m Bool) -> CMD -> m (Maybe ASError)
stepwiseSafe f cmd = catchError (stepwise f cmd >> return Nothing) g
where g = return . Just
printStep :: MessagePrinter m => String -> EvalAtom -> m ()
printStep _ (AssAtom n def) = printMessage $ ("Evaluate Assignment: " ++)
$ show $ pretty n <+> pretty def
printStep _ (CaseAtom e) = printMessage $ ("Evaluate Case Step: " ++)
$ show $ pretty e
printStep s (RepeatAtom e _ _) = printMessage
$ (("Evaluate Repeat Step, " ++ s ++ ": ") ++)
$ show $ pretty e
stepwise :: MessagePrinter m => (m () -> EvalAtom -> m Bool) -> CMD
-> m ()
stepwise f (Ass (OpDecl n [] l _) e) = do
let def = mkDefinition (map varDeclName l) e
printStep "" $ AssAtom n def
f (return ()) $ AssAtom n def
return ()
stepwise _ (Cond []) = error "stepwise: non-exhaustive conditional"
stepwise f (Cond ((e, pl) : cl)) = do
printStep "" $ CaseAtom e
b <- f (return ()) $ CaseAtom e
stepwise f $ if b then Sequence pl else Cond cl
stepwise f (Repeat e l) = do
{- only in the first entry of a repeat loop we need to transform the
until expression, in all consecutive runs of the same loop we just
need to update the values of the temporarily introduced constants. -}
(m, e') <- translateConvergence e
let rAtom = RepeatAtom e m e'
printStep "entering loop" rAtom
let al = Map.toList m
reploop = do
-- mapM (uncurry convergenceTerm) al >>= assigns
mapM_ (uncurry convergenceTerm >=> f (return ()) . uncurry AssAtom) al
b <- f (stepwise f $ Sequence l) rAtom
unless b $ printStep "repeating loop" rAtom >> reploop
reploop
stepwise f (Sequence l) = mapM_ (stepwise f) l
stepwise _ (Cmd c l)
| c == "print" =
let p x x' = printMessage
$ show $ pretty x <+> text "evaluates to"
<+> pretty x'
in case l of
[] -> printMessage "Nothing to print"
[e] -> eval e >>= p e
_ -> mapM eval l >>= p l
| otherwise = error $ "stepwise: unsupported command " ++ c
stepwise _ a@(Ass _ _) = error $ "stepwise: unsupported assignment " ++ show a
{- | We check if the expression contains free constants
(undefined in the assignment graph) and in this case we replace the
definition of the constant by the undefined constant. -}
convergenceTerm :: AssignmentStore m => EXPRESSION -> Int
-> m (ConstantName, AssDefinition)
convergenceTerm conve i = do
s <- getUndefinedConstants conve
let e = if Set.null s then conve else mkPredefOp OP_undef []
return (internalConstant i, mkDefinition [] e)
translateConvergence :: AssignmentStore m =>
EXPRESSION -> m (Map.Map EXPRESSION Int, EXPRESSION)
translateConvergence = f Map.empty where
f m (Op (OpId OP_convergence) [] [x, e] rg) =
do
i <- genNewKey
let ilf _ _ v = v
(mI, m') = Map.insertLookupWithKey ilf e i m
i' = fromMaybe i mI
genC = Op (OpUser $ internalConstant i') [] [] rg
return (m', mkPredefOp OP_reldistLe [genC, e, x])
f m (Op oi epl el rg) =
liftM (\ (m', x) -> (m', Op oi epl x rg)) $ mapAccumLM f m el
-- ignoring lists, see TODO in AS_BASIC_CSL
f m e = return (m, e)
-- | Loads a dependency ordered assignment list into the store.
loadAS :: AssignmentStore m => [(ConstantName, AssDefinition)] -> m ()
loadAS = assigns . reverse
{- ----------------------------------------------------------------------
Term translator
---------------------------------------------------------------------- -}
{- | For use for constants in the CAS namespace.
We only need to make sure that x<Num> is not already used in the
default namespace of the CAS in question. We take for all CAS the
same prefix, namely "x".
-}
constPrefix :: String
constPrefix = "x"
{- | The variable prefix is used for auxiliary variables in the CAS namespace.
We use the prefix "v". The same remarks are valid as for 'constPrefix'.
-}
varPrefix :: String
varPrefix = "v"
{- | For use for auxiliary constants in the EnCL specification
namespace. A dollar prefix is suitable here because this prefix is not
accepted by the input processor for user defined constants.
-}
internalPrefix :: String
internalPrefix = "$"
internalConstant :: Int -> ConstantName
internalConstant i = SimpleConstant $ internalPrefix ++ show i
{- | A data structure for invertible maps, with automatic new key generation
and insertion at lookup -}
data BMap = BMap { mThere :: Map.Map ConstantName Int
, mBack :: IMap.IntMap ConstantName
, newkey :: Int
, opMap :: OpInfoMap
}
deriving Show
instance SimpleMember BMap ConstantName where
member k = Map.member k . mThere
count = Map.size . mThere
toList = Map.keys . mThere
genKey :: BMap -> (BMap, Int)
genKey bm = let i = newkey bm in (bm { newkey = i + 1 }, i)
-- ** Interface functions for BMap
empty :: BMap
empty = BMap
{ mThere = Map.empty
, mBack = IMap.empty
, newkey = 1
, opMap = operatorInfoMap
}
initWithOpMap :: OpInfoMap -> BMap
initWithOpMap m = CSL.Interpreter.empty { opMap = m }
{- | The only way to also insert a value is to use lookup. One should not
insert values explicitly. Note that you don't control the inserted value. -}
lookupOrInsert :: BMap
-> ConstantName
-> (BMap, String)
lookupOrInsert m c =
let f _ _ x = x
nv = newkey m
(mNv', nm) = Map.insertLookupWithKey f c nv $ mThere m
in case mNv' of
Just nv' -> (m, bmapIntToString m nv')
_ -> (m { mThere = nm
, mBack = IMap.insert nv c $ mBack m
, newkey = nv + 1 }
, bmapIntToString m nv)
-- | A read-only version of 'lookupOrInsert'
rolookup :: BMap
-> ConstantName
-> Maybe String
rolookup m c = fmap (bmapIntToString m) $ Map.lookup c $ mThere m
revlookup :: BMap -> String -> Maybe OPID
revlookup m k = case revlookupGen IMap.empty m k of
Left x -> x
_ -> Nothing
revlookupGen :: RevVarMap -> BMap -> String
-> Either (Maybe OPID) (Maybe EXPRESSION)
revlookupGen vm m k =
case bmapStringToInt m k of
Left i -> Left $ fmap OpUser $ IMap.lookup i $ mBack m
Right i -> Right $ fmap (Var . mkSimpleId) $ IMap.lookup i vm
{-
bmToList :: BMap -> [(ConstantName, String)]
bmToList m = let prf = constPrefix
f (x, y) = (x, prf ++ show y)
in map f $ Map.toList $ mThere m
-}
-- ** Internal functions for BMap
bmapIntToString :: BMap -> Int -> String
bmapIntToString _ i = constPrefix ++ show i
{- | Returns the 'Int' contained in the given constant. If this constant
represents a user-defined constant then we return the left value, if
it represents a variable then we return the right value -}
bmapStringToInt :: BMap -> String -> Either Int Int
bmapStringToInt _ s =
let prf = constPrefix
(prf', n) = splitAt (length prf) s
(prf'', n') = splitAt 1 s
out
| prf == prf' = Left $ read n
| prf'' == varPrefix = Right $ read n'
| otherwise = error $ concat [ "bmapStringToInt: invalid string"
, " for prefix ", prf, ":", s ]
in out
-- ** Translation functions for (generic) BMaps
type VarMap = Map.Map String Int
type RevVarMap = IMap.IntMap String
varList :: [String] -> [(String, Int)]
varList l = zip l [1 ..]
addToVarMap :: VarMap -> String -> VarMap
addToVarMap vm s = Map.insert s (Map.size vm + 1) vm
revVarList :: [String] -> [(Int, String)]
revVarList = zip [1 ..]
varName :: BMap -> Int -> String
varName _ i = varPrefix ++ show i
translateArgVars :: BMap -> [String] -> [String]
translateArgVars m = map f . varList where
f (_, i) = varName m i
translateExprWithVars :: [String] -> BMap -> EXPRESSION -> (BMap, EXPRESSION)
translateExprWithVars = translateExprGen . Map.fromList . varList
translateExpr :: BMap -> EXPRESSION -> (BMap, EXPRESSION)
translateExpr = translateExprGen Map.empty
-- TODO: check if we can simplify by not checking if a var is in a given scope..
{- | Translate EXPRESSION into a CAS compatible form. Variables are translated
as constants with a namespace disjoint from that of the usual constants. -}
translateExprGen :: VarMap -> BMap -> EXPRESSION -> (BMap, EXPRESSION)
translateExprGen vm m (Op (OpUser c) epl el rg) =
let (m', s) = lookupOrInsert m c
(m'', el') = mapAccumL (translateExprGen vm) m' el
in (m'', Op (OpUser $ SimpleConstant s) epl el' rg)
translateExprGen vm m (Op oi epl el rg) =
let vm' = case lookupBindInfo operatorInfoNameMap oi $ length el of
Just bi ->
foldl addToVarMap vm
$ toArgList $ map (el !!) $ bindingVarPos bi
_ -> vm
(m', el') = mapAccumL (translateExprGen vm') m el
in (m', Op oi epl el' rg)
translateExprGen vm m (List el rg) =
let (m', el') = mapAccumL (translateExprGen vm) m el
in (m', List el' rg)
translateExprGen vm m (Var tok) =
let err = error $ "translateExprGen: Variable not mapped: " ++ show tok
i = Map.findWithDefault err (tokStr tok) vm
in (m, Op (OpUser $ SimpleConstant $ varName m i) [] [] nullRange)
translateExprGen _ m e = (m, e)
-- | Retranslate CAS EXPRESSION back, we do not allow OPNAMEs as OpIds
revtranslateExprWithVars :: [String] -> BMap -> EXPRESSION -> EXPRESSION
revtranslateExprWithVars = revtranslateExprGen . IMap.fromList . revVarList
revtranslateExpr :: BMap -> EXPRESSION -> EXPRESSION
revtranslateExpr = revtranslateExprGen IMap.empty
revtranslateExprGen :: RevVarMap -> BMap -> EXPRESSION -> EXPRESSION
revtranslateExprGen rvm m (Op (OpUser c) epl el rg) =
case c of
SimpleConstant s ->
let el' = map (revtranslateExprGen rvm m) el
in case revlookupGen rvm m s of
Left (Just oi) -> Op oi epl el' rg
Right (Just v) -> v
_ -> error $ "revtranslateExpr: no mapping for " ++ s
_ -> error $ "revtranslateExpr: elim constants on CAS side encountered "
++ show c
revtranslateExprGen rvm m e = mapExpr (revtranslateExprGen rvm m) e
-- ** Pretty printing of BMap
printMapping :: Doc -> Doc -> Doc
printMapping x y = x <+> mapsto <+> y
printBMap :: BMap -> Doc
printBMap bm =
braces $ text "BMap" $+$ md
where
md = printMap braces vcat printMapping $ mThere bm
instance Pretty BMap where
pretty = printBMap