Gentactic hide that the underlying implem is genarg based

dev/ci/user-overlays/21568-SkySkimmer-gentac-up.sh

@@ -0,0 +1,5 @@
+overlay tactician https://github.com/SkySkimmer/coq-tactician gentac-up 21568
+
+overlay mtac2 https://github.com/SkySkimmer/Mtac2 gentac-up 21568
+
+overlay waterproof https://github.com/SkySkimmer/coq-waterproof gentac-up 21568

plugins/ltac/pltac.ml

@@ -60,7 +60,6 @@ let () =
   register_grammar wit_constr_with_bindings (constr_with_bindings);
   register_grammar wit_bindings (bindings);
   register_grammar wit_tactic (tactic);
-  register_grammar wit_ltac (tactic);
   register_grammar wit_clause_dft_concl (clause_dft_concl);
   register_grammar wit_destruction_arg (destruction_arg);
   ()

plugins/ltac/pptactic.ml

@@ -1433,7 +1433,12 @@ let () =
   ltop (LevelLe 0)
 
 let () =
-  let pr_unit _env _sigma _ _ _ _ () = str "()" in
-  let printer env sigma _ _ prtac = prtac env sigma in
-  declare_extra_genarg_pprule_with_level wit_ltac printer printer pr_unit
-  ltop (LevelLe 0)
+  let printer f x =
+    Genprint.PrinterNeedsLevel {
+      default_already_surrounded = ltop;
+      default_ensure_surrounded = LevelLe 0;
+      printer = (fun env sigma n -> f env sigma n x);
+    }
+  in
+  Gentactic.register_print wit_ltac (printer pr_raw_tactic_level)
+    (printer (fun env _sigma n x -> pr_glob_tactic_level env n x))

plugins/ltac/tacarg.ml

@@ -32,7 +32,7 @@ let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type =
 
 let wit_ltac_in_term = make0 "ltac_in_term"
 
-let wit_ltac = make0 ~dyn:(val_tag (topwit Stdarg.wit_unit)) "ltac"
+let wit_ltac = Gentactic.make "ltac"
 
 let wit_destruction_arg =
   make0 "destruction_arg"

plugins/ltac/tacarg.mli

