psilo

CESKM

Description

The evaluation algorithm is presented as a small-step transition relation from a CESKM to either

• another CESKM if the computation is not finished; or
• a terminal Value if it is.

This machine is written to be, as much as possible, an executable semantics for psilo. Its code should be useful as a reference for writing evaluators in general and for clarifying the meaning of the language in a concrete way.

Hence there is a broad separation between the algorithm itself (principally defined by step and CESKM); and the array of utilities and helpers necessary to support that algorithm (starting with Runtime) so that the language semantics are not obscured by implementation details.

Synopsis

# Documentation

The top-level function taking an expression CbpvExp to either an error String or a result Value.

Runtime support for the CESK(M) algorithm. Runtime does the following:

• generates fresh, unique Addresses on demand (via gensym);
• provides a mechanism for throwing exceptions (throwError); and
• implements the operators (op) that are assumed to exist.

The actual evaluation algorithm begins with evaluate. See also: CESKM.

State managed by Runtime.

Constructors

 RuntimeState Fieldsgensym_val :: IntIncremented and returned to generate an Address.

Utility function for generating globally unique Addresses.

op :: Symbol -> [Value] -> Runtime Value Source #

This function provides implementations of the built-in operators.

# CESK(M) evaluation

data CESKM Source #

CESKM contains the state required for the operation of an abstract Control-string Environment Store Kontinuation Meta machine

Constructors

 CESKM Fieldscontrol :: CbpvExpThe expression being evaluatedenvironment :: EnvSymbol -> Address + Defnstore :: StoreAddress -> Valuekontinuation :: KontThe rest of the computationmeta :: [Kont]The meta-continuation: a LIFO stack of Konts.

data Kont Source #

A continuation annihilates with a Value during computation to either halt or transition to the next state.

Constructors

 Halt Bottom of the continuation stack. Argk [Value] Kont Arguments to be popped by a function binder. Letk Symbol CbpvExp Env Kont Sequencing between state transitions.

data Value Source #

A value is data which the machine actually stores, manipulates, and evaluates expressions to.

Constructors

 Closure CbpvExp Env A suspended computation Continuation Kont A captured continuation IntV Integer A literal integer. FloatV Double A literal floating point number. BoolV Bool A literal boolean value.

#### Instances

Instances details
 Source # Instance detailsDefined in CESKM MethodsshowsPrec :: Int -> Value -> ShowS #show :: Value -> String #showList :: [Value] -> ShowS #

Represents a single step of a virtual machine state transition. The function is not recursive although several of its constituent parts are.

Drives each step of the virtual machine until termination or error.

Construct an initial CESKM with a given control expression.

Induces a state machine transition during evaluation.

Halts the termination of a CESK(M) computation.

# Environment & Store

type Address = Int Source #

The Store maps Addresses to Runtime Values.

data Env Source #

Binds symbols to either Addresses or CbpvExp definitions.

data Store Source #

Binds Addresses to Values.