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