psilo
Safe HaskellNone
LanguageHaskell2010

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

evaluate :: CbpvExp -> Either String (Value, [String]) Source #

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

Runtime Monad

type Runtime = StateT RuntimeState (WriterT [String] (Except String)) Source #

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 primitive operators (prim_op) that are assumed to exist.

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

data RuntimeState Source #

State managed by Runtime.

Constructors

RuntimeState 

Fields

gensym :: Runtime Address Source #

Utility function for generating globally unique Addresses.

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

This function provides implementations of the built-in primitive 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 

Fields

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
Show Value Source # 
Instance details

Defined in CESKM

Methods

showsPrec :: Int -> Value -> ShowS #

show :: Value -> String #

showList :: [Value] -> ShowS #

step :: CESKM -> Runtime (Either Value CESKM) Source #

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

drive :: Either Value CESKM -> Runtime Value Source #

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

inject :: CbpvExp -> CESKM Source #

Construct an initial CESKM with a given control expression.

next :: CESKM -> Runtime (Either Value CESKM) Source #

Induces a state machine transition during evaluation.

halt :: Value -> Runtime (Either Value CESKM) Source #

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.