CSPM.DataStructures.Syntax

Contents

Modules
Declarations
- Assertions
- Data Type Clauses
Expressions
- Fields
- Statements
Patterns
Interactive Statements
Type Synonyms
- Pre-Renaming Types
- Post-Renaming Types
Helpers

Description

This module represents the abstract syntax tree of machine CSP. Most of the datatypes are parameterised over the type of variables that they contain. Before renaming (by CSPM.Renamer) the variables are of type UnRenamedName, wheras after renaming they are of type Name (and are hence associated with their bindings instances). Furthermore, nearly all pieces of syntax are annoated with their location in the source code, and (sometimes) with their type (but only after type checking). This is done using the Annotated datatype.

Synopsis

Modules

data Module id Source

Constructors

GlobalModule [AnDecl id]

Instances

TypeCheckable TCModule ()
Eq id => Eq (Module id)
Show id => Show (Module id)
PrettyPrintable id => PrettyPrintable [Module id]
PrettyPrintable id => PrettyPrintable (Module id)
Desugarable (Module Name)
Compressable (Module a)
TypeCheckable [TCModule] ()
TypeCheckable (Module Name) ()
Renamable (Module UnRenamedName) (Module Name)

Declarations

data Decl id Source

Constructors

FunBind id [AnMatch id]	A function binding, e.g. `func(x,y)(z) = 0`.
PatBind (AnPat id) (AnExp id)	The binding of a pattern to an expression, e.g. `(p,q) = e`.
Assert (Assertion id)	An assertion in a file, e.g. `assert P [T= Q`.
External	An import of an external function, e.g. `external test`,
Fields externalImportedNames :: [id]
Transparent	An import of a transparent function, e.g. `transparent normal`.
Fields transparentImportedNames :: [id]
Channel [id] (Maybe (AnExp id))	A channel declaration, e.g. `channel c, d : {0..1}.{0..1}`.
DataType id [AnDataTypeClause id]	A datatype declaration, e.g. `datatype T = Clause1 \| Clause2`.
NameType id (AnExp id)	A nametype declaration, e.g. `nametype T2 = T.T`.

Instances

TypeCheckable TCDecl [(Name, Type)]
Eq id => Eq (Decl id)
Show id => Show (Decl id)
PrettyPrintable id => PrettyPrintable (Decl id)
Desugarable (Decl Name)
FreeVars (Decl UnRenamedName)
Compressable (Decl a)
Dependencies (Decl Name)
TypeCheckable (Decl Name) [(Name, Type)]

data Match id Source

Matches occur on the left hand side of a function declaration and there is one Match for each clause of the declaration. For example, given the declaration:

      f() = 0
      f(x^xs) = 1+f(xs)

there would be two matches.

Constructors

Match
Fields matchPatterns :: [[AnPat id]] The patterns that need to be matched. This is a list of lists as functions may be curried, like `f(x,y)(z) = ...`. matchRightHandSide :: AnExp id The expression to be evaluated if the match succeeds.

Instances

TypeCheckable TCMatch Type
Eq id => Eq (Match id)
Show id => Show (Match id)
Desugarable (Match Name)
Compressable (Match a)
Dependencies (Match Name)
TypeCheckable (Match Name) Type
Renamable (Match UnRenamedName) (Match Name)

Assertions

data Assertion id Source

Constructors

Refinement	A refinement assertion, e.g. `assert P [F= Q`.
Fields refinementSpecification :: AnExp id refinementModel :: Model refinementImplementation :: AnExp id refinementModelOptions :: [ModelOption id]
PropertyCheck	A check of property, like deadlock freedom, e.g. `assert P :[deadlock free [F]]`.
Fields propertyCheckProcess :: AnExp id propertyCheckProperty :: SemanticProperty propertyCheckModel :: Maybe Model
BoolAssertion (AnExp id)	A boolean assertion, not currently supported.
ASNot (Assertion id)	The negation of an assertion, not currently supported.

Instances

Eq id => Eq (Assertion id)
Show id => Show (Assertion id)
PrettyPrintable id => PrettyPrintable (Assertion id)
Desugarable (Assertion Name)
Compressable (Assertion a)
Dependencies (Assertion Name)
TypeCheckable (Assertion Name) ()
Renamable (Assertion UnRenamedName) (Assertion Name)

