module Orderings (B : Terms.Blob) = struct
+ module Pp = Pp.Pp(B)
+
type weight = int * (int * int) list;;
let string_of_weight (cw, mw) =
) else r
| res -> res
;;
-
+
+ let rec lpo s t =
+ match s,t with
+ | s, t when s = t ->
+ XEQ
+ | Terms.Var _, Terms.Var _ ->
+ XINCOMPARABLE
+ | _, Terms.Var i ->
+ if (List.mem i (Terms.vars_of_term s)) then XGT
+ else XINCOMPARABLE
+ | Terms.Var i,_ ->
+ if (List.mem i (Terms.vars_of_term t)) then XLT
+ else XINCOMPARABLE
+ | Terms.Node (hd1::tl1), Terms.Node (hd2::tl2) ->
+ if List.exists (fun x -> let o = lpo x t in o=XGT || o=XEQ) tl1
+ then XGT
+ else if List.exists (fun x -> let o=lpo s x in o=XLT || o=XEQ) tl2
+ then XLT
+ else begin
+ match aux_ordering hd1 hd2 with
+ | XGT -> if List.for_all (fun x -> lpo s x = XGT) tl2 then XGT
+ else XINCOMPARABLE
+ | XLT -> if List.for_all (fun x -> lpo x t = XLT) tl1 then XLT
+ else XINCOMPARABLE
+ | XEQ ->
+ let lex = List.fold_left2
+ (fun acc si ti -> if acc = XEQ then lpo si ti else acc)
+ XEQ tl1 tl2
+ in
+ (match lex with
+ | XGT ->
+ if List.for_all (fun x -> lpo s x = XGT) tl2 then XGT
+ else XINCOMPARABLE
+ | XLT ->
+ if List.for_all (fun x -> lpo x t = XLT) tl1 then XLT
+ else XINCOMPARABLE
+ | o -> o)
+ | XINCOMPARABLE -> XINCOMPARABLE
+ | _ -> assert false
+ end
+ | _,_ -> aux_ordering s t
+
+ ;;
+
+let rec lpo_old t1 t2 =
+ match t1, t2 with
+ | t1, t2 when t1 = t2 -> XEQ
+ | t1, (Terms.Var m) ->
+ if List.mem m (Terms.vars_of_term t1) then XGT else XINCOMPARABLE
+ | (Terms.Var m), t2 ->
+ if List.mem m (Terms.vars_of_term t2) then XLT else XINCOMPARABLE
+ | Terms.Node (hd1::tl1), Terms.Node (hd2::tl2) -> (
+ let res =
+ let f o r t =
+ if r then true else
+ match lpo_old t o with
+ | XGT | XEQ -> true
+ | _ -> false
+ in
+ let res1 = List.fold_left (f t2) false tl1 in
+ if res1 then XGT
+ else let res2 = List.fold_left (f t1) false tl2 in
+ if res2 then XLT
+ else XINCOMPARABLE
+ in
+ if res <> XINCOMPARABLE then
+ res
+ else
+ let f o r t =
+ if not r then false else
+ match lpo_old o t with
+ | XGT -> true
+ | _ -> false
+ in
+ match aux_ordering hd1 hd2 with
+ | XGT ->
+ let res = List.fold_left (f t1) true tl2 in
+ if res then XGT
+ else XINCOMPARABLE
+ | XLT ->
+ let res = List.fold_left (f t2) true tl1 in
+ if res then XLT
+ else XINCOMPARABLE
+ | XEQ -> (
+ let lex_res =
+ try
+ List.fold_left2
+ (fun r t1 t2 -> if r <> XEQ then r else lpo_old t1 t2)
+ XEQ tl1 tl2
+ with Invalid_argument _ ->
+ XINCOMPARABLE
+ in
+ match lex_res with
+ | XGT ->
+ if List.fold_left (f t1) true tl2 then XGT
+ else XINCOMPARABLE
+ | XLT ->
+ if List.fold_left (f t2) true tl1 then XLT
+ else XINCOMPARABLE
+ | _ -> XINCOMPARABLE
+ )
+ | _ -> XINCOMPARABLE
+ )
+ | t1, t2 -> aux_ordering t1 t2
+;;
+
let compare_terms x y =
- match nonrec_kbo x y with
- | XINCOMPARABLE -> Terms.Incomparable
- | XGT -> Terms.Gt
- | XLT -> Terms.Lt
- | XEQ -> Terms.Eq
- | _ -> assert false
+ match lpo x y with
+ | XINCOMPARABLE -> Terms.Incomparable
+ | XGT -> Terms.Gt
+ | XLT -> Terms.Lt
+ | XEQ -> Terms.Eq
+ | _ -> assert false
;;
end