diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 304 |
1 files changed, 128 insertions, 176 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 7c7b31395e..5484e70b61 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -6,16 +6,16 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Term open Vars -open Context open Termops open Univ open Evd open Environ +open Context.Rel.Declaration exception Elimconst @@ -573,7 +573,7 @@ type state = constr * constr Stack.t type contextual_reduction_function = env -> evar_map -> constr -> constr type reduction_function = contextual_reduction_function type local_reduction_function = evar_map -> constr -> constr -type e_reduction_function = env -> evar_map -> constr -> evar_map * constr +type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> constr -> (constr, 'r) Sigma.sigma } type contextual_stack_reduction_function = env -> evar_map -> constr -> constr * constr list @@ -594,9 +594,7 @@ let pr_state (tm,sk) = (*** Reduction Functions Operators ***) (*************************************) -let safe_evar_value sigma ev = - try Some (Evd.existential_value sigma ev) - with NotInstantiatedEvar | Not_found -> None +let safe_evar_value = Evarutil.safe_evar_value let safe_meta_value sigma ev = try Some (Evd.meta_value sigma ev) @@ -608,7 +606,7 @@ let strong whdfun env sigma t = strongrec env t let local_strong whdfun sigma = - let rec strongrec t = map_constr strongrec (whdfun sigma t) in + let rec strongrec t = Constr.map strongrec (whdfun sigma t) in strongrec let rec strong_prodspine redfun sigma c = @@ -621,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 +let eta = CClosure.RedFlags.mkflags [CClosure.RedFlags.fETA] (* Beta Reduction tools *) @@ -800,27 +782,29 @@ let equal_stacks (x, l) (y, l') = | Some (lft1,lft2) -> f_equal (x, lft1) (y, lft2) let rec whd_state_gen ?csts 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 let open Pp in - pp (h 0 (str "<<" ++ Termops.print_constr x ++ + Feedback.msg_notice + (h 0 (str "<<" ++ Termops.print_constr x ++ str "|" ++ cut () ++ Cst_stack.pr cst_l ++ str "|" ++ cut () ++ Stack.pr Termops.print_constr stack ++ str ">>") ++ fnl ()) in let fold () = let () = if !debug_RAKAM then - let open Pp in pp (str "<><><><><>" ++ fnl ()) in + let open Pp in Feedback.msg_notice (str "<><><><><>" ++ fnl ()) 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 - | (_,Some body,_) -> whrec Cst_stack.empty (lift n body, stack) + | 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 - | (_,Some body,_) -> whrec (Cst_stack.add_cst (mkVar id) cst_l) (body, stack) + | LocalDef (_,body,_) -> whrec (Cst_stack.add_cst (mkVar id) cst_l) (body, stack) | _ -> fold ()) | Evar ev -> (match safe_evar_value sigma ev with @@ -830,7 +814,7 @@ 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 -> @@ -870,7 +854,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,7 +895,7 @@ 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 -> + | LetIn (_,b,_,c) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fZETA -> apply_subst whrec [b] cst_l c stack | Cast (c,_,_) -> whrec cst_l (c, stack) | App (f,cl) -> @@ -920,10 +904,10 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = (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 -> + | Some _ when CClosure.RedFlags.red_set flags CClosure.RedFlags.fBETA -> apply_subst whrec [] cst_l x stack - | None when Closure.RedFlags.red_set flags Closure.RedFlags.fETA -> - let env' = push_rel (na,None,t) env in + | 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 | App (f,cl) -> @@ -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 = 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 @@ -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 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 @@ -1010,15 +996,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 +1020,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 +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 = 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) @@ -1105,109 +1093,72 @@ 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_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_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_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) -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) +(* 4. Ad-hoc eta reduction, does not subsitute evars *) -(* 4. Eta reduction Functions *) - -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 *) (****************************************************************************) (* Replacing defined evars for error messages *) -let rec whd_evar sigma c = - match kind_of_term c with - | Evar ev -> - let (evk, args) = ev in - let args = Array.map (fun c -> whd_evar sigma c) args in - (match safe_evar_value sigma (evk, args) with - Some c -> whd_evar sigma c - | None -> c) - | Sort (Type u) -> - let u' = Evd.normalize_universe sigma u in - if u' == u then c else mkSort (Sorts.sort_of_univ u') - | Const (c', u) when not (Univ.Instance.is_empty u) -> - let u' = Evd.normalize_universe_instance sigma u in - if u' == u then c else mkConstU (c', u') - | Ind (i, u) when not (Univ.Instance.is_empty u) -> - let u' = Evd.normalize_universe_instance sigma u in - if u' == u then c else mkIndU (i, u') - | Construct (co, u) when not (Univ.Instance.is_empty u) -> - let u' = Evd.normalize_universe_instance sigma u in - if u' == u then c else mkConstructU (co, u') - | _ -> c - -let nf_evar = - local_strong whd_evar +let whd_evar = Evarutil.whd_evar +let nf_evar = Evarutil.nf_evar (* lazy reduction functions. The infos must be created for each term *) (* Note by HH [oct 08] : why would it be the job of clos_norm_flags to add @@ -1215,16 +1166,16 @@ let 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 (********************************************************************) @@ -1255,31 +1206,29 @@ 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: ?l2r:bool-> ?evars:'a->'b) reds env sigma x y = +let test_trans_conversion (f: constr Reduction.extended_conversion_function) reds env sigma x y = try let evars ev = safe_evar_value sigma ev in - let _ = f ~evars reds env (Evd.universes sigma) x y in + let _ = f ~reds env ~evars:(evars, Evd.universes sigma) x y in true with Reduction.NotConvertible -> false | e when is_anomaly e -> report_anomaly e -let is_trans_conv reds env sigma = test_trans_conversion Reduction.trans_conv_universes reds env sigma -let is_trans_conv_leq reds env sigma = test_trans_conversion Reduction.trans_conv_leq_universes reds env sigma -let is_trans_fconv = function Reduction.CONV -> is_trans_conv | Reduction.CUMUL -> is_trans_conv_leq - -let is_conv = is_trans_conv full_transparent_state -let is_conv_leq = is_trans_conv_leq full_transparent_state -let is_fconv = function | Reduction.CONV -> is_conv | Reduction.CUMUL -> is_conv_leq +let is_conv ?(reds=full_transparent_state) env sigma = test_trans_conversion Reduction.conv reds env sigma +let is_conv_leq ?(reds=full_transparent_state) env sigma = test_trans_conversion Reduction.conv_leq reds env sigma +let is_fconv ?(reds=full_transparent_state) = function + | Reduction.CONV -> is_conv ~reds + | Reduction.CUMUL -> is_conv_leq ~reds let check_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = let f = match pb with - | Reduction.CONV -> Reduction.trans_conv_universes - | Reduction.CUMUL -> Reduction.trans_conv_leq_universes + | Reduction.CONV -> Reduction.conv + | Reduction.CUMUL -> Reduction.conv_leq in - try f ~evars:(safe_evar_value sigma) ts env (Evd.universes sigma) x y; true + try f ~reds:ts env ~evars:(safe_evar_value sigma, Evd.universes sigma) x y; true with Reduction.NotConvertible -> false | Univ.UniverseInconsistency _ -> false | e when is_anomaly e -> report_anomaly e @@ -1301,18 +1250,21 @@ let sigma_univ_state = let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = - try + try + let fold cstr sigma = + try Some (Evd.add_universe_constraints sigma cstr) + with Univ.UniverseInconsistency _ | Evd.UniversesDiffer -> None + in let b, sigma = - let b, cstrs = + let ans = if pb == Reduction.CUMUL then - Universes.leq_constr_univs_infer (Evd.universes sigma) x y + Universes.leq_constr_univs_infer (Evd.universes sigma) fold x y sigma else - Universes.eq_constr_univs_infer (Evd.universes sigma) x y + Universes.eq_constr_univs_infer (Evd.universes sigma) fold x y sigma in - if b then - try true, Evd.add_universe_constraints sigma cstrs - with Univ.UniverseInconsistency _ | Evd.UniversesDiffer -> false, sigma - else false, sigma + match ans with + | None -> false, sigma + | Some sigma -> true, sigma in if b then sigma, true else @@ -1418,7 +1370,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") @@ -1429,7 +1381,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") @@ -1441,10 +1393,10 @@ 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 (n,None,a) env) + decrec (push_rel (LocalAssum (n,a)) env) ((n,a)::m) c0 | _ -> m,t in @@ -1452,10 +1404,10 @@ 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 (n,None,a) env) + decrec (push_rel (LocalAssum (n,a)) env) ((n,a)::m) c0 | _ -> m,t in @@ -1463,21 +1415,21 @@ 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 (x,None,t) env) - (add_rel_decl (x, None, t) l) c + prodec_rec (push_rel (LocalAssum (x,t)) env) + (Context.Rel.add (LocalAssum (x,t)) l) c | LetIn (x,b,t,c) -> - prodec_rec (push_rel (x, Some b, t) env) - (add_rel_decl (x, Some b, t) l) c + prodec_rec (push_rel (LocalDef (x,b,t)) env) + (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 - prodec_rec env empty_rel_context + prodec_rec env Context.Rel.empty let splay_arity env sigma c = let l, c = splay_prod env sigma c in @@ -1489,26 +1441,26 @@ 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 (n,None,a) env) - (m-1) (add_rel_decl (n,None,a) ln) c0 + decrec (push_rel (LocalAssum (n,a)) env) + (m-1) (Context.Rel.add (LocalAssum (n,a)) ln) c0 | _ -> invalid_arg "splay_prod_n" in - decrec env n empty_rel_context + decrec env n Context.Rel.empty 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 (n,None,a) env) - (m-1) (add_rel_decl (n,None,a) ln) c0 + decrec (push_rel (LocalAssum (n,a)) env) + (m-1) (Context.Rel.add (LocalAssum (n,a)) ln) c0 | _ -> invalid_arg "splay_lam_n" in - decrec env n empty_rel_context + 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 @@ -1517,19 +1469,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 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 + (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 + (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 + (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' @@ -1538,10 +1490,10 @@ 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 (x,None,t) env) c0 - | Lambda (x,t,c0) -> decrec (push_rel (x,None,t) env) c0 + | Prod (x,t,c0) -> decrec (push_rel (LocalAssum (x,t)) env) c0 + | Lambda (x,t,c0) -> decrec (push_rel (LocalAssum (x,t)) env) c0 | t -> t in decrec env @@ -1625,7 +1577,7 @@ let meta_reducible_instance evd b = with | Some g -> irec (mkProj (p,g)) | None -> mkProj (p,c)) - | _ -> map_constr irec u + | _ -> Constr.map irec u in if Metaset.is_empty fm then (* nf_betaiota? *) b.rebus else irec b.rebus |