Déplacement de + et * aux niveaux de précédence 7 et 6

Utilisation du parseur de constr pour les productions des règles de syntaxe


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

1 files changed, 29 insertions, 71 deletions

diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v
index 76ab4b3b9b..b64278f7dc 100644
--- a/theories/Init/SpecifSyntax.v
+++ b/theories/Init/SpecifSyntax.v
@@ -14,74 +14,57 @@ Require Specif.
 (** Parsing of things in Specif.v *)
 
 (* To accept {x:A|P}*B without parentheses *)
-Grammar constr constr3 :=
-  sig [ "{" lconstr($lc) ":" lconstr($c1) "|" lconstr($c2) "}" "*" constr3($c) ]
+Grammar constr constr6 :=
+  sig [ "{" lconstr($lc) ":" constr($c1) "|" lconstr($c2) "}" "*" constr6($c) ]
        -> [ (prod (sig $c1 [$lc : $c1]$c2) $c) ]
 
 | sig2 [ "{" lconstr($lc) ":" lconstr($c1)
-           "|" lconstr($c2) "&" lconstr($c3) "}" "*" constr3($c) ]
+           "|" lconstr($c2) "&" lconstr($c3) "}" "*" constr6($c) ]
        -> [ (prod (sig2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3) $c) ]
 
 | sigS [ "{" lconstr($lc) ":" lconstr($c1) "&" lconstr($c2) "}"
-         "*" constr3($c)]
+         "*" constr6($c)]
        -> [ (prod (sigS $c1 [$lc : $c1]$c2) $c) ]
 
 | sigS2 [ "{" lconstr($lc) ":" lconstr($c1)
-             "&" lconstr($c2) "&" lconstr($c3) "}" "*" constr3($c) ]
+             "&" lconstr($c2) "&" lconstr($c3) "}" "*" constr6($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) "}" ]
+Grammar constr constr6 :=
+  sig [ "{" lconstr($lc) ":" constr($c1) "|" lconstr($c2) "}" ]
        -> [ (sig $c1 [$lc : $c1]$c2) ]
 
