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, 3 insertions, 3 deletions

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 52afa7f83..8e44fb008 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -36,7 +36,7 @@ let inductive_type_knowing_parameters env (ind,u) jl =
   Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp
 
 let e_type_judgment env evdref j =
-  match kind_of_term (whd_betadeltaiota env !evdref j.uj_type) with
+  match kind_of_term (whd_all env !evdref j.uj_type) with
     | Sort s -> {utj_val = j.uj_val; utj_type = s }
     | Evar ev ->
         let (evd,s) = Evardefine.define_evar_as_sort env !evdref ev in
@@ -54,7 +54,7 @@ let e_judge_of_apply env evdref funj argjv =
       { uj_val  = mkApp (j_val funj, Array.map j_val argjv);
         uj_type = typ }
   | hj::restjl ->
-      match kind_of_term (whd_betadeltaiota env !evdref typ) with
+      match kind_of_term (whd_all env !evdref typ) with
       | Prod (_,c1,c2) ->
 	 if Evarconv.e_cumul env evdref hj.uj_type c1 then
 	   apply_rec (n+1) (subst1 hj.uj_val c2) restjl
@@ -87,7 +87,7 @@ let e_is_correct_arity env evdref c pj ind specif params =
   let allowed_sorts = elim_sorts specif in
   let error () = error_elim_arity env ind allowed_sorts c pj None in
   let rec srec env pt ar =
-    let pt' = whd_betadeltaiota env !evdref pt in
+    let pt' = whd_all env !evdref pt in
     match kind_of_term pt', ar with
     | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' ->
         if not (Evarconv.e_cumul env evdref a1 a1') then error ();