From 16c884413bbf2f0b5fb43bd0be7da0bf7c5e4e75 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 13 Feb 2018 17:49:21 +0100 Subject: Pass the constant cache as a separate argument in kernel reduction. --- kernel/cClosure.mli | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) (limited to 'kernel/cClosure.mli') diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index c43fc4623..da14ff165 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -98,13 +98,15 @@ 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 -> table_key -> 'a option -val create: ('a infos -> constr -> 'a) -> reds -> env -> +val ref_value_cache: 'a infos -> 'a infos_tab -> table_key -> 'a option +val create: ('a infos -> 'a infos_tab -> constr -> 'a) -> 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 @@ -198,15 +200,15 @@ val infos_with_reds : clos_infos -> reds -> clos_infos (** Reduction function *) (** [norm_val] is for strong normalization *) -val norm_val : clos_infos -> fconstr -> constr +val norm_val : clos_infos -> fconstr infos_tab -> fconstr -> constr (** [whd_val] is for weak head normalization *) -val whd_val : clos_infos -> fconstr -> constr +val whd_val : clos_infos -> fconstr infos_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 -> stack -> fconstr * stack + clos_infos -> fconstr infos_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 @@ -223,7 +225,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 -> table_key -> fconstr option +val unfold_reference : clos_infos -> fconstr infos_tab -> table_key -> fconstr option val eq_table_key : table_key -> table_key -> bool @@ -239,9 +241,9 @@ val mk_clos_deep : (fconstr subs -> constr -> fconstr) -> fconstr subs -> constr -> fconstr -val kni: clos_infos -> fconstr -> stack -> fconstr * stack -val knr: clos_infos -> fconstr -> stack -> fconstr * stack -val kl : clos_infos -> fconstr -> constr +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 to_constr : (lift -> fconstr -> constr) -> lift -> fconstr -> constr -- cgit v1.2.3