From e57aab0559297cff3875931258674cfe2cfbbba3 Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
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.
---
 checker/reduction.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'checker/reduction.ml')

diff --git a/checker/reduction.ml b/checker/reduction.ml
index b280df54a..97cf6ca75 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -92,13 +92,13 @@ let whd_betaiotazeta x =
        Prod _|Lambda _|Fix _|CoFix _) -> x
     | _ -> whd_val (create_clos_infos betaiotazeta empty_env) (inject x)
 
-let whd_betadeltaiota env t =
+let whd_all env t =
   match t with
     | (Sort _|Meta _|Evar _|Ind _|Construct _|
        Prod _|Lambda _|Fix _|CoFix _) -> t
     | _ -> whd_val (create_clos_infos betadeltaiota env) (inject t)
 
-let whd_betadeltaiota_nolet env t =
+let whd_allnolet env t =
   match t with
     | (Sort _|Meta _|Evar _|Ind _|Construct _|
        Prod _|Lambda _|Fix _|CoFix _|LetIn _) -> t
@@ -477,7 +477,7 @@ let vm_conv cv_pb = fconv cv_pb true
  * error message. *)
 
 let hnf_prod_app env t n =
-  match whd_betadeltaiota env t with
+  match whd_all env t with
     | Prod (_,_,b) -> subst1 n b
     | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product")
 
@@ -488,7 +488,7 @@ let hnf_prod_applist env t nl =
 
 let dest_prod env =
   let rec decrec env m c =
-    let t = whd_betadeltaiota env c in
+    let t = whd_all env c in
     match t with
       | Prod (n,a,c0) ->
           let d = LocalAssum (n,a) in
@@ -500,7 +500,7 @@ let dest_prod env =
 (* The same but preserving lets in the context, not internal ones. *)
 let dest_prod_assum env =
   let rec prodec_rec env l ty =
-    let rty = whd_betadeltaiota_nolet env ty in
+    let rty = whd_allnolet env ty in
     match rty with
     | Prod (x,t,c)  ->
         let d = LocalAssum (x,t) in
@@ -510,7 +510,7 @@ let dest_prod_assum env =
 	prodec_rec (push_rel d env) (d::l) c
     | Cast (c,_,_)    -> prodec_rec env l c
     | _               ->
-      let rty' = whd_betadeltaiota env rty in
+      let rty' = whd_all env rty in
 	if Term.eq_constr rty' rty then l, rty
 	else prodec_rec env l rty'
   in
@@ -518,7 +518,7 @@ let dest_prod_assum env =
 
 let dest_lam_assum env =
   let rec lamec_rec env l ty =
-    let rty = whd_betadeltaiota_nolet env ty in
+    let rty = whd_allnolet env ty in
     match rty with
     | Lambda (x,t,c)  ->
         let d = LocalAssum (x,t) in
-- 
cgit v1.2.3