objects

python.Exceptions.names

def Exceptions.names : List String

The built-in exception classes the subset has.

python.Exceptions.isName

def Exceptions.isName (type : String) : Bool

Whether type names a built-in exception class.

python.Exceptions.chainWithin

def Exceptions.chainWithin (fuel : Nat) (type : String) : List String

The built-in exception class type and the ones above it, nearest first, within fuel steps.

python.Exceptions.chain

def Exceptions.chain (type : String) : List String

The built-in class type and the exception classes above it (only itself for a class that is not an exception).

python.Exceptions.chainOf

def Exceptions.chainOf (type : Codes) : List String

The built-in class type (as code points) and the exception classes above it.

python.Attributes.set

def Attributes.set (attributes : List (Codes * Value)) (name : Codes) (v : Value) : List (Codes * Value)

attributes with name set to v: replaced where it is, or added at the end.

python.Attributes.remove

def Attributes.remove (attributes : List (Codes * Value)) (name : Codes) : Option (List (Codes * Value))

attributes without name; none when no attribute has it.

python.Class.same

def Class.same (a : Value) (b : Value) : Bool

Whether a and b are the same class: the same object on the heap, or the same built-in class.

python.Class.among

def Class.among (c : Value) (cs : List Value) : Bool

Whether the class c is among the classes cs.

python.Class.isUser

def Class.isUser (h : Heap) (c : Value) : Bool

Whether c is a user’s class on the heap h.

python.Class.is

def Class.is (h : Heap) (c : Value) : Bool

Whether c is a class: a built-in one or a user’s on the heap h.

python.Class.exceptionBase

def Class.exceptionBase (h : Heap) (c : Value) : Codes

The built-in exception class the class c derives from (a user’s class read from the heap h): empty for a class that is not an exception.

python.Class.isException

def Class.isException (h : Heap) (c : Value) : Bool

Whether the class c is an exception class (a user’s class read from the heap h).

python.Class.firstExceptionBase

def Class.firstExceptionBase (h : Heap) (bases : List Value) : Codes

The built-in exception class the first exception class among bases derives from, with the heap h.

python.Class.tail

def Class.tail (xs : List Value) : List Value

xs without its first item.

python.Class.dropHead

def Class.dropHead (c : Value) (xs : List Value) : List Value

xs without its first item when that item is the class c.

python.Class.pick

def Class.pick (sequences : List (List Value)) (candidates : List (List Value)) : Option Value

C3: the first head among candidates that is in no tail of sequences.

python.Class.mergeWithin

def Class.mergeWithin (fuel : Nat) (sequences : List (List Value)) : Option (List Value)

C3: merging sequences into one order, within fuel steps; none when they cannot be ordered.

python.Class.total

def Class.total (sequences : List (List Value)) : Nat

How many classes sequences hold.

python.Class.listNames

def Class.listNames (names : List String) : String

names joined with commas.

python.Class.make

def Class.make (h : Heap) (name : Codes) (bases : List Value) (attributes : List (Codes * Value)) (exception : Codes) : Changed

class name(bases): a new class on the heap h with its attributes in order, and the built-in exception class it derives from (exception; empty: inherited from the bases); TypeError when the bases cannot be ordered.

python.Descriptor

data Descriptor

What a class attribute is when read: a static method, a class method, a property (its getter and setter, None when it has none), or a plain attribute.

python.Descriptor.ofWrapper

def Descriptor.ofWrapper (kind : Codes) (first : Value) (second : Value) : Descriptor

What a wrapper of kind is, wrapping first and second (a property’s getter and setter; the others use only first).

python.Descriptor.of

def Descriptor.of (h : Heap) (v : Value) : Descriptor

What the class attribute v is, its object read from the heap h.

python.Function.isUser

def Function.isUser (f : Value) : Bool

Whether f is a user’s function (a built-in one’s name starts with “builtin “).

python.Function.bindTo

def Function.bindTo (x : Value) (f : Value) : Value

f bound to the instance x as a method when it is a user’s function; anything else as it is.

python.Function.name

def Function.name (f : Value) : Codes

The name of the function value f.

python.Function.captured

def Function.captured (f : Value) : List Value

The cells the function value f captured.

python.Function.shortName

def Function.shortName (f : Value) : Codes

The __name__ of the function f: a built-in’s name without “builtin “, a nested function’s last part (outer.inner is inner), without the suffix that tells functions of the same name apart (from code point 1 on).

python.Function.qualifiedName

def Function.qualifiedName (f : Value) : Codes

The __qualname__ of the function f: its name in the program’s table before the mark (a built-in’s without its module’s, Printing.builtinName).

python.Function.ownName

def Function.ownName (f : Value) : Codes

The __name__ of the function f: a user’s own name, a built-in’s without its module’s.

python.Descriptor.fromInstance

def Descriptor.fromInstance (h : Heap) (x : Value) (c : Value) (f : Value) : Value

The class attribute f read from the instance x of the class c (wrappers read from the heap h): a user’s function bound to the instance, a static method’s function, a class method bound to the class; anything else as it is.

python.Descriptor.fromClass