-| sig2 [ "{" lconstr($lc) ":" lconstr($c1)
+| sig2 [ "{" lconstr($lc) ":" constr($c1)
            "|" lconstr($c2) "&" lconstr($c3) "}" ]
        -> [ (sig2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3) ]
 
-| sigS [ "{" lconstr($lc) ":" lconstr($c1) "&" lconstr($c2) "}" ]
+| sigS [ "{" lconstr($lc) ":" constr($c1) "&" lconstr($c2) "}" ]
        -> [ (sigS $c1 [$lc : $c1]$c2) ]
 
-| sigS2 [ "{" lconstr($lc) ":" lconstr($c1)
+| sigS2 [ "{" lconstr($lc) ":" constr($c1)
              "&" lconstr($c2) "&" lconstr($c3) "}" ]
        -> [ (sigS2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3) ].
 
-(*
-Grammar constr constr1: ast :=
-  squash [ "{" lconstr($lc) "}" ] -> [(SQUASH $lc)].
-
-Grammar constr lassoc_constr4 :=
-  squash_sum
-  [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] ->
-      case [$c2] of
-        (SQUASH $T2) ->
-            case [$c1] of
-              (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *)
-            | $_           -> [ (sumor $c1 $T2) ]   (* c1+{T2} *)
-            esac
-      | $_           -> [ (sum $c1 $c2) ]           (* c1+c2 *)
-      esac.
-*)
-
-Grammar constr constr3 :=
+Grammar constr constr6 :=
   sumbool [ "{" lconstr($lc) "}" "+" "{" lconstr($lc2) "}" ] -> 
     [ (sumbool $lc $lc2) ].
 
-Grammar constr lassoc_constr4 :=
-  sumor [ lassoc_constr4($c1) "+" "{" lconstr($c2) "}" ] ->
+Grammar constr constr7 :=
+  sumor [ constr7($c1) "+" "{" lconstr($c2) "}" ] ->
     [ (sumor $c1 $c2) ]
 
-| sumsig [ lassoc_constr4($c) "+" "{" lconstr($lc) ":" lconstr($c1) "|" lconstr($c2) "}" ] ->
+| sumsig [ constr7($c) "+" "{" lconstr($lc) ":" constr($c1) "|" lconstr($c2) "}" ] ->
     [ (sum $c (sig $c1 [$lc : $c1]$c2)) ]
 
-| sumsig2 [ lassoc_constr4($c) "+" "{" lconstr($lc) ":" lconstr($c1)
+| sumsig2 [ constr7($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) ":" lconstr($c1) "&" lconstr($c2) "}" ]
+| sumsigS [ constr7($c) "+" "{" lconstr($lc) ":" constr($c1) "&" lconstr($c2) "}" ]
        -> [ (sum $c (sigS $c1 [$lc : $c1]$c2)) ]
 
-| sumsigS2 [ lassoc_constr4($c) "+" "{" lconstr($lc) ":" lconstr($c1)
+| sumsigS2 [ constr7($c) "+" "{" lconstr($lc) ":" constr($c1)
              "&" lconstr($c2) "&" lconstr($c3) "}" ]
        -> [ (sum $c (sigS2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3)) ]
 .
@@ -90,70 +73,45 @@ Grammar constr lassoc_constr4 :=
 (** Pretty-printing of things in Specif.v *)
 
 Syntax constr
-(** Default pretty-printing rules *)
-  level 10:
-    sig_var
-      [<<(ABSTR_B_NB $c1 $c2)>>] -> [ [<hov 0> "sig " $c1:L [1 1] $c2:L ] ]
-  | sig2_var
-      [<<(Sig2_ABSTR_B_NB $c1 $c2 $c3)>>]
-       -> [ [<hov 0> "sig2 " $c1:L [1 1] $c2:L [1 1] $c3:L] ]
-  | sigS_var
-      [<<(SigS_ABSTR_B_NB $c1 $c2)>>] -> [ [<hov 0> "sigS " $c1:L [1 1] $c2:L ] ]
-  | sigS2_var [<<(SigS2_ABSTR_B_NB $c1 $c2 $c3)>>]
-       -> [ [<hov 0> "sigS2 " $c1:L [1 1] $c2:L [1 1] $c3:L] ]
-  ;
-
   level 1:
 (** Pretty-printing of [sig] *)
-    sig  [ (sig $c1 $c2) ] -> [ (ABSTR_B_NB  $c1 $c2):E ]
-  | sig_nb [ << (ABSTR_B_NB $c1 (LAMBDALIST $c1 [<>]$c2)) >> ]
+  | sig_nb [ (sig $c1 [_:$1]$c2) ]
       -> [ [<hov 0> "{_:" $c1:E " |" [1 3] $c2:E "}" ] ]
-  | sigma_b [ << (ABSTR_B_NB $c1 (LAMBDALIST $c1 [$id]$c2)) >> ]
+  | sigma_b [ (sig $c1 [$id:$1]$c2) ]
       -> [ [<hov 0> "{" $id ":" $c1:E " |" [1 3] $c2:E "}" ] ]
 
 (** Pretty-printing of [sig2] *)
-  | sig2 [ (sig2 $c1 $c2 $c3) ] -> [ (Sig2_ABSTR_B_NB  $c1 $c2 $c3):E ]
   | sig2_b_b
-      [ << (Sig2_ABSTR_B_NB $c1 (LAMBDALIST $c1 [$id]$c2)
-                            (LAMBDALIST $c1 [$id]$c3)) >> ]
+      [ (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_ABSTR_B_NB $c1 (LAMBDALIST $c1 [<>]$c2)
-                            (LAMBDALIST  $c1 [$id]$c3)) >> ]
+      [ (sig2 $c1 [_:$c1]$c2 [$id:$c1]$c3) ]
        -> [ [<hov 0> "{"$id":"$c1:E"|" [1 3]$c2:E [1 3]"& "$c3:E "}" ] ]
   | sig2_b_nb
-      [ << (Sig2_ABSTR_B_NB $c1 (LAMBDALIST $c1 [$id]$c2)
-                            (LAMBDALIST $c1 [<>]$c3)) >> ]
+      [ (sig2 $c1 [$id:$c1]$c2 [_:$c1]$c3) ]
        -> [ [<hov 0> "{"$id":"$c1:E"|" [1 3]$c2:E [1 3]"& "$c3:E "}" ] ]
   | sig2_nb_nb
-      [ << (Sig2_ABSTR_B_NB $c1 (LAMBDALIST $c1 [<>]$c2)
-                            (LAMBDALIST $c1 [<>]$c3)) >> ]
+      [ (sig2 $c1 [_:$c1]$c2 [_:$c1]$c3) ]
        -> [ [<hov 0> "{_:"$c1:E "|" [1 3] $c2:E [1 3]"& " $c3:E "}" ] ]
 
 (** Pretty-printing of [sigS] *)
-  | sigS [ (sigS $c1 $c2) ] -> [(SigS_ABSTR_B_NB  $c1 $c2):E]
-  | sigS_nb [ << (SigS_ABSTR_B_NB $c1 (LAMBDALIST $c1 [<>]$c2)) >> ]
+  | sigS_nb [ (sigS $c1 [_:$c1]$c2) ]
        -> [ [<hov 0> "{_:" $c1:E [1 3]"& " $c2:E  "}" ] ]
-  | sigS_b [ << (SigS_ABSTR_B_NB $c1 (LAMBDALIST $c1 [$id]$c2)) >> ]
+  | sigS_b [ (sigS $c1 [$id:$c1]$c2) ]
        -> [ [<hov 0> "{" $id  ":" $c1:E [1 3] "& " $c2:E "}" ] ]
 
 (** Pretty-printing of [sigS2] *)
-  | sigS2 [ (sigS2 $c1 $c2 $c3) ] -> [(SigS2_ABSTR_B_NB  $c1 $c2 $c3):E]
   | sigS2_b_b
-      [ << (SigS2_ABSTR_B_NB $c1 (LAMBDALIST $c1 [$id]$c2)
-                             (LAMBDALIST $c1 [$id]$c3)) >> ]
+      [ (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_ABSTR_B_NB $c1 (LAMBDALIST $c1 [<>]$c2)
-                             (LAMBDALIST  $c1 [$id]$c3)) >> ]
+      [ (sigS2 $c1 [_:$c1]$c2 [$id:$c1]$c3) ]
        -> [ [<hov 0> "{"$id ":" $c1:E [1 3]"& "$c2:E [1 3]"& "$c3:E "}" ] ]
   | sigS2_b_nb
-      [ << (SigS2_ABSTR_B_NB $c1 (LAMBDALIST $c1 [$id]$c2)
-                              (LAMBDALIST $c1 [<>]$c3)) >> ]
+      [ (sigS2 $c1 [$id:$c1]$c2 [_:$c1]$c3) ]
        -> [ [<hov 0> "{"$id ":" $c1:E [1 3]"& "$c2:E [1 3]"& "$c3:E "}" ] ]
   | sigS2_nb_nb
-      [ << (SigS2_ABSTR_B_NB $c1 (LAMBDALIST $c1 [<>]$c2)
-                             (LAMBDALIST $c1 [<>]$c3)) >> ]
+      [ (sigS2 $c1 [_:$c1]$c2 [_:$c1]$c3) ]
        -> [ [<hov 0> "{_:"$c1:E [1 3]"& "$c2:E [1 3]"& "$c3:E "}" ] ]
 
 (** Pretty-printing of [projS1] and [projS2] *)