-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | A library providing a parser, type checker and evaluator for CSPM.
--   
--   A library providing a parser, type checker and evaluator for CSPM.
@package libcspm
@version 0.1.2

module Util.Monad
concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b]

module Util.List

-- | Returns true iff the list has no duplicates.
noDups :: Eq a => [a] -> Bool

module Util.Prelude

-- | Given two orderings, returns the second if the first is <a>EQ</a> 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]]

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 <a>tabWidth</a> characters, on each line (uses
--   <a>nest</a>).
tabIndent :: Doc -> Doc

-- | Surrounds a <a>Doc</a> with <a>&lt;</a> and <a>&gt;</a>.
angles :: Doc -> Doc

-- | Surrounds a <a>Doc</a> with '|'.
bars :: Doc -> Doc

-- | Separates a list of <a>Doc</a>s by ','.
list :: [Doc] -> Doc

-- | Separates a list of <a>Doc</a>s by <a>.</a>.
dotSep :: [Doc] -> Doc

-- | Converts a number into <tt>first</tt>, <tt>second</tt> etc.
speakNth :: Int -> Doc

module Util.Exception

-- | Any type that you wish to throw or catch as an exception must be an
--   instance of the <tt>Exception</tt> class. The simplest case is a new
--   exception type directly below the root:
--   
--   <pre>
--   data MyException = ThisException | ThatException
--       deriving (Show, Typeable)
--   
--   instance Exception MyException
--   </pre>
--   
--   The default method definitions in the <tt>Exception</tt> class do what
--   we need in this case. You can now throw and catch
--   <tt>ThisException</tt> and <tt>ThatException</tt> as exceptions:
--   
--   <pre>
--   *Main&gt; throw ThisException `catch` \e -&gt; putStrLn ("Caught " ++ show (e :: MyException))
--   Caught ThisException
--   </pre>
--   
--   In more complicated examples, you may wish to define a whole hierarchy
--   of exceptions:
--   
--   <pre>
--   ---------------------------------------------------------------------
--   -- Make the root exception type for all the exceptions in a compiler
--   
--   data SomeCompilerException = forall e . Exception e =&gt; SomeCompilerException e
--       deriving Typeable
--   
--   instance Show SomeCompilerException where
--       show (SomeCompilerException e) = show e
--   
--   instance Exception SomeCompilerException
--   
--   compilerExceptionToException :: Exception e =&gt; e -&gt; SomeException
--   compilerExceptionToException = toException . SomeCompilerException
--   
--   compilerExceptionFromException :: Exception e =&gt; SomeException -&gt; Maybe e
--   compilerExceptionFromException x = do
--       SomeCompilerException a &lt;- fromException x
--       cast a
--   
--   ---------------------------------------------------------------------
--   -- Make a subhierarchy for exceptions in the frontend of the compiler
--   
--   data SomeFrontendException = forall e . Exception e =&gt; SomeFrontendException e
--       deriving Typeable
--   
--   instance Show SomeFrontendException where
--       show (SomeFrontendException e) = show e
--   
--   instance Exception SomeFrontendException where
--       toException = compilerExceptionToException
--       fromException = compilerExceptionFromException
--   
--   frontendExceptionToException :: Exception e =&gt; e -&gt; SomeException
--   frontendExceptionToException = toException . SomeFrontendException
--   
--   frontendExceptionFromException :: Exception e =&gt; SomeException -&gt; Maybe e
--   frontendExceptionFromException x = do
--       SomeFrontendException a &lt;- 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
--   </pre>
--   
--   We can now catch a <tt>MismatchedParentheses</tt> exception as
--   <tt>MismatchedParentheses</tt>, <tt>SomeFrontendException</tt> or
--   <tt>SomeCompilerException</tt>, but not other types, e.g.
--   <tt>IOException</tt>:
--   
--   <pre>
--   *Main&gt; throw MismatchedParentheses <tt>catch</tt> e -&gt; putStrLn ("Caught " ++ show (e :: MismatchedParentheses))
--   Caught MismatchedParentheses
--   *Main&gt; throw MismatchedParentheses <tt>catch</tt> e -&gt; putStrLn ("Caught " ++ show (e :: SomeFrontendException))
--   Caught MismatchedParentheses
--   *Main&gt; throw MismatchedParentheses <tt>catch</tt> e -&gt; putStrLn ("Caught " ++ show (e :: SomeCompilerException))
--   Caught MismatchedParentheses
--   *Main&gt; throw MismatchedParentheses <tt>catch</tt> e -&gt; putStrLn ("Caught " ++ show (e :: IOException))
--   *** Exception: MismatchedParentheses
--   </pre>
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
throwException :: Exception e => e -> a
tryM :: (MonadIOException m, MonadIOException m) => m a -> m (Either LibCSPMException a)
panic :: String -> a
throwSourceError :: ErrorMessages -> a
mkErrorMessage :: SrcSpan -> Doc -> ErrorMessage
mkWarningMessage :: SrcSpan -> Doc -> ErrorMessage

