- and stack_term = config lazy_t * C.term lazy_t (* cbv, cbn *)
- and env_term = config lazy_t * C.term lazy_t (* cbv, cbn *)
- let to_env ~reduce ~unwind c = lazy (fst (reduce c)),lazy (unwind c)
- let from_stack (c,_) = Lazy.force c
+ and stack_term =
+ config Lazy.t * (int -> config) * C.term Lazy.t
+ and env_term =
+ config Lazy.t (* cbneed ~delta:0 *)
+ * (int -> config) (* cbvalue ~delta *)
+ * C.term Lazy.t (* cbname ~delta:max_int *)
+ let to_env ~reduce ~unwind c =
+ lazy (fst (reduce ~delta:0 c)),
+ (fun delta -> fst (reduce ~delta c)),
+ lazy (unwind c)
+ let from_stack ~delta (c0,c,_) = if delta = 0 then Lazy.force c0 else c delta