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 288be5fa2d5b06fc11a51d4cd682a1b33c1f068c..2b469ce9d7d4b24585421f5007ff1cc80602c1f4 100644 (file)
--- 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 0b73296e789da2f2adc7993b930da2f489b075a8..d0bf1ee1751c0ea728d727217d714460cd055445 100644 (file)
--- 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 cb1882a7d12a900b0e51a39c4e943c32786c623d..5c74b857b49077bd1d68048af460252e5bc023a3 100644 (file)
--- 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 07bbdeba29d68e389590bd3b72650ac1bbe63d2f..becf2a41229c18b0b3259a1f2d453a05d0e716c7 100644 (file)
--- 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 777fedafd1d3353617c38094b62303970c59a4dc..0151f8d3dd7e8a8aef4d4a573b2622a519164424 100644 (file)
--- 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 03579afabb4091e3b07ae0ab01834faee73bc14a..6ec2c650759d0086fe29f3754319f2c6478a0830 100644 (file)
--- 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
 ;;