lowering

python.Context

record Context

What the translation knows: each module name’s slot, the current function’s names and their places (none at the module level), the first temporary slot (a local slot in a function, a global one at the module level), the program’s symbol table, its functions and their bodies; in a class body, the names it binds and their places; which class each method’s node belongs to, and the class of the current method; in a comprehension run in place, its variables’ temporaries (they hide the names around it); the names import binds anywhere in the program (a module there is read only as module.member); whether the run notes the types it sees (Lowering.watching), and the node of the function being translated, whose own expressions in its body are not the program’s (a comprehension or generator expression made a function: its .0, .acc, append and yield at its node).

python.Lowering

data Lowering (A : Type)

A translation step: from the context and the next free temporary, its result and the next free temporary, or the construct it cannot take.

python.Lowering.run

def Lowering.run {A : Type} (m : Lowering A) (c : Context) (t : Nat) : Either String (A * Nat)

Running a translation step.

python.Lowering.give

def Lowering.give {A : Type} (a : A) : Lowering A

A step that gives a value.

python.Lowering.then

def Lowering.then {A : Type} {B : Type} (m : Lowering A) (k : A -> Lowering B) : Lowering B

A step after another.

python.Lowering.fail

def Lowering.fail {A : Type} (what : String) : Lowering A

The translation stops: a construct it cannot take.

python.Lowering.context

def Lowering.context : Lowering Context

The context.

python.Lowering.within

def Lowering.within {A : Type} (f : Context -> Context) (m : Lowering A) : Lowering A

A translation step under a changed context (a class body’s names, for one).

python.Lowering.fresh

def Lowering.fresh : Lowering Place

A new temporary slot.

python.Lowering.each

def Lowering.each {A : Type} {B : Type} (f : A -> Lowering B) (xs : List A) : Lowering (List B)

Steps in order, their results in a list.

python.Lowering.paired

def Lowering.paired {A : Type} {B : Type} (xs : List A) (ys : List B) : List (A * B)

Two lists paired item by item (as long as the shorter).

python.Lowered

record Lowered

An expression’s translation: the statements to run first, and the expression reading its value.

python.Lowered.plain

def Lowered.plain (e : Expression) : Lowered

A translation that needs nothing first.

python.Lowering.watching

def Lowering.watching (c : Context) (n : String) (e : Expression) : Expression

The expression e, its value’s type noted at the node n when the context c observes types (not at the node of the function being translated).

python.Context.place

def Context.place (c : Context) (name : String) : Option Place

The place of a module name.

python.Lowering.functionNames

def Lowering.functionNames : List String

The built-in functions a name refers to when the module does not bind it.

python.Lowering.classNames

def Lowering.classNames : List String

The built-in classes a name refers to when the module does not bind it (the exception classes too).

python.Lowering.unprovided

def Lowering.unprovided : List String

CPython’s built-in names the model does not provide yet: reading one stops the translation (it is unsupported, not a NameError).

python.Lowering.isBuiltin

def Lowering.isBuiltin (name : String) : Bool

Whether a name is built-in.

python.Lowering.builtin

def Lowering.builtin (name : String) : Value

The value of a built-in name.

python.Lowering.builtinRead

def Lowering.builtinRead (name : String) : Expression

Reading a built-in name.

python.Lowering.mathFunctions

def Lowering.mathFunctions : List String

The math functions the model provides.

python.Lowering.mathConstants

def Lowering.mathConstants : List (String * String)

The math constants, as CPython’s repr writes them (the nearest binary64).

python.Lowering.randomFunctions

def Lowering.randomFunctions : List String

The random module’s functions the model provides (python.random).

python.Lowering.member

def Lowering.member (m : String) (attr : String) : Option Value

A member of math or random: a function (the built-in function named by the module) or a constant.

python.Lowering.moduleValue

def Lowering.moduleValue (m : String) : Value

A module bound by import (its class name starts with module , which no class has).

python.Lowering.moduleOf

def Lowering.moduleOf (v : Value) : Option String

The module a value is, if it is one.

python.Lowering.holdsModule

def Lowering.holdsModule (p : Place) (s : Run) : Checked Stop Bool

Whether the place holds a module.

python.Lowering.memberOf

