execution

python.Run

record Run

A run’s state: the heap, the global and local variables by slot, the console, the random generator, the exception the last expression raised, and the exceptions being handled (innermost first); between preparing a call and entering it, the bound arguments, the function’s position in the table, the instance a class call makes (its __init__ is the function called), and the locals a resumed generator’s continuation starts with; the implementation’s choices noted, and the type texts seen at each node when the run observes types (Run.observe).

python.Signal

data Signal

What a statement returns: a function’s value, or an exception unwinding.

python.Stop

data Stop

Why a run stops: something the model cannot do, or waiting for input.

python.Code

def Code : Type

Python’s statements.

python.Evaluation

data Evaluation

What evaluating an expression gives: the state after it and a value, or the state after it and an exception.

python.Expression

def Expression : Type

Python’s expressions.

python.Run.start

def Run.start (globals : Nat) (input : String) : Run

A run that is about to start: an empty heap, globals global slots, no locals, a console with the input.

python.Heap.chosenOrder

def Heap.chosenOrder (h : Heap) : List String

The implementation’s choices the order of the sets on the heap h depends on, each named once.

python.Run.assumptions

def Run.assumptions (s : Run) : List String

The implementation’s choices the run s assumes, each named once: str.hash (a set ordered by a str’s hash, taken as under PYTHONHASHSEED=0), object.address (a set ordered by objects’ hashes, or an object’s address shown as text, from the model’s addresses), random.seed (a draw before any seed, taken as after seed(0)) and libm:math.correctlyRounded (a call of math.pow, or a float **, whose accuracy CPython leaves to the platform’s math library; the model gives the correctly rounded result).

python.Run.shown

def Run.shown (s : Run) (asRepr : Bool) (vs : List Value) : Either Raised Run

The values vs about to be shown as text (repr of each when asRepr, else str): the run s noting object.address when the text shows an object’s address (the model’s allocation rule, not CPython’s memory); showing a user’s function is what the model cannot do (CPython shows the function’s address, and a function value of the model has none).

python.Run.afterShown

def Run.afterShown (s : Run) (asRepr : Bool) (vs : List Value) (next : Run -> Evaluation) : Evaluation

What follows showing the values vs as text (Run.shown, by repr when asRepr): next evaluated on the run s after it noted that, or what the model cannot do.

python.Run.withHeap

def Run.withHeap (s : Run) (h : Heap) : Run

The run s with the heap h instead.

python.Run.withConsole

def Run.withConsole (s : Run) (c : Console) : Run

The run s with the console c instead.

python.Run.withPending

def Run.withPending (s : Run) (e : Option Raised) : Run

The run s with the exception e pending (or none).

python.Observed.add

def Observed.add (n : String) (t : String) (xs : List (String * List String)) : List (String * List String)

The node n’s type texts xs with the text t seen there (each text once per node, in the order first seen; the nodes in the order first seen).

python.Run.observe

def Run.observe (s : Run) (n : String) (v : Value) : Run

The run s having seen the value v at the node n: its type text (Value.typeText) noted there.

python.Expr.constant

def Expr.constant (v : Value) : Expression

The constant v.

python.Expr.bind

def Expr.bind (e : Expression) (next : Value -> Expression) : Expression

The value of the expression e given to next, or its exception passed on.

python.Expr.all

def Expr.all (es : List Expression) (next : List Value -> Expression) : Expression

The expressions es in order, their values to next (Python evaluates operands left to right).

python.Expr.outcome

def Expr.outcome (f : Heap -> Outcome) : Expression

The outcome the data layer’s f gives on the current heap.

python.Expr.changed

def Expr.changed (f : Heap -> Changed) : Expression

A change of the current heap by the data layer’s f.

python.Place

data Place

Where a variable lives: a global slot, a local slot, or a cell (captured by a nested function) whose reference is in a local slot; with its name for the messages.

python.Run.slot

def Run.slot (slots : Array (Option Value)) (k : Nat) : Option Value

The value of the slot k among slots.

python.Expr.read

def Expr.read (p : Place) : Expression

Reading the variable at p: NameError for a global without a value, UnboundLocalError for a local, a cell’s errors for a captured one.

python.Run.store

def Run.store (s : Run) (p : Place) (v : Value) : Run

The run s with the variable at p given the value v.

python.Run.localValue

def Run.localValue (s : Run) (k : Nat) : Value