@@ -49,7 +49,7 @@ val wit_ltac_in_term : (raw_tactic_expr, Names.Id.Set.t * glob_tactic_expr, Util
 (** [wit_ltac] is subtly different from [wit_tactic]: they only change for their
     toplevel interpretation. The one of [wit_ltac] forces the tactic and
     discards the result. *)
-val wit_ltac : (raw_tactic_expr, glob_tactic_expr, unit) genarg_type
+val wit_ltac : (raw_tactic_expr, glob_tactic_expr) Gentactic.tag
 
 val wit_destruction_arg :
   (constr_expr with_bindings Tactics.destruction_arg,

plugins/ltac/tacintern.ml

@@ -776,7 +776,7 @@ let () =
   Genintern.register_intern0 wit_hyp (lift intern_hyp);
   Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg);
   Genintern.register_intern0 wit_ltac_in_term (lift intern_ltac_in_term);
-  Genintern.register_intern0 wit_ltac (lift intern_ltac);
+  Gentactic.register_intern wit_ltac (lift intern_ltac);
   Genintern.register_intern0 wit_quant_hyp (lift intern_quantified_hypothesis);
   Genintern.register_intern0 wit_constr (fun ist c -> (ist,intern_constr ist c));
   Genintern.register_intern0 wit_uconstr (fun ist c -> (ist,intern_constr ist c));

plugins/ltac/tacinterp.ml

@@ -2147,8 +2147,13 @@ let () =
   register_interp0 wit_tactic interp
 
 let () =
-  let interp ist tac = eval_tactic_ist ist tac >>= fun () -> Ftactic.return () in
-  register_interp0 wit_ltac interp
+  let interp lfun tac =
+    let open Proofview.Notations in
+    Proofview.tclProofInfo[@ocaml.warning"-3"] >>= fun (_name, poly) ->
+    let ist = { lfun; poly; extra = TacStore.empty } in
+    eval_tactic_ist ist tac
+  in
+  Gentactic.register_interp wit_ltac interp
 
 let () =
   register_interp0 wit_uconstr (fun ist c -> Ftactic.enter begin fun gl ->

plugins/ltac/tacsubst.ml

@@ -288,7 +288,7 @@ let () =
   Gensubst.register_subst0 wit_simple_intropattern subst_intro_pattern;
   Gensubst.register_subst0 wit_tactic subst_tactic;
   Gensubst.register_subst0 wit_ltac_in_term (fun s (used_ntnvars,tac) -> used_ntnvars, subst_tactic s tac);
-  Gensubst.register_subst0 wit_ltac subst_tactic;
+  Gentactic.register_subst wit_ltac subst_tactic;
   Gensubst.register_subst0 wit_constr subst_glob_constr;
   Gensubst.register_subst0 wit_clause_dft_concl (fun _ v -> v);
   Gensubst.register_subst0 wit_uconstr (fun subst c -> subst_glob_constr subst c);

plugins/ltac2/tac2env.ml

@@ -308,10 +308,7 @@ type var_quotation_kind =
 
 let wit_ltac2_constr = Genarg.make0 "ltac2:in-constr"
 let wit_ltac2_var_quotation = Genarg.make0 "ltac2:quotation"
-let wit_ltac2_tac = Genarg.make0 "ltac2:tactic"
-
-let () = Geninterp.register_val0 wit_ltac2_tac
-    (Some (Geninterp.val_tag (Genarg.topwit Stdarg.wit_unit)))
+let wit_ltac2_tac = Gentactic.make "ltac2:tactic"
 
 let is_constructor_id id =
   let id = Id.to_string id in

plugins/ltac2/tac2env.mli

@@ -184,7 +184,7 @@ val ltac1_prefix : ModPath.t
 val wit_ltac2_constr : (raw_tacexpr, Id.Set.t * glb_tacexpr, Util.Empty.t) genarg_type
 (** Ltac2 quotations in Gallina terms *)
 
-val wit_ltac2_tac : (raw_tacexpr, glb_tacexpr, unit) genarg_type
+val wit_ltac2_tac : (raw_tacexpr, glb_tacexpr) Gentactic.tag
 (** Ltac2 as a generic tactic depending on proof mode (eg as argument to Solve Obligations) *)
 
 type var_quotation_kind =

plugins/ltac2/tac2extravals.ml

@@ -354,10 +354,9 @@ let () =
   let interp _ist tac =
     (* XXX should we be doing something with the ist? *)
     let tac = Tac2interp.(interp empty_environment) tac in
-    Proofview.tclBIND tac (fun _ ->
-        Ftactic.return (Geninterp.Val.inject (Geninterp.val_tag (topwit Stdarg.wit_unit)) ()))
+    Proofview.tclIGNORE tac
   in
-  Geninterp.register_interp0 wit_ltac2_tac interp
+  Gentactic.register_interp wit_ltac2_tac interp
 
 let () =
   let interp env sigma ist (kind,id) =
@@ -443,8 +442,7 @@ let () =
       Tac2print.pr_rawexpr_gen ~avoid:Id.Set.empty E5 e)
   in
   let pr_glb e = Genprint.PrinterBasic (fun _ _ -> Tac2print.pr_glbexpr ~avoid:Id.Set.empty e) in
-  let pr_top () = assert false in
-  Genprint.register_print0 wit_ltac2_tac pr_raw pr_glb pr_top
+  Gentactic.register_print wit_ltac2_tac pr_raw pr_glb
 
 (** Built-in notation entries *)
 

plugins/ltac2/tac2intern.ml

@@ -2140,10 +2140,10 @@ let () =
     let tac, _ = intern_rec env (Some (GTypRef (Tuple 0, []))) tac in
     ist, tac
   in
-  Genintern.register_intern0 wit_ltac2_tac intern
+  Gentactic.register_intern wit_ltac2_tac intern
 
 let () = Gensubst.register_subst0 wit_ltac2_constr (fun s (ids, e) -> ids, subst_expr s e)
-let () = Gensubst.register_subst0 wit_ltac2_tac subst_expr
+let () = Gentactic.register_subst wit_ltac2_tac subst_expr
 
 let intern_var_quotation_gen ~ispat ist (kind, { CAst.v = id; loc }) =
   let open Genintern in

pretyping/genarg.mli

@@ -32,19 +32,6 @@
 
       NB: only the base [ExtraArg] is allowed here.
 
-    - tactic arguments to commands defined without depending on ltac_plugin
-      (VernacProof, HintsExtern, Hint Rewrite, etc).
-
-      Must be registered with [Genintern.register_intern0] and
-      [Genintern.register_interp0].
-
-      The glob level can be kept (currently with Hint Extern and Hint
-      Rewrite) so [Gensubst.register_subst0] is also needed.
-
-      Currently AFAICT this is just [Tacarg.wit_ltac].
-
-      NB: only the base [ExtraArg] is allowed here.
-
     - vernac arguments, used by vernac extend. Usually declared in mlg
       using VERNAC ARGUMENT EXTEND then used in VERNAC EXTEND.
 
@@ -63,15 +50,15 @@
       then used in TACTIC EXTEND.
 
       Must be registered with [Genintern.register_intern0],
-      [Gensubst.register_subst0] and [Genintern.register_interp0].
+      [Gensubst.register_subst0] and [Geninterp.register_interp0].
 
       Must be registered with [Procq.register_grammar] as tactic extend
       only gets the genarg as argument so must get the grammar from
       the registration.
 
       They must be associated with a [Geninterp.Val.tag] using [Geninterp.register_val0]
       (which creates a fresh tag if passed [None]).
-      Note: although [Genintern.register_interp0] registers a producer
+      Note: although [Geninterp.register_interp0] registers a producer
       of arbitrary [Geninterp.Val.t], tactic_extend requires them to be of the tag
       registered by [Geninterp.register_val0] to work properly.
 

tactics/gentactic.ml

@@ -10,35 +10,103 @@
 
 open Names
 
-type raw_generic_tactic = Genarg.raw_generic_argument
+module TDyn = Dyn.Make()
 
-type glob_generic_tactic = Genarg.glob_generic_argument
+type ('raw, 'glb) tag = ('raw * 'glb) TDyn.tag
 
-let of_raw_genarg x = x
+type raw_generic_tactic = Raw : ('raw, _) tag * 'raw -> raw_generic_tactic
 
-let to_raw_genarg x = x
+type glob_generic_tactic = Glb : (_, 'glb) tag * 'glb -> glob_generic_tactic
 
-let of_glob_genarg x = x
+let make name : _ tag = TDyn.create name
 
-let print_raw = Pputils.pr_raw_generic
+let empty = make "empty"
 
-let print_glob = Pputils.pr_glb_generic
+let of_raw (type a) (tag:(a, _) tag) (x:a) : raw_generic_tactic =
+  Raw (tag, x)
 
-let subst = Gensubst.generic_substitute
+module Print = struct
+  type _ t = Print : {
+      raw_print : 'raw Genprint.printer;
+      glb_print : 'glb Genprint.printer;
+    } -> ('raw * 'glb) t
+end
 
-let intern ?(strict=true) env ?(ltacvars=Id.Set.empty) v =
+module PrintMap = TDyn.Map(Print)
+
+let printers = ref PrintMap.empty
+
+let register_print tag raw_print glb_print =
+  assert (not @@ PrintMap.mem tag !printers);
+  printers := PrintMap.add tag (Print {raw_print; glb_print}) !printers
+
+let apply_printer env sigma level = function
+  | Genprint.PrinterBasic pp -> pp env sigma
+  | Genprint.PrinterNeedsLevel { default_already_surrounded; printer } ->
+    let level = Option.default default_already_surrounded level in
+    printer env sigma level
+
+let print_raw env sigma ?level (Raw (tag, v)) =
+  let Print {raw_print} = PrintMap.find tag !printers in
+  apply_printer env sigma level (raw_print v)
+
+let print_glob env sigma ?level (Glb (tag, v)) =
+  let Print {glb_print} = PrintMap.find tag !printers in
+  apply_printer env sigma level (glb_print v)
+
+module Subst = struct
+  type _ t = Subst : 'glb Gensubst.subst_fun -> (_ * 'glb) t
+end
+
+module SubstMap = TDyn.Map(Subst)
+
+let substs = ref SubstMap.empty
+
+let register_subst tag subst =
+  assert (not @@ SubstMap.mem tag !substs);
+  substs := SubstMap.add tag (Subst subst) !substs
+
+let subst subst (Glb (tag, v)) =
+  let Subst f = SubstMap.find tag !substs in
+  Glb (tag, f subst v)
+
+module Intern = struct
+  (* XXX change type to match how it's called instead of reusing Genintern.intern_fun *)
+  type _ t = Intern : ('raw, 'glb) Genintern.intern_fun -> ('raw * 'glb) t
+end
+
+module InternMap = TDyn.Map(Intern)
+
+let interns = ref InternMap.empty
+
+let register_intern tag intern =
+  assert (not @@ InternMap.mem tag !interns);
+  interns := InternMap.add tag (Intern intern) !interns
+
+let intern ?(strict=true) env ?(ltacvars=Id.Set.empty) (Raw (tag, v)) =
+  let Intern intern = InternMap.find tag !interns in
   let ist = { (Genintern.empty_glob_sign ~strict env) with ltacvars } in
-  let _, v = Genintern.generic_intern ist v in
-  v
-
-let interp ?(lfun=Id.Map.empty) v =
-  let open Geninterp in
-  let open Proofview.Notations in
-  Proofview.tclProofInfo[@ocaml.warning"-3"] >>= fun (_name, poly) ->
-  let ist = { lfun; poly; extra = TacStore.empty } in
-  let Genarg.GenArg (Glbwit tag, v) = v in
-  let v = Geninterp.interp tag ist v in
-  Ftactic.run v (fun _ -> Proofview.tclUNIT ())
+  let _, v = intern ist v in
+  Glb (tag, v)
+
+type 'glb interp_fun = Geninterp.Val.t Id.Map.t -> 'glb -> unit Proofview.tactic
+
+module Interp =
+struct
+  type _ t = Interp : 'glb interp_fun -> (_ * 'glb) t
+end
+
+module InterpMap = TDyn.Map(Interp)
+
+let interps = ref InterpMap.empty
+
+let register_interp tag interp =
+  assert (not @@ InterpMap.mem tag !interps);
+  interps := InterpMap.add tag (Interp interp) !interps
+
+let interp ?(lfun=Id.Map.empty) (Glb (tag, v)) =
+  let Interp interp = InterpMap.find tag !interps in
+  interp lfun v
 
 let wit_generic_tactic = Genarg.make0 "generic_tactic"
 

tactics/gentactic.mli

@@ -8,36 +8,44 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+open Util
 open Names
 
-(** Generic tactic expressions.
-    Internally implemented using [Genarg]. *)
+(** Generic tactic expressions. *)
 
 type raw_generic_tactic
 
 type glob_generic_tactic
 
-val of_raw_genarg : Genarg.raw_generic_argument -> raw_generic_tactic
-(** The genarg must have registrations for all the following APIs. *)
+type ('raw, 'glob) tag
 
-val of_glob_genarg : Genarg.glob_generic_argument -> glob_generic_tactic
-(** The genarg must have registrations for all the following APIs
-    except those operating at the "raw" level. *)
+val make : string -> ('raw, 'glb) tag
+(** Each declared tag must be registered using all the following [register] functions
+    (except when the callback cannot be called ie when the value type at that level is empty). *)
+
+val empty : (Empty.t, Empty.t) tag
+
+val of_raw : ('raw,_) tag -> 'raw -> raw_generic_tactic
+
+val register_print : ('raw, 'glb) tag -> 'raw Genprint.printer -> 'glb Genprint.printer -> unit
 
 val print_raw : Environ.env -> Evd.evar_map -> ?level:Constrexpr.entry_relative_level ->
   raw_generic_tactic -> Pp.t
 
 val print_glob : Environ.env -> Evd.evar_map -> ?level:Constrexpr.entry_relative_level ->
   glob_generic_tactic -> Pp.t
 
+val register_subst : (_, 'glb) tag -> 'glb Gensubst.subst_fun -> unit
+
 val subst : Mod_subst.substitution -> glob_generic_tactic -> glob_generic_tactic
 
+val register_intern : ('raw, 'glb) tag -> ('raw, 'glb) Genintern.intern_fun -> unit
+
 val intern : ?strict:bool -> Environ.env -> ?ltacvars:Id.Set.t -> raw_generic_tactic -> glob_generic_tactic
 (** [strict] is default true *)
 
+val register_interp : (_, 'glb) tag -> (Geninterp.Val.t Id.Map.t -> 'glb -> unit Proofview.tactic) -> unit
+
 val interp : ?lfun:Geninterp.Val.t Id.Map.t -> glob_generic_tactic -> unit Proofview.tactic
 
 val wit_generic_tactic : raw_generic_tactic Genarg.vernac_genarg_type
-
-val to_raw_genarg : raw_generic_tactic -> Genarg.raw_generic_argument
-(** For serlib *)

vernac/pvernac.ml

@@ -12,7 +12,7 @@ open Procq
 
 type proof_mode_entry = ProofMode : {
   command_entry : Vernacexpr.vernac_expr Entry.t;
-  wit_tactic_expr : ('raw,_,unit) Genarg.genarg_type;
+  wit_tactic_expr : ('raw,_) Gentactic.tag;
   tactic_expr_entry : 'raw Entry.t;
 } -> proof_mode_entry
 
@@ -47,7 +47,7 @@ let noedit_tactic_expr = Entry.make "noedit_tactic_expr"
 
 let noedit_mode_entry = ProofMode {
   command_entry = noedit_mode;
-  wit_tactic_expr = Stdarg.wit_unit;
+  wit_tactic_expr = Gentactic.empty;
   tactic_expr_entry = noedit_tactic_expr;
 }
 
@@ -103,7 +103,7 @@ module Vernac_ =
       let mode = get_default_proof_mode () in
       let ProofMode mode = find_proof_mode mode in
       let+ v = Procq.Entry.parse_token_stream mode.tactic_expr_entry strm in
-      Gentactic.of_raw_genarg Genarg.(in_gen (rawwit mode.wit_tactic_expr) v)
+      Gentactic.of_raw mode.wit_tactic_expr v
 
     let command_entry =
       Procq.Entry.(of_parser "command_entry"

vernac/pvernac.mli

@@ -53,7 +53,7 @@ val main_entry : proof_mode option -> vernac_control option Entry.t
 
 type proof_mode_entry = ProofMode : {
     command_entry : Vernacexpr.vernac_expr Entry.t;
-    wit_tactic_expr : ('raw,_,unit) Genarg.genarg_type;
+    wit_tactic_expr : ('raw,_) Gentactic.tag;
     tactic_expr_entry : 'raw Entry.t;
 } -> proof_mode_entry