Merge PR #8707: Separate cache representation between CClosure and CBV

6 files changed, 152 insertions, 183 deletions

diff --git a/checker/closure.ml b/checker/closure.ml
index 5706011607..138499b0e6 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -121,9 +121,6 @@ let betaiotazeta = mkflags [fBETA;fIOTA;fZETA]
  * abstractions, storing a representation (of type 'a) of the body of
  * this constant or abstraction.
  *  * i_tab is the cache table of the results
- *  * i_repr is the function to get the representation from the current
- *         state of the cache and the body of the constant. The result
- *         is stored in the table.
  *  * i_rels = (4,[(1,c);(3,d)]) means there are 4 free rel variables
  *    and only those with index 1 and 3 have bodies which are c and d resp.
  *
@@ -156,33 +153,6 @@ end
 
 module KeyTable = Hashtbl.Make(KeyHash)
 
-type 'a infos = {
-  i_flags : reds;
-  i_repr : 'a infos -> constr -> 'a;
-  i_env : env;
-  i_rels : int * (int * constr) list;
-  i_tab : 'a KeyTable.t }
-
-let ref_value_cache info ref =
-  try
-    Some (KeyTable.find info.i_tab ref)
-  with Not_found ->
-  try
-    let body =
-      match ref with
-	| RelKey n ->
-	    let (s,l) = info.i_rels in lift n (Int.List.assoc (s-n) l)
-	| VarKey id -> raise Not_found
-	| ConstKey cst -> constant_value info.i_env cst
-    in
-    let v = info.i_repr info body in
-    KeyTable.add info.i_tab ref v;
-    Some v
-  with
-    | Not_found (* List.assoc *)
-    | NotEvaluableConst _ (* Const *)
-      -> None
-
 let defined_rels flags env =
 (*  if red_local_const (snd flags) then*)
   fold_rel_context
@@ -193,16 +163,6 @@ let defined_rels flags env =
       (rel_context env) ~init:(0,[])
 (*  else (0,[])*)
 
-let mind_equiv_infos info = mind_equiv info.i_env
-
-let create mk_cl flgs env =
-  { i_flags = flgs;
-    i_repr = mk_cl;
-    i_env = env;
-    i_rels = defined_rels flgs env;
-    i_tab = KeyTable.create 17 }
-
-
 (**********************************************************************)
 (* Lazy reduction: the one used in kernel operations                  *)
 
@@ -255,6 +215,12 @@ and fterm =
   | FCLOS of constr * fconstr subs
   | FLOCKED
 
+type clos_infos = {
+  i_flags : reds;
+  i_env : env;
+  i_rels : int * (int * constr) list;
+  i_tab : fconstr KeyTable.t }
+
 let fterm_of v = v.term
 let set_norm v = v.norm <- Norm
 
@@ -372,6 +338,30 @@ let mk_clos e t =
 
 let mk_clos_vect env v = Array.map (mk_clos env) v
 
+let inject = mk_clos (subs_id 0)
+
+let ref_value_cache info ref =
+  try
+    Some (KeyTable.find info.i_tab ref)
+  with Not_found ->
+  try
+    let body =
+      match ref with
+        | RelKey n ->
+            let (s,l) = info.i_rels in lift n (Int.List.assoc (s-n) l)
+        | VarKey id -> raise Not_found
+        | ConstKey cst -> constant_value info.i_env cst
+    in
+    let v = inject body in
+    KeyTable.add info.i_tab ref v;
+    Some v
+  with
+    | Not_found (* List.assoc *)
+    | NotEvaluableConst _ (* Const *)
+      -> None
+
+let mind_equiv_infos info = mind_equiv info.i_env
+
 (* Translate the head constructor of t from constr to fconstr. This
    function is parameterized by the function to apply on the direct
    subterms.
@@ -783,21 +773,19 @@ let kh info v stk = fapp_stack(kni info v stk)
 let whd_val info v =
   with_stats (lazy (term_of_fconstr (kh info v [])))
 
-let inject = mk_clos (subs_id 0)
-
 let whd_stack infos m stk =
   let k = kni infos m stk in
   let _ = fapp_stack k in (* to unlock Zupdates! *)
   k
 
-(* cache of constants: the body is computed only when needed. *)
-type clos_infos = fconstr infos
-
 let infos_env x = x.i_env
 let infos_flags x = x.i_flags
 let oracle_of_infos x = x.i_env.env_conv_oracle
 
 let create_clos_infos flgs env =
-  create (fun _ -> inject) flgs env
+  { i_flags = flgs;
+    i_env = env;
+    i_rels = defined_rels flgs env;
+    i_tab = KeyTable.create 17 }
 
 let unfold_reference = ref_value_cache
diff --git a/checker/closure.mli b/checker/closure.mli
index cec785699d..4c6643754b 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -61,10 +61,6 @@ val betadeltaiotanolet : reds
 
 type table_key = Constant.t puniverses tableKey
 
-type 'a infos
-val ref_value_cache: 'a infos -> table_key -> 'a option
-val create: ('a infos -> constr -> 'a) -> reds -> env -> 'a infos
-
 (************************************************************************)
 (*s Lazy reduction. *)
 
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 819a66c190..c558689595 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -224,11 +224,6 @@ let unfold_red kn =
  * abstractions, storing a representation (of type 'a) of the body of
  * this constant or abstraction.
  *  * i_tab is the cache table of the results
- *  * i_repr is the function to get the representation from the current
- *         state of the cache and the body of the constant. The result
- *         is stored in the table.
- *  * i_rels is the array of free rel variables together with their optional
- *    body
  *
  * ref_value_cache searchs in the tab, otherwise uses i_repr to
  * compute the result and store it in the table. If the constant can't
@@ -256,74 +251,12 @@ end
 
 module KeyTable = Hashtbl.Make(IdKeyHash)
 
-let eq_table_key = IdKeyHash.equal
-
-type 'a infos_tab = 'a KeyTable.t
-
-type 'a infos_cache = {
-  i_repr : 'a infos -> 'a infos_tab -> constr -> 'a;
-  i_env : env;
-  i_sigma : existential -> constr option;
-  i_rels : (Constr.rel_declaration * lazy_val) Range.t;
-  i_share : bool;
-}
-
-and 'a infos = {
-  i_flags : reds;
-  i_cache : 'a infos_cache }
-
-let info_flags info = info.i_flags
-let info_env info = info.i_cache.i_env
-
 open Context.Named.Declaration
 
 let assoc_defined id env = match Environ.lookup_named id env with
 | LocalDef (_, c, _) -> c
 | _ -> raise Not_found
 
-let ref_value_cache ({i_cache = cache;_} as infos) tab ref =
-  try
-    Some (KeyTable.find tab ref)
-  with Not_found ->
-  try
-    let body =
-      match ref with
-	| RelKey n ->
-          let open! Context.Rel.Declaration in
-          let i = n - 1 in
-          let (d, _) =
-            try Range.get cache.i_rels i
-            with Invalid_argument _ -> raise Not_found
-          in
-          begin match d with
-          | LocalAssum _ -> raise Not_found
-          | LocalDef (_, t, _) -> lift n t
-          end
-	| VarKey id -> assoc_defined id cache.i_env
-	| ConstKey cst -> constant_value_in cache.i_env cst
-    in
-    let v = cache.i_repr infos tab body in
-    KeyTable.add tab ref v;
-    Some v
-  with
-    | Not_found (* List.assoc *)
-    | NotEvaluableConst _ (* Const *)
-      -> None
-
-let evar_value cache ev =
-  cache.i_sigma ev
-
-let create ~repr ~share flgs env evars =
-  let cache =
-    { i_repr = repr;
-      i_env = env;
-      i_sigma = evars;
-      i_rels = env.env_rel_context.env_rel_map;
-      i_share = share;
-    }
-  in { i_flags = flgs; i_cache = cache }
-
-
 (**********************************************************************)
 (* Lazy reduction: the one used in kernel operations                  *)
 
@@ -391,6 +324,23 @@ let update ~share v1 no t =
      v1)
   else {norm=no;term=t}
 
+(** Reduction cache *)
+
+type infos_cache = {
+  i_env : env;
+  i_sigma : existential -> constr option;
+  i_share : bool;
+}
+
+type clos_infos = {
+  i_flags : reds;
+  i_cache : infos_cache }
+
+type clos_tab = fconstr KeyTable.t
+
+let info_flags info = info.i_flags
+let info_env info = info.i_cache.i_env
+
 (**********************************************************************)
 (* The type of (machine) stacks (= lambda-bar-calculus' contexts)     *)
 
@@ -539,6 +489,8 @@ let mk_clos e t =
     | (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _|Proj _) ->
         {norm = Red; term = FCLOS(t,e)}
 
+let inject c = mk_clos (subs_id 0) c
+
 (** Hand-unrolling of the map function to bypass the call to the generic array
     allocation *)
 let mk_clos_vect env v = match v with
@@ -550,6 +502,35 @@ let mk_clos_vect env v = match v with
   [|mk_clos env v0; mk_clos env v1; mk_clos env v2; mk_clos env v3|]
 | v -> Array.Fun1.map mk_clos env v
 
+let ref_value_cache ({ i_cache = cache; _ }) tab ref =
+  try
+    Some (KeyTable.find tab ref)
+  with Not_found ->
+  try
+    let body =
+      match ref with
+        | RelKey n ->
+          let open! Context.Rel.Declaration in
+          let i = n - 1 in
+          let (d, _) =
+            try Range.get cache.i_env.env_rel_context.env_rel_map i
+            with Invalid_argument _ -> raise Not_found
+          in
+          begin match d with
+          | LocalAssum _ -> raise Not_found
+          | LocalDef (_, t, _) -> lift n t
+          end
+        | VarKey id -> assoc_defined id cache.i_env
+        | ConstKey cst -> constant_value_in cache.i_env cst
+    in
+    let v = inject body in
+    KeyTable.add tab ref v;
+    Some v
+  with
+    | Not_found (* List.assoc *)
+    | NotEvaluableConst _ (* Const *)
+      -> None
+
 (* The inverse of mk_clos: move back to constr *)
 let rec to_constr lfts v =
   match v.term with
@@ -944,7 +925,7 @@ let rec knr info tab m stk =
   | FLetIn (_,v,_,bd,e) when red_set info.i_flags fZETA ->
       knit info tab (subs_cons([|v|],e)) bd stk
   | FEvar(ev,env) ->
-      (match evar_value info.i_cache ev with
+      (match info.i_cache.i_sigma ev with
           Some c -> knit info tab env c stk
         | None -> (m,stk))
   | FLOCKED | FRel _ | FAtom _ | FFlex _ | FInd _ | FApp _ | FProj _
@@ -1040,8 +1021,6 @@ let whd_val info tab v =
 let norm_val info tab v =
   with_stats (lazy (kl info tab v))
 
-let inject c = mk_clos (subs_id 0) c
-
 let whd_stack infos tab m stk = match m.norm with
 | Whnf | Norm ->
   (** No need to perform [kni] nor to unlock updates because
@@ -1052,19 +1031,19 @@ let whd_stack infos tab m stk = match m.norm with
   let () = if infos.i_cache.i_share then ignore (fapp_stack k) in (* to unlock Zupdates! *)
   k
 
-(* cache of constants: the body is computed only when needed. *)
-type clos_infos = fconstr infos
-
 let create_clos_infos ?(evars=fun _ -> None) flgs env =
   let share = (Environ.typing_flags env).Declarations.share_reduction in
-  create ~share ~repr:(fun _ _ c -> inject c) flgs env evars
+  let cache = {
+    i_env = env;
+    i_sigma = evars;
+    i_share = share;
+  } in
+  { i_flags = flgs; i_cache = cache }
 
 let create_tab () = KeyTable.create 17
 
 let oracle_of_infos infos = Environ.oracle infos.i_cache.i_env
 
-let env_of_infos infos = infos.i_cache.i_env
-
 let infos_with_reds infos reds =
   { infos with i_flags = reds }
 
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 2a018d172a..1ee4bccc25 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -98,25 +98,7 @@ val unfold_red : evaluable_global_reference -> reds
 (***********************************************************************)
 type table_key = Constant.t Univ.puniverses tableKey
 
-type 'a infos_cache
-type 'a infos_tab
-type 'a infos = {
-  i_flags : reds;
-  i_cache : 'a infos_cache }
-
-val ref_value_cache: 'a infos -> 'a infos_tab -> table_key -> 'a option
-val create:
-  repr:('a infos -> 'a infos_tab -> constr -> 'a) ->
-  share:bool ->
-  reds ->
-  env ->
-  (existential -> constr option) ->
-  'a infos
-val create_tab : unit -> 'a infos_tab
-val evar_value : 'a infos_cache -> existential -> constr option
-
-val info_env : 'a infos -> env
-val info_flags: 'a infos -> reds
+module KeyTable : Hashtbl.S with type key = table_key
 
 (***********************************************************************
   s Lazy reduction. *)
@@ -173,7 +155,6 @@ val stack_tail : int -> stack -> stack
 val stack_nth : stack -> int -> fconstr
 val zip_term : (fconstr -> constr) -> constr -> stack -> constr
 val eta_expand_stack : stack -> stack
-val unfold_projection : 'a infos -> Projection.t -> stack_member option
 
 (** To lazy reduce a constr, create a [clos_infos] with
    [create_clos_infos], inject the term to reduce with [inject]; then use
@@ -193,27 +174,32 @@ val destFLambda :
   (fconstr subs -> constr -> fconstr) -> fconstr -> Name.t * fconstr * fconstr
 
 (** Global and local constant cache *)
-type clos_infos = fconstr infos
+type clos_infos
+type clos_tab
 val create_clos_infos :
   ?evars:(existential->constr option) -> reds -> env -> clos_infos
 val oracle_of_infos : clos_infos -> Conv_oracle.oracle
 
-val env_of_infos : 'a infos -> env
+val create_tab : unit -> clos_tab
+
+val info_env : clos_infos -> env
+val info_flags: clos_infos -> reds
+val unfold_projection : clos_infos -> Projection.t -> stack_member option
 
 val infos_with_reds : clos_infos -> reds -> clos_infos
 
 (** Reduction function *)
 
 (** [norm_val] is for strong normalization *)
-val norm_val : clos_infos -> fconstr infos_tab -> fconstr -> constr
+val norm_val : clos_infos -> clos_tab -> fconstr -> constr
 
 (** [whd_val] is for weak head normalization *)
-val whd_val : clos_infos -> fconstr infos_tab -> fconstr -> constr
+val whd_val : clos_infos -> clos_tab -> fconstr -> constr
 
 (** [whd_stack] performs weak head normalization in a given stack. It
    stops whenever a reduction is blocked. *)
 val whd_stack :
-  clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack
+  clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack
 
 (** [eta_expand_ind_stack env ind c s t] computes stacks correspoding
     to the conversion of the eta expansion of t, considered as an inhabitant
@@ -230,9 +216,7 @@ val eta_expand_ind_stack : env -> inductive -> fconstr -> stack ->
 (** Conversion auxiliary functions to do step by step normalisation *)
 
 (** [unfold_reference] unfolds references in a [fconstr] *)
-val unfold_reference : clos_infos -> fconstr infos_tab -> table_key -> fconstr option
-
-val eq_table_key : table_key -> table_key -> bool
+val unfold_reference : clos_infos -> clos_tab -> table_key -> fconstr option
 
 (***********************************************************************
   i This is for lazy debug *)
@@ -243,9 +227,9 @@ val lift_fconstr_vect : int -> fconstr array -> fconstr array
 val mk_clos      : fconstr subs -> constr -> fconstr
 val mk_clos_vect : fconstr subs -> constr array -> fconstr array
 
-val kni: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack
-val knr: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack
-val kl : clos_infos -> fconstr infos_tab -> fconstr -> constr
+val kni: clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack
+val knr: clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack
+val kl : clos_infos -> clos_tab -> fconstr -> constr
 
 val to_constr : lift -> fconstr -> constr
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 00576476ab..18697d07e5 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -316,8 +316,8 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv =
 
 type conv_tab = {
   cnv_inf : clos_infos;
-  lft_tab : fconstr infos_tab;
-  rgt_tab : fconstr infos_tab;
+  lft_tab : clos_tab;
+  rgt_tab : clos_tab;
 }
 (** Invariant: for any tl ∈ lft_tab and tr ∈ rgt_tab, there is no mutable memory
     location contained both in tl and in tr. *)
@@ -346,7 +346,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	   | (Sort s1, Sort s2) ->
 	       if not (is_empty_stack v1 && is_empty_stack v2) then
 		 anomaly (Pp.str "conversion was given ill-typed terms (Sort).");
-              sort_cmp_universes (env_of_infos infos.cnv_inf) cv_pb s1 s2 cuniv
+              sort_cmp_universes (info_env infos.cnv_inf) cv_pb s1 s2 cuniv
 	   | (Meta n, Meta m) ->
                if Int.equal n m
                then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 265909980b..5061aeff88 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -134,7 +134,12 @@ let mkSTACK = function
   | STACK(0,v0,stk0), stk -> STACK(0,v0,stack_concat stk0 stk)
   | v,stk -> STACK(0,v,stk)
 
-type cbv_infos = { tab : cbv_value infos_tab; infos : cbv_value infos; sigma : Evd.evar_map }
+type cbv_infos = {
+  env : Environ.env;
+  tab : cbv_value KeyTable.t;
+  reds : RedFlags.reds;
+  sigma : Evd.evar_map
+}
 
 (* Change: zeta reduction cannot be avoided in CBV *)
 
@@ -260,8 +265,8 @@ let rec norm_head info env t stack =
   
   | Proj (p, c) -> 
     let p' =
-      if red_set (info_flags info.infos) (fCONST (Projection.constant p)) 
-      	&& red_set (info_flags info.infos) fBETA 
+      if red_set info.reds (fCONST (Projection.constant p))
+        && red_set info.reds fBETA
       then Projection.unfold p
       else p
     in 
@@ -280,16 +285,16 @@ let rec norm_head info env t stack =
   | Var id -> norm_head_ref 0 info env stack (VarKey id)
 
   | Const sp ->
-    Reductionops.reduction_effect_hook (env_of_infos info.infos) info.sigma
+    Reductionops.reduction_effect_hook info.env info.sigma
       (fst sp) (lazy (reify_stack t stack));
     norm_head_ref 0 info env stack (ConstKey sp)
 
   | LetIn (_, b, _, c) ->
       (* zeta means letin are contracted; delta without zeta means we *)
       (* allow bindings but leave let's in place *)
-      if red_set (info_flags info.infos) fZETA then
+      if red_set info.reds fZETA then
         (* New rule: for Cbv, Delta does not apply to locally bound variables
-           or red_set (info_flags info.infos) fDELTA
+           or red_set info.reds fDELTA
          *)
 	let env' = subs_cons ([|cbv_stack_term info TOP env b|],env) in
         norm_head info env' c stack
@@ -297,7 +302,7 @@ let rec norm_head info env t stack =
 	(CBN(t,env), stack) (* Should we consider a commutative cut ? *)
 
   | Evar ev ->
-      (match evar_value info.infos.i_cache ev with
+      (match Reductionops.safe_evar_value info.sigma ev with
           Some c -> norm_head info env c stack
         | None ->
           let e, xs = ev in
@@ -317,8 +322,8 @@ let rec norm_head info env t stack =
   | Prod _ -> (CBN(t,env), 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 info.tab normt with
+  if red_set_ref info.reds normt then
+    match cbv_value_cache info normt with
       | Some body ->
          if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ debug_pr_key normt);
          strip_appl (shift_value k body) stack
@@ -343,7 +348,7 @@ and cbv_stack_term info stack env t =
 and cbv_stack_value info env = function
   (* a lambda meets an application -> BETA *)
   | (LAM (nlams,ctxt,b,env), APP (args, stk))
-      when red_set (info_flags info.infos) fBETA ->
+      when red_set info.reds fBETA ->
     let nargs = Array.length args in
       if nargs == nlams then
           cbv_stack_term info stk (subs_cons(args,env)) b
@@ -357,31 +362,31 @@ and cbv_stack_value info env = function
 
     (* a Fix applied enough -> IOTA *)
     | (FIXP(fix,env,[||]), stk)
-        when fixp_reducible (info_flags info.infos) fix stk ->
+        when fixp_reducible info.reds fix stk ->
         let (envf,redfix) = contract_fixp env fix in
         cbv_stack_term info stk envf redfix
 
     (* constructor guard satisfied or Cofix in a Case -> IOTA *)
     | (COFIXP(cofix,env,[||]), stk)
-        when cofixp_reducible (info_flags info.infos) cofix stk->
+        when cofixp_reducible info.reds cofix stk->
         let (envf,redfix) = contract_cofixp env cofix in
         cbv_stack_term info stk envf redfix
 
     (* constructor in a Case -> IOTA *)
     | (CONSTR(((sp,n),u),[||]), APP(args,CASE(_,br,ci,env,stk)))
-            when red_set (info_flags info.infos) fMATCH ->
+            when red_set info.reds fMATCH ->
 	let cargs =
           Array.sub args ci.ci_npar (Array.length args - ci.ci_npar) in
         cbv_stack_term info (stack_app cargs stk) env br.(n-1)
 
     (* constructor of arity 0 in a Case -> IOTA *)
     | (CONSTR(((_,n),u),[||]), CASE(_,br,_,env,stk))
-            when red_set (info_flags info.infos) fMATCH ->
+            when red_set info.reds fMATCH ->
                     cbv_stack_term info stk env br.(n-1)
 
     (* constructor in a Projection -> IOTA *)
     | (CONSTR(((sp,n),u),[||]), APP(args,PROJ(p,stk)))
-        when red_set (info_flags info.infos) fMATCH && Projection.unfolded p ->
+        when red_set info.reds fMATCH && Projection.unfolded p ->
       let arg = args.(Projection.npars p + Projection.arg p) in
 	cbv_stack_value info env (strip_appl arg stk)
 
@@ -393,6 +398,29 @@ and cbv_stack_value info env = function
     (* definitely a value *)
     | (head,stk) -> mkSTACK(head, stk)
 
+and cbv_value_cache info ref = match KeyTable.find info.tab ref with
+| v -> Some v
+| exception Not_found ->
+  try
+    let body = match ref with
+    | RelKey n ->
+      let open Context.Rel.Declaration in
+      begin match Environ.lookup_rel n info.env with
+      | LocalDef (_, c, _) -> lift n c
+      | LocalAssum _ -> raise Not_found
+      end
+    | VarKey id ->
+      let open Context.Named.Declaration in
+      begin match Environ.lookup_named id info.env with
+      | LocalDef (_, c, _) -> c
+      | LocalAssum _ -> raise Not_found
+      end
+    | ConstKey cst -> Environ.constant_value_in info.env cst
+    in
+    let v = cbv_stack_term info TOP (subs_id 0) body in
+    let () = KeyTable.add info.tab ref v in
+    Some v
+  with Not_found | Environ.NotEvaluableConst _ -> None
 
 (* When we are sure t will never produce a redex with its stack, we
  * normalize (even under binders) the applied terms and we build the
@@ -453,11 +481,5 @@ let cbv_norm infos constr =
   EConstr.of_constr (with_stats (lazy (cbv_norm_term infos (subs_id 0) constr)))
 
 (* constant bodies are normalized at the first expansion *)
-let create_cbv_infos flgs env sigma =
-  let infos = create
-    ~share:true (** Not used by cbv *)
-    ~repr:(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
-  { tab = CClosure.create_tab (); infos; sigma }
+let create_cbv_infos reds env sigma =
+  { tab = KeyTable.create 91; reds; env; sigma }