Hack peu élégant pour permettre de parser des listes avec séparateurs dans

TACTIC EXTEND


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

5 files changed, 25 insertions, 10 deletions

diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 07c1470c9..ebe2b2893 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -213,7 +213,7 @@ EXTEND
       [ e = argtype; LIDENT "list" -> List0ArgType e
       | e = argtype; LIDENT "option" -> OptArgType e ]
     | "0"
-      [ e = LIDENT -> fst (interp_entry_name loc e) 
+      [ e = LIDENT -> fst (interp_entry_name loc e "")
       | "("; e = argtype; ")" -> e ] ]
   ;
   argrule:
@@ -221,7 +221,9 @@ EXTEND
   ;
   genarg:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
-        let t, g = interp_entry_name loc e in (g, Some (s,t))
+        let t, g = interp_entry_name loc e "" in (g, Some (s,t))
+      | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
+        let t, g = interp_entry_name loc e sep in (g, Some (s,t))
       | s = STRING ->
 	  if String.length s > 0 && Util.is_letter s.[0] then
 	    Pcoq.lexer.Token.using ("", s);
diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4
index bc8cd40ec..d4b4682fe 100644
--- a/parsing/q_util.ml4
+++ b/parsing/q_util.ml4
@@ -80,19 +80,28 @@ let modifiers e =
       Gramext.action (fun _ l _ _loc -> l))]
  >>
 
-let rec interp_entry_name loc s =
+let rec interp_entry_name loc s sep =
   let l = String.length s in
   if l > 8 & String.sub s 0 3 = "ne_" & String.sub s (l-5) 5 = "_list" then
-    let t, g = interp_entry_name loc (String.sub s 3 (l-8)) in
+    let t, g = interp_entry_name loc (String.sub s 3 (l-8)) "" in
     List1ArgType t, <:expr< Gramext.Slist1 $g$ >>
+  else if l > 12 & String.sub s 0 3 = "ne_" &
+                   String.sub s (l-9) 9 = "_list_sep" then
+    let t, g = interp_entry_name loc (String.sub s 3 (l-12)) "" in
+    let sep = <:expr< Gramext.Stoken("",$str:sep$) >> in
+    List1ArgType t, <:expr< Gramext.Slist1sep $g$ $sep$ >>
   else if l > 5 & String.sub s (l-5) 5 = "_list" then
-    let t, g = interp_entry_name loc (String.sub s 0 (l-5)) in
+    let t, g = interp_entry_name loc (String.sub s 0 (l-5)) "" in
     List0ArgType t, <:expr< Gramext.Slist0 $g$ >>
+  else if l > 9 & String.sub s (l-9) 9 = "_list_sep" then
+    let t, g = interp_entry_name loc (String.sub s 0 (l-9)) "" in
+    let sep = <:expr< Gramext.Stoken("",$str:sep$) >> in
+    List0ArgType t, <:expr< Gramext.Slist0sep $g$ $sep$ >>
   else if l > 4 & String.sub s (l-4) 4 = "_opt" then
-    let t, g = interp_entry_name loc (String.sub s 0 (l-4)) in
+    let t, g = interp_entry_name loc (String.sub s 0 (l-4)) "" in
     OptArgType t, <:expr< Gramext.Sopt $g$ >>
   else if l > 5 & String.sub s (l-5) 5 = "_mods" then
-    let t, g = interp_entry_name loc (String.sub s 0 (l-1)) in
+    let t, g = interp_entry_name loc (String.sub s 0 (l-1)) "" in
     List0ArgType t, modifiers g
   else
     let s = if s = "hyp" then "var" else s in
diff --git a/parsing/q_util.mli b/parsing/q_util.mli
index 4418c6376..f6660c9d5 100644
--- a/parsing/q_util.mli
+++ b/parsing/q_util.mli
@@ -28,4 +28,5 @@ val mlexpr_of_string : string -> MLast.expr
 
 val mlexpr_of_option : ('a -> MLast.expr) -> 'a option -> MLast.expr
 
-val interp_entry_name : Util.loc -> string -> Pcoq.entry_type * MLast.expr
+val interp_entry_name : Util.loc -> string -> string -> 
+  Pcoq.entry_type * MLast.expr
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index f62aaf202..442bbb6af 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -198,7 +198,10 @@ EXTEND
   ;
   tacargs:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
-        let t, g = Q_util.interp_entry_name loc e in
+        let t, g = Q_util.interp_entry_name loc e "" in
+        TacNonTerm (loc, t, g, Some s)
+      | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
+        let t, g = Q_util.interp_entry_name loc e sep in
         TacNonTerm (loc, t, g, Some s)
       | s = STRING ->
 	if s = "" then Util.user_err_loc (loc,"",Pp.str "Empty terminal");
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index b478e37d9..22df73ba7 100644
--- a/parsing/vernacextend.ml4
+++ b/parsing/vernacextend.ml4
@@ -114,7 +114,7 @@ EXTEND
   ;
   args:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
-        let t, g = Q_util.interp_entry_name loc e in
+        let t, g = Q_util.interp_entry_name loc e "" in
         VernacNonTerm (loc, t, g, Some s)
       | s = STRING ->
         VernacTerm s