Merge PR #13938: Fast Ltac2 quoted variable typing

Reviewed-by: gares

5 files changed, 52 insertions, 29 deletions

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index f2241e78d2..54d7c310aa 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2148,7 +2148,8 @@ let interp_redexp env sigma r =
 (* Backwarding recursive needs of tactic glob/interp/eval functions *)
 
 let _ =
-  let eval lfun poly env sigma ty tac =
+  let eval ?loc ~poly env sigma tycon tac =
+    let lfun = GlobEnv.lfun env in
     let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in
     let ist = { lfun; poly; extra; } in
     let tac = eval_tactic_ist ist tac in
@@ -2156,8 +2157,13 @@ let _ =
        poly seems like enough to get reasonable behavior in practice
      *)
     let name = Id.of_string "ltac_gen" in
-    let (c, sigma) = Proof.refine_by_tactic ~name ~poly env sigma ty tac in
-    (EConstr.of_constr c, sigma)
+    let sigma, ty = match tycon with
+    | Some ty -> sigma, ty
+    | None -> GlobEnv.new_type_evar env sigma ~src:(loc,Evar_kinds.InternalHole)
+    in
+    let (c, sigma) = Proof.refine_by_tactic ~name ~poly (GlobEnv.renamed_env env) sigma ty tac in
+    let j = { Environ.uj_val = EConstr.of_constr c; uj_type = ty } in
+    (j, sigma)
   in
   GlobEnv.register_constr_interp0 wit_tactic eval
 
diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml
index 34fae613bf..ad28b54900 100644
--- a/pretyping/globEnv.ml
+++ b/pretyping/globEnv.ml
@@ -51,6 +51,8 @@ let make ~hypnaming env sigma lvar =
   }
 
 let env env = env.static_env
+let renamed_env env = env.renamed_env
+let lfun env = env.lvar.ltac_genargs
 
 let vars_of_env env =
   Id.Set.union (Id.Map.domain env.lvar.ltac_genargs) (vars_of_env env.static_env)
@@ -183,10 +185,13 @@ let interp_ltac_variable ?loc typing_fun env sigma id : Evd.evar_map * unsafe_ju
 
 let interp_ltac_id env id = ltac_interp_id env.lvar id
 
+type 'a obj_interp_fun =
+  ?loc:Loc.t -> poly:bool -> t -> Evd.evar_map -> Evardefine.type_constraint ->
+  'a -> unsafe_judgment * Evd.evar_map
+
 module ConstrInterpObj =
 struct
