module CSPM.Evaluator.BuiltInFunctions (
injectBuiltInFunctions,
builtInName
) where
import Control.Monad
import qualified Data.Map as M
import qualified CSPM.Compiler.Set as CS
import CSPM.DataStructures.Names
import CSPM.Evaluator.Exceptions
import CSPM.Evaluator.Monad
import CSPM.Evaluator.Values
import qualified CSPM.Evaluator.ValueSet as S
import CSPM.Prelude
import Util.Exception
bMap = M.fromList [(stringName b, name b) | b <- builtins True]
builtInName s = M.findWithDefault (panic "builtin not found") s bMap
builtInFunctions :: [(Name, Value)]
builtInFunctions =
let
nameForString s = builtInName s
cspm_union [VSet s1, VSet s2] = S.union s1 s2
cspm_inter [VSet s1, VSet s2] = S.intersection s1 s2
cspm_diff [VSet s1, VSet s2] = S.difference s1 s2
cspm_Union [VSet s] = S.unions (map (\ (VSet s) -> s) (S.toList s))
cspm_Inter [VSet s] =
S.intersections (map (\ (VSet s) -> s) (S.toList s))
cspm_member [v, VSet s] = VBool $ S.member v s
cspm_card [VSet s] = VInt $ fromIntegral $ S.card s
cspm_empty [VSet s] = VBool $ S.empty s
cspm_set [VList xs] = S.fromList xs
cspm_Set [VSet s] = S.powerset s
cspm_Seq [VSet s] = S.allSequences s
cspm_seq [VSet s] = S.toList s
cspm_length [VList xs] = VInt $ length xs
cspm_null [VList xs] = VBool $ null xs
cspm_head [VList []] = throwError headEmptyListMessage
cspm_head [VList (x:xs)] = x
cspm_tail [VList []] = throwError tailEmptyListMessage
cspm_tail [VList (x:xs)] = xs
cspm_concat [VList xs] = concat (map (\(VList ys) -> ys) xs)
cspm_elem [v, VList vs] = VBool $ v `elem` vs
csp_chaos [VSet a] = VProc chaosCall
where
chaosCall = PProcCall n p
n = procId (nameForString "CHAOS") [[VSet a]]
evSet = S.valueSetToEventSet a
branches = [PPrefix ev chaosCall | ev <- CS.toList evSet]
stopProc = PProcCall (procId (nameForString "STOP") []) csp_stop
p = PInternalChoice (stopProc:branches)
cspm_extensions [v] = do
exs <- extensions v
return $ VSet $ S.fromList exs
cspm_productions [v] = do
exs <- productions v
return $ VSet $ S.fromList exs
set_funcs = [
("union", cspm_union), ("inter", cspm_inter),
("diff", cspm_diff), ("Union", cspm_Union),
("Inter", cspm_Inter), ("set", cspm_set),
("Set", cspm_Set), ("Seq", cspm_Seq)
]
seq_funcs = [
("seq", cspm_seq), ("tail", cspm_tail), ("concat", cspm_concat)
]
proc_operators = [
("chase", Chase),
("diamond", Diamond),
("explicate", Explicate),
("normal", Normalize),
("model_compress", ModelCompress),
("sbisim", StrongBisim),
("tau_loop_factor", TauLoopFactor),
("wbisim", WeakBisim)
]
other_funcs = [
("length", cspm_length), ("null", cspm_null),
("head", cspm_head), ("elem", cspm_elem),
("member", cspm_member), ("card", cspm_card),
("empty", cspm_empty), ("CHAOS", csp_chaos)
]
monadic_funcs = [
("productions", cspm_productions), ("extensions", cspm_extensions)
]
mkFunc (s, f) = (nameForString s, VFunction (\ vs -> return (f vs)))
mkMonadicFunc (s, f) = (nameForString s, VFunction f)
procs = [
("STOP", csp_stop),
("SKIP", PPrefix Tick (PProcCall csp_stop_id csp_stop))
]
csp_skip_id = procId (nameForString "SKIP") []
csp_stop_id = procId (nameForString "STOP") []
csp_stop = PExternalChoice []
mkProc (s, p) = (nameForString s, VProc p)
cspm_true = ("true", VBool True)
cspm_false = ("false", VBool False)
cspm_True = ("True", VBool True)
cspm_False = ("False", VBool False)
cspm_Bool = ("Bool", VSet (S.fromList [snd cspm_true, snd cspm_false]))
cspm_Int = ("Int", VSet S.Integers)
cspm_Proc = ("Proc", VSet S.Processes)
cspm_Events = ("Events", panic "Events not implemented")
constants = [
cspm_true, cspm_false, cspm_True, cspm_False,
cspm_Bool, cspm_Int, cspm_Proc, cspm_Events
]
mkConstant (s, v) = (nameForString s, v)
in
map mkFunc (
map (\ (n, f) -> (n, VSet . f)) set_funcs
++ map (\ (n, f) -> (n, VList . f)) seq_funcs
++ map (\ (n, po) ->
(n,\[VProc p]-> VProc $ POperator po p)) proc_operators
++ other_funcs)
++ map mkMonadicFunc monadic_funcs
++ map mkProc procs
++ map mkConstant constants
injectBuiltInFunctions :: EvaluationMonad a -> EvaluationMonad a
injectBuiltInFunctions = addScopeAndBind builtInFunctions