X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fdisambiguation%2Fdisambiguate.ml;h=5b5b53f52cd8a3b73edc64f35c7cb7670645157a;hb=refs%2Fheads%2Fmatita-lablgtk3;hp=ae56682cef2adbd8fef6ca20c456af16d4e22320;hpb=534a4d25a24227dac52c20d8430d12841b856350;p=helm.git

diff --git a/helm/software/components/disambiguation/disambiguate.ml b/helm/software/components/disambiguation/disambiguate.ml
index ae56682ce..5b5b53f52 100644
--- a/helm/software/components/disambiguation/disambiguate.ml
+++ b/helm/software/components/disambiguation/disambiguate.ml
@@ -310,7 +310,9 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
                 [] subst in
             [ Node ([loc], Id name, terms) ]))
   | Ast.Uri _ -> []
-  | Ast.Implicit -> []
+  | Ast.NRef _ -> []
+  | Ast.NCic _ -> []
+  | Ast.Implicit _ -> []
   | Ast.Num (num, i) -> [ Node ([loc], Num i, []) ]
   | Ast.Meta (index, local_context) ->
       List.fold_left
@@ -333,7 +335,7 @@ let domain_of_term ~context term =
 let domain_of_obj ~context ast =
  assert (context = []);
   match ast with
-   | Ast.Theorem (_,_,ty,bo) ->
+   | Ast.Theorem (_,_,ty,bo,_) ->
       domain_of_term [] ty
       @ (match bo with
           None -> []
@@ -379,8 +381,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,57 +406,18 @@ 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"
 
+type alias_spec =
+  | Ident_alias of string * string        (* identifier, uri *)
+  | Symbol_alias of string * int * string (* name, instance no, description *)
+  | Number_alias of int * string          (* instance no, description *)
+
 let disambiguate_thing 
   ~context ~metasenv ~subst ~use_coercions
   ~string_context_of_context
-  ~initial_ugraph:base_univ ~hint
-  ~mk_implicit ~description_of_alias
+  ~initial_ugraph:base_univ ~expty
+  ~mk_implicit ~description_of_alias ~fix_instance
   ~aliases ~universe ~lookup_in_library 
   ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing 
   ~mk_localization_tbl
@@ -483,17 +444,25 @@ let disambiguate_thing
             input_or_locate_uri item
       | Some e ->
           (try
-            let item =
-              match item with
-              | Symbol (symb, _) -> Symbol (symb, 0)
-              | item -> item
-            in
-            Environment.find item e
-          with Not_found -> 
-            lookup_in_library 
-              interactive_user_uri_choice 
-              input_or_locate_uri item)
+            fix_instance item (Environment.find item e)
+          with Not_found -> [])
    in
+
+   (* items with 1 choice are interpreted ASAP *)
+   let aliases, todo_dom = 
+     let rec aux (aliases,acc) = function 
+       | [] -> aliases, acc
+       | (Node (_, item,extra) as node) :: tl -> 
+           let choices = lookup_choices item in
+           if List.length choices <> 1 then aux (aliases, acc@[node]) tl
+           else
+           let tl = tl @ extra in
+           if Environment.mem item aliases then aux (aliases, acc) tl
+           else aux (Environment.add item (List.hd choices) aliases, acc) tl
+     in
+       aux (aliases,[]) todo_dom
+   in
+
 (*
       (* <benchmark> *)
       let _ =
@@ -538,14 +507,9 @@ let disambiguate_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))