Mise en place d'ensembles de notations symboliques pour nat, Z et R

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

7 files changed, 144 insertions, 28 deletions

diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v
index 7af85c65a..13c17aabb 100755
--- a/theories/Arith/Arith.v
+++ b/theories/Arith/Arith.v
@@ -18,19 +18,3 @@ Require Export Between.
 Require Export Minus.
 Require Export Peano_dec.
 Require Export Compare_dec.
-
-Axiom My_special_variable : nat -> nat.
-
-Grammar nat number :=.
-
-Grammar constr constr10 :=
-  natural_nat [ nat:number($c) ] -> [$c].
-
-Grammar constr pattern :=
-  natural_pat [ nat:pat_number($c) ] -> [$c].
-
-Syntax constr
-  level 10:
-  S [ (S $p) ] -> [$p:"nat_printer":9]
-| O [ O ] -> [ "0" ]
-.
diff --git a/theories/Arith/ArithSyntax.v b/theories/Arith/ArithSyntax.v
deleted file mode 100644
index cd762d425..000000000
--- a/theories/Arith/ArithSyntax.v
+++ /dev/null
@@ -1,6 +0,0 @@
-Infix 4 "+" plus.
-Infix 3 "*" mult.
-Infix 1 "<=" le.
-Infix 1 "<" lt.
-Infix 1 ">=" ge.
-(* Infix 1 ">" gt.*)
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index 5263cb375..3ad37d13a 100755
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -12,7 +12,8 @@
 
 Require Le.
 Require Lt.
-Require ArithSyntax.
+
+Import nat_scope.
 
 Lemma plus_sym : (n,m:nat)(n+m)=(m+n).
 Proof.
diff --git a/theories/Init/PeanoSyntax.v b/theories/Init/PeanoSyntax.v
new file mode 100644
index 000000000..cea2137de
--- /dev/null
+++ b/theories/Init/PeanoSyntax.v
@@ -0,0 +1,68 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$ *)
+
+Require Datatypes.
+Require Peano.
+
+Axiom My_special_variable : nat -> nat.
+
+Grammar nat number :=.
+
+Grammar constr constr10 :=
+  natural_nat [ nat:number($c) ] -> [$c].
+
+Grammar constr pattern :=
+  natural_pat [ nat:pat_number($c) ] -> [$c].
+
+Syntax constr
+  level 10:
+  S [ (S $p) ] -> [$p:"nat_printer":9]
+| O [ O ] -> [ "0" ]
+.
+
+
+(* For parsing/printing based on scopes *)
+Module nat_scope.
+
+Delimiters "'N:" nat_scope "'". (* "[N", "[N:", "]]" are conflicting *)
+
+Infix 3 "+" plus : nat_scope.
+Infix 2 "*" mult : nat_scope.
+Infix NONA 4 "<=" le : nat_scope.
+Infix NONA 4 "<" lt : nat_scope.
+Infix NONA 4 ">=" ge : nat_scope.
+(* Infix 4 ">" gt : nat_scope. (* Conflicts with "<..>Cases ... " *) *)
+
+(* Warning: this hides sum and prod and breaks sumor symbolic notation *)
+Open Scope nat_scope.
+
+(* For (partial) compatibility when parsing Z ` ` and R `` `` grammars *)
+(* while nat_scope is open *)
+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 ' ]
+.
+
+Syntax constr
+  level 0:
+  S' [ (S $p) ] -> [$p:"nat_printer_S":9]
+| O' [ O ] -> [ _:"nat_printer_O" ]
+.
+
+End nat_scope.
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 5f647f373..6cdc8d0b4 100755
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -15,4 +15,5 @@ Require Export LogicSyntax.
 Require Export Specif.
 Require Export SpecifSyntax.
 Require Export Peano.
+Require Export PeanoSyntax.
 Require Export Wf.
diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v
index e13bf9228..e18cfdd76 100644
--- a/theories/Reals/Rsyntax.v
+++ b/theories/Reals/Rsyntax.v
@@ -61,7 +61,7 @@ with rexpr0 : constr :=
 
 with meta : ast :=
 | rimpl [ "?" ] -> [ (ISEVAR) ]
-| rmeta [ "?" prim:numarg($n) ] -> [ (META $n) ]
+| rmeta [ "?" constr:numarg($n) ] -> [ (META $n) ]
 
 with rapplication : constr :=
   apply [ rapplication($p) rexpr($c1) ] -> [ ($p $c1) ]
@@ -107,8 +107,8 @@ Syntax constr
   | Rlt_Rlt [ (Rlt $n1 $n2)/\(Rlt $n2 $n3) ] ->
       [[<hov 0> "``" (REXPR $n1) [1 0] "< " (REXPR $n2)
                                 [1 0] "< " (REXPR $n3) "``"]]
-  | Rzero [ R0 ] -> ["``0``"]
-  | Rone [ R1 ] -> ["``1``"]
+  | Rzero [ R0 ] -> [ "``0``" ]
+  | Rone [ R1 ] -> [ "``1``" ]
   ;
 
   level 7:
@@ -188,4 +188,39 @@ Syntax constr
   level 0:
     Rzero_inside [<<(REXPR <<R0>>)>>] -> ["0"]
   | Rone_inside [<<(REXPR <<R1>>)>>] -> ["1"]