def Lowering.memberOf (p : Place) (attr : String) : Expression

module.attr for the module in a place: its member, or unsupported when the model does not have it.

python.Lowering.nameValue

def Lowering.nameValue (c : Context) (name : String) (p : Place) : Expression

A name’s value from its place: a module there is not taken as a value (only as module.member).

python.Lowering.importedPlace

def Lowering.importedPlace (c : Context) (e : python.ast.Expr) : Option Place

The place of a name import binds, when the expression is that name.

python.Lowering.moduleOr

def Lowering.moduleOr (node : String) (place : Option Place) (watch : Expression -> Expression) (attr : String) (result : Place) (general : Code) : Code

module.attr into result when the place (of a name import binds) holds a module, the general statement otherwise (the name was bound to something else); reading the name first (NameError before the import), through watch (Lowering.watching at the name’s node).

python.Lowering.name

def Lowering.name (name : String) : Lowering Lowered

A name read: its slot, or the built-in it refers to (a CPython built-in the model does not provide stops the translation).

python.Lowering.isPlainBuiltin

def Lowering.isPlainBuiltin (name : String) : Lowering Bool

Whether a name is read as the built-in (the module does not bind it).

python.Lowering.constant

def Lowering.constant (k : python.ast.Constant) : Lowering Value

A constant’s value.

python.Lowering.operator

def Lowering.operator (op : python.ast.BinOp) : String * (String * String)

An operator’s symbol, its method and its reflected method.

python.Lowering.arithmetic

def Lowering.arithmetic (op : python.ast.BinOp) : Heap -> Value -> Value -> Changed

The built-in operation of an operator (the data layer’s).

python.Lowering.powersByLibrary

def Lowering.powersByLibrary (x : Value) (y : Value) : Bool

Whether x ** y is computed by the platform’s math library: both are numbers and one is a float (ints are exact).

python.Lowering.formatsOperands

def Lowering.formatsOperands (op : python.ast.BinOp) (x : Value) (y : Value) (e : Expression) : Expression

a op b on built-in values: printf-style formatting (str % b) shows b (its items) as text, noted by Run.shown (by repr, which %s of an object without a __str__ shows too); a float power is the math library’s (libm:math.correctlyRounded, as Builtins.inexactMath).

python.Lowering.binary

def Lowering.binary (node : String) (op : python.ast.BinOp) (left : Place) (b : Expression) (result : Place) : Lowering Code

result = a op b with the operands in places.

python.Lowering.containing

def Lowering.containing (node : String) (a : Place) (b : Place) (item : Place) (container : Place) (result : Place) : Lowering Code

a in b (Exec.containsBy: a list’s or tuple’s items compared with the user’s __eq__ when they define it).

python.Lowering.identical

def Lowering.identical (a : Value) (b : Value) : Expression

x is y: the same object, None, NotImplemented or bool (each one object); unsupported for numbers and strings (their identity is the implementation’s).

python.Lowering.comparison

def Lowering.comparison (node : String) (op : python.ast.CmpOp) (a : Place) (b : Place) (result : Place) : Lowering Code

result = a op b for one comparison, the operands in places.

python.Lowering.prompt

def Lowering.prompt (p : Place) : Expression

The prompt of input(prompt) (the str at the place p, already made) written to standard output, its value kept: a step of its own before the read, so a debugger that waits for input there has shown the prompt (CPython writes it first).

python.Lowering.input

def Lowering.input : Expression

input(): a line of the input without its newline; EOFError when the input has none left. A read that reaches the end of the input without a newline marks the console (atEnd): a debugger whose input is not closed waits for more there.

python.Lowering.made

def Lowering.made (kind : String) (vs : List Value) : Expression

A list’s items, a tuple, a set or a dict from values.

python.Lowering.dict

def Lowering.dict (keys : List Value) (values : List Value) : Expression

A dict from keys and values in order.

python.Exec.method

def Exec.method (node : String) (functions : List Function) (bodies : Nat -> Code) (receiver : Place) (name : String) (arguments : List Place) (keywords : List (Codes * Place)) (result : Place) : Code

result = receiver.name(*arguments, **keywords): the attribute’s value called (a user’s method bound to an instance, or any callable attribute), else a built-in type’s method.

python.Lowering.definedAt

