dispatch

python.Value.special

def Value.special (h : Heap) (v : Value) (name : String) : Option Value

A user’s special method name of the value v on the heap h, bound to it: looked up on its class along the order (not the instance’s own attributes, as CPython does); none for anything but an instance of a user’s class.

python.Value.hasSpecial

def Value.hasSpecial (h : Heap) (v : Value) (name : String) : Bool

Whether the class of the value v on the heap h has the special method name.

python.Exec.steps

def Exec.steps (cs : List Code) : Code

The statements cs in order.

python.Exec.when

def Exec.when (test : Run -> Bool) (yes : Code) : Code

The statement yes run when the test of the run holds.

python.Exec.put

def Exec.put (p : Place) (v : Value) : Code

The value v into the place p.

python.Exec.flag

def Exec.flag (p : Place) (test : Run -> Bool) : Code

The truth of the test of the run into the place p, as a bool.

python.Exec.choose

def Exec.choose (test : Run -> Bool) (yes : Code) (no : Code) : Code

One of two statements, yes or no, by the test of the run.

python.Run.declined

def Run.declined (s : Run) (p : Place) : Bool

Whether the place p holds NotImplemented in the run s.

python.Run.holds

def Run.holds (s : Run) (p : Place) : Bool

Whether the place p holds a true value in the run s.

python.Exec.special

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

result = receiver.name(*arguments) at node, with the program’s functions and their bodies, for the special method name the receiver’s class has (the arguments read from places), run as a call.

python.Dispatch.reflectedFirst

def Dispatch.reflectedFirst (h : Heap) (a : Value) (b : Value) (reflected : String) : Bool

Whether the method reflected of the right operand b goes first, on the heap h: its class is a user’s, a proper subclass of the class of the left operand a, with that method.

python.Dispatch.tryReflected

def Dispatch.tryReflected (h : Heap) (a : Value) (b : Value) (comparison : Bool) : Bool

Whether the reflected method of the right operand b is tried after the left operand a’s, on the heap h: always for a comparison, for arithmetic when the classes differ.

python.Exec.binary

def Exec.binary (node : String) (functions : List Function) (bodies : Nat -> Code) (method : String) (reflected : String) (comparison : Bool) (base : Value -> Value -> Expression) (a : Expression) (b : Expression) (left : Place) (right : Place) (result : Place) (first : Place) : Code

result = a op b at node, with the program’s functions and their bodies: the user’s methods (method, its reflected reflected), then the built-in operation base when every method gave NotImplemented; the reflected one is tried after the left’s even for the same class when it is a comparison. The operands in the places left and right, whether the reflected method went first in the place first.

python.Value.sameObject

def Value.sameObject (a : Value) (b : Value) : Bool

Whether the values a and b are the same object (is).

python.Dispatch.equal

def Dispatch.equal (a : Value) (b : Value) : Expression

The built-in a == b after the user’s methods: identity when either defines __eq__ (they gave NotImplemented), else equality by contents.

python.Dispatch.order

def Dispatch.order (symbol : String) (a : Value) (b : Value) : Expression

The built-in ordering symbol of a and b after the user’s methods: TypeError when either defines a comparison (they gave NotImplemented), else the order of the data layer.

python.Exec.notEqual

def Exec.notEqual (node : String) (functions : List Function) (bodies : Nat -> Code) (a : Expression) (b : Expression) (left : Place) (right : Place) (result : Place) (first : Place) : Code

result = a != b at node, with the program’s functions and their bodies: __ne__ (both ways), else not (a == b) with __eq__; the operands in the places left and right, whether the reflected method went first in the place first (as in Exec.binary).

python.Exec.unary

def Exec.unary (node : String) (functions : List Function) (bodies : Nat -> Code) (method : String) (base : Value -> Expression) (a : Expression) (operand : Place) (result : Place) : Code

result = op a (-a, +a, ~a, abs(a)) at node, with the program’s functions and their bodies: the user’s method, else the built-in operation base; the operand in the place operand.

python.Dispatch.length

def Dispatch.length (v : Value) : Expression

