Utilisation d'Infix/Distfix autant que possible

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

4 files changed, 75 insertions, 31 deletions

diff --git a/theories/Init/DatatypesSyntax.v b/theories/Init/DatatypesSyntax.v
index 5b57b9e0b7..8d1c2c4248 100644
--- a/theories/Init/DatatypesSyntax.v
+++ b/theories/Init/DatatypesSyntax.v
@@ -24,12 +24,20 @@ with constr0 :=
   pair [ "(" lconstr($lc1) "," lconstr($lc2) ")" ] ->
          [ (pair ? ? $lc1 $lc2) ]
 
+(*
 with constr3 :=
-  prod [ constr2($c1) "*" constr3($c2) ] -> [ (prod $c1 $c2) ].
+  prod [ constr2($c1) "*" constr3($c2) ] -> [ (prod $c1 $c2) ]
+*)
+.
+
+Infix 4 "+" sum.
+
+Infix RIGHTA 3 "*" prod.
 
 (** Pretty-printing of things in Datatypes.v *)
 
 Syntax constr
+(*
   level 4:
     sum [ (sum $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]
   ;
@@ -38,6 +46,7 @@ Syntax constr
     product [ (prod $t1 $t2) ] -> [ [<hov 0>  $t1:L [0 1] "*" $t2:E ] ]
   ;
 
+*)
   level 1:
     pair
       [ (pair $_ $_ $t3 $t4) ] -> [ [<hov 0> "(" $t3:E ","[0 1] $t4:E ")" ] ]
diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v
index 37f1bfad85..8277207996 100644
--- a/theories/Init/LogicSyntax.v
+++ b/theories/Init/LogicSyntax.v
@@ -24,9 +24,9 @@ Grammar constr constr1 :=
 | eq_expl [ "<" lconstr($l1) ">" constr0($c1) "=" constr0($c2) ] ->
           [ (eq $l1 $c1 $c2) ]
 | eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eq ? $c $c2) ]
-| IF [ "IF"   command($c1) "then" command($c2) "else" command($c3)] ->
+| IF [ "IF" constr($c1) "then" constr($c2) "else" constr($c3)] ->
      [ (IF $c1 $c2 $c3) ]
-
+(*
 with constr2 :=
   not [ "~" constr2($c) ] -> [ (not $c) ]
 
@@ -38,7 +38,7 @@ with constr7 :=
 
 with constr8 :=
   iff [ constr7($c1) "<->" constr8($c2) ] -> [ (iff $c1 $c2) ]
-
+*)
 with constr10 :=
   allexplicit [ "ALL" ident($x) ":" constr($t) "|" constr($p) ]
                           -> [ (all $t [$x : $t]$p) ]
@@ -53,12 +53,22 @@ with constr10 :=
 | ex2implicit [ "EX" ident($v) "|" constr($c1) "&" 
            constr($c2) ] -> [ (ex2 ? [$v]$c1 [$v]$c2) ].
 
+Distfix RIGHTA 2 "~ _" not.
+
+Infix RIGHTA 6 "/\\" and.
+
+Infix RIGHTA 7 "\\/" or.
+
+Infix RIGHTA 8 "<->" iff.
 
 (** Pretty-printing of things in Logic.v *)
 
 Syntax constr
   level 1:
-    equal [ (eq $_  $t1  $t2) ] -> [ [<hov 0> $t1:E [0 1]  "=" $t2:E ] ]
+    equal [ (eq $a  $t1  $t2) ] ->
+	 [ [<hov 0> (ANNOT $a) $t1:E [0 1]  "=" $t2:E ] ]
+  | annotskip [ << (ANNOT $_) >> ] -> [ ]
+  | annotmeta [ << (ANNOT (META ($NUM $n))) >> ] -> [ "<" "?" $n ">" ]
   | conj [ (conj $t1 $t2 $t3 $t4) ]
       -> [ [<hov 1> [<hov 1> "<" $t1:L "," [0 0] $t2:L ">" ] [0 0]
                     [<hov 1> "{" $t3:L "," [0 0] $t4:L "}"] ] ]
