Safe Haskell	None

CSPM.Evaluator.Values

Synopsis

Documentation

data Value Source

Constructors

VInt Int
VChar Char
VBool Bool
VTuple (Array Int Value)
VDot [Value]	If A is a datatype clause that has 3 fields a b c then a runtime instantiation of this would be VDot [VDataType A, a, b, c] where a,b and c can contain other VDots.
VChannel Name
VDataType Name
VList [Value]
VMap (Map Value Value)
VSet ValueSet
VFunction FunctionIdentifier ([Value] -> EvaluationMonad Value)
VProc UProc
VThunk (EvaluationMonad Value)

type UProc = UnCompiledProc Source

type UProcOperator = UnCompiledProcOperator Source

data Proc seq op pn ev evs evm Source

A compiled process. Note this is an infinite data structure (due to PProcCall) as this makes compilation easy (we can easily chase dependencies).

Constructors

PUnaryOp (op seq ev evs evm) (Proc seq op pn ev evs evm)
PBinaryOp (op seq ev evs evm) (Proc seq op pn ev evs evm) (Proc seq op pn ev evs evm)
POp (op seq ev evs evm) (seq (Proc seq op pn ev evs evm))
PProcCall pn (Proc seq op pn ev evs evm)	Labels the process this contains. This allows infinite loops to be spotted.

Instances

NFData UProc
PrettyPrintable UnCompiledProc
(Foldable seq, Functor seq, MonadicPrettyPrintable m pn, MonadicPrettyPrintable m ev, MonadicPrettyPrintable m evs) => MonadicPrettyPrintable m (Proc seq CSPOperator pn ev evs (seq (ev, ev)))
(Eq pn, Eq (seq (Proc seq op pn ev evs evm)), Eq (op seq ev evs evm)) => Eq (Proc seq op pn ev evs evm)
(Ord pn, Ord (seq (Proc seq op pn ev evs evm)), Ord (op seq ev evs evm)) => Ord (Proc seq op pn ev evs evm)
(Hashable pn, Hashable (seq (Proc seq op pn ev evs evm)), Hashable (op seq ev evs evm)) => Hashable (Proc seq op pn ev evs evm)
Precedence (Proc seq CSPOperator pn ev evs (seq (ev, ev)))

data CSPOperator seq ev evs evm Source

Constructors

PAlphaParallel (seq evs)
PException evs
PExternalChoice
PGenParallel evs
PHide evs
PInternalChoice
PInterrupt
PInterleave
PLinkParallel evm
POperator (ProcOperator seq evs)
PPrefix ev
PRename evm
PSequentialComp
PSlidingChoice
PSynchronisingExternalChoice evs
PSynchronisingInterrupt evs

Instances

NFData UnCompiledOperator
NFData UProc
PrettyPrintable UnCompiledProc
(Applicative m, Foldable seq, Functor seq, Monad m, MonadicPrettyPrintable m ev, MonadicPrettyPrintable m evs) => MonadicPrettyPrintable m (CSPOperator seq ev evs (seq (ev, ev)))
(Foldable seq, Functor seq, MonadicPrettyPrintable m pn, MonadicPrettyPrintable m ev, MonadicPrettyPrintable m evs) => MonadicPrettyPrintable m (Proc seq CSPOperator pn ev evs (seq (ev, ev)))
(Eq ev, Eq evs, Eq evm, Eq (seq evs)) => Eq (CSPOperator seq ev evs evm)
(Ord ev, Ord evs, Ord evm, Ord (seq evs)) => Ord (CSPOperator seq ev evs evm)
(Hashable ev, Hashable evm, Hashable evs, Hashable (seq evs)) => Hashable (CSPOperator seq ev evs evm)
Precedence (Proc seq CSPOperator pn ev evs (seq (ev, ev)))

data ProcOperator seq evs Source

An operator that can be applied to processes.

Constructors

Chase Bool
Determinise
Diamond
Explicate Bool
Normalize Bool
ModelCompress
Prioritise Bool (seq evs)
StrongBisim
TauLoopFactor
WeakBisim

Instances

