Defsort
Define a sorting function for a given comparator.
NOTE: Defsort's interface has a greater than average likelihood of
changing incompatibly in the future.
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 :weak below.
Usage
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
(def... name ...). In the first form, the prefix is optional; if it is
not provided, the sort name will be used as the prefix for generating other
function names.
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 <-sort.
The third form shows the use of :extra-args to define a parameterized
sort.
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.
Keyword Arguments
- :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.
Troubleshooting
Defsort allows you to specify a lambda rather than a function for most
arguments, and doesn't require that (e.g.) the :extra-args-guard be just a
function call. But things may break if you use, e.g., a lambda containing an
IF (or AND or OR) as, say, the comparablep predicate. It is best for
everything to be a simple function call.
There may also be some bad cases when the setting of :comparablep is a
built-in function that ACL2 treats specially or that is in minimal-theory.
For example, :comparablep atom used to cause defsort to fail, though now
it has a special hack for that particular case.
Subtopics
- Alphanum-sort
- Sorts lists using alphanumeric comparison.
