| 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)))
;;
| 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 =
~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
(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
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