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