unification hints almost ready

[helm.git] / helm / software / components / disambiguation / disambiguate.ml

diff --git a/helm/software/components/disambiguation/disambiguate.ml b/helm/software/components/disambiguation/disambiguate.ml
index d0bf1ee1751c0ea728d727217d714460cd055445..44498d08830b5b7c266f5573739ef119cf772f43 100644 (file)
--- 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,50 +404,6 @@ 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) ->
-    mk_localization_tbl:(int -> '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 
@@ -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> *)
@@ -680,11 +631,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