containers

python.Ordering

data Ordering

How values compare without the heap: an order (-1, 0 or 1), unordered (a NaN takes part: every comparison is false), or incomparable (< raises TypeError).

python.Value.equal

def Value.equal (a : Value) (b : Value) : Bool

Whether the values a and b are equal without looking at the heap: numbers by value, str by code points, tuples item by item, objects on the heap by address.

python.Value.equalOther

def Value.equalOther (a : Value) (b : Value) : Bool

Whether a, a value that is not a number, equals b.

python.Value.equalAll

def Value.equalAll (xs : List Value) (ys : List Value) : Bool

Whether the lists of values xs and ys are equal item by item.

python.Value.compareCodes

def Value.compareCodes (xs : Codes) (ys : Codes) : Int

Comparing the code points xs with ys: -1, 0 or 1.

python.Value.order

def Value.order (a : Value) (b : Value) : Ordering

How the values a and b compare without the heap.

python.Value.orderOther

def Value.orderOther (a : Value) (b : Value) : Ordering

How a, a value that is not a number, compares with b: str by code points, tuples by their first unequal items.

python.Value.orderAll

def Value.orderAll (xs : List Value) (ys : List Value) : Ordering

How the lists xs and ys compare: by the first items that are not equal, else by length.

python.Changed

data Changed

What changing the heap gives: the new heap and the outcome.

python.Changed.same

def Changed.same (h : Heap) (o : Outcome) : Changed

The heap h unchanged, with the outcome o.

python.Changed.value

def Changed.value (h : Heap) (v : Value) : Changed

The heap h with the value v produced.

python.Heap.allocate

def Heap.allocate (h : Heap) (o : Object) : Changed

The new object o on the heap h: the heap with it, and a reference to it.

python.Heap.store

def Heap.store (h : Heap) (a : Nat) (o : Object) : Heap

The heap h with the object at the address a replaced by o.

python.Heap.list

def Heap.list (h : Heap) (xs : List Value) : Changed

A new list of the values xs on the heap h.

python.Attributes.find

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

The attribute of a name among attributes in order.

python.Class.order

def Class.order (h : Heap) (c : Value) : List Value

The class value c’s method resolution order (itself first) on the heap h: empty for a built-in class.

python.Class.attributes

def Class.attributes (h : Heap) (c : Value) : List (Codes * Value)

The class value c’s own attributes on the heap h.

python.Class.hashable

def Class.hashable (h : Heap) (order : List Value) : Bool

Whether instances of the classes in the method resolution order on the heap h are hashable: the first class defining __hash__ or __eq__ decides (only __eq__ makes them unhashable).

python.Value.hashable

def Value.hashable (h : Heap) (v : Value) : Bool

Whether the value v on the heap h can be a dict key or a set item.

python.Value.hashableAll

def Value.hashableAll (h : Heap) (vs : List Value) : Bool

Whether every value of vs on the heap h can be a dict key.

python.Containers.unhashableKey

def Containers.unhashableKey (h : Heap) (v : Value) : Outcome

TypeError for v as an unhashable dict key, its type name read from the heap h (CPython 3.14’s words).

python.Containers.unhashableItem

def Containers.unhashableItem (h : Heap) (v : Value) : Outcome

TypeError for v as an unhashable set item, its type name read from the heap h (CPython 3.14’s words).

python.Dict.get

def Dict.get (pairs : List (Value * Value)) (k : Value) : Option Value

The value for the key k in the dict’s pairs.

python.Dict.set

def Dict.set (pairs : List (Value * Value)) (k : Value) (v : Value) : List (Value * Value)

The dict’s pairs with the key k set to v: an existing key keeps its key and place, a new one goes last.

python.Dict.remove

def Dict.remove (pairs : List (Value * Value)) (k : Value) : List (Value * Value)

The dict’s pairs without the key k.

python.Dict.ofPairs

def Dict.ofPairs (pairs : List (Value * Value)) : List (Value * Value)

A dict from pairs in order (a later pair’s value wins).

python.Dict.keys

def Dict.keys (pairs : List (Value * Value)) : List Value

The keys of the dict’s pairs.

python.Dict.values

def Dict.values (pairs : List (Value * Value)) : List Value

