operations

python.Operations.unsupported

def Operations.unsupported (h : Heap) (symbol : String) (a : Value) (b : Value) : Outcome

TypeError for the operator symbol its operands a and b do not support (their type names read from the heap h).

python.Outcome.float

def Outcome.float (x : Float) : Outcome

The float x produced.

python.Outcome.int

def Outcome.int (n : Int) : Outcome

The int n produced.

python.Operations.asFloat

def Operations.asFloat (n : Int) (next : Float -> Outcome) : Outcome

The int n as a float passed on to next (the operation with a float), or OverflowError.

python.Operations.numeric

def Operations.numeric (onInts : Int -> Int -> Outcome) (onFloats : Float -> Float -> Outcome) (a : Value) (b : Value) : Option Outcome

An arithmetic operator on the numbers a and b: onInts on ints, or onFloats on floats when either is one; none when either is not a number.

python.Operations.pure

def Operations.pure (h : Heap) (o : Outcome) : Changed

An operator’s outcome o that leaves the heap h as it is.

python.Operations.join

def Operations.join (h : Heap) (a : Value) (b : Value) : Outcome

a + b on str and tuples on the heap h (lists are python.containers’s).

python.Operations.add

def Operations.add (h : Heap) (a : Value) (b : Value) : Changed

a + b on the heap h.

python.Operations.setOperation

def Operations.setOperation (symbol : String) (t : SetTable) (u : SetTable) : SetTable

The set the operator symbol gives on the sets t and u (CPython’s set_or, set_and, set_sub, set_xor): | a copy of t updated with u, & the intersection, - the difference, ^ the symmetric difference.

python.Operations.setInPlace

def Operations.setInPlace (symbol : String) (t : SetTable) (u : SetTable) : SetTable

The set t changed in place by the operator symbol with the set u (|= update, &= the intersection’s table, -= difference update, ^= symmetric difference update).

python.Heap.dictPairs

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

A dict’s pairs, if the value v is one on the heap h.

python.Operations.collections

def Operations.collections (h : Heap) (symbol : String) (a : Value) (b : Value) : Option Changed

The set or dict operator symbol on a and b on the heap h, if the left operand a is a set or a dict (a dict only merges with |); none otherwise.

python.Operations.subtract

def Operations.subtract (h : Heap) (a : Value) (b : Value) : Changed

a - b on the heap h.

python.Operations.repeatChecked

def Operations.repeatChecked (k : Int) (size : Nat) (make : Unit -> Outcome) : Outcome

A repetition’s count k checked for a sequence of size items: past an index’s range is OverflowError, a result past 2^32 items MemoryError (the result is made only after the checks: make).

python.Operations.repeatSequence

def Operations.repeatSequence (k : Int) (v : Value) : Option Outcome

A str or tuple repeated k times, if the value v is one.

python.Operations.isSequence

def Operations.isSequence (v : Value) : Bool

Whether the value v is a str or a tuple.

python.Operations.multiplyValues

def Operations.multiplyValues (h : Heap) (a : Value) (b : Value) : Outcome

a * b on the heap h when neither is a list: numbers, or a str or tuple and an int.

python.Operations.multiply

def Operations.multiply (h : Heap) (a : Value) (b : Value) : Changed

a * b on the heap h.

python.Operations.byZero

def Operations.byZero : Outcome

ZeroDivisionError.

python.Operations.divideInts

def Operations.divideInts (x : Int) (y : Int) : Outcome

x / y on ints: the exact quotient correctly rounded to a float.

python.Operations.divide

def Operations.divide (h : Heap) (a : Value) (b : Value) : Changed

a / b on the heap h.

python.Operations.floorDivide

def Operations.floorDivide (h : Heap) (a : Value) (b : Value) : Changed

a // b on the heap h.

python.Operations.modulo

def Operations.modulo (h : Heap) (a : Value) (b : Value) : Changed

a % b on the heap h: the remainder of numbers, or printf-style formatting when a is a str.

python.Operations.power

def Operations.power (x : Int) (k : Nat) : Int

The int x to the natural power k.

python.Operations.powerInts

def Operations.powerInts (x : Int) (y : Int) : Outcome

x ** y on ints: an int for a power not negative, else the exact value as a float.

python.Operations.isFinite

def Operations.isFinite (x : Float) : Bool

Whether the float x is finite.

python.Operations.isIntegral

def Operations.isIntegral (x : Float) : Bool

Whether the float x is an integer (NaN and infinities count as integers here).

python.Operations.powerFloats

def Operations.powerFloats (x : Float) (y : Float) : Outcome

