diff options
57 files changed, 366 insertions, 317 deletions
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 -> diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index f7c8fbb30..dd0a81603 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -2,6 +2,52 @@ = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 = ========================================= +** Reduction functions ** + +In closure.ml, we introduced the more precise reduction flags fMATCH, fFIX, +fCOFIX. + +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 + ** Notation_ops ** Use Glob_ops.glob_constr_eq instead of Notation_ops.eq_glob_constr. diff --git a/kernel/closure.ml b/kernel/closure.ml index 960bdb649..817012d8e 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 diff --git a/kernel/closure.mli b/kernel/closure.mli index 8e172290f..76145e3f8 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -41,8 +41,10 @@ module type RedFlagsSig = sig val fBETA : red_kind val fDELTA : red_kind val fETA : red_kind - (** This flag is never used by the kernel reduction but pretyping does *) - val fIOTA : red_kind + (** The fETA flag is never used by the kernel reduction but pretyping does *) + 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 @@ -73,11 +75,18 @@ end module RedFlags : RedFlagsSig open RedFlags -val beta : reds -val betaiota : reds -val betadeltaiota : reds -val betaiotazeta : reds -val betadeltaiotanolet : reds +(* These flags do not contain eta *) +val all : reds +val allnolet : reds +val beta : reds +val betadeltazeta : reds +val betaiota : reds +val betaiotazeta : reds +val betazeta : reds +val delta : reds +val zeta : reds +val nored : reds + val unfold_side_red : reds val unfold_red : evaluable_global_reference -> reds diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index c2c8ee242..e28d770e8 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.ml @@ -35,12 +35,12 @@ let check_constraints cst env = (* This should be a type (a priori without intention to be an assumption) *) let type_judgment env c t = - match kind_of_term(whd_betadeltaiota env t) with + match kind_of_term(whd_all env t) with | Sort s -> {utj_val = c; utj_type = s } | _ -> error_not_type env (make_judge c t) let check_type env c t = - match kind_of_term(whd_betadeltaiota env t) with + match kind_of_term(whd_all env t) with | Sort s -> s | _ -> error_not_type env (make_judge c t) @@ -157,7 +157,7 @@ let judge_of_apply env func funt argsv argstv = let rec apply_rec i typ = if Int.equal i len then typ else - (match kind_of_term (whd_betadeltaiota env typ) with + (match kind_of_term (whd_all env typ) with | Prod (_,c1,c2) -> let arg = argsv.(i) and argt = argstv.(i) in (try diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index b6942e133..0b99c8dc2 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -50,7 +50,7 @@ let is_indices_matter () = !indices_matter 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 @@ -129,7 +129,7 @@ let is_unit constrsinfos = let infos_and_sort env t = let rec aux env t max = - let t = whd_betadeltaiota env t in + let t = whd_all env t in match kind_of_term t with | Prod (name,c1,c2) -> let varj = infer_type env c1 in @@ -409,7 +409,7 @@ let check_correct_par (env,n,ntypes,_) paramdecls ind_index args = | LocalDef _ :: paramdecls -> check param_index (paramdecl_index+1) paramdecls | _::paramdecls -> - match kind_of_term (whd_betadeltaiota env params.(param_index)) with + match kind_of_term (whd_all env params.(param_index)) with | Rel w when Int.equal w paramdecl_index -> check (param_index-1) (paramdecl_index+1) paramdecls | _ -> @@ -436,7 +436,7 @@ if Int.equal nmr 0 then 0 else | (_,[]) -> assert false (* |paramsctxt|>=nmr *) | (lp, LocalDef _ :: paramsctxt) -> find k (index-1) (lp,paramsctxt) | (p::lp,_::paramsctxt) -> - ( match kind_of_term (whd_betadeltaiota env p) with + ( match kind_of_term (whd_all env p) with | Rel w when Int.equal w index -> find (k+1) (index-1) (lp,paramsctxt) | _ -> k) in find 0 (n-1) (lpar,List.rev paramsctxt) @@ -466,7 +466,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lrecparams) = 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 kind_of_term c' with Prod(na,a,b) -> let ienv' = ienv_push_var ienv (na,a,mk_norec) in @@ -495,7 +495,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( constructor [cn] has a type of the shape [… -> c … -> P], where, more generally, the arrows may be dependent). *) let rec check_pos (env, n, ntypes, ra_env as ienv) nmr c = - let x,largs = decompose_app (whd_betadeltaiota env c) in + let x,largs = decompose_app (whd_all env c) in match kind_of_term x with | Prod (na,b,d) -> let () = assert (List.is_empty largs) in @@ -513,7 +513,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d) | Rel k -> (try let (ra,rarg) = List.nth ra_env (k-1) in - let largs = List.map (whd_betadeltaiota env) largs in + let largs = List.map (whd_all env) largs in let nmr1 = (match ra with Mrec _ -> compute_rec_par ienv paramsctxt nmr largs @@ -603,7 +603,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( inductive type. *) and check_constructors ienv check_head nmr c = let rec check_constr_rec (env,n,ntypes,ra_env as ienv) nmr lrec c = - let x,largs = decompose_app (whd_betadeltaiota env c) in + let x,largs = decompose_app (whd_all env c) in match kind_of_term x with | Prod (na,b,d) -> diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 8e26370ec..29966facb 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -29,20 +29,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 kind_of_term 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 kind_of_term t with | Ind ind when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite <> Decl_kinds.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 kind_of_term t with | Ind ind when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite == Decl_kinds.CoFinite -> (ind, l) @@ -313,7 +313,7 @@ let check_allowed_sort ksort specif = let is_correct_arity env c 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 kind_of_term pt', ar with | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' -> let () = @@ -323,7 +323,7 @@ let is_correct_arity env c pj ind specif params = (* The last Prod domain is the type of the scrutinee *) | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *) let env' = push_rel (LocalAssum (na1,a1)) env in - let ksort = match kind_of_term (whd_betadeltaiota env' a2) with + let ksort = match kind_of_term (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 @@ -563,7 +563,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 isInd i (* The following functions are almost duplicated from indtypes.ml, except @@ -586,7 +586,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 kind_of_term c' with Prod(na,a,b) -> let ienv' = ienv_push_var ienv (na,a,mk_norec) in @@ -618,7 +618,7 @@ close to check_positive in indtypes.ml, but does no positivity check and does no 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 kind_of_term x with | Prod (na,b,d) -> assert (List.is_empty largs); @@ -677,7 +677,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 kind_of_term x with | Prod (na,b,d) -> @@ -706,7 +706,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 kind_of_term i with | Ind i -> begin match spec with @@ -727,7 +727,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 kind_of_term f with | Rel k -> subterm_var k renv | Case (ci,p,c,lbr) -> @@ -854,11 +854,11 @@ let filter_stack_domain env ci p stack = if noccur_with_meta 1 (Context.Rel.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, kind_of_term 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 kind_of_term ty with | Ind ind -> let spec' = stack_element_specif elt in @@ -1047,7 +1047,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 kind_of_term (whd_betadeltaiota env def) with + match kind_of_term (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 @@ -1101,7 +1101,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 kind_of_term b with | Prod (x,a,b) -> codomain_is_coind (push_rel (LocalAssum (x,a)) env) b @@ -1113,7 +1113,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 kind_of_term c with | Rel p when n <= p && p < n+nbfix -> (* recursive call: must be guarded and no nested recursive diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 710bfa19b..2dc2f0c7c 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -107,17 +107,17 @@ let whd_betaiotazeta env x = Prod _|Lambda _|Fix _|CoFix _) -> x | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x) -let whd_betadeltaiota env t = +let whd_all env t = match kind_of_term t with | (Sort _|Meta _|Evar _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _) -> t - | _ -> whd_val (create_clos_infos betadeltaiota env) (inject t) + | _ -> whd_val (create_clos_infos all env) (inject t) -let whd_betadeltaiota_nolet env t = +let whd_allnolet env t = match kind_of_term t with | (Sort _|Meta _|Evar _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _|LetIn _) -> t - | _ -> whd_val (create_clos_infos betadeltaiotanolet env) (inject t) + | _ -> whd_val (create_clos_infos allnolet env) (inject t) (********************************************************************) (* Conversion *) @@ -731,7 +731,7 @@ let betazeta_appvect = lambda_appvect_assum * error message. *) let hnf_prod_app env t n = - match kind_of_term (whd_betadeltaiota env t) with + match kind_of_term (whd_all env t) with | Prod (_,_,b) -> subst1 n b | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product") @@ -742,7 +742,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 kind_of_term t with | Prod (n,a,c0) -> let d = LocalAssum (n,a) in @@ -754,7 +754,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 kind_of_term rty with | Prod (x,t,c) -> let d = LocalAssum (x,t) in @@ -764,7 +764,7 @@ let dest_prod_assum env = prodec_rec (push_rel d env) (Context.Rel.add 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 @@ -772,7 +772,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 kind_of_term rty with | Lambda (x,t,c) -> let d = LocalAssum (x,t) in diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 389644692..9812c45f7 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -12,9 +12,11 @@ open Environ (*********************************************************************** s Reduction functions *) +(* None of these functions do eta reduction *) + val whd_betaiotazeta : env -> 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 val whd_betaiota : env -> constr -> constr val nf_betaiota : env -> constr -> constr diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 0ea68e2bc..683f6bde5 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -37,7 +37,7 @@ let check_constraints cst env = (* This should be a type (a priori without intension to be an assumption) *) let type_judgment env j = - match kind_of_term(whd_betadeltaiota env j.uj_type) with + match kind_of_term(whd_all env j.uj_type) with | Sort s -> {utj_val = j.uj_val; utj_type = s } | _ -> error_not_type env j @@ -137,7 +137,7 @@ let make_polymorphic_if_constant_for_ind env {uj_val = c; uj_type = t} = let params, ccl = dest_prod_assum env t in match kind_of_term ccl with | Sort (Type u) -> - let ind, l = decompose_app (whd_betadeltaiota env c) in + let ind, l = decompose_app (whd_all env c) in if isInd ind && List.is_empty l then let mis = lookup_mind_specif env (fst (destInd ind)) in let nparams = Inductive.inductive_params mis in @@ -233,7 +233,7 @@ let judge_of_apply env funj argjv = { uj_val = mkApp (j_val funj, Array.map j_val argjv); uj_type = typ } | hj::restjl -> - (match kind_of_term (whd_betadeltaiota env typ) with + (match kind_of_term (whd_all env typ) with | Prod (_,c1,c2) -> (try let () = conv_leq false env hj.uj_type c1 in diff --git a/library/impargs.ml b/library/impargs.ml index feb3bf018..52d5c9c91 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -188,7 +188,7 @@ let is_reversible_pattern bound depth f l = (* Precondition: rels in env are for inductive types only *) let add_free_rels_until strict strongly_strict revpat bound env m pos acc = let rec frec rig (env,depth as ed) c = - let hd = if strict then whd_betadeltaiota env c else c in + let hd = if strict then whd_all env c else c in let c = if strongly_strict then hd else c in match kind_of_term hd with | Rel n when (n < bound+depth) && (n >= depth) -> @@ -236,7 +236,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t = let rigid = ref true in let open Context.Rel.Declaration in let rec aux env avoid n names t = - let t = whd_betadeltaiota env t in + let t = whd_all env t in match kind_of_term t with | Prod (na,a,b) -> let na',avoid' = find_displayed_name_in all avoid na (names,b) in @@ -250,7 +250,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t = add_free_rels_until strict strongly_strict revpat n env t Conclusion v else v in - match kind_of_term (whd_betadeltaiota env t) with + match kind_of_term (whd_all env t) with | Prod (na,a,b) -> let na',avoid = find_displayed_name_in all [] na ([],b) in let v = aux (push_rel (LocalAssum (na',a)) env) avoid 1 [na'] b in diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index cb39df8ab..0b01eeef4 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -218,7 +218,7 @@ end) = struct | Some (x, Some rel) -> evars, rel in let rec aux env evars ty l = - let t = Reductionops.whd_betadeltaiota env (goalevars evars) ty in + let t = Reductionops.whd_all env (goalevars evars) ty in match kind_of_term t, l with | Prod (na, ty, b), obj :: cstrs -> let b = Reductionops.nf_betaiota (goalevars evars) b in @@ -321,7 +321,7 @@ end) = struct let rec aux evars env prod n = if Int.equal n 0 then start evars env prod else - match kind_of_term (Reduction.whd_betadeltaiota env prod) with + match kind_of_term (Reduction.whd_all env prod) with | Prod (na, ty, b) -> if noccurn 1 b then let b' = lift (-1) b in @@ -339,7 +339,7 @@ end) = struct try let evars, found = aux evars env ty (succ (List.length args)) in Some (evars, found, c, ty, arg :: args) with Not_found -> - let ty = whd_betadeltaiota env ty in + let ty = whd_all env ty in find env (mkApp (c, [| arg |])) (prod_applist ty [arg]) args in find env c ty args diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index bd788a425..de64368e2 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -42,7 +42,7 @@ let whd env= (fun t -> Closure.whd_val infos (Closure.inject t)) let whd_delta env= - let infos=Closure.create_clos_infos Closure.betadeltaiota env in + let infos=Closure.create_clos_infos Closure.all env in (fun t -> Closure.whd_val infos (Closure.inject t)) (* decompose member of equality in an applicative format *) diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 34307a358..c0ef34305 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -153,7 +153,7 @@ let interp_constr check_sort env sigma c = fst (understand env sigma (fst c)) let special_whd env = - let infos=Closure.create_clos_infos Closure.betadeltaiota env in + let infos=Closure.create_clos_infos Closure.all env in (fun t -> Closure.whd_val infos (Closure.inject t)) let _eq = lazy (Universes.constr_of_global (Coqlib.glob_eq)) diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 836f1982d..b6c34d270 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -84,7 +84,7 @@ let tcl_erase_info gls = tcl_change_info_gen info_gen gls let special_whd gl= - let infos=Closure.create_clos_infos Closure.betadeltaiota (pf_env gl) in + let infos=Closure.create_clos_infos Closure.all (pf_env gl) in (fun t -> Closure.whd_val infos (Closure.inject t)) let special_nf gl= diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 0153348de..4308b4633 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -74,7 +74,7 @@ type flag = info * scheme Really important function. *) let rec flag_of_type env t : flag = - let t = whd_betadeltaiota env none t in + let t = whd_all env none t in match kind_of_term t with | Prod (x,t,c) -> flag_of_type (push_rel (LocalAssum (x,t)) env) c | Sort s when Sorts.is_prop s -> (Logic,TypeScheme) @@ -102,14 +102,14 @@ let is_info_scheme env t = match flag_of_type env t with (*s [type_sign] gernerates a signature aimed at treating a type application. *) let rec type_sign env c = - match kind_of_term (whd_betadeltaiota env none c) with + match kind_of_term (whd_all env none c) with | Prod (n,t,d) -> (if is_info_scheme env t then Keep else Kill Kprop) :: (type_sign (push_rel_assum (n,t) env) d) | _ -> [] let rec type_scheme_nb_args env c = - match kind_of_term (whd_betadeltaiota env none c) with + match kind_of_term (whd_all env none c) with | Prod (n,t,d) -> let n = type_scheme_nb_args (push_rel_assum (n,t) env) d in if is_info_scheme env t then n+1 else n @@ -135,7 +135,7 @@ let make_typvar n vl = next_ident_away id' vl let rec type_sign_vl env c = - match kind_of_term (whd_betadeltaiota env none c) with + match kind_of_term (whd_all env none c) with | Prod (n,t,d) -> let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in if not (is_info_scheme env t) then Kill Kprop::s, vl @@ -143,7 +143,7 @@ let rec type_sign_vl env c = | _ -> [],[] let rec nb_default_params env c = - match kind_of_term (whd_betadeltaiota env none c) with + match kind_of_term (whd_all env none c) with | Prod (n,t,d) -> let n = nb_default_params (push_rel_assum (n,t) env) d in if is_default env t then n+1 else n @@ -489,7 +489,7 @@ and extract_really_ind env kn mib = *) and extract_type_cons env db dbmap c i = - match kind_of_term (whd_betadeltaiota env none c) with + match kind_of_term (whd_all env none c) with | Prod (n,t,d) -> let env' = push_rel_assum (n,t) env in let db' = (try Int.Map.find i dbmap with Not_found -> 0) :: db in diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 81dfa603d..3a9ecc9ff 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -441,7 +441,7 @@ let error_MPfile_as_mod mp b = let argnames_of_global r = let typ = Global.type_of_global_unsafe r in let rels,_ = - decompose_prod (Reduction.whd_betadeltaiota (Global.env ()) typ) in + decompose_prod (Reduction.whd_all (Global.env ()) typ) in List.rev_map fst rels let msg_of_implicit = function @@ -880,7 +880,7 @@ let extract_constant_inline inline r ids s = | ConstRef kn -> let env = Global.env () in let typ = Global.type_of_global_unsafe (ConstRef kn) in - let typ = Reduction.whd_betadeltaiota env typ in + let typ = Reduction.whd_all env typ in if Reduction.is_arity env typ then begin let nargs = Hook.get use_type_scheme_nb_args env typ in diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 5eff2f277..1394f4764 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -107,7 +107,7 @@ let mk_open_instance id idc gl m t= let typ=pf_unsafe_type_of gl idc in (* since we know we will get a product, reduction is not too expensive *) - let (nam,_,_)=destProd (whd_betadeltaiota env evmap typ) in + let (nam,_,_)=destProd (whd_all env evmap typ) in match nam with Name id -> id | Anonymous -> dummy_bvid in diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 52094cf08..146749d32 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 diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 0a0b45915..bb9266db1 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -67,7 +67,7 @@ let l_D_Or = lazy (constant "D_Or") let special_whd gl= - let infos=Closure.create_clos_infos Closure.betadeltaiota (pf_env gl) in + let infos=Closure.create_clos_infos Closure.all (pf_env gl) in (fun t -> Closure.whd_val infos (Closure.inject t)) let special_nf gl= diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 55241ab2b..a6744916a 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -82,7 +82,7 @@ let lookup_map map = errorlabstrm"lookup_map"(str"map "++qs map++str"not found") let protect_red map env sigma c = - kl (create_clos_infos betadeltaiota env) + kl (create_clos_infos all env) (mk_clos_but (lookup_map map c) (Esubst.subs_id 0) c);; let protect_tac map = diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 78c218a50..c39a57012 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1708,7 +1708,7 @@ let build_inversion_problem loc env sigma tms t = let id = next_name_away (named_hd env t Anonymous) avoid in PatVar (Loc.ghost,Name id), ((id,t)::subst, id::avoid) in let rec reveal_pattern t (subst,avoid as acc) = - match kind_of_term (whd_betadeltaiota env sigma t) with + match kind_of_term (whd_all env sigma t) with | Construct (cstr,u) -> PatCstr (Loc.ghost,cstr,[],Anonymous), acc | App (f,v) when isConstruct f -> let cstr,u = destConstruct f in diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index afd86420e..132147487 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -156,7 +156,7 @@ let strip_appl head stack = (* Tests if fixpoint reduction is possible. *) let fixp_reducible flgs ((reci,i),_) stk = - if red_set flgs fIOTA then + if red_set flgs fFIX then match stk with | APP(appl,_) -> Array.length appl > reci.(i) && @@ -168,7 +168,7 @@ let fixp_reducible flgs ((reci,i),_) stk = false let cofixp_reducible flgs _ stk = - if red_set flgs fIOTA then + if red_set flgs fCOFIX then match stk with | (CASE _ | APP(_,CASE _)) -> true | _ -> false @@ -296,19 +296,19 @@ and cbv_stack_value info env = function (* constructor in a Case -> IOTA *) | (CONSTR(((sp,n),u),[||]), APP(args,CASE(_,br,ci,env,stk))) - when red_set (info_flags info) fIOTA -> + when red_set (info_flags info) fMATCH -> let cargs = Array.sub args ci.ci_npar (Array.length args - ci.ci_npar) in cbv_stack_term info (stack_app cargs stk) env br.(n-1) (* constructor of arity 0 in a Case -> IOTA *) | (CONSTR(((_,n),u),[||]), CASE(_,br,_,env,stk)) - when red_set (info_flags info) fIOTA -> + when red_set (info_flags info) fMATCH -> cbv_stack_term info stk env br.(n-1) (* constructor in a Projection -> IOTA *) | (CONSTR(((sp,n),u),[||]), APP(args,PROJ(p,pi,stk))) - when red_set (info_flags info) fIOTA && Projection.unfolded p -> + when red_set (info_flags info) fMATCH && Projection.unfolded p -> let arg = args.(pi.Declarations.proj_npars + pi.Declarations.proj_arg) in cbv_stack_value info env (strip_appl arg stk) diff --git a/pretyping/classops.ml b/pretyping/classops.ml index d3d4201f5..5fb6c130e 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -297,7 +297,7 @@ let lookup_path_to_sort_from env sigma s = let get_coercion_constructor env coe = let c, _ = - Reductionops.whd_betadeltaiota_stack env Evd.empty coe.coe_value + Reductionops.whd_all_stack env Evd.empty coe.coe_value in match kind_of_term c with | Construct (cstr,u) -> diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 65d79bcc8..704559dd7 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -63,7 +63,7 @@ let apply_coercion_args env evd check isproj argl funj = { uj_val = applist (j_val funj,argl); uj_type = typ } | h::restl -> (* On devrait pouvoir s'arranger pour qu'on n'ait pas a faire hnf_constr *) - match kind_of_term (whd_betadeltaiota env evd typ) with + match kind_of_term (whd_all env evd typ) with | Prod (_,c1,c2) -> if check && not (e_cumul env evdref (Retyping.get_type_of env evd h) c1) then raise NoCoercion; @@ -116,7 +116,7 @@ let disc_subset x = exception NoSubtacCoercion -let hnf env evd c = whd_betadeltaiota env evd c +let hnf env evd c = whd_all env evd c let hnf_nodelta env evd c = whd_betaiota evd c let lift_args n sign = @@ -374,7 +374,7 @@ let apply_coercion env sigma p hj typ_cl = (* Try to coerce to a funclass; raise NoCoercion if not possible *) let inh_app_fun_core env evd j = - let t = whd_betadeltaiota env evd j.uj_type in + let t = whd_all env evd j.uj_type in match kind_of_term t with | Prod (_,_,_) -> (evd,j) | Evar ev -> @@ -415,7 +415,7 @@ let inh_tosort_force loc env evd j = error_not_a_type_loc loc env evd j let inh_coerce_to_sort loc env evd j = - let typ = whd_betadeltaiota env evd j.uj_type in + let typ = whd_all env evd j.uj_type in match kind_of_term typ with | Sort s -> (evd,{ utj_val = j.uj_val; utj_type = s }) | Evar ev when not (is_defined evd (fst ev)) -> @@ -467,8 +467,8 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 = try inh_coerce_to_fail env evd rigidonly v t c1 with NoCoercion -> match - kind_of_term (whd_betadeltaiota env evd t), - kind_of_term (whd_betadeltaiota env evd c1) + kind_of_term (whd_all env evd t), + kind_of_term (whd_all env evd c1) with | Prod (name,t1,t2), Prod (_,u1,u2) -> (* Conversion did not work, we may succeed with a coercion. *) diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index d349cf821..f9ab75cea 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -78,7 +78,7 @@ let define_pure_evar_as_product evd evk = let evi = Evd.find_undefined evd evk in let evenv = evar_env evi in let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in - let concl = Reductionops.whd_betadeltaiota evenv evd evi.evar_concl in + let concl = Reductionops.whd_all evenv evd evi.evar_concl in let s = destSort concl in let evd1,(dom,u1) = let evd = Sigma.Unsafe.of_evar_map evd in @@ -131,7 +131,7 @@ let define_pure_evar_as_lambda env evd evk = let open Context.Named.Declaration in let evi = Evd.find_undefined evd evk in let evenv = evar_env evi in - let typ = Reductionops.whd_betadeltaiota evenv evd (evar_concl evi) in + let typ = Reductionops.whd_all evenv evd (evar_concl evi) in let evd1,(na,dom,rng) = match kind_of_term typ with | Prod (na,dom,rng) -> (evd,(na,dom,rng)) | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd typ @@ -169,7 +169,7 @@ let define_evar_as_sort env evd (ev,args) = let evd, u = new_univ_variable univ_rigid evd in let evi = Evd.find_undefined evd ev in let s = Type u in - let concl = Reductionops.whd_betadeltaiota (evar_env evi) evd evi.evar_concl in + let concl = Reductionops.whd_all (evar_env evi) evd evi.evar_concl in let sort = destSort concl in let evd' = Evd.define ev (mkSort s) evd in Evd.set_leq_sort env evd' (Type (Univ.super u)) sort, s @@ -181,10 +181,10 @@ let define_evar_as_sort env evd (ev,args) = let split_tycon loc env evd tycon = let rec real_split evd c = - let t = Reductionops.whd_betadeltaiota env evd c in + let t = Reductionops.whd_all env evd c in match kind_of_term t with | Prod (na,dom,rng) -> evd, (na, dom, rng) - | Evar ev (* ev is undefined because of whd_betadeltaiota *) -> + | Evar ev (* ev is undefined because of whd_all *) -> let (evd',prod) = define_evar_as_product evd ev in let (_,dom,rng) = destProd prod in evd',(Anonymous, dom, rng) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 455a7dbd6..77b0c67ad 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -140,7 +140,7 @@ let recheck_applications conv_algo env evdref t = let argsty = Array.map (fun x -> aux env x; Retyping.get_type_of env !evdref x) args in let rec aux i ty = if i < Array.length argsty then - match kind_of_term (whd_betadeltaiota env !evdref ty) with + match kind_of_term (whd_all env !evdref ty) with | Prod (na, dom, codom) -> (match conv_algo env !evdref Reduction.CUMUL argsty.(i) dom with | Success evd -> evdref := evd; @@ -520,7 +520,7 @@ let solve_pattern_eqn env l c = l c in (* Warning: we may miss some opportunity to eta-reduce more since c' is not in normal form *) - whd_eta c' + shrink_eta c' (*****************************************) (* Refining/solving unification problems *) @@ -797,7 +797,7 @@ let rec do_projection_effects define_fun env ty evd = function let evd = Evd.define evk (mkVar id) evd in (* TODO: simplify constraints involving evk *) let evd = do_projection_effects define_fun env ty evd p in - let ty = whd_betadeltaiota env evd (Lazy.force ty) in + let ty = whd_all env evd (Lazy.force ty) in if not (isSort ty) then (* Don't try to instantiate if a sort because if evar_concl is an evar it may commit to a univ level which is not the right @@ -1553,7 +1553,7 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs = raise e | OccurCheckIn (evd,rhs) -> (* last chance: rhs actually reduces to ev *) - let c = whd_betadeltaiota env evd rhs in + let c = whd_all env evd rhs in match kind_of_term c with | Evar (evk',argsv2) when Evar.equal evk evk' -> solve_refl (fun env sigma pb c c' -> is_fconv pb env sigma c c') diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index fc38e98c6..866b2b495 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -151,7 +151,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = let nparams = List.length vargs in let process_pos env depK pk = let rec prec env i sign p = - let p',largs = whd_betadeltaiota_nolet_stack env sigma p in + let p',largs = whd_allnolet_stack env sigma p in match kind_of_term p' with | Prod (n,t,c) -> let d = LocalAssum (n,t) in @@ -168,7 +168,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = else base | _ -> - let t' = whd_betadeltaiota env sigma p in + let t' = whd_all env sigma p in if Term.eq_constr p' t' then assert false else prec env i sign t' in @@ -227,7 +227,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = let process_pos env fk = let rec prec env i hyps p = - let p',largs = whd_betadeltaiota_nolet_stack env sigma p in + let p',largs = whd_allnolet_stack env sigma p in match kind_of_term p' with | Prod (n,t,c) -> let d = LocalAssum (n,t) in @@ -240,7 +240,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = and arg = appvect (mkRel (i+1), Context.Rel.to_extended_vect 0 hyps) in applist(lift i fk,realargs@[arg]) | _ -> - let t' = whd_betadeltaiota env sigma p in + let t' = whd_all env sigma p in if Term.eq_constr t' p' then assert false else prec env i hyps t' in diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 403dcfd1a..6be6a2d3a 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -417,7 +417,7 @@ let extract_mrectype t = | _ -> raise Not_found let find_mrectype_vect env sigma c = - let (t, l) = decompose_appvect (whd_betadeltaiota env sigma c) in + let (t, l) = decompose_appvect (whd_all env sigma c) in match kind_of_term t with | Ind ind -> (ind, l) | _ -> raise Not_found @@ -426,7 +426,7 @@ let find_mrectype env sigma c = let (ind, v) = find_mrectype_vect env sigma c in (ind, Array.to_list v) let find_rectype env sigma c = - let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in + let (t, l) = decompose_app (whd_all env sigma c) in match kind_of_term t with | Ind (ind,u as indu) -> let (mib,mip) = Inductive.lookup_mind_specif env ind in @@ -436,7 +436,7 @@ let find_rectype env sigma c = | _ -> raise Not_found let find_inductive env sigma c = - let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in + let (t, l) = decompose_app (whd_all env sigma c) in match kind_of_term t with | Ind ind when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite <> Decl_kinds.CoFinite -> @@ -444,7 +444,7 @@ let find_inductive env sigma c = | _ -> raise Not_found let find_coinductive env sigma c = - let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in + let (t, l) = decompose_app (whd_all env sigma c) in match kind_of_term t with | Ind ind when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite == Decl_kinds.CoFinite -> @@ -458,7 +458,7 @@ let find_coinductive env sigma c = let is_predicate_explicitly_dep env pred arsign = let rec srec env pval arsign = - let pv' = whd_betadeltaiota env Evd.empty pval in + let pv' = whd_all env Evd.empty pval in match kind_of_term pv', arsign with | Lambda (na,t,b), (LocalAssum _)::arsign -> srec (push_rel_assum (na,t) env) b arsign diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 2a5e99965..e537a3c0a 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -35,13 +35,13 @@ let invert_tag cst tag reloc_tbl = with Find_at j -> (j+1) let decompose_prod env t = - let (name,dom,codom as res) = destProd (whd_betadeltaiota env t) in + let (name,dom,codom as res) = destProd (whd_all env t) in match name with | Anonymous -> (Name (id_of_string "x"),dom,codom) | _ -> res let app_type env c = - let t = whd_betadeltaiota env c in + let t = whd_all env c in try destApp t with DestKO -> (t,[||]) @@ -289,7 +289,7 @@ and nf_atom_type env atom = let pT = hnf_prod_applist env (Inductiveops.type_of_inductive env ind) (Array.to_list params) in - let pT = whd_betadeltaiota env pT in + let pT = whd_all env pT in let dep, p = nf_predicate env ind mip params p pT in (* Calcul du type des branches *) let btypes = build_branches_type env (fst ind) mib mip u params dep p in diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index b6a57785a..38defe951 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -675,7 +675,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ | c::rest -> let argloc = loc_of_glob_constr c in let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env) evdref resj in - let resty = whd_betadeltaiota env !evdref resj.uj_type in + let resty = whd_all env !evdref resj.uj_type in match kind_of_term resty with | Prod (na,c1,c2) -> let tycon = Some c1 in @@ -1017,7 +1017,7 @@ and pretype_type k0 resolve_tc valcon env evdref lvar = function let s = let sigma = !evdref in let t = Retyping.get_type_of env sigma v in - match kind_of_term (whd_betadeltaiota env sigma t) with + match kind_of_term (whd_all env sigma t) with | Sort s -> s | Evar ev when is_Type (existential_type sigma ev) -> evd_comb1 (define_evar_as_sort env) evdref ev diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 2959bd7c8..95c6725f3 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -326,7 +326,7 @@ let is_open_canonical_projection env sigma (c,args) = (** Check if there is some canonical projection attached to this structure *) let _ = Refmap.find ref !object_table in try - let arg = whd_betadeltaiota env sigma (Stack.nth args n) in + let arg = whd_all env sigma (Stack.nth args n) in let hd = match kind_of_term arg with App (hd, _) -> hd | _ -> arg in not (isConstruct hd) with Failure _ -> false diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 79cb7a2f6..3f89acf33 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -619,23 +619,7 @@ let rec strong_prodspine redfun sigma c = (*** Reduction using bindingss ***) (*************************************) -(* Local *) -let nored = Closure.RedFlags.no_red -let beta = Closure.beta let eta = Closure.RedFlags.mkflags [Closure.RedFlags.fETA] -let zeta = Closure.RedFlags.mkflags [Closure.RedFlags.fZETA] -let betaiota = Closure.betaiota -let betaiotazeta = Closure.betaiotazeta - -(* Contextual *) -let delta = Closure.RedFlags.mkflags [Closure.RedFlags.fDELTA] -let betalet = Closure.RedFlags.mkflags [Closure.RedFlags.fBETA;Closure.RedFlags.fZETA] -let betaetalet = Closure.RedFlags.red_add betalet Closure.RedFlags.fETA -let betadelta = Closure.RedFlags.red_add betalet Closure.RedFlags.fDELTA -let betadeltaeta = Closure.RedFlags.red_add betadelta Closure.RedFlags.fETA -let betadeltaiota = Closure.RedFlags.red_add betadelta Closure.RedFlags.fIOTA -let betadeltaiota_nolet = Closure.betadeltaiotanolet -let betadeltaiotaeta = Closure.RedFlags.red_add betadeltaiota Closure.RedFlags.fETA (* Beta Reduction tools *) @@ -950,13 +934,15 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = whrec Cst_stack.empty (arg, Stack.Fix(f,bef,cst_l)::s')) | Construct ((ind,c),u) -> - if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then + let use_match = Closure.RedFlags.red_set flags Closure.RedFlags.fMATCH in + let use_fix = Closure.RedFlags.red_set flags Closure.RedFlags.fFIX in + if use_match || use_fix then match Stack.strip_app stack with - |args, (Stack.Case(ci, _, lf,_)::s') -> + |args, (Stack.Case(ci, _, lf,_)::s') when use_match -> whrec Cst_stack.empty (lf.(c-1), (Stack.tail ci.ci_npar args) @ s') - |args, (Stack.Proj (n,m,p,_)::s') -> + |args, (Stack.Proj (n,m,p,_)::s') when use_match -> whrec Cst_stack.empty (Stack.nth args (n+m), s') - |args, (Stack.Fix (f,s',cst_l)::s'') -> + |args, (Stack.Fix (f,s',cst_l)::s'') when use_fix -> let x' = Stack.zip(x,args) in let out_sk = s' @ (Stack.append_app [|x'|] s'') in reduce_and_refold_fix whrec env cst_l f out_sk @@ -988,11 +974,11 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = Stack.Cst (const,next,remains',s' @ (Stack.append_app [|x'|] bef),cst_l) :: s''') end |_, (Stack.App _|Stack.Update _|Stack.Shift _)::_ -> assert false - |_, [] -> fold () + |_, _ -> fold () else fold () | CoFix cofix -> - if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then + if Closure.RedFlags.red_set flags Closure.RedFlags.fCOFIX then match Stack.strip_app stack with |args, ((Stack.Case _ |Stack.Proj _)::s') -> reduce_and_refold_cofix whrec env cst_l cofix stack @@ -1059,21 +1045,23 @@ let local_whd_state_gen flags sigma = | None -> s) | Construct ((ind,c),u) -> - if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then + let use_match = Closure.RedFlags.red_set flags Closure.RedFlags.fMATCH in + let use_fix = Closure.RedFlags.red_set flags Closure.RedFlags.fFIX in + if use_match || use_fix then match Stack.strip_app stack with - |args, (Stack.Case(ci, _, lf,_)::s') -> + |args, (Stack.Case(ci, _, lf,_)::s') when use_match -> whrec (lf.(c-1), (Stack.tail ci.ci_npar args) @ s') - |args, (Stack.Proj (n,m,p,_) :: s') -> + |args, (Stack.Proj (n,m,p,_) :: s') when use_match -> whrec (Stack.nth args (n+m), s') - |args, (Stack.Fix (f,s',cst)::s'') -> + |args, (Stack.Fix (f,s',cst)::s'') when use_fix -> let x' = Stack.zip(x,args) in whrec (contract_fix f, s' @ (Stack.append_app [|x'|] s'')) |_, (Stack.App _|Stack.Update _|Stack.Shift _|Stack.Cst _)::_ -> assert false - |_, [] -> s + |_, _ -> s else s | CoFix cofix -> - if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then + if Closure.RedFlags.red_set flags Closure.RedFlags.fCOFIX then match Stack.strip_app stack with |args, ((Stack.Case _ | Stack.Proj _)::s') -> whrec (contract_cofix cofix, stack) @@ -1105,79 +1093,62 @@ let red_of_state_red f sigma x = (* 0. No Reduction Functions *) -let whd_nored_state = local_whd_state_gen nored +let whd_nored_state = local_whd_state_gen Closure.nored let whd_nored_stack = stack_red_of_state_red whd_nored_state let whd_nored = red_of_state_red whd_nored_state (* 1. Beta Reduction Functions *) -let whd_beta_state = local_whd_state_gen beta +let whd_beta_state = local_whd_state_gen Closure.beta let whd_beta_stack = stack_red_of_state_red whd_beta_state let whd_beta = red_of_state_red whd_beta_state -(* Nouveau ! *) -let whd_betaetalet_state = local_whd_state_gen betaetalet -let whd_betaetalet_stack = stack_red_of_state_red whd_betaetalet_state -let whd_betaetalet = red_of_state_red whd_betaetalet_state - -let whd_betalet_state = local_whd_state_gen betalet +let whd_betalet_state = local_whd_state_gen Closure.betazeta let whd_betalet_stack = stack_red_of_state_red whd_betalet_state let whd_betalet = red_of_state_red whd_betalet_state (* 2. Delta Reduction Functions *) -let whd_delta_state e = raw_whd_state_gen delta e +let whd_delta_state e = raw_whd_state_gen Closure.delta e let whd_delta_stack env = stack_red_of_state_red (whd_delta_state env) let whd_delta env = red_of_state_red (whd_delta_state env) -let whd_betadelta_state e = raw_whd_state_gen betadelta e -let whd_betadelta_stack env = - stack_red_of_state_red (whd_betadelta_state env) -let whd_betadelta env = - red_of_state_red (whd_betadelta_state env) - +let whd_betadeltazeta_state e = raw_whd_state_gen Closure.betadeltazeta e +let whd_betadeltazeta_stack env = + stack_red_of_state_red (whd_betadeltazeta_state env) +let whd_betadeltazeta env = + red_of_state_red (whd_betadeltazeta_state env) -let whd_betadeltaeta_state e = raw_whd_state_gen betadeltaeta e -let whd_betadeltaeta_stack env = - stack_red_of_state_red (whd_betadeltaeta_state env) -let whd_betadeltaeta env = - red_of_state_red (whd_betadeltaeta_state env) (* 3. Iota reduction Functions *) -let whd_betaiota_state = local_whd_state_gen betaiota +let whd_betaiota_state = local_whd_state_gen Closure.betaiota let whd_betaiota_stack = stack_red_of_state_red whd_betaiota_state let whd_betaiota = red_of_state_red whd_betaiota_state -let whd_betaiotazeta_state = local_whd_state_gen betaiotazeta +let whd_betaiotazeta_state = local_whd_state_gen Closure.betaiotazeta let whd_betaiotazeta_stack = stack_red_of_state_red whd_betaiotazeta_state let whd_betaiotazeta = red_of_state_red whd_betaiotazeta_state -let whd_betadeltaiota_state env = raw_whd_state_gen betadeltaiota env -let whd_betadeltaiota_stack env = - stack_red_of_state_red (whd_betadeltaiota_state env) -let whd_betadeltaiota env = - red_of_state_red (whd_betadeltaiota_state env) - -let whd_betadeltaiotaeta_state env = raw_whd_state_gen betadeltaiotaeta env -let whd_betadeltaiotaeta_stack env = - stack_red_of_state_red (whd_betadeltaiotaeta_state env) -let whd_betadeltaiotaeta env = - red_of_state_red (whd_betadeltaiotaeta_state env) +let whd_all_state env = raw_whd_state_gen Closure.all env +let whd_all_stack env = + stack_red_of_state_red (whd_all_state env) +let whd_all env = + red_of_state_red (whd_all_state env) -let whd_betadeltaiota_nolet_state env = raw_whd_state_gen betadeltaiota_nolet env -let whd_betadeltaiota_nolet_stack env = - stack_red_of_state_red (whd_betadeltaiota_nolet_state env) -let whd_betadeltaiota_nolet env = - red_of_state_red (whd_betadeltaiota_nolet_state env) +let whd_allnolet_state env = raw_whd_state_gen Closure.allnolet env +let whd_allnolet_stack env = + stack_red_of_state_red (whd_allnolet_state env) +let whd_allnolet env = + red_of_state_red (whd_allnolet_state env) -(* 4. Eta reduction Functions *) +(* 4. Ad-hoc eta reduction, does not subsitute evars *) -let whd_eta c = Stack.zip (local_whd_state_gen eta Evd.empty (c,Stack.empty)) +let shrink_eta c = Stack.zip (local_whd_state_gen eta Evd.empty (c,Stack.empty)) (* 5. Zeta Reduction Functions *) -let whd_zeta c = Stack.zip (local_whd_state_gen zeta Evd.empty (c,Stack.empty)) +let whd_zeta c = Stack.zip (local_whd_state_gen Closure.zeta Evd.empty (c,Stack.empty)) (****************************************************************************) (* Reduction Functions *) @@ -1201,8 +1172,8 @@ let clos_norm_flags flgs env sigma t = let nf_beta = clos_norm_flags Closure.beta (Global.env ()) let nf_betaiota = clos_norm_flags Closure.betaiota (Global.env ()) let nf_betaiotazeta = clos_norm_flags Closure.betaiotazeta (Global.env ()) -let nf_betadeltaiota env sigma = - clos_norm_flags Closure.betadeltaiota env sigma +let nf_all env sigma = + clos_norm_flags Closure.all env sigma (********************************************************************) @@ -1397,7 +1368,7 @@ let instance sigma s c = * error message. *) let hnf_prod_app env sigma t n = - match kind_of_term (whd_betadeltaiota env sigma t) with + match kind_of_term (whd_all env sigma t) with | Prod (_,_,b) -> subst1 n b | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product") @@ -1408,7 +1379,7 @@ let hnf_prod_applist env sigma t nl = List.fold_left (hnf_prod_app env sigma) t nl let hnf_lam_app env sigma t n = - match kind_of_term (whd_betadeltaiota env sigma t) with + match kind_of_term (whd_all env sigma t) with | Lambda (_,_,b) -> subst1 n b | _ -> anomaly ~label:"hnf_lam_app" (Pp.str "Need an abstraction") @@ -1420,7 +1391,7 @@ let hnf_lam_applist env sigma t nl = let splay_prod env sigma = let rec decrec env m c = - let t = whd_betadeltaiota env sigma c in + let t = whd_all env sigma c in match kind_of_term t with | Prod (n,a,c0) -> decrec (push_rel (LocalAssum (n,a)) env) @@ -1431,7 +1402,7 @@ let splay_prod env sigma = let splay_lam env sigma = let rec decrec env m c = - let t = whd_betadeltaiota env sigma c in + let t = whd_all env sigma c in match kind_of_term t with | Lambda (n,a,c0) -> decrec (push_rel (LocalAssum (n,a)) env) @@ -1442,7 +1413,7 @@ let splay_lam env sigma = let splay_prod_assum env sigma = let rec prodec_rec env l c = - let t = whd_betadeltaiota_nolet env sigma c in + let t = whd_allnolet env sigma c in match kind_of_term t with | Prod (x,t,c) -> prodec_rec (push_rel (LocalAssum (x,t)) env) @@ -1452,7 +1423,7 @@ let splay_prod_assum env sigma = (Context.Rel.add (LocalDef (x,b,t)) l) c | Cast (c,_,_) -> prodec_rec env l c | _ -> - let t' = whd_betadeltaiota env sigma t in + let t' = whd_all env sigma t in if Term.eq_constr t t' then l,t else prodec_rec env l t' in @@ -1468,7 +1439,7 @@ let sort_of_arity env sigma c = snd (splay_arity env sigma c) let splay_prod_n env sigma n = let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else - match kind_of_term (whd_betadeltaiota env sigma c) with + match kind_of_term (whd_all env sigma c) with | Prod (n,a,c0) -> decrec (push_rel (LocalAssum (n,a)) env) (m-1) (Context.Rel.add (LocalAssum (n,a)) ln) c0 @@ -1478,7 +1449,7 @@ let splay_prod_n env sigma n = let splay_lam_n env sigma n = let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else - match kind_of_term (whd_betadeltaiota env sigma c) with + match kind_of_term (whd_all env sigma c) with | Lambda (n,a,c0) -> decrec (push_rel (LocalAssum (n,a)) env) (m-1) (Context.Rel.add (LocalAssum (n,a)) ln) c0 @@ -1487,7 +1458,7 @@ let splay_lam_n env sigma n = decrec env n Context.Rel.empty let is_sort env sigma t = - match kind_of_term (whd_betadeltaiota env sigma t) with + match kind_of_term (whd_all env sigma t) with | Sort s -> true | _ -> false @@ -1496,19 +1467,19 @@ let is_sort env sigma t = let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s = let rec whrec csts s = - let (t, stack as s),csts' = whd_state_gen ~csts false betaiota env sigma s in + let (t, stack as s),csts' = whd_state_gen ~csts false Closure.betaiota env sigma s in match Stack.strip_app stack with |args, (Stack.Case _ :: _ as stack') -> let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false - (Closure.RedFlags.red_add_transparent betadeltaiota ts) env sigma (t,args) in + (Closure.RedFlags.red_add_transparent Closure.all ts) env sigma (t,args) in if reducible_mind_case t_o then whrec csts_o (t_o, stack_o@stack') else s,csts' |args, (Stack.Fix _ :: _ as stack') -> let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false - (Closure.RedFlags.red_add_transparent betadeltaiota ts) env sigma (t,args) in + (Closure.RedFlags.red_add_transparent Closure.all ts) env sigma (t,args) in if isConstruct t_o then whrec csts_o (t_o, stack_o@stack') else s,csts' |args, (Stack.Proj (n,m,p,_) :: stack'') -> let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false - (Closure.RedFlags.red_add_transparent betadeltaiota ts) env sigma (t,args) in + (Closure.RedFlags.red_add_transparent Closure.all ts) env sigma (t,args) in if isConstruct t_o then whrec Cst_stack.empty (Stack.nth stack_o (n+m), stack'') else s,csts' @@ -1517,7 +1488,7 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s = let find_conclusion env sigma = let rec decrec env c = - let t = whd_betadeltaiota env sigma c in + let t = whd_all env sigma c in match kind_of_term t with | Prod (x,t,c0) -> decrec (push_rel (LocalAssum (x,t)) env) c0 | Lambda (x,t,c0) -> decrec (push_rel (LocalAssum (x,t)) env) c0 diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index b38252e97..e7a6b3d64 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -148,7 +148,7 @@ val clos_norm_flags : Closure.RedFlags.reds -> reduction_function val nf_beta : local_reduction_function val nf_betaiota : local_reduction_function val nf_betaiotazeta : local_reduction_function -val nf_betadeltaiota : reduction_function +val nf_all : reduction_function val nf_evar : evar_map -> constr -> constr (** Lazy strategy, weak head reduction *) @@ -158,9 +158,8 @@ val whd_nored : local_reduction_function val whd_beta : local_reduction_function val whd_betaiota : local_reduction_function val whd_betaiotazeta : local_reduction_function -val whd_betadeltaiota : contextual_reduction_function -val whd_betadeltaiota_nolet : contextual_reduction_function -val whd_betaetalet : local_reduction_function +val whd_all : contextual_reduction_function +val whd_allnolet : contextual_reduction_function val whd_betalet : local_reduction_function (** Removes cast and put into applicative form *) @@ -168,18 +167,16 @@ val whd_nored_stack : local_stack_reduction_function val whd_beta_stack : local_stack_reduction_function val whd_betaiota_stack : local_stack_reduction_function val whd_betaiotazeta_stack : local_stack_reduction_function -val whd_betadeltaiota_stack : contextual_stack_reduction_function -val whd_betadeltaiota_nolet_stack : contextual_stack_reduction_function -val whd_betaetalet_stack : local_stack_reduction_function +val whd_all_stack : contextual_stack_reduction_function +val whd_allnolet_stack : contextual_stack_reduction_function val whd_betalet_stack : local_stack_reduction_function val whd_nored_state : local_state_reduction_function val whd_beta_state : local_state_reduction_function val whd_betaiota_state : local_state_reduction_function val whd_betaiotazeta_state : local_state_reduction_function -val whd_betadeltaiota_state : contextual_state_reduction_function -val whd_betadeltaiota_nolet_state : contextual_state_reduction_function -val whd_betaetalet_state : local_state_reduction_function +val whd_all_state : contextual_state_reduction_function +val whd_allnolet_state : contextual_state_reduction_function val whd_betalet_state : local_state_reduction_function (** {6 Head normal forms } *) @@ -187,17 +184,11 @@ val whd_betalet_state : local_state_reduction_function val whd_delta_stack : stack_reduction_function val whd_delta_state : state_reduction_function val whd_delta : reduction_function -val whd_betadelta_stack : stack_reduction_function -val whd_betadelta_state : state_reduction_function -val whd_betadelta : reduction_function -val whd_betadeltaeta_stack : stack_reduction_function -val whd_betadeltaeta_state : state_reduction_function -val whd_betadeltaeta : reduction_function -val whd_betadeltaiotaeta_stack : stack_reduction_function -val whd_betadeltaiotaeta_state : state_reduction_function -val whd_betadeltaiotaeta : reduction_function - -val whd_eta : constr -> constr +val whd_betadeltazeta_stack : stack_reduction_function +val whd_betadeltazeta_state : state_reduction_function +val whd_betadeltazeta : reduction_function + +val shrink_eta : constr -> constr val whd_zeta : constr -> constr (** Various reduction functions *) diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 1a6f7832a..5de540a00 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -62,7 +62,7 @@ let get_type_from_constraints env sigma t = let rec subst_type env sigma typ = function | [] -> typ | h::rest -> - match kind_of_term (whd_betadeltaiota env sigma typ) with + match kind_of_term (whd_all env sigma typ) with | Prod (na,c1,c2) -> subst_type env sigma (subst1 h c2) rest | _ -> retype_error NonFunctionalConstruction @@ -71,7 +71,7 @@ let rec subst_type env sigma typ = function let sort_of_atomic_type env sigma ft args = let rec concl_of_arity env n ar args = - match kind_of_term (whd_betadeltaiota env sigma ar), args with + match kind_of_term (whd_all env sigma ar), args with | Prod (na, t, b), h::l -> concl_of_arity (push_rel (LocalDef (na, lift n h, t)) env) (n + 1) b l | Sort s, [] -> s | _ -> retype_error NotASort @@ -83,7 +83,7 @@ let type_of_var env id = with Not_found -> retype_error (BadVariable id) let decomp_sort env sigma t = - match kind_of_term (whd_betadeltaiota env sigma t) with + match kind_of_term (whd_all env sigma t) with | Sort s -> s | _ -> retype_error NotASort @@ -113,7 +113,7 @@ let retype ?(polyprop=true) sigma = in let n = inductive_nrealdecls_env env (fst (fst (dest_ind_family indf))) in let t = betazetaevar_applist sigma n p realargs in - (match kind_of_term (whd_betadeltaiota env sigma (type_of env t)) with + (match kind_of_term (whd_all env sigma (type_of env t)) with | Prod _ -> whd_beta sigma (applist (t, [c])) | _ -> t) | Lambda (name,c1,c2) -> diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 7d2504004..51a89966f 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -257,7 +257,7 @@ let invert_name labs l na0 env sigma ref = function let compute_consteval_direct env sigma ref = let rec srec env n labs onlyproj c = - let c',l = whd_betadelta_stack env sigma c in + let c',l = whd_betadeltazeta_stack env sigma c in match kind_of_term c' with | Lambda (id,t,g) when List.is_empty l && not onlyproj -> let open Context.Rel.Declaration in @@ -870,7 +870,7 @@ let red_product env sigma c = *) let whd_simpl_orelse_delta_but_fix_old env sigma c = - let whd_all = whd_betadeltaiota_state env sigma in + let whd_all = whd_all_state env sigma in let rec redrec (x, stack as s) = match kind_of_term x with | Lambda (na,t,c) -> @@ -1125,7 +1125,7 @@ let cbv_norm_flags flags env sigma t = let cbv_beta = cbv_norm_flags beta empty_env let cbv_betaiota = cbv_norm_flags betaiota empty_env -let cbv_betadeltaiota env sigma = cbv_norm_flags betadeltaiota env sigma +let cbv_betadeltaiota env sigma = cbv_norm_flags all env sigma let compute = cbv_betadeltaiota @@ -1186,7 +1186,7 @@ let reduce_to_ind_gen allow_product env sigma t = | _ -> (* Last chance: we allow to bypass the Opaque flag (as it was partially the case between V5.10 and V8.1 *) - let t' = whd_betadeltaiota env sigma t in + let t' = whd_all env sigma t in match kind_of_term (fst (decompose_app t')) with | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t' l) | _ -> errorlabstrm "" (str"Not an inductive product.") diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 52afa7f83..8e44fb008 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -36,7 +36,7 @@ let inductive_type_knowing_parameters env (ind,u) jl = Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp let e_type_judgment env evdref j = - match kind_of_term (whd_betadeltaiota env !evdref j.uj_type) with + match kind_of_term (whd_all env !evdref j.uj_type) with | Sort s -> {utj_val = j.uj_val; utj_type = s } | Evar ev -> let (evd,s) = Evardefine.define_evar_as_sort env !evdref ev in @@ -54,7 +54,7 @@ let e_judge_of_apply env evdref funj argjv = { uj_val = mkApp (j_val funj, Array.map j_val argjv); uj_type = typ } | hj::restjl -> - match kind_of_term (whd_betadeltaiota env !evdref typ) with + match kind_of_term (whd_all env !evdref typ) with | Prod (_,c1,c2) -> if Evarconv.e_cumul env evdref hj.uj_type c1 then apply_rec (n+1) (subst1 hj.uj_val c2) restjl @@ -87,7 +87,7 @@ let e_is_correct_arity env evdref c pj ind specif params = let allowed_sorts = elim_sorts specif in let error () = error_elim_arity env ind allowed_sorts c pj None in let rec srec env pt ar = - let pt' = whd_betadeltaiota env !evdref pt in + let pt' = whd_all env !evdref pt in match kind_of_term pt', ar with | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' -> if not (Evarconv.e_cumul env evdref a1 a1') then error (); diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 21cf5548f..5bb853b69 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1090,7 +1090,7 @@ let left = true let right = false let rec unify_with_eta keptside flags env sigma c1 c2 = -(* Question: try whd_betadeltaiota on ci if not two lambdas? *) +(* Question: try whd_all on ci if not two lambdas? *) match kind_of_term c1, kind_of_term c2 with | (Lambda (na,t1,c1'), Lambda (_,t2,c2')) -> let env' = push_rel_assum (na,t1) env in @@ -1200,7 +1200,7 @@ let applyHead env (type r) (evd : r Sigma.t) n c = if Int.equal n 0 then Sigma (c, evd, p) else - match kind_of_term (whd_betadeltaiota env (Sigma.to_evar_map evd) cty) with + match kind_of_term (whd_all env (Sigma.to_evar_map evd) cty) with | Prod (_,c1,c2) -> let Sigma (evar, evd', q) = Evarutil.new_evar env evd ~src:(Loc.ghost,Evar_kinds.GoalEvar) c1 in apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) (p +> q) evd' @@ -1343,7 +1343,7 @@ let w_merge env with_types flags (evd,metas,evars) = else let evd' = if occur_meta_evd evd mv c then - if isMetaOf mv (whd_betadeltaiota env evd c) then evd + if isMetaOf mv (whd_all env evd c) then evd else error_cannot_unify env evd (mkMeta mv,c) else meta_assign mv (c,(status,TypeProcessed)) evd in diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 7ea9b9063..0b102f921 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -24,7 +24,7 @@ open Context.Rel.Declaration let crazy_type = mkSet let decompose_prod env t = - let (name,dom,codom as res) = destProd (whd_betadeltaiota env t) in + let (name,dom,codom as res) = destProd (whd_all env t) in match name with | Anonymous -> (Name (Id.of_string "x"), dom, codom) | Name _ -> res @@ -234,7 +234,7 @@ and nf_stk ?from:(from=0) env c t stk = let params,realargs = Util.Array.chop nparams allargs in let pT = hnf_prod_applist env (type_of_ind env (ind,u)) (Array.to_list params) in - let pT = whd_betadeltaiota env pT in + let pT = whd_all env pT in let dep, p = nf_predicate env (ind,u) mip params (type_of_switch sw) pT in (* Calcul du type des branches *) let btypes = build_branches_type env ind mib mip u params dep p in diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 853410db8..ef3845857 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 fd8a70c65..bfaeae712 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 ee5591521..55dfb88b4 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 8c0b4ba98..50984c48e 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 182433cb3..100ed1522 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 diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 6b78ce72c..404e10427 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -106,7 +106,7 @@ let find_mutually_recursive_statements thms = (* Cofixpoint or fixpoint w/o explicit decreasing argument *) | None | Some (None, CStructRec) -> let whnf_hyp_hds = map_rel_context_in_env - (fun env c -> fst (whd_betadeltaiota_stack env Evd.empty c)) + (fun env c -> fst (whd_all_stack env Evd.empty c)) (Global.env()) hyps in let ind_hyps = List.flatten (List.map_i (fun i decl -> @@ -120,7 +120,7 @@ let find_mutually_recursive_statements thms = []) 0 (List.rev whnf_hyp_hds)) in let ind_ccl = let cclenv = push_rel_context hyps (Global.env()) in - let whnf_ccl,_ = whd_betadeltaiota_stack cclenv Evd.empty ccl in + let whnf_ccl,_ = whd_all_stack cclenv Evd.empty ccl in match kind_of_term whnf_ccl with | Ind ((kn,_ as ind),u) when let mind = Global.lookup_mind kn in diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 316a79482..63b5e2a70 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -533,7 +533,7 @@ let make_resolve_hyp env sigma st flags only_classes pri decl = | Ind (i,_) -> is_class (IndRef i) | _ -> let env' = Environ.push_rel_context ctx env in - let ty' = whd_betadeltaiota env' ar in + let ty' = whd_all env' ar in if not (Term.eq_constr ty' ar) then iscl env' ty' else false in diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 26166bd83..c3796b484 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -62,7 +62,7 @@ let contradiction_context = | d :: rest -> let id = get_id d in let typ = nf_evar sigma (get_type d) in - let typ = whd_betadeltaiota env sigma typ in + let typ = whd_all env sigma typ in if is_empty_type typ then simplest_elim (mkVar id) else match kind_of_term typ with @@ -84,7 +84,7 @@ let contradiction_context = end } let is_negation_of env sigma typ t = - match kind_of_term (whd_betadeltaiota env sigma t) with + match kind_of_term (whd_all env sigma t) with | Prod (na,t,u) -> let u = nf_evar sigma u in is_empty_type u && is_conv_leq env sigma typ t diff --git a/tactics/equality.ml b/tactics/equality.ml index 35be1fcb6..1950356b3 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -720,8 +720,8 @@ let find_positions env sigma t1 t2 = then [(List.rev posn,t1,t2)] else [] in let rec findrec sorts posn t1 t2 = - let hd1,args1 = whd_betadeltaiota_stack env sigma t1 in - let hd2,args2 = whd_betadeltaiota_stack env sigma t2 in + let hd1,args1 = whd_all_stack env sigma t1 in + let hd2,args2 = whd_all_stack env sigma t2 in match (kind_of_term hd1, kind_of_term hd2) with | Construct (sp1,_), Construct (sp2,_) when Int.equal (List.length args1) (constructor_nallargs_env env sp1) @@ -1283,7 +1283,7 @@ let build_injector env sigma dflt c cpath = (* let try_delta_expand env sigma t = - let whdt = whd_betadeltaiota env sigma t in + let whdt = whd_all env sigma t in let rec hd_rec c = match kind_of_term c with | Construct _ -> whdt diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 4c2c84d23..f2c72c2f3 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -464,7 +464,7 @@ let match_eq_nf gls eqn (ref, hetero) = match Id.Map.bindings (pf_matches gls pat eqn) with | [(m1,t);(m2,x);(m3,y)] -> assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3); - (t,pf_whd_betadeltaiota gls x,pf_whd_betadeltaiota gls y) + (t,pf_whd_all gls x,pf_whd_all gls y) | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 terms") let dest_nf_eq gls eqn = diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 70782ec64..63b1a7b54 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -114,7 +114,7 @@ let max_prefix_sign lid sign = | id::l -> snd (max_rec (id, sign_prefix id sign) l) *) let rec add_prods_sign env sigma t = - match kind_of_term (whd_betadeltaiota env sigma t) with + match kind_of_term (whd_all env sigma t) with | Prod (na,c1,b) -> let id = id_of_name_using_hdchar env t na in let b'= subst1 (mkVar id) b in @@ -167,7 +167,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option = let goal = mkArrow i (applist(mkVar p, List.rev revargs)) in (pty,goal) in - let npty = nf_betadeltaiota env sigma pty in + let npty = nf_all env sigma pty in let extenv = push_named (LocalAssum (p,npty)) env in extenv, goal diff --git a/tactics/tactics.ml b/tactics/tactics.ml index cf842d6f1..9a39773a8 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -537,7 +537,7 @@ let fix ido n = match ido with mutual_fix id n [] 0 let rec check_is_mutcoind env sigma cl = - let b = whd_betadeltaiota env sigma cl in + let b = whd_all env sigma cl in match kind_of_term b with | Prod (na, c1, b) -> let open Context.Rel.Declaration in @@ -774,15 +774,15 @@ let check_types env sigma mayneedglobalcheck deep newc origc = let sigma, b = infer_conv ~pb:Reduction.CUMUL env sigma t1 t2 in if not b then if - isSort (whd_betadeltaiota env sigma t1) && - isSort (whd_betadeltaiota env sigma t2) + isSort (whd_all env sigma t1) && + isSort (whd_all env sigma t2) then (mayneedglobalcheck := true; sigma) else errorlabstrm "convert-check-hyp" (str "Types are incompatible.") else sigma end else - if not (isSort (whd_betadeltaiota env sigma t1)) then + if not (isSort (whd_all env sigma t1)) then errorlabstrm "convert-check-hyp" (str "Not a type.") else sigma @@ -1204,7 +1204,7 @@ let cut c = try (** Backward compat: ensure that [c] is well-typed. *) let typ = Typing.unsafe_type_of env sigma c in - let typ = whd_betadeltaiota env sigma typ in + let typ = whd_all env sigma typ in match kind_of_term typ with | Sort _ -> true | _ -> false @@ -2293,8 +2293,8 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac = Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let type_of = Tacmach.New.pf_unsafe_type_of gl in - let whd_betadeltaiota = Tacmach.New.pf_apply whd_betadeltaiota gl in - let t = whd_betadeltaiota (type_of (mkVar id)) in + let whd_all = Tacmach.New.pf_apply whd_all gl in + let t = whd_all (type_of (mkVar id)) in let eqtac, thin = match match_with_equality_type t with | Some (hdcncl,[_;lhs;rhs]) -> if l2r && isVar lhs && not (occur_var env (destVar lhs) rhs) then @@ -4253,7 +4253,7 @@ let check_enough_applied env sigma elim = | None -> (* No eliminator given *) fun u -> - let t,_ = decompose_app (whd_betadeltaiota env sigma u) in isInd t + let t,_ = decompose_app (whd_all env sigma u) in isInd t | Some elimc -> let elimt = Retyping.get_type_of env sigma (fst elimc) in let scheme = compute_elim_sig ~elimc elimt in @@ -4573,7 +4573,7 @@ let maybe_betadeltaiota_concl allowred gl = if not allowred then concl else let env = Proofview.Goal.env gl in - whd_betadeltaiota env sigma concl + whd_all env sigma concl let reflexivity_red allowred = Proofview.Goal.enter { enter = begin fun gl -> diff --git a/toplevel/command.ml b/toplevel/command.ml index 2875511d3..f3c2c43c2 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -456,7 +456,7 @@ let sign_level env evd sign = match d with | LocalDef _ -> lev, push_rel d env | LocalAssum _ -> - let s = destSort (Reduction.whd_betadeltaiota env + let s = destSort (Reduction.whd_all env (nf_evar evd (Retyping.get_type_of env evd (get_type d)))) in let u = univ_of_sort s in diff --git a/toplevel/record.ml b/toplevel/record.ml index e9de6b532..f8c70f0af 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -118,7 +118,7 @@ let typecheck_params_and_fields def id pl t ps nots fs = match t with | CSort (_, Misctypes.GType []) -> true | _ -> false in let s = interp_type_evars env evars ~impls:empty_internalization_env t in - let sred = Reductionops.whd_betadeltaiota env !evars s in + let sred = Reductionops.whd_all env !evars s in (match kind_of_term sred with | Sort s' -> (if poly then |