(*** Computation of critical pairs in SML
ML Programs from Chapter 6 of
Term Rewriting and All That
by Franz Baader and Tobias Nipkow,
(Cambridge University Press, 1998)
Copyright (C) 1998 by Cambridge University Press.
Permission to use without fee is granted provided that this copyright
notice is included in any copy.
***)
fun max(i,j:int) = if i > j then i else j;
(* maxs: int list -> int *)
fun maxs (i::is) = max(i, maxs is)
| maxs [] = 0;
(* maxindex: term -> int *)
fun maxindex (V(x,i)) = i
| maxindex (T(_,ts)) = maxs(map maxindex ts);
(* rename: int -> term -> term *)
fun rename n (V(x,i)) = V(x,i+n)
| rename n (T(f,ts)) = T(f, map (rename n) ts);
(* CP: (term -> term) -> term * term -> term * term -> (term * term) list *)
fun CP C (t,r) (l2,r2) = let val sigma = lift(unify(t,l2))
in [(sigma r, sigma(C r2))] end
handle UNIFY => [];
(* CPs: (term * term) list -> term * term -> (term * term) list *)
fun CPs R (l,r) =
let fun cps C (V _, _) = []
| cps C (T(f,ts),r) =
concat(map (CP C (T(f,ts),r)) R) @ (innercps C (f,[],ts,r))
and innercps _ (_, _, [], _) = []
| innercps C (f, ts0, t::ts1, r) =
let fun Cf s = C(T(f, ts0 @ [s] @ ts1))
in (cps Cf (t,r)) @ (innercps C (f, ts0 @ [t], ts1, r)) end
val m = maxs(map (fn (l,r) => max(maxindex l, maxindex r)) R) + 1
in cps (fn t => t) (rename m l, rename m r) end;
fun CriticalPairs2 R1 R2 = concat(map (CPs R1) R2);
fun CriticalPairs R = CriticalPairs2 R R;