-  | Rconst_inside [<<(REXPR <<(Rplus R1 $r)>>)>>] -> [$r:"r_printer"].
+  | Rconst_inside [<<(REXPR <<(Rplus R1 $r)>>)>>] -> [$r:"r_printer"]
+.
+
+(* For parsing/printing based on scopes *)
+Module R_scope.
+
+Delimiters "'R:" R_scope "'".
+Infix NONA 4 "<=" Rle : R_scope.
+Infix NONA 4 "<"  Rlt : R_scope.
+Infix NONA 4 ">=" Rge : R_scope.
+(*Infix NONA 4 ">"  Rgt : R_scope. (* Conflicts with "<..>Cases ... " *) *)
+Infix 3 "+" Rplus : R_scope.
+Infix 3 "-" Rminus : R_scope.
+Infix 2 "*" Rmult : R_scope.
+Distfix 0 "- _" Ropp : R_scope.
+Notation NONA 4 "x == y == z" (eqT R x y)/\(eqT R y z) : R_scope.
+Notation NONA 4 "x <= y <= z" (Rle x y)/\(Rle y z) : R_scope.
+Notation NONA 4 "x <= y <  z" (Rle x y)/\(Rlt y z) : R_scope.
+Notation NONA 4 "x <  y <  z" (Rlt x y)/\(Rlt y z) : R_scope.
+Notation NONA 4 "x <  y <= z" (Rlt x y)/\(Rle y z) : R_scope.
+Notation NONA 4 "x <> y"  ~(eqT R x y) : R_scope.
+Infix LEFTA 2 "/" Rdiv : R_scope.
+Distfix 0 "/ _" Rinv : R_scope.
+
+(* Warning: this hides sum and prod and breaks sumor symbolic notation *)
+Open Scope R_scope.
+
+Syntax constr
+  level 0:
+    Rzero' [ R0 ] -> [ _:"r_printer_R0" ]
+  | Rone' [ R1 ] -> [ _:"r_printer_R1" ]
+  | Rconst' [(Rplus R1 $r)] -> [$r:"r_printer_Rplus1"]
+  | Ropp' [(Ropp $n)] -> [ $n:"r_printer_Ropp" ]
+.
+
+End R_scope.
diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v
index a63503249..8314d25a5 100644
--- a/theories/ZArith/Zsyntax.v
+++ b/theories/ZArith/Zsyntax.v
@@ -114,7 +114,7 @@ Syntax constr
   | Zlt_Zlt [ (Zlt $n1 $n2)/\(Zlt $n2 $n3) ] ->
       [[<hov 0> "`" (ZEXPR $n1) [1 0] "< " (ZEXPR $n2)
                                 [1 0] "< " (ZEXPR $n3) "`"]]
-  | ZZero [ ZERO ] -> ["`0`"]
+  | ZZero [ ZERO ] -> [ "`0`" ]
   | ZPos [ (POS $r) ] -> [$r:"positive_printer":9]
   | ZNeg [ (NEG $r) ] -> [$r:"negative_printer":9]
   ;
@@ -215,3 +215,36 @@ Syntax constr
   | ZPos_inside [ << (ZEXPR <<(POS $p)>>) >>] -> [$p:"positive_printer_inside"]
   | ZNeg_inside [ << (ZEXPR <<(NEG $p)>>) >>] -> [$p:"negative_printer_inside"]
 .
+
+(* For parsing/printing based on scopes *)
+Module Z_scope.
+
+Delimiters "'Z:" Z_scope "'".
+Infix NONA 4 "<=" Zle : Z_scope.
+Infix NONA 4 "<"  Zlt : Z_scope.
+Infix NONA 4 ">=" Zge : Z_scope.
+(*Infix NONA 4 ">"  Zgt : Z_scope. (* Conflicts with "<..>Cases ... " *) *)
+Infix NONA 4 "?=" Zcompare : Z_scope.
+Infix 3 "+" Zplus : Z_scope.
+Infix 3 "-" Zminus : Z_scope.
+Infix 2 "*" Zmult : Z_scope.
+Distfix 0 "- _" Zopp : Z_scope.
+Notation NONA 4 "x <= y <= z" (Zle x y)/\(Zle y z) : Z_scope.
+Notation NONA 4 "x <= y <  z" (Zle x y)/\(Zlt y z) : Z_scope.
+Notation NONA 4 "x <  y <  z" (Zlt x y)/\(Zlt y z) : Z_scope.
+Notation NONA 4 "x <  y <= z" (Zlt x y)/\(Zle y z) : Z_scope.
+Notation NONA 4 "x <> y"      ~(eq Z x y)          : Z_scope.
+(* Notation NONA 1 "| x |" (Zabs x) : Z_scope.(* "|" conflicts with THENS *)*)
+Notation NONA 1 "|| x ||" (Zabs x) : Z_scope.
+
+(* Warning: this hides sum and prod and breaks sumor symbolic notation *)
+Open Scope Z_scope.
+
+Syntax constr
+  level 0:
+  | ZZero' [ ZERO ] -> [dummy:"z_printer_ZERO"]
+  | ZPos' [ (POS $r) ] -> [$r:"z_printer_POS":9]
+  | ZNeg' [ (NEG $r) ] -> [$r:"z_printer_NEG":9]
+.
+
+End Z_scope.