def Lowering.definedAt (infos : List Symbol) (node : String) : Option Symbol

The function defined at a node, in the symbol table.

python.Lowering.argName

def Lowering.argName (a : python.ast.Arg) : String

An argument’s name.

python.Lowering.parameterNames

def Lowering.parameterNames (a : python.ast.Arguments) : List String

The parameters’ names in Calls.bind’s order: positional (positional-only first), keyword-only, *args, **kwargs.

python.Lowering.ownName

def Lowering.ownName (f : Symbol) : String

A function’s own name (<lambda> for a lambda).

python.Lowering.scopedName

def Lowering.scopedName (methods : List (String * String)) (f : Symbol) : String

A function’s name in its scope: a method’s has its class’s name before it.

python.Lowering.enclosing

def Lowering.enclosing (infos : List Symbol) (fuel : Nat) (f : Symbol) : Option Symbol

The function a function is in (within fuel): not a list, set or dict comprehension’s, which CPython runs in place (a generator expression’s is a function of its own).

python.Lowering.qualname

def Lowering.qualname (methods : List (String * String)) (infos : List Symbol) (fuel : Nat) (f : Symbol) : String

A function’s __qualname__: the enclosing functions’ names with .<locals>. between (a generator expression’s scope adds only a dot, as CPython’s compiler does for a comprehension’s), within fuel.

python.Lowering.tableName

def Lowering.tableName (methods : List (String * String)) (infos : List Symbol) (f : Symbol) : String

A function’s name in the program’s table: its qualified name, a mark (code 1, which the messages cut at) and its number, so that two functions of the same name differ.

python.Lowering.signature

def Lowering.signature (methods : List (String * String)) (infos : List Symbol) (f : Symbol) : Signature

A function’s signature for Calls.bind.

python.Lowering.layout

def Lowering.layout (f : Symbol) : List (String * Place) * Nat

Where a function’s names live: its parameters (in Calls.bind’s order), then its free variables (the cells its value captured), then its other locals; a variable a nested function captures is a cell. The second is the count.

python.Lowering.cellsMade

def Lowering.cellsMade (f : Symbol) (layout : List (String * Place)) : Code

A function’s own cells made on entry: a parameter’s cell holds the argument, any other is empty.

python.Lowering.cellRef

def Lowering.cellRef (c : Context) (name : String) : Lowering Expression

The reference of a cell a new function captures (its place in the current scope must be a cell).

python.Lowering.madeFunction

def Lowering.madeFunction (node : String) (defaults : List Place) : Lowering Expression

A function value made at its definition: its table name, the cells it captures, its defaults (already in temporaries: positional, then the keyword-only ones that have one).

python.Lowering.read

def Lowering.read (c : Context) (name : String) : Expression

A name’s read when it is not a built-in shortcut (the module binds it).

python.Lowering.forcedStop

def Lowering.forcedStop (n : String) : Code

A step that always stops the debugger at a node (marked with the code 1; python.debugging).

python.Lowering.leavingStops

def Lowering.leavingStops (node : String) (body : Code) : Code

A comprehension run in place, where an exception leaving it stops the debugger at it once more (CPython’s cleanup of the comprehension’s variables is on its line) and goes on out.

python.Lowering.special

def Lowering.special (node : String) (name : String) (args : List Place) (keywords : List (Codes * Place)) (result : Place) : Lowering (Option Code)

The built-ins whose calls are statements here (they may run the user’s methods, or use the console): print (with sep and end), len, str, repr and bool of one argument, input of none or one; none for any other name or shape.

python.Lowering.stepping

def Lowering.stepping (node : String) (name : String) (round : Code) (args : List Place) (keywords : List (Codes * Place)) (result : Place) : Lowering (Option Code)

The built-ins that take items one by one as for does (a generator’s included): any and all of one argument, stopping at the first item that decides; next of one or two (the default).

python.Lowering.consumes

def Lowering.consumes (name : String) (args : List Place) : Bool

The built-ins that take all the items of their first argument (min and max only when it is their only argument): it is gathered into a list first when taking its items runs a user’s code (Exec.gathered).

python.Lowering.gathering

def Lowering.gathering (node : String) (should : Run -> Bool) (hinted : Bool) (round : Code) (args : List Place) : Lowering (Code * List Place)

