flattening

python.Flat

data Flat

A generator’s body to flatten: plain statements and the structure around its yields (a try’s handlers end with handlersEnd, what runs when none catches: it is a clause of its own, run while the exception is handled).

python.FlatEnv

record FlatEnv

What compiling needs: the program’s functions and bodies, how many locals the generator keeps, what wraps every statement of the region (the trys around it), and how a return leaves (a finally keeps the value and runs its cleanup first).

python.Compiled

record Compiled

A compiled part: the statement that enters it, the blocks it made (state, statement), the next free state.

python.Handled

record Handled

A try’s compiled handlers: its clauses (each going to its block), the blocks, the next free state.

python.Flat.state

def Flat.state (saved : Nat) : Place

The continuation’s state slot, past the generator’s saved locals.

python.Flat.sent

def Flat.sent (saved : Nat) : Place

The slot with what the resumption sent: (how, value), for a generator that keeps saved locals.

python.Flat.owner

def Flat.owner (saved : Nat) : Place

The slot with the generator, for a generator that keeps saved locals.

python.Flat.scratch

def Flat.scratch (saved : Nat) : Place

The scratch slot, for a generator that keeps saved locals.

python.Flat.final

def Flat.final : Nat

The state past the last block: the generator ends.

python.Flat.goto

def Flat.goto (saved : Nat) (k : Nat) : Code

Going to the block of the state k (not a stop for the debugger), for a generator that keeps saved locals.

python.Flat.suspend

def Flat.suspend (saved : Nat) (state : Nat) : Code

Suspending: the generator’s own saved locals and the state to resume at kept in the generator.

python.Flat.finish

def Flat.finish (saved : Nat) : Code

The generator, which keeps saved locals, finished.

python.Flat.returning

def Flat.returning (node : String) (saved : Nat) (yielded : Bool) (e : Expression) : Code

Returning a step from the continuation at node: whether it yielded, and the value of the expression e (through the scratch slot past the saved locals).

python.Flat.yielding

def Flat.yielding (node : String) (saved : Nat) (e : Expression) (resumeAt : Nat) : Code

yield e at node: the value of e evaluated, the generator (keeping saved locals) suspended at the state resumeAt, the value given out.

python.Flat.how

def Flat.how (s : Run) (saved : Nat) : Nat

How the generator that keeps saved locals was resumed in the run s (0 next or send, 1 throw, 2 close).

python.Flat.value

def Flat.value (saved : Nat) : Expression

What was sent (or thrown) to the generator that keeps saved locals.

python.Flat.resumedAt

def Flat.resumedAt (node : String) : Code

Where a resumed generator goes on: a step telling the debugger, without stopping, the statement it is in (its node marked with the code 2; python.debugging), as CPython has no line event for going on with the same line.

python.Flat.resuming

def Flat.resuming (node : String) (saved : Nat) (into : Option Place) : Code

Where a yield at node resumes: raise what throw sent, GeneratorExit for close, else store what was sent into the place into, if any; for a generator that keeps saved locals.

python.Flat.at

def Flat.at (s : Run) (saved : Nat) (k : Nat) : Bool

Whether the state in the run s is k, for a generator that keeps saved locals.

python.Flat.dispatch

def Flat.dispatch (saved : Nat) (blocks : List (Nat * Code)) (otherwise : Code) : Code

The block of the current state among the blocks (state, statement), else what otherwise does; for a generator that keeps saved locals.

python.Compiled.only

def Compiled.only (entry : Code) (next : Nat) : Compiled

A compiled part with nothing but the statement entry, and next the next free state.

python.Flat.delegated

def Flat.delegated (node : String) (saved : Nat) (iterator : Place) (item : Place) (ended : Place) (into : Option Place) (k : Nat) (again : Nat) : Code

A yield from’s decision at node after the inner iterator in the place iterator moved (its step in item, the end in the flag ended): ended, its value (an inner generator’s return value, else None) into the target into and on to k; else its item given out, resuming at the state again. For a generator that keeps saved locals.

python.Flat.forwarded

def Flat.forwarded (env : FlatEnv) (node : String) (iterator : Place) (item : Place) (ended : Place) (trying : Place) : Code

A yield from at node resumed, in the environment env: to an inner generator, the same resumption (close also raises GeneratorExit here); to another iterator, throw and close raise here and next takes its next item. The inner iterator is in the place iterator, its step goes into item and ended, and trying is the place the try around the continuation needs.

python.Flat.exits

def Flat.exits (env : FlatEnv) (cleanup : Code) (kept : Place) (n : Nat) (k : Nat) (bk : Nat) (ck : Nat) : List (Nat * Code)

A finally’s exit blocks from state n in the environment env: the normal end (to k), a return (its value kept in the place kept), a break (to bk) and a continue (to ck), each running the cleanup first.

python.Flat.inFinally

def Flat.inFinally (env : FlatEnv) (cleanup : Code) (kept : Place) (trying : Place) (n : Nat) : FlatEnv

The environment env inside a finally’s region whose exit blocks start at state n: an exception, kept in the place kept (trying is the try’s flag place), runs the cleanup and is raised again; a return keeps its value in kept and goes to the return exit (state n + 1).

python.Flat.body

def Flat.body (functions : List Function) (bodies : Nat -> Code) (saved : Nat) (f : Flat) : Code

The continuation’s body for the part f of a generator that keeps saved locals, with the program’s functions and their bodies: the blocks run by state from 0 (the entry); past the last, the generator ends and returns None.