methods

python.Methods.fails

def Methods.fails (h : Heap) (e : Raised) : Changed

The exception e raised, the heap h unchanged.

python.Methods.gives

def Methods.gives (h : Heap) (v : Value) : Changed

The value v produced, the heap h unchanged.

python.Methods.checked

def Methods.checked (h : Heap) (problem : Option Raised) (work : Unit -> Changed) : Changed

The check’s problem raised, else the method’s work when it passed, on the heap h.

python.Methods.notInteger

def Methods.notInteger (h : Heap) (v : Value) : Raised

TypeError: the value v on the heap h is not an index.

python.Methods.sizeLimit

def Methods.sizeLimit : Nat

The largest Py_ssize_t, 2^63 - 1.

python.Methods.fitsSize

def Methods.fitsSize (n : Int) : Bool

Whether the int n fits a Py_ssize_t.

python.Methods.size

def Methods.size (h : Heap) (v : Value) : Either Raised Int

The index argument v on the heap h as a Py_ssize_t: TypeError for a value that is not an index, OverflowError past the range.

python.Methods.sliceBound

def Methods.sliceBound (h : Heap) (noneAllowed : Bool) (v : Value) : Either Raised (Option Int)

The slice bound v on the heap h (_PyEval_SliceIndex): an index clamped to Py_ssize_t, or None when noneAllowed (none).

python.Methods.adjust

def Methods.adjust (size : Nat) (isEnd : Bool) (bound : Int) : Int

The bound adjusted to the length size (ADJUST_INDICES): from the end when negative, then clamped to 0 and the length (the length only when isEnd).

python.Methods.range

def Methods.range (h : Heap) (size : Nat) (start : Option Value) (finish : Option Value) : Either Raised (Int * Int)

The start and end (finish) arguments of find and the others on the heap h (each optional, None allowed), adjusted to the length size.

python.Methods.slot

def Methods.slot (values : List (Option Value)) (k : Nat) : Option Value

The value of the parsed parameter at the position k of the values, if it was given.

python.Methods.codes

def Methods.codes (self : Value) : Codes

The code points of the str receiver self.

python.Methods.text

def Methods.text (h : Heap) (cs : Codes) : Changed

The text cs produced, the heap h unchanged.

python.Methods.bool

def Methods.bool (h : Heap) (b : Bool) : Changed

The bool b produced, the heap h unchanged.

python.Methods.unclassified

def Methods.unclassified (method : String) : Raised

What the model cannot tell: a code point it does not classify, for a method that needs its class.

python.Methods.classifiedOnly

def Methods.classifiedOnly (h : Heap) (method : String) (self : Value) (positional : List Value) (keywords : List (Codes * Value)) (work : Codes -> Changed) : Changed

The str method named method of no arguments that needs every code point classified: its work on the code points of self, on the heap h, once the call’s positional and keywords arguments are checked to be none.

python.Methods.isAlpha

def Methods.isAlpha (c : Nat) : Bool

Whether the code point c is a letter (str.isalpha).

python.Methods.isDigit

def Methods.isDigit (c : Nat) : Bool

Whether the code point c is a decimal digit (str.isdigit on the classified code points).

python.Methods.allOf

def Methods.allOf (p : Nat -> Bool) (cs : Codes) : Bool

Whether the text cs is not empty and every code point is of the class p.

python.Methods.caseChange

def Methods.caseChange (method : String) (cs : Codes) : Codes

s.upper(), s.lower(), s.title(), s.capitalize() (the method) on the code points cs of s.

python.Methods.classTest

def Methods.classTest (method : String) (cs : Codes) : Bool

s.isdigit(), s.isalpha(), s.isupper(), s.islower() (the method) on the code points cs of s.

python.Methods.strip

def Methods.strip (h : Heap) (method : String) (self : Value) (positional : List Value) (keywords : List (Codes * Value)) : Changed

s.strip(chars), lstrip, rstrip (the method) on the str self with the call’s positional and keywords arguments, on the heap h: whitespace, or the code points of chars (None: whitespace).

python.Methods.wordsWithin

def Methods.wordsWithin (fuel : Nat) (k : Nat) (cs : Codes) : List Codes

