calls

python.Suggest.substitution

def Suggest.substitution (a : Nat) (b : Nat) : Nat

The cost of changing the code point a to b in a suggestion’s distance (CPython’s suggestions.c): nothing for the same, 1 for the same letter in another case, 2 otherwise.

python.Suggest.trimStart

def Suggest.trimStart (a : Codes) (b : Codes) : Codes * Codes

The texts a and b without the code points they start with in common.

python.Suggest.trim

def Suggest.trim (a : Codes) (b : Codes) : Codes * Codes

The texts a and b without the code points they start or end with in common.

python.Suggest.row

def Suggest.row (code : Nat) (a : Codes) (buffer : List Nat) (distance : Nat) (result : Nat) : List Nat * Nat

One row of the distance table for the code point code of the longer text against the shorter text a, after the row buffer: the new row and its last entry (distance and result as CPython names them).

python.Suggest.least

def Suggest.least (xs : List Nat) : Nat

The smallest of the naturals xs (zero when there are none).

python.Suggest.rows

def Suggest.rows (a : Codes) (b : Codes) (index : Nat) (buffer : List Nat) (result : Nat) (most : Nat) : Nat

The distance table row by row, for the code points of the longer text b against the shorter a from row index on, after the row buffer whose last entry is result; past the largest cost allowed, most, as soon as a row’s least entry is.

python.Suggest.firstRow

def Suggest.firstRow (k : Nat) (a : Codes) : List Nat

The first costs of a row: 2, 4, 6 and so on for each code point of a, the first after k code points.

python.Suggest.distance

def Suggest.distance (a : Codes) (b : Codes) (most : Nat) : Nat

CPython’s weighted Levenshtein distance of the texts a and b, or one more than the largest cost allowed, most, when it is past it.

python.Suggest.nearestAfter

def Suggest.nearestAfter (name : Codes) (names : List String) (best : Option (String * Nat)) : Option String

The nearest of names to a name, after the best so far (CPython’s _Py_CalculateSuggestions): at most a third of the code points involved changed, the first of the nearest.

python.Suggest.nearest

def Suggest.nearest (name : Codes) (names : List String) : Option String

The nearest of names to a name, if one is near enough.

python.Signature

record Signature

A function’s parameters: its __qualname__, the positional parameters (the first positionalOnly of them before /, the last defaults of them with defaults), the keyword-only ones and which of them have defaults, whether it takes *args and **kwargs, and how many cells its value captured.

python.Calls.nameList

def Calls.nameList (names : List String) : String

The names quoted as a list: ‘a’, ‘a’ and ‘b’, ‘a’, ‘b’, and ‘c’ (CPython’s format_missing).

python.Calls.nameTail

def Calls.nameTail (names : List String) : String

The names after the first in a list of three or more: ‘b’, and ‘c’.

python.Calls.plural

def Calls.plural (k : Nat) : String

“s” unless the count k is one.

python.Calls.fails

def Calls.fails (s : Signature) (message : String) : Raised

TypeError with message after the name of the function whose parameters are s.

python.Calls.tooMany

def Calls.tooMany (s : Signature) (given : Nat) (keywordGiven : Nat) : Raised

Too many positional arguments, given of them, for the parameters s (CPython’s too_many_positional): the keywordGiven keyword-only arguments given are counted when there are some.

python.Calls.missing

def Calls.missing (s : Signature) (kind : String) (names : List String) : Raised

The missing parameters names of s, of a kind (“positional” or “keyword-only”).

python.Calls.indexFrom

def Calls.indexFrom (k : Nat) (names : List String) (name : Codes) : Option Nat

Where a name is among names, counting from k.

python.Calls.indexOf

def Calls.indexOf (names : List String) (name : Codes) : Option Nat

Where a name is among names.

python.Calls.keyword

def Calls.keyword (keywords : List (Codes * Value)) (name : String) : Option Value

The value of the keyword argument name among keywords.