data Model Source

Constructors

Traces
Failures
FailuresDivergences
Refusals
RefusalsDivergences
Revivals
RevivalsDivergences

Instances

Eq Model
Show Model
PrettyPrintable Model
Compressable Model

data ModelOption id Source

Constructors

TauPriority (AnExp id)

Instances

Eq id => Eq (ModelOption id)
Show id => Show (ModelOption id)
PrettyPrintable id => PrettyPrintable (ModelOption id)
Desugarable (ModelOption Name)
Compressable (ModelOption a)
Dependencies (ModelOption Name)
TypeCheckable (ModelOption Name) ()
Renamable (ModelOption UnRenamedName) (ModelOption Name)

data SemanticProperty Source

Constructors

DeadlockFreedom
Deterministic
LivelockFreedom

Instances

Eq SemanticProperty
Show SemanticProperty
PrettyPrintable SemanticProperty
Compressable SemanticProperty

Data Type Clauses

data DataTypeClause id Source

The clause of a datatype, e.g. if a datatype declaration was:

 datatype T = A.Int.Bool | B.Bool | C

Then T would have three datatype clauses, one for each of its tags (i.e. A, B and C).

Constructors

DataTypeClause
Fields dataTypeClauseName :: id The name of the datatype clause. dataTypeClauseTypeExpression :: Maybe (AnExp id) The expression that gives the set of values that can be dotted with this clause. For example, in the above example the datatype clause for A would have Int.Bool as its type expression.

Instances

TypeCheckable TCDataTypeClause (Name, [Type])
Eq id => Eq (DataTypeClause id)
Show id => Show (DataTypeClause id)
PrettyPrintable id => PrettyPrintable (DataTypeClause id)
Desugarable (DataTypeClause Name)
Compressable (DataTypeClause a)
Dependencies (DataTypeClause Name)
TypeCheckable (DataTypeClause Name) (Name, [Type])

Expressions

data Exp id Source

An expression.

Constructors

