Merge PR #10861: Fix #10615: Notation substitution for Ltac2 terms.

Reviewed-by: SkySkimmer
Ack-by: jfehrle

13 files changed, 199 insertions, 32 deletions

diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 18d2c79461..cfdc70d50e 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -563,6 +563,20 @@ for it.
 - `&x` as a Coq constr expression expands to
   `ltac2:(Control.refine (fun () => hyp @x))`.
 
+In the special case where Ltac2 antiquotations appear inside a Coq term
+notation, the notation variables are systematically bound in the body
+of the tactic expression with type `Ltac2.Init.preterm`. Such a type represents
+untyped syntactic Coq expressions, which can by typed in the
+current context using the `Ltac2.Constr.pretype` function.
+
+.. example::
+
+   The following notation is essentially the identity.
+
+   .. coqtop:: in
+
+      Notation "[ x ]" := ltac2:(let x := Ltac2.Constr.pretype x in exact $x) (only parsing).
+
 Dynamic semantics
 *****************
 
diff --git a/test-suite/ltac2/term_notations.v b/test-suite/ltac2/term_notations.v
new file mode 100644
index 0000000000..85eb858d4e
--- /dev/null
+++ b/test-suite/ltac2/term_notations.v
@@ -0,0 +1,33 @@
+Require Import Ltac2.Ltac2.
+
+(* Preterms are not terms *)
+Fail Notation "[ x ]" := $x.
+
+Section Foo.
+
+Notation "[ x ]" := ltac2:(Control.refine (fun _ => Constr.pretype x)).
+
+Goal [ True ].
+Proof.
+constructor.
+Qed.
+
+End Foo.
+
+Section Bar.
+
+(* Have fun with context capture *)
+Notation "[ x ]" := ltac2:(
+  let c () := Constr.pretype x in
+  refine constr:(forall n : nat, n = ltac2:(Notations.exact0 true c))
+).
+
+Goal forall n : nat, [ n ].
+Proof.
+reflexivity.
+Qed.
+
+(* This fails currently, which is arguably a bug *)
+Fail Goal [ n ].
+
+End Bar.
diff --git a/user-contrib/Ltac2/Constr.v b/user-contrib/Ltac2/Constr.v
index 1e330b06d7..942cbe8916 100644
--- a/user-contrib/Ltac2/Constr.v
+++ b/user-contrib/Ltac2/Constr.v
@@ -77,3 +77,6 @@ Ltac2 @ external in_context : ident -> constr -> (unit -> unit) -> constr := "lt
 (** On a focused goal [Γ ⊢ A], [in_context id c tac] evaluates [tac] in a
     focused goal [Γ, id : c ⊢ ?X] and returns [fun (id : c) => t] where [t] is
     the proof built by the tactic. *)
+
+Ltac2 @ external pretype : preterm -> constr := "ltac2" "constr_pretype".
+(** Pretype the provided preterm. Assumes the goal to be focussed. *)
diff --git a/user-contrib/Ltac2/Init.v b/user-contrib/Ltac2/Init.v
index 88454ff2fb..6eed261554 100644
--- a/user-contrib/Ltac2/Init.v
+++ b/user-contrib/Ltac2/Init.v
@@ -30,6 +30,7 @@ Ltac2 Type constructor.
 Ltac2 Type projection.
 Ltac2 Type pattern.
 Ltac2 Type constr.
+Ltac2 Type preterm.
 
 Ltac2 Type message.
 Ltac2 Type exn := [ .. ].
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index 8a878bb0d0..9d4a3706f4 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -838,11 +838,11 @@ END
 GRAMMAR EXTEND Gram
   Pcoq.Constr.operconstr: LEVEL "0"
     [ [ IDENT "ltac2"; ":"; "("; tac = tac2expr; ")" ->
-      { let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in
+      { let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_constr) tac in
         CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg)) }
       | test_ampersand_ident; "&"; id = Prim.ident ->
       { 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_constr) tac in
         CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg)) }
       | test_dollar_ident; "$"; id = Prim.ident ->
       { let id = Loc.tag ~loc id in
@@ -873,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_constr) tac in
       CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg))
     end
   );
@@ -882,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_constr) 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 34870345a5..0268e8f9ef 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -17,6 +17,28 @@ open Tac2expr
 open Tac2entries.Pltac
 open Proofview.Notations
 