The value of the local slot k of the run s (None when it has none).

python.Run.placeValue

def Run.placeValue (s : Run) (p : Place) : Value

The value in the slot of the variable at p in the run s (None when it has none; a cell’s slot holds its reference).

python.Exec.keep

def Exec.keep (v : Value) (s : Run) : Run

Keeping the run s as it is (v, an expression statement’s value, is dropped).

python.Exec.storing

def Exec.storing (p : Place) (v : Value) (s : Run) : Run

Storing the value v into the variable at p in the run s.

python.Raised.ofBuiltin

def Raised.ofBuiltin (type : Codes) (message : Codes) : Raised

A built-in exception raised with its type and message.

python.Run.cannot

def Run.cannot (e : Raised) : Bool

Whether the exception e is one a stop reports: what the model cannot do.

python.Exec.evaluate

def Exec.evaluate (e : Expression) (store : Value -> Run -> Run) : Code

Evaluating the expression e, then changing the state with store given its value; an exception becomes pending (what the model cannot do stops the run).

python.Exec.check

def Exec.check : Code

Raising the pending exception, if there is one.

python.Exec.checkAt

def Exec.checkAt (node : String) : Code

Raising the pending exception, if there is one, marked as raised at node when it has no node yet (the innermost one, as a traceback’s last line; not the model’s own nodes, builtin ... and model ...).

python.Exec.at

def Exec.at (node : String) (work : Code) : Code

A source statement at node: the node for the debugger, the work, the check.

python.Expr.observed

def Expr.observed (n : String) (e : Expression) : Expression

The expression e, its value’s type noted at the node n (Run.observe).

python.Exec.observePlace

def Exec.observePlace (n : String) (p : Place) : Code

The value in the place p noted at the node n (Run.observe); nothing when it has none.

python.Exec.assign

def Exec.assign (node : String) (p : Place) (e : Expression) : Code

x = e at node, the variable at p being the one target x.

python.Exec.expression

def Exec.expression (node : String) (e : Expression) : Code

An expression statement at node: the value of e is dropped.

python.Expr.print

def Expr.print (values : List Value) (sep : Value) (finish : Value) : Expression

print(*values, sep=' ', end='\n'), finish being end: the str of each value (an int too long is ValueError), sep between, end after (sep and end must be None or a str).

python.Expr.truth

def Expr.truth (e : Expression) : Expression

The truth of the value of e for if and while (a user’s __bool__ or __len__ is the lowering’s to run first).

python.Exec.holds

def Exec.holds (p : Place) : Run -> Checked Stop Bool

A truth already evaluated into the slot of the variable at p, as the machine’s condition.

python.Exec.ifThen

def Exec.ifThen (node : String) (scratch : Place) (c : Expression) (yes : Code) (no : Code) : Code

if c: yes else: no at node: the condition’s truth evaluated into the place scratch first (it may raise).

python.Exec.whileLoop

def Exec.whileLoop (node : String) (scratch : Place) (c : Expression) (body : Code) : Code

while c: body at node: each round the condition’s truth into the place scratch, leaving when it is false.

python.Exec.breakOut

def Exec.breakOut (node : String) : Code

break at node.

python.Exec.continueOn

def Exec.continueOn (node : String) : Code

continue at node.

python.Exec.returnWith

def Exec.returnWith (node : String) (scratch : Place) (e : Expression) : Code

return e at node: the value evaluated into the place scratch, then returned.

python.Raised.ofInstance

def Raised.ofInstance (h : Heap) (a : Nat) (v : Value) : Raised

The instance v of a user’s exception class, at the address a on the heap h, raised: its classes, its text, its object.

python.Raised.ofClass

def Raised.ofClass (h : Heap) (cls : Value) : Changed

The user’s exception class cls raised as a class: a new instance on the heap h with no arguments, raised.

python.Raised.ofValue

def Raised.ofValue (h : Heap) (v : Value) : Changed

The exception the raised value v is, on the heap h: an exception instance (built-in or a user’s), or a class instantiated with no arguments; TypeError for anything else.

python.Exec.raise

def Exec.raise (node : String) (e : Expression) : Code

raise e at node: the exception pending (a value that is not an exception is TypeError).

python.Exec.reraise

def Exec.reraise (node : String) : Code

A bare raise at node: the exception being handled again; RuntimeError when none is.

python.Exec.run

def Exec.run (fuel : Nat) (c : Code) (s : Run) : Configuration Run Signal Stop

