builtins

python.Builtin

def Builtin : Type

What a built-in does with its arguments: the heap, the positional arguments, the keyword arguments.

python.Builtins.natural

def Builtins.natural (n : Nat) : Value

An int of the natural value n.

python.Builtins.floatResult

def Builtins.floatResult (h : Heap) (f : Float) : Changed

The float f produced, on the heap h.

python.Builtins.floatOutcome

def Builtins.floatOutcome (f : Float) : Outcome

The float f as an outcome.

python.Builtins.argument

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

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

python.Builtins.runsCode

def Builtins.runsCode (what : String) : Raised

What running a user’s method what would need: unsupported here.

python.Builtins.definesAny

def Builtins.definesAny (h : Heap) (v : Value) (names : List String) : Bool

Whether the value v on the heap h is an instance whose class defines one of the methods names.

python.Builtins.len

def Builtins.len (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Changed

len(x), with the call’s positional and keywords arguments on the heap h.

python.Builtins.abs

def Builtins.abs (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Changed

abs(x), with the call’s positional and keywords arguments on the heap h.

python.Builtins.round

def Builtins.round (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Changed

round(number, ndigits=None), with the call’s positional and keywords arguments on the heap h.

python.Builtins.divmod

def Builtins.divmod (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Changed

divmod(a, b): the floor quotient and the remainder. With the call’s positional and keywords arguments on the heap h.

python.Builtins.digitValue

def Builtins.digitValue (c : Nat) : Option Nat

The value of the digit c in bases up to 36 (none for anything else).

python.Builtins.digitsIn

def Builtins.digitsIn (base : Nat) (value : Nat) (count : Nat) (afterDigit : Bool) (underscoreFirst : Bool) (cs : Codes) : Option (Nat * Nat)

The digits cs in base with single underscores between them (an underscore may come first when underscoreFirst: a prefix came before), after count digits read so far of value value (afterDigit when the last was a digit): the value and how many digits; none for anything else.

python.Builtins.digitsAfterUnderscore

def Builtins.digitsAfterUnderscore (base : Nat) (value : Nat) (count : Nat) (cs : Codes) : Option (Nat * Nat)

The digits cs in base after an underscore, after count digits read so far of value value: a digit must come next.

python.Builtins.prefixBase

def Builtins.prefixBase (cs : Codes) : Option Nat

The base a prefix gives (0x, 0o, 0b in either case), if the text cs has one.

python.Builtins.powerOfTwo

def Builtins.powerOfTwo (base : Nat) : Bool

Whether a base is a power of two (its texts have no digit limit).

python.Builtins.allZeros

def Builtins.allZeros (cs : Codes) : Bool

Whether the decimal digits cs are all zeros (base 0 allows leading zeros only then).

python.Builtins.parseInt

def Builtins.parseInt (cs : Codes) (base : Nat) : Either Raised Int

int(text, base) of the text cs (CPython’s PyLong_FromString): whitespace and a sign around, then a prefix that matches the base, then digits.

python.Builtins.toInt

def Builtins.toInt (h : Heap) (x : Value) : Outcome

int(x) of the value x on the heap h without a base: a number truncated toward zero, a text in base 10.

python.Builtins.int

def Builtins.int (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Changed

int(x=0, /, base=10), with the call’s positional and keywords arguments on the heap h.

python.Builtins.float

def Builtins.float (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Changed

float(x=0.0), with the call’s positional and keywords arguments on the heap h.

python.Builtins.shown

def Builtins.shown (h : Heap) (asRepr : Bool) (x : Value) : Changed

str(x), or repr(x) when asRepr, of the value x on the heap h, checked for ints too long.

python.Builtins.str

def Builtins.str (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Changed

str(object=''), and str(object, encoding, errors) (bytes are not in the subset). With the call’s positional and keywords arguments on the heap h.

python.Builtins.repr

def Builtins.repr (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Changed

repr(x), with the call’s positional and keywords arguments on the heap h.

python.Builtins.truth

def Builtins.truth (h : Heap) (v : Value) : Option Bool

The truth of the value v on the heap h; none when it would run a user’s __bool__ or __len__.

python.Builtins.bool

def Builtins.bool (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Changed

bool(x=False), with the call’s positional and keywords arguments on the heap h.

python.Builtins.type

def Builtins.type (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Changed

type(x): its class (making a class with three arguments is not in the subset). With the call’s positional and keywords arguments on the heap h.

python.Builtins.format

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

format(value, format_spec=''), with the call’s positional and keywords arguments on the heap h.

python.Builtins.range

def Builtins.range (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Changed

range(stop), range(start, stop[, step]), with the call’s positional and keywords arguments on the heap h.

python.Builtins.items

def Builtins.items (h : Heap) (v : Value) (work : Heap -> List Value -> Changed) : Changed

The items of the iterable argument v on the heap h given to work, or the exception.

python.Builtins.collection

def Builtins.collection (h : Heap) (kind : String) (positional : List Value) (keywords : List (Codes * Value)) : Changed

list(iterable=()), tuple(iterable=()), set(iterable=()), by kind, with the call’s positional and keywords arguments on the heap h.

python.Builtins.dict

def Builtins.dict (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Changed

dict(**kwargs), dict(mapping, **kwargs), dict(iterable, **kwargs): a new dict updated as dict.update. With the call’s positional and keywords arguments on the heap h.

python.Builtins.sorted

def Builtins.sorted (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Changed

sorted(iterable, /, *, key=None, reverse=False): a new list sorted as list.sort. With the call’s positional and keywords arguments on the heap h.

python.Builtins.floatSum

def Builtins.floatSum (total : Float) (compensation : Float) (xs : List Value) : Float * (Float * List Value)

Neumaier’s compensated sum of floats (CPython’s builtin_sum_impl from 3.12): the sum so far total, the compensation, the items left xs; an int that fits a C long is converted to a float first. The rest (the first item that is not a float or such an int) goes to the generic addition.

python.Builtins.compensated

def Builtins.compensated (total : Float) (compensation : Float) : Float

The sum total with the compensation added in when it is finite and not zero.

python.Builtins.sumWithin

def Builtins.sumWithin (fuel : Nat) (h : Heap) (total : Value) (xs : List Value) : Changed

Adding the items xs to the sum total in turn, on the heap h (fuel: the items left): a float sum is compensated.

python.Builtins.addThen

def Builtins.addThen (fuel : Nat) (h : Heap) (total : Value) (x : Value) (rest : List Value) : Changed

Adding the item x to the sum total with + on the heap h, then the rest (fuel: the items left).

python.Builtins.sum

def Builtins.sum (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Changed

sum(iterable, /, start=0): a str start is TypeError. With the call’s positional and keywords arguments on the heap h.

python.Builtins.extreme

def Builtins.extreme (h : Heap) (isMax : Bool) (best : Value) (xs : List Value) : Outcome

The first greatest (max, when isMax) or least (min) of best and the values xs after it, on the heap h.

python.Builtins.zipped

def Builtins.zipped (keys : List Value) (items : List Value) : List (Value * Value)

The keys paired with the items, in order (as long as the shorter).

python.Builtins.extremeBy

def Builtins.extremeBy (h : Heap) (isMax : Bool) (best : Value * Value) (xs : List (Value * Value)) : Outcome

The item of the greatest (max, when isMax) or least key among the key and item pair best so far and the rest xs, on the heap h: the first such item, as CPython keeps the one it has unless a later key is strictly greater (or less).

python.Builtins.byKeys

def Builtins.byKeys (h : Heap) (name : String) (items : List Value) (keys : List Value) (reversed : Bool) (fallback : Option Value) : Changed

sorted, min and max (by name) on the heap h once a key function’s keys are known (the caller called it on each item, as CPython does before comparing): the items in the order of their keys (reversed as reverse says), or the item of the least or greatest key (the default fallback, or ValueError, for none); keys whose comparison is a user’s code are not taken here.

python.Builtins.exceptionInit

def Builtins.exceptionInit (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Changed

An exception’s built-in __init__(self, *args) (a user’s exception class calling super().__init__): its args set (and a StopIteration’s value), None returned; keyword arguments are a TypeError. With the call’s positional and keywords arguments on the heap h.

python.Builtins.exceptionStr

def Builtins.exceptionStr (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Changed

An exception’s built-in __str__(self): ‘’ for no arguments, the str of the only one, else the str of the tuple; an argument whose str is a user’s code is not taken here. With the call’s positional and keywords arguments on the heap h.

python.Builtins.extremeOf

def Builtins.extremeOf (h : Heap) (name : String) (positional : List Value) (keywords : List (Codes * Value)) : Changed

max(iterable, *, key=None, default), max(a, b, *args, key=None), and min, by name, with the call’s positional and keywords arguments on the heap h.

python.Builtins.decide

def Builtins.decide (h : Heap) (wanted : Bool) (xs : List Value) : Option Bool

The truths of the values xs on the heap h in order, until one decides (any: a true one, wanted true; all: a false one); none when a user’s code would run first.

python.Builtins.decideTaking

def Builtins.decideTaking (fuel : Nat) (h : Heap) (wanted : Bool) (it : Value) : Changed

any and all (wanted true for any) over the iterator it on the heap h: items taken one at a time, at most fuel, until one decides (the rest stay in the iterator).

python.Builtins.anyAll

def Builtins.anyAll (h : Heap) (name : String) (positional : List Value) (keywords : List (Codes * Value)) : Changed

any(iterable), all(iterable), by name, with the call’s positional and keywords arguments on the heap h.

python.Builtins.ord

def Builtins.ord (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Changed

ord(c), with the call’s positional and keywords arguments on the heap h.

python.Builtins.chr

def Builtins.chr (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Changed

chr(i), with the call’s positional and keywords arguments on the heap h.

python.Builtins.classTest

def Builtins.classTest (h : Heap) (name : String) (positional : List Value) (keywords : List (Codes * Value)) : Changed

isinstance(x, classes), issubclass(c, classes), by name, with the call’s positional and keywords arguments on the heap h.

python.Builtins.wrapped

def Builtins.wrapped (h : Heap) (name : String) (positional : List Value) (keywords : List (Codes * Value)) : Changed

staticmethod(f), classmethod(f), by name, with the call’s positional and keywords arguments on the heap h.

python.Builtins.property

def Builtins.property (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Changed

property(fget=None, fset=None, fdel=None, doc=None) (deleting through a property is not in the subset). With the call’s positional and keywords arguments on the heap h.

python.Builtins.propertyWith

def Builtins.propertyWith (which : String) (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Changed

p.getter(f) and p.setter(f): a new property with the function as its getter or setter, the other kept (p.deleter is not in the subset, as deleting through a property is not). By which, with the call’s positional and keywords arguments on the heap h.

python.Builtins.iter

def Builtins.iter (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Changed

iter(object) (with a sentinel it needs a callable: the user’s code, unsupported here). With the call’s positional and keywords arguments on the heap h.

python.Exec.builtinOf

def Exec.builtinOf (f : Value) : Option Codes

Whether f is a built-in function’s value: its name if it is.

python.Builtins.next

def Builtins.next (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Changed

next(iterator[, default]): StopIteration when it has run out and there is no default. With the call’s positional and keywords arguments on the heap h.

python.Builtins.enumerate

def Builtins.enumerate (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Changed

enumerate(iterable, start=0) (CPython’s own argument parsing: its own messages for keywords). With the call’s positional and keywords arguments on the heap h.

python.Builtins.iteratorsOf

def Builtins.iteratorsOf (h : Heap) (xs : List Value) (so : List Value) : Changed

Iterators of the iterables xs in turn on the heap h, after the ones so far, or the first exception.

python.Builtins.zip

def Builtins.zip (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Changed

zip(*iterables, strict=False), with the call’s positional and keywords arguments on the heap h.

python.Builtins.reversed

def Builtins.reversed (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Changed

reversed(seq): a list walked backward as it is, a tuple’s or a str’s items backward, a range backward (a dict, a dict’s view or a user’s sequence: unsupported here). With the call’s positional and keywords arguments on the heap h.

python.Builtins.named

def Builtins.named (name : String) (f : Heap -> String -> List Value -> List (Codes * Value) -> Changed) : Builtin

The built-in f with name as the name it takes first.

python.Builtins.functions

def Builtins.functions : List Builtin

The built-in functions the model provides.

python.Builtins.real

def Builtins.real (h : Heap) (v : Value) : Either Raised Float

The real number argument v of a math function, on the heap h, as a float: TypeError for anything else, OverflowError for an int too large.

python.Builtins.sqrt

def Builtins.sqrt (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Changed

math.sqrt(x): ValueError for a negative x. With the call’s positional and keywords arguments on the heap h.

python.Builtins.fabs

def Builtins.fabs (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Changed

math.fabs(x), with the call’s positional and keywords arguments on the heap h.

python.Builtins.rounded

def Builtins.rounded (h : Heap) (name : String) (positional : List Value) (keywords : List (Codes * Value)) : Changed

math.floor(x), math.ceil(x): an int. By name, with the call’s positional and keywords arguments on the heap h.

python.Builtins.mathPow

def Builtins.mathPow (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Changed

math.pow(x, y) (CPython’s math_pow_impl): a NaN from finite arguments, or zero to a negative power, is ValueError; an infinite result from finite arguments is OverflowError. With the call’s positional and keywords arguments on the heap h.

python.Builtins.truncatedRemainder

def Builtins.truncatedRemainder (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Changed

math.fmod(x, y) (CPython’s math_fmod_impl): the remainder of the truncating division, with the sign of x. An infinite y leaves a finite x as it is; a NaN from arguments that are not NaN (y zero, or x infinite) is ValueError. With the call’s positional and keywords arguments on the heap h.

python.Builtins.gcdWithin

def Builtins.gcdWithin (fuel : Nat) (a : Nat) (b : Nat) : Nat

The greatest common divisor of the naturals a and b, within fuel steps.

python.Builtins.gcdOf

def Builtins.gcdOf (a : Nat) (b : Nat) : Nat

The greatest common divisor of the naturals a and b.

python.Builtins.gcd

def Builtins.gcd (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Changed

math.gcd(*integers): zero for none. With the call’s positional and keywords arguments on the heap h.

python.Builtins.factorialOf

def Builtins.factorialOf (n : Nat) : Nat

n!, the factorial of n.

python.Builtins.factorial

def Builtins.factorial (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Changed

math.factorial(n): ValueError for a negative n, OverflowError past a C long. With the call’s positional and keywords arguments on the heap h.

python.Builtins.inexactMath

def Builtins.inexactMath : List String

The math functions whose accuracy CPython leaves to the platform’s math library (it calls libm’s pow): the model gives the correctly rounded result, which the verdict assumes of the library (the same choice the C family names for pow). sqrt and fmod are exact by IEEE 754 and assume nothing.

python.Builtins.math

def Builtins.math : List Builtin

The math module’s functions the model provides.

python.Builtins.mathConstant

def Builtins.mathConstant (name : String) : Option Value

The math module’s constant name: the binary64 nearest to each (their shortest decimals read back to them).

python.Builtins.call

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

Calling the built-in function or math function name (math.sqrt) with the call’s positional and keywords arguments on the heap h; a name the model does not provide is unsupported.