Copyright | (c) Fontaine 2008 - 2012 |
---|---|
License | BSD3 |
Maintainer | Fontaine@cs.uni-duesseldorf.de |
Stability | experimental |
Portability | GHC-only |
Safe Haskell | None |
Language | Haskell2010 |
Language.CSPM.AST
Description
This module defines an Abstract Syntax Tree for CSPM. This is the AST that is computed by the parser. For historical reasons, it is rather unstructured.
- type AstAnnotation x = IntMap x
- type Bindings = Map String UniqueIdent
- type FreeNames = IntMap UniqueIdent
- newtype NodeId = NodeId {}
- mkNodeId :: Int -> NodeId
- data Labeled t = Labeled {}
- labeled :: t -> Labeled t
- setNode :: Labeled t -> y -> Labeled y
- type LIdent = Labeled Ident
- data Ident
- = Ident { }
- | UIdent UniqueIdent
- unUIdent :: Ident -> UniqueIdent
- identId :: LIdent -> Int
- data UniqueIdent = UniqueIdent {
- uniqueIdentId :: Int
- bindingSide :: NodeId
- bindingLoc :: SrcLoc
- idType :: IDType
- realName :: String
- newName :: String
- prologMode :: PrologMode
- bindType :: BindType
- data IDType
- data PrologMode
- data BindType
- isLetBound :: BindType -> Bool
- data Module a = Module {
- moduleDecls :: [LDecl]
- moduleTokens :: Maybe [Token]
- moduleSrcLoc :: SrcLoc
- moduleComments :: [LocComment]
- modulePragmas :: [Pragma]
- data FromParser
- castModule :: Module a -> Module b
- type ModuleFromParser = Module FromParser
- type LExp = Labeled Exp
- type LProc = LExp
- data Exp
- = Var LIdent
- | IntExp Integer
- | SetExp LRange (Maybe [LCompGen])
- | ListExp LRange (Maybe [LCompGen])
- | ClosureComprehension ([LExp], [LCompGen])
- | Let [LDecl] LExp
- | Ifte LExp LExp LExp
- | CallFunction LExp [[LExp]]
- | CallBuiltIn LBuiltIn [[LExp]]
- | Lambda [LPattern] LExp
- | Stop
- | Skip
- | CTrue
- | CFalse
- | Events
- | BoolSet
- | IntSet
- | TupleExp [LExp]
- | Parens LExp
- | AndExp LExp LExp
- | OrExp LExp LExp
- | NotExp LExp
- | NegExp LExp
- | Fun1 LBuiltIn LExp
- | Fun2 LBuiltIn LExp LExp
- | DotTuple [LExp]
- | Closure [LExp]
- | ProcSharing LExp LProc LProc
- | ProcAParallel LExp LExp LProc LProc
- | ProcLinkParallel LLinkList LProc LProc
- | ProcRenaming [LRename] (Maybe LCompGenList) LProc
- | ProcException LExp LProc LProc
- | ProcRepSequence LCompGenList LProc
- | ProcRepInternalChoice LCompGenList LProc
- | ProcRepExternalChoice LCompGenList LProc
- | ProcRepInterleave LCompGenList LProc
- | ProcRepAParallel LCompGenList LExp LProc
- | ProcRepLinkParallel LCompGenList LLinkList LProc
- | ProcRepSharing LCompGenList LExp LProc
- | PrefixExp LExp [LCommField] LProc
- | PrefixI FreeNames LExp [LCommField] LProc
- | LetI [LDecl] FreeNames LExp
- | LambdaI FreeNames [LPattern] LExp
- | ExprWithFreeNames FreeNames LExp
- type LRange = Labeled Range
- data Range
- type LCommField = Labeled CommField
- data CommField
- type LLinkList = Labeled LinkList
- data LinkList
- = LinkList [LLink]
- | LinkListComprehension [LCompGen] [LLink]
- type LLink = Labeled Link
- data Link = Link LExp LExp
- type LRename = Labeled Rename
- data Rename = Rename LExp LExp
- type LBuiltIn = Labeled BuiltIn
- data BuiltIn = BuiltIn Const
- lBuiltInToConst :: LBuiltIn -> Const
- type LCompGenList = Labeled [LCompGen]
- type LCompGen = Labeled CompGen
- data CompGen
- type LPattern = Labeled Pattern
- data Pattern
- data Selector
- = IntSel Integer
- | TrueSel
- | FalseSel
- | SelectThis
- | ConstrSel UniqueIdent
- | DotSel Int Selector
- | SingleSetSel Selector
- | EmptySetSel
- | TupleLengthSel Int Selector
- | TupleIthSel Int Selector
- | ListLengthSel Int Selector
- | ListIthSel Int Selector
- | HeadSel Selector
- | HeadNSel Int Selector
- | PrefixSel Int Int Selector
- | TailSel Selector
- | SliceSel Int Int Selector
- | SuffixSel Int Int Selector
- type LDecl = Labeled Decl
- data Decl
- type FunArgs = [[LPattern]]
- data FunCase
- type LTypeDef = Labeled TypeDef
- data TypeDef
- type LConstructor = Labeled Constructor
- data Constructor = Constructor LIdent (Maybe LTypeDef)
- withLabel :: (NodeId -> a -> b) -> Labeled a -> Labeled b
- type LAssertDecl = Labeled AssertDecl
- data AssertDecl
- type LFDRModels = Labeled FDRModels
- data FDRModels
- type LFdrExt = Labeled FdrExt
- data FdrExt
- type LTauRefineOp = Labeled TauRefineOp
- data TauRefineOp
- type LRefineOp = Labeled RefineOp
- data RefineOp
- data Const
- = F_true
- | F_false
- | F_not
- | F_and
- | F_or
- | F_union
- | F_inter
- | F_diff
- | F_Union
- | F_Inter
- | F_member
- | F_card
- | F_empty
- | F_set
- | F_Set
- | F_Seq
- | F_null
- | F_head
- | F_tail
- | F_concat
- | F_elem
- | F_length
- | F_STOP
- | F_SKIP
- | F_Events
- | F_Int
- | F_Bool
- | F_CHAOS
- | F_Concat
- | F_Len2
- | F_Mult
- | F_Div
- | F_Mod
- | F_Add
- | F_Sub
- | F_Eq
- | F_NEq
- | F_GE
- | F_LE
- | F_LT
- | F_GT
- | F_Guard
- | F_Sequential
- | F_Interrupt
- | F_ExtChoice
- | F_IntChoice
- | F_Hiding
- | F_Timeout
- | F_Interleave
- type Pragma = String
- type LocComment = (Comment, SrcLoc)
- data Comment
Documentation
type AstAnnotation x = IntMap x Source #
type FreeNames = IntMap UniqueIdent Source #
labeled :: t -> Labeled t Source #
Wrap a node with a dummyLabel. todo: Redo we need a specal case in DataConstructor Labeled.
Constructors
Ident | |
UIdent UniqueIdent |
unUIdent :: Ident -> UniqueIdent Source #
data UniqueIdent Source #
Constructors
UniqueIdent | |
Fields
|
Instances
Constructors
VarID | |
ChannelID | |
NameTypeID | |
FunID | |
ConstrID | |
DataTypeID | |
TransparentID | |
BuiltInID |
Constructors
LetBound | |
NotLetBound |
isLetBound :: BindType -> Bool Source #
Constructors
Module | |
Fields
|
data FromParser Source #
Instances
castModule :: Module a -> Module b Source #
type ModuleFromParser = Module FromParser Source #
Constructors
type LCommField = Labeled CommField Source #
Constructors
LinkList [LLink] | |
LinkListComprehension [LCompGen] [LLink] |
lBuiltInToConst :: LBuiltIn -> Const Source #
type LCompGenList = Labeled [LCompGen] Source #
Constructors
type LConstructor = Labeled Constructor Source #
type LAssertDecl = Labeled AssertDecl Source #
data AssertDecl Source #
Constructors
AssertBool LExp | |
AssertRefine Bool LExp LRefineOp LExp | |
AssertTauPrio Bool LExp LTauRefineOp LExp LExp | |
AssertModelCheck Bool LExp LFDRModels (Maybe LFdrExt) |
Instances
type LFDRModels = Labeled FDRModels Source #
Constructors
DeadlockFree | |
Deterministic | |
LivelockFree |
type LTauRefineOp = Labeled TauRefineOp Source #
data TauRefineOp Source #
Instances
Constructors
type LocComment = (Comment, SrcLoc) Source #