diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-04-15 18:26:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-04-24 19:16:33 +0200 |
| commit | b090942f20ac8854bf227698d31ca1efec492c47 (patch) | |
| tree | 61cdc57146c4151fa743de9b3c2ab59b11722f92 /grammar | |
| parent | f3515efc26a693f4c525ad91c37c982f4c96e6ec (diff) | |
Higher-level API for tactic notations.
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/tacextend.ml4 | 23 | ||||
| -rw-r--r-- | grammar/vernacextend.ml4 | 8 |
2 files changed, 26 insertions, 5 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index e52770aa2..19b6e1b5f 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -45,13 +45,26 @@ let make_fun_clauses loc s l = let map c = Compat.make_fun loc [make_clause c] in mlexpr_of_list map l +let get_argt e = <:expr< match $e$ with [ Genarg.ExtraArg tag -> tag | _ -> assert False ] >> + +let rec mlexpr_of_symbol = function +| Ulist1 s -> <:expr< Extend.Ulist1 $mlexpr_of_symbol s$ >> +| Ulist1sep (s,sep) -> <:expr< Extend.Ulist1sep $mlexpr_of_symbol s$ $str:sep$ >> +| Ulist0 s -> <:expr< Extend.Ulist0 $mlexpr_of_symbol s$ >> +| Ulist0sep (s,sep) -> <:expr< Extend.Ulist0sep $mlexpr_of_symbol s$ $str:sep$ >> +| Uopt s -> <:expr< Extend.Uopt $mlexpr_of_symbol s$ >> +| Uentry e -> + let arg = get_argt <:expr< $lid:"wit_"^e$ >> in + <:expr< Extend.Uentry (Genarg.ArgT.Any $arg$) >> +| Uentryl (e, l) -> + assert (e = "tactic"); + let arg = get_argt <:expr< Constrarg.wit_tactic >> in + <:expr< Extend.Uentryl (Genarg.ArgT.Any $arg$) $mlexpr_of_int l$>> + let make_prod_item = function - | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >> + | ExtTerminal s -> <:expr< Tacentries.TacTerm $str:s$ >> | ExtNonTerminal (g, id) -> - let nt = type_of_user_symbol g in - let base s = <:expr< Pcoq.name_of_entry (Pcoq.genarg_grammar $mk_extraarg loc s$) >> in - <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$ - $mlexpr_of_prod_entry_key base g$ >> + <:expr< Tacentries.TacNonTerm $default_loc$ $mlexpr_of_symbol g$ $mlexpr_of_ident id$ >> let mlexpr_of_clause cl = mlexpr_of_list (fun (a,_,_) -> mlexpr_of_list make_prod_item a) cl diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index aedaead71..0d4bec69d 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -102,6 +102,14 @@ let make_fun_classifiers loc s c l = let cl = List.map (fun x -> Compat.make_fun loc [make_clause_classifier c s x]) l in mlexpr_of_list (fun x -> x) cl +let make_prod_item = function + | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >> + | ExtNonTerminal (g, id) -> + let nt = type_of_user_symbol g in + let base s = <:expr< Pcoq.name_of_entry (Pcoq.genarg_grammar $mk_extraarg loc s$) >> in + <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$ + $mlexpr_of_prod_entry_key base g$ >> + let mlexpr_of_clause cl = let mkexpr { r_head = a; r_patt = b; } = match a with | None -> mlexpr_of_list make_prod_item b |