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/indtypes.ml   | 14 +++++++-------
 checker/inductive.ml  | 32 ++++++++++++++++----------------
 checker/reduction.ml  | 14 +++++++-------
 checker/reduction.mli |  4 ++--
 checker/typeops.ml    |  4 ++--
 5 files changed, 34 insertions(+), 34 deletions(-)

(limited to 'checker')

diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 29b16392b..40f55a571 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -44,7 +44,7 @@ let prcon c =
 let weaker_noccur_between env x nvars t =
   if noccur_between x nvars t then Some t
   else
-   let t' = whd_betadeltaiota env t in
+   let t' = whd_all env t in
    if noccur_between x nvars t' then Some t'
    else None
 
@@ -90,7 +90,7 @@ exception InductiveError of inductive_error
 (* Typing the arities and constructor types *)
 
 let rec sorts_of_constr_args env t =
-  let t = whd_betadeltaiota_nolet env t in
+  let t = whd_allnolet env t in
   match t with
     | Prod (name,c1,c2) ->
         let varj = infer_type env c1 in
@@ -321,7 +321,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs =
     | [] -> ()
     | LocalDef _ :: hyps -> check k (index+1) hyps
     | _::hyps ->
-        match whd_betadeltaiota env lpar.(k) with
+        match whd_all env lpar.(k) with
 	  | Rel w when w = index -> check (k-1) (index+1) hyps
 	  | _ -> raise (IllFormedInd (LocalNonPar (k+1,index,l)))
   in check (nparams-1) (n-nhyps) hyps;
@@ -342,7 +342,7 @@ let check_rec_par (env,n,_,_) hyps nrecp largs =
           failwith "number of recursive parameters cannot be greater than the number of parameters."
       | (lp,LocalDef _ :: hyps) -> find (index-1) (lp,hyps)
       | (p::lp,_::hyps) ->
-          (match whd_betadeltaiota env p with
+          (match whd_all env p with
 	    | Rel w when w = index -> find (index-1) (lp,hyps)
             | _ -> failwith "bad number of recursive parameters")
   in find (n-1) (lpar,List.rev hyps)
@@ -388,7 +388,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lpar) =
 
 let rec ienv_decompose_prod (env,_,_,_ as ienv) n c =
   if n=0 then (ienv,c) else
-    let c' = whd_betadeltaiota env c in
+    let c' = whd_all env c in
     match c' with
 	Prod(na,a,b) ->
 	  let ienv' = ienv_push_var ienv (na,a,mk_norec) in
@@ -401,7 +401,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc
   let lparams = rel_context_length hyps in
   (* check the inductive types occur positively in [c] *)
   let rec check_pos (env, n, ntypes, ra_env as ienv) c =
-    let x,largs = decompose_app (whd_betadeltaiota env c) in
+    let x,largs = decompose_app (whd_all env c) in
       match x with
 	| Prod (na,b,d) ->
 	    assert (List.is_empty largs);
@@ -470,7 +470,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc
 
   and check_constructors ienv check_head c =
     let rec check_constr_rec (env,n,ntypes,ra_env as ienv) lrec c =
-      let x,largs = decompose_app (whd_betadeltaiota env c) in
+      let x,largs = decompose_app (whd_all env c) in
 	match x with
           | Prod (na,b,d) ->
 	      assert (List.is_empty largs);
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 6f9b5f204..8bbd0f142 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -31,20 +31,20 @@ let lookup_mind_specif env (kn,tyi) =
   (mib, mib.mind_packets.(tyi))
 
 let find_rectype env c =
-  let (t, l) = decompose_app (whd_betadeltaiota env c) in
+  let (t, l) = decompose_app (whd_all env c) in
   match t with
   | Ind ind -> (ind, l)
   | _ -> raise Not_found
 
 let find_inductive env c =
-  let (t, l) = decompose_app (whd_betadeltaiota env c) in
+  let (t, l) = decompose_app (whd_all env c) in
   match t with
     | Ind (ind,_)
         when (fst (lookup_mind_specif env ind)).mind_finite != CoFinite -> (ind, l)
     | _ -> raise Not_found
 
 let find_coinductive env c =
-  let (t, l) = decompose_app (whd_betadeltaiota env c) in
+  let (t, l) = decompose_app (whd_all env c) in
   match t with
     | Ind (ind,_)
         when (fst (lookup_mind_specif env ind)).mind_finite == CoFinite -> (ind, l)
@@ -299,7 +299,7 @@ let check_allowed_sort ksort specif =
 let is_correct_arity env c (p,pj) ind specif params =
   let arsign,_ = get_instantiated_arity ind specif params in
   let rec srec env pt ar =