x ** y on floats: zero to a negative power is ZeroDivisionError (-0.0 is not negative: anything to the power zero is 1.0), a negative base to a power that is not an integer is a complex number (outside the subset: what the model cannot do, not an exception of Python), a finite result too large is OverflowError.

python.Operations.toPower

def Operations.toPower (h : Heap) (a : Value) (b : Value) : Changed

a ** b (and pow(a, b)) on the heap h.

python.Operations.badOperand

def Operations.badOperand (h : Heap) (symbol : String) (a : Value) : Outcome

TypeError for the unary operator symbol its operand a does not support (its type name read from the heap h).

python.Operations.negate

def Operations.negate (h : Heap) (a : Value) : Outcome

-a on the heap h.

python.Operations.plus

def Operations.plus (h : Heap) (a : Value) : Outcome

+a on the heap h: a bool becomes an int, a number stays.

python.Operations.invert

def Operations.invert (h : Heap) (a : Value) : Outcome

~a on an int, on the heap h.

python.Operations.isBool

def Operations.isBool (v : Value) : Bool

Whether the value v is a bool.

python.Operations.bitwiseValues

def Operations.bitwiseValues (h : Heap) (symbol : String) (f : Int -> Int -> Int) (a : Value) (b : Value) : Outcome

a & b, a | b or a ^ b on ints on the heap h: the operator symbol computed by f (two bools give a bool).

python.Operations.bitwise

def Operations.bitwise (h : Heap) (symbol : String) (f : Int -> Int -> Int) (a : Value) (b : Value) : Changed

a & b, a | b or a ^ b on the heap h, the operator symbol computed on ints by f: sets and dicts first, then ints.

python.Operations.shift

def Operations.shift (h : Heap) (left : Bool) (a : Value) (b : Value) : Outcome

a << b (when left) or a >> b on ints on the heap h: a negative count is ValueError.

python.Operations.round

def Operations.round (h : Heap) (a : Value) : Outcome

round(a) on the heap h: an int rounded half to even.

python.Operations.roundTo

def Operations.roundTo (h : Heap) (a : Value) (n : Int) : Outcome

round(a, n) on the heap h: a float rounded half to even at n decimal places of its exact value (n may be negative), as the nearest float; an int rounded to a power of ten when n is negative.

python.Operations.compare

def Operations.compare (h : Heap) (symbol : String) (a : Value) (b : Value) : Outcome

The order comparison symbol of a and b by contents on the heap h: <, <=, > or >=.

python.Operations.notEqual

def Operations.notEqual (h : Heap) (a : Value) (b : Value) : Outcome

a != b on the heap h.

python.Operations.isLazy

def Operations.isLazy (h : Heap) (v : Value) : Bool

Whether taking the items of the value v on the heap h would run the user’s code: a generator, or an instance whose class defines __iter__ (an iterator is used up by Iterator.take).

python.Heap.storeList

def Heap.storeList (h : Heap) (a : Nat) (items : List Value) : Heap

The heap h with the list at the address a holding items.

python.Heap.storeDict

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

The heap h with the dict at the address a holding pairs (later pairs win).

python.Operations.lazyError

def Operations.lazyError (h : Heap) : Changed

What the model cannot do in place, on the heap h: taking items that run the user’s code.

python.Operations.extend

def Operations.extend (h : Heap) (a : Nat) (x : Value) (xs : List Value) (y : Value) : Changed

l += y on the list x at the address a on the heap h: its items xs extended by y’s.

python.Operations.pairs

def Operations.pairs (h : Heap) (items : List Value) : Option (List (Value * Value))

The items as pairs, when each is a pair (two items) on the heap h.

python.Operations.update

def Operations.update (h : Heap) (a : Nat) (x : Value) (pairs : List (Value * Value)) (y : Value) : Changed

d |= y on the dict x at the address a on the heap h, its pairs followed by another dict’s pairs, or by pairs from an iterable.

python.Operations.inPlace

def Operations.inPlace (h : Heap) (symbol : String) (x : Value) (y : Value) : Option Changed

The in-place form of the operator symbol with y on the object x refers to on the heap h, if it has one.

python.Operations.unsupportedPrefix

def Operations.unsupportedPrefix : Codes

The prefix of the “unsupported operand” message.

python.Operations.augmentedError

def Operations.augmentedError (symbol : String) (e : Raised) : Raised

The exception e with the operator symbol written as op= in its message when it is the “unsupported operand” TypeError.

python.Operations.augmented

def Operations.augmented (h : Heap) (symbol : String) (binary : Heap -> Value -> Value -> Changed) (x : Value) (y : Value) : Changed

x op= y for the operator symbol on the heap h: the in-place form when x’s object has one, else the operator’s binary form (its error written with op=).