Safe Haskell	Safe-Inferred
Language	Haskell2010

CESKM

Contents

Runtime Monad
CESK(M) evaluation
Environment & Store

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

evaluate :: CbpvExp -> Either String (Value, [String])
type Runtime = StateT RuntimeState (WriterT [String] (Except String))
newtype RuntimeState = RuntimeState {
- gensym_val :: Int
}
runtime :: RuntimeState -> Runtime a -> Either String (a, [String])
runtimeLog :: String -> Runtime ()
gensym :: Runtime Address
op :: Symbol -> [Value] -> Runtime Value
data CESKM = CESKM {
- control :: CbpvExp
- environment :: Env
- store :: Store
- kontinuation :: Kont
- meta :: [Kont]
}
data Kont
- = Halt
- | Argk [Value] Kont
- | Letk Symbol CbpvExp Env Kont
data Value
- = Closure CbpvExp Env
- | Continuation Kont
- | IntV Integer
- | FloatV Double
- | BoolV Bool
step :: CESKM -> Runtime (Either Value CESKM)
drive :: Either Value CESKM -> Runtime Value
inject :: CbpvExp -> CESKM
type Address = Int
data Env
data Store
emptyEnv :: Env
emptyStore :: Store
bindEnv :: Env -> Symbol -> Either Address CbpvExp -> Env
bindEnv' :: Env -> [Symbol] -> [Either Address CbpvExp] -> Env
bindStore :: Store -> Address -> Value -> Store
bindStore' :: Store -> [Address] -> [Value] -> Store
lookupEnv :: MonadError String m => Env -> Symbol -> m (Either Address CbpvExp)
lookupStore :: MonadError String m => Store -> Address -> m Value

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

The actual evaluation algorithm begins with evaluate. See also: CESKM. TODO RuntimeT, Runtime = RuntimeT Identity

newtype RuntimeState Source #

State managed by Runtime.

Constructors

RuntimeState
Fields gensym_val :: Int Incremented and returned to generate an `Address`.

runtime :: RuntimeState -> Runtime a -> Either String (a, [String]) Source #

runtimeLog :: String -> Runtime () Source #

gensym :: Runtime Address Source #

Utility function for generating globally unique Addresses.

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

This function provides implementations of the built-in operators. TODO After making Runtime = RuntimeT Identity, rename this to baseOps and for all monads m => RuntimeT m THEN create a typeclass ops and different monads

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 control :: CbpvExp The expression being evaluated environment :: Env Symbol -> Address + Defn store :: Store Address -> Value kontinuation :: Kont The rest of the computation meta :: [Kont] The meta-continuation: a LIFO stack of `Kont`s.

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 #