diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-02-13 17:49:21 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-03-04 15:13:02 +0100 |
| commit | 16c884413bbf2f0b5fb43bd0be7da0bf7c5e4e75 (patch) | |
| tree | a0685d4245d355104d2c84feaf0950df6fb18e02 /kernel/cClosure.mli | |
| parent | df9d3a36e71d6d224286811fdc529ad5a955deb7 (diff) | |
Pass the constant cache as a separate argument in kernel reduction.
Diffstat (limited to 'kernel/cClosure.mli')
| -rw-r--r-- | kernel/cClosure.mli | 20 |
1 files changed, 11 insertions, 9 deletions
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 |