-- | An error message that resulted from something in the user's input.
data ErrorMessage
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 CSPM.Compiler.Processes
data Proc
PAlphaParallel :: [(EventSet, Proc)] -> Proc
PException :: Proc -> EventSet -> Proc -> Proc
PExternalChoice :: [Proc] -> Proc
PGenParallel :: EventSet -> [Proc] -> Proc
PHide :: Proc -> EventSet -> Proc
PInternalChoice :: [Proc] -> Proc
PInterrupt :: Proc -> Proc -> Proc
PInterleave :: [Proc] -> Proc
PPrefix :: Event -> Proc -> Proc
PSequentialComp :: Proc -> Proc -> Proc
PSlidingChoice :: Proc -> Proc -> Proc

-- | PLinkParallel EventMap [Proc] | PRename EventMap Proc | POperator
--   ProcOperator Proc where: data ProcOperator = Normalise | Explicate |
--   StrongBisim | TauLoopFactor | Diamond | ModelCompress
PProcCall :: ProcName -> (Maybe Proc) -> Proc
type ProcName = String
instance Show Proc
instance PrettyPrintable Proc

module Util.HierarchicalMap
data Ord a => HierarchicalMap a b
HierarchicalMap :: [Map a b] -> HierarchicalMap a b
data (Ord a, Show a, Typeable a) => 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 (Ord a, Show a, Show b) => Show (HierarchicalMap a b)
instance (Ord a, Show a, Typeable 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

module CSPM.DataStructures.Names
data Name
Name :: String -> Name
InternalName :: String -> Name
isInternal :: Name -> Bool
mkInternalName :: String -> Name
data QualifiedName
UnQual :: Name -> QualifiedName
instance Typeable Name
instance Eq Name
instance Ord Name
instance Show Name
instance Eq QualifiedName
instance Show QualifiedName

module CSPM.DataStructures.Types
newtype TypeVar
TypeVar :: Int -> TypeVar
data TypeScheme
ForAll :: [(TypeVar, [Constraint])] -> Type -> TypeScheme
data Constraint
Eq :: Constraint
Ord :: 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
newtype IORefMaybe a
IORefMaybe :: (Maybe a) -> IORefMaybe a
type SymbolTable = PartialFunction Name TypeScheme
type PType = IORef (Maybe Type)
type PSymbolTable = IORef SymbolTable
readPType :: MonadIO m => PType -> m (Maybe Type)
setPType :: MonadIO m => PType -> Type -> m ()
freshPType :: MonadIO m => m PType
readPSymbolTable :: MonadIO m => PSymbolTable -> m SymbolTable
setPSymbolTable :: MonadIO m => PSymbolTable -> SymbolTable -> m ()
freshPSymbolTable :: MonadIO m => m PSymbolTable

-- | Pretty prints several types using the same variable substitutions
prettyPrintTypes :: [Type] -> [Doc]
prettyPrintType :: PartialFunction Int Char -> Type -> Doc
collectConstraints :: Type -> [(TypeVar, [Constraint])]
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

module CSPM.DataStructures.Syntax
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
getSymbolTable :: Annotated (Maybe SymbolTable, PSymbolTable) a -> SymbolTable
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 -> Literal
Bool :: Bool -> Literal
data Module
GlobalModule :: [AnDecl] -> Module
data BinaryBooleanOp
And :: BinaryBooleanOp
Or :: BinaryBooleanOp
Equals :: BinaryBooleanOp
NotEquals :: BinaryBooleanOp
LessThan :: BinaryBooleanOp
GreaterThan :: BinaryBooleanOp
LessThanEq :: BinaryBooleanOp
GreaterThanEq :: BinaryBooleanOp
data UnaryBooleanOp
Not :: UnaryBooleanOp
data UnaryMathsOp
Negate :: UnaryMathsOp
data BinaryMathsOp
Divide :: BinaryMathsOp
Minus :: BinaryMathsOp
Mod :: BinaryMathsOp
Plus :: BinaryMathsOp
Times :: BinaryMathsOp
data Exp
App :: AnExp -> [AnExp] -> Exp
BooleanBinaryOp :: BinaryBooleanOp -> AnExp -> AnExp -> Exp
BooleanUnaryOp :: UnaryBooleanOp -> AnExp -> Exp
Concat :: AnExp -> AnExp -> Exp
DotApp :: AnExp -> AnExp -> Exp
If :: AnExp -> AnExp -> AnExp -> Exp
Lambda :: AnPat -> AnExp -> Exp
Let :: [AnDecl] -> AnExp -> Exp
Lit :: Literal -> Exp
List :: [AnExp] -> Exp
ListComp :: [AnExp] -> [AnStmt] -> Exp
ListEnumFrom :: AnExp -> Exp
ListEnumFromTo :: AnExp -> AnExp -> Exp
ListLength :: AnExp -> Exp
MathsBinaryOp :: BinaryMathsOp -> AnExp -> AnExp -> Exp
MathsUnaryOp :: UnaryMathsOp -> AnExp -> Exp
Paren :: AnExp -> Exp
Set :: [AnExp] -> Exp
SetComp :: [AnExp] -> [AnStmt] -> Exp
SetEnum :: [AnExp] -> Exp
SetEnumComp :: [AnExp] -> [AnStmt] -> Exp
SetEnumFrom :: AnExp -> Exp
SetEnumFromTo :: AnExp -> AnExp -> Exp
Tuple :: [AnExp] -> Exp
Var :: QualifiedName -> Exp
AlphaParallel :: AnExp -> AnExp -> AnExp -> AnExp -> Exp
Exception :: AnExp -> AnExp -> AnExp -> Exp
ExternalChoice :: AnExp -> AnExp -> Exp
GenParallel :: AnExp -> AnExp -> AnExp -> Exp
GuardedExp :: AnExp -> AnExp -> Exp
Hiding :: AnExp -> AnExp -> Exp
InternalChoice :: AnExp -> AnExp -> Exp
Interrupt :: AnExp -> AnExp -> Exp
Interleave :: AnExp -> AnExp -> Exp
LinkParallel :: AnExp -> [(AnExp, AnExp)] -> [AnStmt] -> AnExp -> Exp
Prefix :: AnExp -> [AnField] -> AnExp -> Exp
Rename :: AnExp -> [(AnExp, AnExp)] -> [AnStmt] -> Exp
SequentialComp :: AnExp -> AnExp -> Exp
SlidingChoice :: AnExp -> AnExp -> Exp
ReplicatedAlphaParallel :: [AnStmt] -> AnExp -> AnExp -> Exp
ReplicatedExternalChoice :: [AnStmt] -> AnExp -> Exp
ReplicatedInterleave :: [AnStmt] -> AnExp -> Exp
ReplicatedInternalChoice :: [AnStmt] -> AnExp -> Exp
ReplicatedLinkParallel :: [(AnExp, AnExp)] -> [AnStmt] -> AnExp -> Exp
ReplicatedParallel :: AnExp -> [AnStmt] -> AnExp -> Exp
ExpPatWildCard :: Exp
ExpPatDoublePattern :: AnExp -> AnExp -> Exp
data Field

-- | !x
Output :: AnExp -> Field

-- | ?x:A
Input :: AnPat -> (Maybe AnExp) -> Field

-- | $x:A (see P395 UCS)
NonDetInput :: AnPat -> (Maybe AnExp) -> Field
data Stmt
Generator :: AnPat -> AnExp -> Stmt
Qualifier :: AnExp -> Stmt
data InteractiveStmt
Evaluate :: AnExp -> InteractiveStmt
Bind :: AnDecl -> InteractiveStmt
RunAssertion :: Assertion -> InteractiveStmt
data Decl
FunBind :: Name -> [AnMatch] -> Decl
PatBind :: AnPat -> AnExp -> Decl
Assert :: Assertion -> Decl
External :: [Name] -> Decl
Transparent :: [Name] -> Decl
Channel :: [Name] -> (Maybe AnExp) -> Decl
DataType :: Name -> [AnDataTypeClause] -> Decl
NameType :: Name -> AnExp -> Decl
data Assertion
Refinement :: AnExp -> Model -> AnExp -> [ModelOption] -> Assertion
PropertyCheck :: AnExp -> SemanticProperty -> (Maybe Model) -> Assertion
BoolAssertion :: AnExp -> Assertion
ASNot :: Assertion -> Assertion
data Model
Traces :: Model
Failures :: Model
FailuresDivergences :: Model
Refusals :: Model
RefusalsDivergences :: Model
Revivals :: Model
RevivalsDivergences :: Model
data ModelOption
TauPriority :: AnExp -> ModelOption
data SemanticProperty
DeadlockFreedom :: SemanticProperty
Deterministic :: SemanticProperty
LivelockFreedom :: SemanticProperty
data DataTypeClause
DataTypeClause :: Name -> (Maybe AnExp) -> DataTypeClause
data Match
Match :: [[AnPat]] -> AnExp -> Match
data Pat
PConcat :: AnPat -> AnPat -> Pat
PDotApp :: AnPat -> AnPat -> Pat
PDoublePattern :: AnPat -> AnPat -> Pat
PList :: [AnPat] -> Pat
PLit :: Literal -> Pat
PParen :: AnPat -> Pat
PSet :: [AnPat] -> Pat
PTuple :: [AnPat] -> Pat
PVar :: Name -> Pat
PWildCard :: Pat
PCompList :: [AnPat] -> (Maybe (AnPat, [AnPat])) -> Pat -> Pat
PCompDot :: [AnPat] -> Pat -> Pat
instance Eq Literal
instance Show Literal
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 Pat
instance Show Pat
instance Eq Exp
instance Show Exp
instance Eq Stmt
instance Show Stmt
instance Eq Field
instance Show Field
instance Eq Decl
instance Show Decl
instance Eq Assertion
instance Show Assertion
instance Eq ModelOption
instance Show ModelOption
instance Eq DataTypeClause
instance Show DataTypeClause
instance Eq Match
instance Show Match
instance Eq Module
instance Show Module
instance Show InteractiveStmt

module CSPM.PrettyPrinter
prettyPrint :: PrettyPrintable a => a -> Doc
prettyPrintMatch :: Name -> AnMatch -> Doc
instance PrettyPrintable Literal
instance PrettyPrintable Stmt
instance PrettyPrintable Field
instance PrettyPrintable Exp
instance PrettyPrintable UnaryMathsOp
instance PrettyPrintable BinaryMathsOp
instance PrettyPrintable UnaryBooleanOp
instance PrettyPrintable BinaryBooleanOp
instance PrettyPrintable Pat
instance PrettyPrintable DataTypeClause
instance PrettyPrintable SemanticProperty
instance PrettyPrintable ModelOption
instance PrettyPrintable Model
instance PrettyPrintable Assertion
instance PrettyPrintable Decl
instance PrettyPrintable InteractiveStmt
instance PrettyPrintable Module
instance PrettyPrintable [Module]
instance PrettyPrintable QualifiedName
instance PrettyPrintable Name

module CSPM.Desugar
class Desugarable a
desugar :: Desugarable a => a -> a
desugarWithType :: Desugarable a => a -> Type -> a
instance Desugarable Literal
instance Desugarable Pat
instance Desugarable InteractiveStmt
instance Desugarable Stmt
instance Desugarable Field
instance Desugarable Exp
instance Desugarable Match
instance Desugarable DataTypeClause
instance Desugarable ModelOption
instance Desugarable Assertion
instance Desugarable Decl
instance Desugarable Module
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 :: Integer -> 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
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 <a>strip</a>, but applies only to the left side of the string.
lstrip :: String -> String

-- | Same as <a>strip</a>, 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 = HierarchicalMap Name Value

module CSPM.Evaluator.Exceptions
patternMatchFailureMessage :: SrcSpan -> AnPat -> Value -> ErrorMessage
funBindPatternMatchFailureMessage :: SrcSpan -> Name -> [[Value]] -> ErrorMessage
typeCheckerFailureMessage :: String -> ErrorMessage

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
addScopeAndBind :: [(Name, Value)] -> EvaluationMonad a -> EvaluationMonad a
addScopeAndBindM :: EvaluationMonad [(Name, Value)] -> EvaluationMonad a -> EvaluationMonad a
throwError :: ErrorMessage -> a
instance Monad (LazyEvalMonad a)

module CSPM.Evaluator.Values
data Value
VInt :: Integer -> Value
VBool :: Bool -> Value
VTuple :: [Value] -> Value
VDot :: [Value] -> Value
VEvent :: Name -> [Value] -> Value
VDataType :: Name -> [Value] -> Value
VList :: [Value] -> Value
VSet :: ValueSet -> Value
VFunction :: ([Value] -> EvaluationMonad Value) -> Value
VProc :: Proc -> Value
data Proc
PAlphaParallel :: [(EventSet, Proc)] -> Proc
PException :: Proc -> EventSet -> Proc -> Proc
PExternalChoice :: [Proc] -> Proc
PGenParallel :: EventSet -> [Proc] -> Proc
PHide :: Proc -> EventSet -> Proc
PInternalChoice :: [Proc] -> Proc
PInterrupt :: Proc -> Proc -> Proc
PInterleave :: [Proc] -> Proc
PPrefix :: Event -> Proc -> Proc
PSequentialComp :: Proc -> Proc -> Proc
PSlidingChoice :: Proc -> Proc -> Proc

-- | PLinkParallel EventMap [Proc] | PRename EventMap Proc | POperator
--   ProcOperator Proc where: data ProcOperator = Normalise | Explicate |
--   StrongBisim | TauLoopFactor | Diamond | ModelCompress
PProcCall :: ProcName -> (Maybe Proc) -> Proc

-- | 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
procId :: Name -> [[Value]] -> String
valueEventToEvent :: Value -> Event
instance Show Value
instance PrettyPrintable Value
instance Ord Value
instance Eq Value

module CSPM.Evaluator.ValueSet
data ValueSet
Integers :: ValueSet
Processes :: ValueSet
ExplicitSet :: (Set Value) -> ValueSet
IntSetFrom :: Integer -> ValueSet
RangedSet :: Integer -> Integer -> ValueSet
LazySet :: [Value] -> ValueSet

-- | Produces a ValueSet of the carteisan product of several ValueSets,
--   using <tt>vc</tt> 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
allSequences :: ValueSet -> ValueSet

-- | The empty set
emptySet :: ValueSet

-- | Converts a list to a set
fromList :: [Value] -> ValueSet

-- | Converts a set to list.
toList :: ValueSet -> [Value]

-- | Returns the value iff the set contains one item only
singletonValue :: ValueSet -> Maybe Value
member :: Value -> ValueSet -> Bool
card :: ValueSet -> Integer
empty :: ValueSet -> Bool
mapMonotonic :: (Value -> Value) -> ValueSet -> ValueSet
unions :: [ValueSet] -> ValueSet
intersections :: [ValueSet] -> ValueSet
union :: ValueSet -> ValueSet -> ValueSet
intersection :: ValueSet -> ValueSet -> ValueSet
difference :: ValueSet -> ValueSet -> ValueSet
valueSetToEventSet :: ValueSet -> EventSet
instance Show ValueSet
instance PrettyPrintable ValueSet
instance Ord ValueSet
instance Eq ValueSet

module CSPM.Evaluator.BuiltInFunctions
builtInFunctions :: [(Name, Value)]
injectBuiltInFunctions :: EvaluationMonad a -> EvaluationMonad a

module CSPM.Evaluator.PatBind
class Bindable a
bind :: Bindable a => a -> Value -> EvaluationMonad (Bool, [(Name, Value)])
bindAll :: Bindable a => [a] -> [Value] -> EvaluationMonad (Bool, [(Name, Value)])
instance Bindable Pat
instance Bindable a => Bindable (Annotated b a)

module CSPM.Evaluator.DeclBind
bindDecls :: [TCDecl] -> EvaluationMonad [(Name, Value)]
valuesForChannel :: Name -> EvaluationMonad [ValueSet]
valuesForDataTypeClause :: Name -> EvaluationMonad [ValueSet]

module CSPM.Evaluator.Module
bindModules :: [TCModule] -> EvaluationMonad [(Name, Value)]
bindModule :: TCModule -> EvaluationMonad [(Name, Value)]

module CSPM.Evaluator.Expr
class Evaluatable a
eval :: Evaluatable a => a -> EvaluationMonad Value
instance Evaluatable Exp
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, Value)]

