values

python.Codes

def Codes : Type

Text as Python sees it: its code points.

python.Codes.of

def Codes.of (s : String) : Codes

A string’s code points.

python.Codes.toString

def Codes.toString (cs : Codes) : String

The string of the code points cs.

python.Codes.startsWith

def Codes.startsWith (head : Codes) (cs : Codes) : Bool

Whether the code points cs start with the code points head.

python.Value

data Value

A Python value. functionValue is a function by name with its captured cells (a built-in’s name starts with “builtin “); boundValue is a method bound to its object; notImplementedValue is NotImplemented (an operator method declining).

python.Slot

data Slot

A slot of a set’s hash table: never used, used once and emptied (a dummy), or holding an item with its hash.

python.SetTable

data SetTable

A set’s items: CPython’s hash table (its slots, how many hold items, how many hold items or dummies, and the implementation’s choices its order depends on: str.hash for a str’s hash, taken as under PYTHONHASHSEED=0, and object.address for an object’s, from the model’s addresses), or, when an item’s hash is not one the model gives, the items in the order they were added.

python.Iterating

data Iterating

What an iterator walks: a list (forward or backward, as the list is now), the items of a tuple, str or reversed sequence (its type name), a range, a dict’s keys, values or items or a set (with the size they had and, for a dict, its keys then, to notice changes), an enumerate (its iterator and the next count), or a zip (its iterators and whether it is strict).

python.Object

data Object

An object on the heap. A dict keeps its pairs in insertion order and a set its items in a SetTable; a view is a dict’s keys, values or items as the dict is now (its kind is its type name; it holds the dict’s address); an iterator walks what Iterating says, at a position; an instance has its class and attributes in order, and the text __repr__ and __str__ gave before printing; a class has its name, its method resolution order without itself, its attributes in order and the built-in exception class it derives from (empty when none); a wrapper is a staticmethod, classmethod or property (a property’s getter and setter, None when absent); a generator has its function, its next state, its locals while paused and whether it is done.

python.Iterating.typeName

def Iterating.typeName (w : Iterating) : String

The CPython type name of an iterator walking w.

python.Slot.item

def Slot.item (slot : Slot) : List Value

The item a slot holds, if any.

python.SetTable.items

def SetTable.items (t : SetTable) : List Value

The items of the set table t in the order iterating gives them: the slots’ order, or the order they were added.

python.Names.joined

def Names.joined (a : List String) (b : List String) : List String

The names a followed by those of b not already in a: each once, in the order first seen.

python.SetTable.chosen

def SetTable.chosen (t : SetTable) : List String

The implementation’s choices the order of the set table t depends on.

python.SetTable.choosing

def SetTable.choosing (t : SetTable) (more : List String) : SetTable

The set table t, its order now also depending on the choices more (built from a table that did).

python.Heap

def Heap : Type

The heap: objects by address.

python.Heap.empty

def Heap.empty : Heap

An empty heap.

python.Heap.object

def Heap.object (h : Heap) (a : Nat) : Option Object

The object at address a on the heap h, if there is one.

python.Value.ofString

def Value.ofString (s : String) : Value

The str value of the string s.

python.Value.ofDecimal

def Value.ofDecimal (m : Nat) (e : Int) : Value

A float literal m * 10^e, correctly rounded to binary64 (0.1 is m = 1, e = -1).

python.Value.negativeZero

def Value.negativeZero : Value

Negative zero (-0.0).

python.Raised

record Raised

A raised exception: the classes it is an instance of (its own first, then its bases), its message, for an instance of a user’s class its object on the heap, the node of the statement that raised it (empty until the statement fills it in), and its details as a verdict reports them (undeclared for a name not defined: its name; none for an exception not structured yet).

python.Raised.named

def Raised.named (type : String) (message : String) : Raised

A built-in exception of a type with a message, raised.

python.Raised.notDefined

def Raised.notDefined (name : String) : Raised

NameError for a name nothing defines (CPython’s message), with the name as its detail.

python.Raised.unsupportedType

def Raised.unsupportedType : String

The class name of what the model cannot do (a space first, so no program’s class has it): a run stops with it and the verdict is unknown, not Python’s behavior.

python.Raised.unsupported

def Raised.unsupported (what : String) : Raised

What the model cannot do, described by what, raised (for example calling a user’s __eq__ while comparing containers).

python.Raised.type

def Raised.type (e : Raised) : String

The own class of the raised exception e.

python.Outcome

