rocq/backend/Order.v
Prolog's standard order of terms, and the sorted lists the Prolog compiler makes with it: sort/2, msort/2 and the ordsets of library(ordsets). The backend's plans list temporaries, live ranges and thunks in this order, so the Gallina backend sorts by it too.
For the ground terms of Term.v the order is: integers by value, then [ ], then atoms by character code, then compounds, by arity, then by name, then by their arguments from the left. A list that is not empty is the compound '[|]'(Head, Tail).
Comparing
The order of two atoms' names: by character code, a prefix first. Extract.v makes it OCaml's comparison of strings.
As compare(Order, T, U): the standard order of the terms t and u.
Sorting
The merges below take one element off one list or both at each step, so the two lengths together are steps enough. Each is one function over that count, not a function of xs holding another of ys, so that its C++ extraction is a loop: a merge of two long lists would otherwise be as deep as they are long.
merge in at most n steps.
The sorted lists xs and ys merged; of two equal elements, xs's comes first.
A merge sort's stack of sorted runs: the run at depth i, if there is one, has 2^i elements.
The runs of a stack merged, the oldest first.
As msort(Xs, Sorted): xs in the order of cmp, equal elements in the order they had (a merge sort, as SWI-Prolog's is).
A sorted list with one element of each run of equal ones.
As sort(Xs, Sorted): xs sorted, without duplicates. Its results are ordsets.
ord_union in at most n steps.
As ord_union(Xs, Ys, Zs): the union of two ordsets.
ord_subtract in at most n steps.
As ord_subtract(Xs, Ys, Zs): the elements of the ordset xs that are not in the ordset ys.
ord_intersection in at most n steps.
As ord_intersection(Xs, Ys, Zs): the elements of the ordset xs that are in the ordset ys too.
As ord_memberchk(X, Xs): whether x is in the ordset xs.
Whether two ordsets of names are the same.