def Descriptor.fromClass (h : Heap) (c : Value) (f : Value) : Value

The class attribute f read from the class c (wrappers read from the heap h): a static method’s function, a class method bound to the class; anything else (a function too) as it is.

python.Class.property

def Class.property (h : Heap) (c : Value) (name : String) : Option (Value * Value)

The property name along the order of the class c on the heap h: its getter and setter.

python.Access

data Access

What accessing an attribute gives: the heap and a value, a user’s function to call with arguments (a property’s getter or setter), or an exception.

python.Objects.always

def Objects.always : List String

The attributes every object has in CPython (dir(object), and a user’s instance’s __dict__, __module__ and __weakref__): one the model does not give is something it cannot do, not an AttributeError.

python.Objects.alwaysOnClasses

def Objects.alwaysOnClasses : List String

The attributes every class has in CPython (dir(type) and dir(object), without __abstractmethods__, which an ordinary class does not have).

python.Objects.missing

def Objects.missing (h : Heap) (v : Value) (name : String) : Access

AttributeError: the type of v (read from the heap h) has no attribute name.

python.Objects.classMissing

def Objects.classMissing (className : Codes) (name : String) : Access

AttributeError: the class named className has no attribute name.

python.Objects.throughProperty

def Objects.throughProperty (h : Heap) (x : Value) (name : String) (which : String) (f : Value) (arguments : List Value) : Access

The which (“getter” or “setter”) f of the property name of the instance x, called with arguments; AttributeError naming the type of x (read from the heap h) when it has none (None).

python.Objects.ofInstance

def Objects.ofInstance (h : Heap) (x : Value) (c : Value) (own : List (Codes * Value)) (name : String) : Access

The attribute name of the instance x of the class c whose own attributes are own, on the heap h: __class__, a property, its own attribute, then along its class’s order.

python.Class.mro

def Class.mro (c : Value) (order : List Value) (base : Codes) : Value

The __mro__ of the class c: itself, its order, the built-in exception classes above base (the one it derives from) that are not in it, and object.

python.Class.builtinMro

def Class.builtinMro (name : Codes) : Value

The __mro__ of the built-in class name: bool is under int, an exception class under its own, all under object.

python.Objects.ofClass

def Objects.ofClass (h : Heap) (c : Value) (className : Codes) (order : List Value) (base : Codes) (name : String) : Access

The attribute name of the user’s class c (named className, with its order and exception base) on the heap h: __name__, __mro__, then along its order; a class that defines __eq__ and no __hash__ has __hash__ None (CPython sets it so).

python.Objects.ofProperty

def Objects.ofProperty (h : Heap) (v : Value) (getter : Value) (setter : Value) (name : String) : Access

The attribute name of the property v on the heap h: fget and fset (its getter and setter, None when it has none), and its methods getter, setter and deleter bound to it (python.builtins).

python.Objects.ofObject

def Objects.ofObject (h : Heap) (v : Value) (o : Object) (name : String) : Access

The attribute name of v, whose object on the heap h is o.

python.Objects.ofException

def Objects.ofException (h : Heap) (v : Value) (type : Codes) (message : Codes) (name : String) : Access

The attribute name of the built-in exception v (of the class type, with message) on the heap h: args, and a StopIteration’s value.

python.Objects.get

def Objects.get (h : Heap) (v : Value) (name : String) : Access

v.name: the attribute name of v on the heap h.

python.Objects.noDict

def Objects.noDict (h : Heap) (v : Value) (name : String) : Access

AttributeError for setting the attribute name on v, a value that has no attributes of its own (its type read from the heap h).

python.Objects.setObject

def Objects.setObject (h : Heap) (v : Value) (a : Nat) (o : Object) (name : String) (x : Value) : Access

v.name = x where v is the object o at the address a on the heap h: its attribute name set to x.

python.Objects.set

def Objects.set (h : Heap) (v : Value) (name : String) (x : Value) : Access

v.name = x on the heap h: an instance’s or a user’s class’s own attribute name, or a property’s setter called.

python.Objects.deleteObject

def Objects.deleteObject (h : Heap) (v : Value) (a : Nat) (o : Object) (name : String) : Access

del v.name where v is the object o at the address a on the heap h: its own attribute name removed.

python.Objects.delete

def Objects.delete (h : Heap) (v : Value) (name : String) : Access

del v.name on the heap h: an instance’s or a user’s class’s own attribute name.

python.Value.classOf

def Value.classOf (h : Heap) (v : Value) : Value

The class of v: an instance’s class (read from the heap h), or the built-in class of its type.

python.Objects.hasUserAttribute

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

Whether v (an instance or a user’s class on the heap h) or its class has an attribute name (a user’s attribute, not a built-in method).

python.Class.after

def Class.after (c : Value) (order : List Value) : List Value

The classes after the class c in order.

python.Objects.super

def Objects.super (h : Heap) (c : Value) (x : Value) (name : String) : Outcome

super().name in a method of the class c whose first argument is x: the attribute name looked up along the order of the class of x after c, on the heap h. An exception class’s __init__ and __str__ are the built-in exception’s.

