From a3ca416fdbe04b22a921dfd18b55e67564b045cc Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 25 Apr 2009 21:24:50 +0000 Subject: [PATCH] It is now possible to declare new aliases using the old syntax (maybe confusing, but a string is a string). Thus much code becomes useless in GrafiteDisambiguate. But it will be moved in the next commit to nCicLibrary to implement the nlookup_in_library function. --- .../components/grafite_parser/grafiteDisambiguate.ml | 11 ++++++++--- .../components/grafite_parser/grafiteParser.ml | 6 ++++-- helm/software/matita/tests/ng_commands.ma | 10 +++++----- 3 files changed, 17 insertions(+), 10 deletions(-) diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index 411f39361..d27079d81 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -89,8 +89,10 @@ 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 nref = NReference.reference_of_string uri in + NCic.Const nref +(* let _,height,_,_,obj = NCicEnvironment.get_checked_obj nuri in let spec = match obj with @@ -125,8 +127,11 @@ let ncic_mk_choice = function NCic.Const (NReference.reference_of_spec nuri spec) with NCicEnvironment.ObjectNotFound _ -> - let uri = UriManager.uri_of_string uri in - fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri))) +*) + with + NReference.IllFormedReference _ -> + let uri = UriManager.uri_of_string uri in + fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri))) ;; diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 633d98ea9..324231b50 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -629,10 +629,12 @@ EXTEND let rex = Str.regexp ("^"^ident^"$") in if Str.string_match rex id 0 then if (try ignore (UriManager.uri_of_string uri); true - with UriManager.IllFormedUri _ -> false) + with UriManager.IllFormedUri _ -> false) || + (try ignore (NReference.reference_of_string uri); true + with NReference.IllFormedReference _ -> false) then L.Ident_alias (id, uri) - else + else raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri))) else diff --git a/helm/software/matita/tests/ng_commands.ma b/helm/software/matita/tests/ng_commands.ma index 6a65ea039..d6f97499e 100644 --- a/helm/software/matita/tests/ng_commands.ma +++ b/helm/software/matita/tests/ng_commands.ma @@ -16,25 +16,25 @@ include "nat/plus.ma". ndefinition thesis0: ∀A:Type.Type ≝ λA. A → A. -alias id "thesis0" = "cic:/matita/tests/ng_commands/thesis0.con". +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.con". +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.con". +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.con". +alias id "P" = "cic:/matita/tests/ng_commands/P.decl". ndefinition Q: Prop ≝ P. @@ -43,7 +43,7 @@ nlet rec nzero (n:nat) : nat ≝ [ O ⇒ O | S m ⇒ nzero m]. -alias id "nzero" = "cic:/matita/tests/ng_commands/nzero.con". +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); -- 2.39.2