sorting

python.SortPlaces

record SortPlaces

The places sorting uses: the list of pairs, its length, the indexes, the pivot, the operands and the truth of a comparison.

python.Sorting.at

def Sorting.at (s : Run) (p : Place) : Nat

The natural number kept in the place p in the run s.

python.Sorting.index

def Sorting.index (p : Place) : Run -> Nat

The natural number in the place p, read from the run.

python.Sorting.zero

def Sorting.zero : Run -> Nat

Zero, for any run.

python.Sorting.put

def Sorting.put (p : Place) (f : Run -> Nat) : Code

The natural number f reads from the run, put in the place p.

python.Sorting.nth

def Sorting.nth (xs : List Value) (k : Nat) : Value

The value at the position k of the list xs (None past its end).

python.Sorting.keyOf

def Sorting.keyOf (pair : Value) : Value

A pair’s key.

python.Sorting.itemOf

def Sorting.itemOf (pair : Value) : Value

A pair’s item.

python.Sorting.pairAt

def Sorting.pairAt (s : Run) (ps : SortPlaces) (k : Nat) : Value

The pair at the position k in the run s, with the sorting places ps.

python.Sorting.key

def Sorting.key (s : Run) (ps : SortPlaces) (k : Nat) : Value

The key of the pair at the position k in the run s, with the sorting places ps.

python.Sorting.change

def Sorting.change (node : String) (ps : SortPlaces) (f : Run -> List Value -> List Value) : Code

The pairs (in the sorting places ps) changed by the function f of the run and them, at node.

python.Sorting.reversed

def Sorting.reversed (node : String) (ps : SortPlaces) (i : Run -> Nat) (j : Run -> Nat) : Code

The pairs (in the sorting places ps) from the position i up to j reversed, at node.

python.Sorting.compared

def Sorting.compared (node : String) (functions : List Function) (bodies : Nat -> Code) (ps : SortPlaces) (method : String) (reflected : String) (symbol : String) (x : Run -> Value) (y : Run -> Value) : Code

The truth of the comparison x symbol y of keys read from the run (its method, the reflected one, the built-in order), in the truth place of ps, at node with the program’s functions and their bodies.

python.Sorting.less

def Sorting.less (node : String) (functions : List Function) (bodies : Nat -> Code) (ps : SortPlaces) (x : Run -> Value) (y : Run -> Value) : Code

The truth of x < y (the user’s __lt__, or the reflected __gt__), in the truth place of ps, at node with the program’s functions and their bodies.

python.Sorting.greater

def Sorting.greater (node : String) (functions : List Function) (bodies : Nat -> Code) (ps : SortPlaces) (x : Run -> Value) (y : Run -> Value) : Code

The truth of x > y (the user’s __gt__, or the reflected __lt__), in the truth place of ps, at node with the program’s functions and their bodies.

python.Sorting.up

def Sorting.up (p : Place) : Code

The index place p one up.

python.Sorting.within

def Sorting.within (ps : SortPlaces) (s : Run) : Checked Stop Bool

Whether n (in the sorting places ps) is before the end in the run s.

python.Sorting.next

def Sorting.next (ps : SortPlaces) (s : Run) : Value

The key at n (in the sorting places ps) in the run s.

python.Sorting.previous

def Sorting.previous (ps : SortPlaces) (s : Run) : Value

The key before n (in the sorting places ps) in the run s.

python.Sorting.ascending

def Sorting.ascending (node : String) (functions : List Function) (bodies : Nat -> Code) (ps : SortPlaces) : Code

count_run’s ascending stretch from n (in the sorting places ps): while the next key is not less than the one before; at node with the program’s functions and their bodies.

python.Sorting.lastEqual

def Sorting.lastEqual (node : String) (ps : SortPlaces) : Code

REVERSE_LAST_NEQ at node: the last stretch of equal keys (neq of the sorting places ps after the first) reversed, neq back to 0.

python.Sorting.descending

def Sorting.descending (node : String) (functions : List Function) (bodies : Nat -> Code) (ps : SortPlaces) : Code

count_run’s descending stretch from n (in the sorting places ps): a next key less than the one before ends a stretch of equal keys; one greater ends the run; else it is equal to it. At node with the program’s functions and their bodies.

python.Sorting.countRun

def Sorting.countRun (node : String) (functions : List Function) (bodies : Nat -> Code) (ps : SortPlaces) : Code

count_run: the length of the run at the start in run of the sorting places ps (a descending one reversed into an ascending one); at node with the program’s functions and their bodies.

python.Sorting.binarySort

def Sorting.binarySort (node : String) (functions : List Function) (bodies : Nat -> Code) (ps : SortPlaces) : Code

