-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
-;;
-