module CSPM.DataStructures.Syntax where
import CSPM.DataStructures.Types
import CSPM.DataStructures.Names
import Util.Annotated
import Util.Exception
type AnModule = Annotated () Module
type AnDecl = Annotated (Maybe SymbolTable, PSymbolTable) Decl
type AnMatch = Annotated () Match
type AnPat = Annotated () Pat
type AnExp = Annotated (Maybe Type, PType) Exp
type AnField = Annotated () Field
type AnStmt = Annotated () Stmt
type AnDataTypeClause = Annotated () DataTypeClause
type AnAssertion = Annotated () Assertion
type AnInteractiveStmt = Annotated () InteractiveStmt
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
type PDecl = AnDecl
type PMatch = AnMatch
type PPat = AnPat
type PExp = AnExp
type PStmt = AnStmt
type PField = AnField
type PDataTypeClause = AnDataTypeClause
type PAssertion = AnAssertion
type PInteractiveStmt = AnInteractiveStmt
type TCModule = AnModule
type TCDecl = AnDecl
type TCMatch = AnMatch
type TCPat = AnPat
type TCExp = AnExp
type TCField = AnField
type TCStmt = AnStmt
type TCDataTypeClause = AnDataTypeClause
type TCAssertion = AnAssertion
type TCInteractiveStmt = AnInteractiveStmt
data Literal =
Int Integer
| Bool Bool
deriving (Eq, Show)
data Module =
GlobalModule [AnDecl]
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 =
App AnExp [AnExp]
| BooleanBinaryOp BinaryBooleanOp AnExp AnExp
| BooleanUnaryOp UnaryBooleanOp AnExp
| Concat AnExp AnExp
| DotApp AnExp AnExp
| If AnExp AnExp AnExp
| Lambda AnPat AnExp
| Let [AnDecl] AnExp
| Lit Literal
| List [AnExp]
| ListComp [AnExp] [AnStmt]
| ListEnumFrom AnExp
| ListEnumFromTo AnExp AnExp
| ListLength AnExp
| MathsBinaryOp BinaryMathsOp AnExp AnExp
| MathsUnaryOp UnaryMathsOp AnExp
| Paren AnExp
| Set [AnExp]
| SetComp [AnExp] [AnStmt]
| SetEnum [AnExp]
| SetEnumComp [AnExp] [AnStmt]
| SetEnumFrom AnExp
| SetEnumFromTo AnExp AnExp
| Tuple [AnExp]
| Var QualifiedName
| AlphaParallel AnExp AnExp AnExp AnExp
| Exception AnExp AnExp AnExp
| ExternalChoice AnExp AnExp
| GenParallel AnExp AnExp AnExp
| GuardedExp AnExp AnExp
| Hiding AnExp AnExp
| InternalChoice AnExp AnExp
| Interrupt AnExp AnExp
| Interleave AnExp AnExp
| LinkParallel AnExp [(AnExp, AnExp)] [AnStmt] AnExp
| Prefix AnExp [AnField] AnExp
| Rename AnExp [(AnExp, AnExp)] [AnStmt]
| SequentialComp AnExp AnExp
| SlidingChoice AnExp AnExp
| ReplicatedAlphaParallel [AnStmt] AnExp AnExp
| ReplicatedExternalChoice [AnStmt] AnExp
| ReplicatedInterleave [AnStmt] AnExp
| ReplicatedInternalChoice [AnStmt] AnExp
| ReplicatedLinkParallel [(AnExp, AnExp)] [AnStmt] AnExp
| ReplicatedParallel AnExp [AnStmt] AnExp
| ExpPatWildCard
| ExpPatDoublePattern AnExp AnExp
deriving (Eq, Show)
data Field =
Output AnExp
| Input AnPat (Maybe AnExp)
| NonDetInput AnPat (Maybe AnExp)
deriving (Eq, Show)
data Stmt =
Generator AnPat AnExp
| Qualifier AnExp
deriving (Eq, Show)
data InteractiveStmt =
Evaluate AnExp
| Bind AnDecl
| RunAssertion Assertion
deriving Show
data Decl =
FunBind Name [AnMatch]
| PatBind AnPat AnExp
| Assert Assertion
| External [Name]
| Transparent [Name]
| Channel [Name] (Maybe AnExp)
| DataType Name [AnDataTypeClause]
| NameType Name AnExp
deriving (Eq, Show)
data Assertion =
Refinement AnExp Model AnExp [ModelOption]
| PropertyCheck AnExp SemanticProperty (Maybe Model)
| BoolAssertion AnExp
| ASNot Assertion
deriving (Eq, Show)
data Model =
Traces
| Failures
| FailuresDivergences
| Refusals
| RefusalsDivergences
| Revivals
| RevivalsDivergences
deriving (Eq, Show)
data ModelOption =
TauPriority AnExp
deriving (Eq, Show)
data SemanticProperty =
DeadlockFreedom
| Deterministic
| LivelockFreedom
deriving (Eq, Show)
data DataTypeClause =
DataTypeClause Name (Maybe AnExp)
deriving (Eq, Show)
data Match =
Match [[AnPat]] AnExp
deriving (Eq, Show)
data Pat =
PConcat AnPat AnPat
| PDotApp AnPat AnPat
| PDoublePattern AnPat AnPat
| PList [AnPat]
| PLit Literal
| PParen AnPat
| PSet [AnPat]
| PTuple [AnPat]
| PVar Name
| PWildCard
| PCompList [AnPat] (Maybe (AnPat, [AnPat])) Pat
| PCompDot [AnPat] Pat
deriving (Eq, Show)