Merge PR #12502: Preserve sharing in evar instances

Reviewed-by: SkySkimmer
Ack-by: gares

5 files changed, 23 insertions, 15 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index ca681e58f8..42c9359ff0 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -733,6 +733,11 @@ let map_rel_context_in_env f env sign =
   in
   aux env [] (List.rev sign)
 
+let match_named_context_val :
+  named_context_val -> (named_declaration * lazy_val * named_context_val) option =
+  match unsafe_eq with
+  | Refl -> match_named_context_val
+
 let fresh_global ?loc ?rigid ?names env sigma reference =
   let (evd,t) = Evd.fresh_global ?loc ?rigid ?names env sigma reference in
   evd, t
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 9a73c3e3f5..aea441b90b 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -322,6 +322,9 @@ val lookup_named_val : variable -> named_context_val -> named_declaration
 val map_rel_context_in_env :
   (env -> constr -> constr) -> env -> rel_context -> rel_context
 
+val match_named_context_val :
+  named_context_val -> (named_declaration * lazy_val * named_context_val) option
+
 (* XXX Missing Sigma proxy *)
 val fresh_global :
   ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env ->
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 5fcadfcef7..eea7e38f87 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -287,7 +287,7 @@ let csubst_subst { csubst_len = k; csubst_var = v; csubst_rel = s } c =
   EConstr.of_constr c
 
 type ext_named_context =
-  csubst * Id.Set.t * EConstr.named_context
+  csubst * Id.Set.t * named_context_val
 
 let push_var id { csubst_len = n; csubst_var = v; csubst_rel = s; csubst_rev = r } =
   let s = Int.Map.add n (Constr.mkVar id) s in
@@ -325,22 +325,22 @@ type naming_mode =
 
 let push_rel_decl_to_named_context
   ?(hypnaming=KeepUserNameAndRenameExistingButSectionNames)
-  sigma decl (subst, avoid, nc) =
+  sigma decl ((subst, avoid, nc) : ext_named_context) =
   let open EConstr in
   let open Vars in
   let map_decl f d =
     NamedDecl.map_constr f d
   in
-  let rec replace_var_named_declaration id0 id = function
-  | [] -> []
-  | decl :: nc ->
+  let rec replace_var_named_declaration id0 id nc = match match_named_context_val nc with
+  | None -> empty_named_context_val
+  | Some (decl, _, nc) ->
     if Id.equal id0 (NamedDecl.get_id decl) then
       (* Stop here, the variable cannot occur before its definition *)
-      (NamedDecl.set_id id decl) :: nc
+      push_named_context_val (NamedDecl.set_id id decl) nc
     else
       let nc = replace_var_named_declaration id0 id nc in
       let vsubst = [id0 , mkVar id] in
-      map_decl (fun c -> replace_vars vsubst c) decl :: nc
+      push_named_context_val (map_decl (fun c -> replace_vars vsubst c) decl) nc
   in
   let extract_if_neq id = function
     | Anonymous -> None
@@ -372,7 +372,7 @@ let push_rel_decl_to_named_context
       let subst = update_var id0 id subst in
       let d = decl |> NamedDecl.of_rel_decl (fun _ -> id0) |> map_decl (csubst_subst subst) in
       let nc = replace_var_named_declaration id0 id nc in
-      (push_var id0 subst, Id.Set.add id avoid, d :: nc)
+      (push_var id0 subst, Id.Set.add id avoid, push_named_context_val d nc)
   | Some id0 when hypnaming = FailIfConflict ->
        user_err Pp.(Id.print id0 ++ str " is already used.")
   | _ ->
@@ -381,7 +381,7 @@ let push_rel_decl_to_named_context
           the new binder has name [id]. Which amounts to the same
           behaviour than when [id=id0]. *)
       let d = decl |> NamedDecl.of_rel_decl (fun _ -> id) |> map_decl (csubst_subst subst) in
-      (push_var id subst, Id.Set.add id avoid, d :: nc)
+      (push_var id subst, Id.Set.add id avoid, push_named_context_val d nc)
 
 let push_rel_context_to_named_context ?hypnaming env sigma typ =
   (* compute the instances relative to the named context and rel_context *)
@@ -399,8 +399,8 @@ let push_rel_context_to_named_context ?hypnaming env sigma typ =
     (* We do keep the instances corresponding to local definition (see above) *)
     let (subst, _, env) =
       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
-    (val_of_named_context env, csubst_subst subst typ, inst_rels@inst_vars, subst)
+        (rel_context env) ~init:(empty_csubst, avoid, named_context_val env) in
+    (env, csubst_subst subst typ, inst_rels@inst_vars, subst)
 
 (*------------------------------------*
  * Entry points to define new evars   *
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index b5c7ccb283..b3c94e6b3b 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -268,7 +268,7 @@ val empty_csubst : csubst
 val csubst_subst : csubst -> constr -> constr
 
 type ext_named_context =
-  csubst * Id.Set.t * named_context
+  csubst * Id.Set.t * named_context_val
 
 val push_rel_decl_to_named_context : ?hypnaming:naming_mode ->
   evar_map -> rel_declaration -> ext_named_context -> ext_named_context
diff --git a/engine/univSubst.ml b/engine/univSubst.ml
index a691239ee2..92211d5f3d 100644
--- a/engine/univSubst.ml
+++ b/engine/univSubst.ml
@@ -131,9 +131,9 @@ let nf_evars_and_universes_opt_subst f subst =
   let rec aux c =
     match kind c with
     | Evar (evk, args) ->
-      let args = List.map aux args in
-      (match try f (evk, args) with Not_found -> None with
-      | None -> mkEvar (evk, args)
+      let args' = List.Smart.map aux args in
+      (match try f (evk, args') with Not_found -> None with
+      | None -> if args == args' then c else mkEvar (evk, args')
       | Some c -> aux c)
     | Const pu ->
       let pu' = subst_univs_fn_puniverses lsubst pu in