Allow to pass Ltac1 values to Ltac2 quotations.

This is the dual of #10344.

8 files changed, 123 insertions, 18 deletions

diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 045d028d02..18d2c79461 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -853,6 +853,9 @@ a Ltac1 expression, and semantics of this quotation is the evaluation of the
 corresponding code for its side effects. In particular, it cannot return values,
 and the quotation has type :n:`unit`.
 
+.. productionlist:: coq
+  ltac2_term : ltac1 : ( `ltac_expr` )
+
 Ltac1 **cannot** implicitly access variables from the Ltac2 scope, but this can
 be done with an explicit annotation on the :n:`ltac1` quotation.
 
@@ -890,10 +893,19 @@ Ltac2 from Ltac1
 Same as above by switching Ltac1 by Ltac2 and using the `ltac2` quotation
 instead.
 
-Note that the tactic expression is evaluated eagerly, if one wants to use it as
-an argument to a Ltac1 function, one has to resort to the good old
-:n:`idtac; ltac2:(foo)` trick. For instance, the code below will fail immediately
-and won't print anything.
+.. productionlist:: coq
+  ltac_expr : ltac2 : ( `ltac2_term` )
+            : ltac2 : ( `ident` ... `ident` |- `ltac2_term` )
+
+The typing rules are dual, that is, the optional identifiers are bound
+with type `Ltac2.Ltac1.t` in the Ltac2 expression, which is expected to have
+type unit. The value returned by this quotation is an Ltac1 function with the
+same arity as the number of bound variables.
+
+Note that when no variables are bound, the inner tactic expression is evaluated
+eagerly, if one wants to use it as an argument to a Ltac1 function, one has to
+resort to the good old :n:`idtac; ltac2:(foo)` trick. For instance, the code
+below will fail immediately and won't print anything.
 
 .. coqtop:: in
 
@@ -902,11 +914,17 @@ and won't print anything.
 
 .. coqtop:: all
 
-   Ltac mytac tac := idtac "wow"; tac.
+   Ltac mytac tac := idtac "I am being evaluated"; tac.
 
    Goal True.
    Proof.
+   (* Doesn't print anything *)
    Fail mytac ltac2:(fail).
+   (* Prints and fails *)
+   Fail mytac ltac:(idtac; ltac2:(fail)).
+
+In any case, the value returned by the fully applied quotation is an
+unspecified dummy Ltac1 closure and should not be further used.
 
 Transition from Ltac1
 ---------------------
diff --git a/test-suite/ltac2/ltac2env.v b/test-suite/ltac2/ltac2env.v
new file mode 100644
index 0000000000..743e62932d
--- /dev/null
+++ b/test-suite/ltac2/ltac2env.v
@@ -0,0 +1,15 @@
+Require Import Ltac2.Ltac2.
+
+Ltac2 get_opt o := match o with None => Control.throw Not_found | Some x => x end.
+
+Goal True.
+Proof.
+(* Fails at runtime because not fully applied *)
+Fail ltac1:(ltac2:(x |- ())).
+(* Type mismatch: Ltac1.t vs. constr *)
+Fail ltac1:(ltac2:(x |- pose $x)).
+(* Check that runtime cast is OK *)
+ltac1:(let t := ltac2:(x |- let c := (get_opt (Ltac1.to_constr x)) in pose $c) in t nat).
+(* Type mismatch *)
+Fail ltac1:(let t := ltac2:(x |- let c := (get_opt (Ltac1.to_constr x)) in pose $c) in t ident:(foo)).
+Abort.
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index adc1606016..8a878bb0d0 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -109,6 +109,7 @@ let tac2def_mut = Entry.create "tactic:tac2def_mut"
 let tac2mode = Entry.create "vernac:ltac2_command"
 
 let ltac1_expr = Pltac.tactic_expr
+let tac2expr_in_env = Tac2entries.Pltac.tac2expr_in_env
 
 let inj_wit wit loc x = CAst.make ~loc @@ CTacExt (wit, x)
 let inj_open_constr loc c = inj_wit Tac2quote.wit_open_constr loc c
@@ -129,7 +130,7 @@ let pattern_of_qualid qid =
 
 GRAMMAR EXTEND Gram
   GLOBAL: tac2expr tac2type tac2def_val tac2def_typ tac2def_ext tac2def_syn
-          tac2def_mut;
+          tac2def_mut tac2expr_in_env;
   tac2pat:
     [ "1" LEFTA
       [ qid = Prim.qualid; pl = LIST1 tac2pat LEVEL "0" -> {
@@ -248,6 +249,18 @@ GRAMMAR EXTEND Gram
       | e = ltac1_expr -> { [], e }
     ] ]
   ;
+  tac2expr_in_env :
+    [ [ test_ltac1_env; ids = LIST0 locident; "|-"; e = tac2expr ->
+      { let check { CAst.v = id; CAst.loc = loc } =
+          if Tac2env.is_constructor (Libnames.qualid_of_ident ?loc id) then
+            CErrors.user_err ?loc Pp.(str "Invalid bound Ltac2 identifier " ++ Id.print id)
+        in
+        let () = List.iter check ids in
+        (ids, e)
+      }
+      | tac = tac2expr -> { [], tac }
+    ] ]
+  ;
   let_clause:
     [ [ binder = let_binder; ":="; te = tac2expr ->
       { let (pat, fn) = binder in
@@ -860,7 +873,7 @@ let rules = [
     Stop ++ Aentry test_ampersand_ident ++ Atoken (PKEYWORD "&") ++ Aentry Prim.ident,
     begin fun id _ _ loc ->
       let tac = Tac2quote.of_exact_hyp ~loc (CAst.make ~loc id) in
-      let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in
+      let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) ([], tac) in
       CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg))
     end
   );
@@ -869,7 +882,7 @@ let rules = [
     Stop ++ Atoken (PIDENT (Some "ltac2")) ++ Atoken (PKEYWORD ":") ++
       Atoken (PKEYWORD "(") ++ Aentry tac2expr ++ Atoken (PKEYWORD ")"),
     begin fun _ tac _ _ _ loc ->
-      let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in
+      let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) ([], tac) in
       CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg))
     end
   )
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index f6775ddd1f..34870345a5 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1220,7 +1220,9 @@ let () =
 (** Ltac2 in terms *)
 
 let () =
