iterators

python.Iterator.make

def Iterator.make (h : Heap) (walk : Iterating) (position : Nat) : Changed

A new iterator on the heap h, walking walk from position.

python.Iterator.textKind

def Iterator.textKind (cs : Codes) : Codes

An iterator’s type name for a str of the code points cs: str_ascii_iterator when every one is ASCII.

python.Iterator.viewKind

def Iterator.viewKind (kind : Codes) : Codes

A dict view’s iterator type name, by the view’s own type name kind: dict_keyiterator, dict_valueiterator, dict_itemiterator.

python.Iterator.cannotIterate

def Iterator.cannotIterate (h : Heap) (v : Value) : Raised

TypeError: v cannot be iterated (its type name read from the heap h).

python.Iterator.ofObject

def Iterator.ofObject (h : Heap) (v : Value) (a : Nat) (o : Object) : Changed

iter(v) of the object o at the address a on the heap h.

python.Iterator.of

def Iterator.of (h : Heap) (v : Value) : Changed

iter(v) on the heap h: an iterator over a str, tuple, range, list, dict, set or dict view; an iterator itself.

python.Advance

data Advance

What taking the next item gives: the heap and the item, the heap and the end, or the heap and an exception.

python.Iterator.moved

def Iterator.moved (h : Heap) (a : Nat) (walk : Iterating) (position : Nat) (v : Value) : Advance

The iterator at the address a on the heap h, walking walk, moved to position, giving the item v.

python.Iterator.ended

def Iterator.ended (h : Heap) (a : Nat) (walk : Iterating) : Advance

The iterator at the address a on the heap h, walking walk, run out: it stays out (a list’s iterator forgets the list, as CPython’s does).

python.Iterator.nextInList

def Iterator.nextInList (h : Heap) (a : Nat) (walk : Iterating) (list : Nat) (position : Nat) : Advance

The next item of the list at the address list (forward), as it is now on the heap h, for the iterator at a walking walk at position.

python.Iterator.nextBackward

def Iterator.nextBackward (h : Heap) (a : Nat) (walk : Iterating) (list : Nat) (position : Nat) : Advance

The next item of the list at the address list walked backward, for the iterator at a on the heap h walking walk: position counts down from the list’s length when it began.

python.Iterator.nextInDict

def Iterator.nextInDict (h : Heap) (a : Nat) (walk : Iterating) (kind : Codes) (dict : Nat) (size : Nat) (keys : List Value) (position : Nat) : Advance

The next item of the dict at the address dict (its keys, values or items by the iterator’s kind) at position, for the iterator at a on the heap h walking walk: RuntimeError when it no longer has size entries, unsupported when its keys are no longer keys though the size is the same.

python.Iterator.slotFrom

def Iterator.slotFrom (slots : List Slot) (k : Nat) : Option (Value * Nat)

The first filled slot of slots, the first of which is at position k, and the position after it.

python.Iterator.nextInSet

def Iterator.nextInSet (h : Heap) (a : Nat) (walk : Iterating) (set : Nat) (size : Nat) (position : Nat) : Advance

The next item of the set at the address set, in its table’s slot order (position is a slot), for the iterator at a on the heap h walking walk: RuntimeError when it no longer has size items.

python.Iterator.step

def Iterator.step (fuel : Nat) (h : Heap) (a : Nat) (walk : Iterating) (position : Nat) : Advance

The next item of the iterator at the address a on the heap h, walking walk at position, within fuel levels of iterators inside (enumerate, zip).

python.Iterator.nextWithin

def Iterator.nextWithin (fuel : Nat) (h : Heap) (it : Value) : Advance

The next item of the iterator it on the heap h, within fuel levels; TypeError for a value that is not an iterator, unsupported for a generator (it runs the user’s code).

python.Iterator.fuel

def Iterator.fuel : Nat

How deep iterators inside iterators may go.

python.Iterator.next

def Iterator.next (h : Heap) (it : Value) : Advance

next(it) on the heap h.

python.Iterator.before

def Iterator.before (i : Nat) : String

The names of the arguments before argument i of zip: “1” or “1-k”.

python.Iterator.nextZip

def Iterator.nextZip (fuel : Nat) (h : Heap) (a : Nat) (walk : Iterating) (inners : List Value) (strict : Bool) : Advance

The next item of the zip at the address a on the heap h, walking walk: an item from each of the iterators inners in turn, within fuel levels; the end at the first that runs out (when strict: ValueError naming the shorter argument, or the longer one when the first runs out and a later one does not).

python.Iterator.takeEach

def Iterator.takeEach (fuel : Nat) (h : Heap) (inners : List Value) (so : List Value) : Heap * Either Raised (Either Nat (List Value))

An item from each of the iterators inners in turn on the heap h, within fuel levels, after the items so far: the items, or the position of the first that ran out, or an exception.

python.Iterator.checkLonger

def Iterator.checkLonger (fuel : Nat) (h : Heap) (rest : List Value) (k : Nat) : Advance

After the first iterator of a strict zip ran out: ValueError when one of the later iterators rest still gives an item, on the heap h within fuel levels; k counts the arguments before the first of rest.

python.Taken

data Taken

What taking every remaining item gives: the heap after and the items (or the exception).

python.Iterator.drainWithin

def Iterator.drainWithin (fuel : Nat) (h : Heap) (it : Value) (so : List Value) : Taken

Taking the next items of the iterator it on the heap h until it runs out, within fuel items, after the items so far (the latest first).

python.Iterator.is

def Iterator.is (h : Heap) (v : Value) : Bool

Whether v is an iterator object on the heap h.

python.Iterator.limit

def Iterator.limit : Nat

The most items taking from an iterator goes through (the model’s memory, as for repeating a sequence).

python.Iterator.take

def Iterator.take (h : Heap) (v : Value) : Taken

Every item of the iterable v on the heap h, using an iterator up (what list(), sum(), str.join and the others do).