| Copyright | Brent Yorgey |
|---|---|
| License | BSD-3-Clause |
| Maintainer | byorgey@gmail.com |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Swarm.Game.CESK
Description
The Swarm interpreter uses a technique known as a CESK machine (if you want to read up on them, you may want to start by reading about CEK machines first). Execution happens simply by iterating a step function, sending one state of the CESK machine to the next. In addition to being relatively efficient, this means we can easily run a bunch of robots synchronously, in parallel, without resorting to any threads (by stepping their machines in a round-robin fashion); pause and single-step the game; save and resume, and so on.
Essentially, a CESK machine state has four components:
- The Control is the thing we are currently focused on:
either a
Termto evaluate, or aValuethat we have just finished evaluating. - The Environment (
Env) is a mapping from variables that might occur free in the Control to their values. - The Store (
Store) is a mapping from abstract integer locations to values. We use it to store delayed (lazy) values, so they will be computed at most once. - The Kontinuation (
Cont) is a stack ofFrames, representing the evaluation context, i.e. what we are supposed to do after we finish with the currently focused thing. When we reduce the currently focused term to a value, the top frame on the stack tells us how to proceed.
You can think of a CESK machine as a defunctionalization of a recursive big-step interpreter, where we explicitly keep track of the call stack and the environments that would be in effect at various places in the recursion. One could probably even derive this mechanically, by writing a recursive big-step interpreter, then converting it to CPS, then defunctionalizing the continuations.
The slightly confusing thing about CESK machines is how we have to pass around environments everywhere. Basically, anywhere there can be unevaluated terms containing free variables (in values, in continuation stack frames, ...), we have to store the proper environment alongside so that when we eventually get around to evaluating it, we will be able to pull out the environment to use.
Synopsis
- data Frame
- type Cont = [Frame]
- newtype WorldUpdate = WorldUpdate {}
- newtype RobotUpdate = RobotUpdate {}
- data Store
- type Loc = Int
- emptyStore :: Store
- data Cell
- allocate :: Env -> Term -> Store -> (Loc, Store)
- lookupCell :: Loc -> Store -> Maybe Cell
- setCell :: Loc -> Cell -> Store -> Store
- data CESK
- initMachine :: ProcessedTerm -> Env -> Store -> CESK
- initMachine' :: ProcessedTerm -> Env -> Store -> Cont -> CESK
- cancel :: CESK -> CESK
- resetBlackholes :: Store -> Store
- finalValue :: CESK -> Maybe (Value, Store)
- prettyFrame :: Frame -> String
- prettyCont :: Cont -> String
- prettyCESK :: CESK -> String
Frames and continuations
A frame is a single component of a continuation stack, explaining what to do next after we finish evaluating the currently focused term.
Constructors
| FSnd Term Env | We were evaluating the first component of a pair; next, we
should evaluate the second component which was saved in this
frame (and push a |
| FFst Value | We were evaluating the second component of a pair; when done, we should combine it with the value of the first component saved in this frame to construct a fully evaluated pair. |
| FArg Term Env |
|
| FApp Value |
|
| FLet Var Term Env |
|
| FTry Value | We are executing inside a |
| FUnionEnv Env | We were executing a command; next we should take any environment it returned and union it with this one to produce the result of a bind expression. |
| FLoadEnv TCtx ReqCtx | We were executing a command that might have definitions; next
we should take the resulting |
| FDef Var | We were executing a definition; next we should take the resulting value and return a context binding the variable to the value. |
| FExec | An |
| FBind (Maybe Var) Term Env | We are in the process of executing the first component of a bind; once done, we should also execute the second component in the given environment (extended by binding the variable, if there is one, to the output of the first command). |
| FImmediate WorldUpdate RobotUpdate | Apply specific updates to the world and current robot. |
| FUpdate Loc | Update the memory cell at a certain location with the computed value. |
| FFinishAtomic | Signal that we are done with an atomic computation. |
Instances
Wrappers for creating delayed change of state
newtype WorldUpdate Source #
Constructors
| WorldUpdate | |
Instances
| FromJSON WorldUpdate Source # | |
Defined in Swarm.Game.CESK | |
| ToJSON WorldUpdate Source # | |
Defined in Swarm.Game.CESK Methods toJSON :: WorldUpdate -> Value # toEncoding :: WorldUpdate -> Encoding # toJSONList :: [WorldUpdate] -> Value # toEncodingList :: [WorldUpdate] -> Encoding # | |
| Show WorldUpdate Source # | |
Defined in Swarm.Game.CESK Methods showsPrec :: Int -> WorldUpdate -> ShowS # show :: WorldUpdate -> String # showList :: [WorldUpdate] -> ShowS # | |
| Eq WorldUpdate Source # | |
Defined in Swarm.Game.CESK | |
newtype RobotUpdate Source #
Constructors
| RobotUpdate | |
Fields | |
Instances
| FromJSON RobotUpdate Source # | |
Defined in Swarm.Game.CESK | |
| ToJSON RobotUpdate Source # | |
Defined in Swarm.Game.CESK Methods toJSON :: RobotUpdate -> Value # toEncoding :: RobotUpdate -> Encoding # toJSONList :: [RobotUpdate] -> Value # toEncodingList :: [RobotUpdate] -> Encoding # | |
| Show RobotUpdate Source # | |
Defined in Swarm.Game.CESK Methods showsPrec :: Int -> RobotUpdate -> ShowS # show :: RobotUpdate -> String # showList :: [RobotUpdate] -> ShowS # | |
| Eq RobotUpdate Source # | |
Defined in Swarm.Game.CESK | |
Store
Instances
| FromJSON Store Source # | |
| ToJSON Store Source # | |
Defined in Swarm.Game.CESK | |
| Generic Store Source # | |
| Show Store Source # | |
| Eq Store Source # | |
| type Rep Store Source # | |
Defined in Swarm.Game.CESK type Rep Store = D1 ('MetaData "Store" "Swarm.Game.CESK" "swarm-0.2.0.0-D1mAmWsUEjoFqpCaq9DHG0" 'False) (C1 ('MetaCons "Store" 'PrefixI 'True) (S1 ('MetaSel ('Just "next") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Loc) :*: S1 ('MetaSel ('Just "mu") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (IntMap Cell)))) | |
emptyStore :: Store Source #
A memory cell can be in one of three states.
Constructors
| E Term Env | A cell starts out life as an unevaluated term together with its environment. |
| Blackhole Term Env | When the cell is A |
| V Value | Once evaluation is complete, we cache the final |
Instances
| FromJSON Cell Source # | |
| ToJSON Cell Source # | |
Defined in Swarm.Game.CESK | |
| Generic Cell Source # | |
| Show Cell Source # | |
| Eq Cell Source # | |
| type Rep Cell Source # | |
Defined in Swarm.Game.CESK type Rep Cell = D1 ('MetaData "Cell" "Swarm.Game.CESK" "swarm-0.2.0.0-D1mAmWsUEjoFqpCaq9DHG0" 'False) (C1 ('MetaCons "E" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Term) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Env)) :+: (C1 ('MetaCons "Blackhole" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Term) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Env)) :+: C1 ('MetaCons "V" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Value)))) | |
allocate :: Env -> Term -> Store -> (Loc, Store) Source #
Allocate a new memory cell containing an unevaluated expression with the current environment. Return the index of the allocated cell.
CESK machine states
The overall state of a CESK machine, which can actually be one of three kinds of states. The CESK machine is named after the first kind of state, and it would probably be possible to inline a bunch of things and get rid of the second state, but I find it much more natural and elegant this way. Most tutorial presentations of CEK/CESK machines only have one kind of state, but then again, most tutorial presentations only deal with the bare lambda calculus, so one can tell whether a term is a value just by seeing whether it is syntactically a lambda. I learned this approach from Harper's Practical Foundations of Programming Languages.
Constructors
| In Term Env Store Cont | When we are on our way "in/down" into a term, we have a
currently focused term to evaluate in the environment, a store,
and a continuation. In this mode we generally pattern-match on the
|
| Out Value Store Cont | Once we finish evaluating a term, we end up with a Note that there is no |
| Up Exn Store Cont | An exception has been raised. Keep unwinding the
continuation stack (until finding an enclosing |
| Waiting Integer CESK | The machine is waiting for the game to reach a certain time to resume its execution. |
Instances
Construction
initMachine :: ProcessedTerm -> Env -> Store -> CESK Source #
Initialize a machine state with a starting term along with its type; the term will be executed or just evaluated depending on whether it has a command type or not.
initMachine' :: ProcessedTerm -> Env -> Store -> Cont -> CESK Source #
Like initMachine, but also take an explicit starting continuation.
resetBlackholes :: Store -> Store Source #
Extracting information
finalValue :: CESK -> Maybe (Value, Store) Source #
Is the CESK machine in a final (finished) state? If so, extract the final value and store.
Pretty-printing
prettyFrame :: Frame -> String Source #
Poor pretty-printing of frames.
prettyCont :: Cont -> String Source #
Poor pretty-printing of continuations.
prettyCESK :: CESK -> String Source #
Very poor pretty-printing of CESK machine states, really just for debugging. At some point we should make a nicer version.