From: Enrico Tassi Date: Fri, 5 Dec 2008 11:26:55 +0000 (+0000) Subject: disambiguation takes ~mk_localization_tbl and not ~localization_tbl, thus can X-Git-Tag: make_still_working~4456 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=93ce01455cfeba6b29e3c8a57e28f56559fb891d;p=helm.git disambiguation takes ~mk_localization_tbl and not ~localization_tbl, thus can create the hashtable when needed (after every interpretation) --- diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.ml b/helm/software/components/cic_disambiguation/cicDisambiguate.ml index 288be5fa2..2b469ce9d 100644 --- a/helm/software/components/cic_disambiguation/cicDisambiguate.ml +++ b/helm/software/components/cic_disambiguation/cicDisambiguate.ml @@ -642,7 +642,7 @@ let disambiguate_term ~context ~metasenv ~subst ?goal | _ -> assert false) | k -> k in - let localization_tbl = Cic.CicHash.create 503 in + let mk_localization_tbl x = Cic.CicHash.create x in MultiPassDisambiguator.disambiguate_thing ~context ~metasenv ~subst ~initial_ugraph ~aliases ~string_context_of_context ~universe ~lookup_in_library ~mk_implicit ~description_of_alias @@ -650,7 +650,7 @@ let disambiguate_term ~context ~metasenv ~subst ?goal ~domain_of_thing:Disambiguate.domain_of_term ~interpretate_thing:(interpretate_term (?create_dummy_ids:None) ~mk_choice) ~refine_thing:refine_term (text,prefix_len,term) - ~localization_tbl + ~mk_localization_tbl ~hint ~freshen_thing:CicNotationUtil.freshen_term ~passes:(MultiPassDisambiguator.passes ()) @@ -659,7 +659,7 @@ let disambiguate_obj ~mk_implicit ~description_of_alias ~mk_choice ~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj) = let hint = (fun _ x -> x), fun k -> k in - let localization_tbl = Cic.CicHash.create 503 in + let mk_localization_tbl x = Cic.CicHash.create x in MultiPassDisambiguator.disambiguate_thing ~context:[] ~metasenv:[] ~subst:[] ~aliases ~universe ~uri ~string_context_of_context ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) @@ -668,7 +668,7 @@ let disambiguate_obj ~mk_implicit ~description_of_alias ~mk_choice ~initial_ugraph:CicUniv.empty_ugraph ~interpretate_thing:(interpretate_obj ~mk_choice) ~refine_thing:refine_obj - ~localization_tbl + ~mk_localization_tbl ~hint ~passes:(MultiPassDisambiguator.passes ()) ~freshen_thing:CicNotationUtil.freshen_obj diff --git a/helm/software/components/disambiguation/disambiguate.ml b/helm/software/components/disambiguation/disambiguate.ml index 0b73296e7..d0bf1ee17 100644 --- a/helm/software/components/disambiguation/disambiguate.ml +++ b/helm/software/components/disambiguation/disambiguate.ml @@ -443,7 +443,7 @@ sig 'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool -> 'raw_thing -> 'ugraph -> localization_tbl:'cichash -> ('refined_thing, 'metasenv,'subst,'ugraph) test_result) -> - localization_tbl:'cichash -> + mk_localization_tbl:(int -> 'cichash) -> string * int * 'ast_thing -> ((DisambiguateTypes.Environment.key * 'alias) list * 'metasenv * 'subst * 'refined_thing * 'ugraph) @@ -459,7 +459,7 @@ let disambiguate_thing ~mk_implicit ~description_of_alias ~aliases ~universe ~lookup_in_library ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing - ~localization_tbl + ~mk_localization_tbl (thing_txt,thing_txt_prefix_len,thing) = debug_print (lazy "DISAMBIGUATE INPUT"); @@ -533,6 +533,7 @@ let disambiguate_thing env in aux (aux env l) tl in let filled_env = aux aliases todo_dom in + let localization_tbl = mk_localization_tbl 503 in let cic_thing = interpretate_thing ~context ~env:filled_env ~uri ~is_path:false thing ~localization_tbl @@ -636,6 +637,7 @@ in refine_profiler.HExtlib.profile foo () (inner_dom@remaining_dom@rem_dom) base_univ with | Ok (thing, metasenv,subst,new_univ) -> +(* prerr_endline "OK"; *) let res = (match inner_dom with | [] -> @@ -648,6 +650,7 @@ in refine_profiler.HExtlib.profile foo () in res @@ filter tl | Uncertain loc_msg -> +(* prerr_endline ("UNCERTAIN"); *) let res = (match inner_dom with | [] -> [],[new_env,new_diff,loc_msg],[] @@ -658,6 +661,7 @@ in refine_profiler.HExtlib.profile foo () in res @@ filter tl | Ko loc_msg -> +(* prerr_endline "KO"; *) let res = [],[],[new_env,new_diff,loc_msg,true] in res @@ filter tl) in diff --git a/helm/software/components/disambiguation/disambiguate.mli b/helm/software/components/disambiguation/disambiguate.mli index cb1882a7d..5c74b857b 100644 --- a/helm/software/components/disambiguation/disambiguate.mli +++ b/helm/software/components/disambiguation/disambiguate.mli @@ -123,7 +123,7 @@ val disambiguate_thing: 'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool -> 'raw_thing -> 'ugraph -> localization_tbl:'cichash -> ('refined_thing, 'metasenv,'subst,'ugraph) test_result) -> - localization_tbl:'cichash -> + mk_localization_tbl:(int -> 'cichash) -> string * int * 'ast_thing -> ((DisambiguateTypes.Environment.key * 'alias) list * 'metasenv * 'subst * 'refined_thing * 'ugraph) diff --git a/helm/software/components/disambiguation/multiPassDisambiguator.ml b/helm/software/components/disambiguation/multiPassDisambiguator.ml index 07bbdeba2..becf2a412 100644 --- a/helm/software/components/disambiguation/multiPassDisambiguator.ml +++ b/helm/software/components/disambiguation/multiPassDisambiguator.ml @@ -142,16 +142,15 @@ let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~f thing let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst ~string_context_of_context ~initial_ugraph ~hint ~mk_implicit ~description_of_alias ~aliases ~universe ~lookup_in_library ~uri ~pp_thing - ~domain_of_thing ~interpretate_thing ~refine_thing ~localization_tbl thing + ~domain_of_thing ~interpretate_thing ~refine_thing ~mk_localization_tbl thing = let f ~fresh_instances ~aliases ~universe ~use_coercions (txt,len,thing) = - let thing = if fresh_instances then freshen_thing thing else thing - in + let thing = if fresh_instances then freshen_thing thing else thing in Disambiguate.disambiguate_thing ~context ~metasenv ~subst ~use_coercions ~string_context_of_context ~initial_ugraph ~hint ~mk_implicit ~description_of_alias ~aliases ~universe ~lookup_in_library ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing - ~localization_tbl (txt,len,thing) + ~mk_localization_tbl (txt,len,thing) in disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~f thing diff --git a/helm/software/components/disambiguation/multiPassDisambiguator.mli b/helm/software/components/disambiguation/multiPassDisambiguator.mli index 777fedafd..0151f8d3d 100644 --- a/helm/software/components/disambiguation/multiPassDisambiguator.mli +++ b/helm/software/components/disambiguation/multiPassDisambiguator.mli @@ -74,7 +74,7 @@ val disambiguate_thing: 'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool -> 'raw_thing -> 'ugraph -> localization_tbl:'cichash -> ('refined_thing, 'metasenv,'subst,'ugraph) Disambiguate.test_result) -> - localization_tbl:'cichash -> + mk_localization_tbl:(int -> 'cichash) -> string * int * 'ast_thing -> ((DisambiguateTypes.Environment.key * 'alias) list * 'metasenv * 'subst * 'refined_thing * 'ugraph) diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index 03579afab..6ec2c6507 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -75,8 +75,9 @@ let interpretate_term match t with | CicNotationPt.AttributedTerm (`Loc loc, term) -> let res = aux ~localize loc context term in - if localize then NCicUntrusted.NCicHash.add localization_tbl res loc; - res + if localize then + NCicUntrusted.NCicHash.add localization_tbl res loc; + res | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) -> let cic_args = List.map (aux ~localize loc context) args in @@ -400,14 +401,14 @@ patterns not implemented *) | _ -> assert false (* god bless Bologna *) in - prerr_endline (NCicPp.ppterm ~metasenv:[] ~context:[] ~subst:[] - res); +(* prerr_endline (NCicPp.ppterm ~metasenv:[] ~context:[] ~subst:[] res); *) res and aux_option ~localize loc context annotation = function | None -> NCic.Implicit annotation | Some (CicNotationPt.AttributedTerm (`Loc loc, term)) -> let res = aux_option ~localize loc context annotation (Some term) in - if localize then NCicUntrusted.NCicHash.add localization_tbl res loc; + if localize then + NCicUntrusted.NCicHash.add localization_tbl res loc; res | Some (CicNotationPt.AttributedTerm (_, term)) -> aux_option ~localize loc context annotation (Some term) @@ -433,7 +434,7 @@ let disambiguate_term ~context ~metasenv ~subst ?goal ~aliases ~universe ~lookup_in_library (text,prefix_len,term) = - let localization_tbl = NCicUntrusted.NCicHash.create 503 in + let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in let hint = match goal with None -> (fun _ y -> y),(fun x -> x) @@ -459,7 +460,7 @@ let disambiguate_term ~context ~metasenv ~subst ?goal ~lookup_in_library ~domain_of_thing:domain_of_term ~interpretate_thing:(interpretate_term ~mk_choice (?create_dummy_ids:None)) ~refine_thing:refine_term (text,prefix_len,term) - ~localization_tbl ~hint ~subst + ~mk_localization_tbl ~hint ~subst in List.map (function (a,b,c,d,_) -> a,b,c,d) res, b ;;