The values of the dict’s pairs.

python.Dict.items

def Dict.items (pairs : List (Value * Value)) : List Value

The dict’s pairs as tuples.

python.Set.has

def Set.has (x : Value) (xs : List Value) : Bool

Whether the value x is among the values xs (by ==, without the heap).

python.Set.remove

def Set.remove (x : Value) (xs : List Value) : List Value

The set’s items xs without the item x.

python.Heap.dict

def Heap.dict (h : Heap) (pairs : List (Value * Value)) : Changed

A new dict from pairs on the heap h.

python.Index.within

def Index.within (i : Int) (size : Nat) : Option Nat

The index i, counted from the end when negative, if it is within the length size.

python.Index.wrongType

def Index.wrongType (h : Heap) (what : String) (i : Value) : Outcome

TypeError for the index i that is not an int, into the sequence named what (its type name read from the heap h).

python.Index.notSubscriptable

def Index.notSubscriptable (h : Heap) (c : Value) : Outcome

TypeError for the value c that cannot be indexed, its type name read from the heap h.

python.Index.item

def Index.item (h : Heap) (what : String) (items : List Value) (i : Value) : Outcome

The item of items at the index i on the heap h, or IndexError (what: the sequence’s name in the message).

python.Containers.listValues

def Containers.listValues (xs : Array Value) : List Value

The list’s items xs (every place in a list holds a value).

python.Index.objectItem

def Index.objectItem (h : Heap) (c : Value) (o : Object) (i : Value) : Outcome

c[i] of the object o that c refers to on the heap h.

python.Index.get

def Index.get (h : Heap) (c : Value) (i : Value) : Outcome

c[i] on the heap h.

python.Index.notAssignable

def Index.notAssignable (h : Heap) (c : Value) : Outcome

TypeError for the value c whose items cannot be assigned, its type name read from the heap h.

python.Index.setObject

def Index.setObject (h : Heap) (c : Value) (a : Nat) (o : Object) (i : Value) (v : Value) : Changed

c[i] = v on the object o that c refers to at the address a on the heap h.

python.Index.set

def Index.set (h : Heap) (c : Value) (i : Value) (v : Value) : Changed

c[i] = v on the heap h.

python.Index.notDeletable

def Index.notDeletable (h : Heap) (c : Value) : Outcome

TypeError for the value c whose items cannot be deleted, its type name read from the heap h (a tuple’s and a str’s message says “doesn’t”, as CPython’s do).

python.Index.deleteObject

def Index.deleteObject (h : Heap) (c : Value) (a : Nat) (o : Object) (i : Value) : Changed

del c[i] on the object o that c refers to at the address a on the heap h: a list’s item at an index (counted from the end when negative), a dict’s key (KeyError when it is not there).

python.Index.delete

def Index.delete (h : Heap) (c : Value) (i : Value) : Changed

del c[i] on the heap h.

python.Slice.bound

def Slice.bound (size : Nat) (up : Bool) (v : Value) (absent : Int) : Int

The slice bound v clamped to a sequence of size items as CPython’s PySlice_AdjustIndices does (counted from the end when negative; up is whether the step is positive); None is the bound’s default absent.

python.Slice.indexesWithin

def Slice.indexesWithin (fuel : Nat) (i : Int) (stop : Int) (step : Int) (up : Bool) : List Nat

The indexes from i toward stop by step (going up when up), within fuel indexes.

python.Slice.indexes

def Slice.indexes (size : Nat) (start : Value) (stop : Value) (step : Int) : List Nat

The indexes the slice from start to stop by step takes from a sequence of size items.

python.Slice.pick

def Slice.pick {A : Type} (xs : List A) (indexes : List Nat) : List A

The items of xs at the indexes.

python.Slice.get

def Slice.get (h : Heap) (c : Value) (start : Value) (stop : Value) (step : Value) : Changed

c[start:stop:step] on the heap h (None bounds and step take their defaults).

python.Containers.noLength

def Containers.noLength (h : Heap) (v : Value) : Outcome

TypeError for the value v without a length, its type name read from the heap h.

python.Object.size

def Object.size (h : Heap) (o : Object) : Option Nat

The number of items in the object o on the heap h, if it has a length.

