Internal representation of funcon terms. The generic constructors FName and FApp use names to represent nullary funcons and applications of funcons to other terms. Funcon terms are easily created using applyFuncon or via the smart constructors exported by Funcons.Core.

Representation of builtin types.

Postfix operators for specifying sequences.

Build funcon terms by applying a funcon name to `zero or more' funcon terms. This function is useful for defining smart constructors, e,g,

handle_thrown_ :: [Funcons] -> Funcons
handle_thrown_ = applyFuncon "handle-thrown"

or alternatively,

handle_thrown_ :: Funcons -> Funcons -> Funcons
handle_thrown_ x y = applyFuncon "handle-thrown" [x,y]

Creates a set of funcon terms.

Create an environment from a list of bindings (String to Values) This function has been introduced for easy expression of the semantics of builtin identifiers

Creates an integer literal.

Creates a natural literal.

Creates a string literal.

Creates an atom from a String.

Creates a tuple of funcon terms. tuple_ :: [Funcons] -> Funcons tuple_ = FTuple

Pretty-print a Values.

Pretty-print a sequence of Values.

Pretty-print a Funcons.

Pretty-print a sequence of Funcons.

Pretty-print a Types.

Returns the unicode representation of an assci value. Otherwise it returns the original value.

Attempt to downcast a funcon term to a value.

Returns the natural representation of a value if it is a subtype. Otherwise it returns the original value.

Returns the integer representation of a value if it is a subtype. Otherwise it returns the original value.

Returns the rational representation of a value if it is a subtype. Otherwise it returns the original value.

Evaluation functions capture the operational behaviour of a funcon. Evaluation functions come in multiple flavours, each with a different treatment of the arguments of the funcon. Before the application of an evaluation funcon, any argument may be evaluated, depending on the Strictness of the argument.

Denotes whether an argument of a funcon should be evaluated or not.

Type synonym for the evaluation function of strict funcons. The evaluation function of a StrictFuncon receives fully evaluated arguments.

Type synonym for the evaluation function of non-strict funcons.

Type synonym for the evaluation function of fully non-strict funcons.

Type synonym for value operations.

Type synonym for the evaluation functions of nullary funcons.

A funcon library maps funcon names to their evaluation functions.

Creates an empty FunconLibrary.

Unites two FunconLibrarys.

Right-based union of FunconLibrarys

Unites a list of FunconLibrarys.

Right-based union of list of FunconLibrarys

Creates a FunconLibrary from a list.

A funcon library with funcons for builtin types.

Monadic type for the propagation of semantic entities and meta-information on the evaluation of funcons. The meta-information includes a library of funcons (see FunconLibrary), a typing environment (see TypeRelation), runtime options, etc.

The semantic entities are divided into five classes:

• inherited entities, propagated similar to values of a reader monad.
• mutable entities, propagated similar to values of a state monad.
• output entities, propagation similar to values of a write monad.
• control entities, similar to output entities except only a single control signal can be emitted at once (signals do not form a monoid).
• input entities, propagated like values of a state monad, but access like value of a reader monad. This package provides simulated input/outout and real interaction via the IO monad. See Funcons.Tools.

For each entity class a map is propagated, mapping entity names to values. This enables modular access to the entities.

Monadic type for the implicit propagation of meta-information on the evaluation of funcon terms (no semantic entities). It is separated from MSOS to ensure that side-effects (access or modification of semantic entities) can not occur during syntactic rewrites.

After a term is fully rewritten it is either a value or a term that requires a computational step to proceed. This types forms the interface between syntactic rewrites and computational steps.

Yield a funcon term as the result of a syntactic rewrite. This function must be used instead of return. The given term is fully rewritten.

Yield a sequence of funcon terms as the result of a rewrite. This is only valid when all terms rewrite to a value

Yield a funcon term as the result of an MSOS computation. This function must be used instead of return.

Yield a sequence of funcon terms as the result of a computation. This is only valid when all terms rewrite to a value

Yield an MSOS computation as a fully rewritten term. This function must be used in order to access entities in the definition of funcons.

Returns a value as a fully rewritten term.

Execute a premise as either a rewrite or a step. Depending on whether only rewrites are necessary to yield a value, or whether a computational step is necessary, a different continuation is applied (first and second argument). Example usage:

stepScope :: NonStrictFuncon --strict in first argument
stepScope [FValue (Map e1), x] = premiseEval x rule1 step1 
 where   rule1 v  = rewritten v
         step1 stepX = do   
             Map e0  <- getInh "environment"
             x'      <- withInh "environment" (Map (union e1 e0)) stepX
             stepTo (scope_ [FValue e1, x'])

Yields an error signaling that no rule is applicable. The funcon term argument may be used to provide a useful error message.

Yields an error signaling that a sort error was encountered. These errors render a rule inapplicable and a next rule is attempted when a backtracking procedure like evalRules is applied. The funcon term argument may be used to provide a useful error message.

Yields an error signaling that a partial operation was applied to a value outside of its domain (e.g. division by zero). These errors render a rule inapplicable and a next rule is attempted when a backtracking procedure like evalRules is applied. The funcon term argument may be used to provide a useful error message.

a map storing the values of inherited entities.

Get the value of an inherited entity.

Set the value of an inherited entity. The new value is only set for MSOS computation given as a third argument.

A map storing the values of mutable entities.

Get the value of some mutable entity.

Set the value of some mutable entity.

a map storing the values of output entities.

Add new values to a certain output entity.

Read the values of a certain output entity. The output is obtained from the MSOS computation given as a second argument.

a map storing the values of control entities.

Signal a value of some control entity.

Receive the value of a control entity from a given MSOS computation.

A map storing the values of input entities.

Provides extra values to a certain input entity, available to be consumed by the given MSOS computation argument.

Provides an exact amount of input for some input entity, that is to be completely consumed by the given MSOS computation. If less output is consumed a 'insufficient input consumed' exception is thrown.

Funcon term representation identical to Funcons, but with meta-variables.

An environment mapping meta-variables to funcon terms. This environment is used by a substitution procedure to transform funcon terms from FTerm representation to Funcons.

The empty substitution environment. Bindings are inserted by pattern-matching.

Variant of rewriteTo that applies substitution.

Variant of stepTo that applies substitution.

Variant of premiseStep that applies substitute and pattern-matching.

Variant of withInh that performs substitution.

Version of getInh that applies pattern-matching.

Variant of putMut that applies substitution.

Variant of getMut that performs pattern-matching.

Variant of writeOut that applies substitution.

Variant of readOut that performs pattern-matching.

Variant of receiveSignal that performs pattern-matching.

Variant of raiseSignal that applies substitution.

Variant of consumeInput that matches the given VPattern to the consumed value in the given Env.

Variant of withExtraInput that performs substitution.

Variant of withExactInput that performs substitution.

Version of getControl that applies pattern-matching.

Function evalRules implements a backtracking procedure. It receives two lists of alternatives as arguments, the first containing all rewrite rules of a funcon and the second all step rules. The first successful rule is the only rule fully executed. A rule is unsuccessful if it throws an exception. Some of these exceptions (partial operation, sort error or pattern-match failure) cause the next alternative to be tried. Other exceptions (different forms of internal errors) will be propagated further. All side-effects of attempting a rule are discarded when a rule turns out not to be applicable.

First all rewrite rules are attempted, therefore avoiding performing a step until it is absolutely necessary. This is a valid strategy as valid (I)MSOS rules can be considered in any order.

When no rules are successfully executed to completetion a 'no rule exception' is thrown.

CSB supports five kinds of side conditions. Each of the side conditions are explained below. When a side condition is not accepted an exception is thrown that is caught by the backtrackign procedure evalRules. A value is a ground value if it is not a thunk (and not composed out of thunks).

Executes a side condition, given an Env environment, throwing possible exceptions, and possibly extending the environment.

Variant of sideCondition that is lifted into the MSOS monad.

Patterns for matching values (Values).

Patterns for matching funcon terms (FTerm).

Matching values with value patterns patterns. If the list of patterns is a singleton list, then vsMatch attempts to match the values as a tuple against the pattern as well.

Match a sequence of terms to a sequence of patterns.

Variant of vsMatch that is lifted into the MSOS monad.

Variant of fsMatch that is lifted into the MSOS monad. If all given terms are values, then vsMatch is used instead.

Apply as many rewrites as possible to the term bound to the given variable in the meta-environment

Associates types (Terms) with meta-variables

Used for replacing meta-variables T in pattern annotations `P:T` with the type to which T is bound in some type-environment (if any)

Version of subsTypeVar that does not replace the meta-variables in the given set

Version of subsTypeVarWildcard that does not replace the meta-variables in the given set

Parameterisable evaluation function function for types.

A list of EntityDefaults is used to declare (and possibly initialise) entities.

Default values of entities can be specified for inherited and mutable entities.

The typing environment maps datatype names to their definitions.

A type parameter is of the form X:T where the name of the parameter,X, is optional. When present, X can be used to specify the type of constructors. Variable X be a sequence variable.

A datatype has `zero or more' type parameters and `zero or more' alternatives.

An alternative is either a datatype constructor or the inclusion of some other type. The types are arbitrary funcon terms (with possible variables) that may require evaluation to be resolved to a Types.

Lookup the definition of a datatype in the typing environment.

Unites two TypeRelations.

Unites a list of TypeRelations.

Creates a TypeRelation from a list.

The empty TypeRelation.