The first argument gathered (when it should be, by the run’s check; its length hint taken first when hinted, Exec.gathered), and the arguments with the gathered one first.

python.Lowering.concatenated

def Lowering.concatenated (vs : List Value) : Expression

Texts joined (an f-string’s parts).

python.Lowering.formatting

def Lowering.formatting (value : Place) (spec : Option Place) (s : Run) : Changed

format(value, spec) with the value and the spec (none for no spec) in places.

python.Lowering.isSuper

def Lowering.isSuper (e : python.ast.Expr) : Bool

Whether an expression is super() with no arguments.

python.Lowering.superCall

def Lowering.superCall (node : String) (attr : String) (args : List Place) (keywords : List (Codes * Place)) (before : Code) (result : Place) : Lowering Lowered

super().attr(*args, **keywords) in a method: the attribute found after the method’s class along the order of the first parameter’s class, bound to it (Objects.super), then called.

python.Lowering.formattedFrom

def Lowering.formattedFrom (node : String) (v : Code * Place) (sp : Code * Option Place) (conversion : Int) : Lowering Lowered

A formatted value of an f-string from its value and spec (in temporaries): the conversion (!s, !r; !a not yet), the methods its str needs run, then format(value, spec).

python.Lowering.keywordAt

def Lowering.keywordAt (keywords : List (Codes * Place)) (name : String) : Option Place

A keyword argument’s place, by name.

python.Lowering.numeric

def Lowering.numeric (v : Value) : Bool

Whether a value is a number sum’s fast paths take (an int, a float or a bool).

python.Lowering.summed

def Lowering.summed (node : String) (args : List Place) (keywords : List (Codes * Place)) (general : Code) (result : Place) : Lowering Code

sum(iterable, start) when the start or an item is a user’s object with __add__ or __radd__: as CPython, the numbers before the first other item summed by the built-in’s fast paths (a number start), then each item after added with + (the user’s methods run); any other sum is the built-in’s (general).

python.Lowering.sumShape

def Lowering.sumShape (args : List Place) (keywords : List (Codes * Place)) : Bool

Whether sum is called as sum(iterable), sum(iterable, start) or sum(iterable, start=s).

python.Lowering.ordered

def Lowering.ordered (node : String) (name : String) (args : List Place) (keywords : List (Codes * Place)) (result : Place) : Lowering Code

sorted(xs, key=f, reverse=r), min(..., key=f, default=d) and max: the items in a list (an iterable’s taken as for takes them; several arguments’ as they are), their keys (the key function called on each, as CPython does before comparing; the items themselves for none or None), then the items by their keys (python.sorting: the user’s comparisons when the keys define them, else the built-in’s).

python.Lowering.takesOrder

def Lowering.takesOrder (name : String) (args : List Place) (keywords : List (Codes * Place)) : Bool

Whether sorted, min or max is called in a shape taken here: sorted of one argument with key and reverse, min and max with key and (of one argument) default.

python.Lowering.listSort

def Lowering.listSort (node : String) (receiver : Place) (keywords : List (Codes * Place)) (general : Code) (result : Place) : Lowering Code

xs.sort(key=f, reverse=r) when xs is a list (Sorting.listSort), the method called otherwise (general).

python.Lowering.lazyCall

def Lowering.lazyCall (node : String) (name : String) (args : List Place) (keywords : List (Codes * Place)) (general : Code) (result : Place) : Lowering (Option Code)

map(f, *iterables), filter(f, iterable), zip(*iterables) and enumerate(iterable) called by name: each iterable’s iterator taken first (Exec.iterate: a user’s __iter__ runs now, as CPython takes them when it is called), then the built-in generator (python.lazy); zip and enumerate over iterables whose items do not run a user’s code are the built-in iterators (general). Other shapes are the built-in’s (none).

python.Lowering.generatorOnly

def Lowering.generatorOnly (args : List python.ast.Expr) (keywords : List python.ast.Keyword) : Bool

Whether a call’s only argument is a generator expression: CPython 3.14 runs any, all and tuple of one in a loop of the caller’s, which stops the debugger at the call after each item that does not end it.

python.Lowering.callByName

