diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 271 |
1 files changed, 137 insertions, 134 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 79cb7a2f67..4ccbc81b47 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Term @@ -26,6 +26,19 @@ exception Elimconst their parameters in its stack. *) +let refolding_in_reduction = ref false +let _ = Goptions.declare_bool_option { + Goptions.optsync = true; Goptions.optdepr = false; + Goptions.optname = + "Perform refolding of fixpoints/constants like cbn during reductions"; + Goptions.optkey = ["Refolding";"Reduction"]; + Goptions.optread = (fun () -> !refolding_in_reduction); + Goptions.optwrite = (fun a -> refolding_in_reduction:=a); +} + +let get_refolding_in_reduction () = !refolding_in_reduction +let set_refolding_in_reduction = (:=) refolding_in_reduction + (** Machinery to custom the behavior of the reduction *) module ReductionBehaviour = struct open Globnames @@ -619,36 +632,21 @@ 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 +let eta = CClosure.RedFlags.mkflags [CClosure.RedFlags.fETA] (* Beta Reduction tools *) -let apply_subst recfun env cst_l t stack = +let apply_subst recfun env refold cst_l t stack = let rec aux env cst_l t stack = match (Stack.decomp stack,kind_of_term t) with | Some (h,stacktl), Lambda (_,_,c) -> - aux (h::env) (Cst_stack.add_param h cst_l) c stacktl + let cst_l' = if refold then Cst_stack.add_param h cst_l else cst_l in + aux (h::env) cst_l' c stacktl | _ -> recfun cst_l (substl env t, stack) in aux env cst_l t stack let stacklam recfun env t stack = - apply_subst (fun _ -> recfun) env Cst_stack.empty t stack + apply_subst (fun _ -> recfun) env false Cst_stack.empty t stack let beta_applist (c,l) = stacklam Stack.zip [] c (Stack.append_app_list l Stack.empty) @@ -713,11 +711,16 @@ let contract_cofix ?env ?reference (bodynum,(names,types,bodies as typedbodies)) substl closure bodies.(bodynum) (** Similar to the "fix" case below *) -let reduce_and_refold_cofix recfun env cst_l cofix sk = - let raw_answer = contract_cofix ~env ?reference:(Cst_stack.reference cst_l) cofix in +let reduce_and_refold_cofix recfun env refold cst_l cofix sk = + let raw_answer = + let env = if refold then Some env else None in + contract_cofix ?env ?reference:(Cst_stack.reference cst_l) cofix in apply_subst - (fun x (t,sk') -> recfun x (Cst_stack.best_replace (mkCoFix cofix) cst_l t,sk')) - [] Cst_stack.empty raw_answer sk + (fun x (t,sk') -> + let t' = + if refold then Cst_stack.best_replace (mkCoFix cofix) cst_l t else t in + recfun x (t',sk')) + [] refold Cst_stack.empty raw_answer sk let reduce_mind_case mia = match kind_of_term mia.mconstr with @@ -753,11 +756,18 @@ let contract_fix ?env ?reference ((recindices,bodynum),(names,types,bodies as ty replace the fixpoint by the best constant from [cst_l] Other rels are directly substituted by constants "magically found from the context" in contract_fix *) -let reduce_and_refold_fix recfun env cst_l fix sk = - let raw_answer = contract_fix ~env ?reference:(Cst_stack.reference cst_l) fix in +let reduce_and_refold_fix recfun env refold cst_l fix sk = + let raw_answer = + let env = if refold then None else Some env in + contract_fix ?env ?reference:(Cst_stack.reference cst_l) fix in apply_subst - (fun x (t,sk') -> recfun x (Cst_stack.best_replace (mkFix fix) cst_l t,sk')) - [] Cst_stack.empty raw_answer sk + (fun x (t,sk') -> + let t' = + if refold then + Cst_stack.best_replace (mkFix fix) cst_l t + else t + in recfun x (t',sk')) + [] refold Cst_stack.empty raw_answer sk let fix_recarg ((recindices,bodynum),_) stack = assert (0 <= bodynum && bodynum < Array.length recindices); @@ -797,7 +807,7 @@ let equal_stacks (x, l) (y, l') = | None -> false | Some (lft1,lft2) -> f_equal (x, lft1) (y, lft2) -let rec whd_state_gen ?csts tactic_mode flags env sigma = +let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = let open Context.Named.Declaration in let rec whrec cst_l (x, stack as s) = let () = if !debug_RAKAM then @@ -806,21 +816,22 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = (h 0 (str "<<" ++ Termops.print_constr x ++ str "|" ++ cut () ++ Cst_stack.pr cst_l ++ str "|" ++ cut () ++ Stack.pr Termops.print_constr stack ++ - str ">>") ++ fnl ()) + str ">>")) in let fold () = let () = if !debug_RAKAM then - let open Pp in Feedback.msg_notice (str "<><><><><>" ++ fnl ()) in + let open Pp in Feedback.msg_notice (str "<><><><><>") in (s,cst_l) in match kind_of_term x with - | Rel n when Closure.RedFlags.red_set flags Closure.RedFlags.fDELTA -> + | Rel n when CClosure.RedFlags.red_set flags CClosure.RedFlags.fDELTA -> (match lookup_rel n env with | LocalDef (_,body,_) -> whrec Cst_stack.empty (lift n body, stack) | _ -> fold ()) - | Var id when Closure.RedFlags.red_set flags (Closure.RedFlags.fVAR id) -> + | Var id when CClosure.RedFlags.red_set flags (CClosure.RedFlags.fVAR id) -> (match lookup_named id env with - | LocalDef (_,body,_) -> whrec (Cst_stack.add_cst (mkVar id) cst_l) (body, stack) + | LocalDef (_,body,_) -> + whrec (if refold then Cst_stack.add_cst (mkVar id) cst_l else cst_l) (body, stack) | _ -> fold ()) | Evar ev -> (match safe_evar_value sigma ev with @@ -830,12 +841,13 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = (match safe_meta_value sigma ev with | Some body -> whrec cst_l (body, stack) | None -> fold ()) - | Const (c,u as const) when Closure.RedFlags.red_set flags (Closure.RedFlags.fCONST c) -> + | Const (c,u as const) when CClosure.RedFlags.red_set flags (CClosure.RedFlags.fCONST c) -> (match constant_opt_value_in env const with | None -> fold () | Some body -> if not tactic_mode - then whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, stack) + then whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l) + (body, stack) else (* Looks for ReductionBehaviour *) match ReductionBehaviour.get (Globnames.ConstRef c) with | None -> whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, stack) @@ -870,7 +882,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = whrec Cst_stack.empty (arg,Stack.Cst(Stack.Cst_const const,curr,remains,bef,cst_l)::s') ) - | Proj (p, c) when Closure.RedFlags.red_projection flags p -> + | Proj (p, c) when CClosure.RedFlags.red_projection flags p -> (let pb = lookup_projection p env in let kn = Projection.constant p in let npars = pb.Declarations.proj_npars @@ -911,21 +923,21 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = (arg,Stack.Cst(Stack.Cst_proj p,curr,remains, Stack.append_app [|c|] bef,cst_l)::s')) - | LetIn (_,b,_,c) when Closure.RedFlags.red_set flags Closure.RedFlags.fZETA -> - apply_subst whrec [b] cst_l c stack + | LetIn (_,b,_,c) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fZETA -> + apply_subst whrec [b] refold cst_l c stack | Cast (c,_,_) -> whrec cst_l (c, stack) | App (f,cl) -> whrec - (Cst_stack.add_args cl cst_l) + (if refold then Cst_stack.add_args cl cst_l else cst_l) (f, Stack.append_app cl stack) | Lambda (na,t,c) -> (match Stack.decomp stack with - | Some _ when Closure.RedFlags.red_set flags Closure.RedFlags.fBETA -> - apply_subst whrec [] cst_l x stack - | None when Closure.RedFlags.red_set flags Closure.RedFlags.fETA -> + | Some _ when CClosure.RedFlags.red_set flags CClosure.RedFlags.fBETA -> + apply_subst whrec [] refold cst_l x stack + | None when CClosure.RedFlags.red_set flags CClosure.RedFlags.fETA -> let env' = push_rel (LocalAssum (na,t)) env in - let whrec' = whd_state_gen tactic_mode flags env' sigma in - (match kind_of_term (Stack.zip ~refold:true (fst (whrec' (c, Stack.empty)))) with + let whrec' = whd_state_gen ~refold ~tactic_mode flags env' sigma in + (match kind_of_term (Stack.zip ~refold (fst (whrec' (c, Stack.empty)))) with | App (f,cl) -> let napp = Array.length cl in if napp > 0 then @@ -950,16 +962,18 @@ 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 = CClosure.RedFlags.red_set flags CClosure.RedFlags.fMATCH in + let use_fix = CClosure.RedFlags.red_set flags CClosure.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 + reduce_and_refold_fix whrec env refold cst_l f out_sk |args, (Stack.Cst (const,curr,remains,s',cst_l) :: s'') -> let x' = Stack.zip(x,args) in begin match remains with @@ -969,7 +983,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = (match constant_opt_value_in env const with | None -> fold () | Some body -> - whrec (Cst_stack.add_cst (mkConstU const) cst_l) + whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l) (body, s' @ (Stack.append_app [|x'|] s''))) | Stack.Cst_proj p -> let pb = lookup_projection p env in @@ -988,14 +1002,14 @@ 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 CClosure.RedFlags.red_set flags CClosure.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 + reduce_and_refold_cofix whrec env refold cst_l cofix stack |_ -> fold () else fold () @@ -1010,15 +1024,15 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = let local_whd_state_gen flags sigma = let rec whrec (x, stack as s) = match kind_of_term x with - | LetIn (_,b,_,c) when Closure.RedFlags.red_set flags Closure.RedFlags.fZETA -> + | LetIn (_,b,_,c) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fZETA -> stacklam whrec [b] c stack | Cast (c,_,_) -> whrec (c, stack) | App (f,cl) -> whrec (f, Stack.append_app cl stack) | Lambda (_,_,c) -> (match Stack.decomp stack with - | Some (a,m) when Closure.RedFlags.red_set flags Closure.RedFlags.fBETA -> + | Some (a,m) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fBETA -> stacklam whrec [a] c m - | None when Closure.RedFlags.red_set flags Closure.RedFlags.fETA -> + | None when CClosure.RedFlags.red_set flags CClosure.RedFlags.fETA -> (match kind_of_term (Stack.zip (whrec (c, Stack.empty))) with | App (f,cl) -> let napp = Array.length cl in @@ -1034,7 +1048,7 @@ let local_whd_state_gen flags sigma = | _ -> s) | _ -> s) - | Proj (p,c) when Closure.RedFlags.red_projection flags p -> + | Proj (p,c) when CClosure.RedFlags.red_projection flags p -> (let pb = lookup_projection p (Global.env ()) in whrec (c, Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, p, Cst_stack.empty) @@ -1059,21 +1073,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 = CClosure.RedFlags.red_set flags CClosure.RedFlags.fMATCH in + let use_fix = CClosure.RedFlags.red_set flags CClosure.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 CClosure.RedFlags.red_set flags CClosure.RedFlags.fCOFIX then match Stack.strip_app stack with |args, ((Stack.Case _ | Stack.Proj _)::s') -> whrec (contract_cofix cofix, stack) @@ -1085,7 +1101,7 @@ let local_whd_state_gen flags sigma = whrec let raw_whd_state_gen flags env = - let f sigma s = fst (whd_state_gen false flags env sigma s) in + let f sigma s = fst (whd_state_gen (get_refolding_in_reduction ()) false flags env sigma s) in f let stack_red_of_state_red f = @@ -1095,7 +1111,7 @@ let stack_red_of_state_red f = (* Drops the Cst_stack *) let iterate_whd_gen refold flags env sigma s = let rec aux t = - let (hd,sk),_ = whd_state_gen refold flags env sigma (t,Stack.empty) in + let (hd,sk),_ = whd_state_gen refold false flags env sigma (t,Stack.empty) in let whd_sk = Stack.map aux sk in Stack.zip ~refold (hd,whd_sk) in aux s @@ -1105,79 +1121,64 @@ 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 CClosure.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 CClosure.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 CClosure.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 CClosure.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 CClosure.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 CClosure.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 CClosure.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 CClosure.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 CClosure.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_state = local_whd_state_gen CClosure.zeta +let whd_zeta_stack = stack_red_of_state_red whd_zeta_state +let whd_zeta = red_of_state_red whd_zeta_state (****************************************************************************) (* Reduction Functions *) @@ -1193,16 +1194,16 @@ let nf_evar = Evarutil.nf_evar let clos_norm_flags flgs env sigma t = try let evars ev = safe_evar_value sigma ev in - Closure.norm_val - (Closure.create_clos_infos ~evars flgs env) - (Closure.inject t) + CClosure.norm_val + (CClosure.create_clos_infos ~evars flgs env) + (CClosure.inject t) with e when is_anomaly e -> error "Tried to normalize ill-typed term" -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_beta = clos_norm_flags CClosure.beta (Global.env ()) +let nf_betaiota = clos_norm_flags CClosure.betaiota (Global.env ()) +let nf_betaiotazeta = clos_norm_flags CClosure.betaiotazeta (Global.env ()) +let nf_all env sigma = + clos_norm_flags CClosure.all env sigma (********************************************************************) @@ -1233,7 +1234,7 @@ let pb_equal = function let report_anomaly _ = let e = UserError ("", Pp.str "Conversion test raised an anomaly") in - let e = Errors.push e in + let e = CErrors.push e in iraise e let test_trans_conversion (f: constr Reduction.extended_conversion_function) reds env sigma x y = @@ -1397,7 +1398,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 +1409,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 +1421,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 +1432,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 +1443,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 +1453,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 +1469,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 +1479,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 +1488,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 @@ -1495,20 +1496,22 @@ let is_sort env sigma t = of case/fix (heuristic used by evar_conv) *) let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s = + let refold = get_refolding_in_reduction () in + let tactic_mode = false in 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 ~refold ~tactic_mode CClosure.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 + let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' ~refold ~tactic_mode + (CClosure.RedFlags.red_add_transparent CClosure.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 + let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' ~refold ~tactic_mode + (CClosure.RedFlags.red_add_transparent CClosure.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 + let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' ~refold ~tactic_mode + (CClosure.RedFlags.red_add_transparent CClosure.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 +1520,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 |