STM: additional fix for STM + vm_compute

Thanks again Maximes.

This time the C value was stored in the env_(named|rel)_val of
the environment

4 files changed, 41 insertions, 34 deletions

diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index b606384ad..93473d704 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -110,36 +110,39 @@ let rec slot_for_getglobal env kn =
     pos
 
 and slot_for_fv env fv =
+  let fill_fv_cache cache id v_of_id env_of_id b =
+    let v,d =
+      match b with
+      | None -> v_of_id id, Id.Set.empty
+      | 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
+  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
-	| VKvalue (v,_) -> v
-	| VKnone ->
-	    let (_, b, _) = Context.lookup_named id env.env_named_context in
-	    let v,d =
-	      match b with
-		| None -> (val_of_named id, Id.Set.empty)
-		| Some c -> (val_of_constr env c, Environ.global_vars_set (Environ.env_of_pre_env env) c)
-	    in
-	      nv := VKvalue (v,d); v
-      end
+      begin match !nv with
+      | VKnone ->
+          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
   | FVrel i ->
       let rv = Pre_env.lookup_rel_val i env in
-      begin
-	match !rv with
-	| VKvalue (v, _) -> v
-	| VKnone ->
-	    let (_, b, _) = lookup_rel i env.env_rel_context in
-	    let (v, d) =
-	      match b with
-		| None -> (val_of_rel (nb_rel env - i), Id.Set.empty)
-		| Some c -> let renv =  env_of_rel i env in
-			      (val_of_constr renv c, Environ.global_vars_set (Environ.env_of_pre_env renv) c)
-	    in
-	      rv := VKvalue (v,d); v
-      end
+      begin match !rv with
+      | VKnone ->
+          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
 
 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 b548348e0..5040df5aa 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -50,7 +50,7 @@ type stratification = {
 }
 
 type val_kind =
-    | VKvalue of values * Id.Set.t
+    | VKvalue of (values * Id.Set.t) Ephemeron.key
     | VKnone
 
 type lazy_val = val_kind ref
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 3968ebcd5..35223db82 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -37,7 +37,7 @@ type stratification = {
 }
 
 type val_kind =
-    | VKvalue of values * Id.Set.t
+    | VKvalue of (values * Id.Set.t) Ephemeron.key
     | VKnone
 
 type lazy_val = val_kind ref
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 737846766..8e3057e8e 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -495,13 +495,17 @@ let clear_hyps_in_evi evdref hyps concl ids =
     let check_value vk =
       match !vk with
 	| VKnone -> vk
-	| VKvalue (v,d) ->
-	    if (Id.Set.for_all (fun e -> not (Id.Set.mem e d)) ids) then
-	      (* v does depend on any of ids, it's ok *)
-	      vk
-	    else
-	      (* v depends on one of the cleared hyps: we forget the computed value *)
-	      ref VKnone
+	| VKvalue key ->
+            try
+              let _, d = Ephemeron.get key in
+	      if (Id.Set.for_all (fun e -> not (Id.Set.mem e d)) ids) then
+	        (* v does depend on any of ids, it's ok *)
+	        vk
+	      else
+	        (* v depends on one of the cleared hyps:
+                   we forget the computed value *)
+	        ref VKnone
+            with Ephemeron.InvalidKey -> ref VKnone
     in
       remove_hyps ids check_context check_value hyps
   in