diff options
Diffstat (limited to 'parsing/q_util.ml4')
| -rw-r--r-- | parsing/q_util.ml4 | 38 |
1 files changed, 37 insertions, 1 deletions
diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4 index b3f5393c..07b23972 100644 --- a/parsing/q_util.ml4 +++ b/parsing/q_util.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: q_util.ml4,v 1.2.2.2 2004/07/16 19:30:41 herbelin Exp $ *) +(* $Id: q_util.ml4 7732 2005-12-26 13:51:24Z herbelin $ *) (* This file defines standard combinators to build ml expressions *) @@ -66,3 +66,39 @@ let mlexpr_of_string s = <:expr< $str:s$ >> let mlexpr_of_option f = function | None -> <:expr< None >> | Some e -> <:expr< Some $f e$ >> + +open Vernacexpr +open Pcoq +open Genarg + +let rec interp_entry_name loc s = + 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 > 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 > 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 + let s = if s = "hyp" then "var" else s in + let t, se = + match Pcoq.entry_type (Pcoq.get_univ "prim") s with + | Some _ as x -> x, <:expr< Prim. $lid:s$ >> + | None -> + match Pcoq.entry_type (Pcoq.get_univ "constr") s with + | Some _ as x -> x, <:expr< Constr. $lid:s$ >> + | None -> + match Pcoq.entry_type (Pcoq.get_univ "tactic") s with + | Some _ as x -> x, <:expr< Tactic. $lid:s$ >> + | None -> None, <:expr< $lid:s$ >> in + let t = + match t with + | Some t -> t + | None -> +(* Pp.warning_with Pp_control.err_ft + ("Unknown primitive grammar entry: "^s);*) + ExtraArgType s + in t, <:expr< Gramext.Snterm (Pcoq.Gram.Entry.obj $se$) >> |