libcspm-0.2.0: A library providing a parser, type checker and evaluator for CSPM.




data Value Source


VInt Int 
VBool Bool 
VTuple [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] 
VSet ValueSet 
VFunction ([Value] -> EvaluationMonad Value) 
VProc Proc 

data Proc Source

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

data Event Source

Events, as represented in the LTS.



The internal special event tau.


The internal event tick, representing termination.

UserEvent String

Any event defined in a channel definition.

compareValues :: Value -> Value -> Maybe OrderingSource

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

valueEventToEvent :: Value -> EventSource

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

combineDots :: Value -> Value -> EvaluationMonad ValueSource

Takes two values and dots then together appropriately.

extensions :: Value -> EvaluationMonad [Value]Source

Takes a datatype or a channel value and then computes all x such that ev.x is a full datatype/event. Each of the returned values is guaranteed to be a VDot.

oneFieldExtensions :: Value -> EvaluationMonad [Value]Source

Returns an x such that ev.x has been extended by exactly one atomic field. This could be inside a subfield or elsewhere.

productions :: Value -> EvaluationMonad [Value]Source

Takes a datatype or a channel value and computes v.x for all x that complete the value.