python.Containers.size

def Containers.size (h : Heap) (v : Value) : Outcome

len(v) on the heap h.

python.Items

data Items

What iterating gives: the values in order, or an exception.

python.Range.values

def Range.values (start : Int) (step : Int) (count : Nat) : List Value

The count values of a range from start by step.

python.Heap.listItems

def Heap.listItems (h : Heap) (v : Value) : Option (List Value)

The values the list v holds now on the heap h (none if it is not a list).

python.Object.items

def Object.items (h : Heap) (o : Object) : Option (List Value)

The values iterating over the object o on the heap h gives, if it can be iterated.

python.Containers.runsCode

def Containers.runsCode (h : Heap) (v : Value) (o : Object) : Bool

Whether iterating over the object o that v refers to on the heap h runs a user’s code or changes its state: a generator, an iterator (taking its items uses it up: python.iterators’s Iterator.drain), or an instance whose class defines __iter__ or __getitem__.

python.Containers.runs

def Containers.runs (h : Heap) (v : Value) : Bool

Whether iterating over the value v on the heap h runs a user’s code or uses up an iterator (Containers.runsCode).

python.Containers.iterate

def Containers.iterate (h : Heap) (v : Value) : Items

Iterating over the value v on the heap h; iterating that runs a user’s code or uses up an iterator is the caller’s, unsupported here.

python.Text.findWithin

def Text.findWithin (fuel : Nat) (k : Nat) (part : Codes) (cs : Codes) : Option Nat

Where part (not empty) first occurs in cs, within fuel steps (k: the position so far).

python.Containers.concatenate

def Containers.concatenate (h : Heap) (a : Value) (b : Value) : Option Changed

a + b for two lists on the heap h (none when a is not a list: another operator’s case).

python.Containers.repeat

def Containers.repeat (n : Int) (xs : List Value) : List Value

The items xs repeated n times (none when n is not positive).

python.Containers.repeatError

def Containers.repeatError (h : Heap) (v : Value) : Outcome

TypeError for repeating a sequence by the value v that is not an int, its type name read from the heap h.

python.Containers.repeatList

def Containers.repeatList (h : Heap) (a : Value) (b : Value) : Option Changed

a * b for a list a or b and a count, on the heap h (none when neither side is a list).

python.Outcome.truth

def Outcome.truth (b : Bool) : Outcome

The bool b produced.

python.Set.same

def Set.same (xs : List Value) (ys : List Value) : Bool

Whether the sets with the items xs and ys have the same items.

python.Contents.fuel

def Contents.fuel : Nat

How deep comparing contents may go.

python.Contents.unsupported

def Contents.unsupported : Outcome

The comparison the model cannot make: a user’s comparison method inside a container.

python.Class.lookup

def Class.lookup (h : Heap) (order : List Value) (name : String) : Option Value

The attribute name along the method resolution order on the heap h, if a class in it defines it.

python.Value.isInstance

def Value.isInstance (h : Heap) (v : Value) : Bool

Whether the value v is an instance of a user’s class on the heap h.

python.Value.defines

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

Whether the value v is an instance on the heap h whose class defines a method name.

python.Value.definesComparison

def Value.definesComparison (h : Heap) (v : Value) : Bool

Whether the class of the value v on the heap h defines a comparison method.

python.Contents.equalOther

def Contents.equalOther (h : Heap) (a : Value) (b : Value) : Option Bool

Equality of the values a and b of different kinds (or a user’s objects) on the heap h: not equal, unless one defines __eq__ (unsupported here: none).

python.Object.isView

def Object.isView (o : Object) : Bool

Whether the object o is a dict’s view.

python.Object.setLike

def Object.setLike (h : Heap) (o : Object) : Option (List Value)

The items of the object o on the heap h if it compares as a set: a set, or a dict’s keys or items view.

python.Contents.equalViews

def Contents.equalViews (h : Heap) (a : Value) (b : Value) (x : Object) (y : Object) : Option Bool

Equality of the objects x and y that a and b refer to on the heap h, where a view takes part: as sets when both compare as sets, else as other objects do.

python.Contents.equal

def Contents.equal (h : Heap) (a : Value) (b : Value) : Outcome

