From: Claudio Sacerdoti Coen Date: Sat, 25 Apr 2009 22:30:39 +0000 (+0000) Subject: Lookup_in_library implemented for new objects. Basically, this stupid (??), X-Git-Tag: make_still_working~4047 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e02c6eaf8d50025c3be8bbf6988ab8b2a37b40da;p=helm.git Lookup_in_library implemented for new objects. Basically, this stupid (??), inefficient (??) implementation just keeps an associative list that maps names to URIs and is used to resolve names in the library. This functionality is provided by ng_kernel/nCicLibrary. Note: automatic addition of preferences is not there yet. Thus you need to activate lookup in library to see it working. --- diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index d27079d81..8830a600d 100644 --- 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 diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml index 4e9133417..fa96a69b4 100644 --- a/helm/software/components/ng_kernel/nCicLibrary.ml +++ b/helm/software/components/ng_kernel/nCicLibrary.ml @@ -14,7 +14,48 @@ 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;; diff --git a/helm/software/components/ng_kernel/nCicLibrary.mli b/helm/software/components/ng_kernel/nCicLibrary.mli index fdcbbde5c..357927f06 100644 --- a/helm/software/components/ng_kernel/nCicLibrary.mli +++ b/helm/software/components/ng_kernel/nCicLibrary.mli @@ -14,6 +14,7 @@ exception ObjectNotFound of string Lazy.t val add_obj: NUri.uri -> NCic.obj -> unit +val resolve: string -> NReference.reference list val get_obj: NUri.uri -> NCic.obj val clear_cache : unit -> unit diff --git a/helm/software/matita/tests/ng_commands.ma b/helm/software/matita/tests/ng_commands.ma index d6f97499e..b59715649 100644 --- a/helm/software/matita/tests/ng_commands.ma +++ b/helm/software/matita/tests/ng_commands.ma @@ -12,39 +12,33 @@ (* *) (**************************************************************************) +(* 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.