-  type ('r, 'g, 't) obj =
-    unbound_ltac_var_map -> bool -> env -> Evd.evar_map -> types -> 'g -> constr * Evd.evar_map
+  type ('r, 'g, 't) obj = 'g obj_interp_fun
   let name = "constr_interp"
   let default _ = None
 end
@@ -195,8 +200,8 @@ module ConstrInterp = Genarg.Register(ConstrInterpObj)
 
 let register_constr_interp0 = ConstrInterp.register0
 
-let interp_glob_genarg env poly sigma ty arg =
+let interp_glob_genarg ?loc ~poly env sigma ty arg =
   let open Genarg in
   let GenArg (Glbwit tag, arg) = arg in
   let interp = ConstrInterp.obj tag in
-  interp env.lvar.ltac_genargs poly env.renamed_env sigma ty arg
+  interp ?loc ~poly env sigma ty arg
diff --git a/pretyping/globEnv.mli b/pretyping/globEnv.mli
index 023e24e6d8..40feb8206b 100644
--- a/pretyping/globEnv.mli
+++ b/pretyping/globEnv.mli
@@ -15,11 +15,18 @@ open EConstr
 open Ltac_pretype
 open Evarutil
 
+(** Type of environment extended with naming and ltac interpretation data *)
+
+type t
+
 (** To embed constr in glob_constr *)
 
+type 'a obj_interp_fun =
+  ?loc:Loc.t -> poly:bool -> t -> Evd.evar_map -> Evardefine.type_constraint ->
+  'a -> unsafe_judgment * Evd.evar_map
+
 val register_constr_interp0 :
-  ('r, 'g, 't) Genarg.genarg_type ->
-    (unbound_ltac_var_map -> bool -> env -> evar_map -> types -> 'g -> constr * evar_map) -> unit
+  ('r, 'g, 't) Genarg.genarg_type -> 'g obj_interp_fun -> unit
 
 (** {6 Pretyping name management} *)
 
@@ -32,10 +39,6 @@ val register_constr_interp0 :
       variables used to build purely-named evar contexts
 *)
 
-(** Type of environment extended with naming and ltac interpretation data *)
-
-type t
-
 (** Build a pretyping environment from an ltac environment *)
 
 val make : hypnaming:naming_mode -> env -> evar_map -> ltac_var_map -> t
@@ -43,6 +46,8 @@ val make : hypnaming:naming_mode -> env -> evar_map -> ltac_var_map -> t
 (** Export the underlying environment *)
 
 val env : t -> env
+val renamed_env : t -> env
+val lfun : t -> unbound_ltac_var_map
 
 val vars_of_env : t -> Id.Set.t
 
@@ -85,5 +90,5 @@ val interp_ltac_id : t -> Id.t -> Id.t
 (** Interpreting a generic argument, typically a "ltac:(...)", taking
     into account the possible renaming *)
 
-val interp_glob_genarg : t -> bool -> evar_map -> constr ->
-  Genarg.glob_generic_argument -> constr * evar_map
+val interp_glob_genarg : ?loc:Loc.t -> poly:bool -> t -> evar_map -> Evardefine.type_constraint ->
+  Genarg.glob_generic_argument -> unsafe_judgment * evar_map
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 3ccc6ea125..800096f2b3 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -653,12 +653,8 @@ struct
       sigma, { uj_val; uj_type }
 
     | Some arg ->
-      let sigma, ty =
-        match tycon with
-        | Some ty -> sigma, ty
-        | None -> new_type_evar env sigma ~src:(loc,Evar_kinds.InternalHole) in
-      let c, sigma = GlobEnv.interp_glob_genarg env poly sigma ty arg in
-      sigma, { uj_val = c; uj_type = ty }
+      let j, sigma = GlobEnv.interp_glob_genarg ?loc ~poly env sigma tycon arg in
+      sigma, j
 
   let pretype_rec self (fixkind, names, bl, lar, vdef) =
     fun ?loc ~program_mode ~poly resolve_tc tycon env sigma ->
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index d8fe03b7c0..bcf9ece7c8 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1436,24 +1436,35 @@ let () =
 (** Ltac2 in terms *)
 
 let () =
-  let interp ist poly env sigma concl (ids, tac) =
+  let interp ?loc ~poly env sigma tycon (ids, tac) =
     (* Syntax prevents bound notation variables in constr quotations *)
     let () = assert (Id.Set.is_empty ids) in
-    let ist = Tac2interp.get_env ist in
+    let ist = Tac2interp.get_env @@ GlobEnv.lfun env in
     let tac = Proofview.tclIGNORE (Tac2interp.interp ist tac) in
     let name, poly = Id.of_string "ltac2", poly in
-    let c, sigma = Proof.refine_by_tactic ~name ~poly env sigma concl tac in
-    (EConstr.of_constr c, sigma)
+    let sigma, concl = match tycon with
+    | Some ty -> sigma, ty
+    | None -> GlobEnv.new_type_evar env sigma ~src:(loc,Evar_kinds.InternalHole)
+    in
+    let c, sigma = Proof.refine_by_tactic ~name ~poly (GlobEnv.renamed_env env) sigma concl tac in
+    let j = { Environ.uj_val = EConstr.of_constr c; Environ.uj_type = concl } in
+    (j, sigma)
   in
   GlobEnv.register_constr_interp0 wit_ltac2_constr interp
 
 let () =
-  let interp ist poly env sigma concl id =
-    let ist = Tac2interp.get_env ist in
+  let interp ?loc ~poly env sigma tycon id =
+    let ist = Tac2interp.get_env @@ GlobEnv.lfun env in
     let c = Id.Map.find id ist.env_ist in
     let c = Value.to_constr c in
-    let sigma = Typing.check env sigma c concl in
-    (c, sigma)
+    let t = Retyping.get_type_of (GlobEnv.renamed_env env) sigma c in
+    match tycon with
+    | None ->
+      { Environ.uj_val = c; Environ.uj_type = t }, sigma
+    | Some ty ->
+      let sigma = Evarconv.unify_leq_delay (GlobEnv.renamed_env env) sigma t ty in
+      let j = { Environ.uj_val = c; Environ.uj_type = ty } in
+      j, sigma
   in
   GlobEnv.register_constr_interp0 wit_ltac2_quotation interp