Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; améliorations diverses de l'affichage; affinement de la syntaxe et des options de Notation; branchement de Syntactic Definition sur Notation

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

1 files changed, 69 insertions, 84 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 8644cb724b..6476cec513 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -52,12 +52,23 @@ let test_int_rparen =
             end
         | _ -> raise Stream.Failure)
 
+(* Hack to parse "n" at level 0 without conflicting with "n!" at level 91 *)
+(* admissible notation "(n)" *)
+let test_int_bang =
+  Gram.Entry.of_parser "test_int_bang"
+    (fun strm ->
+      match Stream.npeek 1 strm with
+        | [("INT", n)] ->
+            begin match Stream.npeek 2 strm with
+              | [_; ("", "!")] -> ()
+              | _ -> raise Stream.Failure
+            end
+        | _ -> raise Stream.Failure)
+
 
 GEXTEND Gram
-  GLOBAL: constr0 constr1 constr2 constr3 lassoc_constr4 constr5
-          constr6 constr7 constr8 constr9 constr10 lconstr constr
-          ne_name_comma_list ne_constr_list sort
-          global constr_pattern Constr.ident;
+  GLOBAL: constr9 lconstr constr sort global constr_pattern Constr.ident
+          (*ne_name_comma_list*);
   Constr.ident:
     [ [ id = Prim.ident -> id
 
@@ -70,12 +81,6 @@ GEXTEND Gram
       (* This is used in quotations *)
       | id = METAIDENT -> Ident (loc,id_of_string id) ] ]
   ;
-  constr:
-    [ [ c = constr8 -> c ] ]
-  ;
-  lconstr:
-    [ [ c = constr10 -> c ] ]
-  ;
   constr_pattern:
     [ [ c = constr -> c ] ]
   ;
@@ -87,10 +92,47 @@ GEXTEND Gram
       | "Prop" -> RProp Null
       | "Type" -> RType None ] ]
   ;
-  constr0:
-    [ [ "?" -> CHole loc
+  constr:
+    [ "top" RIGHTA
+      [ c1 = constr; "->"; c2 = constr -> CArrow (loc, c1, c2) ]
+    | "1"
+      [ "<"; p = lconstr; ">"; IDENT "Match"; c = constr; "with";
+        cl = LIST0 constr; "end" ->
+	  COrderedCase (loc, MatchStyle, Some p, c, cl)
+      | "<"; p = lconstr; ">"; IDENT "Case"; c = constr; "of";
+        cl = LIST0 constr; "end" ->
+	  COrderedCase (loc, RegularStyle, Some p, c, cl)
+      | IDENT "Case"; c = constr; "of"; cl = LIST0 constr; "end" ->
+          COrderedCase (loc, RegularStyle, None, c, cl)
+      | IDENT "Match"; c = constr; "with"; cl = LIST1 constr; "end" ->
+          COrderedCase (loc, MatchStyle, None, c, cl)
+      | IDENT "let"; "("; b = ne_name_comma_list; ")"; "=";
+        c = constr; "in"; c1 = constr LEVEL "top"->
+          (* TODO: right loc *)
+	  COrderedCase
+            (loc, LetStyle, None, c, [CLambdaN (loc, [b, CHole loc], c1)])
+      | IDENT "let"; na = name; "="; c = opt_casted_constr; 
+	"in"; c1 = constr LEVEL "top" ->
+          CLetIn (loc, na, c, c1)
+      | IDENT "if"; c1 = constr;
+        IDENT "then"; c2 = constr;
+        IDENT "else"; c3 = constr LEVEL "top" ->
+	  COrderedCase (loc, IfStyle, None, c1, [c2; c3])
+      | "<"; p = lconstr; ">";
+        IDENT "let"; "("; b = ne_name_comma_list; ")"; "="; c = constr; 
+        "in"; c1 = constr LEVEL "top" ->
+          (* TODO: right loc *)
+	  COrderedCase (loc, LetStyle, Some p, c,
+            [CLambdaN (loc, [b, CHole loc], c1)])
+      | "<"; p = lconstr; ">";
+        IDENT "if"; c1 = constr;
+        IDENT "then"; c2 = constr; 
+        IDENT "else"; c3 = constr LEVEL "top" ->
+	  COrderedCase (loc, IfStyle, Some p, c1, [c2; c3]) ]
+    | "0"
+      [ "?" -> CHole loc
       | "?"; n = Prim.natural -> CMeta (loc, n)
-      | bll = binders; c = constr -> abstract_constr loc c bll
+      | bll = binders; c = constr LEVEL "top" -> abstract_constr loc c bll
       (* Hack to parse syntax "(n)" as a natural number *)
       | "("; test_int_rparen; n = INT; ")" ->
 	  let n = CNumeral (loc,Bignat.POS (Bignat.of_string n)) in
@@ -99,7 +141,7 @@ GEXTEND Gram
           let id = coerce_to_name lc1 in
 	  CProdN (loc, ([id], c)::bl, body)
 (* TODO: Syntaxe (_:t...)t et (_,x...)t *)
-      | "("; lc1 = lconstr; ","; lc2 = lconstr; ":"; c = constr; 
+      | "("; lc1 = lconstr; ","; lc2 = lconstr; ":"; c = constr;
         (bl,body) = product_tail ->
           let id1 = coerce_to_name lc1 in
           let id2 = coerce_to_name lc2 in
@@ -124,70 +166,11 @@ GEXTEND Gram
       | v = global -> CRef v
       | n = INT -> CNumeral (loc,Bignat.POS (Bignat.of_string n))
       | "-"; n = INT -> CNumeral (loc,Bignat.NEG (Bignat.of_string n))
-      | "!"; f = global -> CAppExpl (loc,f,[])
-    ] ]
-  ;
-  constr1:
-    [ [ "<"; p = lconstr; ">"; IDENT "Match"; c = constr; "with";
-        cl = LIST0 constr; "end" ->
-	  COrderedCase (loc, MatchStyle, Some p, c, cl)
-      | "<"; p = lconstr; ">"; IDENT "Case"; c = constr; "of";
-        cl = LIST0 constr; "end" ->
-	  COrderedCase (loc, RegularStyle, Some p, c, cl)
-      | IDENT "Case"; c = constr; "of"; cl = LIST0 constr; "end" ->
-          COrderedCase (loc, RegularStyle, None, c, cl)
-      | IDENT "Match"; c = constr; "with"; cl = LIST1 constr; "end" ->
-          COrderedCase (loc, MatchStyle, None, c, cl)
-      | IDENT "let"; "("; b = ne_name_comma_list; ")"; "=";
-        c = constr; "in"; c1 = constr->
-          (* TODO: right loc *)
-	  COrderedCase
-            (loc, LetStyle, None, c, [CLambdaN (loc, [b, CHole loc], c1)])
-      | IDENT "let"; na = name; "="; c = opt_casted_constr; "in"; c1 = constr
-          -> CLetIn (loc, na, c, c1)
-      | IDENT "if"; c1 = constr; IDENT "then"; c2 = constr;
-        IDENT "else"; c3 = constr ->
-	  COrderedCase (loc, IfStyle, None, c1, [c2; c3])
-      | "<"; p = lconstr; ">";
-        IDENT "let"; "("; b = ne_name_comma_list; ")"; "=";
-        c = constr; "in"; c1 = constr ->
-          (* TODO: right loc *)
-	  COrderedCase (loc, LetStyle, Some p, c,
-            [CLambdaN (loc, [b, CHole loc], c1)])
-      | "<"; p = lconstr; ">";
-        IDENT "if"; c1 = constr; IDENT "then";
-        c2 = constr; IDENT "else"; c3 = constr ->
-	  COrderedCase (loc, IfStyle, Some p, c1, [c2; c3])
-      | c = constr0 -> c ] ]
-  ;
-  constr2: (* ~ will be here *)
-    [ [ c = constr1 -> c ] ]
+      | "!"; f = global -> CAppExpl (loc,f,[]) ] ]
   ;
