Define a sorting function for a given comparator.

Defsort creates a relatively-high-performance sorting function for a given comparison function, and proves that its output is an ordered (with respect to the comparison function) permutation of the input list. It is currently implemented as a mergesort on lists with some fixnum optimizations.

It also may optionally prove the generated mergesort function equivalent to
an insertion sort; this requires some extra properties to be proved about the
comparison function beforehand; see the discussion of

These forms show various ways of invoking defsort:

(defsort sort-by-foo< :prefix foosort :compare< foo< :comparablep foo-p :comparable-listp foolist-p :true-listp nil :weak t) (defsort :comparablep rationalp :compare< < :prefix < :comparable-listp rational-listp :true-listp t :weak nil) (defsort intalist-sort :extra-args (alist) :extra-args-guard (intalistp alist) :compare< intalist-< :comparablep (lambda (x alist) (consp (assoc-equal x alist)))) (defsort intalist-sort2 (x alist) :extra-args-guard (intalistp alist) :compare< intalist2-< :comparablep (lambda (x alist) (stringp x)))

The first form is a new syntax that gives the name of the sorting function
explicitly; it is also good for etags generation since it is of the form

The second form shows an older syntax in which the sort name is omitted and
every function name is generated from the prefix, so the name of the sorting
function will in this case be

The third form shows the use of

The fourth form shows a different syntax for specifying extra-args by giving a formals list before the keyword arguments, which looks a bit nicer. (Note: In this syntax the first formal must be the symbol X, although it can be in any package.) Additionally, it shows how to use extra-args in conjunction with a comparablep predicate that doesn't use them.

:compare< gives the function to use to compare elements; this may be a binary function name or a lambda such as(lambda (x y) (< y x)) . Defsort needs to prove that this is a transitive relation.:prefix defaults to the sort name when it is provided, but otherwise is required. It is used to generate function and theorem names.:comparablep gives the type of element to be compared. The comparison function's guards should be satisfied by any two elements that both satisfy this predicate. This may be a unary function symbol or lambda. If it is omitted, then it is treated as(lambda (x) t) , i.e. all objects are comparable.:comparable-listp gives the name of a function that recognizes a list of comparable elements. This may be omitted, in which case such a function will be defined (named<prefix>-list-p ).:true-listp defaults to NIL and determines whether the comparable-listp function requires the final cdr to be NIL. If an existing:comparable-listp function name is provided, then the value of:true-listp must correspond to that function; i.e. true-listp must be true iff the comparable-listp function requires the final cdr to be nil. If:comparable-listp is not provided, then the comparable-listp function will be generated so that this is true.:weak defaults to NIL in the new syntax and T in the old syntax, for historical reasons. When:weak is NIL, defsort will introduce a simple insertion sort function in addition to the optimized mergesort, and prove the two equivalent. To do this, it needs a couple of extra facts about the comparison function, in addition to its transitivity: its negation must also be a transitive relation, and it must be strict, i.e.,(not (compare< x x)) .:extra-args may be a list of variables that are used as extra parameters to all the functions involved. (If some of your functions don't require all the arguments, you must wrap them in a lambda in order to accept the right arguments.) When using the new syntax with a formals list, extra-args is not accepted since the formals list already specifies them.:extra-args-guard may be a term giving a guard that will be required of the extra-args.

Defsort allows you to specify a lambda rather than a function for most
arguments, and doesn't require that (e.g.) the

There may also be some bad cases when the setting of

- Alphanum-sort
- Sorts lists using alphanumeric comparison.