Bug fixed: the relevance list can be shorted then leftno args.

[helm.git] / helm / software / components / grafite_parser / grafiteDisambiguate.ml

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index d27079d81d26f0809faec20f80966bd91476c2ea..8830a600dbaa315497030e0c61c716ab19b1c5b7 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -92,42 +92,6 @@ let ncic_mk_choice = function
         try
          let nref = NReference.reference_of_string uri in
           NCic.Const nref
-(*
-         let _,height,_,_,obj = NCicEnvironment.get_checked_obj nuri in
-         let spec =
-          match obj with
-             NCic.Constant (_,_,None,_,_) -> NReference.Decl
-           | NCic.Constant (_,_,Some _,_,_) -> NReference.Def height
-           | NCic.Fixpoint (is_ind,fl,_) ->
-              (* CSC: bug here: name need not be the wanted name
-                 Solution: a real new _reference_ should arrive here *)
-              (match
-                HExtlib.list_index (fun (_,name',_,_,_) -> name=name') fl,is_ind
-               with
-                  None,_ -> assert false
-                | Some (i,(_,_,recno,_,_)),true-> NReference.Fix(i,recno,height)
-                | Some (i,(_,_,_,_,_)),false -> NReference.CoFix i)
-           | NCic.Inductive (inductive,leftno,il,_) ->
-              (match
-                HExtlib.list_index (fun (_,name',_,_) -> name=name') il
-               with
-                  None ->
-                   let cl =
-                    List.concat
-                     (HExtlib.list_mapi (fun (_,_,_,cl) i ->
-                       List.map (fun t -> i,t) cl) il)
-                   in
-                    (match
-                      HExtlib.list_index (fun i,(_,name',_) -> name=name') cl
-                     with
-                        None -> assert false
-                      | Some (j,(i,_)) -> NReference.Con (i,j,leftno))
-                | Some (i,_) -> NReference.Ind (inductive,i,leftno))
-         in
-          NCic.Const (NReference.reference_of_spec nuri spec)
-        with
-         NCicEnvironment.ObjectNotFound _ ->
-*)
         with
          NReference.IllFormedReference _ ->
           let uri = UriManager.uri_of_string uri in
@@ -193,6 +157,23 @@ let lookup_in_library
   | DisambiguateTypes.Num instance -> mk_num_alias instance
 ;;
 
+let nlookup_in_library 
+  interactive_user_uri_choice input_or_locate_uri item 
+=
+  match item with
+  | DisambiguateTypes.Id id -> 
+     (try
+       let references = NCicLibrary.resolve id in
+        List.map
+         (fun u -> LexiconAst.Ident_alias (id,NReference.string_of_reference u)
+         ) references @
+        lookup_in_library interactive_user_uri_choice input_or_locate_uri item
+      with
+       NCicLibrary.ObjectNotFound _ ->
+        lookup_in_library interactive_user_uri_choice input_or_locate_uri item)
+  | _ -> lookup_in_library interactive_user_uri_choice input_or_locate_uri item 
+;;
+
   (** @param term not meaningful when context is given *)
 let disambiguate_term expty text prefix_len lexicon_status_ref context metasenv
 term =
@@ -222,7 +203,7 @@ let disambiguate_nterm expty lexicon_status context metasenv subst thing
         ~aliases:lexicon_status.LexiconEngine.aliases
         ~expty 
         ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
-        ~lookup_in_library
+        ~lookup_in_library:nlookup_in_library
         ~mk_choice:ncic_mk_choice
         ~mk_implicit
         ~description_of_alias:LexiconAst.description_of_alias
@@ -705,7 +686,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
        (try
          (match 
           NCicDisambiguate.disambiguate_obj
-           ~lookup_in_library
+           ~lookup_in_library:nlookup_in_library
            ~description_of_alias:LexiconAst.description_of_alias
            ~mk_choice:ncic_mk_choice
            ~mk_implicit
@@ -793,7 +774,7 @@ let disambiguate_nobj lexicon_status ?baseuri (text,prefix_len,obj) =
   let diff, _, _, cic =
    singleton "third"
     (NCicDisambiguate.disambiguate_obj
-      ~lookup_in_library
+      ~lookup_in_library:nlookup_in_library
       ~description_of_alias:LexiconAst.description_of_alias
       ~mk_choice:ncic_mk_choice
       ~mk_implicit