Un hack camlp4 qui marche à tous les coups pour continuer à parser '(n)' comme un entier de nat

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3222 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 24 insertions, 58 deletions

diff --git a/parsing/g_cases.ml4 b/parsing/g_cases.ml4
index 6bee39b122..e84a890920 100644
--- a/parsing/g_cases.ml4
+++ b/parsing/g_cases.ml4
@@ -18,6 +18,10 @@ GEXTEND Gram
 
   pattern:
     [ [ qid = global -> qid
+      (* Hack to parse syntax "(n)" as a natural number *)
+      | "("; G_constr.test_int_rparen; n = INT; ")" ->
+ 	  let n = Coqast.Str (loc,n) in
+          <:ast< (PATTDELIMITERS "nat_scope" (PATTNUMERAL $n)) >>
       | "("; p = compound_pattern; ")" -> p
       | n = INT ->
 	  let n = Coqast.Str (loc,n) in <:ast< (PATTNUMERAL $n) >>
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index df8c7bbeef..620b6a8002 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -13,6 +13,20 @@
 open Pcoq
 open Constr
 
+(* Hack to parse "(n)" as nat without conflicts with the (useless) *)
+(* admissible notation "(n)" *)
+let test_int_rparen =
+  Gram.Entry.of_parser "test_int_rparen"
+    (fun strm ->
+      match Stream.npeek 1 strm with
+        | [("INT", _)] ->
+            begin match Stream.npeek 2 strm with
+              | [_; ("", ")")] -> ()
+              | _ -> raise Stream.Failure
+            end
+        | _ -> raise Stream.Failure)
+
+
 GEXTEND Gram
   GLOBAL: constr0 constr1 constr2 constr3 lassoc_constr4 constr5
           constr6 constr7 constr8 constr9 constr10 lconstr constr
@@ -71,6 +85,10 @@ GEXTEND Gram
       | "?"; n = Prim.natural ->
 	  let n = Coqast.Num (loc,n) in <:ast< (META $n) >>
       | bl = binders; c = constr -> <:ast< ($ABSTRACT "LAMBDALIST" $bl $c) >>
+      (* Hack to parse syntax "(n)" as a natural number *)
+      | "("; test_int_rparen; n = INT; ")" ->
+ 	  let n = Coqast.Str (loc,n) in
+          <:ast< (DELIMITERS "nat_scope" (NUMERAL $n)) >>
       | "("; lc1 = lconstr; ":"; c = constr; body = product_tail ->
           let id = Ast.coerce_to_var lc1 in
             <:ast< (PROD $c [$id]$body) >>
@@ -147,7 +165,8 @@ GEXTEND Gram
         IDENT "if"; c1 = constr; IDENT "then";
         c2 = constr; IDENT "else"; c3 = constr ->
           <:ast< (IF $l1 $c1 $c2 $c3) >>
-      | c = constr0 -> c ] ]
+      | c = constr0 -> c
+    ] ]
   ;
   constr2: (* ~ will be here *)
     [ [ c = constr1 -> c ] ]
diff --git a/theories/Init/PeanoSyntax.v b/theories/Init/PeanoSyntax.v
index 0782c71880..f42fccfd90 100644
--- a/theories/Init/PeanoSyntax.v
+++ b/theories/Init/PeanoSyntax.v
@@ -50,60 +50,3 @@ Syntax constr
 .
 
 End nat_scope.
