Add an abstraction function in the LtacX FFI.

This allows to embed Ltac2 functions manipulating Ltac1 values as simple
Ltac1 values.

4 files changed, 47 insertions, 6 deletions

diff --git a/user-contrib/Ltac2/Ltac1.v b/user-contrib/Ltac2/Ltac1.v
index 1a69708a7d..fd1555c2fb 100644
--- a/user-contrib/Ltac2/Ltac1.v
+++ b/user-contrib/Ltac2/Ltac1.v
@@ -25,6 +25,12 @@ Ltac2 @ external run : t -> unit := "ltac2" "ltac1_run".
 (** Runs an Ltac1 value, assuming it is a 'tactic', i.e. not returning
     anything. *)
 
+Ltac2 @ external lambda : (t -> t) -> t := "ltac2" "ltac1_lambda".
+(** Embed an Ltac2 function into Ltac1 values. Contrarily to the ltac1:(...)
+    quotation, this function allows both to capture an Ltac2 context inside the
+    closure and to return an Ltac1 value. Returning values in Ltac1 is a
+    intrepid endeavour prone to weird runtime semantics. *)
+
 Ltac2 @ external apply : t -> t list -> (t -> unit) -> unit := "ltac2" "ltac1_apply".
 (** Applies an Ltac1 value to a list of arguments, and provides the result in
     CPS style. It does **not** run the returned value. *)
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index d1066c48cb..8663691c0a 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1369,6 +1369,40 @@ let () =
 let typ_ltac2 : valexpr Geninterp.Val.typ =
   Geninterp.Val.create "ltac2:ltac2_eval"
 
+let cast_typ (type a) (tag : a Geninterp.Val.typ) (v : Geninterp.Val.t) : a =
+  let Geninterp.Val.Dyn (tag', v) = v in
+  match Geninterp.Val.eq tag tag' with
+  | None -> assert false
+  | Some Refl -> v
+
+let () =
+  let open Ltac_plugin in
+  (* This is a hack similar to Tacentries.ml_val_tactic_extend *)
+  let intern_fun _ e = Empty.abort e in
+  let subst_fun s v = v in
+  let () = Genintern.register_intern0 wit_ltac2_val intern_fun in
+  let () = Genintern.register_subst0 wit_ltac2_val subst_fun in
+  (* These are bound names and not relevant *)
+  let tac_id = Id.of_string "F" in
+  let arg_id = Id.of_string "X" in
+  let interp_fun ist () =
+    let tac = cast_typ typ_ltac2 @@ Id.Map.get tac_id ist.Tacinterp.lfun in
+    let arg = Id.Map.get arg_id ist.Tacinterp.lfun in
+    let tac = Tac2ffi.to_closure tac in
+    Tac2ffi.apply tac [of_ltac1 arg] >>= fun ans ->
+    let ans = Tac2ffi.to_ext val_ltac1 ans in
+    Ftactic.return ans
+  in
+  let () = Geninterp.register_interp0 wit_ltac2_val interp_fun in
+  define1 "ltac1_lambda" valexpr begin fun f ->
+    let body = Tacexpr.TacGeneric (Some "ltac2", in_gen (glbwit wit_ltac2_val) ()) in
+    let clos = Tacexpr.TacFun ([Name arg_id], Tacexpr.TacArg (CAst.make body)) in
+    let f = Geninterp.Val.inject (Geninterp.Val.Base typ_ltac2) f in
+    let lfun = Id.Map.singleton tac_id f in
+    let ist = { (Tacinterp.default_ist ()) with Tacinterp.lfun } in
+    Proofview.tclUNIT (of_ltac1 (Tacinterp.Value.of_closure ist clos))
+  end
+
 let ltac2_eval =
   let open Ltac_plugin in
   let ml_name = {
@@ -1380,11 +1414,7 @@ let ltac2_eval =
   | tac :: args ->
     (* By convention the first argument is the tactic being applied, the rest
       being the arguments it should be fed with *)
-    let Geninterp.Val.Dyn (tag, tac) = tac in
-    let tac : valexpr = match Geninterp.Val.eq tag typ_ltac2 with
-    | None -> assert false
-    | Some Refl -> tac
-    in
+    let tac = cast_typ typ_ltac2 tac in
     let tac = Tac2ffi.to_closure tac in
     let args = List.map (fun arg -> Tac2ffi.of_ext val_ltac1 arg) args in
     Proofview.tclIGNORE (Tac2ffi.apply tac args)
diff --git a/user-contrib/Ltac2/tac2env.ml b/user-contrib/Ltac2/tac2env.ml
index f6d07e484b..5479ba0d54 100644
--- a/user-contrib/Ltac2/tac2env.ml
+++ b/user-contrib/Ltac2/tac2env.ml
@@ -288,7 +288,8 @@ let ltac1_prefix =
 
 (** Generic arguments *)
 
-let wit_ltac2 = Genarg.make0 "ltac2:value"
+let wit_ltac2 = Genarg.make0 "ltac2:tactic"
+let wit_ltac2_val = Genarg.make0 "ltac2:value"
 let wit_ltac2_constr = Genarg.make0 "ltac2:in-constr"
 let wit_ltac2_quotation = Genarg.make0 "ltac2:quotation"
 let () = Geninterp.register_val0 wit_ltac2 None
diff --git a/user-contrib/Ltac2/tac2env.mli b/user-contrib/Ltac2/tac2env.mli
index af1197c24c..95dcdd7e1b 100644
--- a/user-contrib/Ltac2/tac2env.mli
+++ b/user-contrib/Ltac2/tac2env.mli
@@ -144,6 +144,10 @@ val ltac1_prefix : ModPath.t
 val wit_ltac2 : (Id.t CAst.t list * raw_tacexpr, Id.t list * glb_tacexpr, Util.Empty.t) genarg_type
 (** Ltac2 quotations in Ltac1 code *)
 
+val wit_ltac2_val : (Util.Empty.t, unit, Util.Empty.t) genarg_type
+(** Embedding Ltac2 closures of type [Ltac1.t -> Ltac1.t] inside Ltac1. There is
+    no relevant data because arguments are passed by conventional names. *)
+
 val wit_ltac2_constr : (raw_tacexpr, Id.Set.t * glb_tacexpr, Util.Empty.t) genarg_type
 (** Ltac2 quotations in Gallina terms *)