libcspm-1.0.0: A library providing a parser, type checker and evaluator for CSPM.

Safe HaskellNone




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 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:

Parses strings or files and produces an AST, parametrised by UnRenamedName, which are simply pieces of text.
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.
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.
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 False
        (value, resultingSession) <- unCSPM session $ do
            -- Parse the file, returning something of type PCSPMFile.
            parsedFile <- parseFile "test.csp"
            -- Rename the file, returning something of type TCCSPMFile.
            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.


CSPM Monad

data CSPMSession Source

A CSPMSession represents the internal states of all the various components.


class MonadIO m => CSPMMonad m whereSource

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.


getSession :: m CSPMSessionSource

Get the current session.

setSession :: CSPMSession -> m ()Source

Update the current session.

handleWarnings :: [ErrorMessage] -> m ()Source

This is called whenever warnings are emitted.


withSession :: CSPMMonad m => (CSPMSession -> m a) -> m aSource

Executes an operation giving it access to the current CSPMSession.

A basic implementation of the monad

type CSPM = StateT CSPMSession IOSource

A basic implementation of CSPMMonad, using the StateT monad. This prints out any warnings to stdout.

unCSPM :: CSPMSession -> CSPM a -> IO (a, CSPMSession)Source

Runs a CSPM function, returning the result and the resulting session.

Common Data Types

Defines the names that are used by machine CSP.

Defines the abstract syntax for machine CSP.

Defines the types used by the typechecker.

Defines the values produced by the evaluator.

Parser API

parseStringAsFile :: CSPMMonad m => String -> m PCSPMFileSource

Parses a string, treating it as though it were a file. Throws a SourceError on any parse error.

parseFile :: CSPMMonad m => FilePath -> m PCSPMFileSource

Parse a file fp. Throws a SourceError on any parse error.

parseInteractiveStmt :: CSPMMonad m => String -> m PInteractiveStmtSource

Parses a PInteractiveStmt. Throws a SourceError on any parse error.

parseExpression :: CSPMMonad m => String -> m PExpSource

Parses an Exp. Throws a SourceError on any parse error.

Renamer API

renameFile :: CSPMMonad m => PCSPMFile -> m TCCSPMFileSource

Renames a file.

renameInteractiveStmt :: CSPMMonad m => PInteractiveStmt -> m TCInteractiveStmtSource

Rename ian interactive statement.

renameExpression :: CSPMMonad m => PExp -> m TCExpSource

Renames an expression.

getBoundNames :: CSPMMonad m => m [Name]Source

Get a list of currently bound names in the environment.

Type Checker API

typeCheckFile :: CSPMMonad m => TCCSPMFile -> m TCCSPMFileSource

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.

typeCheckExpression :: CSPMMonad m => TCExp -> m TCExpSource

Type checkes a PExp, returning the desugared and annotated version.

ensureExpressionIsOfType :: CSPMMonad m => Type -> TCExp -> m TCExpSource

Given a Type, ensures that the PExp is of that type. It returns the annoated and desugared expression.

typeOfExpression :: CSPMMonad m => TCExp -> m TypeSource

Gets the type of the expression in the current context.

typeOfName :: CSPMMonad m => Name -> m TypeSchemeSource

Returns the type of the given name in the current context.

The file in which this name has been bound must have been typechecked using typeCheckFile.



:: CSPMMonad m 
=> Bool

If true includes functions that evaluate to processes.

-> m [Name] 

Returns all currently bound process names, optionally including functions that evaluate to processes

Desugarer API

desugarFile :: CSPMMonad m => TCCSPMFile -> m TCCSPMFileSource

Desugar a file, preparing it for evaulation.

desugarInteractiveStmt :: CSPMMonad m => TCInteractiveStmt -> m TCInteractiveStmtSource

Desugars an interactive statement.

desugarExpression :: CSPMMonad m => TCExp -> m TCExpSource

Desugars an expression.

Evaluator API

bindFile :: CSPMMonad m => TCCSPMFile -> m ()Source

Binds all the declarations that are in a particular file. Requires the file to be desugared.

bindDeclaration :: CSPMMonad m => TCDecl -> m ()Source

Takes a declaration and adds it to the current environment. Requires the declaration to be desugared.

evaluateExpression :: CSPMMonad m => TCExp -> m ValueSource

Evaluates the expression in the current context. Requires the expression to be desugared.

maybeProcessNameToProcess :: CSPMMonad m => ProcName -> m (Maybe UProc)Source

Given a process name, attempts to convert the name into a process. This is only possible for top-level function applications.

profilingData :: CSPMMonad m => m ProfilingDataSource

Obtains the profiling data that the evaluator has produced so far.


stringToValue :: CSPMMonad m => Type -> String -> m ValueSource

Takes an expression string and a type and evaluates the expression, providing the expression is of the correct type.

Low-Level API

Whilst this module provides many of the commonly used functionality within the CSPM monad, sometimes there are additional functions exported by other modules that are of use. The following functions allow the renamer, typechecker and evaluator to be run in the current state. They also save the resulting state in the current session.

runParserInCurrentState :: CSPMMonad m => FilePath -> ParseMonad a -> m aSource

Runs the parser.

runRenamerInCurrentState :: CSPMMonad m => RenamerMonad a -> m aSource

Runs renamer in the current state.

runTypeCheckerInCurrentState :: CSPMMonad m => TypeCheckMonad a -> m (a, [ErrorMessage])Source

Runs the typechecker in the current state, saving the resulting state and returning any warnings encountered.

runEvaluatorInCurrentState :: CSPMMonad m => EvaluationMonad a -> m aSource

Runs the evaluator in the current state, saving the resulting state.

reportWarnings :: CSPMMonad m => m (a, [ErrorMessage]) -> m aSource

Given a program that can return warnings, runs the program and raises any warnings found using handleWarnings.

Misc functions

getLibCSPMVersion :: VersionSource

Return the version of libcspm that is being used.