Pass the constant cache as a separate argument in kernel reduction.

3 files changed, 12 insertions, 8 deletions

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index e42576d95..1718269b4 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -132,7 +132,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 *)
 
@@ -316,7 +316,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
@@ -453,8 +453,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 }
diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml
index a4097237f..33cbbc091 100644
--- a/pretyping/inferCumulativity.ml
+++ b/pretyping/inferCumulativity.ml
@@ -81,10 +81,12 @@ let infer_table_key infos variances c =
     infer_generic_instance_eq variances u
   | VarKey _ | RelKey _ -> variances
 
+let whd_stack (infos, tab) hd stk = CClosure.whd_stack infos tab hd stk
+
 let rec infer_fterm cv_pb infos variances hd stk =
   Control.check_for_interrupt ();
-  let open CClosure in
   let hd,stk = whd_stack infos hd stk in
+  let open CClosure in
   match fterm_of hd with
   | FAtom a ->
     begin match kind a with
@@ -114,7 +116,7 @@ let rec infer_fterm cv_pb infos variances hd stk =
       if Instance.is_empty u then variances
       else
         let nargs = stack_args_size stk in
-        infer_inductive_instance cv_pb (info_env infos) variances ind nargs u
+        infer_inductive_instance cv_pb (info_env (fst infos)) variances ind nargs u
     in
     infer_stack infos variances stk
   | FConstruct (ctor,u) ->
@@ -122,7 +124,7 @@ let rec infer_fterm cv_pb infos variances hd stk =
       if Instance.is_empty u then variances
       else
         let nargs = stack_args_size stk in
-        infer_constructor_instance_eq (info_env infos) variances ctor nargs u
+        infer_constructor_instance_eq (info_env (fst infos)) variances ctor nargs u
     in
     infer_stack infos variances stk
   | FFix ((_,(_,tys,cl)),e) | FCoFix ((_,(_,tys,cl)),e) ->
@@ -159,7 +161,7 @@ and infer_vect infos variances v =
 
 let infer_term cv_pb env variances c =
   let open CClosure in
-  let infos = create_clos_infos all env in
+  let infos = (create_clos_infos all env, create_tab ()) in
   infer_fterm cv_pb infos variances (CClosure.inject c) []
 
 let infer_arity_constructor is_arity env variances arcn =
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 418ea271c..1e53faccd 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1230,6 +1230,7 @@ let clos_norm_flags flgs env sigma t =
     let evars ev = safe_evar_value sigma ev in
     EConstr.of_constr (CClosure.norm_val
       (CClosure.create_clos_infos ~evars flgs env)
+      (CClosure.create_tab ())
       (CClosure.inject (EConstr.Unsafe.to_constr t)))
   with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term")
 
@@ -1238,6 +1239,7 @@ let clos_whd_flags flgs env sigma t =
     let evars ev = safe_evar_value sigma ev in
     EConstr.of_constr (CClosure.whd_val
       (CClosure.create_clos_infos ~evars flgs env)
+      (CClosure.create_tab ())
       (CClosure.inject (EConstr.Unsafe.to_constr t)))
   with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term")