-- | Evaluates the declaration but doesn't add it to the current
--   environment.
evaluateFile :: [TCModule] -> EvaluationMonad [(Name, Value)]
getBoundNames :: EvaluationMonad [Name]
addToEnvironment :: EvaluationMonad [(Name, 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

module CSPM.Parser
parseFile :: String -> ParseMonad [PModule]
parseInteractiveStmt :: String -> ParseMonad PInteractiveStmt
parseExpression :: String -> ParseMonad PExp
parseStringAsFile :: String -> ParseMonad [PModule]
type ParseMonad = StateT ParserState IO
runParser :: ParseMonad a -> String -> IO a

module CSPM.TypeChecker.Environment
type Environment = HierarchicalMap 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 -> Bool -> SymbolInformation

-- | The type of the symbol
typeScheme :: SymbolInformation -> TypeScheme

-- | Is this symbol deprecated
isDeprecated :: SymbolInformation -> Bool

-- | 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
varNotInScopeMessage :: Name -> Error
infiniteUnificationMessage :: Type -> Type -> Error
unificationErrorMessage :: [(Type, Type)] -> Error
duplicatedDefinitionsMessage :: [(Name, SrcSpan)] -> [Error]
incorrectArgumentCountMessage :: Doc -> Int -> Int -> Error
constraintUnificationErrorMessage :: Constraint -> Type -> Error
transparentFunctionNotRecognised :: Name -> Error
externalFunctionNotRecognised :: Name -> 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 :: TypeCheckMonad Type
freshTypeVarWithConstraints :: [Constraint] -> TypeCheckMonad Type

-- | Get the type of <tt>n</tt> and throw an exception if it doesn't exist.
getType :: Name -> TypeCheckMonad TypeScheme

-- | Get the type of <tt>n</tt> if it exists, othewise return Nothing.
safeGetType :: Name -> TypeCheckMonad (Maybe TypeScheme)

-- | Sets the type of n to be t in the current scope only. No unification
--   is performed.
setType :: Name -> TypeScheme -> TypeCheckMonad ()
isDeprecated :: Name -> TypeCheckMonad Bool
isTypeUnsafe :: Name -> TypeCheckMonad Bool
markAsDeprecated :: Name -> TypeCheckMonad ()
markTypeAsUnsafe :: 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 <tt>st</tt>. If any errors
--   are encountered then a <a>SourceError</a> will be thrown with the
--   relevent error messages.
runTypeChecker :: TypeInferenceState -> TypeCheckMonad a -> IO a
newTypeInferenceState :: TypeInferenceState
data TypeInferenceState
TypeInferenceState :: Environment -> [Name] -> Int -> 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]

-- | Next TypeVar to be allocated
nextTypeId :: TypeInferenceState -> Int

-- | 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
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 ()
externalFunctions :: PartialFunction String Type
transparentFunctions :: PartialFunction String Type
builtInNames :: [String]
replacementForDeprecatedName :: Name -> Maybe Name

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
instance Compressable InteractiveStmt
instance Compressable Stmt
instance Compressable Field
instance Compressable Match
instance Compressable DataTypeClause
instance Compressable ModelOption
instance Compressable Assertion
instance Compressable Decl
instance Compressable Module
instance Compressable Exp
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 -> TypeCheckMonad [Name]
namesBoundByDecl' :: Decl -> StateT TypeInferenceState IO [Name]
class FreeVars a
freeVars :: FreeVars a => a -> TypeCheckMonad [Name]
instance FreeVars Field
instance FreeVars Stmt
instance FreeVars Pat
instance FreeVars a => FreeVars (Annotated b a)
instance FreeVars a => FreeVars [a]
instance Dependencies DataTypeClause
instance Dependencies Match
instance Dependencies ModelOption
instance Dependencies Assertion
instance Dependencies Decl
instance Dependencies Field
instance Dependencies Stmt
instance Dependencies Exp
instance Dependencies Pat
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 <tt>names</tt>
--   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 Type
instance TypeCheckable PPat Type

module CSPM.TypeChecker.Expr
instance TypeCheckable Exp Type
instance TypeCheckable PExp Type

module CSPM.TypeChecker.Decl

-- | Type check a list of possibly mutually recursive functions
typeCheckDecls :: [PDecl] -> TypeCheckMonad ()
instance TypeCheckable Match Type
instance TypeCheckable PMatch Type
instance TypeCheckable DataTypeClause (Name, [Type])
instance TypeCheckable PDataTypeClause (Name, [Type])
instance TypeCheckable ModelOption ()
instance TypeCheckable Assertion ()
instance TypeCheckable Decl [(Name, Type)]
instance TypeCheckable PDecl [(Name, Type)]

module CSPM.TypeChecker.InteractiveStmt
instance TypeCheckable InteractiveStmt ()
instance TypeCheckable PInteractiveStmt ()

module CSPM.TypeChecker.Module
instance TypeCheckable Module ()
instance TypeCheckable PModule ()
instance TypeCheckable [PModule] ()

module CSPM.TypeChecker
typeCheck :: (Compressable a, TypeCheckable a b) => a -> TypeCheckMonad a
typeCheckExpect :: (Compressable a, TypeCheckable a Type) => Type -> a -> TypeCheckMonad a
typeOfExp :: PExp -> 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 <tt>st</tt>. If any errors
--   are encountered then a <a>SourceError</a> will be thrown with the
--   relevent error messages.
runTypeChecker :: TypeInferenceState -> TypeCheckMonad a -> IO a
runFromStateToState :: TypeInferenceState -> TypeCheckMonad a -> IO (a, [ErrorMessage], TypeInferenceState)

module CSPM

-- | A <a>CSPMSession</a> represents the internal states of all the various
--   components.
data CSPMSession

-- | Create a new <a>CSPMSession</a>.
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 <a>CSPM</a>) 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 ()
withSession :: CSPMMonad m => (CSPMSession -> m a) -> m a
type CSPM = StateT CSPMSession IO
unCSPM :: CSPMSession -> CSPM a -> IO (a, CSPMSession)

