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
| 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
exception ObjectNotFound of string Lazy.t
let storage = ref [];;
-let add_obj u obj = storage := (u,obj)::!storage;;
+
+let aliases = ref [];;
+
+let resolve name =
+ try
+ HExtlib.filter_map
+ (fun (name',nref) -> if name'=name then Some nref else None) !aliases
+ with
+ Not_found -> raise (ObjectNotFound (lazy name))
+;;
+
+let add_obj u obj =
+ storage := (u,obj)::!storage;
+ let _,height,_,_,obj = obj in
+ let references =
+ match obj with
+ NCic.Constant (_,name,None,_,_) ->
+ [name,NReference.reference_of_spec u NReference.Decl]
+ | NCic.Constant (_,name,Some _,_,_) ->
+ [name,NReference.reference_of_spec u (NReference.Def height)]
+ | NCic.Fixpoint (is_ind,fl,_) ->
+ HExtlib.list_mapi
+ (fun (_,name,recno,_,_) i ->
+ if is_ind then
+ name,NReference.reference_of_spec u (NReference.Fix(i,recno,height))
+ else
+ name,NReference.reference_of_spec u (NReference.CoFix i)) fl
+ | NCic.Inductive (inductive,leftno,il,_) ->
+ List.flatten
+ (HExtlib.list_mapi
+ (fun (_,iname,_,cl) i ->
+ HExtlib.list_mapi
+ (fun (_,cname,_) j->
+ cname,NReference.reference_of_spec u (NReference.Con (i,j,leftno))
+ ) cl @
+ [iname,
+ NReference.reference_of_spec u
+ (NReference.Ind (inductive,i,leftno))]
+ ) il)
+ in
+ aliases := references @ !aliases
+;;
let cache = NUri.UriHash.create 313;;
(* *)
(**************************************************************************)
+(* ATTENZIONE: si puo' eseguire solo con MatitaC e dopo aver scelto
+ Debug → always show all disambiguation errors (that, moreover, slows
+ down the library a lot) *)
+
include "nat/plus.ma".
ndefinition thesis0: ∀A:Type.Type ≝ λA. A → A.
-alias id "thesis0" = "cic:/matita/tests/ng_commands/thesis0.def(0)".
-
ndefinition thesis: ∀A:Type.Type ≝ λA. ?.
napply (A → A);
nqed.
-alias id "thesis" = "cic:/matita/tests/ng_commands/thesis.def(0)".
-
ntheorem foo: ∀A:Type.thesis A.#A;#x;napply x;
nqed.
-alias id "foo" = "cic:/matita/tests/ng_commands/foo.def(0)".
-
ntheorem goo: ∀A:Type.A → A. #A; napply (foo ?);
nqed.
-naxiom P: Prop.
-
-alias id "P" = "cic:/matita/tests/ng_commands/P.decl".
+naxiom NP: Prop.
-ndefinition Q: Prop ≝ P.
+ndefinition Q: Prop ≝ NP.
nlet rec nzero (n:nat) : nat ≝
match n with
[ O ⇒ O
| S m ⇒ nzero m].
-alias id "nzero" = "cic:/matita/tests/ng_commands/nzero.fix(0,0,0)".
-
ntheorem nzero_ok: nzero (S (S O)) = O.
napply (refl_eq ? O);
nqed.
projects / helm.git / commitdiff