- Cleaning (unification of ML names, removal of obsolete code,

  reorganization of code) and documentation (in pcoq.mli) of the code
  for parsing extensions (TACTIC/VERNAC/ARGUMENT EXTEND, Tactic
  Notation, Notation); merged the two copies of interp_entry_name to
  avoid they diverge.  
- Added support in Tactic Notation for ne_..._list_sep in general and
  for (ne_)ident_list(_sep) in particular.



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

1 files changed, 15 insertions, 61 deletions

diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4
index 9b59ba8e5b..4694497491 100644
--- a/parsing/q_util.ml4
+++ b/parsing/q_util.ml4
@@ -13,6 +13,8 @@
 (* This file defines standard combinators to build ml expressions *)
 
 open Util
+open Extrawit
+open Pcoq
 
 let not_impl name x =
   let desc =
@@ -78,64 +80,16 @@ open Vernacexpr
 open Pcoq
 open Genarg
 
-let modifiers e =
-<:expr<  Gramext.srules
-    [([], Gramext.action(fun _loc -> []));
-     ([Gramext.Stoken ("", "(");
-       Gramext.Slist1sep ($e$, Gramext.Stoken ("", ","));
-       Gramext.Stoken ("", ")")],
-      Gramext.action (fun _ l _ _loc -> l))]
- >>
-
-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
-    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
-    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
-    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
-    List0ArgType t, modifiers g
-  else
-    let s = if s = "hyp" then "var" else s in
-    let t, se, lev =
-      match tactic_genarg_level s with
-        | Some 5 ->
-            Some (ExtraArgType s), <:expr< Tactic. binder_tactic >>, None
-	| Some n ->
-            Some (ExtraArgType s), <:expr< Tactic. tactic_expr >>, Some n
-	| None ->
-      match Pcoq.entry_type (Pcoq.get_univ "prim") s with
-	| Some _ as x -> x, <:expr< Prim. $lid:s$ >>, None
-	| None -> 
-      match Pcoq.entry_type (Pcoq.get_univ "constr") s with
-	| Some _ as x -> x, <:expr< Constr. $lid:s$ >>, None
-	| None -> 
-      match Pcoq.entry_type (Pcoq.get_univ "tactic") s with
-	| Some _ as x -> x, <:expr< Tactic. $lid:s$ >>, None
-	| None -> None, <:expr< $lid:s$ >>, None in
-    let t =
-      match t with
-	| Some t -> t
-	| None -> ExtraArgType s in
-    let entry = match lev with
-      | Some n ->
-	  let s = string_of_int n in
-	  <:expr< Gramext.Snterml (Pcoq.Gram.Entry.obj $se$, $str:s$) >>
-      | None -> 
-	  <:expr< Gramext.Snterm (Pcoq.Gram.Entry.obj $se$) >>
-    in t, entry
+let rec mlexpr_of_prod_entry_key = function
+  | Extend.Alist1 s -> <:expr< Extend.Alist1 $mlexpr_of_prod_entry_key s$ >>
+  | Extend.Alist1sep (s,sep) -> <:expr< Extend.Alist1sep $mlexpr_of_prod_entry_key s$ $str:sep$ >>
+  | Extend.Alist0 s -> <:expr< Extend.Alist0 $mlexpr_of_prod_entry_key s$ >>
+  | Extend.Alist0sep (s,sep) -> <:expr< Extend.Alist0sep $mlexpr_of_prod_entry_key s$ $str:sep$ >>
+  | Extend.Aopt s -> <:expr< Extend.Aopt $mlexpr_of_prod_entry_key s$ >>
+  | Extend.Amodifiers s -> <:expr< Extend.Amodifiers $mlexpr_of_prod_entry_key s$ >>
+  | Extend.Aself -> <:expr< Extend.Aself >>
+  | Extend.Anext -> <:expr< Extend.Anext >>
+  | Extend.Atactic n -> <:expr< Extend.Atactic $mlexpr_of_int n$ >>
+  | Extend.Agram s -> anomaly "Agram not supported"
+  | Extend.Aentry ("",s) -> <:expr< Extend.Agram (Gram.Entry.obj $lid:s$) >>
+  | Extend.Aentry (u,s) -> <:expr< Extend.Aentry $str:u$ $str:s$ >>