Fix #10615: Notation substitution for Ltac2 terms.

We implement a new type of "preterms" that represent untyped ASTs, corresponding
to glob_expr in the ML implementations. Ltac2 quotations inside notations are
provided with such preterms, and have to pretype them in order to do anything
of relevance with them.

11 files changed, 152 insertions, 32 deletions

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. *)