@@ -67,7 +77,7 @@ Syntax constr
                   "then " $c2:E [1 0]
                   "else " $c3:E ] ]
   ;
-
+(*
   level 2:
     not [ ~ $t1 ] -> [ [<hov 0> "~" $t1:E ] ]
   ;
@@ -83,7 +93,7 @@ Syntax constr
   level 8:
     iff [ $t1 <-> $t2 ] -> [ [<hov 0> $t1:L [0 0] "<->" $t2:E ] ]
   ;
-
+*)
   level 10:
     all_pred [ (all $_ $p) ] -> [ [<hov 4> "All " $p:L ] ]
   | all_imp [ (all $_ [$x : $T]$t) ]
diff --git a/theories/Init/Logic_TypeSyntax.v b/theories/Init/Logic_TypeSyntax.v
index c68d496d07..96d3b74b83 100644
--- a/theories/Init/Logic_TypeSyntax.v
+++ b/theories/Init/Logic_TypeSyntax.v
@@ -12,27 +12,27 @@ Require Logic_Type.
 
 (** Parsing of things in [Logic_type.v] *)
 
-Grammar command command1 :=
-  eqT_expl [ "<" lcommand($l1) ">" command0($c1) "==" command0($c2) ] ->
-          [<<(eqT $l1 $c1 $c2)>>]
-| eqT_impl [ command0($c) "==" command0($c2) ] -> [<<(eqT ? $c $c2)>>]
-| idT_expl [ "<" lcommand($l1) ">" command0($c1) "===" command0($c2) ] ->
-          [<<(identityT $l1 $c1 $c2)>>]
-| idT_impl [ command0($c) "===" command0($c2) ] -> [<<(identityT ? $c $c2)>>]
-
-with command10 :=
-  allTexplicit [ "ALLT" ident($v) ":" command($t) "|" command($c1) ]
-                          -> [<<(allT $t [$v : $t]$c1)>>]
-| allTimplicit [ "ALLT" ident($v) "|" command($c1) ] 
-                          -> [<<(allT ? [$v]$c1)>>]
-| exTexplicit [ "EXT" ident($v) ":" command($t) "|" command($c1) ]
-                          -> [<<(exT $t [$v : $t]$c1)>>]
-| exTimplicit [ "EXT" ident($v) "|" command($c1) ] 
-                          -> [<<(exT ? [$v]$c1)>>]
-| exT2explicit [ "EXT" ident($v) ":" command($t) "|" command($c1) "&"
-           command($c2) ] -> [<<(exT2 $t [$v : $t]$c1 [$v : $t]$c2)>>]
-| exT2implicit [ "EXT" ident($v) "|" command($c1) "&" 
-           command($c2) ] -> [<<(exT2 ? [$v]$c1 [$v]$c2)>>].
+Grammar constr constr1 :=
+  eqT_expl [ "<" lconstr($l1) ">" constr0($c1) "==" constr0($c2) ] ->
+          [ (eqT $l1 $c1 $c2) ]
+| eqT_impl [ constr0($c) "==" constr0($c2) ] -> [ (eqT ? $c $c2) ]
+| idT_expl [ "<" lconstr($l1) ">" constr0($c1) "===" constr0($c2) ] ->
+          [ (identityT $l1 $c1 $c2) ]
+| idT_impl [ constr0($c) "===" constr0($c2) ] -> [ (identityT ? $c $c2) ]
+
+with constr10 :=
+  allTexplicit [ "ALLT" ident($v) ":" constr($t) "|" constr($c1) ]
+                          -> [ (allT $t [$v : $t]$c1) ]
+| allTimplicit [ "ALLT" ident($v) "|" constr($c1) ] 
+                          -> [ (allT ? [$v]$c1) ]
+| exTexplicit [ "EXT" ident($v) ":" constr($t) "|" constr($c1) ]
+                          -> [ (exT $t [$v : $t]$c1) ]
+| exTimplicit [ "EXT" ident($v) "|" constr($c1) ] 
+                          -> [ (exT ? [$v]$c1) ]
+| exT2explicit [ "EXT" ident($v) ":" constr($t) "|" constr($c1) "&"
+           constr($c2) ] -> [ (exT2 $t [$v : $t]$c1 [$v : $t]$c2) ]
+| exT2implicit [ "EXT" ident($v) "|" constr($c1) "&" 
+           constr($c2) ] -> [ (exT2 ? [$v]$c1 [$v]$c2) ].
 
 (** Pretty-printing of things in [Logic_type.v] *)
 
