1signature AC_Sort =
2sig
3
4  include Abbrev
5  val sort : {assoc : thm, comm : thm,
6              dest : term -> term * term, mk : term * term -> term,
7              cmp : term * term -> order,
8              combine : conv, preprocess : conv} -> conv
9
10end
11
12(*
13
14   [sort {assoc,comm,dest,mk,cmp,combine,preprocess}] is a conversion for
15   sorting terms with respect to an associative and commutative operator.
16   It uses a merge sort internally, so should be reasonably efficient.
17
18   The record's fields are:
19
20     assoc:      associativity theorem in standard r-to-l format:
21                  a + (b + c) = (a + b) + c
22                 can be universally quantified
23
24     comm:       commutativity theorem (can be universally quantified)
25
26     dest:       destructor function for operator
27
28     mk:         constructor function for operator
29
30     cmp:        comparison function for performing sort.  Terms identified
31                 as EQUAL will be combined by combine conversion.
32
33     combine:    conv taking terms of the form (t1 op t2) where t1 and t2
34                 have compared as equal.  Should always succeed (can be
35                 ALL_CONV).
36
37     preprocess: applied to all leaf terms as term is first examined.
38                 If it fails or raises UNCHANGED (i.e., both ALL_CONV and
39                 NO_CONV are OK here), nothing further is done.  If it
40                 succeeds, further processing is performed on the resulting
41                 term
42
43    E.g., combine can combine numeric literals; preprocess could convert
44    a - b into a + -b, or -x into -1 * x, or ~~p into p.
45
46*)
47