What __len__ gave, v, checked: a non-negative int (a bool counts as one), else ValueError or TypeError.

python.Exec.length

def Exec.length (node : String) (functions : List Function) (bodies : Nat -> Code) (a : Expression) (operand : Place) (result : Place) : Code

result = len(a) at node, with the program’s functions and their bodies: the user’s __len__ (checked), else the built-in length; the operand in the place operand.

python.Dispatch.boolean

def Dispatch.boolean (v : Value) : Expression

What __bool__ gave, v, checked: a bool, else TypeError.

python.Exec.truth

def Exec.truth (node : String) (functions : List Function) (bodies : Nat -> Code) (a : Expression) (operand : Place) (result : Place) : Code

result = bool(a) at node (the truth if, while, not, and and or use), with the program’s functions and their bodies: __bool__ (checked), else __len__ (checked, true when not zero), else the built-in truth; the operand in the place operand.

python.Expr.ofChanged

def Expr.ofChanged (f : Run -> Changed) : Expression

The change of the heap f computes from the run, as an expression.

python.Expr.ofOutcome

def Expr.ofOutcome (f : Run -> Outcome) : Expression

The outcome f computes from the run, as an expression.

python.Dispatch.unsupported

def Dispatch.unsupported (what : String) : Raised

Unsupported: what CPython would do by running a user’s what in a way the model does not take.

python.Exec.contains

def Exec.contains (node : String) (functions : List Function) (bodies : Nat -> Code) (x : Expression) (c : Expression) (item : Place) (container : Place) (result : Place) : Code

result = x in c at node, with the program’s functions and their bodies: the user’s __contains__ (its truth), else the data layer’s; x and c evaluated into the places item and container.

python.Exec.containsBy

def Exec.containsBy (node : String) (functions : List Function) (bodies : Nat -> Code) (x : Expression) (c : Expression) (item : Place) (container : Place) (result : Place) (iterator : Place) (element : Place) (ended : Place) (trying : Place) (left : Place) (right : Place) (equal : Place) (first : Place) (operand : Place) : Code

x in c at node, with the program’s functions and their bodies, for a list or tuple when x or an item defines comparison methods, as CPython’s list.__contains__: each item in turn (the list as it is then), true at the first that is x or equals it (item == x: the item’s __eq__, then the reflected one); else Exec.contains. x and c go into the places item and container, the answer into result; the loop’s places are iterator, element (each item), the end flag ended and trying (the flag place of the try around a user’s __next__); the comparison’s are left, right, equal (its result), first and operand (as in Exec.binary and Exec.truth).

python.Expr.forKey

def Expr.forKey (key : Place) (e : Expression) : Expression

The expression e looking up the key in the place key: a KeyError it raises shows the key’s repr (Run.raisedForKeys).

python.Exec.getItem

def Exec.getItem (node : String) (functions : List Function) (bodies : Nat -> Code) (c : Expression) (k : Expression) (container : Place) (key : Place) (result : Place) : Code

result = c[k] at node, with the program’s functions and their bodies: the user’s __getitem__, else the data layer’s; c and k evaluated into the places container and key.

python.Exec.setItem

def Exec.setItem (node : String) (functions : List Function) (bodies : Nat -> Code) (c : Expression) (k : Expression) (v : Expression) (container : Place) (key : Place) (value : Place) (scratch : Place) : Code

c[k] = v at node (the value first, then the container and the key, as CPython evaluates them), with the program’s functions and their bodies: the user’s __setitem__ (its result into the place scratch), else the data layer’s; v, c and k evaluated into the places value, container and key.

python.Exec.deleteItem

def Exec.deleteItem (node : String) (functions : List Function) (bodies : Nat -> Code) (c : Expression) (k : Expression) (container : Place) (key : Place) (scratch : Place) : Code

del c[k] at node, with the program’s functions and their bodies: the user’s __delitem__ (its result into the place scratch), else the data layer’s; c and k evaluated into the places container and key.

python.Dispatch.isIterator

def Dispatch.isIterator (h : Heap) (v : Value) : Bool

Whether the value v on the heap h is an iterator: a user’s object with __next__, or a built-in iterator or generator.

