Made Pre_env.lazy_val opaque.

3 files changed, 20 insertions, 19 deletions

diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 93473d704..c431d1075 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -117,32 +117,26 @@ and slot_for_fv env fv =
       | Some c ->
           val_of_constr (env_of_id id env) c,
           Environ.global_vars_set (Environ.env_of_pre_env env) c in
-    cache := VKvalue (Ephemeron.create (v,d)); v in
+    build_lazy_val cache (v, d); v in
   let val_of_rel i = val_of_rel (nb_rel env - i) in
   let idfun _ x = x in
   match fv with
   | FVnamed id ->
       let nv = Pre_env.lookup_named_val id env in
-      begin match !nv with
-      | VKnone ->
+      begin match force_lazy_val nv with
+      | None ->
           let _, b, _ = Context.lookup_named id env.env_named_context in
           fill_fv_cache nv id val_of_named idfun b
-      | VKvalue key ->
-          try fst (Ephemeron.get key)
-          with Ephemeron.InvalidKey ->
-            let _, b, _ = Context.lookup_named id env.env_named_context in
-            fill_fv_cache nv id val_of_named idfun b end
+      | Some (v, _) -> v
+      end
   | FVrel i ->
       let rv = Pre_env.lookup_rel_val i env in
-      begin match !rv with
-      | VKnone ->
+      begin match force_lazy_val rv with
+      | None ->
           let _, b, _ = lookup_rel i env.env_rel_context in
           fill_fv_cache rv i val_of_rel env_of_rel b
-      | VKvalue key ->
-          try fst (Ephemeron.get key)
-          with Ephemeron.InvalidKey ->
-            let _, b, _ = lookup_rel i env.env_rel_context in
-            fill_fv_cache rv i val_of_rel env_of_rel b end
+      | Some (v, _) -> v
+      end
 
 and eval_to_patch env (buff,pl,fv) =
   (* copy code *before* patching because of nested evaluations:
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 5040df5aa..b655887d7 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -55,6 +55,13 @@ type val_kind =
 
 type lazy_val = val_kind ref
 
+let force_lazy_val vk = match !vk with
+| VKnone -> None
+| VKvalue v -> try Some (Ephemeron.get v) with Ephemeron.InvalidKey -> None
+
+let dummy_lazy_val () = ref VKnone
+let build_lazy_val vk key = vk := VKvalue (Ephemeron.create key)
+
 type named_vals = (Id.t * lazy_val) list
 
 type env = {
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 35223db82..964d709cf 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -36,11 +36,11 @@ type stratification = {
   env_engagement : engagement option
 }
 
-type val_kind =
-    | VKvalue of (values * Id.Set.t) Ephemeron.key
-    | VKnone
+type lazy_val
 
-type lazy_val = val_kind ref
+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