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 | |
parent | f3515efc26a693f4c525ad91c37c982f4c96e6ec (diff) |
Higher-level API for tactic notations.
-rw-r--r-- | grammar/tacextend.ml4 | 23 | ||||
-rw-r--r-- | grammar/vernacextend.ml4 | 8 | ||||
-rw-r--r-- | intf/extend.mli | 16 | ||||
-rw-r--r-- | ltac/g_ltac.ml4 | 2 | ||||
-rw-r--r-- | ltac/tacentries.ml | 52 | ||||
-rw-r--r-- | ltac/tacentries.mli | 11 |
6 files changed, 77 insertions, 35 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 diff --git a/intf/extend.mli b/intf/extend.mli index 10713745e..381d47dd1 100644 --- a/intf/extend.mli +++ b/intf/extend.mli @@ -53,14 +53,14 @@ type simple_constr_prod_entry_key = (** {5 AST for user-provided entries} *) -type user_symbol = -| Ulist1 : user_symbol -> user_symbol -| Ulist1sep : user_symbol * string -> user_symbol -| Ulist0 : user_symbol -> user_symbol -| Ulist0sep : user_symbol * string -> user_symbol -| Uopt : user_symbol -> user_symbol -| Uentry : string -> user_symbol -| Uentryl : string * int -> user_symbol +type 'a user_symbol = +| Ulist1 of 'a user_symbol +| Ulist1sep of 'a user_symbol * string +| Ulist0 of 'a user_symbol +| Ulist0sep of 'a user_symbol * string +| Uopt of 'a user_symbol +| Uentry of 'a +| Uentryl of 'a * int (** {5 Type-safe grammar extension} *) diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4 index fe750f429..df499a2c9 100644 --- a/ltac/g_ltac.ml4 +++ b/ltac/g_ltac.ml4 @@ -405,7 +405,7 @@ VERNAC COMMAND EXTEND VernacTacticNotation [ let l = Locality.LocalityFixme.consume () in let n = Option.default 0 n in - Tacentries.add_tactic_notation (Locality.make_module_locality l, n, r, e) + Tacentries.add_tactic_notation (Locality.make_module_locality l) n r e ] END diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index a3e15866e..dfcfdece6 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -97,7 +97,7 @@ let rec parse_user_entry s sep = let arg_list = function Rawwit t -> Rawwit (ListArg t) let arg_opt = function Rawwit t -> Rawwit (OptArg t) -let interp_entry_name up_level s sep = +let interp_entry_name interp symb = let open Extend in let rec eval = function | Ulist1 e -> @@ -115,19 +115,10 @@ let interp_entry_name up_level s sep = | Uopt e -> let EntryName (t, g) = eval e in EntryName (arg_opt t, Aopt g) - | Uentry s -> - begin - try try_get_entry uprim s with Not_found -> - try try_get_entry uconstr s with Not_found -> - try try_get_entry utactic s with Not_found -> - error ("Unknown entry "^s^".") - end - | Uentryl (s, n) -> - (** FIXME: do better someday *) - assert (String.equal s "tactic"); - get_tacentry n up_level + | Uentry s -> interp s None + | Uentryl (s, n) -> interp s (Some n) in - eval (parse_user_entry s sep) + eval symb (**********************************************************************) (** Grammar declaration for Tactic Notation (Coq level) *) @@ -217,8 +208,22 @@ let extend_ml_tactic_grammar n ntn = extend_grammar ml_tactic_grammar (n, ntn) let interp_prod_item lev = function | TacTerm s -> GramTerminal s | TacNonTerm (loc, (nt, sep), _) -> - let EntryName (etyp, e) = interp_entry_name lev nt sep in - GramNonTerminal (loc, etyp, e) + let symbol = parse_user_entry nt sep in + let interp s = function + | None -> + begin + try try_get_entry uprim s with Not_found -> + try try_get_entry uconstr s with Not_found -> + try try_get_entry utactic s with Not_found -> + error ("Unknown entry "^s^".") + end + | Some n -> + (** FIXME: do better someday *) + assert (String.equal s "tactic"); + get_tacentry n lev + in + let EntryName (etyp, e) = interp_entry_name interp symbol in + GramNonTerminal (loc, etyp, e) let make_terminal_status = function | GramTerminal s -> Some s @@ -294,7 +299,7 @@ let cons_production_parameter = function | TacTerm _ -> None | TacNonTerm (_, _, id) -> Some id -let add_tactic_notation (local,n,prods,e) = +let add_tactic_notation local n prods e = let ids = List.map_filter cons_production_parameter prods in let prods = List.map (interp_prod_item n) prods in let pprule = { @@ -380,6 +385,21 @@ let inMLTacticGrammar : ml_tactic_grammar_obj -> obj = } let add_ml_tactic_notation name prods = + let interp_prods = function + | TacTerm s -> GramTerminal s + | TacNonTerm (loc, symb, _) -> + let interp (ArgT.Any tag) lev = match lev with + | None -> + let wit = ExtraArg tag in + EntryName (Rawwit wit, Extend.Aentry (Pcoq.name_of_entry (Pcoq.genarg_grammar wit))) + | Some lev -> + assert (coincide (ArgT.repr tag) "tactic" 0); + EntryName (Rawwit Constrarg.wit_tactic, atactic lev) + in + let EntryName (etyp, e) = interp_entry_name interp symb in + GramNonTerminal (loc, etyp, e) + in + let prods = List.map (fun p -> List.map interp_prods p) prods in let obj = { mltacobj_name = name; mltacobj_prod = prods; diff --git a/ltac/tacentries.mli b/ltac/tacentries.mli index 0f4bb2530..cd9f430cb 100644 --- a/ltac/tacentries.mli +++ b/ltac/tacentries.mli @@ -13,14 +13,15 @@ type 'a grammar_tactic_prod_item_expr = | TacTerm of string | TacNonTerm of Loc.t * 'a * Names.Id.t -(** Adding a tactic notation in the environment *) - val add_tactic_notation : - locality_flag * int * (string * string option) grammar_tactic_prod_item_expr list * raw_tactic_expr -> - unit + locality_flag -> int -> (string * string option) grammar_tactic_prod_item_expr list -> + raw_tactic_expr -> unit +(** [add_tactic_notation local level prods expr] adds a tactic notation in the + environment at level [level] with locality [local] made of the grammar + productions [prods] and returning the body [expr] *) val add_ml_tactic_notation : ml_tactic_name -> - Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list list -> unit + Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list list -> unit val register_ltac : bool -> Vernacexpr.tacdef_body list -> unit |