diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2015-10-08 18:06:55 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2015-10-15 14:36:30 +0200 |
commit | 3116aeff0cdc51e6801f3e8ae4a6c0533e1a75ac (patch) | |
tree | b6b33c6c6167656b1ca9799407eeb56aa1de749f | |
parent | d08aa6b4f742a7162e726920810765258802c176 (diff) |
Fix #4346 1/2: native casts were not inferring universe constraints.
-rw-r--r-- | kernel/fast_typeops.ml | 2 | ||||
-rw-r--r-- | kernel/nativeconv.ml | 116 | ||||
-rw-r--r-- | kernel/nativeconv.mli | 4 | ||||
-rw-r--r-- | kernel/reduction.ml | 19 | ||||
-rw-r--r-- | kernel/reduction.mli | 19 | ||||
-rw-r--r-- | kernel/typeops.ml | 2 | ||||
-rw-r--r-- | pretyping/nativenorm.ml | 20 | ||||
-rw-r--r-- | pretyping/nativenorm.mli | 6 | ||||
-rw-r--r-- | pretyping/pretyping.ml | 8 | ||||
-rw-r--r-- | pretyping/reductionops.ml | 11 | ||||
-rw-r--r-- | pretyping/reductionops.mli | 9 | ||||
-rw-r--r-- | proofs/redexpr.ml | 3 |
12 files changed, 117 insertions, 102 deletions
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index d22abff10..063c9cf12 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.ml @@ -227,7 +227,7 @@ let judge_of_cast env c ct k expected_type = default_conv ~l2r:true CUMUL env ct expected_type | NATIVEcast -> let sigma = Nativelambda.empty_evars in - native_conv CUMUL sigma env ct expected_type + Nativeconv.native_conv CUMUL sigma env ct expected_type with NotConvertible -> error_actual_type env (make_judge c ct) expected_type diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index d0aa96fd1..fc68575cd 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -16,21 +16,21 @@ open Nativecode (** This module implements the conversion test by compiling to OCaml code *) -let rec conv_val env pb lvl cu v1 v2 = - if v1 == v2 then () +let rec conv_val env pb lvl v1 v2 cu = + if v1 == v2 then cu else match kind_of_value v1, kind_of_value v2 with | Vfun f1, Vfun f2 -> let v = mk_rel_accu lvl in - conv_val env CONV (lvl+1) cu (f1 v) (f2 v) + conv_val env CONV (lvl+1) (f1 v) (f2 v) cu | Vfun f1, _ -> - conv_val env CONV lvl cu v1 (fun x -> v2 x) + conv_val env CONV lvl v1 (fun x -> v2 x) cu | _, Vfun f2 -> - conv_val env CONV lvl cu (fun x -> v1 x) v2 + conv_val env CONV lvl (fun x -> v1 x) v2 cu | Vaccu k1, Vaccu k2 -> - conv_accu env pb lvl cu k1 k2 + conv_accu env pb lvl k1 k2 cu | Vconst i1, Vconst i2 -> - if not (Int.equal i1 i2) then raise NotConvertible + if Int.equal i1 i2 then cu else raise NotConvertible | Vblock b1, Vblock b2 -> let n1 = block_size b1 in let n2 = block_size b2 in @@ -38,76 +38,76 @@ let rec conv_val env pb lvl cu v1 v2 = raise NotConvertible; let rec aux lvl max b1 b2 i cu = if Int.equal i max then - conv_val env CONV lvl cu (block_field b1 i) (block_field b2 i) + conv_val env CONV lvl (block_field b1 i) (block_field b2 i) cu else - (conv_val env CONV lvl cu (block_field b1 i) (block_field b2 i); - aux lvl max b1 b2 (i+1) cu) + let cu = conv_val env CONV lvl (block_field b1 i) (block_field b2 i) cu in + aux lvl max b1 b2 (i+1) cu in aux lvl (n1-1) b1 b2 0 cu | Vaccu _, _ | Vconst _, _ | Vblock _, _ -> raise NotConvertible -and conv_accu env pb lvl cu k1 k2 = +and conv_accu env pb lvl k1 k2 cu = let n1 = accu_nargs k1 in let n2 = accu_nargs k2 in if not (Int.equal n1 n2) then raise NotConvertible; if Int.equal n1 0 then conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu else - (conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu; - List.iter2 (conv_val env CONV lvl cu) (args_of_accu k1) (args_of_accu k2)) + let cu = conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu in + List.fold_right2 (conv_val env CONV lvl) (args_of_accu k1) (args_of_accu k2) cu and conv_atom env pb lvl a1 a2 cu = - if a1 == a2 then () + if a1 == a2 then cu else match a1, a2 with | Ameta _, _ | _, Ameta _ | Aevar _, _ | _, Aevar _ -> assert false | Arel i1, Arel i2 -> - if not (Int.equal i1 i2) then raise NotConvertible + if Int.equal i1 i2 then cu else raise NotConvertible | Aind ind1, Aind ind2 -> - if not (eq_puniverses eq_ind ind1 ind2) then raise NotConvertible + if eq_puniverses eq_ind ind1 ind2 then cu else raise NotConvertible | Aconstant c1, Aconstant c2 -> - if not (eq_puniverses eq_constant c1 c2) then raise NotConvertible + if eq_puniverses eq_constant c1 c2 then cu else raise NotConvertible | Asort s1, Asort s2 -> - check_sort_cmp_universes env pb s1 s2 cu + sort_cmp_universes env pb s1 s2 cu | Avar id1, Avar id2 -> - if not (Id.equal id1 id2) then raise NotConvertible + if Id.equal id1 id2 then cu else raise NotConvertible | Acase(a1,ac1,p1,bs1), Acase(a2,ac2,p2,bs2) -> if not (eq_ind a1.asw_ind a2.asw_ind) then raise NotConvertible; - conv_accu env CONV lvl cu ac1 ac2; + let cu = conv_accu env CONV lvl ac1 ac2 cu in let tbl = a1.asw_reloc in let len = Array.length tbl in - if Int.equal len 0 then conv_val env CONV lvl cu p1 p2 + if Int.equal len 0 then conv_val env CONV lvl p1 p2 cu else begin - conv_val env CONV lvl cu p1 p2; - let max = len - 1 in - let rec aux i = - let tag,arity = tbl.(i) in - let ci = - if Int.equal arity 0 then mk_const tag - else mk_block tag (mk_rels_accu lvl arity) in - let bi1 = bs1 ci and bi2 = bs2 ci in - if Int.equal i max then conv_val env CONV (lvl + arity) cu bi1 bi2 - else (conv_val env CONV (lvl + arity) cu bi1 bi2; aux (i+1)) in - aux 0 + let cu = conv_val env CONV lvl p1 p2 cu in + let max = len - 1 in + let rec aux i cu = + let tag,arity = tbl.(i) in + let ci = + if Int.equal arity 0 then mk_const tag + else mk_block tag (mk_rels_accu lvl arity) in + let bi1 = bs1 ci and bi2 = bs2 ci in + if Int.equal i max then conv_val env CONV (lvl + arity) bi1 bi2 cu + else aux (i+1) (conv_val env CONV (lvl + arity) bi1 bi2 cu) in + aux 0 cu end | Afix(t1,f1,rp1,s1), Afix(t2,f2,rp2,s2) -> if not (Int.equal s1 s2) || not (Array.equal Int.equal rp1 rp2) then raise NotConvertible; - if f1 == f2 then () + if f1 == f2 then cu else conv_fix env lvl t1 f1 t2 f2 cu | (Acofix(t1,f1,s1,_) | Acofixe(t1,f1,s1,_)), (Acofix(t2,f2,s2,_) | Acofixe(t2,f2,s2,_)) -> if not (Int.equal s1 s2) then raise NotConvertible; - if f1 == f2 then () + if f1 == f2 then cu else if not (Int.equal (Array.length f1) (Array.length f2)) then raise NotConvertible else conv_fix env lvl t1 f1 t2 f2 cu | Aprod(_,d1,c1), Aprod(_,d2,c2) -> - conv_val env CONV lvl cu d1 d2; - let v = mk_rel_accu lvl in - conv_val env pb (lvl + 1) cu (d1 v) (d2 v) + let cu = conv_val env CONV lvl d1 d2 cu in + let v = mk_rel_accu lvl in + conv_val env pb (lvl + 1) (d1 v) (d2 v) cu | Aproj(p1,ac1), Aproj(p2,ac2) -> if not (Constant.equal p1 p2) then raise NotConvertible - else conv_accu env CONV lvl cu ac1 ac2 + else conv_accu env CONV lvl ac1 ac2 cu | Arel _, _ | Aind _, _ | Aconstant _, _ | Asort _, _ | Avar _, _ | Acase _, _ | Afix _, _ | Acofix _, _ | Acofixe _, _ | Aprod _, _ | Aproj _, _ -> raise NotConvertible @@ -118,21 +118,15 @@ and conv_fix env lvl t1 f1 t2 f2 cu = let max = len - 1 in let fargs = mk_rels_accu lvl len in let flvl = lvl + len in - let rec aux i = - conv_val env CONV lvl cu t1.(i) t2.(i); + let rec aux i cu = + let cu = conv_val env CONV lvl t1.(i) t2.(i) cu in let fi1 = napply f1.(i) fargs in let fi2 = napply f2.(i) fargs in - if Int.equal i max then conv_val env CONV flvl cu fi1 fi2 - else (conv_val env CONV flvl cu fi1 fi2; aux (i+1)) in - aux 0 + if Int.equal i max then conv_val env CONV flvl fi1 fi2 cu + else aux (i+1) (conv_val env CONV flvl fi1 fi2 cu) in + aux 0 cu -let native_conv pb sigma env t1 t2 = - if Coq_config.no_native_compiler then begin - let msg = "Native compiler is disabled, falling back to VM conversion test." in - Pp.msg_warning (Pp.str msg); - vm_conv pb env t1 t2 - end - else +let native_conv_gen pb sigma env univs t1 t2 = let penv = Environ.pre_env env in let ml_filename, prefix = get_ml_filename () in let code, upds = mk_conv_code penv sigma prefix t1 t2 in @@ -146,8 +140,26 @@ let native_conv pb sigma env t1 t2 = let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in if !Flags.debug then Pp.msg_debug (Pp.str time_info); (* TODO change 0 when we can have deBruijn *) - conv_val env pb 0 (Environ.universes env) !rt1 !rt2 + fst (conv_val env pb 0 !rt1 !rt2 univs) end | _ -> anomaly (Pp.str "Compilation failure") -let _ = set_nat_conv native_conv +(* Wrapper for [native_conv] above *) +let native_conv cv_pb sigma env t1 t2 = + if Coq_config.no_native_compiler then begin + let msg = "Native compiler is disabled, falling back to VM conversion test." in + Pp.msg_warning (Pp.str msg); + vm_conv cv_pb env t1 t2 + end + else + let univs = Environ.universes env in + let b = + if cv_pb = CUMUL then Constr.leq_constr_univs univs t1 t2 + else Constr.eq_constr_univs univs t1 t2 + in + let univs = (univs, checked_universes) in + if not b then begin + let t1 = Term.it_mkLambda_or_LetIn t1 (Environ.rel_context env) in + let t2 = Term.it_mkLambda_or_LetIn t2 (Environ.rel_context env) in + let _ = native_conv_gen cv_pb sigma env univs t1 t2 in () + end diff --git a/kernel/nativeconv.mli b/kernel/nativeconv.mli index 318a7d830..21f0b2e9e 100644 --- a/kernel/nativeconv.mli +++ b/kernel/nativeconv.mli @@ -12,3 +12,7 @@ open Nativelambda (** This module implements the conversion test by compiling to OCaml code *) val native_conv : conv_pb -> evars -> types conversion_function + +(** A conversion function parametrized by a universe comparator. Used outside of + the kernel. *) +val native_conv_gen : conv_pb -> evars -> (constr, 'a) generic_conversion_function diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 0f105b048..b6c97b11d 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -637,7 +637,7 @@ let infer_cmp_universes env pb s0 s1 univs = let infer_convert_instances flex u u' (univs,cstrs) = (univs, Univ.enforce_eq_instances u u' cstrs) -let infered_universes : (Univ.universes * Univ.Constraint.t) universe_compare = +let inferred_universes : (Univ.universes * Univ.Constraint.t) universe_compare = { compare = infer_cmp_universes; compare_instances = infer_convert_instances } @@ -685,7 +685,7 @@ let conv_leq_vecti ?(l2r=false) ?(evars=fun _->None) env v1 v2 = v1 v2 -let generic_conv cv_pb l2r evars reds env univs t1 t2 = +let generic_conv cv_pb ~l2r evars reds env univs t1 t2 = let (s, _) = clos_fconv reds cv_pb l2r evars env univs t1 t2 in s @@ -697,7 +697,7 @@ let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 = in if b then cstrs else - let univs = ((univs, Univ.Constraint.empty), infered_universes) in + let univs = ((univs, Univ.Constraint.empty), inferred_universes) in let ((_,cstrs), _) = clos_fconv reds cv_pb l2r evars env univs t1 t2 in cstrs @@ -716,19 +716,6 @@ let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_sta env univs t1 t2 = infer_conv_universes CUMUL l2r evars ts env univs t1 t2 -(* option for conversion *) -let nat_conv = ref (fun cv_pb sigma -> - fconv cv_pb false (sigma.Nativelambda.evars_val)) -let set_nat_conv f = nat_conv := f - -let native_conv cv_pb sigma env t1 t2 = - if eq_constr t1 t2 then () - else begin - let t1 = (it_mkLambda_or_LetIn t1 (rel_context env)) in - let t2 = (it_mkLambda_or_LetIn t2 (rel_context env)) in - !nat_conv cv_pb sigma env t1 t2 - end - let vm_conv = ref (fun cv_pb -> fconv cv_pb false (fun _->None)) let set_vm_conv f = vm_conv := f let vm_conv cv_pb env t1 t2 = diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 90c008b19..b71356d03 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -49,14 +49,11 @@ type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.constraints -val check_sort_cmp_universes : - env -> conv_pb -> sorts -> sorts -> Univ.universes -> unit +val sort_cmp_universes : env -> conv_pb -> sorts -> sorts -> + 'a * 'a universe_compare -> 'a * 'a universe_compare -(* val sort_cmp : *) -(* conv_pb -> sorts -> sorts -> Univ.constraints -> Univ.constraints *) - -(* val conv_sort : sorts conversion_function *) -(* val conv_sort_leq : sorts conversion_function *) +val checked_universes : Univ.universes universe_compare +val inferred_universes : (Univ.universes * Univ.Constraint.t) universe_compare val trans_conv_cmp : ?l2r:bool -> conv_pb -> constr trans_conversion_function val trans_conv : @@ -77,22 +74,20 @@ val conv_leq : val conv_leq_vecti : ?l2r:bool -> ?evars:(existential->constr option) -> types array conversion_function +(** These conversion functions are used by module subtyping, which needs to infer + universe constraints inside the kernel *) val infer_conv : ?l2r:bool -> ?evars:(existential->constr option) -> ?ts:Names.transparent_state -> constr infer_conversion_function val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) -> ?ts:Names.transparent_state -> types infer_conversion_function -val generic_conv : conv_pb -> bool -> (existential->constr option) -> +val generic_conv : conv_pb -> l2r:bool -> (existential->constr option) -> Names.transparent_state -> (constr,'a) generic_conversion_function (** option for conversion *) val set_vm_conv : (conv_pb -> types conversion_function) -> unit val vm_conv : conv_pb -> types conversion_function -val set_nat_conv : - (conv_pb -> Nativelambda.evars -> types conversion_function) -> unit -val native_conv : conv_pb -> Nativelambda.evars -> types conversion_function - val default_conv : conv_pb -> ?l2r:bool -> types conversion_function val default_conv_leq : ?l2r:bool -> types conversion_function diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 8895bae5d..70f6fd803 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -310,7 +310,7 @@ let judge_of_cast env cj k tj = | NATIVEcast -> let sigma = Nativelambda.empty_evars in mkCast (cj.uj_val, k, expected_type), - native_conv CUMUL sigma env cj.uj_type expected_type + Nativeconv.native_conv CUMUL sigma env cj.uj_type expected_type in { uj_val = c; uj_type = expected_type } diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 2432b8d29..949a28a1f 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -22,11 +22,6 @@ open Nativelambda (** This module implements normalization by evaluation to OCaml code *) -let evars_of_evar_map evd = - { evars_val = Evd.existential_opt_value evd; - evars_typ = Evd.existential_type evd; - evars_metas = Evd.meta_type evd } - exception Find_at of int let invert_tag cst tag reloc_tbl = @@ -375,11 +370,17 @@ and nf_predicate env ind mip params v pT = true, mkLambda(name,dom,body) | _, _ -> false, nf_type env v +let evars_of_evar_map sigma = + { Nativelambda.evars_val = Evd.existential_opt_value sigma; + Nativelambda.evars_typ = Evd.existential_type sigma; + Nativelambda.evars_metas = Evd.meta_type sigma } + let native_norm env sigma c ty = if Coq_config.no_native_compiler then error "Native_compute reduction has been disabled at configure time." else - let penv = Environ.pre_env env in + let penv = Environ.pre_env env in + let sigma = evars_of_evar_map sigma in (* Format.eprintf "Numbers of free variables (named): %i\n" (List.length vl1); Format.eprintf "Numbers of free variables (rel): %i\n" (List.length vl2); @@ -400,3 +401,10 @@ let native_norm env sigma c ty = if !Flags.debug then Pp.msg_debug (Pp.str time_info); res | _ -> anomaly (Pp.str "Compilation failure") + +let native_conv_generic pb sigma t = + Nativeconv.native_conv_gen pb (evars_of_evar_map sigma) t + +let native_infer_conv ?(pb=Reduction.CUMUL) env sigma x y = + Reductionops.infer_conv_gen (fun pb ~l2r sigma ts -> native_conv_generic pb sigma) + ~catch_incon:true ~pb env sigma x y diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli index c854e8c9c..035203838 100644 --- a/pretyping/nativenorm.mli +++ b/pretyping/nativenorm.mli @@ -12,6 +12,8 @@ open Nativelambda (** This module implements normalization by evaluation to OCaml code *) -val evars_of_evar_map : evar_map -> evars +val native_norm : env -> evar_map -> constr -> types -> constr -val native_norm : env -> evars -> constr -> types -> constr +(** Conversion with inference of universe constraints *) +val native_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr -> + evar_map * bool diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 746b4000e..e1e8982e1 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -942,12 +942,10 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ | NATIVEcast -> let cj = pretype empty_tycon env evdref lvar c in let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in - let evars = Nativenorm.evars_of_evar_map !evdref in - let env = Environ.push_context_set (Evd.universe_context_set !evdref) env in begin - try - ignore (Nativeconv.native_conv Reduction.CUMUL evars env cty tval); cj - with Reduction.NotConvertible -> + let (evd,b) = Nativenorm.native_infer_conv env !evdref cty tval in + if b then (evdref := evd; cj) + else error_actual_type_loc loc env !evdref cj tval (ConversionFailed (env,cty,tval)) end diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index dc70f36cc..a24773b6e 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1295,8 +1295,8 @@ let sigma_univ_state = { Reduction.compare = sigma_compare_sorts; Reduction.compare_instances = sigma_compare_instances } -let infer_conv ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) - env sigma x y = +let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) + ?(ts=full_transparent_state) env sigma x y = try let b, sigma = let b, cstrs = @@ -1313,14 +1313,17 @@ let infer_conv ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_s if b then sigma, true else let sigma' = - Reduction.generic_conv pb false (safe_evar_value sigma) ts + conv_fun pb ~l2r:false sigma ts env (sigma, sigma_univ_state) x y in sigma', true with | Reduction.NotConvertible -> sigma, false | Univ.UniverseInconsistency _ when catch_incon -> sigma, false | e when is_anomaly e -> error "Conversion test raised an anomaly" - + +let infer_conv = infer_conv_gen (fun pb ~l2r sigma -> + Reduction.generic_conv pb ~l2r (safe_evar_value sigma)) + (********************************************************************) (* Special-Purpose Reduction *) (********************************************************************) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 1df2a73b2..b179dbc95 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -266,7 +266,7 @@ val is_trans_fconv : conv_pb -> transparent_state -> env -> evar_map -> constr *) val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> constr -> constr -> bool -(** [infer_fconv] Adds necessary universe constraints to the evar map. +(** [infer_conv] Adds necessary universe constraints to the evar map. pb defaults to CUMUL and ts to a full transparent state. @raises UniverseInconsistency iff catch_incon is set to false, otherwise returns false in that case. @@ -274,6 +274,13 @@ val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> con val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> constr -> constr -> evar_map * bool +(** [infer_conv_gen] behaves like [infer_conv] but is parametrized by a +conversion function. Used to pretype vm and native casts. *) +val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> transparent_state -> + (constr, evar_map) Reduction.generic_conversion_function) -> + ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> env -> + evar_map -> constr -> constr -> evar_map * bool + (** {6 Special-Purpose Reduction Functions } *) val whd_meta : evar_map -> constr -> constr diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index f172bbdd1..be92f2b04 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -35,8 +35,7 @@ let cbv_native env sigma c = cbv_vm env sigma c else let ctyp = Retyping.get_type_of env sigma c in - let evars = Nativenorm.evars_of_evar_map sigma in - Nativenorm.native_norm env evars c ctyp + Nativenorm.native_norm env sigma c ctyp let whd_cbn flags env sigma t = let (state,_) = |