The pieces of cs between whitespace, at most k splits, within fuel steps (CPython’s split_whitespace): the rest after the last split, without its leading whitespace, is the last piece.

python.Methods.splitWithin

def Methods.splitWithin (fuel : Nat) (separator : Codes) (k : Nat) (piece : Codes) (cs : Codes) : List Codes

The pieces of cs between occurrences of the separator, at most k splits, within fuel steps (piece: the current one).

python.Methods.splitCount

def Methods.splitCount (cs : Codes) (count : Int) : Nat

The most splits of the text cs the count asks for: every one for a negative count.

python.Methods.split

def Methods.split (h : Heap) (self : Value) (positional : List Value) (keywords : List (Codes * Value)) : Changed

s.split(sep=None, maxsplit=-1) on the str self with the call’s positional and keywords arguments, on the heap h.

python.Methods.firstNotText

def Methods.firstNotText (k : Nat) (xs : List Value) : Option (Nat * Value)

The first item of the list xs that is not a str, and where it is (counting from k).

python.Methods.joinWith

def Methods.joinWith (separator : Codes) (xs : List Value) : Codes

The texts xs joined with the separator between them.

python.Methods.join

def Methods.join (h : Heap) (self : Value) (positional : List Value) (keywords : List (Codes * Value)) : Changed

s.join(iterable) on the str self with the call’s positional and keywords arguments, on the heap h: every item a str.

python.Methods.mustBeText

def Methods.mustBeText (h : Heap) (method : String) (k : Nat) (v : Value) : Raised

TypeError: the argument v (on the heap h) at the position k of the str method must be a str.

python.Methods.replace

def Methods.replace (h : Heap) (self : Value) (positional : List Value) (keywords : List (Codes * Value)) : Changed

s.replace(old, new, /, count=-1) on the str self with the call’s positional and keywords arguments, on the heap h.

python.Methods.findFrom

def Methods.findFrom (fuel : Nat) (k : Nat) (finish : Nat) (part : Codes) (cs : Codes) : Option Nat

Where the text part first occurs in cs (at the position k) before finish, within fuel steps.

python.Methods.search

def Methods.search (method : String) (cs : Codes) (part : Codes) (low : Nat) (high : Nat) : Int

s.find, s.index, s.count (the method) of a part of cs within [low, high), which is at least as long as the part: where it first is (-1: not there), or how many times it is there without overlapping (an empty part: between every two code points and at both ends).

python.Methods.find

def Methods.find (h : Heap) (method : String) (self : Value) (positional : List Value) (keywords : List (Codes * Value)) : Changed

s.find(sub[, start[, end]]), s.index, s.count (the method) on the str self with the call’s positional and keywords arguments, on the heap h: ValueError from index when it is not there.

python.Methods.tailMatch

def Methods.tailMatch (cs : Codes) (atEnd : Bool) (part : Codes) (start : Int) (finish : Int) : Bool

Whether the text cs has the part at the start (or the end, atEnd) of [start, finish) (CPython’s tailmatch).

python.Methods.prefixes

def Methods.prefixes (h : Heap) (method : String) (v : Value) : Either Raised (List Codes)

The texts the argument v (on the heap h) of startswith or endswith (the method) gives: a str, or a tuple of them.

python.Methods.startsWith

def Methods.startsWith (h : Heap) (method : String) (self : Value) (positional : List Value) (keywords : List (Codes * Value)) : Changed

s.startswith(prefix[, start[, end]]), s.endswith (the method) on the str self with the call’s positional and keywords arguments, on the heap h.

python.Methods.fill

def Methods.fill (h : Heap) (v : Option Value) : Either Raised Nat

The fill character v (on the heap h) of ljust and the others (a space when absent).

python.Methods.padded

def Methods.padded (method : String) (width : Nat) (fill : Nat) (cs : Codes) : Codes

The text cs padded with fill to the width, as the method does: on the right (ljust), the left (rjust), or both (center: the extra one on the left when the margin and the width are both odd, as CPython’s pad does).

python.Methods.memoryLimit

def Methods.memoryLimit : Nat

The width past which a padded text would not fit the model’s memory (2^32 code points): MemoryError.

python.Methods.justify

def Methods.justify (h : Heap) (method : String) (self : Value) (positional : List Value) (keywords : List (Codes * Value)) : Changed

