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
+ let rec ge_subterm t ol = function
+ | [] -> (false, ol)
+ | x::tl ->
+ let res = lpo x t in
+ match res with
+ | XGT | XEQ -> (true,res::ol)
+ | o -> ge_subterm t (o::ol) tl
+ in
+ let (res, l_ol) = ge_subterm t [] tl1 in
+ if res then XGT
+ else let (res, r_ol) = ge_subterm s [] tl2 in
+ if res then XLT
+ else begin
+ let rec check_subterms t = function
+ | _,[] -> true
+ | o::ol,_::tl ->
+ if o = XLT then check_subterms t (ol,tl)
+ else false
+ | [], x::tl ->
+ if lpo x t = XLT then check_subterms t ([],tl)
+ else false
+ in
+ match aux_ordering hd1 hd2 with
+ | XGT -> if check_subterms s (r_ol,tl2) then XGT
+ else XINCOMPARABLE
+ | XLT -> if check_subterms t (l_ol,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