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.

5 files changed, 13 insertions, 10 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 853410db8b..ef38458578 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -72,7 +72,7 @@ let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c
 exception NotExtensibleClause
 
 let clenv_push_prod cl =
-  let typ = whd_betadeltaiota (cl_env cl) (cl_sigma cl) (clenv_type cl) in
+  let typ = whd_all (cl_env cl) (cl_sigma cl) (clenv_type cl) in
   let rec clrec typ = match kind_of_term typ with
     | Cast (t,_,_) -> clrec t
     | Prod (na,t,u) ->
diff --git a/proofs/logic.ml b/proofs/logic.ml
index fd8a70c650..bfaeae712c 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -463,7 +463,7 @@ and mk_hdgoals sigma goal goalacc trm =
 
 and mk_arggoals sigma goal goalacc funty allargs =
   let foldmap (goalacc, funty, sigma) harg =
-    let t = whd_betadeltaiota (Goal.V82.env sigma goal) sigma funty in
+    let t = whd_all (Goal.V82.env sigma goal) sigma funty in
     let rec collapse t = match kind_of_term t with
     | LetIn (_, c1, _, b) -> collapse (subst1 c1 b)
     | _ -> t
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index ee55915211..55dfb88b46 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -146,7 +146,10 @@ let make_flag_constant = function
 let make_flag env f =
   let red = no_red in
   let red = if f.rBeta then red_add red fBETA else red in
-  let red = if f.rIota then red_add red fIOTA else red in
+  let red =
+    if f.rIota then (red_add (red_add (red_add red fMATCH) fFIX) fCOFIX)
+    else red
+  in
   let red = if f.rZeta then red_add red fZETA else red in
   let red =
     if f.rDelta then (* All but rConst *)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 8c0b4ba98a..50984c48e0 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -84,7 +84,7 @@ let pf_eapply f gls x =
 let pf_reduce = pf_apply
 let pf_e_reduce = pf_apply
 
-let pf_whd_betadeltaiota         = pf_reduce whd_betadeltaiota
+let pf_whd_all         = pf_reduce whd_all
 let pf_hnf_constr                = pf_reduce hnf_constr
 let pf_nf                        = pf_reduce simpl
 let pf_nf_betaiota               = pf_reduce (fun _ -> nf_betaiota)
@@ -101,7 +101,7 @@ let pf_const_value              = pf_reduce (fun env _ -> constant_value_in env)
 let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind
 let pf_reduce_to_atomic_ind     = pf_reduce reduce_to_atomic_ind
 
-let pf_hnf_type_of gls          = pf_whd_betadeltaiota gls % pf_get_type_of gls
+let pf_hnf_type_of gls          = pf_whd_all gls % pf_get_type_of gls
 
 let pf_is_matching              = pf_apply Constr_matching.is_matching_conv
 let pf_matches                  = pf_apply Constr_matching.matches_conv
@@ -219,7 +219,7 @@ module New = struct
     let sigma = project gl in
     nf_evar sigma concl
 
-  let pf_whd_betadeltaiota gl t = pf_apply whd_betadeltaiota gl t
+  let pf_whd_all gl t = pf_apply whd_all gl t
 
   let pf_get_type_of gl t = pf_apply Retyping.get_type_of gl t
 
@@ -228,11 +228,11 @@ module New = struct
 
   let pf_hnf_constr gl t = pf_apply hnf_constr gl t
   let pf_hnf_type_of gl t =
-    pf_whd_betadeltaiota gl (pf_get_type_of gl t)
+    pf_whd_all gl (pf_get_type_of gl t)
 
   let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t
 
-  let pf_whd_betadeltaiota gl t = pf_apply whd_betadeltaiota gl t
+  let pf_whd_all gl t = pf_apply whd_all gl t
   let pf_compute gl t = pf_apply compute gl t
 
   let pf_nf_evar gl t = nf_evar (project gl) t
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 182433cb3a..100ed1522e 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -63,7 +63,7 @@ val pf_e_reduce :
   (env -> evar_map -> constr -> evar_map * constr) ->
   goal sigma -> constr -> evar_map * constr
 
-val pf_whd_betadeltaiota       : goal sigma -> constr -> constr
+val pf_whd_all       : goal sigma -> constr -> constr
 val pf_hnf_constr              : goal sigma -> constr -> constr
 val pf_nf                      : goal sigma -> constr -> constr
 val pf_nf_betaiota             : goal sigma -> constr -> constr
@@ -127,7 +127,7 @@ module New : sig
   val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> constr -> types
   val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types
 
-  val pf_whd_betadeltaiota : ('a, 'r) Proofview.Goal.t -> constr -> constr
+  val pf_whd_all : ('a, 'r) Proofview.Goal.t -> constr -> constr
   val pf_compute : ('a, 'r) Proofview.Goal.t -> constr -> constr
 
   val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> constr -> patvar_map