python.Calls.namable

def Calls.namable (s : Signature) : List String

The positional parameters of s a keyword can name (the ones after /); the positional-only ones cannot.

python.Calls.positionalOnlyGiven

def Calls.positionalOnlyGiven (s : Signature) (keywords : List (Codes * Value)) : List String

The positional-only parameters of s given among the keyword arguments keywords, in the order of the parameters.

python.Calls.unexpected

def Calls.unexpected (s : Signature) (name : Codes) (keywords : List (Codes * Value)) : Raised

The keyword argument name no parameter of s has: unexpected (with the nearest name), or the positional-only ones passed as keywords when the call’s keywords have some.

python.Calls.keywordProblem

def Calls.keywordProblem (s : Signature) (filled : Nat) (all : List (Codes * Value)) (keywords : List (Codes * Value)) : Option Raised

The first problem with the keyword arguments keywords (the rest of the call’s all) for the parameters s, in the order the call gives them: one for a parameter the positional arguments filled (the first filled), or one no parameter has (when there is no **kwargs).

python.Calls.positionalSlots

def Calls.positionalSlots (s : Signature) (captured : List Value) (positional : List Value) (keywords : List (Codes * Value)) (k : Nat) (names : List String) : List (Option Value)

The value of each positional parameter of s in names, from position k on: given in positional, by keyword in keywords (not a positional-only one), or its default among the function value’s captured values; none when it has neither.

python.Calls.keywordSlots

def Calls.keywordSlots (names : List String) (hasDefault : List Bool) (defaults : List Value) (keywords : List (Codes * Value)) : List (Option Value)

The value of each keyword-only parameter in names: given in keywords, or its default (hasDefault says which have one; defaults holds only the ones there are); none when it has neither.

python.Calls.unfilled

def Calls.unfilled (names : List String) (slots : List (Option Value)) : List String

The names whose slots have no value.

python.Calls.extra

def Calls.extra (s : Signature) (keywords : List (Codes * Value)) : List (Value * Value)

The keyword arguments for the **kwargs of s: the ones among keywords no parameter a keyword can name has, in the call’s order.

python.Calls.layout

def Calls.layout (h : Heap) (s : Signature) (values : List Value) (positional : List Value) (keywords : List (Codes * Value)) : Changed

The values of the parameters s on the heap h once every check passed: the positional and keyword-only ones’ values, the *args tuple of the rest of positional, the **kwargs dict of the keywords left over.

python.Calls.bind

def Calls.bind (h : Heap) (s : Signature) (captured : List Value) (positional : List Value) (keywords : List (Codes * Value)) : Changed

Binding a call’s positional and keywords arguments to a function’s parameters s on the heap h (CPython’s initialize_locals), the function value’s captured values being its cells and then its defaults.

python.Calls.display

def Calls.display (h : Heap) (f : Value) : String

How a call’s messages name the function f it calls, on the heap h (CPython’s _PyEval_FormatKwargsError): a user’s function by __main__. and its qualified name, a built-in one or a class by its name.

python.Calls.notCallable

def Calls.notCallable (h : Heap) (v : Value) : Raised

TypeError: the value v on the heap h cannot be called.

python.Calls.star

def Calls.star (h : Heap) (f : Value) (alone : Bool) (x : Value) : Taken

The values *x gives at a call site of f on the heap h (an iterator is used up); alone, whether it is the call’s only positional argument, decides CPython’s message for a value that is not iterable.

python.Keyword

data Keyword

A keyword argument at a call site: name=value, or **mapping.

python.Merged

data Merged

The keyword arguments a call site gives (keys not checked yet), or an exception.

python.Calls.dictPairs

def Calls.dictPairs (h : Heap) (v : Value) : Option (List (Value * Value))

The pairs of the dict v on the heap h, if it is one.

python.Calls.add

def Calls.add (h : Heap) (f : Value) (so : List (Value * Value)) (pairs : List (Value * Value)) : Merged