def Lowering.callByName (node : String) (name : String) (inlined : Bool) (args : List Place) (keywords : List (Codes * Place)) (before : Code) (result : Place) : Lowering Lowered

A call of a name: a built-in shortcut (Lowering.special) when the module does not bind the name, else the name’s value called; inlined: its only argument is a generator expression (Lowering.generatorOnly).

python.Lowering.resumed

def Lowering.resumed (node : String) (receiver : Place) (attr : String) (args : List Place) (result : Place) (called : Code) : Lowering Code

A generator’s send, throw or close resuming it (Exec.resumeMethod); the method called otherwise.

python.Lowering.callMethod

def Lowering.callMethod (node : String) (receiver : Code * Place) (attr : String) (args : List Place) (keywords : List (Codes * Place)) (before : Code) (result : Place) : Lowering Lowered

A method call: the receiver (already in a temporary), then the call of its attribute; str.join and list.extend gather their argument first when taking its items runs a user’s code; a generator’s send, throw and close resume it.

python.Lowering.moduleCall

def Lowering.moduleCall (node : String) (p : Place) (name : String) (attr : String) (args : List Place) (keywords : List (Codes * Place)) (before : Code) (result : Place) : Lowering Lowered

name.attr(...) where import binds the name: the module’s member called when it holds a module, the method called otherwise (the name was bound to something else); the name read at its node name.

python.Lowering.spreads

def Lowering.spreads (args : List python.ast.Expr) (keywords : List python.ast.Keyword) : Bool

Whether a call unpacks arguments (*x among them, or **m among its keywords).

python.Lowering.gatheredCall

def Lowering.gatheredCall (node : String) (callee : Place) (items : Place) (named : Place) (result : Place) : Lowering Code

The call with arguments gathered at run time (the callee’s value, the list of positional ones and the dict of keyword ones in places): print with only sep and end writes them as print(*values) does, any other callee is called with them (Exec.callGathered).

python.Lowering.callValue

def Lowering.callValue (node : String) (before : Code) (f : Expression) (args : List Place) (keywords : List (Codes * Place)) (result : Place) : Lowering Lowered

A call of any other callee (its value read by an expression after the statements before).

python.Lowering.sliced

def Lowering.sliced (node : String) (c : Code * Place) (a : Code * Option Place) (b : Code * Option Place) (k : Code * Option Place) (result : Place) : Code

result = c[a:b:k] with the container and the bounds in temporaries.

python.Lowering.indexed

def Lowering.indexed (node : String) (v : Lowered) (k : Lowered) : Lowering Lowered

c[k] from the translations of the container and the key.

python.Lowering.starredAt

def Lowering.starredAt (elts : List python.ast.Expr) (k : Nat) : Option Nat

The position of the starred target among targets, if one is.

python.Lowering.comprehensionCalled

def Lowering.comprehensionCalled (node : String) (first : Code * Place) : Lowering Lowered

A comprehension that is a function of its own (a generator expression, or one where a lambda captures its variables): the function made, then called with an iterator over the first iterable (in a temporary).

python.Lowering.emptyOf

def Lowering.emptyOf (kind : Nat) : Expression

An empty list (kind 0), set (kind 1) or dict (kind 2), for a comprehension to collect into.

python.Lowering.updated

def Lowering.updated (node : String) (op : python.ast.BinOp) (load : Place -> Code) (value : python.ast.Expr) (store : Place -> Code) : Lowering Code

target op= value once the target’s current value can be read into a place and the result stored back: the value, then the operator’s in-place method (__iadd__ and so on, a user’s) or else the binary operation; a list’s += takes the value’s items as list.extend does first (Exec.gathered: its length hint, a user’s iteration).

python.Lowering.augmented

def Lowering.augmented (node : String) (target : python.ast.Expr) (op : python.ast.BinOp) (value : python.ast.Expr) : Lowering Code

target op= value for a name, an attribute (its object evaluated once) or an item (its container and key evaluated once), as CPython reads the target, computes, and stores it back.

python.Lowering.decoratorsEvaluated

def Lowering.decoratorsEvaluated (decorators : List python.ast.Expr) (evaluated : Code) : Code

The decorators’ evaluation with a step at each decorator’s line (CPython’s line events).

python.Lowering.definition