NFData UnCompiledProcOperator
(Applicative m, Foldable seq, Monad m, MonadicPrettyPrintable m evs) => MonadicPrettyPrintable m (ProcOperator seq evs)
Eq (seq evs) => Eq (ProcOperator seq evs)
Ord (seq evs) => Ord (ProcOperator seq evs)
Hashable (seq evs) => Hashable (ProcOperator seq evs)
(Foldable seq, MonadicPrettyPrintable Identity evs) => PrettyPrintable (ProcOperator seq evs)

data Event Source

Events, as represented in the LTS.

Constructors

Tau	The internal special event tau.
Tick	The internal event tick, representing termination.
UserEvent Value	Any event defined in a channel definition.

Instances

type EventSet = Seq Event Source

data ScopeIdentifier Source

A disambiguator between different occurences of either processes or functions. This works by storing the values that are bound (i.e. the free variables the inner thing may depend on). This is used as a ProcName and for FunctionIdentifiers.

Constructors

SFunctionBind
Fields scopeFunctionName :: Name scopeFunctionArguments :: [[Value]] parentScopeIdentifier :: Maybe ScopeIdentifier
SVariableBind
Fields variablesBound :: [Value] parentScopeIdentifier :: Maybe ScopeIdentifier

Instances

Eq ScopeIdentifier
Ord ScopeIdentifier
NFData ScopeIdentifier
Hashable ScopeIdentifier
PrettyPrintable ScopeIdentifier
(Applicative m, Monad m, MonadicPrettyPrintable m Value) => MonadicPrettyPrintable m ScopeIdentifier

data FunctionIdentifier Source

Constructors

FBuiltInFunction
Fields functionName :: Name arguments :: [Value]
FLambda
Fields lambdaExpression :: Exp Name parentFunctionIdentifier :: Maybe ScopeIdentifier
FMatchBind
Fields functionName :: Name argumentGroups :: [[Value]] scopeIdentifier :: Maybe ScopeIdentifier The free variables this is bound in

Instances

Eq FunctionIdentifier
Ord FunctionIdentifier
NFData FunctionIdentifier
Hashable FunctionIdentifier

compareValues :: Value -> Value -> Maybe Ordering Source

Implements CSPM comparisons (note that Ord Value does not).

procName :: ScopeIdentifier -> ProcName Source

scopeId :: Name -> [[Value]] -> Maybe ScopeIdentifier -> ScopeIdentifier Source

annonymousScopeId :: [Value] -> Maybe ScopeIdentifier -> ScopeIdentifier Source

valueEventToEvent :: Value -> Event Source

This assumes that the value is a VDot with the left is a VChannel

noSave :: EvaluationMonad Value -> EvaluationMonad Value Source

Given a program that yields a value, returns a second program that can be inserted into the environment, but will cause the environment not to save the actual value, but to recompute it everytime. This is useful for cheap, to compute, but high cost in terms of memory, computations (like named processes).

maybeSave :: Type -> EvaluationMonad Value -> EvaluationMonad Value Source

removeThunk :: Value -> EvaluationMonad Value Source

lookupVar :: Name -> EvaluationMonad Value Source

tupleFromList :: [Value] -> Value Source

trimValueForProcessName :: Value -> Value Source

module Data.Array

Eq Value
Ord Value
NFData Value
Hashable Value
PrettyPrintable Value
(Applicative m, Monad m, MonadicPrettyPrintable m TCExp, MonadicPrettyPrintable m UProc, MonadicPrettyPrintable m UProcOperator, MonadicPrettyPrintable m ValueSet) => MonadicPrettyPrintable m Value

Eq Event
Ord Event
NFData UnCompiledProcOperator
NFData UnCompiledOperator
NFData Event
NFData UProc
Hashable Event
PrettyPrintable UnCompiledProc
PrettyPrintable Event
(Applicative m, Monad m, MonadicPrettyPrintable m Value) => MonadicPrettyPrintable m Event
Foldable f => MonadicPrettyPrintable Identity (f Event)
Foldable f => MonadicPrettyPrintable EvaluationMonad (f Event)
PrettyPrintable (Seq Event)