-  let interp ist poly env sigma concl tac =
+  let interp ist poly env sigma concl (ids, tac) =
+    (* Syntax prevents bound variables in constr quotations *)
+    let () = assert (List.is_empty ids) in
     let ist = Tac2interp.get_env ist in
     let tac = Proofview.tclIGNORE (Tac2interp.interp ist tac) in
     let name, poly = Id.of_string "ltac2", poly in
@@ -1248,25 +1250,73 @@ let () =
 (** Ltac2 in Ltac1 *)
 
 let () =
-  let e = Tac2entries.Pltac.tac2expr in
+  let e = Tac2entries.Pltac.tac2expr_in_env in
   let inject (loc, v) = Ltac_plugin.Tacexpr.TacGeneric (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 =
+  Geninterp.Val.create "ltac2:ltac2_eval"
+
+let ltac2_eval =
+  let open Ltac_plugin in
+  let ml_name = {
+    Tacexpr.mltac_plugin = "ltac2";
+    mltac_tactic = "ltac2_eval";
+  } in
+  let eval_fun args ist = match args with
+  | [] -> assert false
+  | 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)
+  in
+  let () = Tacenv.register_ml_tactic ml_name [|eval_fun|] in
+  { Tacexpr.mltac_name = ml_name; mltac_index = 0 }
+
 let () =
   let open Ltac_plugin in
   let open Tacinterp in
-  let idtac = Value.of_closure (default_ist ()) (Tacexpr.TacId []) in
-  let interp ist tac =
-(*     let ist = Tac2interp.get_env ist.Geninterp.lfun in *)
+  let interp ist (ids, tac as self) = match ids with
+  | [] ->
+    (* Evaluate the Ltac2 quotation eagerly *)
+    let idtac = Value.of_closure { ist with lfun = Id.Map.empty } (Tacexpr.TacId []) in
     let ist = { env_ist = Id.Map.empty } in
     Tac2interp.interp ist tac >>= fun _ ->
     Ftactic.return idtac
+  | _ :: _ ->
+    (* Return a closure [@f := {blob} |- fun ids => ltac2_eval(f, ids) ] *)
+    (* This name cannot clash with Ltac2 variables which are all lowercase *)
+    let self_id = Id.of_string "F" in
+    let nas = List.map (fun id -> Name id) ids in
+    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 = 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)
   in
   Geninterp.register_interp0 wit_ltac2 interp
 
 let () =
   let pr_raw _ = Genprint.PrinterBasic (fun _env _sigma -> mt ()) in