def Lowering.definition (node : String) (name : String) (args : python.ast.Arguments) (decorators : List python.ast.Expr) : Lowering Code

def name(args): ... with decorators: the decorators evaluated first (top to bottom), then the defaults, then the function value, then the decorators applied (the innermost first), then the name bound. With decorators, the debugger stops as CPython’s line events go: at each decorator, at the def (the function made), at each decorator again (applied), at the def (the name bound).

python.Exec.unbind

def Exec.unbind (p : Place) : Code

A variable without a value again (after except … as name, and del name).

python.Lowering.handlerClass

def Lowering.handlerClass (type : Option python.ast.Expr) : Lowering (Option (Run -> Value))

What an except names, read when an exception reaches it: a name, or a tuple of names (any other expression is not taken yet); none for a bare except.

python.Lowering.raiseStatement

def Lowering.raiseStatement (n : String) (exc : Option python.ast.Expr) (cause : Option python.ast.Expr) : Lowering Code

raise e (the cause after from evaluated and not kept: only the last line of an uncaught exception is shown), or a bare raise (the exception being handled again).

python.Lowering.assertStatement

def Lowering.assertStatement (n : String) (test : python.ast.Expr) (msg : Option python.ast.Expr) : Lowering Code

assert test, msg: AssertionError (with the message’s str, evaluated only then) when the test is false.

python.Lowering.classNamesIn

def Lowering.classNamesIn (body : List python.ast.Stmt) : List String

The names a class body binds, in order.

python.Run.boundValue

def Run.boundValue (s : Run) (p : Place) : Option Value

A place’s value if it has one.

python.Lowering.classMade

def Lowering.classMade (name : String) (bases : List Place) (scope : List (String * Place)) : Expression

The class a class body made: its bases (in places) and the names it bound (in their places, those with a value, in order) as its attributes.

python.Lowering.returnStatement

def Lowering.returnStatement (n : String) (value : Option python.ast.Expr) : Lowering Code

return value (None without one), only inside a function.

python.Lowering.importing

def Lowering.importing (n : String) (names : List python.ast.Alias) : Lowering Code

import m and import m as name: the module bound to the name (math and random; any other is not taken).

python.Lowering.importingFrom

def Lowering.importingFrom (n : String) (m : String) (names : List python.ast.Alias) : Lowering Code

from m import x and from m import x as name: the member bound to the name (a math or random function, a math constant; any other is not taken).

python.Lowering.aliasName

def Lowering.aliasName (a : python.ast.Alias) : String

The name import m [as name] binds.

python.Lowering.readsTraceback

def Lowering.readsTraceback (f : Symbol) : Bool

Whether a function reads its traceback parameter (its fourth positional one, or any through *args or **kwargs): the model gives __exit__ None for it.

python.Lowering.tracebackReaders

def Lowering.tracebackReaders (c : Context) : List Codes

The table names of the program’s __exit__ methods that read their traceback.

python.Lowering.reads

def Lowering.reads (readers : List Codes) (h : Heap) (manager : Value) : Bool

Whether a manager’s __exit__ is one of the readers.

python.Exec.managerChecked

def Exec.managerChecked (node : String) (manager : Place) : Code

A context manager’s methods checked before with uses them (__exit__ first, as CPython does): TypeError when its class does not have one.

python.Lowering.managed

def Lowering.managed (node : String) (manager : Code * Place) (entered : Place) (body : Code) : Lowering Code

with around a body (already translated, the as target’s assignment first): the manager’s __enter__, then the body; an exception out of it goes to __exit__(type, value, None) (the traceback is not modeled: an __exit__ that reads it is not taken), raised again unless that returns true; any other way out (the end, return, break, continue) calls __exit__ with three Nones.

python.Lowering.nodeOf

def Lowering.nodeOf (st : python.ast.Stmt) : String

A statement’s node (the debugger stops when a statement starts; its steps carry their own nodes).

python.Lowering.exprNode

def Lowering.exprNode (e : python.ast.Expr) : String

An expression’s node.

python.Lowering.startNode

def Lowering.startNode (st : python.ast.Stmt) : String

Where a statement starts for the debugger: a decorated def or class at its first decorator (CPython’s first line event there), any other at its node.

python.Lowering.classFrame