-
-Grammar constr constr0 :=
-  natural_nat0 [ "(" "0" ")" ] -> [ 'N: 0 ' ]
-| natural_nat1 [ "(" "1" ")" ] -> [ 'N: 1 ' ]
-| natural_nat2 [ "(" "2" ")" ] -> [ 'N: 2 ' ]
-| natural_nat3 [ "(" "3" ")" ] -> [ 'N: 3 ' ]
-| natural_nat4 [ "(" "4" ")" ] -> [ 'N: 4 ' ]
-| natural_nat5 [ "(" "5" ")" ] -> [ 'N: 5 ' ]
-| natural_nat6 [ "(" "6" ")" ] -> [ 'N: 6 ' ]
-| natural_nat7 [ "(" "7" ")" ] -> [ 'N: 7 ' ]
-| natural_nat8 [ "(" "8" ")" ] -> [ 'N: 8 ' ]
-| natural_nat9 [ "(" "9" ")" ] -> [ 'N: 9 ' ]
-| natural_nat10 [ "(" "10" ")" ] -> [ 'N: 10 ' ]
-| natural_nat11 [ "(" "11" ")" ] -> [ 'N: 11 ' ]
-| natural_nat12 [ "(" "12" ")" ] -> [ 'N: 12 ' ]
-| natural_nat13 [ "(" "13" ")" ] -> [ 'N: 13 ' ]
-| natural_nat14 [ "(" "14" ")" ] -> [ 'N: 14 ' ]
-| natural_nat15 [ "(" "15" ")" ] -> [ 'N: 15 ' ]
-| natural_nat16 [ "(" "16" ")" ] -> [ 'N: 16 ' ]
-| natural_nat17 [ "(" "17" ")" ] -> [ 'N: 17 ' ]
-| natural_nat18 [ "(" "18" ")" ] -> [ 'N: 18 ' ]
-| natural_nat19 [ "(" "19" ")" ] -> [ 'N: 19 ' ]
-| natural_nat20 [ "(" "20" ")" ] -> [ 'N: 20 ' ]
-| natural_nat21 [ "(" "21" ")" ] -> [ 'N: 21 ' ]
-| natural_nat22 [ "(" "22" ")" ] -> [ 'N: 22 ' ]
-| natural_nat23 [ "(" "23" ")" ] -> [ 'N: 23 ' ]
-| natural_nat24 [ "(" "24" ")" ] -> [ 'N: 24 ' ]
-| natural_nat25 [ "(" "25" ")" ] -> [ 'N: 25 ' ]
-| natural_nat26 [ "(" "26" ")" ] -> [ 'N: 26 ' ]
-| natural_nat27 [ "(" "27" ")" ] -> [ 'N: 27 ' ]
-| natural_nat28 [ "(" "28" ")" ] -> [ 'N: 28 ' ]
-| natural_nat29 [ "(" "29" ")" ] -> [ 'N: 29 ' ]
-| natural_nat30 [ "(" "30" ")" ] -> [ 'N: 30 ' ]
-(* ... *)
-| natural_nat48 [ "(" "48" ")" ] -> [ 'N: 48 ' ]
-| natural_nat80 [ "(" "80" ")" ] -> [ 'N: 80 ' ]
-| natural_nat81 [ "(" "81" ")" ] -> [ 'N: 81 ' ]
-| natural_nat91 [ "(" "91" ")" ] -> [ 'N: 91 ' ]
-| natural_nat95 [ "(" "95" ")" ] -> [ 'N: 95 ' ]
-| natural_nat100 [ "(" "100" ")" ] -> [ 'N: 100 ' ]
-| natural_nat110 [ "(" "110" ")" ] -> [ 'N: 110 ' ]
-.
-
-Grammar constr pattern : cases_pattern :=
-  natural_pat0 [ "(" "0" ")" ] -> [ 'N: 0 ' ]
-| natural_pat1 [ "(" "1" ")" ] -> [ 'N: 1 ' ]
-| natural_pat2 [ "(" "2" ")" ] -> [ 'N: 2 ' ]
-| natural_pat3 [ "(" "3" ")" ] -> [ 'N: 3 ' ]
-| natural_pat4 [ "(" "4" ")" ] -> [ 'N: 4 ' ]
-| natural_pat5 [ "(" "5" ")" ] -> [ 'N: 5 ' ]
-| natural_pat6 [ "(" "6" ")" ] -> [ 'N: 6 ' ]
-| natural_pat7 [ "(" "7" ")" ] -> [ 'N: 7 ' ]
-| natural_pat8 [ "(" "8" ")" ] -> [ 'N: 8 ' ]
-| natural_pat9 [ "(" "9" ")" ] -> [ 'N: 9 ' ]
-| natural_pat10 [ "(" "10" ")" ] -> [ 'N: 10 ' ]
-| natural_pat11 [ "(" "11" ")" ] -> [ 'N: 11 ' ]
-.