diff options
Diffstat (limited to 'proofs/redexpr.ml')
| -rw-r--r-- | proofs/redexpr.ml | 30 |
1 files changed, 20 insertions, 10 deletions
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index ea21917a..72cb05f1 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Term @@ -17,7 +17,7 @@ open Genredexpr open Pattern open Reductionops open Tacred -open Closure +open CClosure open RedFlags open Libobject open Misctypes @@ -29,17 +29,22 @@ let cbv_vm env sigma c = error "vm_compute does not support existential variables."; Vnorm.cbv_vm env c ctyp +let warn_native_compute_disabled = + CWarnings.create ~name:"native-compute-disabled" ~category:"native-compiler" + (fun () -> + strbrk "native_compute disabled at configure time; falling back to vm_compute.") + let cbv_native env sigma c = if Coq_config.no_native_compiler then - let () = msg_warning (str "native_compute disabled at configure time; falling back to vm_compute.") in - cbv_vm env sigma c + (warn_native_compute_disabled (); + cbv_vm env sigma c) else let ctyp = Retyping.get_type_of env sigma c in Nativenorm.native_norm env sigma c ctyp let whd_cbn flags env sigma t = let (state,_) = - (whd_state_gen true flags env sigma (t,Reductionops.Stack.empty)) + (whd_state_gen true true flags env sigma (t,Reductionops.Stack.empty)) in Reductionops.Stack.zip ~refold:true state let strong_cbn flags = @@ -141,7 +146,9 @@ 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.rMatch then red_add red fMATCH else red in + let red = if f.rFix then red_add red fFIX else red in + let red = if f.rCofix then red_add red 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 *) @@ -158,8 +165,6 @@ let make_flag env f = f.rConst red in red -let is_reference = function PRef _ | PVar _ -> true | _ -> false - (* table of custom reductino fonctions, not synchronized, filled via ML calls to [declare_reduction] *) let reduction_tab = ref String.Map.empty @@ -196,7 +201,7 @@ let out_arg = function let out_with_occurrences (occs,c) = (Locusops.occurrences_map (List.map out_arg) occs, c) -let e_red f env evm c = evm, f env evm c +let e_red f = { e_redfun = fun env evm c -> Sigma.here (f env (Sigma.to_evar_map evm) c) evm } let head_style = false (* Turn to true to have a semantics where simpl only reduce at the head when an evaluable reference is given, e.g. @@ -211,6 +216,11 @@ let contextualize f g = function e_red (contextually b (l,c) (fun _ -> h)) | None -> e_red g +let warn_simpl_unfolding_modifiers = + CWarnings.create ~name:"simpl-unfolding-modifiers" ~category:"tactics" + (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 @@ -223,7 +233,7 @@ let reduction_of_red_expr env = let am = if !simplIsCbn then strong_cbn (make_flag f) else simpl in let () = if not (!simplIsCbn || List.is_empty f.rConst) then - Pp.msg_warning (Pp.strbrk "The legacy simpl does not deal with delta flags.") in + warn_simpl_unfolding_modifiers () in (contextualize (if head_style then whd_am else am) am o,DEFAULTcast) | Cbv f -> (e_red (cbv_norm_flags (make_flag f)),DEFAULTcast) | Cbn f -> |