diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-27 21:57:13 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-28 12:35:24 +0100 |
| commit | d8cea1c80b71d2cd65daa4bc2126f1bfc61b0047 (patch) | |
| tree | b20f78edea22cf508882767540754717200e1703 /grammar/argextend.ml4 | |
| parent | 04b244a4ba8605a97cd96855b4c4e628ba27db7b (diff) | |
Type-safe Argextend.
Diffstat (limited to 'grammar/argextend.ml4')
| -rw-r--r-- | grammar/argextend.ml4 | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index 1fe66b367..08651de64 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -142,26 +142,28 @@ let make_possibly_empty_subentries loc s cl = let make_act loc act pil = let rec make = function - | [] -> <:expr< Pcoq.Gram.action (fun loc -> ($act$ : 'a)) >> + | [] -> <:expr< (fun loc -> $act$) >> | GramNonTerminal (_,t,_,Some p) :: tl -> let t = Genarg.unquote t in let p = Names.Id.to_string p in <:expr< - Pcoq.Gram.action (fun $lid:p$ -> let _ = Genarg.in_gen $make_rawwit loc t$ $lid:p$ in $make tl$) >> | (GramTerminal _ | GramNonTerminal (_,_,_,None)) :: tl -> - <:expr< Pcoq.Gram.action (fun _ -> $make tl$) >> in + <:expr< (fun _ -> $make tl$) >> in make (List.rev pil) let make_prod_item = function - | GramTerminal s -> <:expr< Pcoq.gram_token_of_string $str:s$ >> - | GramNonTerminal (_,_,g,_) -> - <:expr< Pcoq.symbol_of_prod_entry_key $mlexpr_of_prod_entry_key g$ >> + | GramTerminal s -> <:expr< Pcoq.Atoken (Lexer.terminal $mlexpr_of_string s$) >> + | GramNonTerminal (_,_,g,_) -> mlexpr_of_prod_entry_key g + +let rec make_prod = function +| [] -> <:expr< Extend.Stop >> +| item :: prods -> <:expr< Extend.Next $make_prod prods$ $make_prod_item item$ >> let make_rule loc (prods,act) = - <:expr< ($mlexpr_of_list make_prod_item prods$,$make_act loc act prods$) >> + <:expr< Extend.Rule $make_prod (List.rev prods)$ $make_act loc act prods$ >> let declare_tactic_argument loc s (typ, pr, f, g, h) cl = let rawtyp, rawpr, globtyp, globpr = match typ with @@ -224,8 +226,7 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = <:str_item< value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>; <:str_item< do { - Compat.maybe_uncurry (Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.entry 'a)) - (None, [(None, None, $rules$)]); + Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]); Pptactic.declare_extra_genarg_pprule $wit$ $lid:rawpr$ $lid:globpr$ $lid:pr$ } >> ] @@ -245,8 +246,7 @@ let declare_vernac_argument loc s pr cl = <:str_item< value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>; <:str_item< do { - Compat.maybe_uncurry (Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.entry 'a)) - (None, [(None, None, $rules$)]); + Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]); Pptactic.declare_extra_genarg_pprule $wit$ $pr_rules$ (fun _ _ _ _ -> Errors.anomaly (Pp.str "vernac argument needs not globwit printer")) |