Bug fixed: left parameters of constructors were unified before refining them.

[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 411f393618d54e14b57a833dc5c1b894b5cf351b..8830a600dbaa315497030e0c61c716ab19b1c5b7 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -89,44 +89,13 @@ let ncic_mk_choice = function
   | LexiconAst.Ident_alias (name, uri) -> 
      uri, `Sym_interp 
       (fun l->assert(l = []);
-        let nuri = NUri.uri_of_string uri in
         try
-         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)
+         let nref = NReference.reference_of_string uri in
+          NCic.Const nref
         with
-         NCicEnvironment.ObjectNotFound _ ->
-         let uri = UriManager.uri_of_string uri in
-          fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)))
+         NReference.IllFormedReference _ ->
+          let uri = UriManager.uri_of_string uri in
+           fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)))
 ;;
 
 
@@ -188,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 =
@@ -217,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
@@ -700,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
@@ -788,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