Running the statement c on the state s with a budget of fuel moves.

python.Exec.change

def Exec.change (f : Run -> Run) : Code

The change f of the state, which cannot fail.

python.Exec.only

def Exec.only (c : Code) : Code

The switch block c, not falling through to the next (the machine’s switch is C’s).

python.Exec.caseAt

def Exec.caseAt (k : Nat) : SwitchLabel

The switch label of block k.

python.Raised.value

def Raised.value (e : Raised) : Value

The value the exception e is when it is caught: the object of a user’s exception, else a built-in exception’s value.

python.Raised.isInstance

def Raised.isInstance (h : Heap) (cls : Value) (e : Raised) : Bool

Whether an except clause’s class cls catches the exception e on the heap h: a built-in class by the exception’s chain (a built-in exception’s chain from its type), a user’s class by isinstance of the exception’s object.

python.Raised.isAny

def Raised.isAny (h : Heap) (classes : List Value) (e : Raised) : Bool

Whether any of the classes catches the exception e on the heap h.

python.Clause

record Clause

An except clause: the classes it catches (read from the state when an exception arrives; none: a bare except), where as binds the exception, and its body.

python.Clause.first

def Clause.first (s : Run) (e : Raised) (clauses : List Clause) : Option Clause

The first of the clauses that catches the exception e in the run s.

python.Run.catching

def Run.catching (s : Run) (e : Raised) (c : Clause) : Run

The run s when the clause c catches the exception e: nothing pending, the exception handled, bound with as.

python.Run.handled

def Run.handled (s : Run) : Run

The run s after a clause: the exception no longer handled.

python.Exec.tryExcept

def Exec.tryExcept (flag : Place) (body : Code) (clauses : List Clause) (otherwise : Code) : Code

try: body except ...: clauses else: otherwise: a clause that catches the exception runs with it handled (its end, by any way out, stops handling it); no clause catching passes the exception on; else runs when the body raised nothing (the lowering’s slot flag marks that).

python.Exec.clauseBody

def Exec.clauseBody (clauses : List Clause) (e : Raised) : Code

The body of the one of the clauses that caught the exception e (looked up again from the state the catch left), chosen by tests one after another: not a switch, whose blocks a break in the clause would leave instead of the loop.

python.Exec.clauseFrom

def Exec.clauseFrom (all : List Clause) (e : Raised) (clauses : List Clause) (k : Nat) : Code

The clauses from position k of all: the body of the one at the position of the first that catches the exception e.

python.Clause.index

def Clause.index (s : Run) (e : Raised) (clauses : List Clause) (k : Nat) : Nat

Where the first of the clauses catching the exception e in the run s is, counting from k.

python.Exec.tryFinally

def Exec.tryFinally (body : Code) (cleanup : Code) : Code

finally: the cleanup runs on every way out of the body (an exception’s pending mark cleared first).

python.Function

record Function

A user’s function as the program’s table has it: its function value’s name, its parameters, and how many local slots its body uses.

python.Run.construct

def Run.construct (functions : List Function) (result : Place) (s : Run) (c : Value) (positional : List Value) (keywords : List (Codes * Value)) : Evaluation

Calling the user’s class c in the run s with the arguments positional and keywords: a new instance, then its __init__ (a user’s function among the program’s functions, bound to the instance) prepared with the arguments and the instance kept for when it returns; without one, TypeError for arguments the class does not take (Objects.withoutInit), else the instance into result.

python.Run.showsArguments

def Run.showsArguments (name : String) : Option Bool

Whether the built-in name shows its arguments as text, and how (repr is true): repr and ascii by repr; str, format, print and input (its prompt) by str.

python.Run.assuming

def Run.assuming (s : Run) (choice : String) : Run

The run s assuming the implementation’s choice choice (named once).

python.Run.native

def Run.native (s : Run) (name : String) (arguments : List Value) (call : Run -> Evaluation) : Evaluation

The call of the built-in name on the run s, after what it shows of its arguments is noted (Run.shown).

python.Run.raisedForKeys

def Run.raisedForKeys (s : Run) (e : Raised) (keys : List Value) : Evaluation

The exception e raised in the run s while looking up the keys: a KeyError’s message is the key’s repr, so the run goes on after Run.shown on the keys (or with what the model cannot do); any other exception as it is.

python.Run.builtinClass

