From bf12eb93f3f6a6a824a10878878fadd59745aae0 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sat, 29 Dec 2012 10:57:43 +0100 Subject: Imported Upstream version 8.4pl1dfsg --- pretyping/cases.ml | 2 +- pretyping/detyping.ml | 2 ++ pretyping/evarutil.ml | 42 +++++++++++++++++++++-------------- pretyping/glob_term.ml | 34 ++++++++++++++++++++++++++-- pretyping/typing.ml | 9 ++++++-- pretyping/unification.ml | 56 ++++++++++++++++++----------------------------- pretyping/unification.mli | 1 + 7 files changed, 90 insertions(+), 56 deletions(-) (limited to 'pretyping') diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 1819dc52..38355cf1 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1763,7 +1763,7 @@ let prepare_predicate loc typing_fun sigma env tomatchs arsign tycon pred = (* First strategy: we build an "inversion" predicate *) let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in (* Second strategy: we directly use the evar as a non dependent pred *) - let pred2 = lift (List.length arsign) t in + let pred2 = lift (List.length (List.flatten arsign)) t in [sigma1, pred1; sigma, pred2] (* Some type annotation *) | Some rtntyp, _ -> diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 69ff2af9..a74e4cb4 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -389,6 +389,8 @@ let rec detype (isgoal:bool) avoid env t = with _ -> GVar (dl, id)) | Sort s -> GSort (dl,detype_sort s) + | Cast (c1,REVERTcast,c2) when not !Flags.raw_print -> + detype isgoal avoid env c1 | Cast (c1,k,c2) -> GCast(dl,detype isgoal avoid env c1, CastConv (k, detype isgoal avoid env c2)) | Prod (na,ty,c) -> detype_binder isgoal BProd avoid env na ty c diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index fa29243a..b0248a84 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -135,15 +135,20 @@ let whd_head_evar_stack sigma c = let whd_head_evar sigma c = applist (whd_head_evar_stack sigma c) -let noccur_evar evd evk c = - let rec occur_rec c = match kind_of_term c with - | Evar (evk',_ as ev') -> +let noccur_evar env evd evk c = + let rec occur_rec k c = match kind_of_term c with + | Evar (evk',args' as ev') -> (match safe_evar_value evd ev' with - | Some c -> occur_rec c - | None -> if evk = evk' then raise Occur) - | _ -> iter_constr occur_rec c + | Some c -> occur_rec k c + | None -> + if evk = evk' then raise Occur else Array.iter (occur_rec k) args') + | Rel i when i > k -> + (match pi2 (Environ.lookup_rel (i-k) env) with + | None -> () + | Some b -> occur_rec k (lift i b)) + | _ -> iter_constr_with_binders succ occur_rec k c in - try occur_rec c; true with Occur -> false + try occur_rec 0 c; true with Occur -> false let normalize_evar evd ev = match kind_of_term (whd_evar evd (mkEvar ev)) with @@ -741,7 +746,8 @@ let is_unification_pattern_meta env nb m l t = None let is_unification_pattern_evar env evd (evk,args) l t = - if List.for_all (fun x -> isRel x || isVar x) l & noccur_evar evd evk t then + if List.for_all (fun x -> isRel x || isVar x) l & noccur_evar env evd evk t + then let args = remove_instance_local_defs evd evk (Array.to_list args) in let n = List.length args in match find_unification_pattern_args env (args @ l) t with @@ -1112,10 +1118,11 @@ let invert_arg_from_subst evd aliases k0 subst_in_env_extended_with_k_binders c_ | Not_found -> CannotInvert | NotUnique -> Invertible NoUniqueProjection -let invert_arg evd aliases k evk subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders = +let invert_arg fullenv evd aliases k evk subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders = let res = invert_arg_from_subst evd aliases k subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders in match res with - | Invertible (UniqueProjection (c,_)) when not (noccur_evar evd evk c) -> + | Invertible (UniqueProjection (c,_)) when not (noccur_evar fullenv evd evk c) + -> CannotInvert | _ -> res @@ -1153,10 +1160,11 @@ let extract_candidates sols = let filter_of_projection = function Invertible _ -> true | _ -> false -let invert_invertible_arg evd aliases k (evk,argsv) args' = +let invert_invertible_arg fullenv evd aliases k (evk,argsv) args' = let evi = Evd.find_undefined evd evk in let subst,_ = make_projectable_subst aliases evd evi argsv in - let projs = array_map_to_list (invert_arg evd aliases k evk subst) args' in + let projs = + array_map_to_list (invert_arg fullenv evd aliases k evk subst) args' in Array.of_list (extract_unique_projections projs) (* Redefines an evar with a smaller context (i.e. it may depend on less @@ -1364,12 +1372,14 @@ let has_constrainable_free_vars evd aliases k ev (fv_rels,fv_ids as fvs) t = let ensure_evar_independent g env evd (evk1,argsv1 as ev1) (evk2,argsv2 as ev2)= let filter1 = - restrict_upon_filter evd evk1 (noccur_evar evd evk2) (Array.to_list argsv1) + restrict_upon_filter evd evk1 (noccur_evar env evd evk2) + (Array.to_list argsv1) in let candidates1 = restrict_candidates g env evd filter1 ev1 ev2 in let evd,(evk1,_ as ev1) = do_restrict_hyps evd ev1 filter1 candidates1 in let filter2 = - restrict_upon_filter evd evk2 (noccur_evar evd evk1) (Array.to_list argsv2) + restrict_upon_filter evd evk2 (noccur_evar env evd evk1) + (Array.to_list argsv2) in let candidates2 = restrict_candidates g env evd filter2 ev2 ev1 in let evd,ev2 = do_restrict_hyps evd ev2 filter2 candidates2 in @@ -1389,7 +1399,7 @@ let project_evar_on_evar g env evd aliases k2 (evk1,argsv1 as ev1) (evk2,argsv2 try let candidates1 = restrict_candidates g env evd filter1 ev1 ev2 in let evd,(evk1',args1) = do_restrict_hyps evd ev1 filter1 candidates1 in - evd,mkEvar (evk1',invert_invertible_arg evd aliases k2 ev2 args1) + evd,mkEvar (evk1',invert_invertible_arg env evd aliases k2 ev2 args1) with | EvarSolvedWhileRestricting (evd,ev1) -> raise (EvarSolvedOnTheFly (evd,ev1)) @@ -1585,7 +1595,7 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs = let aliases = lift_aliases k aliases in (try let ev = (evk,Array.map (lift k) argsv) in - let evd,body = project_evar_on_evar conv_algo env !evdref aliases k ev' ev in + let evd,body = project_evar_on_evar conv_algo env' !evdref aliases k ev' ev in evdref := evd; body with diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 24c5ba5b..8e4b211f 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -346,8 +346,38 @@ let rec cases_pattern_of_glob_constr na = function | GHole (loc,_) -> PatVar (loc,na) | GRef (loc,ConstructRef cstr) -> PatCstr (loc,cstr,[],na) - | GApp (loc,GRef (_,ConstructRef cstr),l) -> - PatCstr (loc,cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na) + | GApp (loc,GRef (_,ConstructRef (ind,_ as cstr)),args) -> + let mib,_ = Global.lookup_inductive ind in + let nparams = mib.Declarations.mind_nparams in + if nparams > List.length args then + user_err_loc (loc,"",Pp.str "Invalid notation for pattern."); + let params,args = list_chop nparams args in + List.iter (function GHole _ -> () + | _ -> user_err_loc (loc,"",Pp.str"Invalid notation for pattern.")) + params; + let args = List.map (cases_pattern_of_glob_constr Anonymous) args in + PatCstr (loc,cstr,args,na) + | _ -> raise Not_found + +let rec cases_pattern_of_glob_constr na = function + | GVar (loc,id) when na<>Anonymous -> + (* Unable to manage the presence of both an alias and a variable *) + raise Not_found + | GVar (loc,id) -> PatVar (loc,Name id) + | GHole (loc,_) -> PatVar (loc,na) + | GRef (loc,ConstructRef cstr) -> + PatCstr (loc,cstr,[],na) + | GApp (loc,GRef (_,ConstructRef (ind,_ as cstr)),args) -> + let mib,_ = Global.lookup_inductive ind in + let nparams = mib.Declarations.mind_nparams in + if nparams > List.length args then + user_err_loc (loc,"",Pp.str "Invalid notation for pattern."); + let params,args = list_chop nparams args in + List.iter (function GHole _ -> () + | _ -> user_err_loc (loc,"",Pp.str"Invalid notation for pattern.")) + params; + let args = List.map (cases_pattern_of_glob_constr Anonymous) args in + PatCstr (loc,cstr,args,na) | _ -> raise Not_found (* Turn a closed cases pattern into a glob_constr *) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 665491e7..22aacb29 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -42,6 +42,11 @@ let e_type_judgment env evdref j = evdref := evd; { utj_val = j.uj_val; utj_type = s } | _ -> error_not_type env j +let e_assumption_of_judgment env evdref j = + try (e_type_judgment env evdref j).utj_val + with TypeError _ -> + error_assumption env j + let e_judge_of_apply env evdref funj argjv = let rec apply_rec n typ = function | [] -> @@ -150,7 +155,7 @@ let rec execute env evdref cstr = | Evar ev -> let ty = Evd.existential_type !evdref ev in let jty = execute env evdref (whd_evar !evdref ty) in - let jty = assumption_of_judgment env jty in + let jty = e_assumption_of_judgment env evdref jty in { uj_val = cstr; uj_type = jty } | Rel n -> @@ -243,7 +248,7 @@ let rec execute env evdref cstr = and execute_recdef env evdref (names,lar,vdef) = let larj = execute_array env evdref lar in - let lara = Array.map (assumption_of_judgment env) larj in + let lara = Array.map (e_assumption_of_judgment env evdref) larj in let env1 = push_rec_types (names,lara,vdef) env in let vdefj = execute_array env1 evdref vdef in let vdefv = Array.map j_val vdefj in diff --git a/pretyping/unification.ml b/pretyping/unification.ml index c92c183d..63cdb378 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -198,11 +198,18 @@ type unify_flags = { (* (and activated for apply, rewrite but not auto since Feb 2008 for 8.2) *) modulo_delta : Names.transparent_state; - (* This controls which constant are unfoldable; this is on for apply *) + (* This controls which constants are unfoldable; this is on for apply *) (* (but not simple apply) since Feb 2008 for 8.2 *) modulo_delta_types : Names.transparent_state; + modulo_delta_in_merge : Names.transparent_state option; + (* This controls whether unfoldability is different when trying to unify *) + (* several instances of the same metavariable *) + (* Typical situation is when we give a pattern to be matched *) + (* syntactically against a subterm but we want the metas of the *) + (* pattern to be modulo convertibility *) + check_applied_meta_types : bool; (* This controls whether meta's applied to arguments have their *) (* type unified with the type of their instance *) @@ -240,12 +247,13 @@ type unify_flags = { } (* Default flag for unifying a type against a type (e.g. apply) *) -(* We set all conversion flags *) +(* We set all conversion flags (no flag should be modified anymore) *) let default_unify_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; use_metas_eagerly_in_conv_on_closed_terms = true; modulo_delta = full_transparent_state; modulo_delta_types = full_transparent_state; + modulo_delta_in_merge = None; check_applied_meta_types = true; resolve_evars = false; use_pattern_unification = true; @@ -258,24 +266,22 @@ let default_unify_flags = { (* in fact useless when not used in w_unify_to_subterm_list *) } +let set_merge_flags flags = + match flags.modulo_delta_in_merge with + | None -> flags + | Some ts -> + { flags with modulo_delta = ts; modulo_conv_on_closed_terms = Some ts } + (* Default flag for the "simple apply" version of unification of a *) (* type against a type (e.g. apply) *) (* We set only the flags available at the time the new "apply" extends *) (* out of "simple apply" *) -let default_no_delta_unify_flags = { - modulo_conv_on_closed_terms = Some full_transparent_state; - use_metas_eagerly_in_conv_on_closed_terms = true; +let default_no_delta_unify_flags = { default_unify_flags with modulo_delta = empty_transparent_state; - modulo_delta_types = full_transparent_state; check_applied_meta_types = false; - resolve_evars = false; use_pattern_unification = false; use_meta_bound_pattern_unification = true; - frozen_evars = ExistentialSet.empty; - restrict_conv_on_strict_subterms = false; modulo_betaiota = false; - modulo_eta = true; - allow_K_in_toplevel_higher_order_unification = false } (* Default flags for looking for subterms in elimination tactics *) @@ -283,36 +289,16 @@ let default_no_delta_unify_flags = { (* allow_K) because only closed terms are involved in *) (* induction/destruct/case/elim and w_unify_to_subterm_list does not *) (* call w_unify for induction/destruct/case/elim (13/6/2011) *) -let elim_flags = { - modulo_conv_on_closed_terms = Some full_transparent_state; - use_metas_eagerly_in_conv_on_closed_terms = true; - modulo_delta = full_transparent_state; - modulo_delta_types = full_transparent_state; - check_applied_meta_types = true; - resolve_evars = false; - use_pattern_unification = true; - use_meta_bound_pattern_unification = true; - frozen_evars = ExistentialSet.empty; +let elim_flags = { default_unify_flags with restrict_conv_on_strict_subterms = false; (* ? *) modulo_betaiota = false; - modulo_eta = true; allow_K_in_toplevel_higher_order_unification = true } -let elim_no_delta_flags = { - modulo_conv_on_closed_terms = Some full_transparent_state; - use_metas_eagerly_in_conv_on_closed_terms = true; +let elim_no_delta_flags = { elim_flags with modulo_delta = empty_transparent_state; - modulo_delta_types = full_transparent_state; check_applied_meta_types = false; - resolve_evars = false; use_pattern_unification = false; - use_meta_bound_pattern_unification = true; - frozen_evars = ExistentialSet.empty; - restrict_conv_on_strict_subterms = false; (* ? *) - modulo_betaiota = false; - modulo_eta = true; - allow_K_in_toplevel_higher_order_unification = true } let set_no_head_reduction flags = @@ -865,7 +851,7 @@ let w_merge env with_types flags (evd,metas,evars) = if Evd.is_defined evd evk then let v = Evd.existential_value evd ev in let (evd,metas',evars'') = - unify_0 curenv evd CONV flags rhs v in + unify_0 curenv evd CONV (set_merge_flags flags) rhs v in w_merge_rec evd (metas'@metas) (evars''@evars') eqns else begin (* This can make rhs' ill-typed if metas are *) @@ -943,7 +929,7 @@ let w_merge env with_types flags (evd,metas,evars) = let sp_env = Global.env_of_context ev.evar_hyps in let (evd', c) = applyHead sp_env evd nargs hdc in let (evd'',mc,ec) = - unify_0 sp_env evd' CUMUL flags + unify_0 sp_env evd' CUMUL (set_merge_flags flags) (get_type_of sp_env evd' c) ev.evar_concl in let evd''' = w_merge_rec evd'' mc ec [] in if evd' == evd''' diff --git a/pretyping/unification.mli b/pretyping/unification.mli index e3fd46af..1ec5c1a2 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -15,6 +15,7 @@ type unify_flags = { use_metas_eagerly_in_conv_on_closed_terms : bool; modulo_delta : Names.transparent_state; modulo_delta_types : Names.transparent_state; + modulo_delta_in_merge : Names.transparent_state option; check_applied_meta_types : bool; resolve_evars : bool; use_pattern_unification : bool; -- cgit v1.2.3