--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/KnuthBendixOrder.sml Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,199 @@
+(* ========================================================================= *)
+(* KNUTH-BENDIX TERM ORDERING CONSTRAINTS *)
+(* Copyright (c) 2002-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure KnuthBendixOrder :> KnuthBendixOrder =
+struct
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* Helper functions. *)
+(* ------------------------------------------------------------------------- *)
+
+fun notEqualTerm (x,y) = not (Term.equal x y);
+
+fun firstNotEqualTerm f l =
+ case List.find notEqualTerm l of
+ SOME (x,y) => f x y
+ | NONE => raise Bug "firstNotEqualTerm";
+
+(* ------------------------------------------------------------------------- *)
+(* The weight of all constants must be at least 1, and there must be at most *)
+(* one unary function with weight 0. *)
+(* ------------------------------------------------------------------------- *)
+
+type kbo =
+ {weight : Term.function -> int,
+ precedence : Term.function * Term.function -> order};
+
+(* Default weight = uniform *)
+
+val uniformWeight : Term.function -> int = K 1;
+
+(* Default precedence = by arity *)
+
+val arityPrecedence : Term.function * Term.function -> order =
+ fn ((f1,n1),(f2,n2)) =>
+ case Int.compare (n1,n2) of
+ LESS => LESS
+ | EQUAL => Name.compare (f1,f2)
+ | GREATER => GREATER;
+
+(* The default order *)
+
+val default = {weight = uniformWeight, precedence = arityPrecedence};
+
+(* ------------------------------------------------------------------------- *)
+(* Term weight-1 represented as a linear function of the weight-1 of the *)
+(* variables in the term (plus a constant). *)
+(* *)
+(* Note that the conditions on weight functions ensure that all weights are *)
+(* at least 1, so all weight-1s are at least 0. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype weight = Weight of int NameMap.map * int;
+
+val weightEmpty : int NameMap.map = NameMap.new ();
+
+val weightZero = Weight (weightEmpty,0);
+
+fun weightIsZero (Weight (m,c)) = c = 0 andalso NameMap.null m;
+
+fun weightNeg (Weight (m,c)) = Weight (NameMap.transform ~ m, ~c);
+
+local
+ fun add ((_,n1),(_,n2)) =
+ let
+ val n = n1 + n2
+ in
+ if n = 0 then NONE else SOME n
+ end;
+in
+ fun weightAdd (Weight (m1,c1)) (Weight (m2,c2)) =
+ Weight (NameMap.union add m1 m2, c1 + c2);
+end;
+
+fun weightSubtract w1 w2 = weightAdd w1 (weightNeg w2);
+
+fun weightTerm weight =
+ let
+ fun wt m c [] = Weight (m,c)
+ | wt m c (Term.Var v :: tms) =
+ let
+ val n = Option.getOpt (NameMap.peek m v, 0)
+ in
+ wt (NameMap.insert m (v, n + 1)) (c + 1) tms
+ end
+ | wt m c (Term.Fn (f,a) :: tms) =
+ wt m (c + weight (f, length a)) (a @ tms)
+ in
+ fn tm => wt weightEmpty ~1 [tm]
+ end;
+
+fun weightLowerBound (w as Weight (m,c)) =
+ if NameMap.exists (fn (_,n) => n < 0) m then NONE else SOME c;
+
+(*MetisDebug
+val ppWeightList =
+ let
+ fun ppCoeff n =
+ if n < 0 then Print.sequence (Print.addString "~") (ppCoeff (~n))
+ else if n = 1 then Print.skip
+ else Print.ppInt n
+
+ fun pp_tm (NONE,n) = Print.ppInt n
+ | pp_tm (SOME v, n) = Print.sequence (ppCoeff n) (Name.pp v)
+ in
+ fn [] => Print.ppInt 0
+ | tms => Print.ppOpList " +" pp_tm tms
+ end;
+
+fun ppWeight (Weight (m,c)) =
+ let
+ val l = NameMap.toList m
+ val l = map (fn (v,n) => (SOME v, n)) l
+ val l = if c = 0 then l else l @ [(NONE,c)]
+ in
+ ppWeightList l
+ end;
+
+val weightToString = Print.toString ppWeight;
+*)
+
+(* ------------------------------------------------------------------------- *)
+(* The Knuth-Bendix term order. *)
+(* ------------------------------------------------------------------------- *)
+
+fun compare {weight,precedence} =
+ let
+ fun weightDifference tm1 tm2 =
+ let
+ val w1 = weightTerm weight tm1
+ and w2 = weightTerm weight tm2
+ in
+ weightSubtract w2 w1
+ end
+
+ fun weightLess tm1 tm2 =
+ let
+ val w = weightDifference tm1 tm2
+ in
+ if weightIsZero w then precedenceLess tm1 tm2
+ else weightDiffLess w tm1 tm2
+ end
+
+ and weightDiffLess w tm1 tm2 =
+ case weightLowerBound w of
+ NONE => false
+ | SOME 0 => precedenceLess tm1 tm2
+ | SOME n => n > 0
+
+ and precedenceLess (Term.Fn (f1,a1)) (Term.Fn (f2,a2)) =
+ (case precedence ((f1, length a1), (f2, length a2)) of
+ LESS => true
+ | EQUAL => firstNotEqualTerm weightLess (zip a1 a2)
+ | GREATER => false)
+ | precedenceLess _ _ = false
+
+ fun weightDiffGreater w tm1 tm2 = weightDiffLess (weightNeg w) tm2 tm1
+
+ fun weightCmp tm1 tm2 =
+ let
+ val w = weightDifference tm1 tm2
+ in
+ if weightIsZero w then precedenceCmp tm1 tm2
+ else if weightDiffLess w tm1 tm2 then SOME LESS
+ else if weightDiffGreater w tm1 tm2 then SOME GREATER
+ else NONE
+ end
+
+ and precedenceCmp (Term.Fn (f1,a1)) (Term.Fn (f2,a2)) =
+ (case precedence ((f1, length a1), (f2, length a2)) of
+ LESS => SOME LESS
+ | EQUAL => firstNotEqualTerm weightCmp (zip a1 a2)
+ | GREATER => SOME GREATER)
+ | precedenceCmp _ _ = raise Bug "kboOrder.precendenceCmp"
+ in
+ fn (tm1,tm2) =>
+ if Term.equal tm1 tm2 then SOME EQUAL else weightCmp tm1 tm2
+ end;
+
+(*MetisTrace7
+val compare = fn kbo => fn (tm1,tm2) =>
+ let
+ val () = Print.trace Term.pp "KnuthBendixOrder.compare: tm1" tm1
+ val () = Print.trace Term.pp "KnuthBendixOrder.compare: tm2" tm2
+ val result = compare kbo (tm1,tm2)
+ val () =
+ case result of
+ NONE => trace "KnuthBendixOrder.compare: result = Incomparable\n"
+ | SOME x =>
+ Print.trace Print.ppOrder "KnuthBendixOrder.compare: result" x
+ in
+ result
+ end;
+*)
+
+end