App	Function application.
Fields appFunction :: AnExp id The function. appArguments :: [AnExp id] The arguments applied to the function
BooleanBinaryOp	Application of a binary boolean operator.
Fields booleanBinaryOpOperator :: BinaryBooleanOp booleanBinaryOpLeftExpression :: AnExp id booleanBinaryOpRightExpression :: AnExp id
BooleanUnaryOp	Application of a unary boolean operator.
Fields unaryBooleanOpOperator :: UnaryBooleanOp unaryBooleanExpression :: AnExp id
Concat	List concatenation, e.g. `x^y`.
Fields concatLeftList :: AnExp id concatRightList :: AnExp id
DotApp	Dot operator application, e.g. `c.x`.
Fields dotAppLeftArgument :: AnExp id dotAppRighArgument :: AnExp id
If	If statements, e.g. `if cond then e1 else e2`.
Fields ifCondition :: AnExp id The condition of the if. ifThenBranch :: AnExp id The then branch. ifElseBranch :: AnExp id
Lambda	Lambda functions, e.g. `(x,y) @ e(x,y)`.
Fields lambdaBindingPattern :: AnPat id lambdaRightHandSide :: AnExp id
Let	Let declarations, e.g. `let func = e1 within e2`.
Fields letDeclarations :: [AnDecl id] letExpression :: AnExp id
Lit	Literals, e.g. `true` or `1`.
Fields litLiteral :: Literal
List	List literals, e.g. `1,2,3`.
Fields listItems :: [AnExp id]
ListComp	List comprehensions, e.g. `x,y \| (x,y) <- e`.
Fields listCompItems :: [AnExp id] listCompStatements :: [AnStmt id]
ListEnumFrom	Infinite list of integers from the given value, e.g. `1..`.
Fields listEnumFromLowerBound :: AnExp id
ListEnumFromTo	Bounded list of integers between the given values, e.g. `1..3`.
Fields listEnumFromToLowerBound :: AnExp id listEnumFromToUpperBound :: AnExp id
ListLength	The length of the list, e.g. `#list`.
Fields listLengthExpression :: AnExp id
MathsBinaryOp	Application of binary maths operator, e.g. `x+y`.
Fields mathsBinaryOpOperator :: BinaryMathsOp mathsBinaryOpLeftExpression :: AnExp id mathsBinaryOpRightExpression :: AnExp id
MathsUnaryOp	Application of unary maths operator, e.g. `-x`.
Fields mathsUnaryOpOperator :: UnaryMathsOp mathsUnaryOpExpression :: AnExp id
Paren	A user provided bracket, e.g. `(e)`.
Fields parenExpression :: AnExp id
Set	Set literals, e.g. `{1,2,3}`.
Fields setItems :: [AnExp id]
SetComp	Set comprehensions, e.g. `{x,y \| (x,y) <- e}`.
Fields setCompItems :: [AnExp id] setCompStatements :: [AnStmt id]
SetEnum	Enumerated Sets, i.e. sets that complete the events, e.g. `{\| c.x \|}`.
Fields setEnumItems :: [AnExp id]
SetEnumComp	Set comprehension version of `SetEnum`, e.g. `{\| c.x \| x <- xs \|}`.
Fields setEnumCompItems :: [AnExp id] setEnumCompStatements :: [AnStmt id]
SetEnumFrom	The infinite set of integers from the given value, e.g. `{5..}`.
Fields setEnumFromLowerBound :: AnExp id
SetEnumFromTo	The bounded set of integers between the two given values, e.g. `{5..6}`.
Fields setEnumFromToLowerBound :: AnExp id The lower bound. setEnumFromToUpperBound :: AnExp id The upper bound.
Tuple	Tuples, e.g. `(1,2)`.
Fields tupleItems :: [AnExp id]
Var	Variables, e.g. `x`.
Fields varIdentity :: id
AlphaParallel	Alphabetised parallel, e.g. `P [A \|\| B] Q`.
Fields alphaParLeftProcess :: AnExp id Process 1. alphaParAlphabetLeftProcess :: AnExp id Alphabet of process 1. alphaParAlphabetRightProcess :: AnExp id Alphabet of process 2. alphaParRightProcess :: AnExp id Process 2.
Exception	Exception operator, e.g. `P [\| A \|> Q`.
Fields exceptionLeftProcess :: AnExp id exceptionAlphabet :: AnExp id exceptionRightProcess :: AnExp id
ExternalChoice	External choice, e.g. `P [] Q`.
Fields extChoiceLeftProcess :: AnExp id extChoiceRightOperator :: AnExp id
GenParallel	Generalised parallel, e.g. `P [\| A \|] Q`.
Fields genParallelLeftProcess :: AnExp id genParallelAlphabet :: AnExp id genParallelRightProcess :: AnExp id
GuardedExp	Guarded expressions, e.g. `b & P` where `b` is a boolean expression. This is equivalent to `if b then P else STOP`.
Fields guardedExpCondition :: AnExp id guardedExpProcess :: AnExp id
Hiding	Hiding of events, e.g. `P A`.
Fields hidingProcess :: AnExp id The process the hiding is applied to. hidingAlphabet :: AnExp id The set of events to be hidden.
InternalChoice	Internal choice, e.g. `P \|~\| Q`.
Fields intChoiceLeftProcess :: AnExp id intChoiceRightProcess :: AnExp id
Interrupt	Interrupt (where the left process is turned off once the right process performs an event), e.g. `P / Q`.
Fields interruptLeftProcess :: AnExp id interruptRightProcess :: AnExp id
Interleave	Interleaving of processes, e.g. `P \|\|\| Q`.
Fields interleaveLeftProcess :: AnExp id interleaveRightProcess :: AnExp id
LinkParallel
Fields linkParLeftProcess :: AnExp id linkParTiedEvents :: [(AnExp id, AnExp id)] linkParTieStatements :: [AnStmt id] linkParRightProcess :: AnExp id
Prefix	Event prefixing, e.g. `c$x?y!z -> P`.
Fields prefixChannel :: AnExp id prefixFields :: [AnField id] prefixProcess :: AnExp id
Rename	Event renaming, e.g. `P [[ a.x <- b.x \| x <- X ]]`.
Fields renameProcess :: AnExp id The process that is renamed. renameTiedEvents :: [(AnExp id, AnExp id)] The events that are renamed, in the format of `(old, new)`. renameTieStatements :: [AnStmt id] The statements for the ties.
SequentialComp	Sequential composition, e.g. `P; Q`.
Fields seqCompLeftProcess :: AnExp id seqCompRightProcess :: AnExp id
SlidingChoice	Sliding choice, e.g. `P \|> Q`.
Fields slidingChoiceLeftProcess :: AnExp id slidingChoiceRightProcess :: AnExp id
ReplicatedAlphaParallel	Replicated alphabetised parallel, e.g. `\|\| x : X @ [\| A(x) \|] P(x)`.
Fields repAlphaParReplicatedStatements :: [AnStmt id] repAlphaParAlphabet :: AnExp id repAlphaParProcess :: AnExp id
ReplicatedExternalChoice	Replicated external choice, e.g. `[] x : X @ P(x)`.
Fields repExtChoiceReplicatedStatements :: [AnStmt id] repExtChoiceProcess :: AnExp id
ReplicatedInterleave	Replicated interleave, e.g. `\|\|\| x : X @ P(x)`.
Fields repInterleaveReplicatedStatements :: [AnStmt id] repInterleaveProcess :: AnExp id
ReplicatedInternalChoice	Replicated internal choice, e.g. `\|~\| x : X @ P(x)`.
Fields repIntChoiceReplicatedStatements :: [AnStmt id] repIntChoiceProcess :: AnExp id
ReplicatedLinkParallel	Replicated link parallel, e.g. `[a.x <- b.x \| x <- X(y)] y : Y @ P(y)`.
Fields repLinkParTiedChannels :: [(AnExp id, AnExp id)] The tied events. repLinkParTieStatements :: [AnStmt id] The statements for the ties. repLinkParReplicatedStatements :: [AnStmt id] The `Stmt`s - the process (and ties) are evaluated once for each value generated by these. repLinkParProcess :: AnExp id The process
ReplicatedParallel	Replicated parallel, e.g. `[\| A \|] x : X @ P(x)`.
Fields repParAlphabet :: AnExp id repParReplicatedStatements :: [AnStmt id] repParProcess :: AnExp id
ExpPatWildCard	Used only for parsing - never appears in an AST.
ExpPatDoublePattern (AnExp id) (AnExp id)	Used only for parsing - never appears in an AST.