-    let pt' = whd_betadeltaiota env pt in
+    let pt' = whd_all env pt in
     match pt', ar with
       | Prod (na1,a1,t), LocalAssum (_,a1')::ar' ->
           (try conv env a1 a1'
@@ -307,7 +307,7 @@ let is_correct_arity env c (p,pj) ind specif params =
           srec (push_rel (LocalAssum (na1,a1)) env) t ar'
       | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *)
 	 let env' = push_rel (LocalAssum (na1,a1)) env in
-     let ksort = match (whd_betadeltaiota env' a2) with
+     let ksort = match (whd_all env' a2) with
         | Sort s -> family_of_sort s
 	    | _ -> raise (LocalArity None) in
 	  let dep_ind = build_dependent_inductive ind specif params in
@@ -578,7 +578,7 @@ let check_inductive_codomain env p =
   let env = push_rel_context absctx env in
   let arctx, s = dest_prod_assum env ar in
   let env = push_rel_context arctx env in
-  let i,l' = decompose_app (whd_betadeltaiota env s) in
+  let i,l' = decompose_app (whd_all env s) in
   match i with Ind _ -> true | _ -> false 
 
 (* The following functions are almost duplicated from indtypes.ml, except
@@ -602,7 +602,7 @@ let ienv_push_inductive (env, ra_env) ((mind,u),lpar) =
 
 let rec ienv_decompose_prod (env,_ as ienv) n c =
  if Int.equal n 0 then (ienv,c) else
-   let c' = whd_betadeltaiota env c in
+   let c' = whd_all env c in
    match c' with
    Prod(na,a,b) ->
      let ienv' = ienv_push_var ienv (na,a,mk_norec) in
@@ -632,7 +632,7 @@ close to check_positive in indtypes.ml, but does no positivy check and does not
 compute the number of recursive arguments. *)
 let get_recargs_approx env tree ind args =
   let rec build_recargs (env, ra_env as ienv) tree c =
-    let x,largs = decompose_app (whd_betadeltaiota env c) in
+    let x,largs = decompose_app (whd_all env c) in
     match x with
     | Prod (na,b,d) ->
        assert (List.is_empty largs);
@@ -691,7 +691,7 @@ let get_recargs_approx env tree ind args =
 
   and build_recargs_constructors ienv trees c =
     let rec recargs_constr_rec (env,ra_env as ienv) trees lrec c =
-      let x,largs = decompose_app (whd_betadeltaiota env c) in
+      let x,largs = decompose_app (whd_all env c) in
 	match x with
 
           | Prod (na,b,d) ->
@@ -720,7 +720,7 @@ let restrict_spec env spec p =
   let env = push_rel_context absctx env in
   let arctx, s = dest_prod_assum env ar in
   let env = push_rel_context arctx env in
-  let i,args = decompose_app (whd_betadeltaiota env s) in
+  let i,args = decompose_app (whd_all env s) in
   match i with
   | Ind i ->
      begin match spec with
@@ -742,7 +742,7 @@ let restrict_spec env spec p =
 
 let rec subterm_specif renv stack t =
   (* maybe reduction is not always necessary! *)
-  let f,l = decompose_app (whd_betadeltaiota renv.env t) in
+  let f,l = decompose_app (whd_all renv.env t) in
     match f with
       | Rel k -> subterm_var k renv
 
@@ -856,11 +856,11 @@ let filter_stack_domain env ci p stack =
   if noccur_with_meta 1 (rel_context_length absctx) ar then stack
   else let env = push_rel_context absctx env in
   let rec filter_stack env ar stack =
-    let t = whd_betadeltaiota env ar in
+    let t = whd_all env ar in
     match stack, t with
     | elt :: stack', Prod (n,a,c0) ->
       let d = LocalAssum (n,a) in
-      let ty, args = decompose_app (whd_betadeltaiota env a) in
+      let ty, args = decompose_app (whd_all env a) in
       let elt = match ty with
       | Ind ind -> 
         let spec' = stack_element_specif elt in
@@ -1032,7 +1032,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
     (* check fi does not appear in the k+1 first abstractions,
        gives the type of the k+1-eme abstraction (must be an inductive)  *)
     let rec check_occur env n def =
-      match (whd_betadeltaiota env def) with
+      match (whd_all env def) with
         | Lambda (x,a,b) ->
 	    if noccur_with_meta n nbfix a then
 	      let env' = push_rel (LocalAssum (x,a)) env in
@@ -1081,7 +1081,7 @@ let anomaly_ill_typed () =
   anomaly ~label:"check_one_cofix" (Pp.str "too many arguments applied to constructor")
 
 let rec codomain_is_coind env c =
-  let b = whd_betadeltaiota env c in
+  let b = whd_all env c in
   match b with
     | Prod (x,a,b) ->
 	codomain_is_coind (push_rel (LocalAssum (x,a)) env) b
@@ -1093,7 +1093,7 @@ let rec codomain_is_coind env c =
 let check_one_cofix env nbfix def deftype =
   let rec check_rec_call env alreadygrd n tree vlra  t =
     if not (noccur_with_meta n nbfix t) then
-      let c,args = decompose_app (whd_betadeltaiota env t) in
+      let c,args = decompose_app (whd_all env t) in
       match c with
 	| Rel p when  n <= p && p < n+nbfix ->
 	    (* recursive call: must be guarded and no nested recursive
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
diff --git a/checker/reduction.mli b/checker/reduction.mli
index 2f551f4a6..15a2df1f1 100644
--- a/checker/reduction.mli
+++ b/checker/reduction.mli
@@ -16,8 +16,8 @@ open Environ
 (*s Reduction functions *)
 
 val whd_betaiotazeta        : constr -> constr
-val whd_betadeltaiota       : env -> constr -> constr
-val whd_betadeltaiota_nolet : env -> constr -> constr
+val whd_all       : env -> constr -> constr
+val whd_allnolet : env -> constr -> constr
 
 (************************************************************************)
 (*s conversion functions *)
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 0c7e538be..886689329 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -33,7 +33,7 @@ let check_constraints cst env =
 
 (* This should be a type (a priori without intension to be an assumption) *)
 let type_judgment env (c,ty as j) =
-  match whd_betadeltaiota env ty with
+  match whd_all env ty with
     | Sort s -> (c,s)
     | _ -> error_not_type env j
 
@@ -107,7 +107,7 @@ let judge_of_apply env (f,funj) argjv =
   let rec apply_rec n typ = function
     | [] -> typ
     | (h,hj)::restjl ->
-        (match whd_betadeltaiota env typ with
+        (match whd_all env typ with
           | Prod (_,c1,c2) ->
 	      (try conv_leq env hj c1
 	      with NotConvertible ->
-- 
cgit v1.2.3