def Lowering.classFrame (n : String) (name : String) (body : Code) : Code

A class body in a frame of its own, as CPython runs it (the debugger stops at the class line when it starts, and the caller’s statement goes on without stopping again after it), one call deeper (as CPython’s frame counts toward the recursion limit); its names stay in the caller’s places.

python.Lowering.caughtAs

def Lowering.caughtAs (bound : Option Place) (caught : Place) : Option Place * (Code * Code)

An except ... as name binding: the clause keeps the exception in a temporary, the name gets it after the except line’s stop (CPython binds it after the line event) and is unbound again after the handler.

python.Lowering.yieldsIn

def Lowering.yieldsIn (e : python.ast.Expr) : Bool

Whether an expression has a yield (not in a lambda or a function of its own).

python.Lowering.yielded

def Lowering.yielded (n : String) (value : python.ast.Expr) (into : Option Place) : Lowering Flat

A yield or yield from (the value of a statement, kept in into when it is assigned): its operand evaluated first; a yield anywhere else in an expression is not taken.

python.Lowering.yieldAssigned

def Lowering.yieldAssigned (n : String) (targets : List python.ast.Expr) (value : python.ast.Expr) : Lowering Flat

target = yield …: what was sent (or what the inner generator returned) assigned.

python.Lowering.flatReturned

def Lowering.flatReturned (n : String) (value : Option python.ast.Expr) : Lowering Flat

A flattened return: the generator ends with the value (StopIteration’s).

python.Lowering.finallyAround

def Lowering.finallyAround (tried : Flat) (finalbody : List python.ast.Stmt) : Lowering Flat

A flattened try with its finally (whose cleanup is not flattened: a yield there is not taken yet).

python.Lowering.moduleNames

def Lowering.moduleNames (body : List python.ast.Stmt) : List String

The module’s names: the ones it binds and the ones it reads that are not built-in.

python.Lowering.functionBody

def Lowering.functionBody (f : Symbol) : Lowering Code

A function’s statements (a lambda returns its expression).

python.Lowering.inside

def Lowering.inside (c : Context) (f : Symbol) : Context

The context inside a function: its names in their places, its temporaries after them.

python.Lowering.parameterNodes

def Lowering.parameterNodes (f : Symbol) : List (String * String)

The function f’s parameters, as nodes with their names.

python.Lowering.parametersSeen

def Lowering.parametersSeen (c : Context) (f : Symbol) : Code

At the start of the function f’s body, when the context c observes types: each parameter’s value noted at its node.

python.Lowering.flatOf

def Lowering.flatOf (c : Context) (f : Symbol) : Either String (Flat * Nat)

A generator function’s body as a Flat, with the number of its temporaries.

python.Lowering.kept

def Lowering.kept (f : Symbol) (temporaries : Nat) : Nat

How many locals a generator keeps: its names, its temporaries, and the slot its body makes the generator in.

python.Lowering.translated

def Lowering.translated (c : Context) (f : Symbol) : Either String (Code * Nat)

A function’s body translated (its own cells made first), with the number of its temporaries; a generator function’s body makes the generator (its continuation is a table entry of its own).

python.Lowering.continuation

def Lowering.continuation (c : Context) (f : Symbol) : Either String Function

A generator’s continuation in the table: after the generator’s locals, the state, what was sent, the generator and a scratch slot.

python.Lowering.continuations

def Lowering.continuations (c : Context) (gs : List Symbol) : Either String (List Function)

The continuations of the generator functions, in order.

python.Lowering.entries

def Lowering.entries (c : Context) (infos : List Symbol) : Either String (List Function)

The program’s functions: each with its signature and its number of local slots (its names and temporaries).

python.Lowering.generatorsOf

def Lowering.generatorsOf (infos : List Symbol) : List Symbol

The generator functions, in order.

python.Lowering.table

def Lowering.table (c : Context) (infos : List Symbol) : Either String (List Function)

The program’s table: its functions, then the generator functions’ continuations.

python.Lowering.resumedBody

def Lowering.resumedBody (c : Context) (f : Symbol) : Code

The body of a generator’s continuation.

python.Lowering.modelBody

def Lowering.modelBody (c : Context) (k : Nat) : Code