python.Dispatch.iterator

def Dispatch.iterator (v : Value) : Expression

What __iter__ gave, v, checked: an iterator, else TypeError.

python.Dispatch.builtinIterator

def Dispatch.builtinIterator (v : Value) : Expression

A built-in iterator over the value v (unsupported for a user’s object iterated by __getitem__ alone).

python.Exec.iterate

def Exec.iterate (node : String) (functions : List Function) (bodies : Nat -> Code) (iterable : Expression) (iterator : Place) : Code

iterator = iter(iterable) at node, with the program’s functions and their bodies: the user’s __iter__ (checked), else the built-in iterator.

python.Exec.advance

def Exec.advance (node : String) (functions : List Function) (bodies : Nat -> Code) (iterator : Place) (item : Place) (ended : Place) (trying : Place) : Code

The next item of the iterator in the place iterator into the place item, or the end marked in the flag ended, at node with the program’s functions and their bodies: a generator resumed (Exec.resume), the user’s __next__ (StopIteration is the end; the try needs its own flag place, trying), else the built-in iterator’s.

python.Exec.forEachFrom

def Exec.forEachFrom (node : String) (functions : List Function) (bodies : Nat -> Code) (iterator : Place) (item : Place) (ended : Place) (trying : Place) (target : Code) (body : Code) (otherwise : Code) : Code

The rounds of for over the iterator already in the place iterator (Exec.forEach without taking iter first), at node with the program’s functions and their bodies: each round the next item into the place item (the end flag ended; trying (the flag place of the try around a user’s __next__)), the target assigned from it, the body; otherwise when the loop ran out without a break.

python.Exec.forEach

def Exec.forEach (node : String) (functions : List Function) (bodies : Nat -> Code) (iterator : Place) (item : Place) (ended : Place) (trying : Place) (iterable : Expression) (target : Code) (body : Code) (otherwise : Code) : Code

for target in iterable: body else: otherwise at node, with the program’s functions and their bodies, with the user’s iteration methods (Exec.forLoop is the built-in iteration alone); the loop’s places are iterator, item (each item), the end flag ended and trying (the flag place of the try around a user’s __next__).

python.Dispatch.lengthHint

def Dispatch.lengthHint (v : Value) : Expression

What __length_hint__ gave, v, checked: NotImplemented (no hint) or a non-negative int, else ValueError or TypeError.

python.Exec.lengthHint

def Exec.lengthHint (node : String) (functions : List Function) (bodies : Nat -> Code) (iterable : Place) (result : Place) : Code

How many items the iterable in the place iterable says it has before list takes them (CPython’s PyObject_LengthHint, in the place result), at node with the program’s functions and their bodies: a user’s __len__ (checked; a TypeError, raised in it or by the check, is dropped), else a user’s __length_hint__; nothing for the built-in values, whose lengths run no code.

python.Exec.gathered

def Exec.gathered (node : String) (functions : List Function) (bodies : Nat -> Code) (hinted : Bool) (round : Code) (iterable : Place) (into : Place) (iterator : Place) (item : Place) (ended : Place) (trying : Place) : Code

The iterable in the place iterable, when it runs a user’s code or uses up an iterator (a generator, say), gathered into a new list in the place into, at node with the program’s functions and their bodies: its items taken as for takes them (each followed by round; after iter, its length hint first when hinted, as list and list.extend take it), for a built-in that takes them all (list, sum); any other value put there as it is. The loop’s places are iterator, item (each item), the end flag ended and trying (the flag place of the try around a user’s __next__).

python.Exec.takeRunning

def Exec.takeRunning (node : String) (functions : List Function) (bodies : Nat -> Code) (limit : Option Nat) (hintAfter : Option Nat) (value : Place) (items : Place) (iterator : Place) (item : Place) (ended : Place) (trying : Place) : Code

Items of the iterable in the place value that runs a user’s code (a generator, a user’s iteration) taken as for takes them into a new list in the place items, at node with the program’s functions and their bodies: at most limit of them (all with none), the iterator’s length hint once hintAfter are taken (as list takes the rest of a starred unpacking). The loop’s places are iterator, item (each item), the end flag ended and trying (the flag place of the try around a user’s __next__).

