diff options
| -rw-r--r-- | tactics/redexpr.ml | 46 | ||||
| -rw-r--r-- | tactics/redexpr.mli | 10 |
2 files changed, 39 insertions, 17 deletions
diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml index a8747e0a7c..7ed7e0f50b 100644 --- a/tactics/redexpr.ml +++ b/tactics/redexpr.ml @@ -129,6 +129,9 @@ let set_strategy local str = type red_expr = (constr, evaluable_global_reference, constr_pattern) red_expr_gen +type red_expr_val = + (constr, evaluable_global_reference, constr_pattern, CClosure.RedFlags.reds) red_expr_gen0 + let make_flag_constant = function | EvalVarRef id -> fVAR id | EvalConstRef sp -> fCONST sp @@ -221,38 +224,49 @@ let warn_simpl_unfolding_modifiers = (fun () -> Pp.strbrk "The legacy simpl ignores constant unfolding modifiers.") -let reduction_of_red_expr env = - let make_flag = make_flag env in - let rec reduction_of_red_expr = function +let rec eval_red_expr env = function +| Simpl (f, o) -> + let () = + if not (simplIsCbn () || List.is_empty f.rConst) then + warn_simpl_unfolding_modifiers () in + let f = if simplIsCbn () then make_flag env f else CClosure.all (* dummy *) in + Simpl (f, o) +| Cbv f -> Cbv (make_flag env f) +| Cbn f -> Cbn (make_flag env f) +| Lazy f -> Lazy (make_flag env f) +| ExtraRedExpr s -> + begin match String.Map.find s !red_expr_tab with + | e -> eval_red_expr env e + | exception Not_found -> ExtraRedExpr s (* delay to runtime interpretation *) + end +| (Red _ | Hnf | Unfold _ | Fold _ | Pattern _ | CbvVm _ | CbvNative _) as e -> e + +let reduction_of_red_expr_val = function | Red internal -> if internal then (e_red try_red_product,DEFAULTcast) else (e_red red_product,DEFAULTcast) | Hnf -> (e_red hnf_constr,DEFAULTcast) | Simpl (f,o) -> - let whd_am = if simplIsCbn () then whd_cbn (make_flag f) else whd_simpl in - let am = if simplIsCbn () then strong_cbn (make_flag f) else simpl in - let () = - if not (simplIsCbn () || List.is_empty f.rConst) then - warn_simpl_unfolding_modifiers () in + let whd_am = if simplIsCbn () then whd_cbn f else whd_simpl in + let am = if simplIsCbn () then strong_cbn f else simpl in (contextualize (if head_style then whd_am else am) am o,DEFAULTcast) - | Cbv f -> (e_red (cbv_norm_flags (make_flag f)),DEFAULTcast) + | Cbv f -> (e_red (cbv_norm_flags f),DEFAULTcast) | Cbn f -> - (e_red (strong_cbn (make_flag f)), DEFAULTcast) - | Lazy f -> (e_red (clos_norm_flags (make_flag f)),DEFAULTcast) + (e_red (strong_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) | Pattern lp -> (pattern_occs (List.map out_with_occurrences lp),DEFAULTcast) | ExtraRedExpr s -> (try (e_red (String.Map.find s !reduction_tab),DEFAULTcast) with Not_found -> - (try reduction_of_red_expr (String.Map.find s !red_expr_tab) - with Not_found -> user_err ~hdr:"Redexpr.reduction_of_red_expr" - (str "unknown user-defined reduction \"" ++ str s ++ str "\""))) + (str "unknown user-defined reduction \"" ++ str s ++ str "\"")) | CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast) | CbvNative o -> (contextualize cbv_native cbv_native o, NATIVEcast) - in - reduction_of_red_expr + +let reduction_of_red_expr env r = + reduction_of_red_expr_val (eval_red_expr env r) let subst_mps subst c = EConstr.of_constr (Mod_subst.subst_mps subst (EConstr.Unsafe.to_constr c)) diff --git a/tactics/redexpr.mli b/tactics/redexpr.mli index d43785218f..8350a831ca 100644 --- a/tactics/redexpr.mli +++ b/tactics/redexpr.mli @@ -19,10 +19,18 @@ open Reductionops open Locus type red_expr = - (constr, evaluable_global_reference, constr_pattern) red_expr_gen + (constr, evaluable_global_reference, constr_pattern) red_expr_gen + +type red_expr_val = + (constr, evaluable_global_reference, constr_pattern, CClosure.RedFlags.reds) red_expr_gen0 val out_with_occurrences : 'a with_occurrences -> occurrences * 'a +val eval_red_expr : Environ.env -> red_expr -> red_expr_val + +val reduction_of_red_expr_val : red_expr_val -> e_reduction_function * cast_kind + +(** Composition of {!reduction_of_red_expr_val} with {!eval_red_expr} *) val reduction_of_red_expr : Environ.env -> red_expr -> e_reduction_function * cast_kind |