s.ljust(width[, fillchar]), rjust, center (the method) on the str self with the call’s positional and keywords arguments, on the heap h.

python.Methods.zfill

def Methods.zfill (h : Heap) (self : Value) (positional : List Value) (keywords : List (Codes * Value)) : Changed

s.zfill(width) on the str self with the call’s positional and keywords arguments, on the heap h: zeros on the left, after a leading sign.

python.Method

def Method : Type

A method of a receiver: its name, and what calling it with arguments does.

python.Methods.named

def Methods.named (method : String) (f : Heap -> String -> Value -> List Value -> List (Codes * Value) -> Changed) : Method

The method named method whose handler f takes its own name first.

python.Methods.caseMethod

def Methods.caseMethod (method : String) : Method

s.upper() and the other case changes, by the name method.

python.Methods.testMethod

def Methods.testMethod (method : String) : Method

s.isdigit() and the other class tests, by the name method.

python.Methods.isSpace

def Methods.isSpace (h : Heap) (self : Value) (positional : List Value) (keywords : List (Codes * Value)) : Changed

s.isspace() on the str self with the call’s positional and keywords arguments, on the heap h (whitespace is known for every code point).

python.Methods.ofText

def Methods.ofText : List Method

The str methods the model provides.

python.Piece

data Piece

What reading the next piece of a format string gives (CPython’s MarkupIterator_next): the end, literal text, literal text followed by a replacement field (its name, conversion, spec, and whether the spec holds fields of its own), or an exception.

python.Format.fails

def Format.fails (message : String) : Raised

A format string’s ValueError with the message.

python.Format.spec

def Format.spec (k : Nat) (expands : Bool) (spec : Codes) (cs : Codes) : Either Raised ((Codes * Bool) * Codes)

A field’s spec so far continued in cs up to its closing brace, nested braces counted (k: braces still open; expands: whether a nested field was seen).

python.Format.name

def Format.name (fuel : Nat) (name : Codes) (cs : Codes) : Either Raised ((Codes * Nat) * Codes)

A field’s name so far continued in cs up to :, ! or } (a [ skips to its ]), within fuel steps: the name, the code point that ended it, the rest.

python.Format.afterConversion

def Format.afterConversion (text : Codes) (name : Codes) (conversion : Nat) (cs : Codes) : Piece

The rest cs after the conversion specifier of the field name (after the literal text): } ends the field, : starts its spec.

python.Format.field

def Format.field (text : Codes) (cs : Codes) : Piece

