diff options
35 files changed, 295 insertions, 269 deletions
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index f290fea81..ffaefd5e3 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -177,7 +177,7 @@ let parse_ind_args si args relmax = let rec extract_type env db j c args = - match kind_of_term (whd_betaiotazeta c) with + match kind_of_term (whd_betaiotazeta Evd.empty c) with | App (d, args') -> (* We just accumulate the arguments. *) extract_type env db j d (Array.to_list args' @ args) @@ -285,7 +285,7 @@ and extract_type_app env db (r,s) args = and extract_type_scheme env db c p = if p=0 then extract_type env db 0 c [] else - let c = whd_betaiotazeta c in + let c = whd_betaiotazeta Evd.empty c in match kind_of_term c with | Lambda (n,t,d) -> extract_type_scheme (push_rel_assum (n,t) env) db d (p-1) diff --git a/contrib/firstorder/unify.ml b/contrib/firstorder/unify.ml index 41a100c2b..782129e5c 100644 --- a/contrib/firstorder/unify.ml +++ b/contrib/firstorder/unify.ml @@ -42,8 +42,8 @@ let unif t1 t2= Queue.add (t1,t2) bige; try while true do let t1,t2=Queue.take bige in - let nt1=head_reduce (whd_betaiotazeta t1) - and nt2=head_reduce (whd_betaiotazeta t2) in + let nt1=head_reduce (whd_betaiotazeta Evd.empty t1) + and nt2=head_reduce (whd_betaiotazeta Evd.empty t2) in match (kind_of_term nt1),(kind_of_term nt2) with Meta i,Meta j-> if i<>j then diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml index b9b47fde1..75b811d51 100644 --- a/contrib/funind/functional_principles_proofs.ml +++ b/contrib/funind/functional_principles_proofs.ml @@ -293,7 +293,8 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = (new_end_of_type,0,witness_fun) context in - let new_type_of_hyp = Reductionops.nf_betaiota new_type_of_hyp in + let new_type_of_hyp = + Reductionops.nf_betaiota Evd.empty new_type_of_hyp in let new_ctxt,new_end_of_type = decompose_prod_n_assum ctxt_size new_type_of_hyp in @@ -759,7 +760,8 @@ let build_proof | Const _ -> do_finalize dyn_infos g | Lambda _ -> - let new_term = Reductionops.nf_beta dyn_infos.info in + let new_term = + Reductionops.nf_beta Evd.empty dyn_infos.info in build_proof do_finalize {dyn_infos with info = new_term} g | LetIn _ -> @@ -1107,7 +1109,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : let bodies_with_all_params = Array.map (fun body -> - Reductionops.nf_betaiota + Reductionops.nf_betaiota Evd.empty (applist(substl (List.rev (Array.to_list all_funs_with_full_params)) body, List.rev_map var_of_decl princ_params)) ) @@ -1144,12 +1146,12 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : let body_with_param,num = let body = get_body fnames.(i) in let body_with_full_params = - Reductionops.nf_betaiota ( + Reductionops.nf_betaiota Evd.empty ( applist(body,List.rev_map var_of_decl full_params)) in match kind_of_term body_with_full_params with | Fix((_,num),(_,_,bs)) -> - Reductionops.nf_betaiota + Reductionops.nf_betaiota Evd.empty ( (applist (substl @@ -1225,7 +1227,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : nb_rec_hyps = -100; rec_hyps = []; info = - Reductionops.nf_betaiota + Reductionops.nf_betaiota Evd.empty (applist(fix_body,List.rev_map mkVar args_id)); eq_hyps = [] } @@ -1287,7 +1289,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : nb_rec_hyps = -100; rec_hyps = []; info = - Reductionops.nf_betaiota + Reductionops.nf_betaiota Evd.empty (applist(fbody_with_full_params, (List.rev_map var_of_decl princ_params)@ (List.rev_map mkVar args_id) diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml index cf861642d..2ab62763d 100644 --- a/contrib/interface/showproof.ml +++ b/contrib/interface/showproof.ml @@ -1361,7 +1361,7 @@ and natural_cutintro ig lh g gs arg ltree = {ihsg=No_subgoals_hyp;isgintro=""} (List.nth ltree 0))] ] -and whd_betadeltaiota x = whd_betaiotaevar (Global.env()) Evd.empty x +and whd_betadeltaiota x = whd_betaiota Evd.empty x and type_of_ast s c = type_of (Global.env()) Evd.empty (constr_of_ast c) and prod_head t = match (kind_of_term (strip_outer_cast t)) with diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml index 3e80be65e..09ee456d7 100644 --- a/contrib/subtac/subtac_cases.ml +++ b/contrib/subtac/subtac_cases.ml @@ -822,7 +822,7 @@ let infer_predicate loc env isevars typs cstrs indf = (* Empiric normalization: p may depend in a irrelevant way on args of the*) (* cstr as in [c:{_:Alpha & Beta}] match c with (existS a b)=>(a,b) end *) let typs = - Array.map (local_strong (whd_betaevar empty_env (Evd.evars_of !isevars))) typs + Array.map (local_strong whd_beta (Evd.evars_of !isevars)) typs in let eqns = array_map2 prepare_unif_pb typs cstrs in (* First strategy: no dependencies at all *) @@ -1042,9 +1042,10 @@ let find_predicate loc env isevars p typs cstrs current match p with | Some p -> abstract_predicate env (Evd.evars_of !isevars) indf current tms p | None -> infer_predicate loc env isevars typs cstrs indf in - let typ = whd_beta (applist (pred, realargs)) in + let typ = whd_beta (Evd.evars_of !isevars) (applist (pred, realargs)) in if dep then - (pred, whd_beta (applist (typ, [current])), new_Type ()) + (pred, whd_beta (Evd.evars_of !isevars) (applist (typ, [current])), + new_Type ()) else (pred, typ, new_Type ()) @@ -1246,7 +1247,7 @@ and match_current pb tomatch = find_predicate pb.caseloc pb.env pb.isevars pb.pred brtyps cstrs current indt pb.tomatch in let ci = make_case_info pb.env mind pb.casestyle in - let case = mkCase (ci,nf_betaiota pred,current,brvals) in + let case = mkCase (ci,nf_betaiota Evd.empty pred,current,brvals) in let inst = List.map mkRel deps in { uj_val = applist (case, inst); uj_type = substl inst typ } diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index df700e1b1..8b8bb9ab4 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -288,7 +288,7 @@ let declare_obligation obl body = print_message (Subtac_utils.definition_message obl.obl_name); { obl with obl_body = Some (mkConst constant) } -let red = Reductionops.nf_betaiota +let red = Reductionops.nf_betaiota Evd.empty let init_prog_info n b t deps fixkind notations obls impls kind hook = let obls' = diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml index c62db00bb..13e5e6d5f 100644 --- a/contrib/xml/cic2acic.ml +++ b/contrib/xml/cic2acic.ml @@ -245,9 +245,9 @@ let typeur sigma metamap = let Inductiveops.IndType(_,realargs) = try Inductiveops.find_rectype env sigma (type_of env c) with Not_found -> Util.anomaly "type_of: Bad recursive type" in - let t = Reductionops.whd_beta (T.applist (p, realargs)) in + let t = Reductionops.whd_beta sigma (T.applist (p, realargs)) in (match Term.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma (type_of env t)) with - | T.Prod _ -> Reductionops.whd_beta (T.applist (t, [c])) + | T.Prod _ -> Reductionops.whd_beta sigma (T.applist (t, [c])) | _ -> t) | T.Lambda (name,c1,c2) -> T.mkProd (name, c1, type_of (Environ.push_rel (name,None,c1) env) c2) @@ -390,7 +390,7 @@ Pp.ppnl (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-ty (* We need to refresh the universes because we are doing *) (* type inference on an already inferred type. *) {D.synthesized = - Reductionops.nf_beta + Reductionops.nf_beta evar_map (CPropRetyping.get_type_of env evar_map (Termops.refresh_universes tt)) ; D.expected = None} diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml index de8c540ca..17d1d5dab 100644 --- a/contrib/xml/doubleTypeInference.ml +++ b/contrib/xml/doubleTypeInference.ml @@ -163,7 +163,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types = | hj::restjl -> match T.kind_of_term (Reduction.whd_betadeltaiota env typ) with T.Prod (_,c1,c2) -> - (Some (Reductionops.nf_beta c1)) :: + (Some (Reductionops.nf_beta sigma c1)) :: (aux (T.subst1 hj c2) restjl) | _ -> assert false in @@ -183,7 +183,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types = | Some ety -> match T.kind_of_term (Reduction.whd_betadeltaiota env ety) with T.Prod (_,_,expected_target_type) -> - Some (Reductionops.nf_beta expected_target_type) + Some (Reductionops.nf_beta sigma expected_target_type) | _ -> assert false in let j' = execute env1 sigma c2 expectedc2type in @@ -214,14 +214,14 @@ let double_type_of env sigma cstr expectedty subterms_to_types = Typeops.judge_of_letin env name j1 j2 j3 | T.Cast (c,k,t) -> - let cj = execute env sigma c (Some (Reductionops.nf_beta t)) in + let cj = execute env sigma c (Some (Reductionops.nf_beta sigma t)) in let tj = execute env sigma t None in let tj = type_judgment env sigma tj in let j, _ = Typeops.judge_of_cast env cj k tj in j in let synthesized = E.j_type judgement in - let synthesized' = Reductionops.nf_beta synthesized in + let synthesized' = Reductionops.nf_beta sigma synthesized in let types,res = match expectedty with None -> diff --git a/interp/notation.ml b/interp/notation.ml index b6c1bfa40..bb17eda2c 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -422,7 +422,7 @@ let find_class_scope cl = Gmap.find cl !class_scope_map let find_class t = - let t, _ = decompose_app (Reductionops.whd_betaiotazeta t) in + let t, _ = decompose_app (Reductionops.whd_betaiotazeta Evd.empty t) in match kind_of_term t with | Var id -> CL_SECVAR id | Const sp -> CL_CONST sp @@ -435,7 +435,7 @@ let find_class t = (* Special scopes associated to arguments of a global reference *) let rec compute_arguments_scope t = - match kind_of_term (Reductionops.whd_betaiotazeta t) with + match kind_of_term (Reductionops.whd_betaiotazeta Evd.empty t) with | Prod (_,t,u) -> let sc = try Some (find_class_scope (find_class t)) with Not_found -> None in diff --git a/kernel/closure.ml b/kernel/closure.ml index d29f8b08c..10ef06993 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -28,7 +28,8 @@ let iota = ref 0 let prune = ref 0 let reset () = - beta := 0; delta := 0; zeta := 0; evar := 0; iota := 0; prune := 0 + beta := 0; delta := 0; zeta := 0; evar := 0; iota := 0; evar := 0; + prune := 0 let stop() = msgnl (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++ @@ -83,7 +84,6 @@ module RedFlags = (struct r_delta : bool; r_const : transparent_state; r_zeta : bool; - r_evar : bool; r_iota : bool } type red_kind = BETA | DELTA | IOTA | ZETA @@ -99,7 +99,6 @@ module RedFlags = (struct r_delta = false; r_const = all_opaque; r_zeta = false; - r_evar = false; r_iota = false } let red_add red = function @@ -201,6 +200,7 @@ type 'a infos = { i_flags : reds; i_repr : 'a infos -> constr -> 'a; i_env : env; + i_sigma : existential -> constr option; i_rels : int * (int * constr) list; i_vars : (identifier * constr) list; i_tab : (table_key, 'a) Hashtbl.t } @@ -227,6 +227,9 @@ let ref_value_cache info ref = | NotEvaluableConst _ (* Const *) -> None +let evar_value info ev = + info.i_sigma ev + let defined_vars flags env = (* if red_local_const (snd flags) then*) Sign.fold_named_context @@ -259,10 +262,11 @@ let rec mind_equiv env (kn1,i1) (kn2,i2) = let mind_equiv_infos info = mind_equiv info.i_env -let create mk_cl flgs env = +let create mk_cl flgs env evars = { i_flags = flgs; i_repr = mk_cl; i_env = env; + i_sigma = evars; i_rels = defined_rels flgs env; i_vars = defined_vars flgs env; i_tab = Hashtbl.create 17 } @@ -314,7 +318,7 @@ and fterm = | FLambda of int * (name * constr) list * constr * fconstr subs | FProd of name * fconstr * fconstr | FLetIn of name * fconstr * fconstr * constr * fconstr subs - | FEvar of existential_key * fconstr array + | FEvar of existential * fconstr subs | FLIFT of int * fconstr | FCLOS of constr * fconstr subs | FLOCKED @@ -581,8 +585,8 @@ let mk_clos_deep clos_fun env t = | LetIn (n,b,t,c) -> { norm = Red; term = FLetIn (n, clos_fun env b, clos_fun env t, c, env) } - | Evar(ev,args) -> - { norm = Whnf; term = FEvar(ev,Array.map (clos_fun env) args) } + | Evar ev -> + { norm = Red; term = FEvar(ev,env) } (* A better mk_clos? *) let mk_clos2 = mk_clos_deep mk_clos @@ -632,7 +636,8 @@ let rec to_constr constr_fun lfts v = mkLetIn (n, constr_fun lfts b, constr_fun lfts t, constr_fun (el_lift lfts) fc) - | FEvar (ev,args) -> mkEvar(ev,Array.map (constr_fun lfts) args) + | FEvar ((ev,args),env) -> + mkEvar(ev,Array.map (fun a -> constr_fun lfts (mk_clos2 env a)) args) | FLIFT (k,a) -> to_constr constr_fun (el_shft k lfts) a | FCLOS (t,env) -> let fr = mk_clos2 env t in @@ -891,6 +896,10 @@ let rec knr info m stk = | (_,args,s) -> (m,args@s)) | FLetIn (_,v,_,bd,e) when red_set info.i_flags fZETA -> knit info (subs_cons([|v|],e)) bd stk + | FEvar(ev,env) -> + (match evar_value info ev with + Some c -> knit info env c stk + | None -> (m,stk)) | _ -> (m,stk) (* Computes the weak head normal form of a term *) @@ -959,7 +968,8 @@ and norm_head info m = let fbds = Array.map (mk_clos (subs_liftn (Array.length na) e)) bds in mkFix(n,(na, Array.map (kl info) ftys, Array.map (kl info) fbds)) - | FEvar(i,args) -> mkEvar(i, Array.map (kl info) args) + | FEvar((i,args),env) -> + mkEvar(i, Array.map (fun a -> kl info (mk_clos env a)) args) | t -> term_of_fconstr m (* Initialization and then normalization *) @@ -982,7 +992,7 @@ let whd_stack infos m stk = (* cache of constants: the body is computed only when needed. *) type clos_infos = fconstr infos -let create_clos_infos flgs env = - create (fun _ -> inject) flgs env +let create_clos_infos ?(evars=fun _ -> None) flgs env = + create (fun _ -> inject) flgs env evars let unfold_reference = ref_value_cache diff --git a/kernel/closure.mli b/kernel/closure.mli index 926e152e0..ede0d6379 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -85,7 +85,9 @@ type table_key = id_key type 'a infos val ref_value_cache: 'a infos -> table_key -> 'a option val info_flags: 'a infos -> reds -val create: ('a infos -> constr -> 'a) -> reds -> env -> 'a infos +val create: ('a infos -> constr -> 'a) -> reds -> env -> + (existential -> constr option) -> 'a infos +val evar_value : 'a infos -> existential -> constr option (************************************************************************) (*s Lazy reduction. *) @@ -111,7 +113,7 @@ type fterm = | FLambda of int * (name * constr) list * constr * fconstr subs | FProd of name * fconstr * fconstr | FLetIn of name * fconstr * fconstr * constr * fconstr subs - | FEvar of existential_key * fconstr array + | FEvar of existential * fconstr subs | FLIFT of int * fconstr | FCLOS of constr * fconstr subs | FLOCKED @@ -156,7 +158,8 @@ val destFLambda : (* Global and local constant cache *) type clos_infos -val create_clos_infos : reds -> env -> clos_infos +val create_clos_infos : + ?evars:(existential->constr option) -> reds -> env -> clos_infos (* Reduction function *) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 3d2f3e9b9..f1a44b5ca 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -248,10 +248,12 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv = then convert_stacks infos lft1 lft2 v1 v2 cuniv else raise NotConvertible | _ -> raise NotConvertible) - | (FEvar (ev1,args1), FEvar (ev2,args2)) -> + | (FEvar ((ev1,args1),env1), FEvar ((ev2,args2),env2)) -> if ev1=ev2 then let u1 = convert_stacks infos lft1 lft2 v1 v2 cuniv in - convert_vect infos el1 el2 args1 args2 u1 + convert_vect infos el1 el2 + (Array.map (mk_clos env1) args1) + (Array.map (mk_clos env2) args2) u1 else raise NotConvertible (* 2 index known to be bound to no constant *) @@ -382,29 +384,29 @@ and convert_vect infos lft1 lft2 v1 v2 cuniv = fold 0 cuniv else raise NotConvertible -let clos_fconv trans cv_pb env t1 t2 = - let infos = trans, create_clos_infos betaiotazeta env in +let clos_fconv trans cv_pb evars env t1 t2 = + let infos = trans, create_clos_infos ~evars betaiotazeta env in ccnv cv_pb infos ELID ELID (inject t1) (inject t2) Constraint.empty -let trans_fconv reds cv_pb env t1 t2 = +let trans_fconv reds cv_pb evars env t1 t2 = if eq_constr t1 t2 then Constraint.empty - else clos_fconv reds cv_pb env t1 t2 + else clos_fconv reds cv_pb evars env t1 t2 -let trans_conv_cmp conv reds = trans_fconv reds conv -let trans_conv reds = trans_fconv reds CONV -let trans_conv_leq reds = trans_fconv reds CUMUL +let trans_conv_cmp conv reds = trans_fconv reds conv (fun _->None) +let trans_conv ?(evars=fun _->None) reds = trans_fconv reds CONV evars +let trans_conv_leq ?(evars=fun _->None) reds = trans_fconv reds CUMUL evars let fconv = trans_fconv (Idpred.full, Cpred.full) -let conv_cmp = fconv -let conv = fconv CONV -let conv_leq = fconv CUMUL +let conv_cmp cv_pb = fconv cv_pb (fun _->None) +let conv ?(evars=fun _->None) = fconv CONV evars +let conv_leq ?(evars=fun _->None) = fconv CUMUL evars -let conv_leq_vecti env v1 v2 = +let conv_leq_vecti ?(evars=fun _->None) env v1 v2 = array_fold_left2_i (fun i c t1 t2 -> let c' = - try conv_leq env t1 t2 + try conv_leq ~evars env t1 t2 with NotConvertible -> raise (NotConvertibleVect i) in Constraint.union c c') Constraint.empty @@ -413,17 +415,17 @@ let conv_leq_vecti env v1 v2 = (* option for conversion *) -let vm_conv = ref fconv +let vm_conv = ref (fun cv_pb -> fconv cv_pb (fun _->None)) let set_vm_conv f = vm_conv := f let vm_conv cv_pb env t1 t2 = try !vm_conv cv_pb env t1 t2 with Not_found | Invalid_argument _ -> (* If compilation fails, fall-back to closure conversion *) - fconv cv_pb env t1 t2 + fconv cv_pb (fun _->None) env t1 t2 -let default_conv = ref fconv +let default_conv = ref (fun cv_pb -> fconv cv_pb (fun _->None)) let set_default_conv f = default_conv := f @@ -432,7 +434,7 @@ let default_conv cv_pb env t1 t2 = !default_conv cv_pb env t1 t2 with Not_found | Invalid_argument _ -> (* If compilation fails, fall-back to closure conversion *) - fconv cv_pb env t1 t2 + fconv cv_pb (fun _->None) env t1 t2 let default_conv_leq = default_conv CUMUL (* diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 6ac1591bb..de926bd1d 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -40,15 +40,18 @@ val conv_sort : sorts conversion_function val conv_sort_leq : sorts conversion_function val trans_conv_cmp : conv_pb -> constr trans_conversion_function - -val trans_conv : constr trans_conversion_function -val trans_conv_leq : types trans_conversion_function +val trans_conv : + ?evars:(existential->constr option) -> constr trans_conversion_function +val trans_conv_leq : + ?evars:(existential->constr option) -> types trans_conversion_function val conv_cmp : conv_pb -> constr conversion_function - -val conv : constr conversion_function -val conv_leq : types conversion_function -val conv_leq_vecti : types array conversion_function +val conv : + ?evars:(existential->constr option) -> constr conversion_function +val conv_leq : + ?evars:(existential->constr option) -> types conversion_function +val conv_leq_vecti : + ?evars:(existential->constr option) -> types array conversion_function (* option for conversion *) val set_vm_conv : (conv_pb -> types conversion_function) -> unit diff --git a/library/library.ml b/library/library.ml index 7b20f13bf..c812819a2 100644 --- a/library/library.ml +++ b/library/library.ml @@ -632,6 +632,8 @@ let error_recursively_dependent_library dir = strbrk " to save current library because" ++ strbrk " it already depends on a library of this name.") +(* Security weakness: file might have been changed on disk between + writing the content and computing the checksum... *) let save_library_to dir f = let cenv, seg = Declaremods.end_library dir in let md = { diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 00df4c87a..dcedfa51d 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -981,7 +981,8 @@ let specialize_predicate newtomatchs (names,(depna,_)) cs tms ccl = let copti = if depna<>Anonymous then Some (build_dependent_constructor cs) else None in (* The substituends argsi, copti are all defined in gamma, x1...xn *) (* We need _parallel_ bindings to get gamma, x1...xn, tms |- ccl'' *) - let ccl'' = whd_betaiota (subst_predicate (argsi, copti) ccl' tms) in + let ccl'' = + whd_betaiota Evd.empty (subst_predicate (argsi, copti) ccl' tms) in (* We adjust ccl st: gamma, x1..xn, x1..xn, tms |- ccl'' *) let ccl''' = liftn_predicate n (n+1) ccl'' tms in (* We finally get gamma,x1..xn |- [X1,x1:=R1,x1]..[Xn,xn:=Rn,xn]pred'''*) @@ -989,7 +990,8 @@ let specialize_predicate newtomatchs (names,(depna,_)) cs tms ccl = let find_predicate loc env evdref p current (IndType (indf,realargs)) dep tms = let pred= abstract_predicate env (evars_of !evdref) indf current dep tms p in - (pred, whd_betaiota (applist (pred, realargs@[current])), new_Type ()) + (pred, whd_betaiota (evars_of !evdref) + (applist (pred, realargs@[current])), new_Type ()) let adjust_predicate_from_tomatch ((_,oldtyp),_,(nadep,_)) typ pb = match typ, oldtyp with @@ -1211,7 +1213,7 @@ and match_current pb tomatch = find_predicate pb.caseloc pb.env pb.evdref pb.pred current indt (names,dep) pb.tomatch in let ci = make_case_info pb.env mind pb.casestyle in - let case = mkCase (ci,nf_betaiota pred,current,brvals) in + let case = mkCase (ci,nf_betaiota Evd.empty pred,current,brvals) in let inst = List.map mkRel deps in { uj_val = applist (case, inst); uj_type = substl inst typ } @@ -1454,8 +1456,8 @@ let adjust_to_extended_env_and_remove_deps env extenv subst t = *) let abstract_tycon loc env evdref subst _tycon extenv t = - let t = nf_betaiota t in (* it helps in some cases to remove K-redex... *) let sigma = evars_of !evdref in + let t = nf_betaiota sigma t in (* it helps in some cases to remove K-redex *) let subst0,t0 = adjust_to_extended_env_and_remove_deps env extenv subst t in (* We traverse the type T of the original problem Xi looking for subterms that match the non-constructor part of the constraints (this part diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index ea7f6f065..179438252 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -218,6 +218,11 @@ let rec norm_head info env t stack = cbv_norm_term info env' c) in (VAL(0,normt), stack) (* Considérer une coupure commutative ? *) + | Evar ev -> + (match evar_value info ev with + Some c -> norm_head info env c stack + | None -> (VAL(0, t), stack)) + (* non-neutral cases *) | Lambda _ -> let ctxt,b = decompose_lam t in @@ -227,7 +232,7 @@ let rec norm_head info env t stack = | Construct c -> (CONSTR(c, [||]), stack) (* neutral cases *) - | (Sort _ | Meta _ | Ind _|Evar _) -> (VAL(0, t), stack) + | (Sort _ | Meta _ | Ind _) -> (VAL(0, t), stack) | Prod (x,t,c) -> (VAL(0, mkProd (x, cbv_norm_term info env t, cbv_norm_term info (subs_lift env) c)), @@ -353,8 +358,9 @@ let cbv_norm infos constr = type cbv_infos = cbv_value infos (* constant bodies are normalized at the first expansion *) -let create_cbv_infos flgs env = +let create_cbv_infos flgs env sigma = create (fun old_info c -> cbv_stack_term old_info TOP (ESID 0) c) flgs env + (Reductionops.safe_evar_value sigma) diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli index 21b65a57e..461115a56 100644 --- a/pretyping/cbv.mli +++ b/pretyping/cbv.mli @@ -22,7 +22,7 @@ open Esubst (* Entry point for cbv normalization of a constr *) type cbv_infos -val create_cbv_infos : RedFlags.reds -> env -> cbv_infos +val create_cbv_infos : RedFlags.reds -> env -> Evd.evar_map -> cbv_infos val cbv_norm : cbv_infos -> constr -> constr (************************************************************************) diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 548ca7596..b0554540a 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -143,7 +143,7 @@ let coercion_params coe_info = coe_info.coe_param (* find_class_type : env -> evar_map -> constr -> cl_typ * int *) let find_class_type env sigma t = - let t', args = Reductionops.whd_betaiotazetaevar_stack env sigma t in + let t', args = Reductionops.whd_betaiotazeta_stack sigma t in match kind_of_term t' with | Var id -> CL_SECVAR id, args | Const sp -> CL_CONST sp, args diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index 732ff1e69..24f3b7726 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -254,7 +254,7 @@ let clenv_unify_meta_types ?(flags=default_unify_flags) clenv = { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd } let clenv_unique_resolver allow_K ?(flags=default_unify_flags) clenv gl = - if isMeta (fst (whd_stack clenv.templtyp.rebus)) then + if isMeta (fst (whd_stack (evars_of clenv.evd) clenv.templtyp.rebus)) then clenv_unify allow_K CUMUL ~flags:flags (clenv_type clenv) (pf_concl gl) (clenv_unify_meta_types ~flags:flags clenv) else @@ -402,7 +402,7 @@ let error_already_defined b = (str "Position " ++ int n ++ str" already defined.") let clenv_unify_binding_type clenv c t u = - if isMeta (fst (whd_stack u)) then + if isMeta (fst (whd_stack (evars_of clenv.evd) u)) then (* Not enough information to know if some subtyping is needed *) CoerceToType, clenv, c else @@ -416,7 +416,7 @@ let clenv_unify_binding_type clenv c t u = let clenv_assign_binding clenv k (sigma,c) = let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in let clenv' = { clenv with evd = evar_merge clenv.evd sigma} in - let c_typ = nf_betaiota (clenv_get_type_of clenv' c) in + let c_typ = nf_betaiota (evars_of clenv'.evd) (clenv_get_type_of clenv' c) in let status,clenv'',c = clenv_unify_binding_type clenv' c c_typ k_typ in { clenv'' with evd = meta_assign k (c,(UserGiven,status)) clenv''.evd } diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 18cb9457d..aba6e2e19 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -62,7 +62,7 @@ let evar_apprec env evd stack c = in aux (c, append_stack_list stack empty_stack) let apprec_nohdbeta env evd c = - match kind_of_term (fst (Reductionops.whd_stack c)) with + match kind_of_term (fst (Reductionops.whd_stack (evars_of evd) c)) with | (Case _ | Fix _) -> applist (evar_apprec env evd [] c) | _ -> c diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 40599f4a3..fee8e29f5 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -122,7 +122,7 @@ let evars_to_metas sigma (emap, c) = let emap = nf_evars emap in let sigma',emap' = push_dependent_evars sigma emap in let change_exist evar = - let ty = nf_betaiota (nf_evar emap (existential_type emap evar)) in + let ty = nf_betaiota emap (existential_type emap evar) in let n = new_meta() in mkCast (mkMeta n, DEFAULTcast, ty) in let rec replace c = @@ -909,7 +909,7 @@ let rec invert_definition env evd (evk,argsv as ev) rhs = map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1) imitate envk t in - let rhs = whd_beta rhs (* heuristic *) in + let rhs = whd_beta (evars_of evd) rhs (* heuristic *) in let body = imitate (env,0) rhs in (!evdref,body) @@ -963,7 +963,7 @@ and evar_define env (evk,_ as ev) rhs evd = *) let has_undefined_evars evd t = - try let _ = local_strong (whd_ise (evars_of evd)) t in false + try let _ = local_strong whd_ise (evars_of evd) t in false with Uninstantiated_evar _ -> true let is_ground_term evd t = diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 689257c3b..f8dab16cd 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -229,7 +229,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = | None -> lambda_name env (n,t,process_constr (push_rel d env) (i+1) - (whd_beta (applist (lift 1 f, [(mkRel 1)]))) + (whd_beta Evd.empty (applist (lift 1 f, [(mkRel 1)]))) (cprest,rest)) | Some(_,f_0) -> let nF = lift (i+1+decF) f_0 in @@ -237,7 +237,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = let arg = process_pos env' nF (lift 1 t) in lambda_name env (n,t,process_constr env' (i+1) - (whd_beta (applist (lift 1 f, [(mkRel 1); arg]))) + (whd_beta Evd.empty (applist (lift 1 f, [(mkRel 1); arg]))) (cprest,rest))) | (n,Some c,t as d)::cprest, rest -> mkLetIn diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 9d99ed6d4..8a40361d3 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -114,31 +114,41 @@ type state = constr * constr stack type contextual_reduction_function = env -> evar_map -> constr -> constr type reduction_function = contextual_reduction_function -type local_reduction_function = constr -> constr +type local_reduction_function = evar_map -> constr -> constr type contextual_stack_reduction_function = env -> evar_map -> constr -> constr * constr list type stack_reduction_function = contextual_stack_reduction_function -type local_stack_reduction_function = constr -> constr * constr list +type local_stack_reduction_function = + evar_map -> constr -> constr * constr list type contextual_state_reduction_function = env -> evar_map -> state -> state type state_reduction_function = contextual_state_reduction_function -type local_state_reduction_function = state -> state +type local_state_reduction_function = evar_map -> state -> state (*************************************) (*** Reduction Functions Operators ***) (*************************************) -let rec whd_app_state (x, stack as s) = +let safe_evar_value sigma ev = + try Some (Evd.existential_value sigma ev) + with NotInstantiatedEvar | Not_found -> None + +let rec whd_app_state sigma (x, stack as s) = match kind_of_term x with - | App (f,cl) -> whd_app_state (f, append_stack cl stack) - | Cast (c,_,_) -> whd_app_state (c, stack) + | App (f,cl) -> whd_app_state sigma (f, append_stack cl stack) + | Cast (c,_,_) -> whd_app_state sigma (c, stack) + | Evar ev -> + (match safe_evar_value sigma ev with + Some c -> whd_app_state sigma (c,stack) + | _ -> s) | _ -> s let appterm_of_stack (f,s) = (f,list_of_stack s) -let whd_stack x = appterm_of_stack (whd_app_state (x, empty_stack)) +let whd_stack sigma x = + appterm_of_stack (whd_app_state sigma (x, empty_stack)) let whd_castapp_stack = whd_stack let stack_reduction_of_reduction red_fun env sigma s = @@ -150,14 +160,14 @@ let strong whdfun env sigma t = map_constr_with_full_binders push_rel strongrec env (whdfun env sigma t) in strongrec env t -let local_strong whdfun = - let rec strongrec t = map_constr strongrec (whdfun t) in +let local_strong whdfun sigma = + let rec strongrec t = map_constr strongrec (whdfun sigma t) in strongrec -let rec strong_prodspine redfun c = - let x = redfun c in +let rec strong_prodspine redfun sigma c = + let x = redfun sigma c in match kind_of_term x with - | Prod (na,a,b) -> mkProd (na,a,strong_prodspine redfun b) + | Prod (na,a,b) -> mkProd (na,a,strong_prodspine redfun sigma b) | _ -> x (*************************************) @@ -171,7 +181,6 @@ module type RedFlagsSig = sig type flags type flag val fbeta : flag - val fevar : flag val fdelta : flag val feta : flag val fiota : flag @@ -179,7 +188,6 @@ module type RedFlagsSig = sig val mkflags : flag list -> flags val red_beta : flags -> bool val red_delta : flags -> bool - val red_evar : flags -> bool val red_eta : flags -> bool val red_iota : flags -> bool val red_zeta : flags -> bool @@ -191,14 +199,12 @@ module RedFlags = (struct type flags = int let fbeta = 1 let fdelta = 2 - let fevar = 4 let feta = 8 let fiota = 16 let fzeta = 32 let mkflags = List.fold_left (lor) 0 let red_beta f = f land fbeta <> 0 let red_delta f = f land fdelta <> 0 - let red_evar f = f land fevar <> 0 let red_eta f = f land feta <> 0 let red_iota f = f land fiota <> 0 let red_zeta f = f land fzeta <> 0 @@ -209,20 +215,16 @@ open RedFlags (* Local *) let beta = mkflags [fbeta] let eta = mkflags [feta] -let evar = mkflags [fevar] -let betaevar = mkflags [fevar; fbeta] let betaiota = mkflags [fiota; fbeta] let betaiotazeta = mkflags [fiota; fbeta;fzeta] -let betaiotazetaevar = mkflags [fiota; fbeta;fzeta;fevar] (* Contextual *) -let delta = mkflags [fdelta;fevar] -let betadelta = mkflags [fbeta;fdelta;fzeta;fevar] -let betadeltaeta = mkflags [fbeta;fdelta;fzeta;fevar;feta] -let betadeltaiota = mkflags [fbeta;fdelta;fzeta;fevar;fiota] -let betadeltaiota_nolet = mkflags [fbeta;fdelta;fevar;fiota] -let betadeltaiotaeta = mkflags [fbeta;fdelta;fzeta;fevar;fiota;feta] -let betaiotaevar = mkflags [fbeta;fiota;fevar] +let delta = mkflags [fdelta] +let betadelta = mkflags [fbeta;fdelta;fzeta] +let betadeltaeta = mkflags [fbeta;fdelta;fzeta;feta] +let betadeltaiota = mkflags [fbeta;fdelta;fzeta;fiota] +let betadeltaiota_nolet = mkflags [fbeta;fdelta;fiota] +let betadeltaiotaeta = mkflags [fbeta;fdelta;fzeta;fiota;feta] let betaetalet = mkflags [fbeta;feta;fzeta] let betalet = mkflags [fbeta;fzeta] @@ -283,11 +285,11 @@ let fix_recarg ((recindices,bodynum),_) stack = type fix_reduction_result = NotReducible | Reduced of state -let reduce_fix whdfun fix stack = +let reduce_fix whdfun sigma fix stack = match fix_recarg fix stack with | None -> NotReducible | Some (recargnum,recarg) -> - let (recarg'hd,_ as recarg') = whdfun (recarg, empty_stack) in + let (recarg'hd,_ as recarg') = whdfun sigma (recarg, empty_stack) in let stack' = stack_assign stack recargnum (app_stack recarg') in (match kind_of_term recarg'hd with | Construct _ -> Reduced (contract_fix fix, stack') @@ -313,8 +315,8 @@ let rec whd_state_gen flags env sigma = (match lookup_named id env with | (_,Some body,_) -> whrec (body, stack) | _ -> s) - | Evar ev when red_evar flags -> - (match existential_opt_value sigma ev with + | Evar ev -> + (match safe_evar_value sigma ev with | Some body -> whrec (body, stack) | None -> s) | Const const when red_delta flags -> @@ -355,7 +357,7 @@ let rec whd_state_gen flags env sigma = (mkCase (ci, p, app_stack (c,cargs), lf), stack) | Fix fix when red_iota flags -> - (match reduce_fix whrec fix stack with + (match reduce_fix (fun _ -> whrec) sigma fix stack with | Reduced s' -> whrec s' | NotReducible -> s) @@ -363,7 +365,7 @@ let rec whd_state_gen flags env sigma = in whrec -let local_whd_state_gen flags = +let local_whd_state_gen flags sigma = let rec whrec (x, stack as s) = match kind_of_term x with | LetIn (_,b,_,c) when red_zeta flags -> stacklam whrec [b] c stack @@ -398,105 +400,91 @@ let local_whd_state_gen flags = (mkCase (ci, p, app_stack (c,cargs), lf), stack) | Fix fix when red_iota flags -> - (match reduce_fix whrec fix stack with + (match reduce_fix (fun _ ->whrec) sigma fix stack with | Reduced s' -> whrec s' | NotReducible -> s) + | Evar ev -> + (match safe_evar_value sigma ev with + Some c -> whrec (c,stack) + | None -> s) + | x -> s in whrec +let stack_red_of_state_red f sigma x = + appterm_of_stack (f sigma (x, empty_stack)) + +let red_of_state_red f sigma x = + app_stack (f sigma (x,empty_stack)) + (* 1. Beta Reduction Functions *) let whd_beta_state = local_whd_state_gen beta -let whd_beta_stack x = appterm_of_stack (whd_beta_state (x, empty_stack)) -let whd_beta x = app_stack (whd_beta_state (x,empty_stack)) +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 x = - appterm_of_stack (whd_betaetalet_state (x, empty_stack)) -let whd_betaetalet x = app_stack (whd_betaetalet_state (x,empty_stack)) +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_stack x = appterm_of_stack (whd_betalet_state (x, empty_stack)) -let whd_betalet x = app_stack (whd_betalet_state (x,empty_stack)) +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 = whd_state_gen delta e -let whd_delta_stack env sigma x = - appterm_of_stack (whd_delta_state env sigma (x, empty_stack)) -let whd_delta env sigma c = - app_stack (whd_delta_state env sigma (c, empty_stack)) +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 = whd_state_gen betadelta e -let whd_betadelta_stack env sigma x = - appterm_of_stack (whd_betadelta_state env sigma (x, empty_stack)) -let whd_betadelta env sigma c = - app_stack (whd_betadelta_state env sigma (c, empty_stack)) - -let whd_betaevar_state e = whd_state_gen betaevar e -let whd_betaevar_stack env sigma c = - appterm_of_stack (whd_betaevar_state env sigma (c, empty_stack)) -let whd_betaevar env sigma c = - app_stack (whd_betaevar_state env sigma (c, empty_stack)) +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_betadeltaeta_state e = whd_state_gen betadeltaeta e -let whd_betadeltaeta_stack env sigma x = - appterm_of_stack (whd_betadeltaeta_state env sigma (x, empty_stack)) -let whd_betadeltaeta env sigma x = - app_stack (whd_betadeltaeta_state env sigma (x, empty_stack)) +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_stack x = - appterm_of_stack (whd_betaiota_state (x, empty_stack)) -let whd_betaiota x = - app_stack (whd_betaiota_state (x, empty_stack)) +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_stack x = - appterm_of_stack (whd_betaiotazeta_state (x, empty_stack)) -let whd_betaiotazeta x = - app_stack (whd_betaiotazeta_state (x, empty_stack)) - -let whd_betaiotazetaevar_state = whd_state_gen betaiotazetaevar -let whd_betaiotazetaevar_stack env sigma x = - appterm_of_stack (whd_betaiotazetaevar_state env sigma (x, empty_stack)) -let whd_betaiotazetaevar env sigma x = - app_stack (whd_betaiotazetaevar_state env sigma (x, empty_stack)) - -let whd_betaiotaevar_state e = whd_state_gen betaiotaevar e -let whd_betaiotaevar_stack env sigma x = - appterm_of_stack (whd_betaiotaevar_state env sigma (x, empty_stack)) -let whd_betaiotaevar env sigma x = - app_stack (whd_betaiotaevar_state env sigma (x, empty_stack)) +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 e = whd_state_gen betadeltaiota e -let whd_betadeltaiota_stack env sigma x = - appterm_of_stack (whd_betadeltaiota_state env sigma (x, empty_stack)) -let whd_betadeltaiota env sigma x = - app_stack (whd_betadeltaiota_state env sigma (x, empty_stack)) +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_betadeltaiotaeta_state e = whd_state_gen betadeltaiotaeta e -let whd_betadeltaiotaeta_stack env sigma x = - appterm_of_stack (whd_betadeltaiotaeta_state env sigma (x, empty_stack)) -let whd_betadeltaiotaeta env sigma x = - app_stack (whd_betadeltaiotaeta_state env sigma (x, empty_stack)) +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_betadeltaiota_nolet_state e = whd_state_gen betadeltaiota_nolet e -let whd_betadeltaiota_nolet_stack env sigma x = - appterm_of_stack (whd_betadeltaiota_nolet_state env sigma (x, empty_stack)) -let whd_betadeltaiota_nolet env sigma x = - app_stack (whd_betadeltaiota_nolet_state env sigma (x, empty_stack)) +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) (* 3. Eta reduction Functions *) -let whd_eta c = app_stack (local_whd_state_gen eta (c,empty_stack)) +let whd_eta c = app_stack (local_whd_state_gen eta Evd.empty (c,empty_stack)) (****************************************************************************) (* Reduction Functions *) @@ -506,24 +494,25 @@ let whd_eta c = app_stack (local_whd_state_gen eta (c,empty_stack)) let rec whd_evar sigma c = match kind_of_term c with | Evar ev -> - let d = - try Some (Evd.existential_value sigma ev) - with NotInstantiatedEvar | Not_found -> None in - (match d with Some c -> whd_evar sigma c | None -> c) + (match safe_evar_value sigma ev with + Some c -> whd_evar sigma c + | None -> c) | Sort s when is_sort_variable sigma s -> whd_sort_variable sigma c | _ -> c -let nf_evar sigma = - local_strong (whd_evar sigma) +let nf_evar = + local_strong whd_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 a [nf_evar] here *) let clos_norm_flags flgs env sigma t = - norm_val (create_clos_infos flgs env) (inject (nf_evar sigma t)) + norm_val + (create_clos_infos ~evars:(safe_evar_value sigma) flgs env) + (inject t) -let nf_beta = clos_norm_flags Closure.beta empty_env Evd.empty -let nf_betaiota = clos_norm_flags Closure.betaiota empty_env Evd.empty +let nf_beta = clos_norm_flags Closure.beta empty_env +let nf_betaiota = clos_norm_flags Closure.betaiota empty_env let nf_betadeltaiota env sigma = clos_norm_flags Closure.betadeltaiota env sigma @@ -533,7 +522,7 @@ let nf_betadeltaiota env sigma = du type checking : (fun x => x + x) M *) -let rec whd_betaiotaevar_preserving_vm_cast env sigma t = +let rec whd_betaiota_preserving_vm_cast env sigma t = let rec stacklam_var subst t stack = match (decomp_stack stack,kind_of_term t) with | Some (h,stacktl), Lambda (_,_,c) -> @@ -548,7 +537,7 @@ let rec whd_betaiotaevar_preserving_vm_cast env sigma t = and whrec (x, stack as s) = match kind_of_term x with | Evar ev -> - (match existential_opt_value sigma ev with + (match safe_evar_value sigma ev with | Some body -> whrec (body, stack) | None -> s) | Cast (c,VMcast,t) -> @@ -574,12 +563,14 @@ let rec whd_betaiotaevar_preserving_vm_cast env sigma t = in app_stack (whrec (t,empty_stack)) -let nf_betaiotaevar_preserving_vm_cast = - strong whd_betaiotaevar_preserving_vm_cast +let nf_betaiota_preserving_vm_cast = + strong whd_betaiota_preserving_vm_cast (* lazy weak head reduction functions *) let whd_flags flgs env sigma t = - whd_val (create_clos_infos flgs env) (inject (nf_evar sigma t)) + whd_val + (create_clos_infos ~evars:(safe_evar_value sigma) flgs env) + (inject t) (********************************************************************) (* Conversion *) @@ -621,9 +612,9 @@ let nf_red_env sigma env = (fun d env -> push_rel (nf_decl d) env) ~init:env ctxt -let test_conversion f env sigma x y = +let test_conversion (f:?evars:'a->'b) env sigma x y = try let _ = - f (nf_red_env sigma env) (nf_evar sigma x) (nf_evar sigma y) in true + f ~evars:(safe_evar_value sigma) env x y in true with NotConvertible -> false let is_conv env sigma = test_conversion Reduction.conv env sigma @@ -709,7 +700,8 @@ let plain_instance s c = *) let instance s c = - (* if s = [] then c else *) local_strong whd_betaiota (plain_instance s c) + (* if s = [] then c else *) + local_strong whd_betaiota Evd.empty (plain_instance s c) (* pseudo-reduction rule: * [hnf_prod_app env s (Prod(_,B)) N --> B[N] @@ -820,7 +812,7 @@ let is_sort env sigma arity = let whd_betaiota_deltazeta_for_iota_state env sigma s = let rec whrec s = - let (t, stack as s) = whd_betaiota_state s in + let (t, stack as s) = whd_betaiota_state sigma s in match kind_of_term t with | Case (ci,p,d,lf) -> let (cr,crargs) = whd_betadeltaiota_stack env sigma d in @@ -830,7 +822,7 @@ let whd_betaiota_deltazeta_for_iota_state env sigma s = else s | Fix fix -> - (match reduce_fix (whd_betadeltaiota_state env sigma) fix stack with + (match reduce_fix (whd_betadeltaiota_state env) sigma fix stack with | Reduced s -> whrec s | NotReducible -> s) | _ -> s @@ -872,7 +864,7 @@ let whd_programs_stack env sigma = else (mkCase (ci, p, app_stack(c,cargs), lf), stack) | Fix fix -> - (match reduce_fix whrec fix stack with + (match reduce_fix (fun _ ->whrec) sigma fix stack with | Reduced s' -> whrec s' | NotReducible -> s) | _ -> s @@ -942,7 +934,7 @@ let meta_reducible_instance evd b = | Some (g,(_,s)) -> (mv,(g.rebus,s))::l | None -> l) [] fm in let rec irec u = - let u = whd_betaiota u in + let u = whd_betaiota Evd.empty u in match kind_of_term u with | Case (ci,p,c,bl) when isMeta c or isCast c & isMeta (pi1 (destCast c)) -> let m = try destMeta c with _ -> destMeta (pi1 (destCast c)) in diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 171967583..535101d74 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -54,17 +54,18 @@ type state = constr * constr stack type contextual_reduction_function = env -> evar_map -> constr -> constr type reduction_function = contextual_reduction_function -type local_reduction_function = constr -> constr +type local_reduction_function = evar_map -> constr -> constr type contextual_stack_reduction_function = env -> evar_map -> constr -> constr * constr list type stack_reduction_function = contextual_stack_reduction_function -type local_stack_reduction_function = constr -> constr * constr list +type local_stack_reduction_function = + evar_map -> constr -> constr * constr list type contextual_state_reduction_function = env -> evar_map -> state -> state type state_reduction_function = contextual_state_reduction_function -type local_state_reduction_function = state -> state +type local_state_reduction_function = evar_map -> state -> state (* Removes cast and put into applicative form *) val whd_stack : local_stack_reduction_function @@ -92,13 +93,12 @@ val nf_betaiota : local_reduction_function val nf_betadeltaiota : reduction_function val nf_evar : evar_map -> constr -> constr -val nf_betaiotaevar_preserving_vm_cast : reduction_function +val nf_betaiota_preserving_vm_cast : reduction_function (* Lazy strategy, weak head reduction *) val whd_evar : evar_map -> constr -> constr val whd_beta : local_reduction_function val whd_betaiota : local_reduction_function val whd_betaiotazeta : local_reduction_function -val whd_betaiotazetaevar : contextual_reduction_function val whd_betadeltaiota : contextual_reduction_function val whd_betadeltaiota_nolet : contextual_reduction_function val whd_betaetalet : local_reduction_function @@ -106,7 +106,7 @@ val whd_betalet : local_reduction_function val whd_beta_stack : local_stack_reduction_function val whd_betaiota_stack : local_stack_reduction_function -val whd_betaiotazetaevar_stack : contextual_stack_reduction_function +val whd_betaiotazeta_stack : local_stack_reduction_function val whd_betadeltaiota_stack : contextual_stack_reduction_function val whd_betadeltaiota_nolet_stack : contextual_stack_reduction_function val whd_betaetalet_stack : local_stack_reduction_function @@ -114,7 +114,7 @@ val whd_betalet_stack : local_stack_reduction_function val whd_beta_state : local_state_reduction_function val whd_betaiota_state : local_state_reduction_function -val whd_betaiotazetaevar_state : contextual_state_reduction_function +val whd_betaiotazeta_state : local_state_reduction_function val whd_betadeltaiota_state : contextual_state_reduction_function val whd_betadeltaiota_nolet_state : contextual_state_reduction_function val whd_betaetalet_state : local_state_reduction_function @@ -128,12 +128,6 @@ val whd_delta : reduction_function val whd_betadelta_stack : stack_reduction_function val whd_betadelta_state : state_reduction_function val whd_betadelta : reduction_function -val whd_betaevar_stack : stack_reduction_function -val whd_betaevar_state : state_reduction_function -val whd_betaevar : reduction_function -val whd_betaiotaevar_stack : stack_reduction_function -val whd_betaiotaevar_state : state_reduction_function -val whd_betaiotaevar : reduction_function val whd_betadeltaeta_stack : stack_reduction_function val whd_betadeltaeta_state : state_reduction_function val whd_betadeltaeta : reduction_function @@ -143,8 +137,9 @@ val whd_betadeltaiotaeta : reduction_function val whd_eta : constr -> constr +(* Various reduction functions *) - +val safe_evar_value : evar_map -> existential -> constr option val beta_applist : constr * constr list -> constr @@ -187,7 +182,7 @@ val whd_programs : reduction_function type fix_reduction_result = NotReducible | Reduced of state val fix_recarg : fixpoint -> constr stack -> (int * constr) option -val reduce_fix : local_state_reduction_function -> fixpoint +val reduce_fix : local_state_reduction_function -> evar_map -> fixpoint -> constr stack -> fix_reduction_result (*s Querying the kernel conversion oracle: opaque/transparent constants *) diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 2460c7642..3323c75b4 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -62,9 +62,9 @@ let retype sigma metamap = let Inductiveops.IndType(_,realargs) = try Inductiveops.find_rectype env sigma (type_of env c) with Not_found -> anomaly "type_of: Bad recursive type" in - let t = whd_beta (applist (p, realargs)) in + let t = whd_beta sigma (applist (p, realargs)) in (match kind_of_term (whd_betadeltaiota env sigma (type_of env t)) with - | Prod _ -> whd_beta (applist (t, [c])) + | Prod _ -> whd_beta sigma (applist (t, [c])) | _ -> t) | Lambda (name,c1,c2) -> mkProd (name, c1, type_of (push_rel (name,None,c1) env) c2) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 2c2bddb45..cca6b1855 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -204,7 +204,7 @@ let invert_name labs l na0 env sigma ref = function | None -> None | Some c -> let labs',ccl = decompose_lam c in - let _, l' = whd_betalet_stack ccl in + let _, l' = whd_betalet_stack sigma ccl in let labs' = List.map snd labs' in if labs' = labs & l = l' then Some (minfxargs,ref) else None @@ -234,7 +234,7 @@ let compute_consteval_direct sigma env ref = let compute_consteval_mutual_fix sigma env ref = let rec srec env minarg labs ref c = - let c',l = whd_betalet_stack c in + let c',l = whd_betalet_stack sigma c in let nargs = List.length l in match kind_of_term c' with | Lambda (na,t,g) when l=[] -> @@ -378,7 +378,7 @@ let solve_arity_problem env sigma fxminargs c = let evm = ref sigma in let set_fix i = evm := Evd.define !evm i (mkVar vfx) in let rec check strict c = - let c' = whd_betaiotazeta c in + let c' = whd_betaiotazeta sigma c in let (h,rcargs) = decompose_app c' in match kind_of_term h with Evar(i,_) when Intmap.mem i fxminargs && not (Evd.is_defined !evm i) -> @@ -418,14 +418,14 @@ let substl_checking_arity env subst c = -let contract_fix_use_function env f +let contract_fix_use_function env sigma f ((recindices,bodynum),(_names,_types,bodies as typedbodies)) = let nbodies = Array.length recindices in let make_Fi j = (mkFix((recindices,j),typedbodies), f j) in let lbodies = list_tabulate make_Fi nbodies in - substl_checking_arity env (List.rev lbodies) (nf_beta bodies.(bodynum)) + substl_checking_arity env (List.rev lbodies) (nf_beta sigma bodies.(bodynum)) -let reduce_fix_use_function env f whfun fix stack = +let reduce_fix_use_function env sigma f whfun fix stack = match fix_recarg fix stack with | None -> NotReducible | Some (recargnum,recarg) -> @@ -438,17 +438,18 @@ let reduce_fix_use_function env f whfun fix stack = let stack' = stack_assign stack recargnum (app_stack recarg') in (match kind_of_term recarg'hd with | Construct _ -> - Reduced (contract_fix_use_function env f fix,stack') + Reduced (contract_fix_use_function env sigma f fix,stack') | _ -> NotReducible) -let contract_cofix_use_function env f +let contract_cofix_use_function env sigma f (bodynum,(_names,_,bodies as typedbodies)) = let nbodies = Array.length bodies in let make_Fi j = (mkCoFix(j,typedbodies), f j) in let subbodies = list_tabulate make_Fi nbodies in - substl_checking_arity env (List.rev subbodies) (nf_beta bodies.(bodynum)) + substl_checking_arity env (List.rev subbodies) + (nf_beta sigma bodies.(bodynum)) -let reduce_mind_case_use_function func env mia = +let reduce_mind_case_use_function func env sigma mia = match kind_of_term mia.mconstr with | Construct(ind_sp,i) -> let real_cargs = list_skipn mia.mci.ci_npar mia.mcargs in @@ -476,11 +477,11 @@ let reduce_mind_case_use_function func env mia = else fun _ -> None in let cofix_def = - contract_cofix_use_function env build_cofix_name cofix in + contract_cofix_use_function env sigma build_cofix_name cofix in mkCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf) | _ -> assert false -let special_red_case sigma env whfun (ci, p, c, lf) = +let special_red_case env sigma whfun (ci, p, c, lf) = let rec redrec s = let (constr, cargs) = whfun s in if isEvalRef env constr then @@ -489,7 +490,7 @@ let special_red_case sigma env whfun (ci, p, c, lf) = | None -> raise Redelimination | Some gvalue -> if reducible_mind_case gvalue then - reduce_mind_case_use_function constr env + reduce_mind_case_use_function constr env sigma {mP=p; mconstr=gvalue; mcargs=list_of_stack cargs; mci=ci; mlf=lf} else @@ -514,15 +515,15 @@ let rec red_elim_const env sigma ref largs = let c = reference_value sigma env ref in let c', lrest = whd_betadelta_state env sigma (c,largs) in let whfun = whd_simpl_state env sigma in - (special_red_case sigma env whfun (destCase c'), lrest) + (special_red_case env sigma whfun (destCase c'), lrest) | EliminationFix (min,minfxargs,infos) when stack_args_size largs >=min -> let c = reference_value sigma env ref in let d, lrest = whd_betadelta_state env sigma (c,largs) in let f = make_elim_fun ([|Some (minfxargs,ref)|],infos) largs in let whfun = whd_construct_state env sigma in - (match reduce_fix_use_function env f whfun (destFix d) lrest with + (match reduce_fix_use_function env sigma f whfun (destFix d) lrest with | NotReducible -> raise Redelimination - | Reduced (c,rest) -> (nf_beta c, rest)) + | Reduced (c,rest) -> (nf_beta sigma c, rest)) | EliminationMutualFix (min,refgoal,refinfos) when stack_args_size largs >= min -> let rec descend ref args = @@ -530,15 +531,15 @@ let rec red_elim_const env sigma ref largs = if ref = refgoal then (c,args) else - let c', lrest = whd_betalet_state (c,args) in + let c', lrest = whd_betalet_state sigma (c,args) in descend (destEvalRef c') lrest in let (_, midargs as s) = descend ref largs in let d, lrest = whd_betadelta_state env sigma s in let f = make_elim_fun refinfos midargs in let whfun = whd_construct_state env sigma in - (match reduce_fix_use_function env f whfun (destFix d) lrest with + (match reduce_fix_use_function env sigma f whfun (destFix d) lrest with | NotReducible -> raise Redelimination - | Reduced (c,rest) -> (nf_beta c, rest)) + | Reduced (c,rest) -> (nf_beta sigma c, rest)) | _ -> raise Redelimination (* reduce to whd normal form or to an applied constant that does not hide @@ -556,11 +557,11 @@ and whd_simpl_state env sigma s = | Cast (c,_,_) -> redrec (c, stack) | Case (ci,p,c,lf) -> (try - redrec (special_red_case sigma env redrec (ci,p,c,lf), stack) + redrec (special_red_case env sigma redrec (ci,p,c,lf), stack) with Redelimination -> s) | Fix fix -> - (try match reduce_fix (whd_construct_state env sigma) fix stack with + (try match reduce_fix (whd_construct_state env) sigma fix stack with | Reduced s' -> redrec s' | NotReducible -> s with Redelimination -> s) @@ -660,7 +661,7 @@ let whd_simpl_orelse_delta_but_fix_old env sigma c = | Cast (c,_,_) -> redrec (c, stack) | Case (ci,p,d,lf) -> (try - redrec (special_red_case sigma env whd_all (ci,p,d,lf), stack) + redrec (special_red_case env sigma whd_all (ci,p,d,lf), stack) with Redelimination -> s) | Fix fix -> @@ -795,7 +796,7 @@ let unfoldoccs env sigma ((nowhere_except_in,locs as plocs),name) c = error ((string_of_evaluable_ref env name)^" does not occur."); let rest = List.filter (fun o -> o >= nbocc) locs in if rest <> [] then error_invalid_occurrence rest; - nf_betaiota uc + nf_betaiota sigma uc (* Unfold reduction tactic: *) let unfoldn loccname env sigma c = @@ -824,10 +825,10 @@ let fold_commands cl env sigma c = (* call by value reduction functions *) let cbv_norm_flags flags env sigma t = - cbv_norm (create_cbv_infos flags env) (nf_evar sigma t) + cbv_norm (create_cbv_infos flags env sigma) t -let cbv_beta = cbv_norm_flags beta empty_env Evd.empty -let cbv_betaiota = cbv_norm_flags betaiota empty_env Evd.empty +let cbv_beta = cbv_norm_flags beta empty_env +let cbv_betaiota = cbv_norm_flags betaiota empty_env let cbv_betadeltaiota env sigma = cbv_norm_flags betadeltaiota env sigma let compute = cbv_betadeltaiota @@ -899,11 +900,11 @@ let one_step_reduce env sigma c = | Cast (c,_,_) -> redrec (c,stack) | Case (ci,p,c,lf) -> (try - (special_red_case sigma env (whd_simpl_state env sigma) + (special_red_case env sigma (whd_simpl_state env sigma) (ci,p,c,lf), stack) with Redelimination -> raise NotStepReducible) | Fix fix -> - (match reduce_fix (whd_construct_state env sigma) fix stack with + (match reduce_fix (whd_construct_state env) sigma fix stack with | Reduced s' -> s' | NotReducible -> raise NotStepReducible) | _ when isEvalRef env x -> @@ -932,7 +933,7 @@ let reduce_to_ref_gen allow_product env sigma ref t = else (* lazily reduces to match the head of [t] with the expected [ref] *) let rec elimrec env t l = - let c, _ = Reductionops.whd_stack t in + let c, _ = Reductionops.whd_stack sigma t in match kind_of_term c with | Prod (n,ty,t') -> if allow_product then @@ -948,7 +949,7 @@ let reduce_to_ref_gen allow_product env sigma ref t = else raise Not_found with Not_found -> try - let t' = nf_betaiota (one_step_reduce env sigma t) in + let t' = nf_betaiota sigma (one_step_reduce env sigma t) in elimrec env t' l with NotStepReducible -> errorlabstrm "" diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 102d918fb..54421f96f 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -268,21 +268,25 @@ let unify_0_with_initial_metas subst conv_at_top env sigma cv_pb flags m n = | Some true -> (match expand_key curenv cf1 with | Some c -> - unirec_rec curenvnb pb b substn (whd_betaiotazeta (mkApp(c,l1))) cN + unirec_rec curenvnb pb b substn + (whd_betaiotazeta sigma (mkApp(c,l1))) cN | None -> (match expand_key curenv cf2 with | Some c -> - unirec_rec curenvnb pb b substn cM (whd_betaiotazeta (mkApp(c,l2))) + unirec_rec curenvnb pb b substn cM + (whd_betaiotazeta sigma (mkApp(c,l2))) | None -> error_cannot_unify curenv sigma (cM,cN))) | Some false -> (match expand_key curenv cf2 with | Some c -> - unirec_rec curenvnb pb b substn cM (whd_betaiotazeta (mkApp(c,l2))) + unirec_rec curenvnb pb b substn cM + (whd_betaiotazeta sigma (mkApp(c,l2))) | None -> (match expand_key curenv cf1 with | Some c -> - unirec_rec curenvnb pb b substn (whd_betaiotazeta (mkApp(c,l1))) cN + unirec_rec curenvnb pb b substn + (whd_betaiotazeta sigma (mkApp(c,l1))) cN | None -> error_cannot_unify curenv sigma (cM,cN))) else @@ -489,7 +493,7 @@ let unify_to_type env evd flags c u = let sigma = evars_of evd in let c = refresh_universes c in let t = get_type_of_with_meta env sigma (metas_of evd) c in - let t = Tacred.hnf_constr env sigma (nf_betaiota (nf_meta evd t)) in + let t = Tacred.hnf_constr env sigma (nf_betaiota sigma (nf_meta evd t)) in let u = Tacred.hnf_constr env sigma u in try unify_0 env sigma Cumul flags t u with e when precatchable_exception e -> ([],[]) @@ -613,11 +617,12 @@ let w_unify_meta_types env ?(flags=default_unify_flags) evd = types of metavars are unifiable with the types of their instances *) let check_types env evd flags subst m n = - if isEvar (fst (whd_stack m)) or isEvar (fst (whd_stack n)) then + let sigma = evars_of evd in + if isEvar (fst (whd_stack sigma m)) or isEvar (fst (whd_stack sigma n)) then unify_0_with_initial_metas subst true env (evars_of evd) topconv flags - (Retyping.get_type_of_with_meta env (evars_of evd) (metas_of evd) m) - (Retyping.get_type_of_with_meta env (evars_of evd) (metas_of evd) n) + (Retyping.get_type_of_with_meta env sigma (metas_of evd) m) + (Retyping.get_type_of_with_meta env sigma (metas_of evd) n) else subst @@ -738,8 +743,8 @@ let secondOrderAbstraction env flags allow_K typ (p, oplist) evd = w_merge env false flags ([p,pred,(ConvUpToEta 0,TypeProcessed)],[]) evd' let w_unify2 env flags allow_K cv_pb ty1 ty2 evd = - let c1, oplist1 = whd_stack ty1 in - let c2, oplist2 = whd_stack ty2 in + let c1, oplist1 = whd_stack (evars_of evd) ty1 in + let c2, oplist2 = whd_stack (evars_of evd) ty2 in match kind_of_term c1, kind_of_term c2 with | Meta p1, _ -> (* Find the predicate *) @@ -777,8 +782,8 @@ let w_unify2 env flags allow_K cv_pb ty1 ty2 evd = Meta(1) had meta-variables in it. *) let w_unify allow_K env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd = let cv_pb = of_conv_pb cv_pb in - let hd1,l1 = whd_stack ty1 in - let hd2,l2 = whd_stack ty2 in + let hd1,l1 = whd_stack (evars_of evd) ty1 in + let hd2,l2 = whd_stack (evars_of evd) ty2 in match kind_of_term hd1, l1<>[], kind_of_term hd2, l2<>[] with (* Pattern case *) | (Meta _, true, Lambda _, _ | Lambda _, _, Meta _, true) diff --git a/proofs/logic.ml b/proofs/logic.ml index 7755efeb5..7424685bc 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -336,7 +336,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = *) match kind_of_term trm with | Meta _ -> - let conclty = nf_betaiota conclty in + let conclty = nf_betaiota sigma conclty in if !check && occur_meta conclty then raise (RefinerError (MetaInType conclty)); (mk_goal hyps conclty)::goalacc, conclty @@ -390,7 +390,7 @@ and mk_hdgoals sigma goal goalacc trm = match kind_of_term trm with | Cast (c,_, ty) when isMeta c -> check_typability env sigma ty; - (mk_goal hyps (nf_betaiota ty))::goalacc,ty + (mk_goal hyps (nf_betaiota sigma ty))::goalacc,ty | Cast (t,_, ty) -> check_typability env sigma ty; @@ -502,7 +502,7 @@ let prim_refiner r sigma goal = raise (RefinerError IntroNeedsProduct)) | Cut (b,replace,id,t) -> - let sg1 = mk_goal sign (nf_betaiota t) in + let sg1 = mk_goal sign (nf_betaiota sigma t) in let sign,cl,sigma = if replace then let nexthyp = get_hyp_after id (named_context_of_val sign) in diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 7240e8b85..7a66067cd 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -763,7 +763,7 @@ let extract_pftreestate pts = else str "Attempt to save a proof with existential variables still non-instantiated"); let env = Global.env_of_context pts.tpf.goal.evar_hyps in - nf_betaiotaevar_preserving_vm_cast env pts.tpfsigma pfterm + nf_betaiota_preserving_vm_cast env pts.tpfsigma pfterm (* strong whd_betaiotaevar env pts.tpfsigma pfterm *) (*** local_strong (Evarutil.whd_ise (ts_it pts.tpfsigma)) pfterm diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 45bd0c896..19ea5c398 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -99,7 +99,7 @@ let pf_whd_betadeltaiota_stack = pf_reduce whd_betadeltaiota_stack let pf_hnf_constr = pf_reduce hnf_constr let pf_red_product = pf_reduce red_product let pf_nf = pf_reduce nf -let pf_nf_betaiota = pf_reduce (fun _ _ -> nf_betaiota) +let pf_nf_betaiota = pf_reduce (fun _ -> nf_betaiota) let pf_compute = pf_reduce compute let pf_unfoldn ubinds = pf_reduce (unfoldn ubinds) let pf_type_of = pf_reduce type_of diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 4eb20cb53..9d8b6c3b5 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -650,14 +650,14 @@ let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a Lazy. | Prod (na, ty, b), obj :: cstrs -> if dependent (mkRel 1) b then let (b, arg, evars) = aux (Environ.push_rel (na, None, ty) env) b cstrs in - let ty = Reductionops.nf_betaiota ty in + let ty = Reductionops.nf_betaiota (Evd.evars_of !isevars) ty in let pred = mkLambda (na, ty, b) in let liftarg = mkLambda (na, ty, arg) in let arg' = mkApp (Lazy.force forall_relation, [| ty ; pred ; liftarg |]) in mkProd(na, ty, b), arg', (ty, None) :: evars else let (b', arg, evars) = aux env (subst1 mkProp b) cstrs in - let ty = Reductionops.nf_betaiota ty in + let ty = Reductionops.nf_betaiota(Evd.evars_of !isevars) ty in let relty = mk_relty ty obj in let newarg = mkApp (Lazy.force respectful, [| ty ; b' ; relty ; arg |]) in mkProd(na, ty, b), newarg, (ty, Some relty) :: evars @@ -665,7 +665,7 @@ let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a Lazy. | _, [] -> (match finalcstr with None -> - let t = Reductionops.nf_betaiota ty in + let t = Reductionops.nf_betaiota(Evd.evars_of !isevars) ty in let rel = mk_relty t None in t, rel, [t, Some rel] | Some codom -> let (t, rel) = Lazy.force codom in diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml index 7e25b072e..967bc88e8 100644 --- a/tactics/decl_proof_instr.ml +++ b/tactics/decl_proof_instr.ml @@ -1093,7 +1093,7 @@ let thesis_for obj typ per_info env= ((Printer.pr_constr_env env obj) ++ spc () ++ str "cannot give an induction hypothesis (wrong parameters).") in let hd2 = (applist ((lift (List.length rc) per_info.per_pred),args@[obj])) in - compose_prod rc (whd_beta hd2) + compose_prod rc (whd_beta Evd.empty hd2) let rec build_product_dep pat_info per_info args body gls = match args with @@ -1225,7 +1225,7 @@ let hrec_for fix_id per_info gls obj_id = try List.for_all2 eq_constr params per_info.per_params with Invalid_argument _ -> false end; let hd2 = applist (mkVar fix_id,args@[obj]) in - compose_lam rc (whd_beta hd2) + compose_lam rc (whd_beta gls.sigma hd2) let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = match tree, objs with diff --git a/tactics/equality.ml b/tactics/equality.ml index 721623c91..dd9f648ca 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -120,7 +120,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs ((c,l) : open_constr with_ let sigma, c' = c in let sigma = Evd.merge sigma (project gl) in let ctype = get_type_of env sigma c' in - let rels, t = decompose_prod (whd_betaiotazeta ctype) in + let rels, t = decompose_prod (whd_betaiotazeta sigma ctype) in match match_with_equality_type t with | Some (hdcncl,args) -> (* Fast path: direct leibniz rewrite *) let lft2rgt = adjust_rewriting_direction args lft2rgt in @@ -739,7 +739,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = else error "Cannot solve an unification problem." else - let (a,p_i_minus_1) = match whd_beta_stack p_i with + let (a,p_i_minus_1) = match whd_beta_stack (evars_of !evdref) p_i with | (_sigS,[a;p]) -> (a,p) | _ -> anomaly "sig_clausal_form: should be a sigma type" in let ev = Evarutil.e_new_evar evdref env a in diff --git a/tactics/leminv.ml b/tactics/leminv.ml index c1f20e8c3..1046ecbf0 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -237,7 +237,8 @@ let inversion_scheme env sigma t sort dep_option inv_op = meta_types in let invProof = - it_mkNamedLambda_or_LetIn (local_strong (whd_meta mvb) pfterm) ownSign + it_mkNamedLambda_or_LetIn + (local_strong (fun _ -> whd_meta mvb) Evd.empty pfterm) ownSign in invProof diff --git a/tactics/tactics.ml b/tactics/tactics.ml index caef1c94a..527b66c9e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -753,7 +753,7 @@ let general_apply with_delta with_destruct with_evars (c,lbind) gl0 = let concl_nprod = nb_prod (pf_concl gl0) in let evm, c = c in let rec try_main_apply c gl = - let thm_ty0 = nf_betaiota (pf_type_of gl c) in + let thm_ty0 = nf_betaiota (project gl) (pf_type_of gl c) in let try_apply thm_ty nprod = let n = nb_prod thm_ty - nprod in if n<0 then error "Applied theorem has not enough premisses."; @@ -844,7 +844,7 @@ let progress_with_clause flags innerclause clause = with Failure _ -> error "Unable to unify." let apply_in_once_main flags innerclause (d,lbind) gl = - let thm = nf_betaiota (pf_type_of gl d) in + let thm = nf_betaiota gl.sigma (pf_type_of gl d) in let rec aux clause = try progress_with_clause flags innerclause clause with err -> @@ -979,7 +979,8 @@ let specialize mopt (c,lbind) g = else let clause = make_clenv_binding g (c,pf_type_of g c) lbind in let clause = clenv_unify_meta_types clause in - let (thd,tstack) = whd_stack (clenv_value clause) in + let (thd,tstack) = + whd_stack (evars_of clause.evd) (clenv_value clause) in let nargs = List.length tstack in let tstack = match mopt with | Some m -> |