diff options
| author | Pierre-Marie Pédrot | 2020-12-13 00:51:52 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-12-14 09:57:54 +0100 |
| commit | 78a0d0a557f4fb6885987e99c4a12a0826d48c9a (patch) | |
| tree | 37879f29d00ef8cf7de83925988f70dffd037cb9 /pretyping/reductionops.mli | |
| parent | d0667eb4a165c065b0d64069641ca0cd39d62219 (diff) | |
Remove most of Reductionops.*_state functions.
There functions export the internal stack representation. The only real user
is unification, which is suffering from major performance issues due to the
naive representation of substitutions in processes.
Diffstat (limited to 'pretyping/reductionops.mli')
| -rw-r--r-- | pretyping/reductionops.mli | 35 |
1 files changed, 10 insertions, 25 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index d404a7e414..04dfc5ffe6 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -106,8 +106,6 @@ end (************************************************************************) -type state = constr * constr Stack.t - type reduction_function = env -> evar_map -> constr -> constr type e_reduction_function = env -> evar_map -> constr -> evar_map * constr @@ -115,11 +113,6 @@ type e_reduction_function = env -> evar_map -> constr -> evar_map * constr type stack_reduction_function = env -> evar_map -> constr -> constr * constr list -type state_reduction_function = - env -> evar_map -> state -> state - -val pr_state : env -> evar_map -> state -> Pp.t - (** {6 Reduction Function Operators } *) val strong_with_flags : @@ -127,12 +120,6 @@ val strong_with_flags : (CClosure.RedFlags.reds -> reduction_function) val strong : reduction_function -> reduction_function -val whd_state_gen : - CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> state -> state - -val iterate_whd_gen : CClosure.RedFlags.reds -> - Environ.env -> Evd.evar_map -> constr -> constr - (** {6 Generic Optimized Reduction Function using Closures } *) val clos_norm_flags : CClosure.RedFlags.reds -> reduction_function @@ -166,24 +153,13 @@ val whd_all_stack : stack_reduction_function val whd_allnolet_stack : stack_reduction_function val whd_betalet_stack : stack_reduction_function -val whd_nored_state : state_reduction_function -val whd_beta_state : state_reduction_function -val whd_betaiota_state : state_reduction_function -val whd_betaiotazeta_state : state_reduction_function -val whd_all_state : state_reduction_function -val whd_allnolet_state : state_reduction_function -val whd_betalet_state : state_reduction_function - (** {6 Head normal forms } *) val whd_delta_stack : stack_reduction_function -val whd_delta_state : state_reduction_function val whd_delta : reduction_function val whd_betadeltazeta_stack : stack_reduction_function -val whd_betadeltazeta_state : state_reduction_function val whd_betadeltazeta : reduction_function val whd_zeta_stack : stack_reduction_function -val whd_zeta_state : state_reduction_function val whd_zeta : reduction_function val shrink_eta : Environ.env -> constr -> constr @@ -269,8 +245,17 @@ val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> TransparentState.t -> (** {6 Heuristic for Conversion with Evar } *) +type state = constr * constr Stack.t + +type state_reduction_function = + env -> evar_map -> state -> state + +val pr_state : env -> evar_map -> state -> Pp.t + +val whd_nored_state : state_reduction_function + val whd_betaiota_deltazeta_for_iota_state : - TransparentState.t -> Environ.env -> Evd.evar_map -> state -> state + TransparentState.t -> state_reduction_function (** {6 Meta-related reduction functions } *) val meta_instance : env -> evar_map -> constr freelisted -> constr |