| LexiconAst.Ident_alias (name, uri) ->
uri, `Sym_interp
(fun l->assert(l = []);
- let uri = UriManager.uri_of_string uri in
- fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)))
+ try
+ let nref = NReference.reference_of_string uri in
+ NCic.Const nref
+ with
+ 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
+ ~lookup_in_library:nlookup_in_library
~description_of_alias:LexiconAst.description_of_alias
~mk_choice:ncic_mk_choice
~mk_implicit
| exn ->
(* try_new None; *)
raise exn
+;;
+let disambiguate_nobj lexicon_status ?baseuri (text,prefix_len,obj) =
+ let uri =
+ let baseuri =
+ match baseuri with Some x -> x | None -> raise BaseUriNotSetYet
+ in
+ let name =
+ match obj with
+ | CicNotationPt.Inductive (_,(name,_,_,_)::_)
+ | CicNotationPt.Record (_,name,_,_) -> name ^ ".ind"
+ | CicNotationPt.Theorem (_,name,_,_) -> name ^ ".con"
+ | CicNotationPt.Inductive _ -> assert false
+ in
+ UriManager.uri_of_string (baseuri ^ "/" ^ name)
+ in
+ let diff, _, _, cic =
+ singleton "third"
+ (NCicDisambiguate.disambiguate_obj
+ ~lookup_in_library:nlookup_in_library
+ ~description_of_alias:LexiconAst.description_of_alias
+ ~mk_choice:ncic_mk_choice
+ ~mk_implicit
+ ~uri:(OCic2NCic.nuri_of_ouri uri)
+ ~coercion_db:(NCicCoercion.db ())
+ ~aliases:lexicon_status.LexiconEngine.aliases
+ ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
+ (text,prefix_len,obj)) in
+ let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
+ lexicon_status, cic
;;
let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
| GrafiteAst.Include _
| GrafiteAst.Print _
| GrafiteAst.Qed _
+ | GrafiteAst.NQed _
| GrafiteAst.Set _ as cmd ->
lexicon_status,metasenv,cmd
| GrafiteAst.Obj (loc,obj) ->