-  let pr_glb e = Genprint.PrinterBasic (fun _env _sigma -> Tac2print.pr_glbexpr e) in
+  let pr_glb (ids, e) =
+    let ids =
+      if List.is_empty ids then mt ()
+      else pr_sequence Id.print ids ++ str " |- "
+    in
+    Genprint.PrinterBasic Pp.(fun _env _sigma -> ids ++ Tac2print.pr_glbexpr e)
+  in
   let pr_top _ = Genprint.TopPrinterBasic mt in
   Genprint.register_print0 wit_ltac2 pr_raw pr_glb pr_top
 
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index 17004bb012..6b7b75f0d4 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -25,6 +25,7 @@ open Tac2intern
 module Pltac =
 struct
 let tac2expr = Pcoq.Entry.create "tactic:tac2expr"
+let tac2expr_in_env = Pcoq.Entry.create "tactic:tac2expr_in_env"
 
 let q_ident = Pcoq.Entry.create "tactic:q_ident"
 let q_bindings = Pcoq.Entry.create "tactic:q_bindings"
diff --git a/user-contrib/Ltac2/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli
index a913a62e45..d96a6a95c5 100644
--- a/user-contrib/Ltac2/tac2entries.mli
+++ b/user-contrib/Ltac2/tac2entries.mli
@@ -64,6 +64,7 @@ val backtrace : backtrace Exninfo.t
 module Pltac :
 sig
 val tac2expr : raw_tacexpr Pcoq.Entry.t
+val tac2expr_in_env : (Id.t CAst.t list * raw_tacexpr) Pcoq.Entry.t
 
 (** Quoted entries. To be used for complex notations. *)
 
diff --git a/user-contrib/Ltac2/tac2env.mli b/user-contrib/Ltac2/tac2env.mli
index 2dbb16e184..2f4a49a0f5 100644
--- a/user-contrib/Ltac2/tac2env.mli
+++ b/user-contrib/Ltac2/tac2env.mli
@@ -140,7 +140,7 @@ val ltac1_prefix : ModPath.t
 
 (** {5 Generic arguments} *)
 
-val wit_ltac2 : (raw_tacexpr, glb_tacexpr, Util.Empty.t) genarg_type
+val wit_ltac2 : (Id.t CAst.t list * raw_tacexpr, Id.t list * glb_tacexpr, Util.Empty.t) genarg_type
 val wit_ltac2_quotation : (Id.t Loc.located, Id.t, Util.Empty.t) genarg_type
 
 (** {5 Helper functions} *)
diff --git a/user-contrib/Ltac2/tac2intern.ml b/user-contrib/Ltac2/tac2intern.ml
index 0961e9c9c9..5b3aa799a1 100644
--- a/user-contrib/Ltac2/tac2intern.ml
+++ b/user-contrib/Ltac2/tac2intern.ml
@@ -22,10 +22,12 @@ open Tac2expr
 (** Hardwired types and constants *)
 
 let coq_type n = KerName.make Tac2env.coq_prefix (Label.make n)
+let ltac1_type n = KerName.make Tac2env.ltac1_prefix (Label.make n)
 
 let t_int = coq_type "int"
 let t_string = coq_type "string"
 let t_constr = coq_type "constr"
+let t_ltac1 = ltac1_type "t"
 
 (** Union find *)
 
@@ -1505,7 +1507,8 @@ let rec subst_rawexpr subst ({loc;v=tr} as t) = match tr with
 
 let () =
   let open Genintern in
-  let intern ist tac =
+  let intern ist (ids, tac) =
+    let ids = List.map (fun { CAst.v = id } -> id) ids in
     let env = match Genintern.Store.get ist.extra ltac2_env with
     | None ->
       (* Only happens when Ltac2 is called from a constr or ltac1 quotation *)
@@ -1514,13 +1517,17 @@ let () =
       else { env with env_str = false }
     | Some env -> env
     in
+    let fold env id =
+      push_name (Name id) (monomorphic (GTypRef (Other t_ltac1, []))) env
+    in
+    let env = List.fold_left fold env ids in
     let loc = tac.loc in
     let (tac, t) = intern_rec env tac in
     let () = check_elt_unit loc env t in
-    (ist, tac)
+    (ist, (ids, tac))
   in
   Genintern.register_intern0 wit_ltac2 intern
-let () = Genintern.register_subst0 wit_ltac2 subst_expr
+let () = Genintern.register_subst0 wit_ltac2 (fun s (ids, e) -> ids, subst_expr s e)
 
 let () =
   let open Genintern in