+module CallByValueByNameForUnwind' =
+ struct
+ type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
+ and stack_term = config lazy_t * Cic.term lazy_t (* cbv, cbn *)
+ and env_term = config lazy_t * Cic.term lazy_t (* cbv, cbn *)
+ and ens_term = config lazy_t * Cic.term lazy_t (* cbv, cbn *)
+
+ let to_env ~reduce ~unwind c = lazy (reduce c),lazy (unwind c)
+ let to_ens ~reduce ~unwind c = lazy (reduce c),lazy (unwind c)
+ let from_stack (c,_) = Lazy.force c
+ let from_stack_list_for_unwind ~unwind l = List.map (function (_,c) -> Lazy.force c) l
+ let from_env (c,_) = Lazy.force c
+ let from_ens (c,_) = Lazy.force c
+ let from_env_for_unwind ~unwind (_,c) = Lazy.force c
+ let from_ens_for_unwind ~unwind (_,c) = Lazy.force c
+ let stack_to_env ~reduce ~unwind config = config
+ let compute_to_env ~reduce ~unwind k e ens t =
+ lazy (reduce (k,e,ens,t,[])), lazy (unwind (k,e,ens,t,[]))
+ let compute_to_stack ~reduce ~unwind config = lazy (reduce config), lazy (unwind config)
+ end
+;;
+