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