Généralisation de l'utilisation de Notation

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

1 files changed, 43 insertions, 112 deletions

diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v
index 8d32dcfc86..a617373c82 100644
--- a/theories/Init/SpecifSyntax.v
+++ b/theories/Init/SpecifSyntax.v
@@ -8,118 +8,49 @@
 
 (*i $Id$ i*)
 
-Require Datatypes.
-Require LogicSyntax.
+Require DatatypesSyntax.
 Require Specif.
 
-(** Parsing of things in Specif.v *)
-
-(* To accept {x:A|P}*B without parentheses *)
-Grammar constr constr3 :=
-  sigprod [ "{" lconstr($lc) ":" lconstr($c1) "|" lconstr($c2) "}"
-            "*" constr3($c) ]
-       -> [ (prod (sig $c1 [$lc : $c1]$c2) $c) ]
-
-| sig2prod [ "{" lconstr($lc) ":" lconstr($c1)
-           "|" lconstr($c2) "&" lconstr($c3) "}" "*" constr3($c) ]
-       -> [ (prod (sig2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3) $c) ]
-
-| sigSprod [ "{" lconstr($lc) ":" lconstr($c1) "&" lconstr($c2) "}"
-         "*" constr3($c)]
-       -> [ (prod (sigS $c1 [$lc : $c1]$c2) $c) ]
-
-| sigS2prod [ "{" lconstr($lc) ":" lconstr($c1)
-             "&" lconstr($c2) "&" lconstr($c3) "}" "*" constr3($c) ]
-       -> [ (prod (sigS2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3) $c) ].
-
-(* To factor with {A}+{B} *)
-Grammar constr constr3 :=
-  sig [ "{" lconstr($lc) ":" lconstr($c1) "|" lconstr($c2) "}" ]
-       -> [ (sig $c1 [$lc : $c1]$c2) ]
-
-| sig2 [ "{" lconstr($lc) ":" lconstr($c1)
-           "|" lconstr($c2) "&" lconstr($c3) "}" ]
-       -> [ (sig2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3) ]
-
-| sigS [ "{" lconstr($lc) ":" lconstr($c1) "&" lconstr($c2) "}" ]
-       -> [ (sigS $c1 [$lc : $c1]$c2) ]
-
-| sigS2 [ "{" lconstr($lc) ":" lconstr($c1)
-             "&" lconstr($c2) "&" lconstr($c3) "}" ]
-       -> [ (sigS2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3) ].
-
-Notation 3 "{ x } + { y }" (sumbool x y).
-Notation LEFTA 4 " x + { y }" (sumor x y).
-
-Grammar constr lassoc_constr4 :=
-  sumsig [ lassoc_constr4($c) "+" "{" lconstr($lc) ":" constr($c1) "|" lconstr($c2) "}" ] ->
-    [ (sum $c (sig $c1 [$lc : $c1]$c2)) ]
-
-| sumsig2 [ lassoc_constr4($c) "+" "{" lconstr($lc) ":" constr($c1)
-           "|" lconstr($c2) "&" lconstr($c3) "}" ]
-       -> [ (sum $c (sig2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3)) ]
-
-| sumsigS [ lassoc_constr4($c) "+" "{" lconstr($lc) ":" constr($c1) "&" lconstr($c2) "}" ]
-       -> [ (sum $c (sigS $c1 [$lc : $c1]$c2)) ]
-
-| sumsigS2 [ lassoc_constr4($c) "+" "{" lconstr($lc) ":" constr($c1)
-             "&" lconstr($c2) "&" lconstr($c3) "}" ]
-       -> [ (sum $c (sigS2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3)) ]
-.
-
-
-(** Pretty-printing of things in Specif.v *)
-
-Syntax constr
-  level 1:
-(** Pretty-printing of [sig] *)
-  | sig_nb [ (sig $c1 [_:$1]$c2) ]
-      -> [ [<hov 0> "{_:" $c1:E " |" [1 3] $c2:E "}" ] ]
-  | sigma_b [ (sig $c1 [$id:$1]$c2) ]
-      -> [ [<hov 0> "{" $id ":" $c1:E " |" [1 3] $c2:E "}" ] ]
-
-(** Pretty-printing of [sig2] *)
-  | sig2_b_b
-      [ (sig2 $c1 [$id:$c1]$c2 [$id:$c1]$c3) ]
-       -> [ [<hov 0> "{"$id":"$c1:E"|" [1 3]$c2:E [1 3]"& "$c3:E "}" ] ]
-  | sig2_nb_b
-      [ (sig2 $c1 [_:$c1]$c2 [$id:$c1]$c3) ]
-       -> [ [<hov 0> "{"$id":"$c1:E"|" [1 3]$c2:E [1 3]"& "$c3:E "}" ] ]
-  | sig2_b_nb
-      [ (sig2 $c1 [$id:$c1]$c2 [_:$c1]$c3) ]
-       -> [ [<hov 0> "{"$id":"$c1:E"|" [1 3]$c2:E [1 3]"& "$c3:E "}" ] ]
-  | sig2_nb_nb
-      [ (sig2 $c1 [_:$c1]$c2 [_:$c1]$c3) ]
-       -> [ [<hov 0> "{_:"$c1:E "|" [1 3] $c2:E [1 3]"& " $c3:E "}" ] ]
-
-(** Pretty-printing of [sigS] *)
-  | sigS_nb [ (sigS $c1 [_:$c1]$c2) ]
-       -> [ [<hov 0> "{_:" $c1:E [1 3]"& " $c2:E  "}" ] ]
-  | sigS_b [ (sigS $c1 [$id:$c1]$c2) ]
-       -> [ [<hov 0> "{" $id  ":" $c1:E [1 3] "& " $c2:E "}" ] ]
-
-(** Pretty-printing of [sigS2] *)
-  | sigS2_b_b
-      [ (sigS2 $c1 [$id:$c1]$c2 [$id:$c1]$c3) ]
-       -> [ [<hov 0> "{"$id ":" $c1:E [1 3]"& "$c2:E [1 3]"& "$c3:E "}" ] ]
-  | sigS2_nb_b
-      [ (sigS2 $c1 [_:$c1]$c2 [$id:$c1]$c3) ]
-       -> [ [<hov 0> "{"$id ":" $c1:E [1 3]"& "$c2:E [1 3]"& "$c3:E "}" ] ]
-  | sigS2_b_nb
-      [ (sigS2 $c1 [$id:$c1]$c2 [_:$c1]$c3) ]
-       -> [ [<hov 0> "{"$id ":" $c1:E [1 3]"& "$c2:E [1 3]"& "$c3:E "}" ] ]
-  | sigS2_nb_nb
-      [ (sigS2 $c1 [_:$c1]$c2 [_:$c1]$c3) ]
-       -> [ [<hov 0> "{_:"$c1:E [1 3]"& "$c2:E [1 3]"& "$c3:E "}" ] ]
-
-(** Pretty-printing of [projS1] and [projS2] *)
-  | projS1_imp [ (projS1 ? ? $a) ] -> ["(ProjS1 " $a:E ")"]  
-  | projS2_imp [ (projS2 ? ? $a) ] -> ["(ProjS2 " $a:E ")"]
-
-(** Pretty-printing of [except] *)
-  | Except_imp [ (except $1 $t2) ] -> [ [<hov 0> "Except " $t2 ] ]
-
-(** Pretty-printing of [error] and [value] *)
-  | Error_imp [ (error $t1) ]     -> [ [<hov 0> "Error" ] ]
-  | Value_imp [ (value $t1 $t2) ] -> [ [<hov 0> "(Value " $t2 ")" ] ].
+(** Symbolic notations for things in [Specif.v] *)
+
+(* At level 1 to factor with {x:A|P} etc *)
+Notation "{ A } + { B }" := (sumbool A B)
+  (at level 1, A at level 10, B at level 10).
+
+Notation "A + { B }" := (sumor A B)
+  (at level 4, B at level 10, left associativity).
+
+Notation ProjS1 := (projS1 ?).
+Notation ProjS2 := (projS2 ?).
+Notation Error  := (error ?).
+Notation Value  := (value ?).
+Notation Except := (except ?).
+
+Notation "{ x : A  |  P }"       := (sig A [x:A]P)
+  (at level 1, x at level 10).
+
+Notation "{ x : A  |  P  &  Q }" := (sig2 A [x:A]P [x:A]Q)
+  (at level 1, x at level 10).
+
+Notation "{ x : A  &  P }"       := (sigS A [x:A]P)
+  (at level 1, x at level 10).
+
+Notation "{ x : A  &  P  &  Q }" := (sigS2 A [x:A]P [x:A]Q)
+  (at level 1, x at level 10).
+
+(** Extra factorization of parsing rules *)
+
+(* Factorizing "sumor" at level 4 to parse B+{x:A|P} without parentheses *)
+
+Notation "B + { x : A | P }"     := B + ({x:A | P})
+  (at level 4, x at level 10, left associativity, only parsing).
+
+Notation "B + { x : A | P & Q }" := B + ({x:A | P & Q})
+  (at level 4, x at level 10, left associativity, only parsing).
+
+Notation "B + { x : A & P }"     := B + ({x:A & P})
+  (at level 4, x at level 10, left associativity, only parsing).
+
+Notation "B + { x : A & P & Q }" := B + ({x:A & P & Q})
+  (at level 4, x at level 10, left associativity, only parsing).