Instances

TypeCheckable TCExp Type
Eq id => Eq (Exp id)
Show id => Show (Exp id)
PrettyPrintable id => PrettyPrintable (Exp id)
Desugarable (Exp Name)
Evaluatable (Exp Name)
Compressable (Exp a)
Dependencies (Exp Name)
TypeCheckable (Exp Name) Type
Renamable (Exp UnRenamedName) (Exp Name)

data BinaryMathsOp Source

Constructors

Divide
Minus
Mod
Plus
Times

Instances

Eq BinaryMathsOp
Show BinaryMathsOp
PrettyPrintable BinaryMathsOp

data BinaryBooleanOp Source

Constructors

And
Or
Equals
NotEquals
LessThan
GreaterThan
LessThanEq
GreaterThanEq

Instances

Eq BinaryBooleanOp
Show BinaryBooleanOp
PrettyPrintable BinaryBooleanOp

data UnaryMathsOp Source

Constructors

Negate

Instances

Eq UnaryMathsOp
Show UnaryMathsOp
PrettyPrintable UnaryMathsOp

data UnaryBooleanOp Source

Constructors

Not

Instances

Eq UnaryBooleanOp
Show UnaryBooleanOp
PrettyPrintable UnaryBooleanOp

Fields

Fields occur within prefix statements. For example, if the prefix was c$x?y!z then there would be three fields, of type NonDetInput, Input and Output respectively.

data Field id Source

Constructors

Output (AnExp id)	!x
Input (AnPat id) (Maybe (AnExp id))	?x:A
NonDetInput (AnPat id) (Maybe (AnExp id))	`$x:A` (see P395 UCS)

Instances

Eq id => Eq (Field id)
Show id => Show (Field id)
PrettyPrintable id => PrettyPrintable (Field id)
Desugarable (Field Name)
FreeVars (Field UnRenamedName)
Compressable (Field a)
FreeVars (Field Name)
Dependencies (Field Name)

