Renommage de g_multiple_case en g_cases

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

2 files changed, 62 insertions, 74 deletions

diff --git a/parsing/g_cases.ml4 b/parsing/g_cases.ml4
new file mode 100644
index 0000000000..0b45dd3e47
--- /dev/null
+++ b/parsing/g_cases.ml4
@@ -0,0 +1,62 @@
+
+(* $Id$ *)
+
+open Pcoq
+open Command
+
+GEXTEND Gram
+  pattern_list:
+    [ [  -> []
+      | p = pattern; pl = pattern_list -> p :: pl ] ]
+  ;
+  lsimple_pattern:
+    [ [ c = simple_pattern2 -> c ] ]
+  ;
+  simple_pattern:
+    [ [ id = ident -> id
+      | "("; p = lsimple_pattern; ")" -> p ] ]
+  ;
+  simple_pattern_list:
+    [ [  -> []
+      | p = simple_pattern; pl = simple_pattern_list ->
+	   p :: pl ] ]
+  ;
+  (* The XTRA"!" means we want to override the implicit arg mecanism of bdize,
+     since params are not given in patterns *)
+  simple_pattern2:
+    [ [ p = simple_pattern; lp = pattern_list ->
+          <:ast< (PATTCONSTRUCT $p ($LIST $lp)) >>
+      | p = simple_pattern; "as"; id = ident -> <:ast< (PATTAS $id $p) >>
+      | c1 = simple_pattern; ","; c2 = simple_pattern ->
+          <:ast< (PATTCONSTRUCT pair $c1 $c2) >> ] ]
+  ;
+  pattern:
+    [ [ p = simple_pattern -> p ] ]
+  ;
+  ne_pattern_list:
+    [ [ c1 = pattern; cl = ne_pattern_list -> c1 :: cl
+      | c1 = pattern -> [c1] ] ]
+  ;
+  equation:
+    [ [ lhs = ne_pattern_list; "=>"; rhs = command ->
+	      <:ast< (EQN $rhs ($LIST $lhs)) >> ] ]
+  ;
+  ne_eqn_list:
+    [ [ e = equation; "|"; leqn = ne_eqn_list -> e :: leqn
+      | e = equation -> [e] ] ]
+  ;
+
+  command1:
+    [ [ "<"; l1 = lcommand; ">"; "Cases"; lc = ne_command_list; "of";
+        OPT "|"; eqs = ne_eqn_list; "end" ->
+          <:ast< (MULTCASE $l1 (TOMATCH ($LIST $lc)) ($LIST $eqs)) >>
+      | "Cases"; lc = ne_command_list; "of";
+	OPT "|"; eqs = ne_eqn_list; "end" ->
+          <:ast< (MULTCASE "SYNTH" (TOMATCH ($LIST $lc)) ($LIST $eqs)) >>
+      | "<"; l1 = lcommand; ">"; "Cases"; lc = ne_command_list; "of";
+        "end" ->
+          <:ast< (MULTCASE $l1 (TOMATCH ($LIST $lc))) >>
+      | "Cases"; lc = ne_command_list; "of"; "end" -> 
+          <:ast< (MULTCASE "SYNTH" (TOMATCH ($LIST $lc))) >> ] ]
+  ;
+END;
diff --git a/parsing/g_multiple_case.ml4 b/parsing/g_multiple_case.ml4
deleted file mode 100644
index 6611911cad..0000000000
--- a/parsing/g_multiple_case.ml4
+++ /dev/null
@@ -1,74 +0,0 @@
-
-(* $Id$ *)
-
-open Pcoq
-
-open Command
-
-GEXTEND Gram
-  pattern_list:
-    [ [  -> ([],[])
-      | (id1,p) = pattern; (id2,pl) = pattern_list -> (id1@id2, p::pl) ] ]
-  ;
-  lsimple_pattern:
-    [ [ c = simple_pattern2 -> c ] ]
-  ;
-  simple_pattern:
-    [ [ id = ident -> ([Ast.nvar_of_ast id], id)
-      | "("; p = lsimple_pattern; ")" -> p ] ]
-  ;
-  simple_pattern_list:
-    [ [  -> ([],[])
-      | (id1,p) = simple_pattern; (id2,pl) = simple_pattern_list ->
-	   (id1@id2, p::pl) ] ]
-  ;
-  (* The XTRA"!" means we want to override the implicit arg mecanism of bdize,
-     since params are not given in patterns *)
-  simple_pattern2:
-    [ [ (id1,p) = simple_pattern; (id2,lp) = pattern_list ->
-          (id1@id2, <:ast< (APPLIST (XTRA "!" $p) ($LIST $lp)) >>)
-      | (id1,p) = simple_pattern; "as"; id = ident ->
-          ((Ast.nvar_of_ast id)::id1, <:ast< (XTRA"AS" $id $p) >>)
-      | (id1,c1) = simple_pattern; ","; (id2,c2) = simple_pattern ->
-          (id1@id2, <:ast< (APPLIST (XTRA "!" pair) $c1 $c2) >>) ] ]
-  ;
-  pattern:
-    [ [ p = simple_pattern -> p ] ]
-  ;
-  ne_pattern_list:
-    [ [ (id1,c1) = pattern; (id2,cl) = ne_pattern_list ->
-	(id1@id2, c1::cl)
-      | (id1,c1) = pattern -> (id1,[c1]) ] ]
-  ;
-  equation:
-    [ [ (ids,lhs) = ne_pattern_list; "=>"; rhs = command ->
-          let br =
-	    List.fold_right (fun s ast -> Coqast.Slam loc (Some s) ast)
-	      ids
-	      <:ast< (XTRA"EQN" $rhs ($LIST $lhs)) >> in
-	  let lid = List.map (fun s -> Coqast.Id loc s) ids in
-	  <:ast< (XTRA"LAMEQN"($LIST $lid) $br) >> ] ]
-  ;
-  ne_eqn_list:
-    [ [ e = equation; "|"; leqn = ne_eqn_list -> e :: leqn
-      | e = equation -> [e] ] ]
-  ;
-
-  command1:
-    [ [ "<"; l1 = lcommand; ">"; "Cases"; lc = ne_command_list; "of";
-        OPT "|"; eqs = ne_eqn_list; "end" ->
-          <:ast< (XTRA"MULTCASE" $l1 (XTRA"TOMATCH" ($LIST $lc))
-                    ($LIST $eqs)) >>
-      | "Cases"; lc = ne_command_list; "of"; 
-	OPT "|"; eqs = ne_eqn_list; "end" ->
-          <:ast< (XTRA"MULTCASE" (XTRA"SYNTH")
-                    (XTRA"TOMATCH"($LIST $lc)) ($LIST $eqs)) >>
-      | "<"; l1 = lcommand; ">"; "Cases"; lc = ne_command_list; "of";
-        "end" ->
-          <:ast< (XTRA"MULTCASE" $l1 (XTRA"TOMATCH" ($LIST $lc))) >>
-      | "Cases"; lc = ne_command_list; "of"; "end" -> 
-          <:ast< (XTRA"MULTCASE" (XTRA"SYNTH")
-                    (XTRA"TOMATCH"($LIST $lc))) >> ] ]
-  ;
-  END
-