a == b on the heap h as the built-in types decide it (a user’s object, whose methods were tried and declined, is equal only to itself).

python.Contents.has

def Contents.has (h : Heap) (x : Value) (xs : List Value) : Outcome

x in xs for a sequence’s items xs on the heap h: x is y or x == y for some item.

python.Position

data Position

Where an item first equals x: its position, none, or the comparison the model cannot make.

python.Contents.position

def Contents.position (h : Heap) (k : Nat) (x : Value) (xs : List Value) : Position

The first position from k where an item of xs equals x on the heap h.

python.Contents.count

def Contents.count (h : Heap) (x : Value) (xs : List Value) (so : Nat) : Outcome

How many items of xs equal x on the heap h (counted so far: so).

python.Contents.contains

def Contents.contains (h : Heap) (c : Value) (x : Value) : Outcome

x in c on the heap h: a substring for a str, a key for a dict (hashable), an item for anything that can be iterated.

python.Contents.sequence

def Contents.sequence (h : Heap) (v : Value) : Option (Nat * List Value)

A sequence’s kind (0 a list, 1 a tuple) and items, if the value v on the heap h is one.

python.Heap.setItems

def Heap.setItems (h : Heap) (v : Value) : Option (List Value)

A set’s items, if the value v on the heap h is one.

python.Contents.notOrdered

def Contents.notOrdered (h : Heap) (symbol : String) (a : Value) (b : Value) : Outcome

TypeError for the comparison symbol between a and b, whose types have no order (their type names read from the heap h).

python.Contents.setOrder

def Contents.setOrder (symbol : String) (xs : List Value) (ys : List Value) : Bool

The set order symbol between the sets with the items xs and ys: <= is a subset, < a proper subset, >= a superset, > a proper superset.

python.Contents.compareValues

def Contents.compareValues (h : Heap) (symbol : String) (wanted : Int -> Bool) (a : Value) (b : Value) : Outcome

The comparison symbol of a and b, values that are neither sequences nor sets: by their order without the heap (wanted: whether a -1, 0 or 1 makes it true; h only names the types in TypeError).

python.Contents.less

def Contents.less (h : Heap) (a : Value) (b : Value) : Outcome

a < b by contents on the heap h.

python.Contents.greater

def Contents.greater (h : Heap) (a : Value) (b : Value) : Outcome

a > b by contents on the heap h.

python.Sorted

data Sorted

What sorting gives: the values in order, or the exception a comparison raised.

python.SortedBy

data SortedBy (A : Type)

What sorting items by keys gives: the items in order, or the exception a comparison raised.

python.SortedBy.prepend

def SortedBy.prepend {A : Type} (x : A) (r : SortedBy A) : SortedBy A

The item x put before the sorted result r.

python.Contents.before

def Contents.before (h : Heap) (b : Value) (a : Value) : Option Raised * Bool

Whether b sorts before a on the heap h: b < a (none with the exception when the comparison raises).

python.Contents.mergeBy

def Contents.mergeBy {A : Type} (h : Heap) (key : A -> Value) (fuel : Nat) (xs : List A) (ys : List A) : SortedBy A

Merging the lists xs and ys, sorted by their items’ key, on the heap h within fuel steps (an item of ys goes first only when its key is less: stable).

python.Contents.mergeSortBy

def Contents.mergeSortBy {A : Type} (h : Heap) (key : A -> Value) (fuel : Nat) (xs : List A) : SortedBy A

A merge sort of xs by the items’ key on the heap h, within fuel halvings.

python.Contents.flip

def Contents.flip {A : Type} (i : Nat) (j : Nat) (xs : List A) : List A

The list xs with its items from position i up to j reversed.

python.Contents.moved

def Contents.moved {A : Type} (at : Nat) (ok : Nat) (moving : A) (xs : List A) : List A

The list xs with the item moving at position ok moved to position at (the ones between moved up one).

python.Contents.lessBy

def Contents.lessBy {A : Type} (h : Heap) (key : A -> Value) (x : A) (y : A) : Either Raised Bool

Whether the key of x is less than the key of y by the built-in order on the heap h, or the exception comparing them raised.

python.Contents.lessAt

