From a0a94c1340a63cdb824507b973393882666ba52a Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 19 Feb 2009 13:13:14 +0100 Subject: Imported Upstream version 8.2-1+dfsg --- pretyping/cases.ml | 12 ++- pretyping/cbv.ml | 12 ++- pretyping/cbv.mli | 4 +- pretyping/classops.ml | 4 +- pretyping/clenv.ml | 8 +- pretyping/evarconv.ml | 35 ++++--- pretyping/evarutil.ml | 26 +++-- pretyping/indrec.ml | 6 +- pretyping/reductionops.ml | 232 ++++++++++++++++++++------------------------- pretyping/reductionops.mli | 27 +++--- pretyping/retyping.ml | 6 +- pretyping/tacred.ml | 63 ++++++------ pretyping/unification.ml | 31 +++--- 13 files changed, 237 insertions(+), 229 deletions(-) (limited to 'pretyping') diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 52b73535..a4880f5e 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cases.ml 11708 2008-12-20 10:50:20Z msozeau $ *) +(* $Id: cases.ml 11897 2009-02-09 19:28:02Z barras $ *) open Util open Names @@ -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 2a01e901..f4c612a5 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cbv.ml 8802 2006-05-10 20:47:28Z barras $ *) +(* $Id: cbv.ml 11897 2009-02-09 19:28:02Z barras $ *) open Util open Pp @@ -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 8c969e2c..9ab15886 100644 --- a/pretyping/cbv.mli +++ b/pretyping/cbv.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: cbv.mli 8799 2006-05-09 21:15:07Z barras $ i*) +(*i $Id: cbv.mli 11897 2009-02-09 19:28:02Z barras $ i*) (*i*) open Names @@ -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 398da529..27418b4d 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: classops.ml 11343 2008-09-01 20:55:13Z herbelin $ *) +(* $Id: classops.ml 11897 2009-02-09 19:28:02Z barras $ *) open Util open Pp @@ -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 8dfec2be..51952f4f 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: clenv.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: clenv.ml 11897 2009-02-09 19:28:02Z barras $ *) open Pp open Util @@ -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 58369811..4c5ebe3e 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evarconv.ml 11745 2009-01-04 18:43:08Z herbelin $ *) +(* $Id: evarconv.ml 11897 2009-02-09 19:28:02Z barras $ *) open Pp open Util @@ -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 @@ -164,18 +164,25 @@ let rec evar_conv_x env evd pbty term1 term2 = (* Maybe convertible but since reducing can erase evars which [evar_apprec] could have found, we do it only if the terms are free of evar. Note: incomplete heuristic... *) - if is_ground_term evd term1 && is_ground_term evd term2 - && is_ground_env evd env - then (evd, is_fconv pbty env (evars_of evd) term1 term2) - else - let term1 = apprec_nohdbeta env evd term1 in - let term2 = apprec_nohdbeta env evd term2 in - if is_undefined_evar evd term1 then - solve_simple_eqn evar_conv_x env evd (pbty,destEvar term1,term2) - else if is_undefined_evar evd term2 then - solve_simple_eqn evar_conv_x env evd (pbty,destEvar term2,term1) - else - evar_eqappr_x env evd pbty (decompose_app term1) (decompose_app term2) + let ground_test = + if is_ground_term evd term1 && is_ground_term evd term2 then + if is_fconv pbty env (evars_of evd) term1 term2 then + Some true + else if is_ground_env evd env then Some false + else None + else None in + match ground_test with + Some b -> (evd,b) + | None -> + let term1 = apprec_nohdbeta env evd term1 in + let term2 = apprec_nohdbeta env evd term2 in + if is_undefined_evar evd term1 then + solve_simple_eqn evar_conv_x env evd (pbty,destEvar term1,term2) + else if is_undefined_evar evd term2 then + solve_simple_eqn evar_conv_x env evd (pbty,destEvar term2,term1) + else + evar_eqappr_x env evd pbty + (decompose_app term1) (decompose_app term2) and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = (* Evar must be undefined since we have whd_ised *) diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index b418f996..c0c0b941 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evarutil.ml 11819 2009-01-20 20:04:50Z herbelin $ *) +(* $Id: evarutil.ml 11897 2009-02-09 19:28:02Z barras $ *) open Util open Pp @@ -119,7 +119,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 = @@ -906,7 +906,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) @@ -959,9 +959,19 @@ and evar_define env (evk,_ as ev) rhs evd = (* Auxiliary functions for the conversion algorithms modulo evars *) -let has_undefined_evars evd t = - try let _ = local_strong (whd_ise (evars_of evd)) t in false - with Uninstantiated_evar _ -> true +let has_undefined_evars evd t = + let evm = evars_of evd in + let rec has_ev t = + match kind_of_term t with + Evar (ev,args) -> + (match evar_body (Evd.find evm ev) with + | Evar_defined c -> + has_ev c; Array.iter has_ev args + | Evar_empty -> + raise NotInstantiatedEvar) + | _ -> iter_constr has_ev t in + try let _ = has_ev t in false + with (Not_found | NotInstantiatedEvar) -> true let is_ground_term evd t = not (has_undefined_evars evd t) @@ -972,6 +982,9 @@ let is_ground_env evd env = | _ -> true in List.for_all is_ground_decl (rel_context env) && List.for_all is_ground_decl (named_context env) +(* Memoization is safe since evar_map and environ are applicative + structures *) +let is_ground_env = memo1_2 is_ground_env let head_evar = let rec hrec c = match kind_of_term c with @@ -1012,6 +1025,7 @@ let is_unification_pattern_evar env (_,args) l t = l else (* Probably strong restrictions coming from t being evar-closed *) + let t = expand_vars_in_term env t in let fv_rels = free_rels t in let fv_ids = global_vars env t in List.filter (fun c -> diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index d3123eb6..88a0c2a6 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: indrec.ml 11735 2009-01-02 17:22:31Z herbelin $ *) +(* $Id: indrec.ml 11897 2009-02-09 19:28:02Z barras $ *) open Pp open Util @@ -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 a1603d69..33928f67 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: reductionops.ml 11796 2009-01-18 13:41:39Z herbelin $ *) +(* $Id: reductionops.ml 11897 2009-02-09 19:28:02Z barras $ *) open Pp open Util @@ -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_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_state sigma (x, stack as s) = match kind_of_term x with - | App (f,cl) -> whd_state (f, append_stack cl stack) - | Cast (c,_,_) -> whd_state (c, stack) + | App (f,cl) -> whd_state sigma (f, append_stack cl stack) + | Cast (c,_,_) -> whd_state sigma (c, stack) + | Evar ev -> + (match safe_evar_value sigma ev with + Some c -> whd_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_state (x, empty_stack)) +let whd_stack sigma x = + appterm_of_stack (whd_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 @@ -211,14 +219,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 @@ -229,20 +235,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] @@ -303,11 +305,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') @@ -333,8 +335,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 -> @@ -375,7 +377,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) @@ -383,7 +385,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 @@ -418,105 +420,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 *) @@ -526,24 +514,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 | _ -> collapse_appl 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 @@ -553,7 +542,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) -> @@ -568,7 +557,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) -> @@ -594,12 +583,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 *) @@ -627,23 +618,9 @@ let pb_equal = function let sort_cmp = sort_cmp - -let nf_red_env sigma env = - let nf_decl = function - (x,Some t,ty) -> (x,Some (nf_evar sigma t),ty) - | d -> d in - let sign = named_context env in - let ctxt = rel_context env in - let env = reset_context env in - let env = Sign.fold_named_context - (fun d env -> push_named (nf_decl d) env) ~init:env sign in - Sign.fold_rel_context - (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 @@ -729,7 +706,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] @@ -830,7 +808,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 @@ -840,7 +818,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 @@ -882,7 +860,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 @@ -952,7 +930,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 c026d9fe..8b3657c7 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: reductionops.mli 11343 2008-09-01 20:55:13Z herbelin $ i*) +(*i $Id: reductionops.mli 11897 2009-02-09 19:28:02Z barras $ i*) (*i*) open Names @@ -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 2465bd1e..19e46a47 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: retyping.ml 11778 2009-01-13 13:17:39Z msozeau $ *) +(* $Id: retyping.ml 11897 2009-02-09 19:28:02Z barras $ *) open Util open Term @@ -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 88a6f499..740b2ca8 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacred.ml 11654 2008-12-03 18:39:40Z barras $ *) +(* $Id: tacred.ml 11897 2009-02-09 19:28:02Z barras $ *) open Pp open Util @@ -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 981a5605..fb29196c 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: unification.ml 11819 2009-01-20 20:04:50Z herbelin $ *) +(* $Id: unification.ml 11897 2009-02-09 19:28:02Z barras $ *) open Pp open Util @@ -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) -- cgit v1.2.3