Merge PR #12204: Ltac helper functions API

4 files changed, 136 insertions, 3 deletions

diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 9910796d9c..e6c59f446d 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -683,6 +683,111 @@ let tactic_extend plugin_name tacname ~level ?deprecation sign =
   Tacenv.register_ml_tactic ml_tactic_name @@ Array.of_list (List.map eval sign);
   Mltop.declare_cache_obj obj plugin_name
 
+type (_, 'a) ml_ty_sig =
+| MLTyNil : ('a, 'a) ml_ty_sig
+| MLTyArg : ('r, 'a) ml_ty_sig -> (Geninterp.Val.t -> 'r, 'a) ml_ty_sig
+
+let rec ml_sig_len : type r a. (r, a) ml_ty_sig -> int = function
+| MLTyNil -> 0
+| MLTyArg sign -> 1 + ml_sig_len sign
+
+let rec cast_ml : type r a. (r, a) ml_ty_sig -> r -> Geninterp.Val.t list -> a =
+  fun sign f ->
+  match sign with
+  | MLTyNil ->
+    begin function
+    | [] -> f
+    | _ :: _ -> CErrors.anomaly (str "Arity mismatch")
+    end
+  | MLTyArg sign ->
+    function
+    | [] -> CErrors.anomaly (str "Arity mismatch")
+    | arg :: args -> cast_ml sign (f arg) args
+
+let ml_tactic_extend ~plugin ~name ~local ?deprecation sign tac =
+  let open Tacexpr in
+  let tac args _ = cast_ml sign tac args in
+  let ml_tactic_name = { mltac_tactic = name; mltac_plugin = plugin } in
+  let ml = { mltac_name = ml_tactic_name; mltac_index = 0 } in
+  let len = ml_sig_len sign in
+  let args = List.init len (fun i -> Id.of_string (Printf.sprintf "arg%i" i)) in
+  let vars = List.map (fun id -> Name id) args in
+  let args = List.map (fun id -> Reference (Locus.ArgVar (CAst.make id))) args in
+  let body = Tacexpr.TacFun (vars, Tacexpr.TacML (CAst.make (ml, args))) in
+  let id = Names.Id.of_string name in
+  let obj () = Tacenv.register_ltac true local id body ?deprecation in
+  let () = Tacenv.register_ml_tactic ml_tactic_name [|tac|] in
+  Mltop.declare_cache_obj obj plugin
+
+module MLName =
+struct
+  open Tacexpr
+  type t = ml_tactic_name
+  let compare tac1 tac2 =
+    let c = String.compare tac1.mltac_tactic tac2.mltac_tactic in
+    if c = 0 then String.compare tac1.mltac_plugin tac2.mltac_plugin
+    else c
+end
+
+module MLTacMap = Map.Make(MLName)
+
+let ml_table : (Geninterp.Val.t list -> Geninterp.Val.t Ftactic.t) MLTacMap.t ref = ref MLTacMap.empty
+
+type ml_ltac_val = {
+  tacval_tac : Tacexpr.ml_tactic_name;
+  tacval_var : Id.t list;
+}
+
+let in_tacval =
+(*  This is a hack to emulate value-returning ML-implemented tactics in Ltac.
+    We use a dummy generic argument to work around the limitations of the Ltac
+    runtime. Indeed, the TacML node needs to return unit values, since it is
+    considered a "tactic" in the runtime. Changing it to allow arbitrary values
+    would require to toggle this status, and thus to make it a "value" node.
+    This would in turn create too much backwards incompatibility. Instead, we
+    piggy back on the TacGeneric node, which by construction is used to return
+    values.
+
+    The trick is to represent a n-ary application of a ML function as a generic
+    argument. We store in the node the name of the tactic and its arity, while
+    giving canonical names to the bound variables of the closure. This trick is
+    already performed in several external developments for specific calls, we
+    make it here generic. The argument should not be used for other purposes, so
+    we only export the registering functions.
+  *)
+  let wit : (Empty.t, ml_ltac_val, Geninterp.Val.t) Genarg.genarg_type =
+    Genarg.create_arg "ltac:val"
+  in
+  (* No need to internalize this ever *)
+  let intern_fun _ e = Empty.abort e in
+  let subst_fun s v = v in
+  let () = Genintern.register_intern0 wit intern_fun in
+  let () = Genintern.register_subst0 wit subst_fun in
+  (* No need to register a value tag for it via register_val0 since we will
+     never access this genarg directly. *)
+  let interp_fun ist tac =
+    let args = List.map (fun id -> Id.Map.get id ist.Geninterp.lfun) tac.tacval_var in
+    let tac = MLTacMap.get tac.tacval_tac !ml_table in
+    tac args
+  in
+  let () = Geninterp.register_interp0 wit interp_fun in
+  (fun v -> Genarg.in_gen (Genarg.Glbwit wit) v)
+
+
+let ml_val_tactic_extend ~plugin ~name ~local ?deprecation sign tac =
+  let open Tacexpr in
+  let tac args = cast_ml sign tac args in
+  let ml_tactic_name = { mltac_tactic = name; mltac_plugin = plugin } in
+  let len = ml_sig_len sign in
+  let vars = List.init len (fun i -> Id.of_string (Printf.sprintf "arg%i" i)) in
+  let body = TacGeneric (in_tacval { tacval_tac = ml_tactic_name;  tacval_var = vars }) in
+  let vars = List.map (fun id -> Name id) vars in
+  let body = Tacexpr.TacFun (vars, Tacexpr.TacArg (CAst.make body)) in
+  let id = Names.Id.of_string name in
+  let obj () = Tacenv.register_ltac true local id body ?deprecation in
+  let () = assert (not @@ MLTacMap.mem ml_tactic_name !ml_table) in
+  let () = ml_table := MLTacMap.add ml_tactic_name tac !ml_table in
+  Mltop.declare_cache_obj obj plugin
 
 (** ARGUMENT EXTEND *)
 
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index ce38431a18..6ee3ce091b 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -69,6 +69,25 @@ val print_ltacs : unit -> unit
 val print_located_tactic : Libnames.qualid -> unit
 (** Display the absolute name of a tactic. *)
 
+(** {5 Low-level registering of tactics} *)
+
+type (_, 'a) ml_ty_sig =
+| MLTyNil : ('a, 'a) ml_ty_sig
+| MLTyArg : ('r, 'a) ml_ty_sig -> (Geninterp.Val.t -> 'r, 'a) ml_ty_sig
+
+val ml_tactic_extend : plugin:string -> name:string -> local:locality_flag ->
+  ?deprecation:Deprecation.t -> ('r, unit Proofview.tactic) ml_ty_sig -> 'r -> unit
+(** Helper function to define directly an Ltac function in OCaml without any
+    associated parsing rule nor further shenanigans. The Ltac function will be
+    defined as [name] in the Coq file that loads the ML plugin where this
+    function is called. It will have the arity given by the [ml_ty_sig]
+    argument. *)
+
+val ml_val_tactic_extend : plugin:string -> name:string -> local:locality_flag ->
+  ?deprecation:Deprecation.t -> ('r, Geninterp.Val.t Ftactic.t) ml_ty_sig -> 'r -> unit
+(** Same as {!ml_tactic_extend} but the function can return an argument
+    instead. *)
+
 (** {5 TACTIC EXTEND} *)
 
 type _ ty_sig =
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index dda7f0742c..6debc7d9b9 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1895,8 +1895,7 @@ module Value = struct
     let closure = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in
     of_tacvalue closure
 
-  (** Apply toplevel tactic values *)
-  let apply (f : value) (args: value list) =
+  let apply_expr f args =
     let fold arg (i, vars, lfun) =
       let id = Id.of_string ("x" ^ string_of_int i) in
       let x = Reference (ArgVar CAst.(make id)) in
@@ -1905,9 +1904,18 @@ module Value = struct
     let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in
     let lfun = Id.Map.add (Id.of_string "F") f lfun in
     let ist = { (default_ist ()) with lfun = lfun; } in
-    let tac = TacArg(CAst.make @@ TacCall (CAst.make (ArgVar CAst.(make @@ Id.of_string "F"),args))) in
+    ist, TacArg(CAst.make @@ TacCall (CAst.make (ArgVar CAst.(make @@ Id.of_string "F"),args)))
+
+
+  (** Apply toplevel tactic values *)
+  let apply (f : value) (args: value list) =
+    let ist, tac = apply_expr f args in
     eval_tactic_ist ist tac
 
+  let apply_val (f : value) (args: value list) =
+    let ist, tac = apply_expr f args in
+    val_interp ist tac
+
 end
 
 (* globalization + interpretation *)
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index ce34356a37..cbb17bf0fa 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -29,6 +29,7 @@ sig
   val of_closure : Geninterp.interp_sign -> glob_tactic_expr -> t
   val cast : 'a typed_abstract_argument_type -> Geninterp.Val.t -> 'a
   val apply : t -> t list -> unit Proofview.tactic
+  val apply_val : t -> t list -> t Ftactic.t
 end
 
 (** Values for interpretation *)