diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-09 17:24:25 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-09 17:24:25 +0100 |
| commit | 6177c792aeb0e7ee523ac9777748125a991b4195 (patch) | |
| tree | 565f74c6c1e6f75ac528c55dc78fe6a9f6e7896e /pretyping/cbv.ml | |
| parent | 3b4bae6246b780961aa49b81a074e77189252bb3 (diff) | |
| parent | f3aa5579c36223c98968c82545500340d76b5378 (diff) | |
Merge PR #6769: Split closure cache and remove whd_both
Diffstat (limited to 'pretyping/cbv.ml')
| -rw-r--r-- | pretyping/cbv.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 7cfb30f4c..a2155697e 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -134,7 +134,7 @@ let mkSTACK = function | STACK(0,v0,stk0), stk -> STACK(0,v0,stack_concat stk0 stk) | v,stk -> STACK(0,v,stk) -type cbv_infos = { infos : cbv_value infos; sigma : Evd.evar_map } +type cbv_infos = { tab : cbv_value infos_tab; infos : cbv_value infos; sigma : Evd.evar_map } (* Change: zeta reduction cannot be avoided in CBV *) @@ -318,7 +318,7 @@ let rec norm_head info env t stack = and norm_head_ref k info env stack normt = if red_set_ref (info_flags info.infos) normt then - match ref_value_cache info.infos normt with + match ref_value_cache info.infos info.tab normt with | Some body -> if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ pr_key normt); strip_appl (shift_value k body) stack @@ -455,8 +455,8 @@ let cbv_norm infos constr = (* constant bodies are normalized at the first expansion *) let create_cbv_infos flgs env sigma = let infos = create - (fun old_info c -> cbv_stack_term { infos = old_info; sigma } TOP (subs_id 0) c) + (fun old_info tab c -> cbv_stack_term { tab; infos = old_info; sigma } TOP (subs_id 0) c) flgs env (Reductionops.safe_evar_value sigma) in - { infos; sigma } + { tab = CClosure.create_tab (); infos; sigma } |