- (match lpo 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 s x = XLT) tl2 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)
- | _ -> assert false
+(* 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
+ | 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