The body of the model’s own function at a position after the program’s (the built-in generators’, then the sorting functions’).

python.Lowering.bodies

def Lowering.bodies (c : Context) (d : Nat) (k : Nat) : Code

The body of the function at position k of the table (past the functions, the continuations), for calls up to depth d (a call deeper than the recursion limit never runs a body).

python.Exec.reraiseAs

def Exec.reraiseAs (node : String) (text : Place) : Code

Re-raising the exception being handled with the text in a place as its message (its str, as the traceback prints it).

python.Lowering.reported

def Lowering.reported (n : String) (body : Code) : Lowering Code

The program, then what the traceback of an uncaught exception runs: a user’s __str__ of it (its output is the program’s; <exception str() failed> when it raises, as CPython prints), the text kept as the message.

python.Lowering.program

def Lowering.program (p : python.ast.Program) : Either String (Code * Nat)

A program as a statement, with its number of global slots; or the construct the translation cannot take.

python.Lowering.programWith

def Lowering.programWith (observing : Bool) (p : python.ast.Program) : Either String (Code * Nat)

A program as a statement (Lowering.program), noting the types the run sees at each node when observing (Lowering.watching, Lowering.parametersSeen).

python.Lowering.problem

def Lowering.problem (kind : String) (category : String) (reason : String) : Json

A problem of a verdict: its kind, its category (by which a host shows it: error, unsupported, indeterminate, termination, incomplete, invalid), the reason, and no details (not structured yet).

python.Lowering.uncaughtProblem

def Lowering.uncaughtProblem (x : Raised) : Json

The uncaught exception x as a problem; the reason is CPython’s last line. A name not defined is the kind undeclared with the name (what is name: Python does not say whether it was meant as a variable or a function) and where it was raised (when known); any other is uncaught, not structured yet.

python.Lowering.holePrefix

def Lowering.holePrefix : String

The prefix of an editor’s empty slot in a construct’s name.

python.Lowering.untaken

def Lowering.untaken (what : String) : Json

What the translation could not take: an editor’s empty slot (pointing at it), or an unsupported construct.

python.Lowering.choice

def Lowering.choice (c : String) : Json

One choice a verdict assumes, as the C family writes it: the implementation and the choice’s name. A name written implementation:choice (libm:math.correctlyRounded) is made by that implementation; any other by CPython.

python.Lowering.fields

def Lowering.fields (verdict : String) (exit : Json) (out : String) (problems : List Json) (assumes : List String) : List (String * Json)

A verdict’s JSON fields: the verdict, its basis, the exit, the out, the problems, and the choices it assumes.

python.Lowering.uncaught

def Lowering.uncaught (e : Raised) : String

An uncaught exception as CPython’s last line shows it: the type, and the message after a colon when there is one.

python.Lowering.thrown

def Lowering.thrown (s : Run) (x : Raised) : List (String * Json)

The verdict’s fields (Lowering.fields) of a run an exception left: what the model cannot do is unknown; any other exception is defined behavior (exit 1), its text noted as shown (Run.shown: an exception object’s str may show an address).

python.Lowering.outcome

def Lowering.outcome (c : Configuration Run Signal Stop) : List (String * Json)

The verdict’s fields (Lowering.fields) of a run where it got: finished, or out of steps.

python.Lowering.verdictFields

def Lowering.verdictFields (src : String) (input : String) (fuel : Nat) : List (String * Json) * Nat

Decodes a program from JSON (src, a python.ast.Program) and runs it on the input for at most fuel steps: the verdict’s fields (Lowering.fields), and the steps the run took (the fuel when it ran out, 0 when it did not run).

python.Lowering.verdict

def Lowering.verdict (src : String) (input : String) (fuel : Nat) : String

Decodes a program from JSON (python.ast.Program), runs it on the input for at most fuel steps and renders the verdict: {verdict, basis, exit, out, problems, assumes}. An uncaught exception is defined behavior (accept, exit 1, the exception as a problem); running out of steps, or what the model cannot do, is unknown.

python.Lowering.verdictReport

def Lowering.verdictReport (src : String) (input : String) (fuel : Nat) : String

The verdict’s report as JSON: the verdict JSON of the program src (Lowering.verdict) run on the input for at most fuel steps, with the steps the run took as its last field.