6 files changed, 60 insertions, 15 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 01b1025da1..8663691c0a 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1365,10 +1365,44 @@ let () =
   let inject (loc, v) = Ltac_plugin.Tacexpr.TacGeneric (Some "ltac2", in_gen (rawwit wit_ltac2) v) in
   Ltac_plugin.Tacentries.create_ltac_quotation "ltac2" inject (e, None)
 
-(* Ltac1 runtime representation of Ltac2 closure quotations *)
-let typ_ltac2 : (Id.t list * glb_tacexpr) Geninterp.Val.typ =
+(* Ltac1 runtime representation of Ltac2 closures. *)
+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,17 +1414,10 @@ 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 (ids, tac) : Id.t list * glb_tacexpr = match Geninterp.Val.eq tag typ_ltac2 with
-    | None -> assert false
-    | Some Refl -> tac
-    in
-    let fold accu id = match Id.Map.find id ist.Geninterp.lfun with
-    | v -> Id.Map.add id (Tac2ffi.of_ext val_ltac1 v) accu
-    | exception Not_found -> assert false
-    in
-    let env_ist = List.fold_left fold Id.Map.empty ids in
-    Proofview.tclIGNORE (Tac2interp.interp { env_ist } tac)
+    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)
   in
   let () = Tacenv.register_ml_tactic ml_name [|eval_fun|] in
   { Tacexpr.mltac_name = ml_name; mltac_index = 0 }
@@ -1398,7 +1425,7 @@ let ltac2_eval =
 let () =
   let open Ltac_plugin in
   let open Tacinterp in
-  let interp ist (ids, tac as self) = match ids with
+  let interp ist (ids, tac) = match ids with
   | [] ->
     (* Evaluate the Ltac2 quotation eagerly *)
     let idtac = Value.of_closure { ist with lfun = Id.Map.empty } (Tacexpr.TacId []) in
@@ -1413,6 +1440,8 @@ let () =
     let mk_arg id = Tacexpr.Reference (Locus.ArgVar (CAst.make id)) in
     let args = List.map mk_arg ids in
     let clos = Tacexpr.TacFun (nas, Tacexpr.TacML (CAst.make (ltac2_eval, mk_arg self_id :: args))) in
+    let self = GTacFun (List.map (fun id -> Name id) ids, tac) in
+    let self = Tac2interp.interp_value { env_ist = Id.Map.empty } self in
     let self = Geninterp.Val.inject (Geninterp.Val.Base typ_ltac2) self in
     let ist = { ist with lfun = Id.Map.singleton self_id self } in
     Ftactic.return (Value.of_closure ist clos)
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 *)
 
diff --git a/user-contrib/Ltac2/tac2interp.ml b/user-contrib/Ltac2/tac2interp.ml
index ed783afce7..8027a22e01 100644
--- a/user-contrib/Ltac2/tac2interp.ml
+++ b/user-contrib/Ltac2/tac2interp.ml
@@ -223,6 +223,8 @@ and eval_pure_args bnd args =
   let map e = eval_pure bnd None e in
   Array.map_of_list map args
 
+let interp_value ist tac =
+  eval_pure ist.env_ist None tac
 
 (** Cross-boundary hacks. *)
 
diff --git a/user-contrib/Ltac2/tac2interp.mli b/user-contrib/Ltac2/tac2interp.mli
index e466c65224..ae7b2ea86d 100644
--- a/user-contrib/Ltac2/tac2interp.mli
+++ b/user-contrib/Ltac2/tac2interp.mli
@@ -18,6 +18,9 @@ val empty_environment : environment
 
 val interp : environment -> glb_tacexpr -> valexpr Proofview.tactic
 
+val interp_value : environment -> glb_tacexpr -> valexpr
+(** Same as [interp] but assumes that the argument is a syntactic value. *)
+
 (* val interp_app : closure -> ml_tactic *)
 
 (** {5 Cross-boundary encodings} *)