aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--grammar/tacextend.ml423
-rw-r--r--grammar/vernacextend.ml48
-rw-r--r--intf/extend.mli16
-rw-r--r--ltac/g_ltac.ml42
-rw-r--r--ltac/tacentries.ml52
-rw-r--r--ltac/tacentries.mli11
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-07 13:51:10 +0000