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

1 files changed, 28 insertions, 25 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: