- | _::_ ->
- let mark_not_significant failures =
- List.map
- (fun (env, diff, loc_msg, _b) ->
- env, diff, loc_msg, false)
- failures in
- let classify_errors ((ok_l,uncertain_l,error_l) as outcome) =
- if ok_l <> [] || uncertain_l <> [] then
- ok_l,uncertain_l,mark_not_significant error_l
- else
- outcome in
- let rec filter = function
- | [] -> [],[],[]
- | codomain_item :: tl ->
- debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
- let new_env = Environment.add item codomain_item aliases in
- let new_diff = (item,codomain_item)::diff in
- (match
- test_env new_env
- (inner_dom@remaining_dom@rem_dom) base_univ
- with
- | Ok (thing, metasenv,subst,new_univ) ->
- let res =
- (match inner_dom with
- | [] ->
- [new_env,new_diff,metasenv,subst,thing,new_univ],
- [], []
- | _ ->
- aux new_env new_diff None inner_dom
- (remaining_dom@rem_dom)
- )
- in
- res @@ filter tl
- | Uncertain loc_msg ->
- let res =
- (match inner_dom with
- | [] -> [],[new_env,new_diff,loc_msg],[]
- | _ ->
- aux new_env new_diff None inner_dom
- (remaining_dom@rem_dom)
- )
- in
- res @@ filter tl
- | Ko loc_msg ->
- let res = [],[],[new_env,new_diff,loc_msg,true] in
- res @@ filter tl)
- in
- let ok_l,uncertain_l,error_l =
- classify_errors (filter choices)
- in
- let res_after_ok_l =
- List.fold_right
- (fun (env,diff,_,_,_,_) res ->
- aux env diff None remaining_dom rem_dom @@ res
- ) ok_l ([],[],error_l)
- in
- List.fold_right
- (fun (env,diff,_) res ->
- aux env diff None remaining_dom rem_dom @@ res
- ) uncertain_l res_after_ok_l
- in
- let aux' aliases diff lookup_in_todo_dom todo_dom =
- match test_env aliases todo_dom base_univ with
- | Ok _
- | Uncertain _ ->
- aux aliases diff lookup_in_todo_dom todo_dom []
- | Ko (loc_msg) -> [],[],[aliases,diff,loc_msg,true] in
- try
- let res =
- match aux' aliases [] None todo_dom with
- | [],uncertain,errors ->
- let errors =
- List.map
- (fun (env,diff,loc_msg) -> (env,diff,loc_msg,true)
- ) uncertain @ errors
+ | _::_ ->
+ let mark_not_significant failures =
+ List.map
+ (fun (env, diff, loc_msg, _b) ->
+ env, diff, loc_msg, false)
+ failures in
+ let classify_errors ((ok_l,uncertain_l,error_l) as outcome) =
+ if ok_l <> [] || uncertain_l <> [] then
+ ok_l,uncertain_l,mark_not_significant error_l
+ else
+ outcome in
+ let rec filter = function
+ | [] -> [],[],[]
+ | codomain_item :: tl ->
+ (*debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));*)
+ let new_env = Environment.add item codomain_item aliases in
+ let new_diff = (item,codomain_item)::diff in
+ (match
+ test_env new_env
+ (inner_dom@remaining_dom@rem_dom) base_univ
+ with
+ | Ok (thing, metasenv,subst,new_univ) ->
+(* prerr_endline "OK"; *)
+ let res =
+ (match inner_dom with
+ | [] ->
+ [new_env,new_diff,metasenv,subst,thing,new_univ],
+ [], []
+ | _ ->
+ aux new_env new_diff None inner_dom
+ (remaining_dom@rem_dom)
+ )
+ in
+ res @@ filter tl
+ | Uncertain loc_msg ->
+(* prerr_endline ("UNCERTAIN"); *)
+ let res =
+ (match inner_dom with
+ | [] -> [],[new_env,new_diff,loc_msg],[]
+ | _ ->
+ aux new_env new_diff None inner_dom
+ (remaining_dom@rem_dom)
+ )
+ in
+ res @@ filter tl
+ | Ko loc_msg ->
+(* prerr_endline "KO"; *)
+ let res = [],[],[new_env,new_diff,loc_msg,true] in
+ res @@ filter tl)
+ in
+ let ok_l,uncertain_l,error_l =
+ classify_errors (filter choices)