module Orderings (B : Terms.Blob) = struct
+ module Pp = Pp.Pp(B)
+
type weight = int * (int * int) list;;
let string_of_weight (cw, mw) =
;;
let rec lpo s t =
- let cmp a1 a2 =
- let res = B.compare a1 a2 in
- if res = 0 then XEQ else if res < 0 then XLT else XGT
- in
match s,t with
| s, t when s = t ->
XEQ
| Terms.Var _, Terms.Var _ ->
XINCOMPARABLE
- | Terms.Leaf a1, Terms.Leaf a2 ->
- cmp a1 a2
| _, Terms.Var i ->
if (List.mem i (Terms.vars_of_term s)) then XGT
else XINCOMPARABLE
- | Terms.Var _, _ ->
- (*| Terms.Leaf _, Terms.Node _ -> *)
- (match lpo t s with
- | XGT -> XLT
- | XLT -> XGT
- | o -> o)
- (*| Terms.Node (Terms.Leaf a1::tl), Terms.Leaf a2 ->
- (match cmp a1 a2 with
- | XGT -> XGT
- | _ ->
- if List.exists (fun x -> let o = lpo x t in o=XGT || o=XEQ) tl
- 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) ->
-(* let lo = List.map (lpo s) tl2 in
- let ro = List.map (lpo t) tl1 in
- if List.exists (fun x -> x=XGT || x=XEQ) lo
- then XGT
- else if List.exists (fun x -> x=XGT || x=XEQ) ro
- then XLT
- else begin
- match lpo hd1 hd2 with
- | XGT -> if List.for_all (fun x -> x=XGT) lo then XGT
- else XINCOMPARABLE
- | XLT -> if List.for_all (fun x -> x=XGT) ro then XLT
- else XINCOMPARABLE
- | XEQ -> List.fold_left2
- (fun acc si ti -> if acc = XEQ then lpo si ti else acc)
- XEQ tl1 tl2
- | XINCOMPARABLE -> XINCOMPARABLE
- | _ -> assert false
- end*)
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 lpo hd1 hd2 with
+ 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
in
match aux_ordering hd1 hd2 with
| XGT ->
- let res = List.fold_left (f t1) false tl2 in
+ let res = List.fold_left (f t1) true tl2 in
if res then XGT
else XINCOMPARABLE
| XLT ->
- let res = List.fold_left (f t2) false tl1 in
+ let res = List.fold_left (f t2) true tl1 in
if res then XLT
else XINCOMPARABLE
| XEQ -> (
in
match lex_res with
| XGT ->
- if List.fold_left (f t1) false tl2 then XGT
+ if List.fold_left (f t1) true tl2 then XGT
else XINCOMPARABLE
| XLT ->
- if List.fold_left (f t2) false tl1 then XLT
+ if List.fold_left (f t2) true tl1 then XLT
else XINCOMPARABLE
| _ -> XINCOMPARABLE
)
;;
let compare_terms x y =
- match lpo_old 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