Merge PR #12502: Preserve sharing in evar instances

Reviewed-by: SkySkimmer
Ack-by: gares

1 files changed, 16 insertions, 8 deletions

diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml
index fad41614b4..05abb86f46 100644
--- a/pretyping/globEnv.ml
+++ b/pretyping/globEnv.ml
@@ -33,6 +33,8 @@ type t = {
   (** For locating indices *)
   renamed_env : env;
   (** For name management *)
+  renamed_vars : EConstr.t list Lazy.t;
+  (** Identity instance of named_context of renamed_env, to maximize sharing *)
   extra : ext_named_context Lazy.t;
   (** Delay the computation of the evar extended environment *)
   lvar : ltac_var_map;
@@ -42,10 +44,12 @@ let make ~hypnaming env sigma lvar =
   let get_extra env sigma =
     let avoid = Environ.ids_of_named_context_val (Environ.named_context_val env) in
     Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context ~hypnaming sigma d acc)
-      (rel_context env) ~init:(empty_csubst, avoid, named_context env) in
+      (rel_context env) ~init:(empty_csubst, avoid, named_context_val env) in
+  let open Context.Named.Declaration in
   {
     static_env = env;
     renamed_env = env;
+    renamed_vars = lazy (List.map (get_id %> mkVar) (named_context env));
     extra = lazy (get_extra env sigma);
     lvar = lvar;
   }
@@ -67,10 +71,12 @@ let ltac_interp_id { ltac_idents ; ltac_genargs } id =
 let ltac_interp_name lvar = Nameops.Name.map (ltac_interp_id lvar)
 
 let push_rel ~hypnaming sigma d env =
-  let d' = Context.Rel.Declaration.map_name (ltac_interp_name env.lvar) d in
+  let open Context.Rel.Declaration in
+  let d' = map_name (ltac_interp_name env.lvar) d in
   let env = {
     static_env = push_rel d env.static_env;
     renamed_env = push_rel d' env.renamed_env;
+    renamed_vars = env.renamed_vars;
     extra = lazy (push_rel_decl_to_named_context ~hypnaming:hypnaming sigma d' (Lazy.force env.extra));
     lvar = env.lvar;
     } in
@@ -83,6 +89,7 @@ let push_rel_context ~hypnaming ?(force_names=false) sigma ctx env =
   let env = {
     static_env = push_rel_context ctx env.static_env;
     renamed_env = push_rel_context ctx' env.renamed_env;
+    renamed_vars = env.renamed_vars;
     extra = lazy (List.fold_right (fun d acc -> push_rel_decl_to_named_context ~hypnaming:hypnaming sigma d acc) ctx' (Lazy.force env.extra));
     lvar = env.lvar;
     } in
@@ -95,13 +102,14 @@ let push_rec_types ~hypnaming sigma (lna,typarray) env =
   Array.map get_annot ctx, env
 
 let new_evar env sigma ?src ?naming typ =
-  let open Context.Named.Declaration in
-  let inst_vars = List.map (get_id %> mkVar) (named_context env.renamed_env) in
-  let inst_rels = List.rev (rel_list 0 (nb_rel env.renamed_env)) in
-  let (subst, _, nc) = Lazy.force env.extra in
+  let lazy inst_vars = env.renamed_vars in
+  let rec rel_list n accu =
+    if n <= 0 then accu
+    else rel_list (n - 1) (mkRel n :: accu)
+  in
+  let instance = rel_list (nb_rel env.renamed_env) inst_vars in
+  let (subst, _, sign) = Lazy.force env.extra in
   let typ' = csubst_subst subst typ in
-  let instance = inst_rels @ inst_vars in
-  let sign = val_of_named_context nc in
   new_evar_instance sign sigma typ' ?src ?naming instance
 
 let new_type_evar env sigma ~src =