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, 50 insertions, 23 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 960bdb649a..817012d8ec 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -37,17 +37,20 @@ let delta = ref 0
 let eta = ref 0
 let zeta = ref 0
 let evar = ref 0
-let iota = ref 0
+let nb_match = ref 0
+let fix = ref 0
+let cofix = ref 0
 let prune = ref 0
 
 let reset () =
-  beta := 0; delta := 0; zeta := 0; evar := 0; iota := 0; evar := 0;
-  prune := 0
+  beta := 0; delta := 0; zeta := 0; evar := 0; nb_match := 0; fix := 0;
+  cofix := 0; evar := 0; prune := 0
 
 let stop() =
   Feedback.msg_debug (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++
 	 str " eta=" ++ int !eta ++ str" zeta=" ++ int !zeta ++ str" evar=" ++
-	 int !evar ++ str" iota=" ++ int !iota ++ str" prune=" ++ int !prune ++
+	 int !evar ++ str" match=" ++ int !nb_match ++ str" fix=" ++ int !fix ++
+         str " cofix=" ++ int !cofix ++ str" prune=" ++ int !prune ++
 	 str"]")
 
 let incr_cnt red cnt =
@@ -78,7 +81,9 @@ module type RedFlagsSig = sig
   val fBETA : red_kind
   val fDELTA : red_kind
   val fETA : red_kind
-  val fIOTA : red_kind
+  val fMATCH : red_kind
+  val fFIX : red_kind
+  val fCOFIX : red_kind
   val fZETA : red_kind
   val fCONST : constant -> red_kind
   val fVAR : Id.t -> red_kind
@@ -103,14 +108,19 @@ module RedFlags = (struct
     r_eta : bool;
     r_const : transparent_state;
     r_zeta : bool;
-    r_iota : bool }
+    r_match : bool;
+    r_fix : bool;
+    r_cofix : bool }
 
-  type red_kind = BETA | DELTA | ETA | IOTA | ZETA
+  type red_kind = BETA | DELTA | ETA | MATCH | FIX
+              | COFIX | ZETA
 	      | CONST of constant | VAR of Id.t
   let fBETA = BETA
   let fDELTA = DELTA
   let fETA = ETA
-  let fIOTA = IOTA
+  let fMATCH = MATCH
+  let fFIX = FIX
+  let fCOFIX = COFIX
   let fZETA = ZETA
   let fCONST kn  = CONST kn
   let fVAR id  = VAR id
@@ -120,7 +130,9 @@ module RedFlags = (struct
     r_eta = false;
     r_const = all_opaque;
     r_zeta = false;
-    r_iota = false }
+    r_match = false;
+    r_fix = false;
+    r_cofix = false }
 
   let red_add red = function
     | BETA -> { red with r_beta = true }