python.Unpack.counted

def Unpack.counted (xs : List Value) (count : Nat) : Items

The items xs taken for unpacking into count targets (at most one more than the count, as CPython takes them from an iterator): ValueError for too few, or for one too many.

python.Unpack.splitAtLeast

def Unpack.splitAtLeast (h : Heap) (xs : List Value) (before : Nat) (after : Nat) : Taken

The items xs taken for 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.unpackRunning

def Exec.unpackRunning (node : String) (functions : List Function) (bodies : Nat -> Code) (value : Place) (targets : List Place) (items : Place) (iterator : Place) (item : Place) (ended : Place) (trying : Place) : Code

a, b = v at node, with the program’s functions and their bodies, for an iterable in the place value that runs a user’s code: at most one item more than the targets taken into the place items (Exec.takeRunning, with the loop’s places iterator, item, ended and trying), then the targets from them.

python.Exec.unpackRunningStarred

def Exec.unpackRunningStarred (node : String) (functions : List Function) (bodies : Nat -> Code) (value : Place) (before : List Place) (rest : Place) (after : List Place) (items : Place) (iterator : Place) (item : Place) (ended : Place) (trying : Place) : Code

a, *b, c = v at node, with the program’s functions and their bodies, for an iterable in the place value that runs a user’s code: all its items taken into the place items (the iterator’s length hint after the targets before the star; Exec.takeRunning, with the loop’s places iterator, item, ended and trying), then the targets before, rest and after from them.

python.Exec.anyAll

def Exec.anyAll (node : String) (functions : List Function) (bodies : Nat -> Code) (round : Code) (all : Bool) (iterable : Expression) (result : Place) (iterator : Place) (item : Place) (ended : Place) (trying : Place) (operand : Place) : Code

any(iterable) (all false) and all(iterable) (all true; all tells which) into the place result, at node with the program’s functions and their bodies: the items taken one by one as for takes them, stopping at the first that decides (round after each that does not); the loop’s places are iterator, item (each item), the end flag ended and trying (the flag place of the try around a user’s __next__), each item’s truth through the place operand.

python.Exec.raiseStop

def Exec.raiseStop (node : String) (value : Place) : Code

StopIteration raised at node with the value in the place value (a generator’s return value): an instance whose args are the value (none for None) and whose value is it, as CPython makes it.

python.Exec.nextOf

def Exec.nextOf (node : String) (functions : List Function) (bodies : Nat -> Code) (iterator : Place) (default : Option Expression) (result : Place) (ended : Place) (trying : Place) : Code

next(iterator) and next(iterator, default) into the place result, at node with the program’s functions and their bodies, as for takes an item (Exec.advance, with the end flag ended and trying (the flag place of the try around a user’s __next__)); when there is none, the default, or StopIteration (with a generator’s return value).

python.Exec.resumeMethod

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

A generator’s send(value) (how 0), throw(value) (how 1) and close() (how 2) into the place result, at node with the program’s functions and their bodies (Exec.resume; the generator in the place generator, the end flag ended, trying (the flag place of the try around a user’s __next__)): what it yields; when it ends, send and throw raise StopIteration with its return value.

python.Raised.isAttributeError

def Raised.isAttributeError (e : Raised) : Bool

Whether the exception e is an AttributeError.

python.Exec.attribute

