-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | A library providing a parser, type checker and evaluator for CSPM.
--
-- This library provides a parser, type checker and evaluator for machine
-- CSP. The parser is designed to be compatible with FDR2 and, in
-- particular, deals with the ambiguity between greater than and end of
-- sequence in the same way (as far as possible, see CSPM.Parser
-- for more information). The typechecker is as liberal as it is possible
-- to make a typechecker without making typechecking undecidable.
-- Documentation on the type system is forthcoming. The evaluator is
-- relatively experimental, but should be able to evaluate any CSPM
-- expression that FDR2 can. The output of this phase (if a process is
-- evaluated) is a tree of CSP (note not CSPM) operator applications
-- which should be suitable for input into a refinement checker, or other
-- process algebraic tool.
--
-- The main module of interest will be the CSPM module. This
-- packages up most of the functionality of the library in an easy to
-- use, relatively high level format. See CSPM for an example of
-- how to use this module.
--
-- Version Numbering Policy: point releases (i.e. from x.y.z to
-- x.y.z') are guaranteed to be backwards compatible. Minor
-- releases (i.e. from x.y.z to x.y'.z') will not be
-- backwards compatible, but should be relatively easy to port to. Major
-- changes (i.e. from x.y.z to x'.y'.z') will not be
-- backwards compatible and may include large API redesigns.
@package libcspm
@version 0.2.1
-- | Various miscellaneous functions utility functions.
module Util.Prelude
-- | Given two orderings, returns the second if the first is EQ and
-- returns the first otherwise.
thenCmp :: Ordering -> Ordering -> Ordering
-- | Given a file path, if the first character is a ~ then expands the ~ to
-- the users' home directory.
expandPathIO :: String -> IO String
-- | Remove whitespace from the beginning and end of a string.
trim :: String -> String
-- | Compute the Cartesian product of a list of lists.
cartProduct :: [[a]] -> [[a]]
-- | Misc utility functions that are defined on monads.
module Util.Monad
concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b]
andM :: Monad m => [m Bool] -> m Bool
orM :: Monad m => [m Bool] -> m Bool
($$) :: Monad m => m (a -> b) -> m a -> m b
module Util.List
-- | Returns true iff the list has no duplicates.
noDups :: Eq a => [a] -> Bool
-- | Replaces the last item in a list. Assumes the list is non empty.
replaceLast :: [a] -> a -> [a]
cartesianProduct :: [[a]] -> [[a]]
module CSPM.Compiler.Set
type Set a = [a]
null :: Eq a => [a] -> Bool
member :: Eq a => a -> [a] -> Bool
empty :: [a]
unions :: Eq a => [[a]] -> [a]
union :: Eq a => [a] -> [a] -> [a]
difference :: Eq a => [a] -> [a] -> [a]
fromList :: a -> a
toList :: a -> a
unionMap :: Ord b => (a -> Set b) -> Set a -> Set b
split :: Set a -> (a, Set a)
subseteq :: Eq a => [a] -> [a] -> Bool
module Util.PrettyPrint
class PrettyPrintable a
prettyPrint :: PrettyPrintable a => a -> Doc
-- | The width, in spaces, of a tab character.
tabWidth :: Int
-- | Indent a document by tabWidth characters, on each line (uses
-- nest).
tabIndent :: Doc -> Doc
-- | Show a double d printing only places places after
-- the decimal place.
shortDouble :: Int -> Double -> Doc
-- | Pretty prints an integer and separates it into groups of 3, separated
-- by commas.
commaSeparatedInt :: Int -> Doc
-- | Surrounds a Doc with < and >.
angles :: Doc -> Doc
-- | Surrounds a Doc with '|'.
bars :: Doc -> Doc
-- | Separates a list of Docs by ','.
list :: [Doc] -> Doc
-- | Separates a list of Docs by ..
dotSep :: [Doc] -> Doc
-- | Converts a number into first, second etc.
speakNth :: Int -> Doc
-- | Equivalent to [d1, sep d2, sep d3, ...].
punctuateFront :: Doc -> [Doc] -> [Doc]
module CSPM.DataStructures.Literals
data Literal
-- | An integer. This is finite size, as per the FDR spec.
Int :: Int -> Literal
-- | A boolean (TODO: remove).
Bool :: Bool -> Literal
instance Eq Literal
instance Show Literal
instance PrettyPrintable Literal
module Util.Exception
-- | Any type that you wish to throw or catch as an exception must be an
-- instance of the Exception class. The simplest case is a new
-- exception type directly below the root:
--
--
-- data MyException = ThisException | ThatException
-- deriving (Show, Typeable)
--
-- instance Exception MyException
--
--
-- The default method definitions in the Exception class do what
-- we need in this case. You can now throw and catch
-- ThisException and ThatException as exceptions:
--
--
-- *Main> throw ThisException `catch` \e -> putStrLn ("Caught " ++ show (e :: MyException))
-- Caught ThisException
--
--
-- In more complicated examples, you may wish to define a whole hierarchy
-- of exceptions:
--
--
-- ---------------------------------------------------------------------
-- -- Make the root exception type for all the exceptions in a compiler
--
-- data SomeCompilerException = forall e . Exception e => SomeCompilerException e
-- deriving Typeable
--
-- instance Show SomeCompilerException where
-- show (SomeCompilerException e) = show e
--
-- instance Exception SomeCompilerException
--
-- compilerExceptionToException :: Exception e => e -> SomeException
-- compilerExceptionToException = toException . SomeCompilerException
--
-- compilerExceptionFromException :: Exception e => SomeException -> Maybe e
-- compilerExceptionFromException x = do
-- SomeCompilerException a <- fromException x
-- cast a
--
-- ---------------------------------------------------------------------
-- -- Make a subhierarchy for exceptions in the frontend of the compiler
--
-- data SomeFrontendException = forall e . Exception e => SomeFrontendException e
-- deriving Typeable
--
-- instance Show SomeFrontendException where
-- show (SomeFrontendException e) = show e
--
-- instance Exception SomeFrontendException where
-- toException = compilerExceptionToException
-- fromException = compilerExceptionFromException
--
-- frontendExceptionToException :: Exception e => e -> SomeException
-- frontendExceptionToException = toException . SomeFrontendException
--
-- frontendExceptionFromException :: Exception e => SomeException -> Maybe e
-- frontendExceptionFromException x = do
-- SomeFrontendException a <- fromException x
-- cast a
--
-- ---------------------------------------------------------------------
-- -- Make an exception type for a particular frontend compiler exception
--
-- data MismatchedParentheses = MismatchedParentheses
-- deriving (Typeable, Show)
--
-- instance Exception MismatchedParentheses where
-- toException = frontendExceptionToException
-- fromException = frontendExceptionFromException
--
--
-- We can now catch a MismatchedParentheses exception as
-- MismatchedParentheses, SomeFrontendException or
-- SomeCompilerException, but not other types, e.g.
-- IOException:
--
--
-- *Main> throw MismatchedParentheses catch e -> putStrLn ("Caught " ++ show (e :: MismatchedParentheses))
-- Caught MismatchedParentheses
-- *Main> throw MismatchedParentheses catch e -> putStrLn ("Caught " ++ show (e :: SomeFrontendException))
-- Caught MismatchedParentheses
-- *Main> throw MismatchedParentheses catch e -> putStrLn ("Caught " ++ show (e :: SomeCompilerException))
-- Caught MismatchedParentheses
-- *Main> throw MismatchedParentheses catch e -> putStrLn ("Caught " ++ show (e :: IOException))
-- *** Exception: MismatchedParentheses
--
class (Typeable e, Show e) => Exception e
-- | Exceptions that cause LibCSPM to abort whatever it is doing.
data LibCSPMException
-- | An unexpected internal error
Panic :: String -> LibCSPMException
-- | An error in the user's input occured
SourceError :: ErrorMessages -> LibCSPMException
-- | An error occured. Normally this is caught by the application and then
-- turned into a SourceError.
UserError :: LibCSPMException
-- | Throws an arbitrary Exception.
throwException :: Exception e => e -> a
-- | A class to allow catching of SourceErrors in arbitrary monads.
class Monad m => MonadIOException m
tryM :: (MonadIOException m, MonadIOException m) => m a -> m (Either LibCSPMException a)
-- | Given a string causes a Panic to be thrown.
panic :: String -> a
-- | Throw an error message as a SourceError.
throwSourceError :: ErrorMessages -> a
-- | Given a SrcSpan and a pretty printed Doc creates an
-- ErrorMessage.
mkErrorMessage :: SrcSpan -> Doc -> ErrorMessage
-- | Constructs a warning from a SrcSpan and a pretty printed
-- Doc, prepending Warning: to the Doc.
mkWarningMessage :: SrcSpan -> Doc -> ErrorMessage
-- | An error message that resulted from something in the user's input.
data ErrorMessage
ErrorMessage :: SrcSpan -> Doc -> ErrorMessage
-- | Used for sorting into order.
location :: ErrorMessage -> SrcSpan
-- | The message.
message :: ErrorMessage -> Doc
WarningMessage :: SrcSpan -> Doc -> ErrorMessage
-- | Used for sorting into order.
location :: ErrorMessage -> SrcSpan
-- | The message.
message :: ErrorMessage -> Doc
type ErrorMessages = [ErrorMessage]
instance Typeable LibCSPMException
instance MonadIOException m => MonadIOException (StateT s m)
instance MonadIOException IO
instance Exception LibCSPMException
instance Show LibCSPMException
instance Show ErrorMessage
instance PrettyPrintable ErrorMessage
instance PrettyPrintable ErrorMessages
instance Ord ErrorMessage
instance Eq ErrorMessage
module Util.PartialFunctions
type PartialFunction a b = [(a, b)]
functionDomain :: Eq a => PartialFunction a b -> [a]
functionImage :: Eq a => PartialFunction a b -> [b]
identityFunction :: Eq a => [a] -> PartialFunction a a
invert :: (Eq a, Eq b) => PartialFunction a b -> PartialFunction b a
apply :: Eq a => PartialFunction a b -> a -> b
applyRelation :: Eq a => PartialFunction a b -> a -> [b]
safeApply :: Eq a => PartialFunction a b -> a -> Maybe b
composeFunctions :: (Eq a, Eq b) => PartialFunction b c -> PartialFunction a b -> PartialFunction a c
mapPF :: Eq a => PartialFunction a b -> [a] -> [b]
safeMapPF :: Eq a => PartialFunction a b -> [a] -> [b]
updatePF :: Eq a => PartialFunction a b -> a -> b -> PartialFunction a b
removeEntry :: Eq a => PartialFunction a b -> a -> PartialFunction a b
module CSPM.Compiler.Map
type Map k v = PartialFunction k v
lookup :: Eq a => a -> PartialFunction a b -> Maybe b
empty :: [a]
insert :: t -> t1 -> [(t, t1)] -> [(t, t1)]
domain :: Eq a => PartialFunction a b -> [a]
unSafeLookup :: Eq a => a -> PartialFunction a b -> b
toList :: a -> a
fromList :: a -> a
type Relation k v = Map k v
applyRelation :: Eq a => PartialFunction a b -> a -> [b]
instance (Eq k, Eq v) => Eq (Map k v)
module CSPM.Compiler.Events
-- | Events, as represented in the LTS.
data Event
-- | The internal special event tau.
Tau :: Event
-- | The internal event tick, representing termination.
Tick :: Event
-- | Any event defined in a channel definition.
UserEvent :: String -> Event
-- | An alias for ease
type EventSet = Set Event
instance Eq Event
instance Ord Event
instance PrettyPrintable EventSet
instance Show Event
instance PrettyPrintable Event
module Util.HierarchicalMap
data HierarchicalMap a b
HierarchicalMap :: [Map a b] -> HierarchicalMap a b
data HierarchicalMapException a
ValueNotFoundException :: a -> HierarchicalMapException a
-- | Creates/updates a key in the top level map.
update :: Ord a => HierarchicalMap a b -> a -> b -> HierarchicalMap a b
updateMulti :: Ord a => HierarchicalMap a b -> [(a, b)] -> HierarchicalMap a b
-- | Looks up a key in any map, starting from the top
lookup :: (Show k, Typeable k, Ord k) => HierarchicalMap k a -> k -> a
maybeLookup :: (Show k, Typeable k, Ord k) => HierarchicalMap k a -> k -> Maybe a
maybeLookupInTopLayer :: (Show k, Typeable k, Ord k) => HierarchicalMap k a -> k -> Maybe a
popLayer :: Ord a => HierarchicalMap a b -> HierarchicalMap a b
flatten :: Ord a => HierarchicalMap a b -> [(a, b)]
newLayer :: Ord a => HierarchicalMap a b -> HierarchicalMap a b
newLayerAndBind :: Ord a => HierarchicalMap a b -> [(a, b)] -> HierarchicalMap a b
newRecursiveLayerAndBind :: Ord a => HierarchicalMap a b -> [HierarchicalMap a b -> (a, b)] -> HierarchicalMap a b
-- | Creates a new map
new :: Ord a => HierarchicalMap a b
instance Typeable1 HierarchicalMapException
instance (Show a, Show b) => Show (HierarchicalMap a b)
instance Show a => Show (HierarchicalMapException a)
instance (Ord a, Show a, Typeable a) => Exception (HierarchicalMapException a)
module Util.Annotated
data SrcLoc
SrcLoc :: String -> !Int -> !Int -> SrcLoc
srcLocFile :: SrcLoc -> String
srcLocLine :: SrcLoc -> !Int
srcLocCol :: SrcLoc -> !Int
NoLoc :: SrcLoc
data SrcSpan
SrcSpanOneLine :: String -> !Int -> !Int -> !Int -> SrcSpan
srcSpanFile :: SrcSpan -> String
srcSpanLine :: SrcSpan -> !Int
srcSpanSCol :: SrcSpan -> !Int
srcSpanECol :: SrcSpan -> !Int
SrcSpanMultiLine :: String -> !Int -> !Int -> !Int -> !Int -> SrcSpan
srcSpanFile :: SrcSpan -> String
srcSpanSLine :: SrcSpan -> !Int
srcSpanSCol :: SrcSpan -> !Int
srcSpanELine :: SrcSpan -> !Int
srcSpanECol :: SrcSpan -> !Int
SrcSpanPoint :: String -> !Int -> !Int -> SrcSpan
srcSpanFile :: SrcSpan -> String
srcSpanLine :: SrcSpan -> !Int
srcSpanCol :: SrcSpan -> !Int
Unknown :: SrcSpan
srcSpanStart :: SrcSpan -> SrcLoc
srcSpanEnd :: SrcSpan -> SrcLoc
combineSpans :: SrcSpan -> SrcSpan -> SrcSpan
data Located a
L :: SrcSpan -> a -> Located a
locatedLoc :: Located a -> SrcSpan
locatedInner :: Located a -> a
data Annotated a b
An :: SrcSpan -> a -> b -> Annotated a b
loc :: Annotated a b -> SrcSpan
annotation :: Annotated a b -> a
inner :: Annotated a b -> b
dummyAnnotation :: a
unAnnotate :: Annotated a b -> b
instance Eq SrcLoc
instance Eq SrcSpan
instance Eq a => Eq (Located a)
instance Eq b => Eq (Annotated a b)
instance PrettyPrintable a => PrettyPrintable (Located a)
instance PrettyPrintable b => PrettyPrintable (Annotated a b)
instance PrettyPrintable [b] => PrettyPrintable [Annotated a b]
instance Show a => Show (Located a)
instance Show b => Show (Annotated a b)
instance PrettyPrintable SrcSpan
instance Show SrcSpan
instance Ord SrcSpan
instance Ord SrcLoc
-- | Names used by the evaluator. This is heavily inspired by GHC.
module CSPM.DataStructures.Names
-- | A name that occurs in the source code somewhere.
data OccName
OccName :: String -> OccName
-- | A name that has not yet been renamed. Created by the parser.
data UnRenamedName
UnQual :: OccName -> UnRenamedName
-- | A renamed name and is the exclusive type used after the renamer. Names
-- are guaranteed to be unique, meaning that two names are equal iff they
-- refer to the same binding instance. For example, consider the
-- following CSPM code:
--
--
-- f = 1
-- g = let f = 2 within (f, f)
--
--
-- This will be renamed to:
--
--
-- f0 = 1
-- g = let f1 = 2 within (f1, f1)
--
data Name
Name :: NameType -> !OccName -> !SrcSpan -> !Int -> Bool -> Name
-- | The type of this name.
nameType :: Name -> NameType
-- | The original occurence of this name (used for error messages).
nameOccurrence :: Name -> !OccName
-- | Where this name was defined. If this occurs in a pattern, then it will
-- be equal to the location of the pattern, otherwise it will be equal to
-- the location of the definition that this name binds to.
nameDefinition :: Name -> !SrcSpan
-- | The unique identifier for this name. Inserted by the renamer.
nameUnique :: Name -> !Int
-- | Is this name a type constructor, i.e. a datatype or a channel?
nameIsConstructor :: Name -> Bool
data NameType
-- | An externally visible name (like a top level definition).
ExternalName :: NameType
-- | A name created by the renamer, but from the users' source (e.g. from a
-- lambda).
InternalName :: NameType
-- | A built in name.
WiredInName :: NameType
mkExternalName :: MonadIO m => OccName -> SrcSpan -> Bool -> m Name
mkInternalName :: MonadIO m => OccName -> SrcSpan -> m Name
mkWiredInName :: MonadIO m => OccName -> Bool -> m Name
mkFreshInternalName :: MonadIO m => m Name
-- | Does the given Name correspond to a data type or a channel definition.
isNameDataConstructor :: Name -> Bool
instance Typeable OccName
instance Typeable UnRenamedName
instance Typeable Name
instance Eq OccName
instance Ord OccName
instance Show OccName
instance Eq UnRenamedName
instance Ord UnRenamedName
instance Show UnRenamedName
instance Eq NameType
instance Show Name
instance PrettyPrintable Name
instance Ord Name
instance Eq Name
instance PrettyPrintable UnRenamedName
instance PrettyPrintable OccName
module CSPM.DataStructures.Types
data TypeVar
data TypeScheme
ForAll :: [(TypeVar, [Constraint])] -> Type -> TypeScheme
data Constraint
Eq :: Constraint
Ord :: Constraint
Inputable :: Constraint
data Type
TVar :: TypeVarRef -> Type
TProc :: Type
TInt :: Type
TBool :: Type
TEvent :: Type
TEventable :: Type
TSet :: Type -> Type
TSeq :: Type -> Type
TDot :: Type -> Type -> Type
TTuple :: [Type] -> Type
TFunction :: [Type] -> Type -> Type
TDotable :: Type -> Type -> Type
TDatatype :: Name -> Type
data TypeVarRef
TypeVarRef :: TypeVar -> [Constraint] -> PType -> TypeVarRef
-- | Pretty prints several types using the same variable substitutions
prettyPrintTypes :: [Type] -> [Doc]
freshTypeVar :: MonadIO m => m Type
freshTypeVarWithConstraints :: MonadIO m => [Constraint] -> m Type
type SymbolTable = PartialFunction Name TypeScheme
type PSymbolTable = IORef SymbolTable
freshPSymbolTable :: MonadIO m => m PSymbolTable
readPSymbolTable :: MonadIO m => PSymbolTable -> m SymbolTable
setPSymbolTable :: MonadIO m => PSymbolTable -> SymbolTable -> m ()
type PType = IORef (Maybe Type)
freshPType :: MonadIO m => m PType
readPType :: MonadIO m => PType -> m (Maybe Type)
setPType :: MonadIO m => PType -> Type -> m ()
instance Eq TypeVar
instance Show TypeVar
instance Eq Constraint
instance Ord Constraint
instance Show Constraint
instance Eq Type
instance Show Type
instance Eq TypeScheme
instance Show TypeScheme
instance PrettyPrintable TypeScheme
instance PrettyPrintable Type
instance PrettyPrintable Constraint
instance Show TypeVarRef
instance Eq TypeVarRef
-- | 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.
module CSPM.DataStructures.Syntax
data Module id
GlobalModule :: [AnDecl id] -> Module id
data Decl id
-- | A function binding, e.g. func(x,y)(z) = 0.
FunBind :: id -> [AnMatch id] -> Decl id
-- | The binding of a pattern to an expression, e.g. (p,q) = e.
PatBind :: (AnPat id) -> (AnExp id) -> Decl id
-- | An assertion in a file, e.g. assert P [T= Q.
Assert :: (Assertion id) -> Decl id
-- | An import of an external function, e.g. external test,
External :: [id] -> Decl id
externalImportedNames :: Decl id -> [id]
-- | An import of a transparent function, e.g. transparent normal.
Transparent :: [id] -> Decl id
transparentImportedNames :: Decl id -> [id]
-- | A channel declaration, e.g. channel c, d : {0..1}.{0..1}.
Channel :: [id] -> (Maybe (AnExp id)) -> Decl id
-- | A datatype declaration, e.g. datatype T = Clause1 | Clause2.
DataType :: id -> [AnDataTypeClause id] -> Decl id
-- | A nametype declaration, e.g. nametype T2 = T.T.
NameType :: id -> (AnExp id) -> Decl id
-- | 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.
data Match id
Match :: [[AnPat id]] -> AnExp id -> Match id
-- | The patterns that need to be matched. This is a list of lists as
-- functions may be curried, like f(x,y)(z) = ....
matchPatterns :: Match id -> [[AnPat id]]
-- | The expression to be evaluated if the match succeeds.
matchRightHandSide :: Match id -> AnExp id
data Assertion id
-- | A refinement assertion, e.g. assert P [F= Q.
Refinement :: AnExp id -> Model -> AnExp id -> [ModelOption id] -> Assertion id
refinementSpecification :: Assertion id -> AnExp id
refinementModel :: Assertion id -> Model
refinementImplementation :: Assertion id -> AnExp id
refinementModelOptions :: Assertion id -> [ModelOption id]
-- | A check of property, like deadlock freedom, e.g. assert P
-- :[deadlock free [F]].
PropertyCheck :: AnExp id -> SemanticProperty -> Maybe Model -> Assertion id
propertyCheckProcess :: Assertion id -> AnExp id
propertyCheckProperty :: Assertion id -> SemanticProperty
propertyCheckModel :: Assertion id -> Maybe Model
-- | A boolean assertion, not currently supported.
BoolAssertion :: (AnExp id) -> Assertion id
-- | The negation of an assertion, not currently supported.
ASNot :: (Assertion id) -> Assertion id
data Model
Traces :: Model
Failures :: Model
FailuresDivergences :: Model
Refusals :: Model
RefusalsDivergences :: Model
Revivals :: Model
RevivalsDivergences :: Model
data ModelOption id
TauPriority :: (AnExp id) -> ModelOption id
data SemanticProperty
DeadlockFreedom :: SemanticProperty
Deterministic :: SemanticProperty
LivelockFreedom :: SemanticProperty
-- | 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).
data DataTypeClause id
DataTypeClause :: id -> Maybe (AnExp id) -> DataTypeClause id
-- | The name of the datatype clause.
dataTypeClauseName :: DataTypeClause id -> 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.
dataTypeClauseTypeExpression :: DataTypeClause id -> Maybe (AnExp id)
-- | An expression.
data Exp id
-- | Function application.
App :: AnExp id -> [AnExp id] -> Exp id
-- | The function.
appFunction :: Exp id -> AnExp id
-- | The arguments applied to the function
appArguments :: Exp id -> [AnExp id]
-- | Application of a binary boolean operator.
BooleanBinaryOp :: BinaryBooleanOp -> AnExp id -> AnExp id -> Exp id
booleanBinaryOpOperator :: Exp id -> BinaryBooleanOp
booleanBinaryOpLeftExpression :: Exp id -> AnExp id
booleanBinaryOpRightExpression :: Exp id -> AnExp id
-- | Application of a unary boolean operator.
BooleanUnaryOp :: UnaryBooleanOp -> AnExp id -> Exp id
unaryBooleanOpOperator :: Exp id -> UnaryBooleanOp
unaryBooleanExpression :: Exp id -> AnExp id
-- | List concatenation, e.g. x^y.
Concat :: AnExp id -> AnExp id -> Exp id
concatLeftList :: Exp id -> AnExp id
concatRightList :: Exp id -> AnExp id
-- | Dot operator application, e.g. c.x.
DotApp :: AnExp id -> AnExp id -> Exp id
dotAppLeftArgument :: Exp id -> AnExp id
dotAppRighArgument :: Exp id -> AnExp id
-- | If statements, e.g. if cond then e1 else e2.
If :: AnExp id -> AnExp id -> AnExp id -> Exp id
-- | The condition of the if.
ifCondition :: Exp id -> AnExp id
-- | The then branch.
ifThenBranch :: Exp id -> AnExp id
ifElseBranch :: Exp id -> AnExp id
-- | Lambda functions, e.g. (x,y) @ e(x,y).
Lambda :: AnPat id -> AnExp id -> Exp id
lambdaBindingPattern :: Exp id -> AnPat id
lambdaRightHandSide :: Exp id -> AnExp id
-- | Let declarations, e.g. let func = e1 within e2.
Let :: [AnDecl id] -> AnExp id -> Exp id
letDeclarations :: Exp id -> [AnDecl id]
letExpression :: Exp id -> AnExp id
-- | Literals, e.g. true or 1.
Lit :: Literal -> Exp id
litLiteral :: Exp id -> Literal
-- | List literals, e.g. 1,2,3.
List :: [AnExp id] -> Exp id
listItems :: Exp id -> [AnExp id]
-- | List comprehensions, e.g. x,y | (x,y) <- e.
ListComp :: [AnExp id] -> [AnStmt id] -> Exp id
listCompItems :: Exp id -> [AnExp id]
listCompStatements :: Exp id -> [AnStmt id]
-- | Infinite list of integers from the given value, e.g.
-- 1...
ListEnumFrom :: AnExp id -> Exp id
listEnumFromLowerBound :: Exp id -> AnExp id
-- | Bounded list of integers between the given values, e.g.
-- 1..3.
ListEnumFromTo :: AnExp id -> AnExp id -> Exp id
listEnumFromToLowerBound :: Exp id -> AnExp id
listEnumFromToUpperBound :: Exp id -> AnExp id
-- | The length of the list, e.g. #list.
ListLength :: AnExp id -> Exp id
listLengthExpression :: Exp id -> AnExp id
-- | Application of binary maths operator, e.g. x+y.
MathsBinaryOp :: BinaryMathsOp -> AnExp id -> AnExp id -> Exp id
mathsBinaryOpOperator :: Exp id -> BinaryMathsOp
mathsBinaryOpLeftExpression :: Exp id -> AnExp id
mathsBinaryOpRightExpression :: Exp id -> AnExp id
-- | Application of unary maths operator, e.g. -x.
MathsUnaryOp :: UnaryMathsOp -> AnExp id -> Exp id
mathsUnaryOpOperator :: Exp id -> UnaryMathsOp
mathsUnaryOpExpression :: Exp id -> AnExp id
-- | A user provided bracket, e.g. (e).
Paren :: AnExp id -> Exp id
parenExpression :: Exp id -> AnExp id
-- | Set literals, e.g. {1,2,3}.
Set :: [AnExp id] -> Exp id
setItems :: Exp id -> [AnExp id]
-- | Set comprehensions, e.g. {x,y | (x,y) <- e}.
SetComp :: [AnExp id] -> [AnStmt id] -> Exp id
setCompItems :: Exp id -> [AnExp id]
setCompStatements :: Exp id -> [AnStmt id]
-- | Enumerated Sets, i.e. sets that complete the events, e.g. {| c.x
-- |}.
SetEnum :: [AnExp id] -> Exp id
setEnumItems :: Exp id -> [AnExp id]
-- | Set comprehension version of SetEnum, e.g. {| c.x | x <-
-- xs |}.
SetEnumComp :: [AnExp id] -> [AnStmt id] -> Exp id
setEnumCompItems :: Exp id -> [AnExp id]
setEnumCompStatements :: Exp id -> [AnStmt id]
-- | The infinite set of integers from the given value, e.g.
-- {5..}.
SetEnumFrom :: AnExp id -> Exp id
setEnumFromLowerBound :: Exp id -> AnExp id
-- | The bounded set of integers between the two given values, e.g.
-- {5..6}.
SetEnumFromTo :: AnExp id -> AnExp id -> Exp id
-- | The lower bound.
setEnumFromToLowerBound :: Exp id -> AnExp id
-- | The upper bound.
setEnumFromToUpperBound :: Exp id -> AnExp id
-- | Tuples, e.g. (1,2).
Tuple :: [AnExp id] -> Exp id
tupleItems :: Exp id -> [AnExp id]
-- | Variables, e.g. x.
Var :: id -> Exp id
varIdentity :: Exp id -> id
-- | Alphabetised parallel, e.g. P [A || B] Q.
AlphaParallel :: AnExp id -> AnExp id -> AnExp id -> AnExp id -> Exp id
-- | Process 1.
alphaParLeftProcess :: Exp id -> AnExp id
-- | Alphabet of process 1.
alphaParAlphabetLeftProcess :: Exp id -> AnExp id
-- | Alphabet of process 2.
alphaParAlphabetRightProcess :: Exp id -> AnExp id
-- | Process 2.
alphaParRightProcess :: Exp id -> AnExp id
-- | Exception operator, e.g. P [| A |> Q.
Exception :: AnExp id -> AnExp id -> AnExp id -> Exp id
exceptionLeftProcess :: Exp id -> AnExp id
exceptionAlphabet :: Exp id -> AnExp id
exceptionRightProcess :: Exp id -> AnExp id
-- | External choice, e.g. P [] Q.
ExternalChoice :: AnExp id -> AnExp id -> Exp id
extChoiceLeftProcess :: Exp id -> AnExp id
extChoiceRightOperator :: Exp id -> AnExp id
-- | Generalised parallel, e.g. P [| A |] Q.
GenParallel :: AnExp id -> AnExp id -> AnExp id -> Exp id
genParallelLeftProcess :: Exp id -> AnExp id
genParallelAlphabet :: Exp id -> AnExp id
genParallelRightProcess :: Exp id -> AnExp id
-- | Guarded expressions, e.g. b & P where b is a
-- boolean expression. This is equivalent to if b then P else
-- STOP.
GuardedExp :: AnExp id -> AnExp id -> Exp id
guardedExpCondition :: Exp id -> AnExp id
guardedExpProcess :: Exp id -> AnExp id
-- | Hiding of events, e.g. P A.
Hiding :: AnExp id -> AnExp id -> Exp id
-- | The process the hiding is applied to.
hidingProcess :: Exp id -> AnExp id
-- | The set of events to be hidden.
hidingAlphabet :: Exp id -> AnExp id
-- | Internal choice, e.g. P |~| Q.
InternalChoice :: AnExp id -> AnExp id -> Exp id
intChoiceLeftProcess :: Exp id -> AnExp id
intChoiceRightProcess :: Exp id -> AnExp id
-- | Interrupt (where the left process is turned off once the right process
-- performs an event), e.g. P / Q.
Interrupt :: AnExp id -> AnExp id -> Exp id
interruptLeftProcess :: Exp id -> AnExp id
interruptRightProcess :: Exp id -> AnExp id
-- | Interleaving of processes, e.g. P ||| Q.
Interleave :: AnExp id -> AnExp id -> Exp id
interleaveLeftProcess :: Exp id -> AnExp id
interleaveRightProcess :: Exp id -> AnExp id
LinkParallel :: AnExp id -> [(AnExp id, AnExp id)] -> [AnStmt id] -> AnExp id -> Exp id
linkParLeftProcess :: Exp id -> AnExp id
linkParTiedEvents :: Exp id -> [(AnExp id, AnExp id)]
linkParTieStatements :: Exp id -> [AnStmt id]
linkParRightProcess :: Exp id -> AnExp id
-- | Event prefixing, e.g. c$x?y!z -> P.
Prefix :: AnExp id -> [AnField id] -> AnExp id -> Exp id
prefixChannel :: Exp id -> AnExp id
prefixFields :: Exp id -> [AnField id]
prefixProcess :: Exp id -> AnExp id
-- | Event renaming, e.g. P [[ a.x <- b.x | x <- X ]].
Rename :: AnExp id -> [(AnExp id, AnExp id)] -> [AnStmt id] -> Exp id
-- | The process that is renamed.
renameProcess :: Exp id -> AnExp id
-- | The events that are renamed, in the format of (old, new).
renameTiedEvents :: Exp id -> [(AnExp id, AnExp id)]
-- | The statements for the ties.
renameTieStatements :: Exp id -> [AnStmt id]
-- | Sequential composition, e.g. P; Q.
SequentialComp :: AnExp id -> AnExp id -> Exp id
seqCompLeftProcess :: Exp id -> AnExp id
seqCompRightProcess :: Exp id -> AnExp id
-- | Sliding choice, e.g. P |> Q.
SlidingChoice :: AnExp id -> AnExp id -> Exp id
slidingChoiceLeftProcess :: Exp id -> AnExp id
slidingChoiceRightProcess :: Exp id -> AnExp id
-- | Replicated alphabetised parallel, e.g. || x : X @ [| A(x) |]
-- P(x).
ReplicatedAlphaParallel :: [AnStmt id] -> AnExp id -> AnExp id -> Exp id
repAlphaParReplicatedStatements :: Exp id -> [AnStmt id]
repAlphaParAlphabet :: Exp id -> AnExp id
repAlphaParProcess :: Exp id -> AnExp id
-- | Replicated external choice, e.g. [] x : X @ P(x).
ReplicatedExternalChoice :: [AnStmt id] -> AnExp id -> Exp id
repExtChoiceReplicatedStatements :: Exp id -> [AnStmt id]
repExtChoiceProcess :: Exp id -> AnExp id
-- | Replicated interleave, e.g. ||| x : X @ P(x).
ReplicatedInterleave :: [AnStmt id] -> AnExp id -> Exp id
repInterleaveReplicatedStatements :: Exp id -> [AnStmt id]
repInterleaveProcess :: Exp id -> AnExp id
-- | Replicated internal choice, e.g. |~| x : X @ P(x).
ReplicatedInternalChoice :: [AnStmt id] -> AnExp id -> Exp id
repIntChoiceReplicatedStatements :: Exp id -> [AnStmt id]
repIntChoiceProcess :: Exp id -> AnExp id
-- | Replicated link parallel, e.g. [a.x <- b.x | x <- X(y)] y :
-- Y @ P(y).
ReplicatedLinkParallel :: [(AnExp id, AnExp id)] -> [AnStmt id] -> [AnStmt id] -> AnExp id -> Exp id
-- | The tied events.
repLinkParTiedChannels :: Exp id -> [(AnExp id, AnExp id)]
-- | The statements for the ties.
repLinkParTieStatements :: Exp id -> [AnStmt id]
-- | The Stmts - the process (and ties) are evaluated once for each
-- value generated by these.
repLinkParReplicatedStatements :: Exp id -> [AnStmt id]
-- | The process
repLinkParProcess :: Exp id -> AnExp id
-- | Replicated parallel, e.g. [| A |] x : X @ P(x).
ReplicatedParallel :: AnExp id -> [AnStmt id] -> AnExp id -> Exp id
repParAlphabet :: Exp id -> AnExp id
repParReplicatedStatements :: Exp id -> [AnStmt id]
repParProcess :: Exp id -> AnExp id
-- | Used only for parsing - never appears in an AST.
ExpPatWildCard :: Exp id
-- | Used only for parsing - never appears in an AST.
ExpPatDoublePattern :: (AnExp id) -> (AnExp id) -> Exp id
data BinaryMathsOp
Divide :: BinaryMathsOp
Minus :: BinaryMathsOp
Mod :: BinaryMathsOp
Plus :: BinaryMathsOp
Times :: BinaryMathsOp
data BinaryBooleanOp
And :: BinaryBooleanOp
Or :: BinaryBooleanOp
Equals :: BinaryBooleanOp
NotEquals :: BinaryBooleanOp
LessThan :: BinaryBooleanOp
GreaterThan :: BinaryBooleanOp
LessThanEq :: BinaryBooleanOp
GreaterThanEq :: BinaryBooleanOp
data UnaryMathsOp
Negate :: UnaryMathsOp
data UnaryBooleanOp
Not :: UnaryBooleanOp
data Field id
-- |
-- !x
--
Output :: (AnExp id) -> Field id
-- |
-- ?x:A
--
Input :: (AnPat id) -> (Maybe (AnExp id)) -> Field id
-- | $x:A (see P395 UCS)
NonDetInput :: (AnPat id) -> (Maybe (AnExp id)) -> Field id
data Stmt id
Generator :: (AnPat id) -> (AnExp id) -> Stmt id
Qualifier :: (AnExp id) -> Stmt id
data Pat id
-- | The concatenation of two patterns, e.g. p1^p2.
PConcat :: AnPat id -> AnPat id -> Pat id
pConcatLeftPat :: Pat id -> AnPat id
pConcatRightPat :: Pat id -> AnPat id
-- | The dot of two patterns, e.g. p1.p2.
PDotApp :: AnPat id -> AnPat id -> Pat id
pDotLeftPat :: Pat id -> AnPat id
pDotRightPat :: Pat id -> AnPat id
-- | A double pattern match, e.g. p1@@p2.
PDoublePattern :: AnPat id -> AnPat id -> Pat id
pDoublePatLeftPat :: Pat id -> AnPat id
pDoublePatRightPat :: Pat id -> AnPat id
-- | A literal pattern list, e.g. p1,p2,p3.
PList :: [AnPat id] -> Pat id
pListItems :: Pat id -> [AnPat id]
-- | A literal pattern, e.g. true, or 0.
PLit :: Literal -> Pat id
pLitLiteral :: Pat id -> Literal
-- | A user supplied parenthesis in a pattern.
PParen :: AnPat id -> Pat id
pParenPattern :: Pat id -> AnPat id
-- | 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.
PSet :: [AnPat id] -> Pat id
pSetItems :: Pat id -> [AnPat id]
-- | A tuple pattern, e.g. (p1,p2,p3).
PTuple :: [AnPat id] -> Pat id
pTupleItems :: Pat id -> [AnPat id]
-- | 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.
PVar :: id -> Pat id
pVarIdentity :: Pat id -> id
-- | Matches anything but does not bind it.
PWildCard :: Pat id
-- | 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).
PCompList :: [AnPat id] -> Maybe (AnPat id, [AnPat id]) -> Pat id -> Pat id
pListStartItems :: Pat id -> [AnPat id]
pListMiddleEndItems :: Pat id -> Maybe (AnPat id, [AnPat id])
pListOriginalPattern :: Pat id -> Pat id
-- | Like with a PCompList we flatten nested dot patterns to make it
-- easier to evaluate.
PCompDot :: [AnPat id] -> Pat id -> Pat id
pDotItems :: Pat id -> [AnPat id]
pDotOriginalpattern :: Pat id -> Pat id
-- | A statement in an interactive session.
data InteractiveStmt id
Evaluate :: (AnExp id) -> InteractiveStmt id
Bind :: (AnDecl id) -> InteractiveStmt id
RunAssertion :: (Assertion id) -> InteractiveStmt id
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)
type PModule = AnModule UnRenamedName
type PDecl = AnDecl UnRenamedName
type PMatch = AnMatch UnRenamedName
type PPat = AnPat UnRenamedName
type PExp = AnExp UnRenamedName
type PField = AnField UnRenamedName
type PStmt = AnStmt 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
getType :: Annotated (Maybe Type, PType) a -> Type
getSymbolTable :: Annotated (Maybe SymbolTable, PSymbolTable) a -> SymbolTable
instance Eq BinaryBooleanOp
instance Show BinaryBooleanOp
instance Eq UnaryBooleanOp
instance Show UnaryBooleanOp
instance Eq UnaryMathsOp
instance Show UnaryMathsOp
instance Eq BinaryMathsOp
instance Show BinaryMathsOp
instance Eq Model
instance Show Model
instance Eq SemanticProperty
instance Show SemanticProperty
instance Eq id => Eq (Pat id)
instance Show id => Show (Pat id)
instance Eq id => Eq (Exp id)
instance Show id => Show (Exp id)
instance Eq id => Eq (Stmt id)
instance Show id => Show (Stmt id)
instance Eq id => Eq (Field id)
instance Show id => Show (Field id)
instance Eq id => Eq (Decl id)
instance Show id => Show (Decl id)
instance Eq id => Eq (Assertion id)
instance Show id => Show (Assertion id)
instance Eq id => Eq (ModelOption id)
instance Show id => Show (ModelOption id)
instance Eq id => Eq (DataTypeClause id)
instance Show id => Show (DataTypeClause id)
instance Eq id => Eq (Match id)
instance Show id => Show (Match id)
instance Eq id => Eq (Module id)
instance Show id => Show (Module id)
instance Show id => Show (InteractiveStmt id)
-- | This module provides the input data structure to the compiler.
module CSPM.Compiler.Processes
-- | A compiled process. Note this is an infinite data structure (due to
-- PProcCall) as this makes compilation easy (we can easily chase
-- dependencies).
data Proc
PAlphaParallel :: [(Set Event, Proc)] -> Proc
PException :: Proc -> (Set Event) -> Proc -> Proc
PExternalChoice :: [Proc] -> Proc
PGenParallel :: (Set Event) -> [Proc] -> Proc
PHide :: Proc -> (Set Event) -> Proc
PInternalChoice :: [Proc] -> Proc
PInterrupt :: Proc -> Proc -> Proc
PInterleave :: [Proc] -> Proc
PLinkParallel :: Proc -> (Map Event Event) -> Proc -> Proc
POperator :: ProcOperator -> Proc -> Proc
PPrefix :: Event -> Proc -> Proc
PRename :: (Relation Event Event) -> Proc -> Proc
PSequentialComp :: Proc -> Proc -> Proc
PSlidingChoice :: Proc -> Proc -> Proc
-- | Labels the process this contains. This allows infinite loops to be
-- spotted.
PProcCall :: ProcName -> Proc -> Proc
-- | An operator that can be applied to processes.
data ProcOperator
Chase :: ProcOperator
Diamond :: ProcOperator
Explicate :: ProcOperator
Normalize :: ProcOperator
ModelCompress :: ProcOperator
StrongBisim :: ProcOperator
TauLoopFactor :: ProcOperator
WeakBisim :: ProcOperator
-- | ProcNames uniquely identify processes.
data ProcName
ProcName :: Name -> [[Value]] -> ProcName
-- | The name of this process (recal Name s are unique).
name :: ProcName -> Name
-- | The arguments applied to this process, in case it was a function call.
arguments :: ProcName -> [[Value]]
-- | Pretty prints the given process and all processes that it depends
-- upon.
prettyPrintAllRequiredProcesses :: Proc -> Doc
instance Eq ProcOperator
instance Show Proc
instance PrettyPrintable Proc
instance Show ProcOperator
instance PrettyPrintable ProcOperator
instance Show ProcName
instance PrettyPrintable ProcName
instance Eq ProcName
module CSPM.PrettyPrinter
prettyPrint :: PrettyPrintable a => a -> Doc
prettyPrintMatch :: PrettyPrintable id => id -> AnMatch id -> Doc
instance PrettyPrintable id => PrettyPrintable (Stmt id)
instance PrettyPrintable id => PrettyPrintable (Field id)
instance PrettyPrintable id => PrettyPrintable (Exp id)
instance PrettyPrintable UnaryMathsOp
instance PrettyPrintable BinaryMathsOp
instance PrettyPrintable UnaryBooleanOp
instance PrettyPrintable BinaryBooleanOp
instance PrettyPrintable id => PrettyPrintable (Pat id)
instance PrettyPrintable id => PrettyPrintable (DataTypeClause id)
instance PrettyPrintable SemanticProperty
instance PrettyPrintable id => PrettyPrintable (ModelOption id)
instance PrettyPrintable Model
instance PrettyPrintable id => PrettyPrintable (Assertion id)
instance PrettyPrintable id => PrettyPrintable (Decl id)
instance PrettyPrintable id => PrettyPrintable (InteractiveStmt id)
instance PrettyPrintable id => PrettyPrintable (Module id)
instance PrettyPrintable id => PrettyPrintable [Module id]
module CSPM.Desugar
class Desugarable a
desugar :: Desugarable a => a -> a
desugarWithType :: Desugarable a => a -> Type -> a
instance Desugarable Literal
instance Desugarable (Pat Name)
instance Desugarable (InteractiveStmt Name)
instance Desugarable (Stmt Name)
instance Desugarable (Field Name)
instance Desugarable (Exp Name)
instance Desugarable (Match Name)
instance Desugarable (DataTypeClause Name)
instance Desugarable (ModelOption Name)
instance Desugarable (Assertion Name)
instance Desugarable (Decl Name)
instance Desugarable (Module Name)
instance (Desugarable a, Desugarable b) => Desugarable (a, b)
instance Desugarable a => Desugarable (Annotated b a)
instance Desugarable a => Desugarable (Annotated Type a)
instance Desugarable a => Desugarable (Maybe a)
instance Desugarable a => Desugarable [a]
module CSPM.DataStructures.Tokens
data Token
TInteger :: Int -> Token
TFalse :: Token
TTrue :: Token
TIdent :: String -> Token
TRefines :: Model -> Token
TModel :: Model -> Token
TTauPriority :: Token
TDeadlockFree :: Token
TDivergenceFree :: Token
TLivelockFree :: Token
TDeterministic :: Token
TNewLine :: Token
TDefineEqual :: Token
TComma :: Token
TDot :: Token
TExclamationMark :: Token
TQuestionMark :: Token
TDollar :: Token
TPipe :: Token
TDoubleDot :: Token
TColon :: Token
TDrawnFrom :: Token
TTie :: Token
TDoubleAt :: Token
TWildCard :: Token
TIf :: Token
TThen :: Token
TElse :: Token
TLet :: Token
TWithin :: Token
TBackSlash :: Token
TLambdaDot :: Token
TChannel :: Token
TAssert :: Token
TDataType :: Token
TExternal :: Token
TTransparent :: Token
TNameType :: Token
TSemiColon :: Token
TGuard :: Token
TNot :: Token
TAnd :: Token
TOr :: Token
TEq :: Token
TNotEq :: Token
TLtEq :: Token
TGtEq :: Token
TLt :: Token
TGt :: Token
TPlus :: Token
TMinus :: Token
TTimes :: Token
TDivide :: Token
TMod :: Token
TCloseSeq :: Token
TEmptySeq :: Token
TConcat :: Token
THash :: Token
TLParen :: Token
TRParen :: Token
TLBrace :: Token
TRBrace :: Token
TLPipeBrace :: Token
TRPipeBrace :: Token
TLDoubleSqBracket :: Token
TRDoubleSqBracket :: Token
TLPipeSqBracket :: Token
TRPipeSqBracket :: Token
TLSqBracket :: Token
TRSqBracket :: Token
TExtChoice :: Token
TIntChoice :: Token
TInterleave :: Token
TPrefix :: Token
TInterrupt :: Token
TSlidingChoice :: Token
TRException :: Token
TParallel :: Token
TEOF :: Token
type LToken = Located Token
data Model
Traces :: Model
Failures :: Model
FailuresDivergences :: Model
Refusals :: Model
RefusalsDivergences :: Model
Revivals :: Model
RevivalsDivergences :: Model
instance Eq Token
instance PrettyPrintable Token
instance Show Token
module CSPM.Parser.Exceptions
invalidPatternErrorMessage :: PExp -> ErrorMessage
invalidDeclarationErrorMessage :: PDecl -> ErrorMessage
invalidExpressionErrorMessage :: PExp -> ErrorMessage
invalidIncludeErrorMessage :: SrcSpan -> ErrorMessage
lexicalErrorMessage :: SrcSpan -> ErrorMessage
parseErrorMessage :: LToken -> ErrorMessage
fileAccessErrorMessage :: FilePath -> ErrorMessage
-- | Throw an error message as a SourceError.
throwSourceError :: ErrorMessages -> a
module CSPM.Parser.Monad
type ParseMonad = StateT ParserState IO
data ParserState
ParserState :: !String -> ![FileParserState] -> ParserState
rootDir :: ParserState -> !String
fileStack :: ParserState -> ![FileParserState]
data FileParserState
FileParserState :: !FilePosition -> !String -> String -> !Char -> !Int -> ![Int] -> FileParserState
tokenizerPos :: FileParserState -> !FilePosition
fileName :: FileParserState -> !String
input :: FileParserState -> String
previousChar :: FileParserState -> !Char
currentStartCode :: FileParserState -> !Int
sequenceStack :: FileParserState -> ![Int]
movePos :: FilePosition -> Char -> FilePosition
setParserState :: ParserState -> ParseMonad ()
getParserState :: ParseMonad ParserState
data FilePosition
FilePosition :: !Int -> !Int -> !Int -> FilePosition
filePositionToSrcLoc :: String -> FilePosition -> SrcSpan
modifyTopFileParserState :: (FileParserState -> FileParserState) -> ParseMonad ()
getTopFileParserState :: ParseMonad FileParserState
runParser :: ParseMonad a -> String -> IO a
pushFile :: String -> ParseMonad a -> ParseMonad a
pushFileContents :: String -> String -> ParseMonad ()
getTokenizerPos :: ParseMonad FilePosition
getFileName :: ParseMonad String
getInput :: ParseMonad String
getPreviousChar :: ParseMonad Char
getCurrentStartCode :: ParseMonad Int
setCurrentStartCode :: Int -> ParseMonad ()
getSequenceStack :: ParseMonad [Int]
setSequenceStack :: [Int] -> ParseMonad ()
instance Eq FilePosition
instance Show FilePosition
instance Show FileParserState
instance Show ParserState
module CSPM.Parser.Lexer
alex_base :: AlexAddr
alex_table :: AlexAddr
alex_check :: AlexAddr
alex_deflt :: AlexAddr
data AlexReturn a
AlexEOF :: AlexReturn a
AlexError :: !AlexInput -> AlexReturn a
AlexSkip :: !AlexInput -> !Int -> AlexReturn a
AlexToken :: !AlexInput -> !Int -> a -> AlexReturn a
data AlexLastAcc a
AlexNone :: AlexLastAcc a
AlexLastAcc :: a -> !AlexInput -> !Int -> AlexLastAcc a
AlexLastSkip :: !AlexInput -> !Int -> AlexLastAcc a
data AlexAcc a user
AlexAcc :: a -> AlexAcc a user
AlexAccSkip :: AlexAcc a user
AlexAccPred :: a -> (AlexAccPred user) -> AlexAcc a user
AlexAccSkipPred :: (AlexAccPred user) -> AlexAcc a user
type AlexAccPred user = user -> AlexInput -> Int -> AlexInput -> Bool
wschars :: String
strip :: String -> String
-- | Same as strip, but applies only to the left side of the string.
lstrip :: String -> String
-- | Same as strip, but applies only to the right side of the
-- string.
rstrip :: String -> String
gt :: AlexInput -> Int -> ParseMonad LToken
soakTok :: Token -> AlexInput -> Int -> ParseMonad LToken
tok :: Token -> AlexInput -> Int -> ParseMonad LToken
stok :: (String -> Token) -> AlexInput -> Int -> ParseMonad LToken
takeChars :: Int -> [FileParserState] -> String
nestedComment :: AlexInput -> Int -> ParseMonad LToken
switchInput :: AlexInput -> Int -> ParseMonad LToken
type AlexInput = ParserState
begin :: Int -> AlexInput -> Int -> ParseMonad LToken
alexInputPrevChar :: AlexInput -> Char
alexGetByte :: AlexInput -> Maybe (Word8, AlexInput)
alexGetChar :: AlexInput -> Maybe (Char, AlexInput)
getNextToken :: ParseMonad LToken
getNextTokenWrapper :: (LToken -> ParseMonad a) -> ParseMonad a
sem_prop, soak :: Int
data AlexAddr
AlexA# :: Addr# -> AlexAddr
instance Functor AlexLastAcc
module CSPM.Evaluator.Environment
type Environment = Map Name Value
new :: Environment
lookup :: Environment -> Name -> Value
newLayerAndBind :: Environment -> [(Name, Value)] -> Environment
toList :: Environment -> [(Name, Value)]
module CSPM.Evaluator.Monad
data EvaluationState
EvaluationState :: Environment -> EvaluationState
environment :: EvaluationState -> Environment
type EvaluationMonad = LazyEvalMonad EvaluationState
newtype LazyEvalMonad s a
LazyEvalMonad :: (s -> a) -> LazyEvalMonad s a
unLazyEvalMonad :: LazyEvalMonad s a -> s -> a
runLazyEvalMonad :: s -> LazyEvalMonad s a -> a
gets :: (s -> a) -> LazyEvalMonad s a
modify :: (s -> s) -> LazyEvalMonad s a -> LazyEvalMonad s a
runEvaluator :: EvaluationState -> EvaluationMonad a -> a
getState :: EvaluationMonad EvaluationState
getEnvironment :: EvaluationMonad Environment
lookupVar :: Name -> EvaluationMonad Value
-- | Implements non-recursive lets.
addScopeAndBind :: [(Name, Value)] -> EvaluationMonad a -> EvaluationMonad a
-- | Implements recursive lets.
addScopeAndBindM :: [(Name, EvaluationMonad Value)] -> EvaluationMonad a -> EvaluationMonad a
throwError :: ErrorMessage -> a
instance Monad (LazyEvalMonad a)
module CSPM.Evaluator.Values
data Value
VInt :: Int -> Value
VBool :: Bool -> Value
VTuple :: [Value] -> 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.
VDot :: [Value] -> Value
VChannel :: Name -> Value
VDataType :: Name -> Value
VList :: [Value] -> Value
VSet :: ValueSet -> Value
VFunction :: ([Value] -> EvaluationMonad Value) -> Value
VProc :: Proc -> Value
-- | A compiled process. Note this is an infinite data structure (due to
-- PProcCall) as this makes compilation easy (we can easily chase
-- dependencies).
data Proc
PAlphaParallel :: [(Set Event, Proc)] -> Proc
PException :: Proc -> (Set Event) -> Proc -> Proc
PExternalChoice :: [Proc] -> Proc
PGenParallel :: (Set Event) -> [Proc] -> Proc
PHide :: Proc -> (Set Event) -> Proc
PInternalChoice :: [Proc] -> Proc
PInterrupt :: Proc -> Proc -> Proc
PInterleave :: [Proc] -> Proc
PLinkParallel :: Proc -> (Map Event Event) -> Proc -> Proc
POperator :: ProcOperator -> Proc -> Proc
PPrefix :: Event -> Proc -> Proc
PRename :: (Relation Event Event) -> Proc -> Proc
PSequentialComp :: Proc -> Proc -> Proc
PSlidingChoice :: Proc -> Proc -> Proc
-- | Labels the process this contains. This allows infinite loops to be
-- spotted.
PProcCall :: ProcName -> Proc -> Proc
-- | An operator that can be applied to processes.
data ProcOperator
Chase :: ProcOperator
Diamond :: ProcOperator
Explicate :: ProcOperator
Normalize :: ProcOperator
ModelCompress :: ProcOperator
StrongBisim :: ProcOperator
TauLoopFactor :: ProcOperator
WeakBisim :: ProcOperator
-- | Events, as represented in the LTS.
data Event
-- | The internal special event tau.
Tau :: Event
-- | The internal event tick, representing termination.
Tick :: Event
-- | Any event defined in a channel definition.
UserEvent :: String -> Event
-- | Implements CSPM comparisons (note that Ord Value does not).
compareValues :: Value -> Value -> Maybe Ordering
procId :: Name -> [[Value]] -> ProcName
-- | This assumes that the value is a VDot with the left is a VChannel
valueEventToEvent :: Value -> Event
-- | Takes two values and dots then together appropriately.
combineDots :: Value -> Value -> EvaluationMonad Value
-- | 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.
extensions :: Value -> EvaluationMonad [Value]
-- | Returns an x such that ev.x has been extended by exactly one atomic
-- field. This could be inside a subfield or elsewhere.
oneFieldExtensions :: Value -> EvaluationMonad [Value]
-- | Takes a datatype or a channel value and computes v.x for all x that
-- complete the value.
productions :: Value -> EvaluationMonad [Value]
instance Show Value
instance PrettyPrintable Value
instance Ord Value
instance Eq Value
module CSPM.Evaluator.Exceptions
patternMatchFailureMessage :: SrcSpan -> TCPat -> Value -> ErrorMessage
headEmptyListMessage :: ErrorMessage
tailEmptyListMessage :: ErrorMessage
funBindPatternMatchFailureMessage :: SrcSpan -> Name -> [[Value]] -> ErrorMessage
replicatedInternalChoiceOverEmptySetMessage :: SrcSpan -> Exp Name -> ErrorMessage
typeCheckerFailureMessage :: String -> ErrorMessage
cannotConvertIntegersToListMessage :: ErrorMessage
cannotConvertProcessesToListMessage :: ErrorMessage
cannotCheckSetMembershipError :: Value -> ValueSet -> ErrorMessage
cardOfInfiniteSetMessage :: ValueSet -> ErrorMessage
cannotUnionSetsMessage :: ValueSet -> ValueSet -> ErrorMessage
cannotIntersectSetsMessage :: ValueSet -> ValueSet -> ErrorMessage
cannotDifferenceSetsMessage :: ValueSet -> ValueSet -> ErrorMessage
eventIsNotValidMessage :: Value -> ErrorMessage
-- | Provides a set implementation for machine CSP sets. This relies
-- heavily on the type checking and assumes in many places that the sets
-- being operated on are suitable for the opertion in question.
--
-- We cannot just use the built in set implementation as FDR assumes in
-- several places that infinite sets are allowed.
module CSPM.Evaluator.ValueSet
data ValueSet
-- | Set of all integers
Integers :: ValueSet
-- | Set of all processes
Processes :: ValueSet
-- | The infinite set of integers starting at lb.
IntSetFrom :: Int -> ValueSet
-- | The empty set
emptySet :: ValueSet
-- | Converts a list to a set
fromList :: [Value] -> ValueSet
-- | Converts a set to list.
toList :: ValueSet -> [Value]
-- | Compares two value sets using subseteq (as per the specification).
compareValueSets :: ValueSet -> ValueSet -> Maybe Ordering
-- | Is the specified value a member of the set.
member :: Value -> ValueSet -> Bool
-- | The cardinality of the set. Throws an error if the set is infinite.
card :: ValueSet -> Integer
-- | Is the specified set empty?
empty :: ValueSet -> Bool
-- | Union two sets throwing an error if it cannot be done in a way that
-- will terminate.
union :: ValueSet -> ValueSet -> ValueSet
-- | Replicated union.
unions :: [ValueSet] -> ValueSet
-- | Intersects two sets throwing an error if it cannot be done in a way
-- that will terminate.
intersection :: ValueSet -> ValueSet -> ValueSet
-- | Replicated intersection.
intersections :: [ValueSet] -> ValueSet
difference :: ValueSet -> ValueSet -> ValueSet
-- | Produces a ValueSet of the carteisan product of several ValueSets,
-- using vc to convert each sequence of values into a single
-- value.
cartesianProduct :: ([Value] -> Value) -> [ValueSet] -> ValueSet
-- | Returns the powerset of a ValueSet. This requires
powerset :: ValueSet -> ValueSet
-- | Returns the set of all sequences over the input set. This is infinite
-- so we use a CompositeSet.
allSequences :: ValueSet -> ValueSet
-- | Returns the value iff the set contains one item only.
singletonValue :: ValueSet -> Maybe Value
valueSetToEventSet :: ValueSet -> Set Event
instance Ord ValueSet
instance Show ValueSet
instance PrettyPrintable ValueSet
instance Eq ValueSet
-- | This module contains all the builtin definitions for the input CSPM
-- language.
module CSPM.Prelude
data BuiltIn
BuiltIn :: Name -> String -> Bool -> Maybe Name -> TypeScheme -> Bool -> Bool -> Bool -> BuiltIn
name :: BuiltIn -> Name
stringName :: BuiltIn -> String
isDeprecated :: BuiltIn -> Bool
deprecatedReplacement :: BuiltIn -> Maybe Name
typeScheme :: BuiltIn -> TypeScheme
isTypeUnsafe :: BuiltIn -> Bool
isExternal :: BuiltIn -> Bool
isTransparent :: BuiltIn -> Bool
builtins :: Bool -> [BuiltIn]
transparentFunctionForOccName :: OccName -> Maybe BuiltIn
externalFunctionForOccName :: OccName -> Maybe BuiltIn
instance Eq BuiltIn
-- | Renames all variables to unique Names, in the process converting all
-- UnRenamedName into Name. This simplifies many subsequent phases as
-- every name is guaranteed to be unique so flat maps may be used, rather
-- than Hierarchical maps. Further, this also flags patterns that match
-- channels and datatype clauses.
module CSPM.Renamer
data RenamerState
type RenamerMonad = StateT RenamerState IO
-- | Runs the renamer starting at the given state and returning the given
-- state.
runFromStateToState :: RenamerState -> RenamerMonad a -> IO (a, RenamerState)
-- | Initialises the renamer.
initRenamer :: IO (RenamerState)
rename :: Renamable e1 e2 => e1 -> RenamerMonad e2
newScope :: RenamerMonad ()
instance FreeVars (Decl UnRenamedName)
instance FreeVars (Field UnRenamedName)
instance FreeVars (Stmt UnRenamedName)
instance FreeVars (Pat UnRenamedName)
instance FreeVars a => FreeVars (Annotated b a)
instance FreeVars a => FreeVars [a]
instance Renamable (Exp UnRenamedName) (Exp Name)
instance Renamable (ModelOption UnRenamedName) (ModelOption Name)
instance Renamable (Assertion UnRenamedName) (Assertion Name)
instance Renamable (Module UnRenamedName) (Module Name)
instance Renamable (InteractiveStmt UnRenamedName) (InteractiveStmt Name)
instance Renamable (Match UnRenamedName) (Match Name)
instance (Renamable e1 e2, Renamable e1' e2') => Renamable (e1, e1') (e2, e2')
instance Renamable e1 e2 => Renamable (Annotated a e1) (Annotated a e2)
instance Renamable e1 e2 => Renamable (Maybe e1) (Maybe e2)
instance Renamable e1 e2 => Renamable [e1] [e2]
module CSPM.Evaluator.BuiltInFunctions
injectBuiltInFunctions :: EvaluationMonad a -> EvaluationMonad a
builtInName :: String -> Name
module CSPM.Evaluator.PatBind
class Bindable a
bind :: Bindable a => a -> Value -> (Bool, [(Name, Value)])
bindAll :: Bindable a => [a] -> [Value] -> (Bool, [(Name, Value)])
instance Bindable (Pat Name)
instance Bindable a => Bindable (Annotated b a)
module CSPM.Evaluator.DeclBind
-- | Given a list of declarations, returns a sequence of names bounds to
-- values that can be passed to addScopeAndBind in order to bind
-- them in the current scope.
bindDecls :: [TCDecl] -> [(Name, EvaluationMonad Value)]
instance FreeVars (Pat Name)
instance FreeVars a => FreeVars (Annotated b a)
module CSPM.Evaluator.Module
bindModules :: [TCModule] -> [(Name, EvaluationMonad Value)]
bindModule :: TCModule -> [(Name, EvaluationMonad Value)]
module CSPM.Evaluator.Expr
class Evaluatable a
eval :: Evaluatable a => a -> EvaluationMonad Value
instance Evaluatable (Exp Name)
instance Evaluatable a => Evaluatable (Annotated b a)
module CSPM.Evaluator
evaluateExp :: TCExp -> EvaluationMonad Value
-- | Evaluates the declaration but doesn't add it to the current
-- environment.
evaluateDecl :: TCDecl -> EvaluationMonad [(Name, EvaluationMonad Value)]
-- | Evaluates the declaration but doesn't add it to the current
-- environment.
evaluateFile :: [TCModule] -> EvaluationMonad [(Name, EvaluationMonad Value)]
getBoundNames :: EvaluationMonad [Name]
addToEnvironment :: [(Name, EvaluationMonad Value)] -> EvaluationMonad EvaluationState
-- | The environment to use initially. This uses the IO monad as the
-- EvaluationMonad cannot be used without a valid environment.
initEvaluator :: EvaluationState
runFromStateToState :: EvaluationState -> EvaluationMonad a -> (a, EvaluationState)
type EvaluationMonad = LazyEvalMonad EvaluationState
runEvaluator :: EvaluationState -> EvaluationMonad a -> a
data EvaluationState
module CSPM.Parser.Parser
parseFile_ :: ParseMonad [PDecl]
parseInteractiveStmt_ :: ParseMonad PInteractiveStmt
parseExpression_ :: ParseMonad PExp
instance Locatable (Annotated a)
instance Locatable Located
-- | A module that parses CSPM modules.
--
-- The biggest problem with parsing CSPM is that > means both greater
-- than and end sequence. For example, consider <x | x > 2
-- and <x | x > 2 >. Both of these are syntactically
-- valid, but the parser has no way of deducing whether or not the first
-- > it sees is an end sequence or a greater than.
--
-- Clearly, without an arbitrary lookahead it is not possible, in
-- general, to solve this. Hence, we go for the 'shortest sequence'
-- approach, in which whenever a > is seen whilst a list is
-- currently open, we assume that it closes the list.
--
-- FDR has a slightly more sophisticated scheme, but this depends on the
-- fact that Bison happens to generate a lazy lookahead in this case,
-- whereas Happy is never lazy in its lookahead token. In particular, FDR
-- has a sequence stack of integers. The top value means the number of
-- open sequence brackets it has seen so far. It lexes < as
-- normal, but whenever it decides that a < token is a open
-- sequence token, adds one to the current top of the sequence stack.
-- Then, whenever a > token is discovered it checks to see if
-- the top value is non-zero, and if so lexes endseq, otherwise lexes gt.
-- It then decrements the value of the top of the sequence stack in the
-- parser. It uses a stack to allow it to open new contexts within
-- parenthesis.
--
-- Laziness is required when scanning something like <1> >
-- <1> as, if it is not lazy then the second >
-- will be lexed just before the first > is dealt with.
--
-- Instead, we decrement the top of the sequence stack within the lexer
-- instead. I don't think this will cause a change in behaviour, as if
-- the lexer lexes a _endseq token then it will definitely decrement the
-- counter later (and it has already checked to make sure it is
-- non-zero). However, we do keep the decision about LT being
-- openseq or < in the parser as this can decide
-- when this is the case (e.g. x < means it must be a
-- LT).
--
-- The above is a problem in conjunction with nested brackets. For
-- example, consider <(0,1) | x>; when we parse this we
-- would take the ( into the lookahead before we actually parse
-- <, meaning that when we push the 1 onto the
-- sequence stack it actually goes onto the new top entry that is popped
-- off after ) is processed. Therefore, the > will
-- be parsed as a GT. To solve this we make sure that whenever
-- we pop off the sequence stack we add any remaining open sequences onto
-- the new top element. Clearly this would be unsafe if we were relying
-- on this for parsing, but as we are not this should be fine and should
-- cause no further ambiguities.
--
-- It should be noted the above is a big hacky workaround, but I see no
-- alternative without resorting to an arbitrary lookahead parser (like
-- parsec) and its obvious inefficiency.
module CSPM.Parser
-- | Parse the given file, returning the parsed PModules.
parseFile :: String -> ParseMonad [PModule]
-- | Parse as string as an PInteractiveStmt.
parseInteractiveStmt :: String -> ParseMonad PInteractiveStmt
-- | Parses a string as an PExp.
parseExpression :: String -> ParseMonad PExp
-- | Parse a string, as though it were an entire file, returning the parsed
-- PModules.
parseStringAsFile :: String -> ParseMonad [PModule]
type ParseMonad = StateT ParserState IO
runParser :: ParseMonad a -> String -> IO a
module CSPM.TypeChecker.Environment
type Environment = Map Name SymbolInformation
new :: Environment
bind :: Environment -> [(Name, SymbolInformation)] -> Environment
maybeLookup :: Environment -> Name -> Maybe SymbolInformation
update :: Environment -> Name -> SymbolInformation -> Environment
delete :: Environment -> Name -> Environment
toList :: Environment -> [(Name, SymbolInformation)]
-- | Make symbol information for the type assuming that the symbol is not
-- deprecated and its type is not unsafe.
mkSymbolInformation :: TypeScheme -> SymbolInformation
-- | Used to represent information about a symbol
data SymbolInformation
SymbolInformation :: TypeScheme -> Bool -> Maybe Name -> Bool -> SymbolInformation
-- | The type of the symbol
typeScheme :: SymbolInformation -> TypeScheme
-- | Is this symbol deprecated
isDeprecated :: SymbolInformation -> Bool
deprecationReplacement :: SymbolInformation -> Maybe Name
-- | Is this symbols' type too general (if so use of it will emit a
-- soundness warning)
isTypeUnsafe :: SymbolInformation -> Bool
instance Eq SymbolInformation
instance Show SymbolInformation
module CSPM.TypeChecker.Exceptions
type Error = Doc
type Warning = Doc
infiniteUnificationMessage :: Type -> Type -> Error
unificationErrorMessage :: [(Type, Type)] -> Error
incorrectArgumentCountMessage :: Doc -> Int -> Int -> Error
constraintUnificationErrorMessage :: Constraint -> Type -> Error
deprecatedNameUsed :: Name -> Maybe Name -> Error
unsafeNameUsed :: Name -> Error
module CSPM.TypeChecker.Monad
readTypeRef :: TypeVarRef -> TypeCheckMonad (Either (TypeVar, [Constraint]) Type)
writeTypeRef :: TypeVarRef -> Type -> TypeCheckMonad ()
freshTypeVar :: MonadIO m => m Type
freshTypeVarWithConstraints :: MonadIO m => [Constraint] -> m Type
-- | Get the type of n and throw an exception if it doesn't exist.
getType :: Name -> TypeCheckMonad TypeScheme
-- | Sets the type of n to be t in the current scope only. No unification
-- is performed.
setType :: Name -> TypeScheme -> TypeCheckMonad ()
isTypeUnsafe :: Name -> TypeCheckMonad Bool
markTypeAsUnsafe :: Name -> TypeCheckMonad ()
replacementForDeprecatedName :: Name -> TypeCheckMonad (Maybe Name)
isDeprecated :: Name -> TypeCheckMonad Bool
markAsDeprecated :: Name -> Maybe Name -> TypeCheckMonad ()
-- | Takes a type and compresses the type by reading all type variables and
-- if they point to another type, it returns that type instead.
compress :: Type -> TypeCheckMonad Type
-- | Apply compress to the type of a type scheme.
compressTypeScheme :: TypeScheme -> TypeCheckMonad TypeScheme
type TypeCheckMonad = StateT TypeInferenceState IO
-- | Runs the typechecker, starting from state st. If any errors
-- are encountered then a SourceError will be thrown with the
-- relevent error messages.
runTypeChecker :: TypeInferenceState -> TypeCheckMonad a -> IO a
newTypeInferenceState :: TypeInferenceState
data TypeInferenceState
TypeInferenceState :: Environment -> [Name] -> SrcSpan -> [ErrorContext] -> [ErrorMessage] -> [ErrorMessage] -> [(Type, Type)] -> Bool -> Bool -> TypeInferenceState
-- | The type environment, which is a map from names to types.
environment :: TypeInferenceState -> Environment
-- | List of names that correspond to channels and datatypes - used when
-- detecting dependencies.
dataTypesAndChannels :: TypeInferenceState -> [Name]
-- | Location of the current AST element - used for error pretty printing
srcSpan :: TypeInferenceState -> SrcSpan
-- | Error stack - provides context information for any errors that might
-- be raised
errorContexts :: TypeInferenceState -> [ErrorContext]
-- | Errors that have occured
errors :: TypeInferenceState -> [ErrorMessage]
-- | List of warnings that have occured
warnings :: TypeInferenceState -> [ErrorMessage]
-- | Stack of attempted unifications - the current one is at the front. In
-- the form (expected, actual).
unificationStack :: TypeInferenceState -> [(Type, Type)]
-- | Are we currently in an error state
inError :: TypeInferenceState -> Bool
symUnificationAllowed :: TypeInferenceState -> Bool
getState :: TypeCheckMonad TypeInferenceState
local :: [Name] -> TypeCheckMonad a -> TypeCheckMonad a
getEnvironment :: TypeCheckMonad Environment
type ErrorContext = Doc
addErrorContext :: ErrorContext -> TypeCheckMonad a -> TypeCheckMonad a
getErrorContexts :: TypeCheckMonad [ErrorContext]
getSrcSpan :: TypeCheckMonad SrcSpan
-- | Sets the SrcSpan only within prog.
setSrcSpan :: SrcSpan -> TypeCheckMonad a -> TypeCheckMonad a
getUnificationStack :: TypeCheckMonad [(Type, Type)]
addUnificationPair :: (Type, Type) -> TypeCheckMonad a -> TypeCheckMonad a
symmetricUnificationAllowed :: TypeCheckMonad Bool
disallowSymmetricUnification :: TypeCheckMonad a -> TypeCheckMonad a
getInError :: TypeCheckMonad Bool
setInError :: Bool -> TypeCheckMonad a -> TypeCheckMonad a
resetWarnings :: TypeCheckMonad ()
getWarnings :: TypeCheckMonad [ErrorMessage]
addWarning :: Warning -> TypeCheckMonad ()
raiseMessageAsError :: Error -> TypeCheckMonad a
-- | Report a message as an error
raiseMessagesAsError :: [Error] -> TypeCheckMonad a
-- | Given a string causes a Panic to be thrown.
panic :: String -> a
manyErrorsIfFalse :: Bool -> [Error] -> TypeCheckMonad ()
errorIfFalseM :: TypeCheckMonad Bool -> Error -> TypeCheckMonad ()
-- | Report the error if first parameter is False.
errorIfFalse :: Bool -> Error -> TypeCheckMonad ()
tryAndRecover :: TypeCheckMonad a -> TypeCheckMonad a -> TypeCheckMonad a
failM :: TypeCheckMonad a
addDataTypeOrChannel :: Name -> TypeCheckMonad ()
isDataTypeOrChannel :: Name -> TypeCheckMonad Bool
module CSPM.TypeChecker.BuiltInFunctions
injectBuiltInFunctions :: TypeCheckMonad ()
-- | Traverses the AST filling in all the type information, ensuring that
-- each type is fully compressed.
module CSPM.TypeChecker.Compressor
class Compressable a
mcompress :: Compressable a => a -> TypeCheckMonad a
instance Compressable Literal
instance Compressable Model
instance Compressable SemanticProperty
instance Compressable (Pat a)
instance Compressable (InteractiveStmt a)
instance Compressable (Stmt a)
instance Compressable (Field a)
instance Compressable (Match a)
instance Compressable (DataTypeClause a)
instance Compressable (ModelOption a)
instance Compressable (Assertion a)
instance Compressable (Decl a)
instance Compressable (Module a)
instance Compressable (Exp a)
instance (Compressable a, Compressable b) => Compressable (a, b)
instance Compressable a => Compressable (Maybe a)
instance Compressable a => Compressable [a]
instance Compressable a => Compressable (Annotated () a)
instance Compressable a => Compressable (Annotated (Maybe Type, PType) a)
instance Compressable a => Compressable (Annotated (Maybe SymbolTable, PSymbolTable) a)
module CSPM.TypeChecker.Dependencies
class Dependencies a
dependencies :: Dependencies a => a -> TypeCheckMonad [Name]
namesBoundByDecl :: AnDecl Name -> TypeCheckMonad [Name]
namesBoundByDecl' :: Decl Name -> StateT TypeInferenceState IO [Name]
class FreeVars a
freeVars :: FreeVars a => a -> TypeCheckMonad [Name]
instance FreeVars (Field Name)
instance FreeVars (Stmt Name)
instance FreeVars (Pat Name)
instance FreeVars a => FreeVars (Annotated b a)
instance FreeVars a => FreeVars [a]
instance Dependencies (DataTypeClause Name)
instance Dependencies (Match Name)
instance Dependencies (ModelOption Name)
instance Dependencies (Assertion Name)
instance Dependencies (Decl Name)
instance Dependencies (Field Name)
instance Dependencies (Stmt Name)
instance Dependencies (Exp Name)
instance Dependencies (Pat Name)
instance Dependencies a => Dependencies (Annotated b a)
instance Dependencies a => Dependencies (Maybe a)
instance Dependencies a => Dependencies [a]
module CSPM.TypeChecker.Unification
-- | Generalise the types of the declarations. The parameter names
-- gives the names that were bound by all the declarations that we are
-- interested in. This is done because we convert a type T into forall vs
-- T where vs = fvts (T) - fvts(Env) where Env does not contain the
-- function whose type we are generalizing (this is because when we type
-- a declaration we are really typing a lambda function).
generaliseGroup :: [Name] -> [TypeCheckMonad [(Name, Type)]] -> TypeCheckMonad [[(Name, TypeScheme)]]
-- | Instantiates the typescheme with some fresh type variables.
instantiate :: TypeScheme -> TypeCheckMonad Type
-- | The main type unification algorithm. This adds values to the
-- unification stack in order to ensure error messages are helpful.
unify :: Type -> Type -> TypeCheckMonad Type
-- | Unifys all types to a single type. The first type is used as the
-- expected Type in error messages.
unifyAll :: [Type] -> TypeCheckMonad Type
-- | Takes a type and attempts to simplify all TDots inside by combining
-- TDotable t1 t2 and arguments.
evaluateDots :: Type -> TypeCheckMonad Type
-- | Takes a type and converts TDot t1 t2 to [t1, t2].
typeToDotList :: Type -> TypeCheckMonad [Type]
module CSPM.TypeChecker.Common
class TypeCheckable a b | a -> b
typeCheck :: TypeCheckable a b => a -> TypeCheckMonad b
typeCheckExpect :: TypeCheckable a b => a -> Type -> TypeCheckMonad b
typeCheck' :: TypeCheckable a b => a -> TypeCheckMonad b
errorContext :: TypeCheckable a b => a -> Maybe ErrorContext
ensureAreEqual :: TypeCheckable a Type => [a] -> TypeCheckMonad Type
ensureIsList :: TypeCheckable a b => a -> TypeCheckMonad b
ensureIsSet :: TypeCheckable a b => a -> TypeCheckMonad b
ensureIsBool :: TypeCheckable a b => a -> TypeCheckMonad b
ensureIsInt :: TypeCheckable a b => a -> TypeCheckMonad b
ensureIsChannel :: TypeCheckable a b => a -> TypeCheckMonad b
ensureIsEvent :: TypeCheckable a b => a -> TypeCheckMonad b
ensureIsProc :: TypeCheckable a b => a -> TypeCheckMonad b
ensureHasConstraint :: Constraint -> Type -> TypeCheckMonad Type
instance TypeCheckable Literal Type
module CSPM.TypeChecker.Pat
instance TypeCheckable (Pat Name) Type
instance TypeCheckable TCPat Type
module CSPM.TypeChecker.Expr
instance TypeCheckable (Exp Name) Type
instance TypeCheckable TCExp Type
module CSPM.TypeChecker.Decl
-- | Type check a list of possibly mutually recursive functions
typeCheckDecls :: [TCDecl] -> TypeCheckMonad ()
instance TypeCheckable (Match Name) Type
instance TypeCheckable TCMatch Type
instance TypeCheckable (DataTypeClause Name) (Name, [Type])
instance TypeCheckable TCDataTypeClause (Name, [Type])
instance TypeCheckable (ModelOption Name) ()
instance TypeCheckable (Assertion Name) ()
instance TypeCheckable (Decl Name) [(Name, Type)]
instance TypeCheckable TCDecl [(Name, Type)]
module CSPM.TypeChecker.InteractiveStmt
instance TypeCheckable (InteractiveStmt Name) ()
instance TypeCheckable TCInteractiveStmt ()
module CSPM.TypeChecker.Module
instance TypeCheckable (Module Name) ()
instance TypeCheckable TCModule ()
instance TypeCheckable [TCModule] ()
module CSPM.TypeChecker
typeCheck :: (Compressable a, TypeCheckable a b) => a -> TypeCheckMonad a
typeCheckExpect :: (Compressable a, TypeCheckable a Type) => Type -> a -> TypeCheckMonad a
typeOfExp :: TCExp -> TypeCheckMonad Type
-- | Returns the list of names that this expression depends on
dependenciesOfExp :: TCExp -> TypeCheckMonad [Name]
initTypeChecker :: IO TypeInferenceState
type TypeCheckMonad = StateT TypeInferenceState IO
data TypeInferenceState
-- | Runs the typechecker, starting from state st. If any errors
-- are encountered then a SourceError will be thrown with the
-- relevent error messages.
runTypeChecker :: TypeInferenceState -> TypeCheckMonad a -> IO a
runFromStateToState :: TypeInferenceState -> TypeCheckMonad a -> IO (a, [ErrorMessage], TypeInferenceState)
-- | This module provides the main high-level interface to the library
-- functionality. It does this through a monadic interface, mainly due to
-- the fact that several of the components require the use of the IO
-- monad. It is highly recommended that users of this library use a monad
-- and then implement the CSPMMonad class on their own custom
-- monad. An example of this is shown by the basic implementation of the
-- CSPM monad.
--
-- The main library datatype is exported by
-- CSPM.DataStructures.Syntax, which provides an AST
-- representation of machine CSP. Most of the pieces of syntax, like
-- expressions (Exp), are parametrised by the type of the
-- variables that it contains. For more information see the comment at
-- the top of the above module.
--
-- The library exports several APIs which, in likely order of usage, are:
--
--
-- - Parser Parses strings or files and produces an
-- AST, parametrised by UnRenamedName, which are simply pieces of
-- text.
-- - Renamer Renames the AST and produces an equivalent
-- AST, but parametrised by Name, which uniquely identify the
-- binding instance of each variable (see documentation of
-- Name).
-- - Type Checker Type checks an AST, in the process
-- annotating it with types.
-- - Desugarer Desugars an AST, remove syntactic sugar
-- and prepares it for evaluation. The AST produced by this phase should
-- not be pretty printed as it parenthesis have been removed, potentially
-- making it not equivalent.
-- - Evaluator Evaluates an AST, returning a
-- Value. Note that the evaluator is lazy, meaning that the
-- resulting Value will be generated as it is consumed, making it
-- suitable for streaming to subsequent compilation phases.
--
--
-- For example, suppose we wish to evaluate the expression
-- test(1,2,3) within the context of the file test.csp
-- we could use the following segment of code:
--
--
-- main :: IO ()
-- main = do
-- session <- newCSPMSession
-- (value, resultingSession) <- unCSPM session $ do
-- -- Parse the file, returning something of type PModule.
-- parsedFile <- parseFile "test.csp"
-- -- Rename the file, returning something of type TCModule.
-- renamedFile <- renameFile parsedFile
-- -- Typecheck the file, annotating it with types.
-- typeCheckedFile <- typeCheckFile renamedFile
-- -- Desugar the file, returning the version ready for evaluation.
-- desugaredFile <- desugarFile typeCheckedFile
-- -- Bind the file, making all functions and patterns available.
-- bindFile desugaredFile
--
-- -- The file is now ready for use, so now we build the expression
-- -- to be evaluated.
-- parsedExpression <- parseExpression "test(1,2,3)"
-- renamedExpression <- renameExpression parsedExpression
-- typeCheckedExpression <- typeCheckExpression renamedExpression
-- desugaredExpression <- desugarExpression typeCheckedExpression
--
-- -- Evaluate the expression in the current context.
-- value <- evaluateExpression desugaredExpression
-- return value
-- putStrLn (show (prettyPrint value))
-- return ()
--
--
-- This would pretty print the value of the expression to stdout.
module CSPM
-- | A CSPMSession represents the internal states of all the various
-- components.
data CSPMSession
-- | Create a new CSPMSession.
newCSPMSession :: MonadIO m => m CSPMSession
-- | The CSPMMonad is the main monad in which all functions must be called.
-- Whilst there is a build in representation (see CSPM) it is
-- recommended that you define an instance of CSPMMonad over
-- whatever monad you use.
class MonadIO m => CSPMMonad m
getSession :: CSPMMonad m => m CSPMSession
setSession :: CSPMMonad m => CSPMSession -> m ()
handleWarnings :: CSPMMonad m => [ErrorMessage] -> m ()
-- | Executes an operation giving it access to the current
-- CSPMSession.
withSession :: CSPMMonad m => (CSPMSession -> m a) -> m a
-- | A basic implementation of CSPMMonad, using the StateT
-- monad. This prints out any warnings to stdout.
type CSPM = StateT CSPMSession IO
-- | Runs a CSPM function, returning the result and the resulting
-- session.
unCSPM :: CSPMSession -> CSPM a -> IO (a, CSPMSession)
-- | Parses a string, treating it as though it were a file. Throws a
-- SourceError on any parse error.
parseStringAsFile :: CSPMMonad m => String -> m [PModule]
-- | Parse a file fp. Throws a SourceError on any parse
-- error.
parseFile :: CSPMMonad m => FilePath -> m [PModule]
-- | Parses a PInteractiveStmt. Throws a SourceError on any
-- parse error.
parseInteractiveStmt :: CSPMMonad m => String -> m PInteractiveStmt
-- | Parses an Exp. Throws a SourceError on any parse error.
parseExpression :: CSPMMonad m => String -> m PExp
-- | Renames a file.
renameFile :: CSPMMonad m => [PModule] -> m [TCModule]
-- | Rename ian interactive statement.
renameInteractiveStmt :: CSPMMonad m => PInteractiveStmt -> m TCInteractiveStmt
-- | Renames an expression.
renameExpression :: CSPMMonad m => PExp -> m TCExp
-- | Type checks a file, also desugaring and annotating it. Throws a
-- SourceError if an error is encountered and will call
-- handleWarnings on any warnings. This also performs desugaraing.
typeCheckFile :: CSPMMonad m => [TCModule] -> m [TCModule]
-- | Type checks a PInteractiveStmt.
typeCheckInteractiveStmt :: CSPMMonad m => TCInteractiveStmt -> m TCInteractiveStmt
-- | Type checkes a PExp, returning the desugared and annotated
-- version.
typeCheckExpression :: CSPMMonad m => TCExp -> m TCExp
-- | Given a Type, ensures that the PExp is of that type. It
-- returns the annoated and desugared expression.
ensureExpressionIsOfType :: CSPMMonad m => Type -> TCExp -> m TCExp
-- | Returns the Names that the given type checked expression
-- depends on.
dependenciesOfExp :: CSPMMonad m => TCExp -> m [Name]
-- | Gets the type of the expression in the current context.
typeOfExpression :: CSPMMonad m => TCExp -> m Type
-- | Desugar a file, preparing it for evaulation.
desugarFile :: CSPMMonad m => [TCModule] -> m [TCModule]
-- | Desugars an interactive statement.
desugarInteractiveStmt :: CSPMMonad m => TCInteractiveStmt -> m TCInteractiveStmt
-- | Desugars an expression.
desugarExpression :: CSPMMonad m => TCExp -> m TCExp
-- | Binds all the declarations that are in a particular file. Requires the
-- file to be desugared.
bindFile :: CSPMMonad m => [TCModule] -> m ()
-- | Takes a declaration and adds it to the current environment. Requires
-- the declaration to be desugared.
bindDeclaration :: CSPMMonad m => TCDecl -> m ()
-- | Get a list of currently bound names in the environment.
getBoundNames :: CSPMMonad m => m [Name]
-- | Evaluates the expression in the current context. Requires the
-- expression to be desugared.
evaluateExpression :: CSPMMonad m => TCExp -> m Value
-- | Runs the parser.
runParserInCurrentState :: CSPMMonad m => FilePath -> ParseMonad a -> m a
-- | Runs renamer in the current state.
runRenamerInCurrentState :: CSPMMonad m => RenamerMonad a -> m a
-- | Runs the typechecker in the current state, saving the resulting state
-- and returning any warnings encountered.
runTypeCheckerInCurrentState :: CSPMMonad m => TypeCheckMonad a -> m (a, [ErrorMessage])
-- | Runs the evaluator in the current state, saving the resulting state.
runEvaluatorInCurrentState :: CSPMMonad m => EvaluationMonad a -> m a
-- | Given a program that can return warnings, runs the program and raises
-- any warnings found using handleWarnings.
reportWarnings :: CSPMMonad m => m (a, [ErrorMessage]) -> m a
-- | Return the version of libcspm that is being used.
getLibCSPMVersion :: Version
instance CSPMMonad CSPM