module CSPM.DataStructures.Syntax (
Module(..),
Decl(..), Match(..),
Assertion(..), Model(..), ModelOption(..), SemanticProperty(..),
DataTypeClause(..),
Exp(..), BinaryMathsOp(..), BinaryBooleanOp(..), UnaryMathsOp(..),
UnaryBooleanOp(..),
Field(..),
Stmt(..),
Pat(..),
InteractiveStmt(..),
AnModule(..), AnDecl(..), AnMatch(..), AnPat(..), AnExp(..), AnField(..),
AnStmt(..), AnDataTypeClause(..), AnAssertion(..), AnInteractiveStmt(..),
PModule(..), PDecl(..), PMatch(..), PPat(..), PExp(..), PField(..),
PStmt(..), PDataTypeClause(..), PAssertion(..), PInteractiveStmt(..),
TCModule(..), TCDecl(..), TCMatch(..), TCPat(..), TCExp(..), TCField(..),
TCStmt(..), TCDataTypeClause(..), TCAssertion(..), TCInteractiveStmt(..),
getType, getSymbolTable,
) where
import CSPM.DataStructures.Literals
import CSPM.DataStructures.Names
import CSPM.DataStructures.Types
import Util.Annotated
import Util.Exception
type AnModule id = Annotated () (Module id)
type AnDecl id = Annotated (Maybe SymbolTable, PSymbolTable) (Decl id)
type AnMatch id = Annotated () (Match id)
type AnPat id = Annotated () (Pat id)
type AnExp id = Annotated (Maybe Type, PType) (Exp id)
type AnField id = Annotated () (Field id)
type AnStmt id = Annotated () (Stmt id)
type AnDataTypeClause id = Annotated () (DataTypeClause id)
type AnAssertion id = Annotated () (Assertion id)
type AnInteractiveStmt id = Annotated () (InteractiveStmt id)
getType :: Annotated (Maybe Type, PType) a -> Type
getType an = case fst (annotation an) of
Just t -> t
Nothing -> panic "Cannot get the type of something that is not typechecked"
getSymbolTable :: Annotated (Maybe SymbolTable, PSymbolTable) a -> SymbolTable
getSymbolTable an = case fst (annotation an) of
Just t -> t
Nothing -> panic "Cannot get the symbol table of something that is not typechecked"
type PModule = AnModule UnRenamedName
type PDecl = AnDecl UnRenamedName
type PMatch = AnMatch UnRenamedName
type PPat = AnPat UnRenamedName
type PExp = AnExp UnRenamedName
type PStmt = AnStmt UnRenamedName
type PField = AnField UnRenamedName
type PDataTypeClause = AnDataTypeClause UnRenamedName
type PAssertion = AnAssertion UnRenamedName
type PInteractiveStmt = AnInteractiveStmt UnRenamedName
type TCModule = AnModule Name
type TCDecl = AnDecl Name
type TCMatch = AnMatch Name
type TCPat = AnPat Name
type TCExp = AnExp Name
type TCField = AnField Name
type TCStmt = AnStmt Name
type TCDataTypeClause = AnDataTypeClause Name
type TCAssertion = AnAssertion Name
type TCInteractiveStmt = AnInteractiveStmt Name
data Module id =
GlobalModule [AnDecl id]
deriving (Eq, Show)
data BinaryBooleanOp =
And
| Or
| Equals
| NotEquals
| LessThan
| GreaterThan
| LessThanEq
| GreaterThanEq
deriving (Eq, Show)
data UnaryBooleanOp =
Not
deriving (Eq, Show)
data UnaryMathsOp =
Negate
deriving (Eq, Show)
data BinaryMathsOp =
Divide | Minus | Mod | Plus | Times
deriving (Eq, Show)
data Exp id =
App {
appFunction :: AnExp id,
appArguments :: [AnExp id]
}
| BooleanBinaryOp {
booleanBinaryOpOperator :: BinaryBooleanOp,
booleanBinaryOpLeftExpression :: AnExp id,
booleanBinaryOpRightExpression :: AnExp id
}
| BooleanUnaryOp {
unaryBooleanOpOperator :: UnaryBooleanOp,
unaryBooleanExpression :: AnExp id
}
| Concat {
concatLeftList :: AnExp id,
concatRightList :: AnExp id
}
| DotApp {
dotAppLeftArgument :: AnExp id,
dotAppRighArgument :: AnExp id
}
| If {
ifCondition :: AnExp id,
ifThenBranch :: AnExp id,
ifElseBranch :: AnExp id
}
| Lambda {
lambdaBindingPattern :: AnPat id,
lambdaRightHandSide :: AnExp id
}
| Let {
letDeclarations :: [AnDecl id],
letExpression :: AnExp id
}
| Lit {
litLiteral :: Literal
}
| List {
listItems :: [AnExp id]
}
| ListComp {
listCompItems :: [AnExp id],
listCompStatements :: [AnStmt id]
}
| ListEnumFrom {
listEnumFromLowerBound :: AnExp id
}
| ListEnumFromTo {
listEnumFromToLowerBound :: AnExp id,
listEnumFromToUpperBound :: AnExp id
}
| ListLength {
listLengthExpression :: AnExp id
}
| MathsBinaryOp {
mathsBinaryOpOperator :: BinaryMathsOp,
mathsBinaryOpLeftExpression :: AnExp id,
mathsBinaryOpRightExpression :: AnExp id
}
| MathsUnaryOp {
mathsUnaryOpOperator :: UnaryMathsOp,
mathsUnaryOpExpression :: AnExp id
}
| Paren {
parenExpression :: AnExp id
}
| Set {
setItems :: [AnExp id]
}
| SetComp {
setCompItems :: [AnExp id],
setCompStatements :: [AnStmt id]
}
| SetEnum {
setEnumItems :: [AnExp id]
}
| SetEnumComp {
setEnumCompItems :: [AnExp id],
setEnumCompStatements :: [AnStmt id]
}
| SetEnumFrom {
setEnumFromLowerBound :: AnExp id
}
| SetEnumFromTo {
setEnumFromToLowerBound :: AnExp id,
setEnumFromToUpperBound :: AnExp id
}
| Tuple {
tupleItems :: [AnExp id]
}
| Var {
varIdentity :: id
}
| AlphaParallel {
alphaParLeftProcess :: AnExp id,
alphaParAlphabetLeftProcess :: AnExp id,
alphaParAlphabetRightProcess :: AnExp id,
alphaParRightProcess :: AnExp id
}
| Exception {
exceptionLeftProcess :: AnExp id,
exceptionAlphabet :: AnExp id,
exceptionRightProcess :: AnExp id
}
| ExternalChoice {
extChoiceLeftProcess :: AnExp id,
extChoiceRightOperator :: AnExp id
}
| GenParallel {
genParallelLeftProcess :: AnExp id,
genParallelAlphabet :: AnExp id,
genParallelRightProcess :: AnExp id
}
| GuardedExp {
guardedExpCondition :: AnExp id,
guardedExpProcess :: AnExp id
}
| Hiding {
hidingProcess :: AnExp id,
hidingAlphabet :: AnExp id
}
| InternalChoice {
intChoiceLeftProcess :: AnExp id,
intChoiceRightProcess :: AnExp id
}
| Interrupt {
interruptLeftProcess :: AnExp id,
interruptRightProcess :: AnExp id
}
| Interleave {
interleaveLeftProcess :: AnExp id,
interleaveRightProcess :: AnExp id
}
| LinkParallel {
linkParLeftProcess :: AnExp id,
linkParTiedEvents :: [(AnExp id, AnExp id)],
linkParTieStatements :: [AnStmt id],
linkParRightProcess :: AnExp id
}
| Prefix {
prefixChannel :: AnExp id,
prefixFields :: [AnField id],
prefixProcess :: AnExp id
}
| Rename {
renameProcess :: AnExp id,
renameTiedEvents :: [(AnExp id, AnExp id)],
renameTieStatements :: [AnStmt id]
}
| SequentialComp {
seqCompLeftProcess :: AnExp id,
seqCompRightProcess :: AnExp id
}
| SlidingChoice {
slidingChoiceLeftProcess :: AnExp id,
slidingChoiceRightProcess :: AnExp id
}
| ReplicatedAlphaParallel {
repAlphaParReplicatedStatements :: [AnStmt id],
repAlphaParAlphabet :: AnExp id,
repAlphaParProcess :: AnExp id
}
| ReplicatedExternalChoice {
repExtChoiceReplicatedStatements :: [AnStmt id],
repExtChoiceProcess :: AnExp id
}
| ReplicatedInterleave {
repInterleaveReplicatedStatements :: [AnStmt id],
repInterleaveProcess :: AnExp id
}
| ReplicatedInternalChoice {
repIntChoiceReplicatedStatements :: [AnStmt id],
repIntChoiceProcess :: AnExp id
}
| ReplicatedLinkParallel {
repLinkParTiedChannels :: [(AnExp id, AnExp id)],
repLinkParTieStatements :: [AnStmt id],
repLinkParReplicatedStatements :: [AnStmt id],
repLinkParProcess :: AnExp id
}
| ReplicatedParallel {
repParAlphabet :: AnExp id,
repParReplicatedStatements :: [AnStmt id],
repParProcess :: AnExp id
}
| ExpPatWildCard
| ExpPatDoublePattern (AnExp id) (AnExp id)
deriving (Eq, Show)
data Field id =
Output (AnExp id)
| Input (AnPat id) (Maybe (AnExp id))
| NonDetInput (AnPat id) (Maybe (AnExp id))
deriving (Eq, Show)
data Stmt id =
Generator (AnPat id) (AnExp id)
| Qualifier (AnExp id)
deriving (Eq, Show)
data InteractiveStmt id =
Evaluate (AnExp id)
| Bind (AnDecl id)
| RunAssertion (Assertion id)
deriving Show
data Decl id =
FunBind id [AnMatch id]
| PatBind (AnPat id) (AnExp id)
| Assert (Assertion id)
| External {
externalImportedNames :: [id]
}
| Transparent {
transparentImportedNames :: [id]
}
| Channel [id] (Maybe (AnExp id))
| DataType id [AnDataTypeClause id]
| NameType id (AnExp id)
deriving (Eq, Show)
data Assertion id =
Refinement {
refinementSpecification :: AnExp id,
refinementModel :: Model,
refinementImplementation :: AnExp id,
refinementModelOptions :: [ModelOption id]
}
| PropertyCheck {
propertyCheckProcess :: AnExp id,
propertyCheckProperty :: SemanticProperty,
propertyCheckModel :: Maybe Model
}
| BoolAssertion (AnExp id)
| ASNot (Assertion id)
deriving (Eq, Show)
data Model =
Traces
| Failures
| FailuresDivergences
| Refusals
| RefusalsDivergences
| Revivals
| RevivalsDivergences
deriving (Eq, Show)
data ModelOption id =
TauPriority (AnExp id)
deriving (Eq, Show)
data SemanticProperty =
DeadlockFreedom
| Deterministic
| LivelockFreedom
deriving (Eq, Show)
data DataTypeClause id =
DataTypeClause {
dataTypeClauseName :: id,
dataTypeClauseTypeExpression :: Maybe (AnExp id)
}
deriving (Eq, Show)
data Match id =
Match {
matchPatterns :: [[AnPat id]],
matchRightHandSide :: AnExp id
}
deriving (Eq, Show)
data Pat id =
PConcat {
pConcatLeftPat :: AnPat id,
pConcatRightPat :: AnPat id
}
| PDotApp {
pDotLeftPat :: AnPat id,
pDotRightPat :: AnPat id
}
| PDoublePattern {
pDoublePatLeftPat :: AnPat id,
pDoublePatRightPat :: AnPat id
}
| PList {
pListItems :: [AnPat id]
}
| PLit {
pLitLiteral :: Literal
}
| PParen {
pParenPattern :: AnPat id
}
| PSet {
pSetItems :: [AnPat id]
}
| PTuple {
pTupleItems :: [AnPat id]
}
| PVar {
pVarIdentity :: id
}
| PWildCard
| PCompList {
pListStartItems :: [AnPat id],
pListMiddleEndItems :: Maybe (AnPat id, [AnPat id]),
pListOriginalPattern :: Pat id
}
| PCompDot {
pDotItems :: [AnPat id],
pDotOriginalpattern :: Pat id
}
deriving (Eq, Show)