def Exec.attribute (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: the user’s __getattr__ for an attribute the object does not have. A built-in value’s method read without calling it ([].append) is not taken: the model has its methods only as calls (Methods.of), and CPython’s value there is a bound method, not an AttributeError.

python.Exec.assignAttribute

def Exec.assignAttribute (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), with the program’s functions and their bodies: the user’s __setattr__ when the class has one; the result into the place scratch.

python.Dispatch.targets

def Dispatch.targets (h : Heap) (top : Bool) (v : Value) : Value

The methods the text of the value v on the heap h needs (__str__ at the top when top holds), as a tuple of (instance, bound method, whether it is __str__) triples.

python.Dispatch.firstTarget

def Dispatch.firstTarget (v : Value) : Showing

The first of the targets still to run in the tuple v, as a Showing.

python.Exec.resolve

def Exec.resolve (node : String) (functions : List Function) (bodies : Nat -> Code) (value : Run -> Value) (top : Bool) (pending : Place) (result : Place) : Code

Runs, at node with the program’s functions and their bodies, the methods the text of the run’s value needs (__str__ at the top when top holds, __repr__ inside), in order, their texts kept on the instances (TypeError for a method that does not return a str); the targets still to run in the place pending, each method’s result in the place result.

python.Exec.text

def Exec.text (node : String) (functions : List Function) (bodies : Nat -> Code) (asRepr : Bool) (a : Expression) (operand : Place) (pending : Place) (result : Place) : Code

result = str(a) or repr(a) (by asRepr) at node, with the program’s functions and their bodies: the methods it needs run first (Exec.resolve, with the place pending), then the built-in text; the operand in the place operand.

python.Dispatch.textOption

def Dispatch.textOption (what : String) (v : Value) : Expression

TypeError unless the value v is None or a str (print’s sep and end, named by what).

python.Exec.printChecked

def Exec.printChecked (node : String) (options : Place) (result : Place) : Code

The checks at node of print’s options (the tuple of sep and end in the place options): each None or a str, else TypeError; the place result takes the checks’ value.

python.Exec.printAt

def Exec.printAt (node : String) (functions : List Function) (bodies : Nat -> Code) (arguments : Place) (options : Place) (position : Run -> Nat) (pending : Place) (result : Place) : Code

One of print’s values written at node with the program’s functions and their bodies: the one at the position (from the run) of the tuple in the place arguments, with the options’ tuple in options; the separator first unless it is the first (a space for a None sep), its str (the user’s __str__ run, by Exec.resolve with the places pending and result), the text.

python.Exec.printEnd

def Exec.printEnd (node : String) (options : Place) (result : Place) : Code

print’s end written at node, from the options’ tuple in the place options; print’s value, None, into the place result (which held the checked options and the values’ text).

python.Exec.print

def Exec.print (node : String) (functions : List Function) (bodies : Nat -> Code) (values : List Expression) (sep : Expression) (finish : Expression) (arguments : Place) (options : Place) (pending : Place) (result : Place) : Code

print(values, sep=, end=) at node, with the program’s functions and their bodies, finish being end: the values and the options in tuples (in the places arguments and options), the options checked, each value written (Exec.printAt, with the places pending and result).

python.Run.position

def Run.position (s : Run) (p : Place) : Nat

The natural number kept in the place p in the run s (a counter).

python.Exec.printFrom

def Exec.printFrom (node : String) (functions : List Function) (bodies : Nat -> Code) (arguments : Place) (options : Place) (index : Place) (pending : Place) (result : Place) : Code

print, at node with the program’s functions and their bodies, of values gathered at run time (print(*xs)): the tuple in the place arguments and the options’ tuple in options already there; each value written in turn (with the places pending and result), its position counted in the place index.

python.Dispatch.calleeName

def Dispatch.calleeName (h : Heap) (f : Value) : String

What a call’s TypeError names for the callee f on the heap h: a user’s function or class as __main__. and its qualified name, a built-in by its name, a bound method by its function.

python.Dispatch.unpackable

def Dispatch.unpackable (h : Heap) (v : Value) : Bool

Whether *v can be unpacked in a call, on the heap h: it is iterable (__iter__) or a sequence (__getitem__).

python.Exec.typeError

def Exec.typeError (node : String) (message : Run -> String) : Code

A TypeError raised at node with the message from the run.

python.Exec.appendTo

def Exec.appendTo (node : String) (items : Place) (value : Place) : Code

The value in the place value appended to the list in the place items, at node.

python.Exec.unpackInto

def Exec.unpackInto (node : String) (functions : List Function) (bodies : Nat -> Code) (hinted : Bool) (message : Option (Run -> String)) (iterable : Place) (items : Place) (iterator : Place) (item : Place) (ended : Place) (trying : Place) : Code

*iterable at node, with the program’s functions and their bodies: the items of the iterable in the place iterable appended to the list in the place items as for takes them (after iter, its length hint first when hinted, as a list or tuple display takes it); when it cannot be unpacked, TypeError with the message given (or, with none, the one iter raises). The loop’s places are iterator, item (each item), the end flag ended and trying (the flag place of the try around a user’s __next__).

python.Exec.spreadItems

def Exec.spreadItems (node : String) (functions : List Function) (bodies : Nat -> Code) (callee : Place) (iterable : Place) (items : Place) (iterator : Place) (item : Place) (ended : Place) (trying : Place) : Code

*iterable among a call’s arguments at node, with the program’s functions and their bodies (Exec.unpackInto: the iterable in the place iterable, its items into the list in the place items, with the loop’s places iterator, item, ended and trying), the TypeError naming the callee in the place callee.

python.Exec.mergeInto

def Exec.mergeInto (node : String) (mapping : Place) (into : Place) : Code

**mapping in a dict display at node: the pairs of the dict in the place mapping stored into the dict in the place into (a later key replacing an earlier one); a user’s mapping is not taken yet; TypeError for anything else.

python.Dispatch.keyword

def Dispatch.keyword (h : Heap) (callee : Value) (pairs : List (Value * Value)) (key : Value) (v : Value) : Either Raised (List (Value * Value))

The keyword argument key with the value v added to the pairs gathered so far (the callee for the message, on the heap h): TypeError when the key is not a str, or when the call already has it.

python.Dispatch.keywords

def Dispatch.keywords (h : Heap) (callee : Value) (pairs : List (Value * Value)) (more : List (Value * Value)) : Either Raised (List (Value * Value))

The keyword arguments more added in order to the pairs gathered so far (the callee for the message, on the heap h).

python.Run.namedAdded

def Run.namedAdded (s : Run) (callee : Place) (named : Place) (more : List (Value * Value)) : Evaluation

The keyword arguments more added to the dict in the place named (an evaluation of the run s, its exception when one is wrong; the callee in the place callee for the message).

python.Exec.namedItem

def Exec.namedItem (node : String) (callee : Place) (named : Place) (key : String) (value : Place) : Code

name=value among a call’s arguments at node, the keyword key with the value in the place value, added to the dict in the place named (the callee in the place callee for the message).

python.Exec.spreadNamed

def Exec.spreadNamed (node : String) (callee : Place) (mapping : Place) (named : Place) : Code

**mapping among a call’s arguments at node: the pairs of the dict in the place mapping added to the dict in the place named; a user’s mapping is not taken yet; TypeError (naming the callee in the place callee) for anything else.

python.Exec.callGathered

def Exec.callGathered (node : String) (functions : List Function) (bodies : Nat -> Code) (callee : Place) (items : Place) (named : Place) (result : Place) : Code

The call at node, with the program’s functions and their bodies, of the callee in the place callee with the arguments gathered at run time: the items of the list in the place items positional, the pairs of the dict in the place named as keywords; its result into the place result.

python.Exec.keysOf

def Exec.keysOf (node : String) (functions : List Function) (bodies : Nat -> Code) (items : Place) (key : Place) (keys : Place) (iterator : Place) (item : Place) (ended : Place) (trying : Place) (result : Place) : Code

The keys of the items of the list in the place items, at node with the program’s functions and their bodies: the key function in the place key (a user’s or a built-in) called on each in turn, as CPython does before it compares, the results in a new list in the place keys (each call’s result through the place result); the loop’s places are iterator, item (each item), the end flag ended and trying (the flag place of the try around a user’s __next__).

python.Run.listed

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

The items of the list in the place p in the run s, in order.

python.Exec.byKeys

def Exec.byKeys (node : String) (name : String) (items : Place) (keys : Place) (reversed : Option Place) (fallback : Option Place) (result : Place) : Code

sorted, min or max (by name) of the items of the list in the place items once their keys are in the list in the place keys (Builtins.byKeys), into the place result at node; the places reversed and fallback, when given, hold reverse= and default=.