Statements

Statements occur on the right hand side of a list comprehension, or in the context of replicated operators. For example, in ... | x <- y, func(b), x <- y and func(b) are both statements, of type Generator and Qualifier respectively.

data Stmt id Source

Constructors

Generator (AnPat id) (AnExp id)
Qualifier (AnExp id)

Instances

Eq id => Eq (Stmt id)
Show id => Show (Stmt id)
PrettyPrintable id => PrettyPrintable (Stmt id)
Desugarable (Stmt Name)
FreeVars (Stmt UnRenamedName)
Compressable (Stmt a)
FreeVars (Stmt Name)
Dependencies (Stmt Name)

Patterns

Patterns match against values and may bind some components of the values to variables.

data Pat id Source

Constructors

PConcat	The concatenation of two patterns, e.g. `p1^p2`.
Fields pConcatLeftPat :: AnPat id pConcatRightPat :: AnPat id
PDotApp	The dot of two patterns, e.g. `p1.p2`.
Fields pDotLeftPat :: AnPat id pDotRightPat :: AnPat id
PDoublePattern	A double pattern match, e.g. `p1@@p2`.
Fields pDoublePatLeftPat :: AnPat id pDoublePatRightPat :: AnPat id
PList	A literal pattern list, e.g. `p1,p2,p3`.
Fields pListItems :: [AnPat id]
PLit	A literal pattern, e.g. `true`, or `0`.
Fields pLitLiteral :: Literal
PParen	A user supplied parenthesis in a pattern.
Fields pParenPattern :: AnPat id
PSet	A set pattern. Only singleton patterns, or zero patterns are supported. This is checked by the desugarer. For example, `{p1,p2}` is not allowed, but `{p1}` and `{}` are allowed.
Fields pSetItems :: [AnPat id]
PTuple	A tuple pattern, e.g. `(p1,p2,p3)`.
Fields pTupleItems :: [AnPat id]
PVar	A variable pattern, e.g. `x`, or `A` where `A` is a datatype clause. If the variable is a datatype clause then it only matches that datatype tag, whereas for anything else it matches anything.
Fields pVarIdentity :: id
PWildCard	Matches anything but does not bind it.
PCompList	Since you can write list patterns such as: f(<x,y>^xs^<z,p>^<9,0>) f(<x,y>) f(xs^<x,y>) we need an easy may of matching them. Thus, we compile the patterns to a `PCompList` instead. `PCompList ps (Just (p, ps'))` corresponds to a list where it starts with ps (where each p in ps matches exactly one list element, has a middle of p (which must be a variable pattern, or a wildcard) and and end matching exactly ps' (again, where each p in ps matches exactly one list component).
Fields pListStartItems :: [AnPat id] pListMiddleEndItems :: Maybe (AnPat id, [AnPat id]) pListOriginalPattern :: Pat id
PCompDot	Like with a `PCompList` we flatten nested dot patterns to make it easier to evaluate.
Fields pDotItems :: [AnPat id] pDotOriginalpattern :: Pat id

Instances

TypeCheckable TCPat Type
Eq id => Eq (Pat id)
Show id => Show (Pat id)
PrettyPrintable id => PrettyPrintable (Pat id)
Desugarable (Pat Name)
FreeVars (Pat UnRenamedName)
Bindable (Pat Name)
FreeVars (Pat Name)
Compressable (Pat a)
FreeVars (Pat Name)
Dependencies (Pat Name)
TypeCheckable (Pat Name) Type

Interactive Statements

Interactive statements are intended to be input by an interactive editor.

data InteractiveStmt id Source

A statement in an interactive session.

Constructors

Evaluate (AnExp id)
Bind (AnDecl id)
RunAssertion (Assertion id)

Instances

TypeCheckable TCInteractiveStmt ()
Show id => Show (InteractiveStmt id)
PrettyPrintable id => PrettyPrintable (InteractiveStmt id)
Desugarable (InteractiveStmt Name)
Compressable (InteractiveStmt a)
TypeCheckable (InteractiveStmt Name) ()
Renamable (InteractiveStmt UnRenamedName) (InteractiveStmt Name)