diff options
| -rw-r--r-- | pretyping/reductionops.ml | 21 | ||||
| -rw-r--r-- | pretyping/reductionops.mli | 7 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 5 | ||||
| -rw-r--r-- | tactics/cbn.ml | 12 | ||||
| -rw-r--r-- | tactics/cbn.mli | 7 | ||||
| -rw-r--r-- | tactics/redexpr.ml | 7 | ||||
| -rw-r--r-- | tactics/tactics.ml | 4 |
7 files changed, 28 insertions, 35 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 10caf855ba..54a47a252d 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -468,23 +468,6 @@ let safe_meta_value sigma ev = try Some (Evd.meta_value sigma ev) with Not_found -> None -let strong_with_flags whdfun flags env sigma t = - let push_rel_check_zeta d env = - let open CClosure.RedFlags in - let d = match d with - | LocalDef (na,c,t) when not (red_set flags fZETA) -> LocalAssum (na,t) - | d -> d in - push_rel d env in - let rec strongrec env t = - map_constr_with_full_binders env sigma - push_rel_check_zeta strongrec env (whdfun flags env sigma t) in - strongrec env t - -let strong whdfun env sigma t = - let rec strongrec env t = - map_constr_with_full_binders env sigma push_rel strongrec env (whdfun env sigma t) in - strongrec env t - (*************************************) (*** Reduction using bindingss ***) (*************************************) @@ -1284,7 +1267,9 @@ let plain_instance sigma s c = match s with let instance env sigma s c = (* if s = [] then c else *) - strong whd_betaiota env sigma (plain_instance sigma s c) + (* No need to compute contexts under binders as whd_betaiota is local *) + let rec strongrec t = EConstr.map sigma strongrec (whd_betaiota env sigma t) in + strongrec (plain_instance sigma s c) (* pseudo-reduction rule: * [hnf_prod_app env s (Prod(_,B)) N --> B[N] diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 9d41e7ab58..41d16f1c3c 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -143,13 +143,6 @@ type e_reduction_function = env -> evar_map -> constr -> evar_map * constr type stack_reduction_function = env -> evar_map -> constr -> constr * constr list -(** {6 Reduction Function Operators } *) - -val strong_with_flags : - (CClosure.RedFlags.reds -> reduction_function) -> - (CClosure.RedFlags.reds -> reduction_function) -val strong : reduction_function -> reduction_function - (** {6 Generic Optimized Reduction Function using Closures } *) val clos_norm_flags : CClosure.RedFlags.reds -> reduction_function diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 1523ec502d..a103699716 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1054,7 +1054,10 @@ let hnf_constr env sigma c = whd_simpl_orelse_delta_but_fix env sigma (c, []) let whd_simpl env sigma c = applist (whd_simpl_stack env sigma (c, [])) -let simpl env sigma c = strong whd_simpl env sigma c +let simpl env sigma c = + let rec strongrec env t = + map_constr_with_full_binders env sigma push_rel strongrec env (whd_simpl env sigma t) in + strongrec env c (* Reduction at specific subterms *) diff --git a/tactics/cbn.ml b/tactics/cbn.ml index 39959d6fb8..6fb6cff04f 100644 --- a/tactics/cbn.ml +++ b/tactics/cbn.ml @@ -820,3 +820,15 @@ let whd_cbn flags env sigma t = (whd_state_gen ~refold:true ~tactic_mode:true flags env sigma (t, Stack.empty)) in Stack.zip ~refold:true sigma state + +let norm_cbn flags env sigma t = + let push_rel_check_zeta d env = + let open CClosure.RedFlags in + let d = match d with + | LocalDef (na,c,t) when not (red_set flags fZETA) -> LocalAssum (na,t) + | d -> d in + push_rel d env in + let rec strongrec env t = + map_constr_with_full_binders env sigma + push_rel_check_zeta strongrec env (whd_cbn flags env sigma t) in + strongrec env t diff --git a/tactics/cbn.mli b/tactics/cbn.mli index af54771382..a02a74f9e4 100644 --- a/tactics/cbn.mli +++ b/tactics/cbn.mli @@ -8,6 +8,13 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +(** Weak-head cbn reduction. Despite the name, the cbn reduction is a complex + reduction distinct from call-by-name or call-by-need. *) val whd_cbn : CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr + +(** Strong variant of cbn reduction. *) +val norm_cbn : + CClosure.RedFlags.reds -> + Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml index b415b30de8..87cae3abe5 100644 --- a/tactics/redexpr.ml +++ b/tactics/redexpr.ml @@ -46,9 +46,6 @@ let cbv_native env sigma c = let whd_cbn = Cbn.whd_cbn -let strong_cbn flags = - strong_with_flags whd_cbn flags - let simplIsCbn = Goptions.declare_bool_option_and_ref ~depr:false ~key:["SimplIsCbn"] ~value:false @@ -248,11 +245,11 @@ let reduction_of_red_expr_val = function | Hnf -> (e_red hnf_constr,DEFAULTcast) | Simpl (f,o) -> let whd_am = if simplIsCbn () then whd_cbn f else whd_simpl in - let am = if simplIsCbn () then strong_cbn f else simpl in + let am = if simplIsCbn () then Cbn.norm_cbn f else simpl in (contextualize (if head_style then whd_am else am) am o,DEFAULTcast) | Cbv f -> (e_red (cbv_norm_flags f),DEFAULTcast) | Cbn f -> - (e_red (strong_cbn f), DEFAULTcast) + (e_red (Cbn.norm_cbn f), DEFAULTcast) | Lazy f -> (e_red (clos_norm_flags f),DEFAULTcast) | Unfold ubinds -> (e_red (unfoldn (List.map out_with_occurrences ubinds)),DEFAULTcast) | Fold cl -> (e_red (fold_commands cl),DEFAULTcast) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index f72764945c..c64f583428 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1244,8 +1244,6 @@ let force_destruction_arg with_evars env sigma c = (* tactic "cut" (actually modus ponens) *) (****************************************) -let normalize_cut = false - let cut c = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in @@ -1260,8 +1258,6 @@ let cut c = | sigma, s -> let r = Sorts.relevance_of_sort s in let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_set_of_hyps gl) in - (* Backward compat: normalize [c]. *) - let c = if normalize_cut then strong whd_betaiota env sigma c else c in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Refine.refine ~typecheck:false begin fun h -> let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c r (Vars.lift 1 concl)) in |