X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fcic_disambiguation%2Fdisambiguate.ml;h=9d42899c6895fffeeb3366f210c7dd6a3fbbe2f4;hb=8d58fba703fcb1cfddd2a78a0b157a087bcf2a5b;hp=45186669d09d482f7a55ebf5da9a73ed7ac1b0b8;hpb=424982ded255df68245241f56064202844ed1194;p=helm.git diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml index 45186669d..9d42899c6 100644 --- a/helm/software/components/cic_disambiguation/disambiguate.ml +++ b/helm/software/components/cic_disambiguation/disambiguate.ml @@ -37,7 +37,7 @@ exception NoWellTypedInterpretation of int * ((Stdpp.location list * string * string) list * (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * - Stdpp.location option * string Lazy.t * bool) list + (Stdpp.location * string) Lazy.t * bool) list exception PathNotWellFormed (** raised when an environment is not enough informative to decide *) @@ -105,8 +105,8 @@ let descr_of_domain_item = function type ('term,'metasenv,'subst,'graph) test_result = | Ok of 'term * 'metasenv * 'subst * 'graph - | Ko of Stdpp.location option * string Lazy.t - | Uncertain of Stdpp.location option * string Lazy.t + | Ko of (Stdpp.location * string) Lazy.t + | Uncertain of (Stdpp.location * string) Lazy.t let refine_term metasenv subst context uri term ugraph ~localization_tbl = (* if benchmark then incr actual_refinements; *) @@ -120,17 +120,17 @@ let refine_term metasenv subst context uri term ugraph ~localization_tbl = exn -> let rec process_exn loc = function - HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn + HExtlib.Localized (loc,exn) -> process_exn loc exn | CicRefine.Uncertain msg -> debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ; - Uncertain (loc,msg) + Uncertain (lazy (loc,Lazy.force msg)) | CicRefine.RefineFailure msg -> debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" (CicPp.ppterm term) (Lazy.force msg))); - Ko (loc,msg) + Ko (lazy (loc,Lazy.force msg)) | exn -> raise exn in - process_exn None exn + process_exn Stdpp.dummy_loc exn let refine_obj metasenv subst context uri obj ugraph ~localization_tbl = assert (context = []); @@ -146,18 +146,18 @@ let refine_obj metasenv subst context uri obj ugraph ~localization_tbl = exn -> let rec process_exn loc = function - HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn + HExtlib.Localized (loc,exn) -> process_exn loc exn | CicRefine.Uncertain msg -> debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ; - Uncertain (loc,msg) + Uncertain (lazy (loc,Lazy.force msg)) | CicRefine.RefineFailure msg -> debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" (CicPp.ppobj obj) (Lazy.force msg))) ; - Ko (loc,msg) + Ko (lazy (loc,Lazy.force msg)) | exn -> raise exn in - process_exn None exn + process_exn Stdpp.dummy_loc exn let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () = try @@ -1146,8 +1146,9 @@ let foo () = k in refine_profiler.HExtlib.profile foo () with - | Try_again msg -> Uncertain (None,msg) - | Invalid_choice (loc,msg) -> Ko (loc,msg) + | Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg)) + | Invalid_choice (None,msg) -> Ko(lazy (Stdpp.dummy_loc,Lazy.force msg)) + | Invalid_choice (Some loc,msg) -> Ko (lazy (loc,Lazy.force msg)) in (* (4) build all possible interpretations *) let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in @@ -1161,9 +1162,9 @@ in refine_profiler.HExtlib.profile foo () (match test_env aliases rem_dom base_univ with | Ok (thing, metasenv,subst,new_univ) -> [ aliases, diff, metasenv, subst, thing, new_univ ], [], [] - | Ko (loc,msg) -> [],[],[aliases,diff,loc,msg,true] - | Uncertain (loc,msg) -> - [],[aliases,diff,loc,msg],[]) + | Ko loc_msg -> [],[],[aliases,diff,loc_msg,true] + | Uncertain loc_msg -> + [],[aliases,diff,loc_msg],[]) | Node (locs,item,inner_dom) :: remaining_dom -> debug_print (lazy (sprintf "CHOOSED ITEM: %s" (string_of_domain_item item))); @@ -1174,8 +1175,9 @@ in refine_profiler.HExtlib.profile foo () match choices with [] -> [], [], - [aliases, diff, Some (List.hd locs), - lazy ("No choices for " ^ string_of_domain_item item), + [aliases, diff, + (lazy (List.hd locs, + "No choices for " ^ string_of_domain_item item)), true] (* | [codomain_item] -> @@ -1215,8 +1217,8 @@ in refine_profiler.HExtlib.profile foo () | _::_ -> let mark_not_significant failures = List.map - (fun (env, diff, loc, msg, _b) -> - env, diff, loc, msg, false) + (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 @@ -1245,18 +1247,18 @@ in refine_profiler.HExtlib.profile foo () ) in res @@ filter tl - | Uncertain (loc,msg) -> + | Uncertain loc_msg -> let res = (match inner_dom with - | [] -> [],[new_env,new_diff,loc,msg],[] + | [] -> [],[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 + | Ko loc_msg -> + let res = [],[],[new_env,new_diff,loc_msg,true] in res @@ filter tl) in let ok_l,uncertain_l,error_l = @@ -1269,7 +1271,7 @@ in refine_profiler.HExtlib.profile foo () ) ok_l ([],[],error_l) in List.fold_right - (fun (env,diff,_,_) res -> + (fun (env,diff,_) res -> aux env diff None remaining_dom rem_dom @@ res ) uncertain_l res_after_ok_l in @@ -1278,19 +1280,19 @@ in refine_profiler.HExtlib.profile foo () | Ok _ | Uncertain _ -> aux aliases diff lookup_in_todo_dom todo_dom [] - | Ko (loc,msg) -> [],[],[aliases,diff,loc,msg,true] in + | 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) + (fun (env,diff,loc_msg) -> (env,diff,loc_msg,true) ) uncertain @ errors in let errors = List.map - (fun (env,diff,loc,msg,significant) -> + (fun (env,diff,loc_msg,significant) -> let env' = filter_map_domain (fun locs domain_item -> @@ -1303,7 +1305,7 @@ in refine_profiler.HExtlib.profile foo () Not_found -> None) thing_dom in - env',diff,loc,msg,significant + env',diff,loc_msg,significant ) errors in raise (NoWellTypedInterpretation (0,errors))