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.

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 411f393618d54e14b57a833dc5c1b894b5cf351b..d27079d81d26f0809faec20f80966bd91476c2ea 100644 (file)
--- 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 633d98ea9d69bece6e5c6de070adbdc8be59269f..324231b50db3e0bdc9655036535acc93f9f8fbe1 100644 (file)
--- 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 6a65ea039a68774d0ec0e759b04e1cdf36e7c3a6..d6f97499e10d582d9d119685f1edd472a5a91ffd 100644 (file)
--- 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);