@@ -53,7 +53,6 @@ Syntax constr
   ;
 
   level 1:
-    eqT [ (eqT $_ $c1 $c2) ] -> [ [<hov 1> $c1:E [0 0] "==" $c2:E ] ]
-
+    eqT [ (eqT $a $c1 $c2) ] -> [ [<hov 1> (ANNOT $a) $c1:E [0 0] "==" $c2:E ] ]
   | identityT [ (identityT $_ $c1 $c2) ]
        -> [ [<hov 1> $c1:E [0 0] "===" $c2:E ] ].
diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v
index 3aadaaec73..8d09ccd9bc 100644
--- a/theories/Init/SpecifSyntax.v
+++ b/theories/Init/SpecifSyntax.v
@@ -13,7 +13,7 @@ Require Specif.
 
 (** Parsing of things in Specif.v *)
 
-Grammar constr constr1 :=
+Grammar constr constr3 :=
   sig [ "{" lconstr($lc) ":" lconstr($c1) "|" lconstr($c2) "}" ]
        -> [ (sig $c1 [$lc : $c1]$c2) ]
 
@@ -28,6 +28,7 @@ Grammar constr constr1 :=
              "&" lconstr($c2) "&" lconstr($c3) "}" ]
        -> [ (sigS2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3) ].
 
+(*
 Grammar constr constr1: ast :=
   squash [ "{" lconstr($lc) "}" ] -> [(SQUASH $lc)].
 
@@ -42,6 +43,31 @@ Grammar constr lassoc_constr4 :=
             esac
       | $_           -> [ (sum $c1 $c2) ]           (* c1+c2 *)
       esac.
+*)
+
+Grammar constr constr3 :=
+  sumbool [ "{" lconstr($lc) "}" "+" "{" lconstr($lc2) "}" ] -> 
+    [ (sumbool $lc $lc2) ].
+
+Grammar constr lassoc_constr4 :=
+  sumor [ lassoc_constr4($c1) "+" "{" lconstr($c2) "}" ] ->
+    [ (sumor $c1 $c2) ]
+
+| sumsig [ lassoc_constr4($c) "+" "{" lconstr($lc) ":" lconstr($c1) "|" lconstr($c2) "}" ] ->
+    [ (sum $c (sig $c1 [$lc : $c1]$c2)) ]
+
+| sumsig2 [ lassoc_constr4($c) "+" "{" lconstr($lc) ":" lconstr($c1)
+           "|" lconstr($c2) "&" lconstr($c3) "}" ]
+       -> [ (sum $c (sig2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3)) ]
+
+| sumsigS [ lassoc_constr4($c) "+" "{" lconstr($lc) ":" lconstr($c1) "&" lconstr($c2) "}" ]
+       -> [ (sum $c (sigS $c1 [$lc : $c1]$c2)) ]
+
+| sumsigS2 [ lassoc_constr4($c) "+" "{" lconstr($lc) ":" lconstr($c1)
+             "&" lconstr($c2) "&" lconstr($c3) "}" ]
+       -> [ (sum $c (sigS2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3)) ]
+.
+
 
 (** Pretty-printing of things in Specif.v *)