-  constr3:
-    [ [ c1 = constr2 -> c1 ] ]
-  ;
-  lassoc_constr4:
-    [ [ c1 = constr3 -> c1 ] ]
-  ;
-  constr5:
-    [ [ c1 = lassoc_constr4 -> c1 ] ]
-  ;
-  constr6:  (* /\ will be here *)
-    [ [ c1 = constr5 -> c1 ] ]
-  ;
-  constr7:  (* \/ will be here *)
-    [ RIGHTA [ c1 = constr6 -> c1 ] ]
-  ;
-  constr8:  (* <-> will be here *)
-    [ [ c1 = constr7 -> c1
-      | c1 = constr7; "->"; c2 = constr8 -> CArrow (loc, c1, c2) ] ]
-  ;
-  constr9:
-    [ [ c1 = constr8 -> c1
-      | c1 = constr8; "::"; c2 = constr8 -> CCast (loc, c1, c2) ] ]
-  ;
-  constr10:
-    [ [ "!"; f = global; args = LIST0 constr9 -> CAppExpl (loc, f, args)
+  lconstr:
+    [ "10"
+      [ "!"; f = global; args = LIST0 constr9 -> CAppExpl (loc, f, args)
 (*
       | "!"; f = global; "with"; b = binding_list ->
 	  <:ast< (APPLISTWITH $f $b) >>
@@ -195,11 +178,19 @@ GEXTEND Gram
       | f = constr9; args = LIST1 constr91 -> CApp (loc, f, args)
       | f = constr9 -> f ] ]
   ;
+  constr91:
+    [ [ test_int_bang; n = INT; "!"; c = constr9 ->
+        (c, Some (int_of_string n))
+      | c = constr9 -> (c, None) ] ]
+  ;
+  constr9:
+    [ [ c1 = constr -> c1
+      | c1 = constr; "::"; c2 = constr -> CCast (loc, c1, c2) ] ]
+  ;
   ne_name_comma_list:
     [ [ nal = LIST1 name SEP "," -> nal ] ]
   ;
   name_comma_list_tail:
-
     [ [ ","; idl = ne_name_comma_list -> idl
       | -> [] ] ]
   ;
@@ -241,12 +232,6 @@ GEXTEND Gram
     [ [ ":"; c = constr -> c 
       | -> CHole loc ] ]
   ;
-  constr91:
-    [ [ n = natural; "!"; c = constr9 -> (c, Some n)
-      | n = natural ->
-          (CNumeral (loc, Bignat.POS (Bignat.of_string (string_of_int n))), None)
-      | c = constr9 -> (c, None) ] ]
-  ;
   fixbinder:
     [ [ id = base_ident; "/"; recarg = natural; ":"; type_ = constr;
         ":="; def = constr ->