Adding the ability to transfer Ltac2 variables to Ltac1 quotations.

6 files changed, 105 insertions, 20 deletions

diff --git a/test-suite/ltac2/compat.v b/test-suite/ltac2/compat.v
index 489fa638e4..a24c9af10d 100644
--- a/test-suite/ltac2/compat.v
+++ b/test-suite/ltac2/compat.v
@@ -27,6 +27,22 @@ 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.
+(* Missing variable *)
+Fail ltac1:(x |- idtac).
+(* Wrong type *)
+Fail let x := 0 in ltac1:(x |- idtac).
+(* OK, and runtime has access to variable *)
+let x := Ltac1.of_constr constr:(Type) in ltac1:(x |- idtac x).
+
+(* 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).
+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..781f8cd25c 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1118,16 +1118,30 @@ let () =
   define_ml_object Tac2quote.wit_reference obj
 
 let () =
-  let intern self ist tac =
+  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
     (* 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
+    GlbVal (ids, tac), gtypref t_unit
   in
-  let interp ist tac =
+  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
+    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 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
@@ -1135,9 +1149,13 @@ let () =
     Proofview.tclOR tac wrap >>= fun () ->
     return v_unit
   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 +1167,41 @@ let () =
 
 let () =
   let open Ltac_plugin in
-  let intern self ist tac =
+  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
     (* 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
+    GlbVal (ids, tac), t_ltac1
   in
-  let interp ist tac =
+  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
+    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 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 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/tac2intern.ml b/user-contrib/Ltac2/tac2intern.ml
index 0961e9c9c9..9538943635 100644
--- a/user-contrib/Ltac2/tac2intern.ml
+++ b/user-contrib/Ltac2/tac2intern.ml
@@ -1191,6 +1191,23 @@ 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 5e282a386a..1caca3a411 100644
--- a/user-contrib/Ltac2/tac2intern.mli
+++ b/user-contrib/Ltac2/tac2intern.mli
@@ -46,3 +46,4 @@ 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
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. *)