1(* ========================================================================= *) 2(* KNUTH-BENDIX TERM ORDERING CONSTRAINTS *) 3(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *) 4(* ========================================================================= *) 5 6structure KnuthBendixOrder :> KnuthBendixOrder = 7struct 8 9open Useful; 10 11(* ------------------------------------------------------------------------- *) 12(* Helper functions. *) 13(* ------------------------------------------------------------------------- *) 14 15fun notEqualTerm (x,y) = not (Term.equal x y); 16 17fun firstNotEqualTerm f l = 18 case List.find notEqualTerm l of 19 SOME (x,y) => f x y 20 | NONE => raise Bug "firstNotEqualTerm"; 21 22(* ------------------------------------------------------------------------- *) 23(* The weight of all constants must be at least 1, and there must be at most *) 24(* one unary function with weight 0. *) 25(* ------------------------------------------------------------------------- *) 26 27type kbo = 28 {weight : Term.function -> int, 29 precedence : Term.function * Term.function -> order}; 30 31(* Default weight = uniform *) 32 33val uniformWeight : Term.function -> int = K 1; 34 35(* Default precedence = by arity *) 36 37val arityPrecedence : Term.function * Term.function -> order = 38 fn ((f1,n1),(f2,n2)) => 39 case Int.compare (n1,n2) of 40 LESS => LESS 41 | EQUAL => Name.compare (f1,f2) 42 | GREATER => GREATER; 43 44(* The default order *) 45 46val default = {weight = uniformWeight, precedence = arityPrecedence}; 47 48(* ------------------------------------------------------------------------- *) 49(* Term weight-1 represented as a linear function of the weight-1 of the *) 50(* variables in the term (plus a constant). *) 51(* *) 52(* Note that the conditions on weight functions ensure that all weights are *) 53(* at least 1, so all weight-1s are at least 0. *) 54(* ------------------------------------------------------------------------- *) 55 56datatype weight = Weight of int NameMap.map * int; 57 58val weightEmpty : int NameMap.map = NameMap.new (); 59 60val weightZero = Weight (weightEmpty,0); 61 62fun weightIsZero (Weight (m,c)) = c = 0 andalso NameMap.null m; 63 64fun weightNeg (Weight (m,c)) = Weight (NameMap.transform ~ m, ~c); 65 66local 67 fun add ((_,n1),(_,n2)) = 68 let 69 val n = n1 + n2 70 in 71 if n = 0 then NONE else SOME n 72 end; 73in 74 fun weightAdd (Weight (m1,c1)) (Weight (m2,c2)) = 75 Weight (NameMap.union add m1 m2, c1 + c2); 76end; 77 78fun weightSubtract w1 w2 = weightAdd w1 (weightNeg w2); 79 80fun weightTerm weight = 81 let 82 fun wt m c [] = Weight (m,c) 83 | wt m c (Term.Var v :: tms) = 84 let 85 val n = Option.getOpt (NameMap.peek m v, 0) 86 in 87 wt (NameMap.insert m (v, n + 1)) (c + 1) tms 88 end 89 | wt m c (Term.Fn (f,a) :: tms) = 90 wt m (c + weight (f, length a)) (a @ tms) 91 in 92 fn tm => wt weightEmpty ~1 [tm] 93 end; 94 95fun weightLowerBound (w as Weight (m,c)) = 96 if NameMap.exists (fn (_,n) => n < 0) m then NONE else SOME c; 97 98(*MetisDebug 99val ppWeightList = 100 let 101 fun ppCoeff n = 102 if n < 0 then Print.sequence (Print.ppString "~") (ppCoeff (~n)) 103 else if n = 1 then Print.skip 104 else Print.ppInt n 105 106 fun pp_tm (NONE,n) = Print.ppInt n 107 | pp_tm (SOME v, n) = Print.sequence (ppCoeff n) (Name.pp v) 108 in 109 fn [] => Print.ppInt 0 110 | tms => Print.ppOpList " +" pp_tm tms 111 end; 112 113fun ppWeight (Weight (m,c)) = 114 let 115 val l = NameMap.toList m 116 val l = List.map (fn (v,n) => (SOME v, n)) l 117 val l = if c = 0 then l else l @ [(NONE,c)] 118 in 119 ppWeightList l 120 end; 121 122val weightToString = Print.toString ppWeight; 123*) 124 125(* ------------------------------------------------------------------------- *) 126(* The Knuth-Bendix term order. *) 127(* ------------------------------------------------------------------------- *) 128 129fun compare {weight,precedence} = 130 let 131 fun weightDifference tm1 tm2 = 132 let 133 val w1 = weightTerm weight tm1 134 and w2 = weightTerm weight tm2 135 in 136 weightSubtract w2 w1 137 end 138 139 fun weightLess tm1 tm2 = 140 let 141 val w = weightDifference tm1 tm2 142 in 143 if weightIsZero w then precedenceLess tm1 tm2 144 else weightDiffLess w tm1 tm2 145 end 146 147 and weightDiffLess w tm1 tm2 = 148 case weightLowerBound w of 149 NONE => false 150 | SOME 0 => precedenceLess tm1 tm2 151 | SOME n => n > 0 152 153 and precedenceLess (Term.Fn (f1,a1)) (Term.Fn (f2,a2)) = 154 (case precedence ((f1, length a1), (f2, length a2)) of 155 LESS => true 156 | EQUAL => firstNotEqualTerm weightLess (zip a1 a2) 157 | GREATER => false) 158 | precedenceLess _ _ = false 159 160 fun weightDiffGreater w tm1 tm2 = weightDiffLess (weightNeg w) tm2 tm1 161 162 fun weightCmp tm1 tm2 = 163 let 164 val w = weightDifference tm1 tm2 165 in 166 if weightIsZero w then precedenceCmp tm1 tm2 167 else if weightDiffLess w tm1 tm2 then SOME LESS 168 else if weightDiffGreater w tm1 tm2 then SOME GREATER 169 else NONE 170 end 171 172 and precedenceCmp (Term.Fn (f1,a1)) (Term.Fn (f2,a2)) = 173 (case precedence ((f1, length a1), (f2, length a2)) of 174 LESS => SOME LESS 175 | EQUAL => firstNotEqualTerm weightCmp (zip a1 a2) 176 | GREATER => SOME GREATER) 177 | precedenceCmp _ _ = raise Bug "kboOrder.precendenceCmp" 178 in 179 fn (tm1,tm2) => 180 if Term.equal tm1 tm2 then SOME EQUAL else weightCmp tm1 tm2 181 end; 182 183(*MetisTrace7 184val compare = fn kbo => fn (tm1,tm2) => 185 let 186 val () = Print.trace Term.pp "KnuthBendixOrder.compare: tm1" tm1 187 val () = Print.trace Term.pp "KnuthBendixOrder.compare: tm2" tm2 188 val result = compare kbo (tm1,tm2) 189 val () = 190 case result of 191 NONE => trace "KnuthBendixOrder.compare: result = Incomparable\n" 192 | SOME x => 193 Print.trace Print.ppOrder "KnuthBendixOrder.compare: result" x 194 in 195 result 196 end; 197*) 198 199end 200