data Outcome

What evaluating gives: a value, or an exception raised.

python.Outcome.raise

def Outcome.raise (type : String) (message : String) : Outcome

Raising a built-in exception of a type with a message.

python.Exceptions.parent

def Exceptions.parent (type : String) : Option String

The base of the built-in exception class type (CPython’s Objects/exceptions.c); none for BaseException.

python.Exceptions.derivesWithin

def Exceptions.derivesWithin (fuel : Nat) (type : String) (k : String) : Bool

Whether the built-in exception class type is k or derives from it, within fuel steps up the hierarchy.

python.Exceptions.isSubclass

def Exceptions.isSubclass (type : String) (k : String) : Bool

Whether except k catches a built-in exception of a type: the type is k or derives from it (the hierarchy is at most five deep).

python.Range.length

def Range.length (start : Int) (stop : Int) (step : Int) : Nat

How many values the range from start up to stop by step gives: none when it is empty (or step is zero).

python.Value.className

def Value.className (h : Heap) (c : Value) : Codes

The name of the class value c (a built-in class’s is its name; a user’s is on the heap h).

python.Value.generatorType

def Value.generatorType (function : Value) : String

A generator’s type name: a built-in generator’s is its function’s name (builtin map is a map).

python.Object.typeName

def Object.typeName (h : Heap) (o : Object) : String

The type name of the object o on the heap h.

python.Value.builtinClasses

def Value.builtinClasses : List String

The built-ins the model has as functions that are classes in CPython (type(map) is type).

python.Value.randomMethods

def Value.randomMethods : List String

The functions of random that are methods of its hidden Random instance written in Python (random.random and random.getrandbits are C methods: builtin_function_or_method).

python.Value.functionType

def Value.functionType (name : Codes) : String

type(f).__name__ for the function named name (a built-in’s name starts with “builtin “): a user’s is function; a built-in’s is type when CPython has it as a class, method for random’s Python methods, else builtin_function_or_method.

python.Value.boundType

def Value.boundType (function : Value) : String

type(m).__name__ for the method function bound to an object: a built-in’s ([].append, a property’s setter) is builtin_function_or_method, a user’s is method.

python.Value.typeName

def Value.typeName (h : Heap) (v : Value) : String

type(x).__name__ for the value v, looking up objects on the heap h.

python.Texts.distinct

def Texts.distinct (ts : List String) : List String

The texts ts, each once, in the order first seen.

python.Texts.joinedBy

def Texts.joinedBy (sep : String) (ts : List String) : String

The texts ts with sep between them.

python.Texts.union

def Texts.union (ts : List String) : String

The union of the type texts ts as Python’s typing writes it: each once, in the order first seen, joined by |.

python.Texts.contained

def Texts.contained (kind : String) (ts : List String) : String

A container’s type text: its kind with the union of its items’ types ts, or ? when it has none.

python.Pair.key

def Pair.key (p : Value * Value) : Value

The key of a dict’s pair p.

python.Pair.value

def Pair.value (p : Value * Value) : Value

The value of a dict’s pair p.

python.Value.typeText

def Value.typeText (fuel : Nat) (path : List Nat) (h : Heap) (v : Value) : String

The type of the value v as Python’s typing writes it, looking up objects on the heap h: None; a list, set or dict with the union of its items’ (keys’, values’) types, ? for none (list[?], dict[?, ?]); a tuple with each item’s type (tuple[()] when empty); anything else its type(x).__name__. A list, set or dict inside itself (one of the addresses on the path) is ..., and so is anything deeper than fuel levels.

python.Value.typeDepth

def Value.typeDepth : Nat

How deep a type text looks into containers (Value.typeText).

python.Heap.dictAt

def Heap.dictAt (h : Heap) (a : Nat) : List (Value * Value)

The pairs of the dict at address a on the heap h (none for anything else).

python.Heap.viewItems

def Heap.viewItems (h : Heap) (kind : Codes) (a : Nat) : List Value

What a view of the dict at address a on the heap h holds now: its keys, values or items (as 2-tuples), by the view’s type name kind.

python.Object.truthy

def Object.truthy (h : Heap) (o : Object) : Bool

bool(x) of the object o on the heap h: an empty list, dict, set or view is false; anything else is true.

python.Value.truthy

def Value.truthy (h : Heap) (v : Value) : Bool

bool(x) of the value v, looking up objects on the heap h: None, False, zero, an empty str, tuple, range or container is false; anything else is true.