diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-18 19:48:50 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-18 19:48:50 +0000 |
| commit | a3b4bde65a350bf3dc54ccec8f7608355c6a008a (patch) | |
| tree | 46107f5a916af73f9c0051097ce73f2bdd3455b8 /grammar | |
| parent | 7a2701e6741fcf1e800e35b7721fc89abe40cbba (diff) | |
Proof-of-concept: moved four easy-to-handle generic arguments to
their own file, Stdarg.
This required a little trick to correctly handle wit_* naming. We
use a dynamic table to remember exactly where those arguments come
from.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16587 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/argextend.ml4 | 20 | ||||
| -rw-r--r-- | grammar/grammar.mllib | 1 | ||||
| -rw-r--r-- | grammar/q_coqast.ml4 | 4 |
3 files changed, 11 insertions, 14 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index b5830e789..4ea5f35c1 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -18,20 +18,20 @@ let default_loc = <:expr< Loc.ghost >> let mk_extraarg s = if Extrawit.tactic_genarg_level s = None then - <:expr< $lid:"wit_"^s$ >> + try + let name = Genarg.get_name0 s in + <:expr< $lid:name$ >> + with Not_found -> + <:expr< $lid:"wit_"^s$ >> else - <:expr< - let module WIT = struct - open Extrawit; - value wit = $lid:"wit_"^s$; - end in WIT.wit >> + <:expr< + let module WIT = struct + open Extrawit; + value wit = $lid:"wit_"^s$; + end in WIT.wit >> let rec make_wit loc = function - | BoolArgType -> <:expr< Genarg.wit_bool >> - | IntArgType -> <:expr< Genarg.wit_int >> | IntOrVarArgType -> <:expr< Genarg.wit_int_or_var >> - | StringArgType -> <:expr< Genarg.wit_string >> - | PreIdentArgType -> <:expr< Genarg.wit_pre_ident >> | IntroPatternArgType -> <:expr< Genarg.wit_intro_pattern >> | IdentArgType b -> <:expr< Genarg.wit_ident_gen $mlexpr_of_bool b$ >> | VarArgType -> <:expr< Genarg.wit_var >> diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index 818d220b8..a97b8a2a6 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -27,6 +27,7 @@ Unicode Names Libnames Genarg +Stdarg Tok Lexer Extrawit diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index 0f5be6efb..65aeef11e 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -201,15 +201,11 @@ let mlexpr_of_red_expr = function <:expr< Genredexpr.ExtraRedExpr $mlexpr_of_string s$ >> let rec mlexpr_of_argtype loc = function - | Genarg.BoolArgType -> <:expr< Genarg.BoolArgType >> - | Genarg.IntArgType -> <:expr< Genarg.IntArgType >> | Genarg.IntOrVarArgType -> <:expr< Genarg.IntOrVarArgType >> | Genarg.RefArgType -> <:expr< Genarg.RefArgType >> - | Genarg.PreIdentArgType -> <:expr< Genarg.PreIdentArgType >> | Genarg.IntroPatternArgType -> <:expr< Genarg.IntroPatternArgType >> | Genarg.IdentArgType b -> <:expr< Genarg.IdentArgType $mlexpr_of_bool b$ >> | Genarg.VarArgType -> <:expr< Genarg.VarArgType >> - | Genarg.StringArgType -> <:expr< Genarg.StringArgType >> | Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >> | Genarg.OpenConstrArgType b -> <:expr< Genarg.OpenConstrArgType $mlexpr_of_bool b$ >> | Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >> |