A replacement field in cs after its {, after the literal text (CPython’s parse_field).

python.Format.next

def Format.next (cs : Codes) : Piece

The next piece of the format string cs.

python.Numbering

data Numbering

How replacement fields are numbered so far: not yet, automatically (the next number), or by hand.

python.Format.integer

def Format.integer (cs : Codes) : Either Raised (Option Nat)

The field name’s part cs as an index (CPython’s get_integer): none unless every code point is a decimal digit; ValueError past Py_ssize_t.

python.Formatting

record Formatting

The arguments a format string reads.

python.Found

data Found

What a field’s name gives: its value and the numbering after it, or an exception.

python.Format.argument

def Format.argument (c : Formatting) (numbering : Numbering) (first : Codes) (index : Option Nat) : Found

The argument among c that a field’s first part names (its index, if it is one), with the fields’ numbering so far: the next one for an empty part, by position for an index, else by keyword (CPython’s field_name_split and get_field_object).

python.Format.attribute

def Format.attribute (h : Heap) (v : Value) (name : Codes) : Outcome

The attribute name of the value v on the heap h, in a field name (a property would run a user’s code: unsupported here).

python.Format.walk

def Format.walk (fuel : Nat) (h : Heap) (v : Value) (cs : Codes) : Outcome

The rest cs of a field name after its first part, from the value v on the heap h: .name and [key] in turn, within fuel steps (CPython’s FieldNameIterator).

python.Format.object

def Format.object (c : Formatting) (numbering : Numbering) (name : Codes) : Found

The value the field’s name gives among the arguments c, with the fields’ numbering so far.

python.Format.hex

def Format.hex (width : Nat) (n : Nat) : Codes

Hexadecimal digits of n, in small letters, at least width of them.

python.Format.ascii

def Format.ascii (cs : Codes) : Codes

ascii() of the repr cs: code points past ASCII as \xNN, \uNNNN or \UNNNNNNNN.

python.Format.convert

def Format.convert (h : Heap) (conversion : Option Nat) (v : Value) : Outcome

A field’s value v on the heap h converted by its conversion: !r repr, !s str, !a ascii.

python.Built

data Built

What building a format string gives: the text and the numbering after it, or an exception.

python.Format.build

def Format.build (fuel : Nat) (c : Formatting) (depth : Nat) (numbering : Numbering) (cs : Codes) (out : Codes) : Built

The format string cs built after out (CPython’s build_string) from the arguments c, at a recursion depth with the fields’ numbering so far, within fuel steps: each field’s value converted, its spec built first when it holds fields, then formatted.

python.Format.render

def Format.render (fuel : Nat) (c : Formatting) (depth : Nat) (numbering : Numbering) (name : Codes) (conversion : Option Nat) (spec : Codes) (expands : Bool) : Built

One replacement field rendered (CPython’s output_markup): the field name among the arguments c, with the fields’ numbering so far, its conversion, and its spec (built at the recursion depth within fuel steps when it expands).

python.Methods.format

def Methods.format (h : Heap) (self : Value) (positional : List Value) (keywords : List (Codes * Value)) : Changed

s.format(*args, **kwargs) on the str self with the call’s positional and keywords arguments, on the heap h.

python.Methods.without

def Methods.without (j : Nat) (xs : List Value) : List Value

The items xs without the one at the position j.

python.Methods.argument

def Methods.argument (positional : List Value) (k : Nat) : Value

The positional argument at k (None when absent: the check before has made sure it is there).

python.Methods.setAll

def Methods.setAll (pairs : List (Value * Value)) (more : List (Value * Value)) : List (Value * Value)

The pairs more set in a dict’s pairs in turn.

python.Format.inName

def Format.inName (c : Nat) : Bool

Whether the code point c continues a field name’s first part or attribute (not . or [).

python.Methods.address

def Methods.address (self : Value) : Nat

The address of the receiver self on the heap.

python.Methods.items

def Methods.items (h : Heap) (self : Value) : List Value

The items of the list receiver self on the heap h.

python.Methods.storeList

def Methods.storeList (h : Heap) (self : Value) (xs : List Value) (v : Value) : Changed

The list receiver self on the heap h with the new items xs, and the value v produced.

python.Methods.outcome

def Methods.outcome (h : Heap) (o : Outcome) : Changed

The outcome o with the heap h unchanged.

python.Methods.append

def Methods.append (h : Heap) (self : Value) (positional : List Value) (keywords : List (Codes * Value)) : Changed

xs.append(x) on the list self with the call’s positional and keywords arguments, on the heap h.

python.Methods.extend

def Methods.extend (h : Heap) (self : Value) (positional : List Value) (keywords : List (Codes * Value)) : Changed

xs.extend(iterable) on the list self with the call’s positional and keywords arguments, on the heap h: the items the iterable has now.

python.Methods.insertAt

def Methods.insertAt (size : Nat) (k : Int) : Nat

The position k for insert in a list of the length size: from the end when negative, clamped to the list.

python.Methods.insert

def Methods.insert (h : Heap) (self : Value) (positional : List Value) (keywords : List (Codes * Value)) : Changed

xs.insert(i, x) on the list self with the call’s positional and keywords arguments, on the heap h.

python.Methods.pop

def Methods.pop (h : Heap) (self : Value) (positional : List Value) (keywords : List (Codes * Value)) : Changed

xs.pop(i=-1) on the list self with the call’s positional and keywords arguments, on the heap h: IndexError for an empty list or an index past it.

python.Methods.remove

def Methods.remove (h : Heap) (self : Value) (positional : List Value) (keywords : List (Codes * Value)) : Changed

xs.remove(x) on the list self with the call’s positional and keywords arguments, on the heap h: the first item equal to x.

python.Methods.sequence

def Methods.sequence (h : Heap) (self : Value) : List Value

The items of the list or tuple receiver self on the heap h.

python.Methods.sequenceIndex

def Methods.sequenceIndex (h : Heap) (self : Value) (positional : List Value) (keywords : List (Codes * Value)) : Changed

xs.index(x[, start[, stop]]) of the list or tuple self with the call’s positional and keywords arguments, on the heap h: within [start, stop) adjusted to it (None not allowed).

python.Methods.sequenceCount

def Methods.sequenceCount (h : Heap) (self : Value) (positional : List Value) (keywords : List (Codes * Value)) : Changed

xs.count(x) of the list or tuple self with the call’s positional and keywords arguments, on the heap h.

python.Methods.storeSorted

def Methods.storeSorted (h : Heap) (self : Value) (r : Option Raised * List Value) : Changed

The list self on the heap h stored with its items as a sort left them, then the sort’s exception, if it raised one (r: the exception and the items; CPython’s list.sort leaves the items as far as it got).

python.Methods.sort

def Methods.sort (h : Heap) (self : Value) (positional : List Value) (keywords : List (Codes * Value)) : Changed

xs.sort(*, key=None, reverse=False) on the list self with the call’s positional and keywords arguments, on the heap h: reverse by its truth; a key is a user’s code (the caller’s).

python.Methods.listPlain

def Methods.listPlain (h : Heap) (method : String) (self : Value) (positional : List Value) (keywords : List (Codes * Value)) : Changed

A list method of no arguments, by the name method: reverse, clear, copy; on the list self with the call’s positional and keywords arguments, on the heap h.

python.Methods.ofList

def Methods.ofList : List Method

The list methods the model provides.

python.Methods.pairs

def Methods.pairs (h : Heap) (self : Value) : List (Value * Value)

The pairs of the dict receiver self on the heap h.

python.Methods.storeDict

def Methods.storeDict (h : Heap) (self : Value) (pairs : List (Value * Value)) (v : Value) : Changed

The dict receiver self on the heap h with the new pairs, and the value v produced.

python.Methods.key

def Methods.key (h : Heap) (k : Value) (work : Unit -> Changed) : Changed

The key k’s check on the heap h, then the method’s work: TypeError for one that is not hashable.

python.Methods.get

def Methods.get (h : Heap) (self : Value) (positional : List Value) (keywords : List (Codes * Value)) : Changed

d.get(key, default=None) on the dict self with the call’s positional and keywords arguments, on the heap h.

python.Methods.dictPop

def Methods.dictPop (h : Heap) (self : Value) (positional : List Value) (keywords : List (Codes * Value)) : Changed

d.pop(key[, default]) on the dict self with the call’s positional and keywords arguments, on the heap h: KeyError when it is not there and there is no default.

python.Methods.setDefault

def Methods.setDefault (h : Heap) (self : Value) (positional : List Value) (keywords : List (Codes * Value)) : Changed

d.setdefault(key, default=None) on the dict self with the call’s positional and keywords arguments, on the heap h.

python.Methods.addPairs

def Methods.addPairs (h : Heap) (k : Nat) (pairs : List (Value * Value)) (items : List Value) : List (Value * Value) * Option Raised

What adding the pairs from the items of an iterable (on the heap h) to the pairs gives, k the number of the next element for messages: the pairs so far, and the exception that stopped it if one did (the pairs before it stay, as in CPython).

python.Methods.raised

def Methods.raised (o : Outcome) : Raised

The exception the outcome o raised (a TypeError if it did not raise).

python.Methods.update

def Methods.update (h : Heap) (self : Value) (positional : List Value) (keywords : List (Codes * Value)) : Changed

d.update([other, ]**kwargs) on the dict self with the call’s positional and keywords arguments, on the heap h: a dict’s pairs, or pairs from an iterable (a user’s mapping would run its code: unsupported here), then the keyword arguments.

python.Methods.dictPlain

def Methods.dictPlain (h : Heap) (method : String) (self : Value) (positional : List Value) (keywords : List (Codes * Value)) : Changed

A dict method of no arguments, by the name method: keys, values, items (a view), clear, copy; on the dict self with the call’s positional and keywords arguments, on the heap h.

python.Methods.ofDict

def Methods.ofDict : List Method

The dict methods the model provides.

python.Methods.setTable

def Methods.setTable (h : Heap) (self : Value) : SetTable

The table of the set receiver self on the heap h.

python.Methods.storeSet

def Methods.storeSet (h : Heap) (self : Value) (t : SetTable) (v : Value) : Changed

The set receiver self on the heap h with the new table t, and the value v produced.

python.Methods.element

def Methods.element (h : Heap) (x : Value) (work : Unit -> Changed) : Changed

The item x’s check on the heap h, then the method’s work: TypeError for one that is not hashable, unsupported for one the user’s __hash__ hashes.

python.Methods.setChange

def Methods.setChange (h : Heap) (method : String) (self : Value) (positional : List Value) (keywords : List (Codes * Value)) : Changed

s.add(x), s.remove(x) (KeyError when it is not there), s.discard(x) (the method) on the set self with the call’s positional and keywords arguments, on the heap h.

python.Methods.operand

def Methods.operand (h : Heap) (v : Value) : Heap * Either Raised Operand

What a set method reads from the argument v on the heap h: a set’s table, a dict’s keys, or an iterable’s items (every one hashable).

python.Methods.operands

def Methods.operands (h : Heap) (others : List Value) (so : List Operand) : Heap * Either Raised (List Operand)

The operands of the arguments others in turn on the heap h, after the ones so far; the exception that stopped it if one did.

python.Methods.combined

def Methods.combined (method : String) (t : SetTable) (operands : List Operand) : SetTable

The table the set method named method gives from the receiver’s table t and the operands (CPython’s set_union, set_intersection_multi, set_difference_multi, set_symmetric_difference).

python.Methods.combine

def Methods.combine (h : Heap) (method : String) (self : Value) (positional : List Value) (keywords : List (Codes * Value)) : Changed

s.union(*others), intersection, difference, symmetric_difference (exactly one other), by the name method, on the set self with the call’s positional and keywords arguments, on the heap h.

python.Methods.setPlain

def Methods.setPlain (h : Heap) (method : String) (self : Value) (positional : List Value) (keywords : List (Codes * Value)) : Changed

A set method of no arguments, by the name method: clear, copy; on the set self with the call’s positional and keywords arguments, on the heap h.

python.Methods.ofSet

def Methods.ofSet : List Method

The set methods the model provides.

python.Methods.ofTuple

def Methods.ofTuple : List Method

The tuple methods.

python.Methods.propertyWith

def Methods.propertyWith (h : Heap) (method : String) (self : Value) (positional : List Value) (keywords : List (Codes * Value)) : Changed

property.getter(f), property.setter(f) (the method) on the property self with the call’s positional and keywords arguments, on the heap h: a new property with that function.

python.Methods.ofProperty

def Methods.ofProperty : List Method

The property methods.

python.Methods.typeAttributes

def Methods.typeAttributes : List (String * List String)

The attribute names other than __dunder__ ones each built-in type has in CPython 3.14 (dir()).

python.Methods.isDunder

def Methods.isDunder (name : String) : Bool

Whether a name is __dunder__.

python.Methods.typeHas

def Methods.typeHas (typeName : String) (name : String) : Bool

Whether the built-in type named typeName may have the attribute name in CPython: one of its names, or any __dunder__ name.

python.Methods.of

def Methods.of (h : Heap) (self : Value) : List Method

The methods the model provides for the type of the receiver self on the heap h.

python.Methods.missing

def Methods.missing (h : Heap) (self : Value) (name : String) : Raised

Reading the attribute name of the value self on the heap h that the model does not provide: unsupported when CPython’s type has it, AttributeError otherwise (a user’s instance or class: AttributeError as Objects.get gives it).

python.Methods.call

def Methods.call (h : Heap) (self : Value) (name : String) (positional : List Value) (keywords : List (Codes * Value)) : Changed

self.name(*positional, **keywords) for the built-in method name of the receiver self with the call’s positional and keywords arguments, on the heap h.

python.Methods.has

def Methods.has (h : Heap) (self : Value) (name : String) : Bool

Whether the model provides a built-in method named name for the receiver self on the heap h.

python.Methods.attribute

def Methods.attribute (h : Heap) (v : Value) (name : String) : Access

Reading the attribute name of the value v on the heap h: Objects.get, with a built-in type’s attribute the model does not provide reported as unsupported rather than AttributeError.