module CSPM.Evaluator.Expr (
Evaluatable, eval,
) where
import qualified Data.Foldable as F
import Data.List (nub)
import qualified Data.Map as M
import Data.Maybe
import Data.Sequence ((<|))
import qualified Data.Sequence as Sq
import CSPM.DataStructures.Literals
import CSPM.DataStructures.Names
import CSPM.DataStructures.Syntax
import CSPM.Evaluator.BuiltInFunctions
import CSPM.Evaluator.DeclBind
import CSPM.Evaluator.Dot
import CSPM.Evaluator.Exceptions
import CSPM.Evaluator.Monad
import CSPM.Evaluator.PatBind
import CSPM.Evaluator.Values
import qualified CSPM.Evaluator.ValueSet as S
import Util.Annotated
import Util.Exception
class Evaluatable a where
eval :: a -> EvaluationMonad Value
instance Evaluatable a => Evaluatable (Annotated b a) where
eval (An loc _ a) = setCurrentExpressionLocation loc (eval a)
instance Evaluatable (Exp Name) where
eval (App func args) = do
vs <- mapM eval args
VFunction _ f <- eval func
f vs
eval (BooleanBinaryOp op e1 e2) = do
v1 <- eval e1
v2 <- eval e2
case op of
And ->
let
VBool b1 = v1
VBool b2 = v2
in return $ VBool (b1 && b2)
Or ->
let
VBool b1 = v1
VBool b2 = v2
in return $ VBool (b1 || b2)
Equals -> return $ VBool (compareValues v1 v2 == Just EQ)
NotEquals -> return $ VBool (compareValues v1 v2 /= Just EQ)
LessThan -> return $ VBool (compareValues v1 v2 == Just LT)
GreaterThan -> return $ VBool (compareValues v1 v2 == Just GT)
LessThanEq -> return $ VBool (compareValues v1 v2 `elem` [Just LT, Just EQ])
GreaterThanEq -> return $ VBool (compareValues v1 v2 `elem` [Just GT, Just EQ])
eval (BooleanUnaryOp op e) = do
VBool b <- eval e
case op of
Not -> return $ VBool (not b)
eval (Concat e1 e2) = do
VList vs1 <- eval e1
v2 <- eval e2
let VList vs2 = v2
return $ VList (vs1++vs2)
eval (DotApp e1 e2) = do
v1 <- eval e1
v2 <- eval e2
combineDots v1 v2
eval (If e1 e2 e3) = do
VBool b <- eval e1
if b then eval e2 else eval e3
eval (Lambda ps e) = do
st <- getState
psid <- getParentScopeIdentifier
let fid = FLambda (Lambda ps e) psid
return $ VFunction fid $ \ vs -> return $ runEvaluator st $ do
let (matches, binds) = bindAll ps vs
if matches then do
p <- getParentScopeIdentifier
updateParentScopeIdentifier (annonymousScopeId vs psid) $
addScopeAndBind binds (eval e)
else do
loc <- getCurrentExpressionLocation
throwError $ patternMatchesFailureMessage loc ps vs
eval (Let decls e) = do
nvs <- bindDecls decls
addScopeAndBindM nvs (eval e)
eval (Lit lit) = return $
case lit of
Int i -> VInt i
Bool b -> VBool b
Char c -> VChar c
String s -> VList (map VChar s)
eval (List es) = mapM eval es >>= return . VList
eval (ListComp es stmts) = do
xs <- evalStmts (\(VList xs) -> xs) stmts (mapM eval es)
return $ VList xs
eval (ListEnumFrom e) = do
VInt lb <- eval e
return $ VList (map VInt [lb..])
eval (ListEnumFromTo e1 e2) = do
VInt lb <- eval e1
VInt ub <- eval e2
return $ VList (map VInt [lb..ub])
eval (ListEnumFromComp e1 stmts) = do
ss <- evalStmts (\ (VList xs) -> xs) stmts $ do
VInt lb <- eval e1
return $ map VInt [lb..]
return $ VList ss
eval (ListEnumFromToComp e1 e2 stmts) = do
ss <- evalStmts (\ (VList xs) -> xs) stmts $ do
VInt lb <- eval e1
VInt ub <- eval e2
return $ map VInt [lb..ub]
return $ VList ss
eval (ListLength e) = do
VList xs <- eval e
return $ VInt (length xs)
eval (Map kvs) = do
xs <- mapM (\ (k, v) -> do
k <- eval k
v <- eval v
return (k, v)) kvs
return $ VMap $ M.fromList xs
eval (MathsBinaryOp op e1 e2) = do
VInt i1 <- eval e1
VInt i2 <- eval e2
case op of
Divide -> do
scopeId <- getParentScopeIdentifier
loc <- getCurrentExpressionLocation
return $ VInt $
case i2 of
0 -> throwError $ divideByZeroMessage loc scopeId
_ -> i1 `div` i2
Minus -> return $ VInt (i1 i2)
Mod -> return $ VInt (i1 `mod` i2)
Plus -> return $ VInt (i1 + i2)
Times -> return $ VInt (i1 * i2)
eval (MathsUnaryOp op e) = do
VInt i <- eval e
case op of
Negate -> return $ VInt (i)
eval (Paren e) = eval e
eval (Set es) = mapM eval es >>= return . VSet . S.fromList
eval (SetComp es stmts) = do
xs <- evalStmts (\(VSet s) -> S.toList s) stmts (mapM eval es)
return $ VSet (S.fromList xs)
eval (SetEnum es) = do
evs <- mapM eval es
ss <- mapM productionsSet evs
return $ VSet (S.unions ss)
eval (SetEnumComp es stmts) = do
ss <- evalStmts (\(VSet s) -> S.toList s) stmts
(mapM (\e -> eval e >>= productionsSet) es)
return $ VSet (S.unions ss)
eval (SetEnumFrom e) = do
VInt lb <- eval e
return $ VSet (S.IntSetFrom lb)
eval (SetEnumFromTo e1 e2) = do
VInt lb <- eval e1
VInt ub <- eval e2
return $ VSet (S.fromList (map VInt [lb..ub]))
eval (SetEnumFromComp e1 stmts) = do
ss <- evalStmts (\ (VSet s) -> S.toList s) stmts $ do
VInt lb <- eval e1
return [S.IntSetFrom lb]
return $ VSet $ S.unions ss
eval (SetEnumFromToComp e1 e2 stmts) = do
ss <- evalStmts (\ (VSet s) -> S.toList s) stmts $ do
VInt lb <- eval e1
VInt ub <- eval e2
return [S.fromList (map VInt [lb..ub])]
return $ VSet $ S.unions ss
eval (Tuple es) = mapM eval es >>= return . tupleFromList
eval (Var n) | isNameDataConstructor n = do
(dc, _, _) <- dataTypeInfo n
return dc
eval (Var n) = lookupVar n
eval (Prefix e1 fs e2) =
let
evalInputField :: Value -> [Field Name] -> TCPat -> S.ValueSet ->
(Value -> [Field Name] -> EvaluationMonad UProc) ->
EvaluationMonad (Sq.Seq UProc)
evalInputField evBase fs p s evalRest = do
mps <- mapM (\v -> do
let (matches, binds) = bind p v
if matches then do
ev' <- combineDots evBase v
pid <- getParentScopeIdentifier
p <- updateParentScopeIdentifier (annonymousScopeId [v] pid) $
addScopeAndBind binds $ evalRest ev' fs
return $ Just p
else return Nothing) (S.toList s)
return $ Sq.fromList $ catMaybes mps
evalInputField2 :: Value -> [Field Name] -> Pat Name ->
(Value -> [Field Name] -> EvaluationMonad UProc) ->
(Sq.Seq UProc -> UProc) -> EvaluationMonad UProc
evalInputField2 evBase fs p evalRest procConstructor =
let
extensionsOperator ::
[Pat Name] -> Value -> EvaluationMonad [Value]
extensionsOperator ps | fs /= [] = oneFieldExtensions
extensionsOperator [p] = extensions
extensionsOperator (p1:p2:ps) = oneFieldExtensions
patToFields :: Pat Name -> [Pat Name]
patToFields (PCompDot ps _) = map unAnnotate ps
patToFields (PDoublePattern p1 p2) = patToFields (unAnnotate p1)
patToFields p = [p]
evExtensions :: Value -> [Pat Name] -> [(Name, Value)] ->
EvaluationMonad (Sq.Seq UProc)
evExtensions evBase [] bs = do
pid <- getParentScopeIdentifier
p <- updateParentScopeIdentifier (annonymousScopeId (map snd bs) pid) $
addScopeAndBind bs $ evalRest evBase fs
return $ Sq.singleton p
evExtensions evBase (PVar n:ps) bs | isNameDataConstructor n = do
(dc, _, _) <- dataTypeInfo n
evBase' <- combineDots evBase dc
evExtensions evBase' ps bs
evExtensions evBase (p:ps) bs = do
vs <- extensionsOperator (p:ps) evBase
mps <- mapM (\v -> do
let (matches, bs') = bind p v
if matches then do
evBase' <- combineDots evBase v
proc <- evExtensions evBase' ps (bs++bs')
return $ Just proc
else return Nothing) vs
return $ F.msum $ catMaybes mps
in do
ps <- evExtensions evBase (patToFields p) []
return $ procConstructor ps
evalNonDetFields :: Value -> [Field Name] -> EvaluationMonad UProc
evalNonDetFields evBase (NonDetInput p (Just e):fs) = do
VSet s <- eval e
ps <- evalInputField evBase fs p s evalNonDetFields
if Sq.null ps then
throwError' $ replicatedInternalChoiceOverEmptySetMessage (unAnnotate e)
else return $ POp PInternalChoice ps
evalNonDetFields evBase (NonDetInput p Nothing:fs) = do
POp _ ps <- evalInputField2 evBase fs (unAnnotate p) evalNonDetFields (POp PInternalChoice)
if Sq.null ps then
throwError' $ replicatedInternalChoiceOverEmptySetMessage' (unAnnotate p)
else return $ POp PInternalChoice ps
evalNonDetFields evBase fs = evalFields evBase fs
evalFields :: Value -> [Field Name] -> EvaluationMonad UProc
evalFields ev [] = do
p <- evalProc e2
return $ PUnaryOp (PPrefix (valueEventToEvent ev)) p
evalFields evBase (Output e:fs) = do
v <- eval e
ev' <- combineDots evBase v
evalFields ev' fs
evalFields evBase (Input p (Just e):fs) = do
VSet s <- eval e
ps <- evalInputField evBase fs p s evalFields
return $ POp PExternalChoice ps
evalFields evBase (Input p Nothing:fs) =
evalInputField2 evBase fs (unAnnotate p) evalFields (POp PExternalChoice)
evalFields evBase (NonDetInput _ _:fs) =
panic "Evaluation of $ after ! or ? is not supported."
in do
ev@(VDot (VChannel n:vfs)) <- eval e1
p <- evalNonDetFields ev (map unAnnotate fs)
return $ VProc p
eval (TimedPrefix n e) = do
p <- evalProc e
Just (eventFunc, tockName) <- gets timedSection
parentScope <- getParentScopeIdentifier
let addTocker (POp PExternalChoice ps) =
POp PExternalChoice (fmap addTocker ps)
addTocker (PUnaryOp (PPrefix ev) p) =
PUnaryOp (PPrefix ev) (makeTocker tockName (eventFunc ev) p)
p' = addTocker p
tocker = PUnaryOp (PPrefix (tock tockName)) procCall
mainProc = POp PExternalChoice (tocker <| p' <| Sq.empty)
procCall = PProcCall (procName $ scopeId n [] parentScope) mainProc
return $ VProc procCall
eval (AlphaParallel e1 e2 e3 e4) = do
p1 <- evalProc e1
p2 <- evalProc e4
VSet a1 <- timedCSPSyncSet $ eval e2
VSet a2 <- timedCSPSyncSet $ eval e3
return $ VProc $ POp (PAlphaParallel
(S.valueSetToEventSet a1 <| S.valueSetToEventSet a2 <| Sq.empty))
(p1 <| p2 <| Sq.empty)
eval (Exception e1 e2 e3) = do
p1 <- evalProc e1
VSet a <- eval e2
p2 <- evalProc e3
return $ VProc $ PBinaryOp (PException (S.valueSetToEventSet a)) p1 p2
eval (ExternalChoice e1 e2) = do
p1 <- evalProc e1
p2 <- evalProc e2
let ps = (p1 <| p2 <| Sq.empty)
maybeTimedCSP
(return $ VProc $ POp PExternalChoice ps)
(\ tn _ -> return $ VProc $
POp (PSynchronisingExternalChoice (tockSet tn)) ps)
eval (GenParallel e1 e2 e3) = do
ps <- evalProcs [e1, e3]
VSet a <- timedCSPSyncSet $ eval e2
return $ VProc $ POp (PGenParallel (S.valueSetToEventSet a)) ps
eval (GuardedExp guard proc) = do
VBool b <- eval guard
if b then eval proc
else maybeTimedCSP
(lookupVar (builtInName "STOP"))
(\ _ _ -> do
VFunction _ tstop <- lookupVar (builtInName "TSTOP")
tstop [])
eval (Hiding e1 e2) = do
p <- evalProc e1
VSet s <- eval e2
if S.empty s then return $ VProc p
else return $ VProc $ PUnaryOp (PHide (S.valueSetToEventSet s)) p
eval (InternalChoice e1 e2) = do
ps <- evalProcs [e1, e2]
return $ VProc $ POp PInternalChoice ps
eval (Interrupt e1 e2) = do
p1 <- evalProc e1
p2 <- evalProc e2
maybeTimedCSP
(return $ VProc $ PBinaryOp PInterrupt p1 p2)
(\ tn _ -> return $ VProc $
PBinaryOp (PSynchronisingInterrupt (tockSet tn)) p1 p2)
eval (Interleave e1 e2) = do
ps <- evalProcs [e1, e2]
maybeTimedCSP
(return $ VProc $ POp PInterleave ps)
(\ tn _ -> return $ VProc $ POp (PGenParallel (tockSet tn)) ps)
eval (LinkParallel e1 ties stmts e2) = do
p1 <- evalProc e1
p2 <- evalProc e2
ts <- evalTies stmts ties
return $ VProc $
PBinaryOp (PLinkParallel (removeDuplicateTies ts)) p1 p2
eval (Rename e1 ties stmts) = do
p1 <- evalProc e1
ts <- evalTies stmts ties
return $ VProc $ if Sq.null ts then p1 else
PUnaryOp (PRename (removeDuplicateTies ts)) p1
eval (SequentialComp e1 e2) = do
p1 <- evalProc e1
p2 <- evalProc e2
return $ VProc $ PBinaryOp PSequentialComp p1 p2
eval (SlidingChoice e1 e2) = do
p1 <- evalProc e1
p2 <- evalProc e2
return $ VProc $ PBinaryOp PSlidingChoice p1 p2
eval (SynchronisingExternalChoice e1 e2 e3) = do
ps <- evalProcs [e1, e3]
VSet a <- timedCSPSyncSet $ eval e2
return $ VProc $ POp
(PSynchronisingExternalChoice (S.valueSetToEventSet a)) ps
eval (SynchronisingInterrupt e1 e2 e3) = do
p1 <- evalProc e1
VSet a <- timedCSPSyncSet $ eval e2
p2 <- evalProc e3
return $ VProc $
PBinaryOp (PSynchronisingInterrupt (S.valueSetToEventSet a)) p1 p2
eval (ReplicatedAlphaParallel stmts e1 e2) = do
aps <- evalStmts' (\(VSet s) -> S.toSeq s) stmts $ do
VSet s <- timedCSPSyncSet $ eval e1
p <- evalProc e2
return (S.valueSetToEventSet s, p)
let (as, ps) = unzipSq aps
maybeTSTOP ps $ return $ VProc $ POp (PAlphaParallel as) ps
eval (ReplicatedExternalChoice stmts e) = do
ps <- evalStmts' (\(VSet s) -> S.toSeq s) stmts (evalProc e)
maybeTimedCSP
(return $ VProc $ POp PExternalChoice ps)
(\ tn _ -> maybeTSTOP ps $ return $ VProc $
POp (PSynchronisingExternalChoice (tockSet tn)) ps)
eval (ReplicatedInterleave stmts e) = do
ps <- evalStmts' (\(VSet s) -> S.toSeq s) stmts (evalProc e)
maybeTimedCSP
(return $ VProc $ POp PInterleave ps)
(\ tn _ -> maybeTSTOP ps $
return $ VProc $ POp (PGenParallel (tockSet tn)) ps)
eval (e'@(ReplicatedInternalChoice stmts e)) = do
ps <- evalStmts' (\(VSet s) -> S.toSeq s) stmts (evalProc e)
if Sq.null ps then
throwError' $ replicatedInternalChoiceOverEmptySetMessage e'
else return $ VProc $ POp PInternalChoice ps
eval (e'@(ReplicatedLinkParallel ties tiesStmts stmts e)) = do
tsps <- evalStmts' (\(VList vs) -> Sq.fromList vs) stmts $ do
ts <- evalTies tiesStmts ties
p <- evalProc e
return (ts, p)
if Sq.null tsps then
throwError' $ replicatedLinkParallelOverEmptySeqMessage e'
else do
let
(tsps' Sq.:> (_, lastProc)) = Sq.viewr tsps
mkLinkPar (ts, p1) p2 =
PBinaryOp (PLinkParallel (removeDuplicateTies ts)) p1 p2
return $ VProc $ F.foldr mkLinkPar lastProc tsps'
eval (ReplicatedParallel e1 stmts e2) = do
VSet s <- timedCSPSyncSet $ eval e1
ps <- evalStmts' (\(VSet s) -> S.toSeq s) stmts (evalProc e2)
maybeTSTOP ps $
return $ VProc $ POp (PGenParallel (S.valueSetToEventSet s)) ps
eval (ReplicatedSequentialComp stmts e) = do
ps <- evalStmts' (\(VList vs) -> Sq.fromList vs) stmts (evalProc e)
if Sq.null ps then
maybeTimedCSP
(lookupVar (builtInName "SKIP"))
(\ _ _ -> do
VFunction _ tskip <- lookupVar (builtInName "TSKIP")
tskip [])
else return $ VProc $ F.foldr1 (PBinaryOp PSequentialComp) ps
eval (ReplicatedSynchronisingExternalChoice e1 stmts e2) = do
VSet a <- timedCSPSyncSet $ eval e1
ps <- evalStmts' (\(VSet s) -> S.toSeq s) stmts (evalProc e2)
maybeTSTOP ps $ return $ VProc $ POp
(PSynchronisingExternalChoice (S.valueSetToEventSet a)) ps
eval e = panic ("No clause to eval "++show e)
evalProcs :: Evaluatable a => [a] -> EvaluationMonad (Sq.Seq UProc)
evalProcs as = mapM evalProc as >>= return . Sq.fromList
evalProc :: Evaluatable a => a -> EvaluationMonad UProc
evalProc a = eval a >>= \v -> case v of
VProc x -> return x
_ -> panic "Type checker error"
removeDuplicateTies :: Sq.Seq (Event, Event) -> Sq.Seq (Event, Event)
removeDuplicateTies = Sq.fromList . nub . F.toList . Sq.unstableSort
evalTies :: [TCStmt] -> [(TCExp, TCExp)] -> EvaluationMonad (Sq.Seq (Event, Event))
evalTies stmts ties = do
tss <- evalStmts (\(VSet s) -> S.toList s) stmts (mapM evalTie ties)
return $ Sq.fromList (concat tss)
where
extendTie :: (Value, Value) -> Value -> EvaluationMonad (Event, Event)
extendTie (evOld, evNew) ex = do
ev1 <- combineDots evOld ex
ev2 <- combineDots evNew ex
return (valueEventToEvent ev1, valueEventToEvent ev2)
evalTie (eOld, eNew) = do
evOld <- eval eOld
evNew <- eval eNew
exsOld <- extensions evOld
mapM (\ex -> extendTie (evOld, evNew) ex) exsOld
evalStmts :: (Value -> [Value]) -> [TCStmt] -> EvaluationMonad [a] ->
EvaluationMonad [a]
evalStmts extract anStmts prog =
let
evStmts [] = prog
evStmts (Qualifier e:stmts) = do
VBool b <- eval e
if b then evStmts stmts else return []
evStmts (Generator p e:stmts) = do
v <- eval e
vss <- mapM (\v -> do
let (matches, binds) = bind p v
if matches then do
pid <- getParentScopeIdentifier
updateParentScopeIdentifier (annonymousScopeId [v] pid) $
addScopeAndBind binds (evStmts stmts)
else return []) (extract v)
return $ concat vss
in
evStmts (map unAnnotate anStmts)
evalStmts' :: (Value -> Sq.Seq Value) -> [TCStmt] -> EvaluationMonad a ->
EvaluationMonad (Sq.Seq a)
evalStmts' extract anStmts prog =
let
evStmts [] = prog >>= return . Sq.singleton
evStmts (Qualifier e:stmts) = do
VBool b <- eval e
if b then evStmts stmts else return Sq.empty
evStmts (Generator p e:stmts) = do
v <- eval e
F.foldlM (\ s v -> do
let (matches, binds) = bind p v
if matches then do
pid <- getParentScopeIdentifier
s' <- updateParentScopeIdentifier (annonymousScopeId [v] pid) $
addScopeAndBind binds (evStmts stmts)
return $ s Sq.>< s'
else return s) Sq.empty (extract v)
in evStmts (map unAnnotate anStmts)
unzipSq :: Sq.Seq (a,b) -> (Sq.Seq a, Sq.Seq b)
unzipSq sqs = F.foldr
(\ (a,b) (as, bs) -> (a <| as, b <| bs) ) (Sq.empty, Sq.empty) sqs
timedCSPSyncSet :: EvaluationMonad Value -> EvaluationMonad Value
timedCSPSyncSet prog = do
VSet a <- prog
maybeTimedCSP
(return $ VSet a)
(\ tn _ -> return $ VSet (S.union (S.fromList [tockValue tn]) a))
tSTOP :: EvaluationMonad Value
tSTOP = do
VFunction _ tstop <- lookupVar (builtInName "TSTOP")
tstop []
maybeTSTOP :: Sq.Seq a -> EvaluationMonad Value -> EvaluationMonad Value
maybeTSTOP sq p1 =
maybeTimedCSP p1 (\ _ _ -> if Sq.null sq then tSTOP else p1)
tock :: Name -> Event
tock tn = UserEvent (tockValue tn)
tockValue :: Name -> Value
tockValue tn = VDot [VChannel tn]
tockSet :: Name -> EventSet
tockSet tn = Sq.singleton (tock tn)
makeTocker :: Name -> Int -> UProc -> UProc
makeTocker tn 0 p = p
makeTocker tn tocks p =
PUnaryOp (PPrefix (tock tn)) (makeTocker tn (tocks1) p)