generators

python.Exec.raiseNamed

def Exec.raiseNamed (node : String) (type : String) (message : String) : Code

Raising, at node, the built-in exception named type with message.

python.Generator.continuation

def Generator.continuation (name : Codes) : Codes

The name of a generator function’s continuation in the table.

python.Generator.running

def Generator.running : Nat

The state of a generator that is running (being resumed, not yet suspended).

python.Suspended

record Suspended

A generator’s object: its address, its function, its state, its locals, whether it is done.

python.Generator.of

def Generator.of (h : Heap) (v : Value) : Option Suspended

The generator object of the value v in the heap h, if it is a generator.

python.Generator.store

def Generator.store (h : Heap) (g : Suspended) (state : Nat) (locals : List (Option Value)) (done : Bool) : Heap

The heap h with the object of the generator g stored with a new state, locals and whether it is done.

python.Generator.finished

def Generator.finished (s : Run) (p : Place) : Run

The run s with the generator in the place p finished.

python.Exec.makeGenerator

def Exec.makeGenerator (node : String) (name : Codes) (scratch : Place) : Code

The body of the generator function name at node: a generator over the locals the call bound (state 0), returned through the slot scratch.

python.Generator.step

def Generator.step (yielded : Bool) (v : Value) : Value

A step’s result as the continuation gives it: whether it yielded, and the value v.

python.Generator.prepare

def Generator.prepare (functions : List Function) (item : Place) (s : Run) (how : Nat) (v : Value) (g : Suspended) (self : Value) : Evaluation

What resuming the generator g (the value self) in the run s does before the continuation, how it is resumed (0 send, 1 throw, 2 close) with the value v sent or thrown: end at once, fail, or prepare the call of the continuation (its position in the program’s functions, the kept locals with the state, what was sent and the generator after them); the step goes into the place item.

python.Exec.generatorFailed

def Exec.generatorFailed (node : String) (how : Nat) (generator : Place) (caught : Place) (item : Place) : Code

What resuming the generator in the place generator at node does with the exception its continuation raised (in the place caught): the generator is finished; StopIteration is RuntimeError (PEP 479); for close (how 2), GeneratorExit and StopIteration end it normally, the step into the place item.

python.Exec.resume

def Exec.resume (node : String) (functions : List Function) (bodies : Nat -> Code) (how : Nat) (generator : Place) (value : Expression) (item : Place) (ended : Place) (trying : Place) : Code

next(g) (how 0 with None), g.send(value) (how 0), g.throw(value) (how 1), g.close() (how 2) at node, with the program’s functions and their bodies: the generator in the place generator, the expression value sent or thrown, its step into item and ended (ended when it finished; item is what it yielded or returned); trying is the place the try around the continuation needs.