Give a functional type to Ltac1 quotations with a context.

This looks more principled, and doesn't require as much tinkering with
the typing implementation.

5 files changed, 56 insertions, 69 deletions

diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 3812fd7631..3036648b08 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -856,9 +856,11 @@ be done via an explicit annotation to the :n:`ltac1` quotation.
 .. productionlist:: coq
   ltac2_term : ltac1 : ( `ident` ... `ident` |- `ltac_expr` )
 
-The identifiers must be bound in the surrounding Ltac2 environment to values of
-type `Ltac2.Ltac1.t` (see below). This syntax will make them available to the
-quoted Ltac1 code as if they had been bound from Ltac1 itself.
+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
 +++++++++++++
diff --git a/test-suite/ltac2/compat.v b/test-suite/ltac2/compat.v
index a24c9af10d..9c11d19c27 100644
--- a/test-suite/ltac2/compat.v
+++ b/test-suite/ltac2/compat.v
@@ -30,17 +30,14 @@ Fail Ltac2 pose1 (v : constr) :=
 (** Variables explicitly crossing the boundary must satisfy typing properties *)
 Goal True.
 Proof.
-(* Missing variable *)
-Fail ltac1:(x |- idtac).
 (* Wrong type *)
-Fail let x := 0 in ltac1:(x |- idtac).
+Fail ltac1:(x |- idtac) 0.
 (* OK, and runtime has access to variable *)
-let x := Ltac1.of_constr constr:(Type) in ltac1:(x |- idtac x).
+ltac1:(x |- idtac x) (Ltac1.of_constr constr:(Type)).
 
 (* Same for ltac1val *)
-Fail Ltac1.run ltac1val:(x |- idtac).
-Fail let x := 0 in Ltac1.run ltac1val:(x |- idtac).
-let x := Ltac1.of_constr constr:(Type) in Ltac1.run ltac1val:(x |- idtac x).
+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 *)
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 781f8cd25c..a05612c1b1 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1119,35 +1119,38 @@ let () =
 
 let () =
   let intern self ist (ids, tac) =
-    (* Check that variables have the Ltac1 type *)
-    let t_ltac1 = gtypref t_ltac1 in
-    let check { CAst.loc; v = id } =
-      let () = Tac2intern.check_ltac2_var ist.Genintern.extra ?loc id t_ltac1 in
-      id
-    in
-    let ids = List.map check ids in
+    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 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 (ids, 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 (ids, tac) =
-    let add lfun id =
-      let v = Id.Map.find id ist.env_ist in
-      let v = Tac2ffi.to_ext val_ltac1 v in
-      Id.Map.add id v lfun
+  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 lfun = List.fold_left add Id.Map.empty ids 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
+    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 (ids, tac) = (ids, Genintern.substitute Ltac_plugin.Tacarg.wit_tactic s tac) in
   let print env (ids, tac) =
@@ -1168,32 +1171,35 @@ let () =
 let () =
   let open Ltac_plugin in
   let intern self ist (ids, tac) =
-    (* Check that variables have the Ltac1 type *)
-    let t_ltac1 = gtypref t_ltac1 in
-    let check { CAst.loc; v = id } =
-      let () = Tac2intern.check_ltac2_var ist.Genintern.extra ?loc id t_ltac1 in
-      id
-    in
-    let ids = List.map check ids in
+    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 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 (ids, tac), 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 (ids, tac) =
-    let add lfun id =
-      let v = Id.Map.find id ist.env_ist in
-      let v = Tac2ffi.to_ext val_ltac1 v in
-      Id.Map.add id v lfun
+  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 lfun = List.fold_left add Id.Map.empty ids 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))
+    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 (ids, tac) = (ids, Genintern.substitute Tacarg.wit_tactic s tac) in
   let print env (ids, tac) =
diff --git a/user-contrib/Ltac2/tac2intern.ml b/user-contrib/Ltac2/tac2intern.ml
index 9538943635..0961e9c9c9 100644
--- a/user-contrib/Ltac2/tac2intern.ml
+++ b/user-contrib/Ltac2/tac2intern.ml
@@ -1191,23 +1191,6 @@ let intern_open_type t =
   let t = normalize env (count, vars) t in
   (!count, t)
 
-let rec get_closed = function
-| GTypVar _ -> assert false
-| GTypArrow (t, u) -> GTypArrow (get_closed t, get_closed u)
-| GTypRef (t, args) -> GTypRef (t, List.map get_closed args)
-
-let check_ltac2_var ?loc store id t =
-  let env = match Genintern.Store.get store ltac2_env with
-  | None -> empty_env ()
-  | Some env -> env
-  in
-  match Id.Map.find id env.env_var with
-  | sch ->
-    let t' = fresh_mix_type_scheme env sch in
-    unify ?loc env t' (get_closed t)
-  | exception Not_found ->
-    CErrors.user_err ?loc (Id.print id ++ str " is not a bound variable")
-
 (** Subtyping *)
 
 let check_subtype t1 t2 =
diff --git a/user-contrib/Ltac2/tac2intern.mli b/user-contrib/Ltac2/tac2intern.mli
index 1caca3a411..5e282a386a 100644
--- a/user-contrib/Ltac2/tac2intern.mli
+++ b/user-contrib/Ltac2/tac2intern.mli
@@ -46,4 +46,3 @@ val error_nparams_mismatch : ?loc:Loc.t -> int -> int -> 'a
 (** Misc *)
 
 val drop_ltac2_env : Genintern.Store.t -> Genintern.Store.t
-val check_ltac2_var : ?loc:Loc.t -> Genintern.Store.t -> Id.t -> 'a glb_typexpr -> unit