From e57aab0559297cff3875931258674cfe2cfbbba3 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 30 Jun 2016 14:22:02 +0200
Subject: 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.
---
 plugins/funind/functional_principles_proofs.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 52094cf085..146749d32b 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -281,7 +281,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type  =
 	  List.fold_left2 compute_substitution sub args1 args2
 	end
       else
-	if (eq_constr t1 t2) then sub else nochange ~t':(make_refl_eq constructor (Reduction.whd_betadeltaiota env t1) t2)  "cannot solve (diff)"
+	if (eq_constr t1 t2) then sub else nochange ~t':(make_refl_eq constructor (Reduction.whd_all env t1) t2)  "cannot solve (diff)"
     in
     let sub = compute_substitution Int.Map.empty (snd t1) (snd t2) in
     let sub = compute_substitution sub (fst t1) (fst t2) in
-- 
cgit v1.2.3


From 1b09098cc4830f262820d2935a9cd0afa383ed3f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 1 Jul 2016 13:57:14 +0200
Subject: Add and document match, fix and cofix reduction flags.

---
 plugins/funind/recdef.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index e742f7b80d..ceea4fa535 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -161,7 +161,7 @@ let rec n_x_id ids n =
 let simpl_iter clause =
   reduce
     (Lazy
-       {rBeta=true;rIota=true;rZeta= true; rDelta=false;
+       {rBeta=true;rMatch=true;rFix=true;rCofix=true;rZeta=true;rDelta=false;
         rConst = [ EvalConstRef (const_of_ref (delayed_force iter_ref))]})
     clause
 
-- 
cgit v1.2.3