{-# 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