def Contents.lessAt {A : Type} (h : Heap) (key : A -> Value) (xs : List A) (i : Nat) (j : Nat) : Either (Raised * List A) Bool

Whether the item of xs at i is less than the one at j by their key on the heap h (false past the end); a failure keeps the items as they are.

python.Contents.ascendFrom

def Contents.ascendFrom {A : Type} (h : Heap) (key : A -> Value) (fuel : Nat) (xs : List A) (n : Nat) (count : Nat) : Either (Raised * List A) Nat

count_run‘s ascending stretch of xs from n, by the items’ key on the heap h within fuel steps: the first n whose item is less than the one before (or the count of items).

python.Contents.lastEqual

def Contents.lastEqual {A : Type} (xs : List A) (n : Nat) (neq : Nat) : List A

REVERSE_LAST_NEQ: xs with the last stretch of equal items before n (neq after the first) reversed.

python.Contents.descendFrom

def Contents.descendFrom {A : Type} (h : Heap) (key : A -> Value) (fuel : Nat) (xs : List A) (n : Nat) (neq : Nat) (count : Nat) : Either (Raised * List A) (List A * (Nat * Nat))

count_run‘s descending stretch of xs from n (neq equal items so far), by the items’ key on the heap h within fuel steps, among count items: the items with each finished stretch of equal ones reversed, where it ends, and the equal ones still open.

python.Contents.descending

def Contents.descending {A : Type} (h : Heap) (key : A -> Value) (xs : List A) (n : Nat) (count : Nat) : Either (Raised * List A) (List A * Nat)

count_run on the count items xs from a descending start at n, by their key on the heap h: the stretch, its last equal items reversed, the whole run reversed, then extended by an ascending stretch.

python.Contents.countRun

def Contents.countRun {A : Type} (h : Heap) (key : A -> Value) (xs : List A) (count : Nat) : Either (Raised * List A) (List A * Nat)

count_run (CPython’s listsort) on the count items xs by their key on the heap h: the items with the run at the start ascending, and its length.

python.Contents.searchFrom

def Contents.searchFrom {A : Type} (h : Heap) (key : A -> Value) (fuel : Nat) (xs : List A) (pivot : A) (low : Nat) (high : Nat) : Either (Raised * List A) Nat

binarysort‘s search in xs by the items’ key on the heap h, within fuel halvings: where the pivot belongs between low and high (pivot < a[M] halving).

python.Contents.insertFrom

def Contents.insertFrom {A : Type} (h : Heap) (key : A -> Value) (fuel : Nat) (xs : List A) (ok : Nat) (count : Nat) : Either (Raised * List A) (List A)

binarysort of the count items xs from ok (the items before it sorted), by their key on the heap h within fuel steps: each next item moved where it belongs among those before it.

python.Contents.shortSort

def Contents.shortSort {A : Type} (h : Heap) (key : A -> Value) (xs : List A) : Option Raised * List A

The items xs (fewer than 64) sorted by their key on the heap h as CPython’s listsort does (one run: count_run then binarysort), so a comparison that raises is the one CPython makes first: the items sorted, or as far as the sorting got, with the exception.

python.Contents.sortPartly

def Contents.sortPartly {A : Type} (h : Heap) (key : A -> Value) (reversed : Bool) (xs : List A) : Option Raised * List A

The items xs sorted by their key on the heap h, with the exception a comparison raised (the items then as far as the sorting got, as CPython’s list.sort leaves them): fewer than 64 as CPython compares them (Contents.shortSort); more by a stable merge sort, which gives the same order, but a comparison that raises there is not taken (CPython may compare another pair first). When reversed, CPython reverses, sorts and reverses again (after a failure too), so items with equal keys keep their order.

python.Contents.sortBy

def Contents.sortBy {A : Type} (h : Heap) (key : A -> Value) (reversed : Bool) (xs : List A) : SortedBy A

The items xs sorted by their key on the heap h (descending when reversed), or the exception a comparison raised (Contents.sortPartly).

python.Contents.itself

def Contents.itself (v : Value) : Value

The value v as its own key.

python.Contents.sort

def Contents.sort (h : Heap) (reversed : Bool) (xs : List Value) : Sorted

sorted(xs) on the heap h: the values sorted by themselves (descending when reversed).