From 338dd533c27374771b0e880dcb74fba972dc79f1 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 13 Oct 2002 13:15:45 +0000 Subject: 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 --- theories/Arith/Arith.v | 16 ----------- theories/Arith/ArithSyntax.v | 6 ---- theories/Arith/Plus.v | 3 +- theories/Init/PeanoSyntax.v | 68 ++++++++++++++++++++++++++++++++++++++++++++ theories/Init/Prelude.v | 1 + theories/Reals/Rsyntax.v | 43 +++++++++++++++++++++++++--- theories/ZArith/Zsyntax.v | 35 ++++++++++++++++++++++- 7 files changed, 144 insertions(+), 28 deletions(-) delete mode 100644 theories/Arith/ArithSyntax.v create mode 100644 theories/Init/PeanoSyntax.v 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 *) +(* 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) ] -> [[ "``" (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 <>)>>] -> ["0"] | Rone_inside [<<(REXPR <>)>>] -> ["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) ] -> [[ "`" (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. -- cgit v1.2.3