The pairs added after the ones so far, for a call of f on the heap h; TypeError for a key given twice.

python.Calls.merge

def Calls.merge (h : Heap) (f : Value) (so : List (Value * Value)) (items : List Keyword) : Merged

The keyword arguments items of a call site of f merged in order after the ones so far, on the heap h (CPython’s DICT_MERGE): a mapping after ** (a user’s mapping would run its code: unsupported), each name once.

python.Keywords

data Keywords

What the keyword arguments of a call site are: names and values, or an exception.

python.Calls.named

def Calls.named (pairs : List (Value * Value)) (so : List (Codes * Value)) : Keywords

The merged keyword arguments pairs with their keys as names, after the ones so far: TypeError for a key that is not a str.

python.Calls.keywords

def Calls.keywords (h : Heap) (f : Value) (items : List Keyword) : Keywords

The keyword arguments items of a call site of f, on the heap h: merged in order, then every key checked to be a str.

python.Native.fails

def Native.fails (message : String) : Option Raised

A built-in’s TypeError with message.

python.Native.noArguments

def Native.noArguments (qualified : String) (positional : List Value) (keywords : List (Codes * Value)) : Option Raised

METH_NOARGS: no arguments, neither positional nor keywords (qualified: the name with its type, str.upper).

python.Native.exactlyOne

def Native.exactlyOne (qualified : String) (positional : List Value) (keywords : List (Codes * Value)) : Option Raised

METH_O: exactly one argument in positional and no keywords (qualified: the name with its type).

python.Native.positionalRange

def Native.positionalRange (short : String) (least : Nat) (most : Nat) (given : Nat) : Option Raised

_PyArg_CheckPositional: between least and most positional arguments, given of them, by the short name.

python.Native.positionalOnly

def Native.positionalOnly (qualified : String) (short : String) (least : Nat) (most : Nat) (positional : List Value) (keywords : List (Codes * Value)) : Option Raised

_PyArg_CheckPositional without keyword arguments: between least and most arguments in positional, none in keywords (qualified for the keyword message, short for the count).

python.Clinic

record Clinic

Parameters as Argument Clinic declares them: the function’s name, the parameters in order (the first positionalOnly cannot be named, the first required must be given, at most positionalMost by position), and whether more positional arguments go to *args.

python.Clinic.bound

def Clinic.bound (which : String) (least : Nat) (most : Nat) : String

which (“at least” or “at most”), or “exactly” when the bounds least and most meet.

python.Clinic.counts

def Clinic.counts (c : Clinic) (given : Nat) (named : Nat) : Option Raised

The first problem with the counts for c, given positional and named keyword arguments: too many in all (or too many keywords, when none can be positional or the rest go to *args), too few positional, too many positional.

python.Clinic.missing

def Clinic.missing (c : Clinic) (given : Nat) (keywords : List (Codes * Value)) (k : Nat) (names : List String) : Option Raised

The first required parameter of c neither among the given by position nor named in keywords, from parameter k on, the parameters in names.

python.Clinic.leftover

def Clinic.leftover (c : Clinic) (given : Nat) (keywords : List (Codes * Value)) : Option Raised

The first of keywords that names no parameter of c it can (unexpected, with the nearest name) or one already among the given by position.

python.Clinic.slots

def Clinic.slots (c : Clinic) (positional : List Value) (keywords : List (Codes * Value)) (k : Nat) (names : List String) : List (Option Value)

The value of each parameter of c in names, from position k on: in positional, else named in keywords (not a positional-only one).

python.Parsed

data Parsed

What parsing a built-in’s arguments gives: each parameter’s value (none: not given) and the positional arguments past them, or an exception.

python.Clinic.parse

def Clinic.parse (c : Clinic) (positional : List Value) (keywords : List (Codes * Value)) : Parsed

_PyArg_UnpackKeywords for the parameters c and the arguments positional and keywords: the counts, then the required parameters, then the keyword arguments left over.