Providing a centralized API for ARGUMENT EXTEND.

We chose to stick to the most general possible API, even though the macro
will not make full use of the possibilities. It makes explicit the various
data expected to be provided in an orthogonal way.

5 files changed, 198 insertions, 1 deletions

diff --git a/plugins/ltac/ltac_plugin.mlpack b/plugins/ltac/ltac_plugin.mlpack
index ec96e1bbdd..e83eab20dc 100644
--- a/plugins/ltac/ltac_plugin.mlpack
+++ b/plugins/ltac/ltac_plugin.mlpack
@@ -7,10 +7,10 @@ Pltac
 Taccoerce
 Tactic_debug
 Tacintern
-Tacentries
 Profile_ltac
 Tactic_matching
 Tacinterp
+Tacentries
 Evar_tactics
 Tactic_option
 Extraargs
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index a77a9c2f45..16cff420bd 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -673,3 +673,96 @@ let tactic_extend plugin_name tacname ~level ?deprecation sign =
   let obj () = add_ml_tactic_notation ml_tactic_name ~level ?deprecation (List.map clause_of_ty_ml sign) in
   Tacenv.register_ml_tactic ml_tactic_name @@ Array.of_list (List.map eval sign);
   Mltop.declare_cache_obj obj plugin_name
+
+
+(** ARGUMENT EXTEND *)
+
+open Geninterp
+
+type ('a, 'b, 'c) argument_printer =
+  'a Pptactic.raw_extra_genarg_printer *
+  'b Pptactic.glob_extra_genarg_printer *
+  'c Pptactic.extra_genarg_printer
+
+type ('a, 'b) argument_intern =
+| ArgInternFun : ('a, 'b) Genintern.intern_fun -> ('a, 'b) argument_intern
+| ArgInternWit : ('a, 'b, 'c) Genarg.genarg_type -> ('a, 'b) argument_intern
+
+type 'b argument_subst =
+| ArgSubstFun : 'b Genintern.subst_fun -> 'b argument_subst
+| ArgSubstWit : ('a, 'b, 'c) Genarg.genarg_type -> 'b argument_subst
+
+type ('b, 'c) argument_interp =
+| ArgInterpRet : ('c, 'c) argument_interp
+| ArgInterpFun : ('b, Val.t) interp_fun -> ('b, 'c) argument_interp
+| ArgInterpWit : ('a, 'b, 'r) Genarg.genarg_type -> ('b, 'c) argument_interp
+| ArgInterpLegacy :
+  (Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp
+
+type ('a, 'b, 'c) tactic_argument = {
+  arg_parsing : 'a Vernacentries.argument_rule;
+  arg_tag : 'c Val.tag option;
+  arg_intern : ('a, 'b) argument_intern;
+  arg_subst : 'b argument_subst;
+  arg_interp : ('b, 'c) argument_interp;
+  arg_printer : ('a, 'b, 'c) argument_printer;
+}
+
+let intern_fun (type a b c) name (arg : (a, b, c) tactic_argument) : (a, b) Genintern.intern_fun =
+match arg.arg_intern with
+| ArgInternFun f -> f
+| ArgInternWit wit ->
+  fun ist v ->
+    let ans = Genarg.out_gen (glbwit wit) (Tacintern.intern_genarg ist (Genarg.in_gen (rawwit wit) v)) in
+    (ist, ans)
+
+let subst_fun (type a b c) (arg : (a, b, c) tactic_argument) : b Genintern.subst_fun =
+match arg.arg_subst with
+| ArgSubstFun f -> f
+| ArgSubstWit wit ->
+  fun s v ->
+    let ans = Genarg.out_gen (glbwit wit) (Tacsubst.subst_genarg s (Genarg.in_gen (glbwit wit) v)) in
+    ans
+
+let interp_fun (type a b c) name (arg : (a, b, c) tactic_argument) (tag : c Val.tag) : (b, Val.t) interp_fun =
+match arg.arg_interp with
+| ArgInterpRet -> (fun ist v -> Ftactic.return (Geninterp.Val.inject tag v))
+| ArgInterpFun f -> f
+| ArgInterpWit wit ->
+  (fun ist x -> Tacinterp.interp_genarg ist (Genarg.in_gen (glbwit wit) x))
+| ArgInterpLegacy f ->
+  (fun ist v -> Ftactic.enter (fun gl ->
+    let (sigma, v) = Tacmach.New.of_old (fun gl -> f ist gl v) gl in
+    let v = Geninterp.Val.inject tag v in
+    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Ftactic.return v)
+  ))
+
+let argument_extend (type a b c) ~name (arg : (a, b, c) tactic_argument) =
+  let wit = Genarg.create_arg name in
+  let () = Genintern.register_intern0 wit (intern_fun name arg) in
+  let () = Genintern.register_subst0 wit (subst_fun arg) in
+  let tag = match arg.arg_tag with
+  | None ->
+    let () = register_val0 wit None in
+    val_tag (topwit wit)
+  | Some tag ->
+    let () = register_val0 wit (Some tag) in
+    tag
+  in
+  let () = register_interp0 wit (interp_fun name arg tag) in
+  let entry = match arg.arg_parsing with
+  | Vernacentries.Arg_alias e ->
+    let () = Pcoq.register_grammar wit e in
+    e
+  | Vernacentries.Arg_rules rules ->
+    let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in
+    let () = Pcoq.grammar_extend e None (None, [(None, None, rules)]) in
+    e
+  in
+  let (rpr, gpr, tpr) = arg.arg_printer in
+  let () = Pptactic.declare_extra_genarg_pprule wit rpr gpr tpr in
+  let () = create_ltac_quotation name
+    (fun (loc, v) -> Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit wit) v))
+    (entry, None)
+  in
+  (wit, entry)
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 0b2b426018..5b4bedb50a 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -70,6 +70,8 @@ val print_ltacs : unit -> unit
 val print_located_tactic : Libnames.qualid -> unit
 (** Display the absolute name of a tactic. *)
 
+(** {5 TACTIC EXTEND} *)
+
 type _ ty_sig =
 | TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig
 | TyIdent : string * 'r ty_sig -> 'r ty_sig
@@ -79,3 +81,60 @@ type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml
 
 val tactic_extend : string -> string -> level:Int.t ->
   ?deprecation:deprecation -> ty_ml list -> unit
+
+(** {5 ARGUMENT EXTEND} *)
+
+(**
+
+  This is the main entry point for the ARGUMENT EXTEND macro that allows to
+  easily create user-made Ltac arguments.
+
+
+  Each argument has three type parameters. See {!Genarg} for more details.
+  There are two kinds of Ltac arguments, uniform and non-uniform. The former
+  have the same type at each level (raw, glob, top) while the latter may vary.
+
+  When declaring an argument one must provide the following data:
+  - Internalization : raw -> glob
+  - Substitution : glob -> glob
+  - Interpretation : glob -> Ltac dynamic value
+  - Printing for every level
+  - An optional toplevel tag of type top (with the proviso that the
+    interpretation function only produces values with this tag)
+
+  This data can be either given explicitly with the [Fun] constructors, or it
+  can be inherited from another argument with the [Wit] constructors.
+
+*)
+
+type ('a, 'b, 'c) argument_printer =
+  'a Pptactic.raw_extra_genarg_printer *
+  'b Pptactic.glob_extra_genarg_printer *
+  'c Pptactic.extra_genarg_printer
+
+type ('a, 'b) argument_intern =
+| ArgInternFun : ('a, 'b) Genintern.intern_fun -> ('a, 'b) argument_intern
+| ArgInternWit : ('a, 'b, 'c) Genarg.genarg_type -> ('a, 'b) argument_intern
+
+type 'b argument_subst =
+| ArgSubstFun : 'b Genintern.subst_fun -> 'b argument_subst
+| ArgSubstWit : ('a, 'b, 'c) Genarg.genarg_type -> 'b argument_subst
+
+type ('b, 'c) argument_interp =
+| ArgInterpRet : ('c, 'c) argument_interp
+| ArgInterpFun : ('b, Geninterp.Val.t) Geninterp.interp_fun -> ('b, 'c) argument_interp
+| ArgInterpWit : ('a, 'b, 'r) Genarg.genarg_type -> ('b, 'c) argument_interp
+| ArgInterpLegacy :
+  (Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp
+
+type ('a, 'b, 'c) tactic_argument = {
+  arg_parsing : 'a Vernacentries.argument_rule;
+  arg_tag : 'c Geninterp.Val.tag option;
+  arg_intern : ('a, 'b) argument_intern;
+  arg_subst : 'b argument_subst;
+  arg_interp : ('b, 'c) argument_interp;
+  arg_printer : ('a, 'b, 'c) argument_printer;
+}
+
+val argument_extend : name:string -> ('a, 'b, 'c) tactic_argument ->
+  ('a, 'b, 'c) Genarg.genarg_type * 'a Pcoq.Entry.t
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 32c61378db..48d4165830 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2613,3 +2613,30 @@ let vernac_extend ~command ?classifier ?entry ext =
   in
   let () = declare_vernac_classifier command cl in
   List.iteri iter ext
+
+(** VERNAC ARGUMENT EXTEND registering *)
+
+type 'a argument_rule =
+| Arg_alias of 'a Pcoq.Entry.t
+| Arg_rules of 'a Extend.production_rule list
+
+type 'a vernac_argument = {
+  arg_printer : 'a -> Pp.t;
+  arg_parsing : 'a argument_rule;
+}
+
+let vernac_argument_extend ~name arg =
+  let wit = Genarg.create_arg name in
+  let entry = match arg.arg_parsing with
+  | Arg_alias e ->
+    let () = Pcoq.register_grammar wit e in
+    e
+  | Arg_rules rules ->
+    let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in
+    let () = Pcoq.grammar_extend e None (None, [(None, None, rules)]) in
+    e
+  in
+  let pr = arg.arg_printer in
+  let pr x = Genprint.PrinterBasic (fun () -> pr x) in
+  let () = Genprint.register_vernac_print0 wit pr in
+  (wit, entry)
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 34f6029e78..0c4630e45f 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -63,6 +63,24 @@ val vernac_extend :
   ?entry:Vernacexpr.vernac_expr Pcoq.Entry.t ->
   ty_ml list -> unit
 
+(** {5 VERNAC ARGUMENT EXTEND} *)
+
+type 'a argument_rule =
+| Arg_alias of 'a Pcoq.Entry.t
+  (** This is used because CAMLP5 parser can be dumb about rule factorization,
+      which sometimes requires two entries to be the same. *)
+| Arg_rules of 'a Extend.production_rule list
+  (** There is a discrepancy here as we use directly extension rules and thus
+    entries instead of ty_user_symbol and thus arguments as roots. *)
+
+type 'a vernac_argument = {
+  arg_printer : 'a -> Pp.t;
+  arg_parsing : 'a argument_rule;
+}
+
+val vernac_argument_extend : name:string -> 'a vernac_argument ->
+  ('a, unit, unit) Genarg.genarg_type * 'a Pcoq.Entry.t
+
 (** {5 STM classifiers} *)
 
 val get_vernac_classifier :