X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fdisambiguation%2Fdisambiguate.ml;h=fa63d1f484e6daca79d910587dafd579fcf5ed15;hb=2b837ca9e298eb44eee95d9ca0e331c577785dcb;hp=0b73296e789da2f2adc7993b930da2f489b075a8;hpb=c04f852241510515f06e3bec8eb79acac6e4952e;p=helm.git

diff --git a/helm/software/components/disambiguation/disambiguate.ml b/helm/software/components/disambiguation/disambiguate.ml
index 0b73296e7..fa63d1f48 100644
--- a/helm/software/components/disambiguation/disambiguate.ml
+++ b/helm/software/components/disambiguation/disambiguate.ml
@@ -379,8 +379,6 @@ let domain_of_obj ~context ast =
 let domain_of_obj ~context obj = 
  uniq_domain (domain_of_obj ~context obj)
 
-let domain_of_ast_term = domain_of_term;;
-
   (* dom1 \ dom2 *)
 let domain_diff dom1 dom2 =
 (* let domain_diff = Domain.diff *)
@@ -406,60 +404,16 @@ let domain_diff dom1 dom2 =
    in
     aux dom1
 
-module type Disambiguator =
-sig
-  val disambiguate_thing:
-    context:'context ->
-    metasenv:'metasenv ->
-    subst:'subst ->
-    use_coercions:bool ->
-    string_context_of_context:('context -> string option list) ->
-    initial_ugraph:'ugraph ->
-    hint: 
-      ('metasenv -> 'raw_thing -> 'raw_thing) * 
-      (('refined_thing,'metasenv,'subst,'ugraph) test_result ->
-         ('refined_thing,'metasenv,'subst,'ugraph) test_result) ->
-    mk_implicit:(bool -> 'alias) ->
-    description_of_alias:('alias -> string) ->
-    aliases:'alias DisambiguateTypes.Environment.t ->
-    universe:'alias list DisambiguateTypes.Environment.t option ->
-    lookup_in_library:(
-      DisambiguateTypes.interactive_user_uri_choice_type ->
-      DisambiguateTypes.input_or_locate_uri_type ->
-      DisambiguateTypes.Environment.key ->
-      'alias list) ->
-    uri:'uri ->
-    pp_thing:('ast_thing -> string) ->
-    domain_of_thing:(context: string option list -> 'ast_thing -> domain) ->
-    interpretate_thing:(
-      context:'context ->
-      env:'alias DisambiguateTypes.Environment.t ->
-      uri:'uri ->
-      is_path:bool -> 
-      'ast_thing -> 
-      localization_tbl:'cichash -> 
-        'raw_thing) ->
-    refine_thing:(
-      'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool ->
-      'raw_thing -> 'ugraph -> localization_tbl:'cichash -> 
-        ('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
-    localization_tbl:'cichash ->
-    string * int * 'ast_thing ->
-    ((DisambiguateTypes.Environment.key * 'alias) list * 
-     'metasenv * 'subst * 'refined_thing * 'ugraph)
-    list * bool
-end
-
 let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
 
 let disambiguate_thing 
   ~context ~metasenv ~subst ~use_coercions
   ~string_context_of_context
-  ~initial_ugraph:base_univ ~hint
+  ~initial_ugraph:base_univ ~expty
   ~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");
@@ -489,10 +443,7 @@ let disambiguate_thing
               | item -> item
             in
             Environment.find item e
-          with Not_found -> 
-            lookup_in_library 
-              interactive_user_uri_choice 
-              input_or_locate_uri item)
+          with Not_found -> [])
    in
 (*
       (* <benchmark> *)
@@ -533,18 +484,14 @@ 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
        in
-       let cic_thing = (fst hint) metasenv cic_thing in
 let foo () =
-       let k =
         refine_thing metasenv subst context uri
-         ~use_coercions cic_thing ugraph ~localization_tbl
-       in
-       let k = (snd hint) k in
-         k
+         ~use_coercions cic_thing expty ugraph ~localization_tbl
 in refine_profiler.HExtlib.profile foo ()
      with
      | Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg))
@@ -636,6 +583,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 +596,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 +607,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
@@ -676,11 +626,14 @@ in refine_profiler.HExtlib.profile foo ()
               ) 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]
+   if todo_dom = [] then
+     aux aliases diff lookup_in_todo_dom todo_dom [] 
+   else
+     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
     let res =
      match aux' aliases [] None todo_dom with