def Run.builtinClass (result : Place) (s : Run) (name : Codes) (positional : List Value) (keywords : List (Codes * Value)) : Evaluation

Calling the built-in class name in the run s with the arguments positional and keywords, its result into result: an exception class makes an instance with the arguments as its args (TypeError for keyword arguments), any other is the built-in function of its name (int, str, list and so on).

python.Run.prepare

def Run.prepare (functions : List Function) (result : Place) (s : Run) (callee : Value) (positional : List Value) (keywords : List (Codes * Value)) : Evaluation

Preparing the call of callee in the run s with the arguments positional and keywords, its result into result: a user’s class makes an instance (Run.construct), a built-in class is called (Run.builtinClass), anything else is a call of a function among the program’s functions.

python.Function.index

def Function.index (functions : List Function) (name : Codes) (k : Nat) : Option Nat

Where the function whose value’s name is name is in the table functions, counting from k.

python.Exec.recursionLimit

def Exec.recursionLimit : Nat

The most frames of the user’s functions there are at once (CPython’s recursion limit of 1000, the module’s frame being one).

python.Function.internal

def Function.internal (name : Codes) : Bool

Whether the function in the table named name is the model’s own (a built-in generator’s continuation, builtin map.<resume>, or a helper such as model sort; a user’s name has no space): CPython runs those in C, so their frames do not count toward the recursion limit.

python.Exec.builtinName

def Exec.builtinName (f : Value) : Option String

A built-in function’s name from its value f (builtin len).

python.Run.prepareFunction

def Run.prepareFunction (functions : List Function) (result : Place) (s : Run) (callee : Value) (positional : List Value) (keywords : List (Codes * Value)) : Evaluation

Preparing the call of callee in the run s once it and the arguments positional and keywords are known: a user’s function’s parameters bound, the cells its value captured after them (its position in the program’s functions is the call’s target), a built-in one called right away (its result stored in result, no target; the random module’s draw from the run’s generator); TypeError for a value that cannot be called.

python.Exec.indexIn

def Exec.indexIn (functions : List Function) (name : Codes) : Option Nat

Where the function whose value’s name is name is in the table functions.

python.Value.functionName

def Value.functionName (f : Value) : Option Codes

A function value’s name, if f is a user’s function.

python.Exec.noSignature

def Exec.noSignature : Signature

A signature for nothing (the table is never asked past its end).

python.Run.enter

def Run.enter (internal : Bool) (slots : Nat) (s : Run) : Run

Entering a function from the run s: its locals are the bound parameters and empty slots after them up to slots (or, resuming a generator, the locals it kept), one frame deeper unless the function is the model’s own (internal, by Function.internal).

python.Run.leave

def Run.leave (result : Place) (saved : Run) (t : Run) (r : Option Signal) : Run

Back in the caller from the callee’s run t: the locals and depth of saved (the run when the call began) again, and the value the signal r returned (None when the body ended) stored in result; when a user’s class was called, the instance instead, TypeError (pending) when __init__ returned anything but None.

python.Run.unwound

def Run.unwound (saved : Run) (t : Run) : Run

Back in the caller from the callee’s run t, with the locals and depth of saved (the run when the call began), while an exception unwinds through the call.

python.Signal.unwinds

def Signal.unwinds (r : Signal) : Bool

Whether the signal r passes through a call: an exception does.

python.Exec.callAt

def Exec.callAt (site : String) (functions : List Function) (bodies : Nat -> Code) (result : Place) (k : Nat) : Code

The call at the source statement site of the function at position k of the program’s functions, its body (from their bodies) built when the call is reached, its result into result.

python.Exec.dispatch

def Exec.dispatch (node : String) (functions : List Function) (bodies : Nat -> Code) (result : Place) (prepared : Expression) : Code

A source statement at node that may call a user’s function: the expression prepared prepares the call (or finishes without one), then the function at the prepared position runs (with the program’s functions and their bodies), its result into result; the checks raise what is pending.

python.Exec.call

def Exec.call (node : String) (functions : List Function) (bodies : Nat -> Code) (callee : Expression) (positional : List Expression) (keywords : List (Codes * Expression)) (result : Place) : Code

result = callee(*positional, **keywords) at node, with the program’s functions and their bodies, where the callee may be a user’s function or class: the callee and the arguments evaluated left to right, the parameters bound, then the function’s body run.

python.Run.access