@@ -129,7 +141,9 @@ module RedFlags = (struct
     | CONST kn ->
 	let (l1,l2) = red.r_const in
 	{ red with r_const = l1, Cpred.add kn l2 }
-    | IOTA -> { red with r_iota = true }
+    | MATCH -> { red with r_match = true }
+    | FIX -> { red with r_fix = true }
+    | COFIX -> { red with r_cofix = true }
     | ZETA -> { red with r_zeta = true }
     | VAR id ->
 	let (l1,l2) = red.r_const in
@@ -142,7 +156,9 @@ module RedFlags = (struct
     | CONST kn ->
  	let (l1,l2) = red.r_const in
 	{ red with r_const = l1, Cpred.remove kn l2 }
-    | IOTA -> { red with r_iota = false }
+    | MATCH -> { red with r_match = false }
+    | FIX -> { red with r_fix = false }
+    | COFIX -> { red with r_cofix = false }
     | ZETA -> { red with r_zeta = false }
     | VAR id ->
 	let (l1,l2) = red.r_const in
@@ -165,7 +181,9 @@ module RedFlags = (struct
 	let c = Id.Pred.mem id l in
 	incr_cnt c delta
     | ZETA -> incr_cnt red.r_zeta zeta
-    | IOTA -> incr_cnt red.r_iota iota
+    | MATCH -> incr_cnt red.r_match nb_match
+    | FIX -> incr_cnt red.r_fix fix
+    | COFIX -> incr_cnt red.r_cofix cofix
     | DELTA -> (* Used for Rel/Var defined in context *)
 	incr_cnt red.r_delta delta
 
@@ -177,15 +195,20 @@ end : RedFlagsSig)
 
 open RedFlags
 
-let betadeltaiota = mkflags [fBETA;fDELTA;fZETA;fIOTA]
-let betadeltaiotanolet = mkflags [fBETA;fDELTA;fIOTA]
-let betaiota = mkflags [fBETA;fIOTA]
+let all = mkflags [fBETA;fDELTA;fZETA;fMATCH;fFIX;fCOFIX]
+let allnolet = mkflags [fBETA;fDELTA;fMATCH;fFIX;fCOFIX]
 let beta = mkflags [fBETA]
-let betaiotazeta = mkflags [fBETA;fIOTA;fZETA]
+let betadeltazeta = mkflags [fBETA;fDELTA;fZETA]
+let betaiota = mkflags [fBETA;fMATCH;fFIX;fCOFIX]
+let betaiotazeta = mkflags [fBETA;fMATCH;fFIX;fCOFIX;fZETA]
+let betazeta = mkflags [fBETA;fZETA]
+let delta = mkflags [fDELTA]
+let zeta = mkflags [fZETA]
+let nored = no_red
 
 (* Removing fZETA for finer behaviour would break many developments *)
-let unfold_side_flags = [fBETA;fIOTA;fZETA]
-let unfold_side_red = mkflags [fBETA;fIOTA;fZETA]
+let unfold_side_flags = [fBETA;fMATCH;fFIX;fCOFIX;fZETA]
+let unfold_side_red = mkflags [fBETA;fMATCH;fFIX;fCOFIX;fZETA]
 let unfold_red kn =
   let flag = match kn with
     | EvalVarRef id -> fVAR id
@@ -896,23 +919,27 @@ let rec knr info m stk =
       (match ref_value_cache info (RelKey k) with
           Some v -> kni info v stk
         | None -> (set_norm m; (m,stk)))
-  | FConstruct((ind,c),u) when red_set info.i_flags fIOTA ->
+  | FConstruct((ind,c),u) ->
+     let use_match = red_set info.i_flags fMATCH in
+     let use_fix = red_set info.i_flags fFIX in
+     if use_match || use_fix then
       (match strip_update_shift_app m stk with
-        | (depth, args, ZcaseT(ci,_,br,e)::s) ->
+        | (depth, args, ZcaseT(ci,_,br,e)::s) when use_match ->
             assert (ci.ci_npar>=0);
             let rargs = drop_parameters depth ci.ci_npar args in
             knit info e br.(c-1) (rargs@s)
-        | (_, cargs, Zfix(fx,par)::s) ->
+        | (_, cargs, Zfix(fx,par)::s) when use_fix ->
             let rarg = fapp_stack(m,cargs) in
             let stk' = par @ append_stack [|rarg|] s in
             let (fxe,fxbd) = contract_fix_vect fx.term in
             knit info fxe fxbd stk'
-	| (depth, args, Zproj (n, m, cst)::s) ->
+	| (depth, args, Zproj (n, m, cst)::s) when use_match ->
 	    let rargs = drop_parameters depth n args in
 	    let rarg = project_nth_arg m rargs in
 	      kni info rarg s
         | (_,args,s) -> (m,args@s))
-  | FCoFix _ when red_set info.i_flags fIOTA ->
+     else (m,stk)
+  | FCoFix _ when red_set info.i_flags fCOFIX ->
       (match strip_update_shift_app m stk with
           (_, args, (((ZcaseT _|Zproj _)::_) as stk')) ->
             let (fxe,fxbd) = contract_fix_vect m.term in