From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 21 Jul 2010 09:46:51 +0200
Subject: Imported Upstream snapshot 8.3~beta0+13298

---
 parsing/q_util.ml4 | 80 ++++++++++++------------------------------------------
 1 file changed, 17 insertions(+), 63 deletions(-)

(limited to 'parsing/q_util.ml4')

diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4
index da4329bb..7b9037d9 100644
--- a/parsing/q_util.ml4
+++ b/parsing/q_util.ml4
@@ -8,17 +8,19 @@
 
 (*i camlp4use: "q_MLast.cmo" i*)
 
-(* $Id: q_util.ml4 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id$ *)
 
 (* This file defines standard combinators to build ml expressions *)
 
 open Util
+open Extrawit
+open Pcoq
 
 let not_impl name x =
   let desc =
     if Obj.is_block (Obj.repr x) then
       "tag = " ^ string_of_int (Obj.tag (Obj.repr x))
-    else 
+    else
       "int_val = " ^ string_of_int (Obj.magic x)
   in
   failwith ("<Q_util." ^ name ^ ", not impl: " ^ 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$ >>
-- 
cgit v1.2.3