Documentation

Creates a list of funcon terms.

Creates a tuple of funcon terms.

Creates a set of funcon terms.

Creates an integer literal.

Creates a natural literal.

Creates a string literal.

left-to-right(X1,...,Xn) executes X1 ,...,Xn from left to right, computing a tuple of result values (V1,...,VN) .

atomic(X) treats the complete evaluation of X as one step, regardless of how many steps that evaluation actually takes.

sequential(X1,...,Xn) executes X1 ,...,Xn from left to right, computing a tuple of results. Any result values that are the empty tuple () are discarded, so the resultant tuple may be smaller.

vector-map(F,V) maps the computation F over the vector V , from left to right, evaluating F for each given value in V .

set-map(F,S) maps the computation F over the set S , interleaved, evaluating F for each given value in S , uniting the results.

list-map(F,L) maps the computation F over the list L , from left to right, evaluating F for each given value in L .

tuple-map(F,Tup) maps the computation F over a tuple Tup , from left to right, evaluating F for each given value in the Tup .

map-map(X,M) maps the computation F over the map M , interleaved, evaluating F for each given keyentry pair in M/ , uniting the results.

lists-map(F,(List+)) maps the computation F over N lists of equal length L, in parallel from left to right. F is evaluated L times, once for each given tuple of argument values, where the Nth component of each tuple is drawn from the Nth argument list.

multiset-filter(P,MS) deletes all values from the the multiset MS that do not satisfy the predicate P . P is given a values /naturals pair.

set-filter(P,S) deletes all entries from the the set S that do not satisfy the predicate P .

map-filter(P,M) discards all entries from the map M that do not satisify the predicate P . P is given a key/value pair.

list-filter(P,L) discards all elements from the list L that do not satisify the predicate P .

list-foldl(F,A,L) reduces a list L to a single value by folding it from the left, using A as the initial accumulator value, and iteratively updating the accumulator by executing the computation F with the accumulator value and the head of the remaining list as its pair of arguments.

list-foldr(F,A,L) reduces a list L to a single value by folding it from the right, using A as the initial accumulator value, and iteratively updating the accumulator by executing the computation F with the the last element of the remaining list and the accumulator value as its pair of arguments.

while(B,C) first evaluates B . Depending on whether the computed value is true or false , it then executes C and repeats, or terminates normally.

do-while(C,B) first executes C . Then it evaluates B . Depending on whether the value is true or false , it then repeats, or terminates normally.

if-then-else(B,X,Y) first evaluates B . Depending on whether the computed value is true or false , it then evaluates X or Y .

stuck cannot be evaluated.

handle-thrown(E,H) evaluates E . If E terminates normally with value V , then V is returned and H is ignored. If E terminates abruptly with value V , then H is executed with given-value V .

finally(C,F) first executes C . If C terminates normally, then F executes. If C abruptly terminates with a thrown value V , then F executes, and then V is rethrown.

throw(V) terminates abruptly with value V .

handle-recursively behaves similarly to handle-thrown , except that another copy of the handler attempts to handle any values thrown by the handler. Thus, many thrown values may get caught by the same handler.

plug(E,V) plugs the value V into a hole that occurs as a subterm within the computation E , provided the hole is in an evaluable position.

shift(F) emits a control-signal that, when handled by an enclosing reset , will cause F to the current continuation of shift(F) , Unlike control , any application of the captured continuation delimits any control operators in its body.

prompt is a delimiter for the control and call-cc operators.

control(F) emits a control-signal that, when handled by an enclosing prompt , will cause F to the current continuation of control(F) , instead of continuing the current computation.

call-cc(F) emits a control-signal that, when handled by an enclosing prompt , applies F to the current continuation. If that current continuation argument is invoked, then the current computation will terminate up to the enclosing prompt when that continuation terminates.

reset is a delimiter for the shift operator. A consequence of our choice of definition of shift is that the semantics of reset conincide exactly with those of prompt , and thus the two can be used interchangeably.

A hole in a term cannot proceed until it receives a resume-signal containing a value to fill the hole.

abort(V) emits a control-signal that, when handled by an enclosing prompt , aborts the current computation up to that enclosing prompt , returning the value V .

else(X1,X2,...,XN) evaluates each computation X in turn, until one does *not*fail, returning the result of the successful computation.

check-true(B) fails if B is false .

fail terminates abruptly.

dereference(P) fails if the pointer P is null , otherwise it returns the value referenced by P .

print-list(L) emits the values contained in the list L on the standard-out .

print(E) evaluates E and emits the resulting value on the standard-out .

read consumes a single value from the standard-in , and returns it.

effect(E) evaluates E , then discards the computed value.

allocate-map(M) computes a map where the entries are uninitialised variables of types given by M .

general-assign(Var,Val) assigns the (potentially composite) value Val to the (potentialy composite) variable Var .

general-assigned(V) takes a (potentially composite) value V , which may contain variables , and computes the value of V with all such contained variables replaced by the values currently assigned to those variables.

allocate-vector(T,N) computes a vector of length N , containing uninitialised variables of type T .

If V is a variable, current-value(V) computes the value currently assigned to V . Otherwise it evaluates to V .

assigned(Var) gives the value currently assigned to the variable Var . If this value is uninitialised , then computation fail s.

allocate-initialised-variable(T,V) computes a simple variable for storing values of type T , and initialises its value to V . This fail s if the type of V is not a subtype of T .

