Merge PR #10344: Allow to pass Ltac2 values to Ltac1 quotations

Ack-by: Zimmi48
Reviewed-by: gares

5 files changed, 115 insertions, 33 deletions

diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 36eeff6192..3036648b08 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -850,8 +850,17 @@ 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`.
 
-Beware, Ltac1 **cannot** access variables from the Ltac2 scope. One is limited
-to the use of standalone function calls.
+Ltac1 **cannot** implicitly access variables from the Ltac2 scope, but this can
+be done via an explicit annotation to the :n:`ltac1` quotation.
+
+.. productionlist:: coq
+  ltac2_term : ltac1 : ( `ident` ... `ident` |- `ltac_expr` )
+
+The return type of this expression is a function of the same arity as the number
+of identifiers, with arguments of type `Ltac2.Ltac1.t` (see below). This syntax
+will bind the variables in the quoted Ltac1 code as if they had been bound from
+Ltac1 itself. Similarly, the arguments applied to the quotation will be passed
+at runtime to the Ltac1 code.
 
 Low-level API
 +++++++++++++
@@ -869,6 +878,9 @@ focus is very hard. This is why some functions return a continuation-passing
 style value, as it can dispatch dynamically between focused and unfocused
 behaviour.
 
+The same mechanism for explicit binding of variables as described in the
+previous section applies.
+
 Ltac2 from Ltac1
 ~~~~~~~~~~~~~~~~
 
diff --git a/test-suite/ltac2/compat.v b/test-suite/ltac2/compat.v
index 489fa638e4..9c11d19c27 100644
--- a/test-suite/ltac2/compat.v
+++ b/test-suite/ltac2/compat.v
@@ -27,6 +27,19 @@ Fail Ltac2 bar nay := ltac1:(discriminate nay).
 Fail Ltac2 pose1 (v : constr) :=
   ltac1:(pose $v).
 
+(** Variables explicitly crossing the boundary must satisfy typing properties *)
+Goal True.
+Proof.
+(* Wrong type *)
+Fail ltac1:(x |- idtac) 0.
+(* OK, and runtime has access to variable *)
+ltac1:(x |- idtac x) (Ltac1.of_constr constr:(Type)).
+
+(* Same for ltac1val *)
+Fail Ltac1.run (ltac1val:(x |- idtac) 0).
+Ltac1.run (ltac1val:(x |- idtac x) (Ltac1.of_constr constr:(Type))).
+Abort.
+
 (** Test calls to Ltac2 from Ltac1 *)
 
 Set Default Proof Mode "Classic".
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index e348396aad..23b5f4daef 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -37,6 +37,8 @@ let (<+>) (lk1 : lookahead) lk2 n strm = match lk1 n strm with
 | None -> lk2 n strm
 | Some n -> Some n
 
+let lk_empty n strm = Some n
+
 let lk_kw kw n strm = match stream_nth n strm with
 | KEYWORD kw' | IDENT kw' -> if String.equal kw kw' then Some (n + 1) else None
 | _ -> None
@@ -51,6 +53,9 @@ let lk_int n strm = match stream_nth n strm with
 
 let lk_ident_or_anti = lk_ident <+> (lk_kw "$" >> lk_ident)
 
+let rec lk_ident_list n strm =
+  ((lk_ident >> lk_ident_list) <+> lk_empty) n strm
+
 (* lookahead for (x:=t), (?x:=t) and (1:=t) *)
 let test_lpar_idnum_coloneq =
   entry_of_lookahead "test_lpar_idnum_coloneq" begin
@@ -85,6 +90,11 @@ let test_dollar_ident =
     lk_kw "$" >> lk_ident
   end
 
+let test_ltac1_env =
+  entry_of_lookahead "test_ltac1_env" begin
+    lk_ident_list >> lk_kw "|-"
+  end
+
 let tac2expr = Tac2entries.Pltac.tac2expr
 let tac2type = Entry.create "tactic:tac2type"
 let tac2def_val = Entry.create "tactic:tac2def_val"
@@ -225,8 +235,13 @@ GRAMMAR EXTEND Gram
       | IDENT "ident"; ":"; "("; c = lident; ")" -> { Tac2quote.of_ident c }
       | IDENT "pattern"; ":"; "("; c = Constr.lconstr_pattern; ")" -> { inj_pattern loc c }
       | IDENT "reference"; ":"; "("; c = globref; ")" -> { inj_reference loc c }
-      | IDENT "ltac1"; ":"; "("; qid = ltac1_expr; ")" -> { inj_ltac1 loc qid }
-      | IDENT "ltac1val"; ":"; "("; qid = ltac1_expr; ")" -> { inj_ltac1val loc qid }
+      | IDENT "ltac1"; ":"; "("; qid = ltac1_expr_in_env; ")" -> { inj_ltac1 loc qid }
+      | IDENT "ltac1val"; ":"; "("; qid = ltac1_expr_in_env; ")" -> { inj_ltac1val loc qid }
+    ] ]
+  ;
+  ltac1_expr_in_env:
+    [ [ test_ltac1_env; ids = LIST0 locident; "|-"; e = ltac1_expr -> { ids, e }
+      | e = ltac1_expr -> { [], e }
     ] ]
   ;
   let_clause:
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 2eb199633d..a05612c1b1 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1118,26 +1118,47 @@ let () =
   define_ml_object Tac2quote.wit_reference obj
 
 let () =
-  let intern self ist tac =
+  let intern self ist (ids, tac) =
+    let map { CAst.v = id } = id in
+    let ids = List.map map ids in
     (* Prevent inner calls to Ltac2 values *)
     let extra = Tac2intern.drop_ltac2_env ist.Genintern.extra in
-    let ist = { ist with Genintern.extra } in
+    let ltacvars = List.fold_right Id.Set.add ids ist.Genintern.ltacvars in
+    let ist = { ist with Genintern.extra; ltacvars } in
     let _, tac = Genintern.intern Ltac_plugin.Tacarg.wit_tactic ist tac in
-    GlbVal tac, gtypref t_unit
+    let fold ty _ = GTypArrow (gtypref t_ltac1, ty) in
+    let ty = List.fold_left fold (gtypref t_unit) ids in
+    GlbVal (ids, tac), ty
   in
-  let interp ist tac =
-    let ist = { env_ist = Id.Map.empty } in
-    let lfun = Tac2interp.set_env ist Id.Map.empty in
-    let ist = Ltac_plugin.Tacinterp.default_ist () in
-    let ist = { ist with Geninterp.lfun = lfun } in
-    let tac = (Ltac_plugin.Tacinterp.eval_tactic_ist ist tac : unit Proofview.tactic) in
-    let wrap (e, info) = set_bt info >>= fun info -> Proofview.tclZERO ~info e in
-    Proofview.tclOR tac wrap >>= fun () ->
-    return v_unit
+  let interp _ (ids, tac) =
+    let clos args =
+      let add lfun id v =
+        let v = Tac2ffi.to_ext val_ltac1 v in
+        Id.Map.add id v lfun
+      in
+      let lfun = List.fold_left2 add Id.Map.empty ids args in
+      let ist = { env_ist = Id.Map.empty } in
+      let lfun = Tac2interp.set_env ist lfun in
+      let ist = Ltac_plugin.Tacinterp.default_ist () in
+      let ist = { ist with Geninterp.lfun = lfun } in
+      let tac = (Ltac_plugin.Tacinterp.eval_tactic_ist ist tac : unit Proofview.tactic) in
+      let wrap (e, info) = set_bt info >>= fun info -> Proofview.tclZERO ~info e in
+      Proofview.tclOR tac wrap >>= fun () ->
+      return v_unit
+    in
+    let len = List.length ids in
+    if Int.equal len 0 then
+      clos []
+    else
+      return (Tac2ffi.of_closure (Tac2ffi.abstract len clos))
   in
-  let subst s tac = Genintern.substitute Ltac_plugin.Tacarg.wit_tactic s tac in
-  let print env tac =
-    str "ltac1:(" ++ Ltac_plugin.Pptactic.pr_glob_tactic env tac ++ str ")"
+  let subst s (ids, tac) = (ids, Genintern.substitute Ltac_plugin.Tacarg.wit_tactic s tac) in
+  let print env (ids, tac) =
+    let ids =
+      if List.is_empty ids then mt ()
+      else pr_sequence Id.print ids ++ spc () ++ str "|-" ++ spc ()
+    in
+    str "ltac1:(" ++ ids ++ Ltac_plugin.Pptactic.pr_glob_tactic env tac ++ str ")"
   in
   let obj = {
     ml_intern = intern;
@@ -1149,23 +1170,44 @@ let () =
 
 let () =
   let open Ltac_plugin in
-  let intern self ist tac =
+  let intern self ist (ids, tac) =
+    let map { CAst.v = id } = id in
+    let ids = List.map map ids in
     (* Prevent inner calls to Ltac2 values *)
     let extra = Tac2intern.drop_ltac2_env ist.Genintern.extra in
-    let ist = { ist with Genintern.extra } in
+    let ltacvars = List.fold_right Id.Set.add ids ist.Genintern.ltacvars in
+    let ist = { ist with Genintern.extra; ltacvars } in
     let _, tac = Genintern.intern Ltac_plugin.Tacarg.wit_tactic ist tac in
-    GlbVal tac, gtypref t_ltac1
+    let fold ty _ = GTypArrow (gtypref t_ltac1, ty) in
+    let ty = List.fold_left fold (gtypref t_ltac1) ids in
+    GlbVal (ids, tac), ty
   in
-  let interp ist tac =
-    let ist = { env_ist = Id.Map.empty } in
-    let lfun = Tac2interp.set_env ist Id.Map.empty in
-    let ist = Ltac_plugin.Tacinterp.default_ist () in
-    let ist = { ist with Geninterp.lfun = lfun } in
-    return (Value.of_ext val_ltac1 (Tacinterp.Value.of_closure ist tac))
+  let interp _ (ids, tac) =
+    let clos args =
+      let add lfun id v =
+        let v = Tac2ffi.to_ext val_ltac1 v in
+        Id.Map.add id v lfun
+      in
+      let lfun = List.fold_left2 add Id.Map.empty ids args in
+      let ist = { env_ist = Id.Map.empty } in
+      let lfun = Tac2interp.set_env ist lfun in
+      let ist = Ltac_plugin.Tacinterp.default_ist () in
+      let ist = { ist with Geninterp.lfun = lfun } in
+      return (Value.of_ext val_ltac1 (Tacinterp.Value.of_closure ist tac))
+    in
+    let len = List.length ids in
+    if Int.equal len 0 then
+      clos []
+    else
+      return (Tac2ffi.of_closure (Tac2ffi.abstract len clos))
   in
-  let subst s tac = Genintern.substitute Tacarg.wit_tactic s tac in
-  let print env tac =
-    str "ltac1val:(" ++ Ltac_plugin.Pptactic.pr_glob_tactic env tac ++ str ")"
+  let subst s (ids, tac) = (ids, Genintern.substitute Tacarg.wit_tactic s tac) in
+  let print env (ids, tac) =
+    let ids =
+      if List.is_empty ids then mt ()
+      else pr_sequence Id.print ids ++ str " |- "
+    in
+    str "ltac1val:(" ++ ids++ Ltac_plugin.Pptactic.pr_glob_tactic env tac ++ str ")"
   in
   let obj = {
     ml_intern = intern;
diff --git a/user-contrib/Ltac2/tac2quote.mli b/user-contrib/Ltac2/tac2quote.mli
index 0cef0e3a2b..da28e04df0 100644
--- a/user-contrib/Ltac2/tac2quote.mli
+++ b/user-contrib/Ltac2/tac2quote.mli
@@ -97,8 +97,8 @@ val wit_constr : (Constrexpr.constr_expr, Glob_term.glob_constr) Arg.tag
 
 val wit_open_constr : (Constrexpr.constr_expr, Glob_term.glob_constr) Arg.tag
 
-val wit_ltac1 : (Ltac_plugin.Tacexpr.raw_tactic_expr, Ltac_plugin.Tacexpr.glob_tactic_expr) Arg.tag
+val wit_ltac1 : (Id.t CAst.t list * Ltac_plugin.Tacexpr.raw_tactic_expr, Id.t list * Ltac_plugin.Tacexpr.glob_tactic_expr) Arg.tag
 (** Ltac1 AST quotation, seen as a 'tactic'. Its type is unit in Ltac2. *)
 
-val wit_ltac1val : (Ltac_plugin.Tacexpr.raw_tactic_expr, Ltac_plugin.Tacexpr.glob_tactic_expr) Arg.tag
+val wit_ltac1val : (Id.t CAst.t list * Ltac_plugin.Tacexpr.raw_tactic_expr, Id.t list * Ltac_plugin.Tacexpr.glob_tactic_expr) Arg.tag
 (** Ltac1 AST quotation, seen as a value-returning expression, with type Ltac1.t. *)