def Run.access (functions : List Function) (result : Place) (s : Run) (a : Access) : Evaluation

The attribute access a as an evaluation in the run s: its value into result, its exception, or the call of the getter or setter it needs (a user’s code, among the program’s functions).

python.Exec.getAttribute

def Exec.getAttribute (node : String) (functions : List Function) (bodies : Nat -> Code) (object : Expression) (name : String) (result : Place) : Code

result = object.name at node, the attribute name read from object, with the program’s functions and their bodies: a property’s getter runs as a call.

python.Exec.setAttribute

def Exec.setAttribute (node : String) (functions : List Function) (bodies : Nat -> Code) (object : Expression) (name : String) (value : Expression) (scratch : Place) : Code

object.name = value at node, the attribute name written on object (the value first, then the object, as CPython evaluates them), with the program’s functions and their bodies: a property’s setter runs as a call, its result into the place scratch.

python.Exec.pairs

def Exec.pairs (names : List Codes) (values : List Value) : List (Codes * Value)

The names paired with the values in order.

python.Expr.function

def Expr.function (name : String) (cells : List Expression) (defaults : List Expression) : Expression

The function value name made by def: with the cells it captures and its defaults evaluated now.

python.Unpack.valueError

def Unpack.valueError (parts : List String) : Items

Unpacking failed with a ValueError (its message in parts).

python.Unpack.cannot

def Unpack.cannot (h : Heap) (v : Value) (e : Raised) : Items

The exception e of the iterable v on the heap h while unpacking it: a TypeError says the value cannot be unpacked.

python.Unpack.taking

def Unpack.taking (fuel : Nat) (h : Heap) (it : Value) (count : Nat) (so : List Value) : Taken

The values of the iterator it on the heap h for unpacking into count targets, after the values so far (the latest first), taking one item at a time within fuel items (an iterator gives at most one item more than the count, as CPython takes it): ValueError for too few, or for one too many.

python.Unpack.exactly

def Unpack.exactly (h : Heap) (v : Value) (count : Nat) : Taken

a, b = v on the heap h with count targets and no star (CPython’s unpack_iterable): a list or tuple by its length (the messages say how many it had), anything else one item at a time; TypeError for what cannot be iterated.

python.Unpack.split

def Unpack.split (now : Heap) (xs : List Value) (before : Nat) (after : Nat) : Taken

a, *b, c = v from all the items xs, on the heap now: before items, the rest as a new list, after items.

python.Unpack.starred

def Unpack.starred (h : Heap) (v : Value) (before : Nat) (after : Nat) : Taken

a, *b, c = v on the heap h: before items, the rest as a new list, after items; ValueError when there are fewer than those together.

python.Exec.nextItem

def Exec.nextItem (iterator : Place) (item : Place) (ended : Place) : Expression

The next item of a for loop’s iterator, held in the place iterator, into the place item, or the end marked in the flag ended.

python.Exec.forLoop

def Exec.forLoop (node : String) (iterator : Place) (item : Place) (ended : Place) (iterable : Expression) (target : Code) (body : Code) (otherwise : Code) : Code

for target in iterable: body else: otherwise at node: an iterator over the iterable into the place iterator, then each round the next item into the place item (the end marked in the flag ended, which else reads: a break leaves it unmarked), the target assigned from it, the body.

python.Expr.taken

def Expr.taken (t : Taken) : Expression

The items t holds as a tuple (the targets are stored from it), or its exception.

python.Value.tupleItems

def Value.tupleItems (v : Value) : List Value

The items of the tuple v (none for anything else).

python.Run.storeAll

def Run.storeAll (s : Run) (targets : List Place) (vs : List Value) : Run

The values vs into the places targets in the run s, in order.

python.Run.items

def Run.items (s : Run) (p : Place) : List Value

The items of a tuple held in the place p in the run s.

python.Run.itemAt

def Run.itemAt (s : Run) (p : Place) (k : Nat) : Value

The k-th item of a tuple held in the place p in the run s (None past the end).

python.Exec.unpack

def Exec.unpack (node : String) (source : Expression) (targets : List Place) : Code

a, b = source at node: the source’s items into the targets, as many as there are targets.

python.Exec.unpackStarred

def Exec.unpackStarred (node : String) (source : Expression) (before : List Place) (rest : Place) (after : List Place) : Code

a, *rest, c = source at node: the first and last items into the targets before and after, the rest as a new list into rest.