diff options
Diffstat (limited to 'parsing/q_util.ml4')
| -rw-r--r-- | parsing/q_util.ml4 | 80 |
1 files changed, 17 insertions, 63 deletions
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$ >> |