python.Objects.instantiate

def Objects.instantiate (h : Heap) (c : Value) (arguments : List Value) : Changed

A new instance of the class c on the heap h; an exception class’s instance keeps its arguments as args.

python.Objects.withoutInit

def Objects.withoutInit (h : Heap) (c : Value) (positional : List Value) (keywords : List (Codes * Value)) : Option Raised

Calling the user’s class c (on the heap h) that has no __init__: TypeError for positional or keywords arguments (an exception class takes positional ones, not keyword ones).

python.Objects.initReturned

def Objects.initReturned (h : Heap) (v : Value) : Option Raised

What __init__ returned, v: TypeError (naming its type, read from the heap h) unless None.

python.Bound.arguments

def Bound.arguments (f : Value) (arguments : List Value) : List Value

The arguments to call f with: a bound method’s instance before the others.

python.Bound.function

def Bound.function (f : Value) : Value

The function to call for f: a bound method’s function.

python.Cell.make

def Cell.make (h : Heap) (content : Option Value) : Changed

A new cell on the heap h holding content (none: without a value).

python.Cell.content

def Cell.content (h : Heap) (cell : Value) : Option Value

What cell holds on the heap h.

python.Cell.read

def Cell.read (h : Heap) (cell : Value) (name : String) (own : Bool) : Outcome

Reading the captured variable name from cell on the heap h: UnboundLocalError for the function’s own variable without a value, NameError for an enclosing function’s.

python.Cell.write

def Cell.write (h : Heap) (cell : Value) (v : Value) : Heap

The heap h with cell given the value v.

python.Exceptions.of

def Exceptions.of (h : Heap) (v : Value) : List String

The exception classes v is an instance of, nearest first (classes read from the heap h): a built-in exception’s by the hierarchy, a user’s exception’s along its class’s order and then the built-in ones; empty for a value that is not an exception.

python.Class.within

def Class.within (h : Heap) (c : Value) (b : Value) : Bool

Whether the class c is the class b or a subclass of it, with user’s classes on the heap h.

python.Objects.isSubclass

def Objects.isSubclass (h : Heap) (c : Value) (b : Value) : Outcome

issubclass(c, b) on the heap h: b a class or a tuple of classes.

python.Objects.instanceOf

def Objects.instanceOf (h : Heap) (x : Value) (c : Value) : Bool

Whether x is an instance of the class c, on the heap h.

python.Objects.isInstance

def Objects.isInstance (h : Heap) (x : Value) (c : Value) : Outcome

isinstance(x, c) on the heap h: c a class or a tuple of classes.

python.Exceptions.arguments

def Exceptions.arguments (h : Heap) (v : Value) : List Value

The args of the exception v on the heap h.

python.Exceptions.text

def Exceptions.text (h : Heap) (v : Value) : Codes

str(e) of the exception v (on the heap h) without its own __str__: empty for no arguments, the str of one (a KeyError’s repr), the tuple’s repr for more.

python.Showing

record Showing

A user’s __str__ or __repr__ to call before printing a value: the instance, the bound method, and whether it is __str__ (whose text str uses) rather than __repr__ (the instance is the target).

python.Showing.ofInstance

def Showing.ofInstance (h : Heap) (top : Bool) (v : Value) (cls : Value) (found : List Showing) : List Showing

The method the instance v of the class cls is shown with, added after the ones found: __str__ at the top (when its class defines one), else __repr__; classes read from the heap h.

python.Showing.flatten

def Showing.flatten (pairs : List (Value * Value)) : List Value

The keys and values of pairs, in order.

python.Showing.ofObject

def Showing.ofObject (fuel : Nat) (h : Heap) (top : Bool) (v : Value) (o : Object) (found : List Showing) : List Showing

The methods to call for v, whose object on the heap h is o, after the ones found, within fuel levels; top when v is printed itself, not inside a container.

python.Showing.collectWithin

def Showing.collectWithin (fuel : Nat) (h : Heap) (top : Bool) (v : Value) (found : List Showing) : List Showing

The methods to call for v, in the order printing reaches them, after the ones found, within fuel levels; top when v is printed itself, not inside a container; objects read from the heap h.

python.Showing.each

def Showing.each (fuel : Nat) (h : Heap) (xs : List Value) (found : List Showing) : List Showing

The methods to call for the items xs of a container (each shown with __repr__), after the ones found, within fuel levels, on the heap h.

python.Showing.targets

def Showing.targets (h : Heap) (top : Bool) (values : List Value) : List Showing

The methods to call before printing values on the heap h, in order: an instance at the top with __str__ when top holds (as print and str do), every one inside with __repr__.

python.Showing.store

def Showing.store (h : Heap) (a : Nat) (o : Object) (isStr : Bool) (text : Codes) : Heap

The heap h with the instance o at the address a keeping the text its method returned for printing (as its str when isStr, else as its repr).

python.Showing.remember

def Showing.remember (h : Heap) (s : Showing) (result : Value) : Changed

The result the method of s returned, kept in its instance on the heap h; TypeError when it is not a str.