diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-01-07 10:24:12 +0100 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-01-07 10:24:40 +0100 |
commit | 81492757797caef50d4eb3eb185f813463da883d (patch) | |
tree | c71a4c4c17e1b5b5585cf41e291b57731ba98473 /kernel | |
parent | 093529c6d4f8eba7370c30b97d8d648340039374 (diff) |
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
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/csymtable.ml | 53 | ||||
-rw-r--r-- | kernel/pre_env.ml | 2 | ||||
-rw-r--r-- | kernel/pre_env.mli | 2 |
3 files changed, 30 insertions, 27 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 |