+let constr_flags =
+  let open Pretyping in
+  {
+    use_typeclasses = true;
+    solve_unification_constraints = true;
+    fail_evar = true;
+    expand_evars = true;
+    program_mode = false;
+    polymorphic = false;
+  }
+
+let open_constr_no_classes_flags =
+  let open Pretyping in
+  {
+  use_typeclasses = false;
+  solve_unification_constraints = true;
+  fail_evar = false;
+  expand_evars = true;
+  program_mode = false;
+  polymorphic = false;
+  }
+
 (** Standard values *)
 
 module Value = Tac2ffi
@@ -587,6 +609,30 @@ let () = define3 "constr_in_context" ident constr closure begin fun id t c ->
     throw err_notfocussed
 end
 
+(** preterm -> constr *)
+let () = define1 "constr_pretype" (repr_ext val_preterm) begin fun c ->
+  let open Pretyping in
+  let open Ltac_pretype in
+  let pretype env sigma =
+  Proofview.V82.wrap_exceptions begin fun () ->
+    (* For now there are no primitives to create preterms with a non-empty
+       closure. I do not know whether [closed_glob_constr] is really the type
+       we want but it does not hurt in the meantime. *)
+    let { closure; term } = c in
+    let vars = {
+      ltac_constrs = closure.typed;
+      ltac_uconstrs = closure.untyped;
+      ltac_idents = closure.idents;
+      ltac_genargs = Id.Map.empty;
+    } in
+    let flags = constr_flags in
+    let sigma, t = understand_ltac flags env sigma vars WithoutTypeConstraint term in
+    let t = Value.of_constr t in
+    Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT t
+  end in
+  pf_apply pretype
+end
+
 (** Patterns *)
 
 let empty_context = EConstr.mkMeta Constr_matching.special_meta
@@ -976,28 +1022,6 @@ end
 
 (** ML types *)
 
-let constr_flags () =
-  let open Pretyping in
-  {
-    use_typeclasses = true;
-    solve_unification_constraints = true;
-    fail_evar = true;
-    expand_evars = true;
-    program_mode = false;
-    polymorphic = false;
-  }
-
-let open_constr_no_classes_flags () =
-  let open Pretyping in
-  {
-  use_typeclasses = false;
-  solve_unification_constraints = true;
-  fail_evar = false;
-  expand_evars = true;
-  program_mode = false;
-  polymorphic = false;
-  }
-
 (** Embed all Ltac2 data into Values *)
 let to_lvar ist =
   let open Glob_ops in
@@ -1033,7 +1057,7 @@ let interp_constr flags ist c =
 
 let () =
   let intern = intern_constr in
-  let interp ist c = interp_constr (constr_flags ()) ist c in
+  let interp ist c = interp_constr constr_flags ist c in
   let print env c = str "constr:(" ++ Printer.pr_lglob_constr_env env c ++ str ")" in
   let subst subst c = Detyping.subst_glob_constr (Global.env()) subst c in
   let obj = {
@@ -1046,7 +1070,7 @@ let () =
 
 let () =
   let intern = intern_constr in
-  let interp ist c = interp_constr (open_constr_no_classes_flags ()) ist c in
+  let interp ist c = interp_constr open_constr_no_classes_flags ist c in
   let print env c = str "open_constr:(" ++ Printer.pr_lglob_constr_env env c ++ str ")" in
   let subst subst c = Detyping.subst_glob_constr (Global.env()) subst c in
   let obj = {
@@ -1092,6 +1116,27 @@ let () =
   define_ml_object Tac2quote.wit_pattern obj
 
 let () =
+  let interp _ c =
+    let open Ltac_pretype in
+    let closure = {
+      idents = Id.Map.empty;
+      typed = Id.Map.empty;
+      untyped = Id.Map.empty;
+    } in
+    let c = { closure; term = c } in
+    return (Value.of_ext val_preterm c)
+  in
+  let subst subst c = Detyping.subst_glob_constr (Global.env()) subst c in
+  let print env c = str "preterm:(" ++ Printer.pr_lglob_constr_env env c ++ str ")" in
+  let obj = {
+    ml_intern = (fun _ _ e -> Empty.abort e);
+    ml_interp = interp;
+    ml_subst = subst;
+    ml_print = print;
+  } in
+  define_ml_object Tac2quote.wit_preterm obj
+
+let () =
   let intern self ist ref = match ref.CAst.v with
   | Tac2qexpr.QHypothesis id ->
     GlbVal (GlobRef.VarRef id), gtypref t_reference
@@ -1221,15 +1266,15 @@ let () =
 
 let () =
   let interp ist poly env sigma concl (ids, tac) =
-    (* Syntax prevents bound variables in constr quotations *)
-    let () = assert (List.is_empty ids) in
+    (* Syntax prevents bound notation variables in constr quotations *)
+    let () = assert (Id.Set.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
     let c, sigma = Pfedit.refine_by_tactic ~name ~poly env sigma concl tac in
     (EConstr.of_constr c, sigma)
   in
-  GlobEnv.register_constr_interp0 wit_ltac2 interp
+  GlobEnv.register_constr_interp0 wit_ltac2_constr interp
 
 let () =
   let interp ist poly env sigma concl id =
@@ -1247,6 +1292,29 @@ let () =
   let pr_top _ = Genprint.TopPrinterBasic mt in
   Genprint.register_print0 wit_ltac2_quotation pr_raw pr_glb pr_top
 
+let () =
+  let subs globs (ids, tac) =
+    (* Let-bind the notation terms inside the tactic *)
+    let fold id (c, _) (rem, accu) =
+      let c = GTacExt (Tac2quote.wit_preterm, c) in
+      let rem = Id.Set.remove id rem in
+      rem, (Name id, c) :: accu
+    in
+    let rem, bnd = Id.Map.fold fold globs (ids, []) in
+    let () = if not @@ Id.Set.is_empty rem then
+      (* FIXME: provide a reasonable middle-ground with the behaviour
+          introduced by 8d9b66b. We should be able to pass mere syntax to
+          term notation without facing the wrath of the internalization. *)
+      let plural = if Id.Set.cardinal rem <= 1 then " " else "s " in
+      CErrors.user_err (str "Missing notation term for variable" ++ str plural ++
+        pr_sequence Id.print (Id.Set.elements rem) ++
+          str ", probably an ill-typed expression")
+    in
+    let tac = if List.is_empty bnd then tac else GTacLet (false, bnd, tac) in
+    (Id.Set.empty, tac)
+  in
+  Genintern.register_ntn_subst0 wit_ltac2_constr subs
+
 (** Ltac2 in Ltac1 *)
 
 let () =
diff --git a/user-contrib/Ltac2/tac2env.ml b/user-contrib/Ltac2/tac2env.ml
index 963c3aa37f..959a912ad2 100644
--- a/user-contrib/Ltac2/tac2env.ml
+++ b/user-contrib/Ltac2/tac2env.ml
@@ -284,6 +284,7 @@ let ltac1_prefix =
 (** Generic arguments *)
 
 let wit_ltac2 = 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
 let () = Geninterp.register_val0 wit_ltac2_quotation None
diff --git a/user-contrib/Ltac2/tac2env.mli b/user-contrib/Ltac2/tac2env.mli
index 2f4a49a0f5..1dfc3400a1 100644
--- a/user-contrib/Ltac2/tac2env.mli
+++ b/user-contrib/Ltac2/tac2env.mli
@@ -141,7 +141,13 @@ val ltac1_prefix : ModPath.t
 (** {5 Generic arguments} *)
 
 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_constr : (raw_tacexpr, Id.Set.t * glb_tacexpr, Util.Empty.t) genarg_type
+(** Ltac2 quotations in Gallina terms *)
+
 val wit_ltac2_quotation : (Id.t Loc.located, Id.t, Util.Empty.t) genarg_type
+(** Ltac2 quotations for variables "$x" in Gallina terms *)
 
 (** {5 Helper functions} *)
 
diff --git a/user-contrib/Ltac2/tac2ffi.ml b/user-contrib/Ltac2/tac2ffi.ml
index 0e6fb94095..7c9613f31b 100644
--- a/user-contrib/Ltac2/tac2ffi.ml
+++ b/user-contrib/Ltac2/tac2ffi.ml
@@ -89,6 +89,7 @@ let val_exn = Val.create "exn"
 let val_constr = Val.create "constr"
 let val_ident = Val.create "ident"
 let val_pattern = Val.create "pattern"
+let val_preterm = Val.create "preterm"
 let val_pp = Val.create "pp"
 let val_sort = Val.create "sort"
 let val_cast = Val.create "cast"
diff --git a/user-contrib/Ltac2/tac2ffi.mli b/user-contrib/Ltac2/tac2ffi.mli
index 480eee51fc..d3c9596e8f 100644
--- a/user-contrib/Ltac2/tac2ffi.mli
+++ b/user-contrib/Ltac2/tac2ffi.mli
@@ -165,6 +165,7 @@ val valexpr : valexpr repr
 val val_constr : EConstr.t Val.tag
 val val_ident : Id.t Val.tag
 val val_pattern : Pattern.constr_pattern Val.tag
+val val_preterm : Ltac_pretype.closed_glob_constr Val.tag
 val val_pp : Pp.t Val.tag
 val val_sort : ESorts.t Val.tag
 val val_cast : Constr.cast_kind Val.tag
diff --git a/user-contrib/Ltac2/tac2intern.ml b/user-contrib/Ltac2/tac2intern.ml
index 5b3aa799a1..4e39b21c53 100644
--- a/user-contrib/Ltac2/tac2intern.ml
+++ b/user-contrib/Ltac2/tac2intern.ml
@@ -28,6 +28,7 @@ let t_int = coq_type "int"
 let t_string = coq_type "string"
 let t_constr = coq_type "constr"
 let t_ltac1 = ltac1_type "t"
+let t_preterm = coq_type "preterm"
 
 (** Union find *)
 
@@ -1511,7 +1512,7 @@ let () =
     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 *)
+      (* Only happens when Ltac2 is called from a toplevel ltac1 quotation *)
       let env = empty_env () in
       if !Ltac_plugin.Tacintern.strict_check then env
       else { env with env_str = false }
@@ -1527,7 +1528,36 @@ let () =
     (ist, (ids, tac))
   in
   Genintern.register_intern0 wit_ltac2 intern
+
+let () =
+  let open Genintern in
+  let intern ist tac =
+    let env = match Genintern.Store.get ist.extra ltac2_env with
+    | None ->
+      (* Only happens when Ltac2 is called from a constr quotation *)
+      let env = empty_env () in
+      if !Ltac_plugin.Tacintern.strict_check then env
+      else { env with env_str = false }
+    | Some env -> env
+    in
+    (* Special handling of notation variables *)
+    let fold id _ (ids, env) =
+      let () = assert (not @@ Id.Map.mem id env.env_var) in
+      let t = monomorphic (GTypRef (Other t_preterm, [])) in
+      let env = push_name (Name id) t env in
+      (Id.Set.add id ids, env)
+    in
+    let ntn_vars = ist.intern_sign.notation_variable_status in
+    let ids, env = Id.Map.fold fold ntn_vars (Id.Set.empty, env) in
+    let loc = tac.loc in
+    let (tac, t) = intern_rec env tac in
+    let () = check_elt_unit loc env t in
+    (ist, (ids, tac))
+  in
+  Genintern.register_intern0 wit_ltac2_constr intern
+
 let () = Genintern.register_subst0 wit_ltac2 (fun s (ids, e) -> ids, subst_expr s e)
+let () = Genintern.register_subst0 wit_ltac2_constr (fun s (ids, e) -> ids, subst_expr s e)
 
 let () =
   let open Genintern in
@@ -1540,6 +1570,12 @@ let () =
       else { env with env_str = false }
     | Some env -> env
     in
+    (* Special handling of notation variables *)
+    let () =
+      if Id.Map.mem id ist.intern_sign.notation_variable_status then
+        (* Always fail *)
+        unify ?loc env (GTypRef (Other t_preterm, [])) (GTypRef (Other t_constr, []))
+    in
     let t =
       try Id.Map.find id env.env_var
       with Not_found ->
diff --git a/user-contrib/Ltac2/tac2quote.ml b/user-contrib/Ltac2/tac2quote.ml
index 405c80fa9b..645b92c302 100644
--- a/user-contrib/Ltac2/tac2quote.ml
+++ b/user-contrib/Ltac2/tac2quote.ml
@@ -23,6 +23,7 @@ let wit_reference = Arg.create "reference"
 let wit_ident = Arg.create "ident"
 let wit_constr = Arg.create "constr"
 let wit_open_constr = Arg.create "open_constr"
+let wit_preterm = Arg.create "preterm"
 let wit_ltac1 = Arg.create "ltac1"
 let wit_ltac1val = Arg.create "ltac1val"
 
diff --git a/user-contrib/Ltac2/tac2quote.mli b/user-contrib/Ltac2/tac2quote.mli
index da28e04df0..f1564cd443 100644
--- a/user-contrib/Ltac2/tac2quote.mli
+++ b/user-contrib/Ltac2/tac2quote.mli
@@ -97,6 +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_preterm : (Util.Empty.t, Glob_term.glob_constr) 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. *)