diff options
| author | Pierre-Marie Pédrot | 2018-07-11 22:57:57 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-07-12 13:53:22 +0200 |
| commit | b9ff36b39eb193757ce57a89afe138cd09e759d7 (patch) | |
| tree | 5c692d9cad8ce9db00c9d7c127750650cd7b26a8 /grammar/q_util.mlp | |
| parent | 270ceed48217797e99ec845cc5d1c599b5729bc2 (diff) | |
Statically typecheck the VERNAC EXTEND wrapper.
This moves the typing code from the macro expansion to the extension
registering mechanism, bringing in more static safety. We also seize
the opportunity to remove dead code in the macro.
Diffstat (limited to 'grammar/q_util.mlp')
| -rw-r--r-- | grammar/q_util.mlp | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp index 0b8d7fda7a..0e2bf55d86 100644 --- a/grammar/q_util.mlp +++ b/grammar/q_util.mlp @@ -128,3 +128,17 @@ let rec parse_user_entry s sep = let s = match s with "hyp" -> "var" | _ -> s in check_separator sep; Uentry s + +let rec mlexpr_of_symbol = function +| Ulist1 s -> <:expr< Extend.TUlist1 $mlexpr_of_symbol s$ >> +| Ulist1sep (s,sep) -> <:expr< Extend.TUlist1sep $mlexpr_of_symbol s$ $str:sep$ >> +| Ulist0 s -> <:expr< Extend.TUlist0 $mlexpr_of_symbol s$ >> +| Ulist0sep (s,sep) -> <:expr< Extend.TUlist0sep $mlexpr_of_symbol s$ $str:sep$ >> +| Uopt s -> <:expr< Extend.TUopt $mlexpr_of_symbol s$ >> +| Uentry e -> + let wit = <:expr< $lid:"wit_"^e$ >> in + <:expr< Extend.TUentry (Genarg.get_arg_tag $wit$) >> +| Uentryl (e, l) -> + assert (e = "tactic"); + let wit = <:expr< $lid:"wit_"^e$ >> in + <:expr< Extend.TUentryl (Genarg.get_arg_tag $wit$) $mlexpr_of_int l$>> |