Separate flags for fix/cofix/match reduction and clean reduction function names.

This is a reimplementation of Hugo's PR#117.

We are trying to address the problem that the name of some reduction functions
was not saying what they were doing (e.g. whd_betadeltaiota was doing let-in
reduction). Like PR#117, we are careful that no function changed semantics
without changing the names. Porting existing ML code should be a matter of
renamings a few function calls.

Also, we introduce more precise reduction flags fMATCH, fFIX, fCOFIX
collectively denominated iota.

We renamed the following functions:

Closure.betadeltaiota -> Closure.all
Closure.betadeltaiotanolet -> Closure.allnolet
Reductionops.beta -> Closure.beta
Reductionops.zeta -> Closure.zeta
Reductionops.betaiota -> Closure.betaiota
Reductionops.betaiotazeta -> Closure.betaiotazeta
Reductionops.delta -> Closure.delta
Reductionops.betalet -> Closure.betazeta
Reductionops.betadelta -> Closure.betadeltazeta
Reductionops.betadeltaiota -> Closure.all
Reductionops.betadeltaiotanolet -> Closure.allnolet
Closure.no_red -> Closure.nored
Reductionops.nored -> Closure.nored
Reductionops.nf_betadeltaiota -> Reductionops.nf_all
Reductionops.whd_betadelta -> Reductionops.whd_betadeltazeta
Reductionops.whd_betadeltaiota -> Reductionops.whd_all
Reductionops.whd_betadeltaiota_nolet -> Reductionops.whd_allnolet
Reductionops.whd_betadelta_stack -> Reductionops.whd_betadeltazeta_stack
Reductionops.whd_betadeltaiota_stack -> Reductionops.whd_all_stack
Reductionops.whd_betadeltaiota_nolet_stack -> Reductionops.whd_allnolet_stack
Reductionops.whd_betadelta_state -> Reductionops.whd_betadeltazeta_state
Reductionops.whd_betadeltaiota_state -> Reductionops.whd_all_state
Reductionops.whd_betadeltaiota_nolet_state -> Reductionops.whd_allnolet_state
Reductionops.whd_eta -> Reductionops.shrink_eta
Tacmach.pf_whd_betadeltaiota -> Tacmach.pf_whd_all
Tacmach.New.pf_whd_betadeltaiota -> Tacmach.New.pf_whd_all

And removed the following ones:

Reductionops.whd_betaetalet
Reductionops.whd_betaetalet_stack
Reductionops.whd_betaetalet_state
Reductionops.whd_betadeltaeta_stack
Reductionops.whd_betadeltaeta_state
Reductionops.whd_betadeltaeta
Reductionops.whd_betadeltaiotaeta_stack
Reductionops.whd_betadeltaiotaeta_state
Reductionops.whd_betadeltaiotaeta

They were unused and having some reduction functions perform eta is confusing
as whd_all and nf_all don't do it.

1 files changed, 12 insertions, 21 deletions

diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index b38252e97..e7a6b3d64 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -148,7 +148,7 @@ val clos_norm_flags : Closure.RedFlags.reds -> reduction_function
 val nf_beta : local_reduction_function
 val nf_betaiota : local_reduction_function
 val nf_betaiotazeta : local_reduction_function
-val nf_betadeltaiota : reduction_function
+val nf_all : reduction_function
 val nf_evar : evar_map -> constr -> constr
 
 (** Lazy strategy, weak head reduction *)
@@ -158,9 +158,8 @@ val whd_nored : local_reduction_function
 val whd_beta : local_reduction_function
 val whd_betaiota : local_reduction_function
 val whd_betaiotazeta : local_reduction_function
-val whd_betadeltaiota :  contextual_reduction_function
-val whd_betadeltaiota_nolet :  contextual_reduction_function
-val whd_betaetalet : local_reduction_function
+val whd_all :  contextual_reduction_function
+val whd_allnolet :  contextual_reduction_function
 val whd_betalet : local_reduction_function
 
 (** Removes cast and put into applicative form *)
@@ -168,18 +167,16 @@ val whd_nored_stack : local_stack_reduction_function
 val whd_beta_stack : local_stack_reduction_function
 val whd_betaiota_stack : local_stack_reduction_function
 val whd_betaiotazeta_stack : local_stack_reduction_function
-val whd_betadeltaiota_stack : contextual_stack_reduction_function
-val whd_betadeltaiota_nolet_stack : contextual_stack_reduction_function
-val whd_betaetalet_stack : local_stack_reduction_function
+val whd_all_stack : contextual_stack_reduction_function
+val whd_allnolet_stack : contextual_stack_reduction_function
 val whd_betalet_stack : local_stack_reduction_function
 
 val whd_nored_state : local_state_reduction_function
 val whd_beta_state : local_state_reduction_function
 val whd_betaiota_state : local_state_reduction_function
 val whd_betaiotazeta_state : local_state_reduction_function
-val whd_betadeltaiota_state : contextual_state_reduction_function
-val whd_betadeltaiota_nolet_state : contextual_state_reduction_function
-val whd_betaetalet_state : local_state_reduction_function
+val whd_all_state : contextual_state_reduction_function
+val whd_allnolet_state : contextual_state_reduction_function
 val whd_betalet_state : local_state_reduction_function
 
 (** {6 Head normal forms } *)
@@ -187,17 +184,11 @@ val whd_betalet_state : local_state_reduction_function
 val whd_delta_stack :  stack_reduction_function
 val whd_delta_state :  state_reduction_function
 val whd_delta :  reduction_function
-val whd_betadelta_stack :  stack_reduction_function
-val whd_betadelta_state :  state_reduction_function
-val whd_betadelta :  reduction_function
-val whd_betadeltaeta_stack :  stack_reduction_function
-val whd_betadeltaeta_state :  state_reduction_function
-val whd_betadeltaeta :  reduction_function
-val whd_betadeltaiotaeta_stack :  stack_reduction_function
-val whd_betadeltaiotaeta_state :  state_reduction_function
-val whd_betadeltaiotaeta :  reduction_function
-
-val whd_eta : constr -> constr
+val whd_betadeltazeta_stack :  stack_reduction_function
+val whd_betadeltazeta_state :  state_reduction_function
+val whd_betadeltazeta :  reduction_function
+
+val shrink_eta : constr -> constr
 val whd_zeta : constr -> constr
 
 (** Various reduction functions *)