binarysort from ok of the sorting places ps (the run before it sorted): each next pair put where its key belongs among those before it, found by halving (pivot < a[M]); at node with the program’s functions and their bodies.

python.Sorting.sort

def Sorting.sort (node : String) (functions : List Function) (bodies : Nat -> Code) (ps : SortPlaces) (backward : Run -> Bool) : Code

The pairs in the sorting places ps sorted by their keys, as CPython’s listsort does for fewer than 64 (backward: reversed first and after, so equal keys keep their order); at node with the program’s functions and their bodies.

python.Sorting.best

def Sorting.best (node : String) (functions : List Function) (bodies : Nat -> Code) (ps : SortPlaces) (isMax : Bool) : Code

min (the first least key: key < best) or max (isMax, the first greatest: key > best) of the pairs in the sorting places ps (there is one at least): its position in run; at node with the program’s functions and their bodies.

python.Sorting.names

def Sorting.names : List String

The model’s own functions for sorting, after the program’s functions and the built-in generators in the table: model sort (the pairs, whether reversed) sorts the list of pairs; model extreme (the pairs, whether max) returns the item of the best key. Their statements are in the table once, not at every call; their frames do not count toward the recursion limit (Function.internal).

python.Sorting.frame

def Sorting.frame : SortPlaces

The kept places of a sorting frame: the two arguments first, then the places sorting uses, then a scratch slot.

python.Sorting.slots

def Sorting.slots : Nat

How many locals a sorting frame has.

python.Sorting.functions

def Sorting.functions : List Function

The sorting functions as table entries.

python.Sorting.body

def Sorting.body (k : Nat) (functions : List Function) (bodies : Nat -> Code) : Code

The body of the sorting function at the position k among them, with the program’s functions and their bodies.

python.Sorting.called

def Sorting.called (node : String) (functions : List Function) (bodies : Nat -> Code) (name : String) (arguments : List Expression) (result : Place) : Code

A call of the sorting function name on the arguments at node, its result into the place result, with the program’s functions and their bodies.

python.Sorting.paired

def Sorting.paired (node : String) (keys : Place) (items : Place) (pairs : Place) : Code

Pairs of the keys and items in two lists (in places), into a new list in the place pairs, at node.

python.Sorting.itemsOf

def Sorting.itemsOf (s : Run) (pairs : Place) : List Value

The items of the list of pairs in the place pairs in the run s, in order.

python.Sorting.user

def Sorting.user (s : Run) (keys : Place) : Bool

Whether one of the keys (a list in a place) in the run s defines comparison methods (a user’s code compares it).

python.Sorting.byKeys

def Sorting.byKeys (node : String) (functions : List Function) (bodies : Nat -> Code) (pairs : Place) (items : Place) (keys : Place) (reversed : Option Place) (result : Place) : Code

The items sorted by their keys (lists in places; the items themselves for no key function), reversed when that place holds true, into a new list in result: by the user’s comparisons when a key defines them (model sort, the pairs made in the place pairs), else the built-in’s. At node with the program’s functions and their bodies.

python.Sorting.extremeByKeys

def Sorting.extremeByKeys (node : String) (functions : List Function) (bodies : Nat -> Code) (pairs : Place) (name : String) (items : Place) (keys : Place) (fallback : Option Place) (result : Place) : Code

min or max (the name) of the items by their keys (lists in places) into result: by the user’s comparisons when a key defines them (model extreme, the pairs made in the place pairs; ValueError, or the default in fallback, for none), else the built-in’s. At node with the program’s functions and their bodies.

python.Sorting.keyed

def Sorting.keyed (s : Run) (key : Option Place) : Bool

Whether a key function was given in the run s (the place key, with a value that is not None).

python.Sorting.listSort

def Sorting.listSort (node : String) (functions : List Function) (bodies : Nat -> Code) (pairs : Place) (receiver : Place) (key : Option Place) (reversed : Option Place) (saved : Place) (keys : Place) (sorted : Place) (iterator : Place) (item : Place) (ended : Place) (trying : Place) (guard : Place) (flag : Place) (result : Place) : Code

xs.sort(key=f, reverse=r) on the list in receiver, with key and reversed the places of f and r, as CPython’s list.sort: the list empty while its keys are computed and it is sorted (Sorting.byKeys); ValueError when the key function or a comparison changed it (the list then has the sorted items); after an exception the list has its items in the order the sorting had left them. The keys are the items themselves without a key function. At node with the program’s functions and their bodies; the places: saved the items copied out, keys their keys, pairs the pairs, sorted the sorted items, iterator, item, ended and trying for computing the keys, guard for the try around it, flag whether the list was changed, and result the None it returns.