-- | Parses a string, treating it as though it were a file. Throws a
--   <a>SourceError</a> on any parse error.
parseStringAsFile :: CSPMMonad m => String -> m [PModule]

-- | Parse a file <tt>fp</tt>. Throws a <a>SourceError</a> on any parse
--   error.
parseFile :: CSPMMonad m => FilePath -> m [PModule]

-- | Parses an <a>InteractiveStmt</a>. Throws a <a>SourceError</a> on any
--   parse error.
parseInteractiveStmt :: CSPMMonad m => String -> m PInteractiveStmt

-- | Parses an <a>Exp</a>. Throws a <a>SourceError</a> on any parse error.
parseExpression :: CSPMMonad m => String -> m PExp

-- | Type checks a file, also desugaring it. Throws a <a>SourceError</a> if
--   an error is encountered and will call handleWarnings
typeCheckFile :: CSPMMonad m => [PModule] -> m [TCModule]

-- | Type checks a <a>InteractiveStmt</a>.
typeCheckInteractiveStmt :: CSPMMonad m => PInteractiveStmt -> m TCInteractiveStmt
typeCheckExpression :: CSPMMonad m => PExp -> m TCExp
ensureExpressionIsOfType :: CSPMMonad m => Type -> PExp -> m TCExp
dependenciesOfExp :: CSPMMonad m => TCExp -> m [Name]

-- | Gets the type of the expression in the current context.
typeOfExpression :: CSPMMonad m => PExp -> m Type

-- | Evaluates the expression in the current context.
evaluateExp :: CSPMMonad m => TCExp -> m Value

-- | Binds all the declarations that are in a particular file.
bindFile :: CSPMMonad m => [TCModule] -> m ()

-- | Takes a declaration and adds it to the current environment.
bindDeclaration :: CSPMMonad m => TCDecl -> m ()

-- | Get a list of currently bound names in the environment.
getBoundNames :: CSPMMonad m => m [Name]

-- | Return the version of libcspm that is being used.
getLibCSPMVersion :: Version
instance CSPMMonad CSPM