From 27c93465dcf0d5233c1195d1649f5e699ed54a90 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 21 Aug 2016 20:55:23 +0200
Subject: Packing the named_context_val in a proper record and marking it
 private.

---
 kernel/pre_env.mli | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

(limited to 'kernel/pre_env.mli')

diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index e551d22c81..928a8009ec 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -42,10 +42,14 @@ val build_lazy_val : lazy_val -> (values * Id.Set.t) -> unit
 
 type named_vals = (Id.t * lazy_val) list
 
+type named_context_val = private {
+  env_named_ctx : Context.Named.t;
+  env_named_val : named_vals;
+}
+
 type env = {
     env_globals       : globals;
-    env_named_context : Context.Named.t;
-    env_named_vals    : named_vals;
+    env_named_context : named_context_val;
     env_rel_context   : Context.Rel.t;
     env_rel_val       : lazy_val list;
     env_nb_rel        : int;
@@ -56,8 +60,6 @@ type env = {
     indirect_pterms : Opaqueproof.opaquetab;
 }
 
-type named_context_val = Context.Named.t * named_vals
-
 val empty_named_context_val : named_context_val
 
 val empty_env : env
@@ -73,6 +75,10 @@ val env_of_rel     : int -> env -> env
 
 val push_named_context_val  :
     Context.Named.Declaration.t -> named_context_val -> named_context_val
+val push_named_context_val_val  :
+    Context.Named.Declaration.t -> lazy_val -> named_context_val -> named_context_val
+val match_named_context_val  :
+  named_context_val -> (Context.Named.Declaration.t * lazy_val * named_context_val) option
 val push_named       : Context.Named.Declaration.t -> env -> env
 val lookup_named_val : Id.t -> env -> lazy_val
 val env_of_named     : Id.t -> env -> env
-- 
cgit v1.2.3


From e046e9b7e35cbe2d419099907cdcc0909b59d52c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 21 Aug 2016 21:43:16 +0200
Subject: Tentative fast-access named env

---
 kernel/pre_env.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/pre_env.mli')

diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 928a8009ec..f916c399f3 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -45,6 +45,7 @@ type named_vals = (Id.t * lazy_val) list
 type named_context_val = private {
   env_named_ctx : Context.Named.t;
   env_named_val : named_vals;
+  env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t;
 }
 
 type env = {
-- 
cgit v1.2.3


From 37195c027472b7f0110249b28356271e713fee6f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 22 Aug 2016 14:39:10 +0200
Subject: More efficient implementation of map_named_val.

---
 kernel/pre_env.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/pre_env.mli')

diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index f916c399f3..4390177da4 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -80,6 +80,9 @@ val push_named_context_val_val  :
     Context.Named.Declaration.t -> lazy_val -> named_context_val -> named_context_val
 val match_named_context_val  :
   named_context_val -> (Context.Named.Declaration.t * lazy_val * named_context_val) option
+val map_named_val :
+   (constr -> constr) -> named_context_val -> named_context_val
+
 val push_named       : Context.Named.Declaration.t -> env -> env
 val lookup_named_val : Id.t -> env -> lazy_val
 val env_of_named     : Id.t -> env -> env
-- 
cgit v1.2.3


From 1888527bb43d6a8c801565af3e6376c91769fbc1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 9 Sep 2016 11:51:51 +0200
Subject: Removing the now useless field env_named_val from named_context_val.

This field was only used by the VM before, but since the previous patches,
this part of the code relies on the map instead.
---
 kernel/pre_env.mli | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'kernel/pre_env.mli')

diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 4390177da4..1e4eff3d59 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -40,11 +40,8 @@ val force_lazy_val : lazy_val -> (values * Id.Set.t) option
 val dummy_lazy_val : unit -> lazy_val
 val build_lazy_val : lazy_val -> (values * Id.Set.t) -> unit
 
-type named_vals = (Id.t * lazy_val) list
-
 type named_context_val = private {
   env_named_ctx : Context.Named.t;
-  env_named_val : named_vals;
   env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t;
 }
 
-- 
cgit v1.2.3


From d55818c7da468ce1c7c9644cb63f68f7561a17bc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 9 Sep 2016 13:29:28 +0200
Subject: Tracking careless uses of slow name lookup.

---
 kernel/pre_env.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/pre_env.mli')

diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 1e4eff3d59..866790367d 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -81,6 +81,7 @@ val map_named_val :
    (constr -> constr) -> named_context_val -> named_context_val
 
 val push_named       : Context.Named.Declaration.t -> env -> env
+val lookup_named     : Id.t -> env -> Context.Named.Declaration.t
 val lookup_named_val : Id.t -> env -> lazy_val
 val env_of_named     : Id.t -> env -> env
 
-- 
cgit v1.2.3