Do not reallocate named_context_val of the pretyping environment.

Instead of costly linear reallocations, we share as much as possible of the
prefixes of the various environment subcomponents.

6 files changed, 24 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/kernel/environ.mli b/kernel/environ.mli
index 79e632daa0..f489b13a3b 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -176,6 +176,8 @@ val named_body : variable -> env -> constr option
 val fold_named_context :
   (env -> Constr.named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
 
+val match_named_context_val : named_context_val -> (named_declaration * lazy_val * named_context_val) option
+
 (** Recurrence on [named_context] starting from younger decl *)
 val fold_named_context_reverse :
   ('a -> Constr.named_declaration -> 'a) -> init:'a -> env -> 'a
diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml
index fad41614b4..e458d030cb 100644
--- a/pretyping/globEnv.ml
+++ b/pretyping/globEnv.ml
@@ -42,7 +42,7 @@ 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
   {
     static_env = env;
     renamed_env = env;
@@ -98,10 +98,9 @@ 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 (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 =