allocate-variable(T) computes an (uninitialised) simple variable for storing values of type T .

deallocate-variable(V) deletes the variable V from the current store .

assign(Var,Val) assigns Val to the the variable Var , provided Var has not been deallocated and Val is of the appropriate type for storing in Var .

variable-accepting-type(Var) returns the type of values that Var accepts. variable-producing-type(Var) returns the type of values that Var can produce.

allocate-initialised-link(T,V) computes a link to values of type T , and sets its value to V . This fail s if the type of V is not a subtype of T .

allocate-link(T) computes a link to values of type T .

If V is a link, then follow-if-link(V) gives the value to which the link V has been set. Otherwise, V is returned.

link-accepting-type(L) returns the type of values that L accepts. link-producing-type(L) returns the type of values that L can produce.

follow-link(L) gives the value linked to by L . If this value is uninitialised , then computation fail s.

set-link(L,V) sets the value linked to by L to be V . If L has already been set, then computation instead fail s.

given returns the current given value.

given1 returns the first component of the currently given tuple. given2 returns the second component of the currently given tuple. given3 returns the third component of the currently given tuple.

give(V,X) evaluates X with V as the given value.

fresh-atom computes a fresh atom, distinct from all other atoms previously generated by other occurrences of fresh-atom .

fresh-binder generates a fresh binder, distinct from all identifiers and any binders previously generated by other occurrences of fresh-binder .

recursive(Bs,D) evaluates D with potential recursion on the binders in Bs (which need not be the same as the set of binders bound by D ).

bind-recursively(B,E) binds B to the result of evaluating E , which may recursively refer to B (using bound-recursively ).

bound-recursively(B) returns the value currently bound to B , unless that value is a links , in which case it returns the value linked to by that link. This is intended to be used in situations when the binder B may be a recursive binding formed using recursive or bind-recursively .

bound(B) returns the value currently bound to the binder B ,

scope(Rho,X) extends (possibly overriding) the current environment with Rho for the execution of X .

accumulate(D1,D*) first evaluates D1 to Rho1 . It then lets Rho1 override the current environment during the evaluation of accumulate(D*) to Rho2 , and finally computes Rho2 overriding Rho1 . accumulate() computes map-empty .

bind(B,V) gives the environment binding the binder B to the value V .

is-in-type(V,T) tests membership of a value in a type.

variants(M) is the type of tagged values variant(K,V) where V . variant-tag(V) returns the tag of a variant V variant-value(V) returns the tagged value of a variant V

is-null tests an arbitrary value to determine if it is equal to null .

newline is the string containing only a line feed character (LF or "n").

An ieee-floats is either one of four special values: quiet-not-a-number , signals-not-a-number , positive-infinity , negative-infinity or is represented (internally) as a triple (S,C,Q). S is a sign bit: 0 denotes "+" and 1 denotes "-". C and Q determine the value. - In binary format the value is: C x 2^Q - In decimal format the value is: C x 10^Q

booleans is the type of truth-values. not(_) is logical negation. and(...) is logical conjunction of a tuple of booleans . or(...) is logical disjunction of a tuple of booleans . xor(_,_) is exclusive disjunction of two booleans . implies(_,_) is logical implication between two booleans . is-equal(_,_) tests equality of arbitrary values .

close(_) closes a thunked computation with respect to the current environment.

closure(X,Rho) evaluates X using Rho as the current environment.

pattern-prefer(P1,P2) is a pattern that attempts to match the value against P1 . If this succeeds then the resulting environment is returned. Otherwise, the value is matched against P2 .

match(V,P) matches the (potentially composite) value V against the (potentially composite) pattern P .

pattern-unite(P1,P2) is a pattern that requires the matched value to match both P1 and P2 , uniting the resulting environments .

pattern-any is a pattern that matches any value, computing the empty environment.

case(P,X) attempts to match the (potentially composite) given-value against the (potentially composite) pattern P . If successful, X is executed in the scope of any computed bindings. Otherwise, it fails.

match-loosely(V,P) loosely matches the (potentially composite) value V against the (potentially composite) pattern P . In the case of sets , maps and vectors , the pattern may be a sub-setsub-multisetsub-map/ sub-vector of the value being matched against (recursively).

pattern-bind(B) is a pattern that matches any value V , computing the singleton environment {B |-> V}

A ground-value is any (potentially composite) value that does not contain thunks anywhere within it.

apply(F,V) applies the function F to the value V .

supply(V,F) supplies V as the argument to the function F , without executing the function. The result is a thunk that does not depend on an argument when forced.

binding-lambda(B,E) computes a statically scoped function (i.e. a closed thunk). When applied to a value V , free occurrences of bound(B) in E refer to V .

curry(F) converts a function that takes a pair of arguments into a function that takes the first argument of the pair, and returns a function that takes the second argument of the pair.

lambda(E) computes a statically scoped function (i.e. a closed thunk). When applied to a value V , free occurrences of given in E refer to V .

uncurry(F) converts a function that computes a function into a single function that takes both arguments as a pair.

partial-apply(F,V) provides V as the first argument to a function expecting a pair of arguments, returning a function expecting only the second argument.

compose(G,F) composes two functions G and F by giving the result of F as the argument to G .

Funcons for inserting a value to a list.

Funcons representing the empty list.

Computes the union over a sequence of maps. If the maps do not have disjoint domains a failure signal is raised.

Computes the left-biased union over two maps.

Concatenate a sequence of strings.