diff options
| -rw-r--r-- | pretyping/cases.ml | 44 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 12 | ||||
| -rw-r--r-- | pretyping/evarutil.mli | 10 | ||||
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2615.v | 6 |
4 files changed, 56 insertions, 16 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index b104db0267..6559084578 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1298,6 +1298,10 @@ let adjust_to_extended_env_and_remove_deps env extenv subst t = let push_binder d (k,env,subst) = (k+1,push_rel d env,List.map (fun (na,u,d) -> (na,lift 1 u,d)) subst) +let rec list_assoc_in_triple x = function + [] -> raise Not_found + | (a,b,_)::l -> if compare a x = 0 then b else list_assoc_in_triple x l + (* Let vijk and ti be a set of dependent terms and T a type, all * defined in some environment env. The vijk and ti are supposed to be * instances for variables aijk and bi. @@ -1323,20 +1327,33 @@ let abstract_tycon loc env evdref subst _tycon extenv t = by an evar that may depend (and only depend) on the corresponding convertible subterms of the substitution *) let rec aux (k,env,subst as x) t = - if isRel t && pi2 (lookup_rel (destRel t) env) <> None then - map_constr_with_full_binders push_binder aux x t - else + let t = whd_evar !evdref t in match kind_of_term t with + | Rel n when pi2 (lookup_rel n env) <> None -> + map_constr_with_full_binders push_binder aux x t + | Evar ev -> + let ty = get_type_of env sigma t in + let inst = + list_map_i + (fun i _ -> + try list_assoc_in_triple i subst0 with Not_found -> mkRel i) + 1 (rel_context env) in + let ev = e_new_evar evdref env ~src:(loc, CasesType) ty in + evdref := add_conv_pb (Reduction.CONV,env,substl inst ev,t) !evdref; + ev + | _ -> let good = List.filter (fun (_,u,_) -> is_conv_leq env sigma t u) subst in if good <> [] then - let u = pi3 (List.hd good) in - let ty = aux x (get_type_of env sigma t) in + let u = pi3 (List.hd good) in (* u is in extenv *) let vl = List.map pi1 good in + let ty = lift (-k) (aux x (get_type_of env !evdref t)) in + let depvl = free_rels ty in let inst = list_map_i (fun i _ -> if List.mem i vl then u else mkRel i) 1 (rel_context extenv) in let rel_filter = - List.map (fun a -> not (isRel a) or dependent a u) inst in + List.map (fun a -> not (isRel a) || dependent a u + || Intset.mem (destRel a) depvl) inst in let named_filter = List.map (fun (id,_,_) -> dependent (mkVar id) u) (named_context extenv) in @@ -1350,17 +1367,22 @@ let abstract_tycon loc env evdref subst _tycon extenv t = aux (0,extenv,subst0) t0 let build_tycon loc env tycon_env subst tycon extenv evdref t = - let t = match t with + let t,tt = match t with | None -> (* This is the situation we are building a return predicate and we are in an impossible branch *) let n = rel_context_length (rel_context env) in let n' = rel_context_length (rel_context tycon_env) in + let tt = new_Type () in let impossible_case_type = - e_new_evar evdref env ~src:(loc,ImpossibleCase) (new_Type ()) in - lift (n'-n) impossible_case_type - | Some t -> abstract_tycon loc tycon_env evdref subst tycon extenv t in - get_judgment_of extenv !evdref t + e_new_evar evdref env ~src:(loc,ImpossibleCase) tt in + (lift (n'-n) impossible_case_type, tt) + | Some t -> + let t = abstract_tycon loc tycon_env evdref subst tycon extenv t in + let evd,tt = Typing.e_type_of extenv !evdref t in + evdref := evd; + (t,tt) in + { uj_val = t; uj_type = tt } (* For a multiple pattern-matching problem Xi on t1..tn with return * type T, [build_inversion_problem Gamma Sigma (t1..tn) T] builds a return diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 993cb3a850..7683778938 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -464,11 +464,8 @@ let define_evar_from_virtual_equation define_fun env evd t_in_env sign filter in * substitution u1..uq. *) -let materialize_evar define_fun env evd k (evk1,args1) ty = - let evi1 = Evd.find_undefined evd evk1 in +let materialize_evar_from_sign define_fun env evd k sign1 filter1 args1 ty = let env1,rel_sign = env_rel_context_chop k env in - let sign1 = evar_hyps evi1 in - let filter1 = evar_filter evi1 in let ids1 = List.map pi1 (named_context_of_val sign1) in let inst_in_sign = List.map mkVar (snd (list_filter2 (fun b id -> b) (filter1,ids1))) in @@ -487,7 +484,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty = (sign,filter,inst_in_env,inst_in_sign, push_rel d env,evd,avoid)) rel_sign - (sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,ids1) + (sign1,filter1,args1,inst_in_sign,env1,evd,ids1) in let evd,ev2ty_in_sign = define_evar_from_virtual_equation define_fun env evd ty @@ -497,6 +494,11 @@ let materialize_evar define_fun env evd k (evk1,args1) ty = let ev2_in_env = (fst (destEvar ev2_in_sign), Array.of_list inst2_in_env) in (evd, ev2_in_sign, ev2_in_env) +let materialize_evar define_fun env evd k (evk1,args1) ty = + let evi1 = Evd.find_undefined evd evk1 in + materialize_evar_from_sign define_fun env evd k + (evar_hyps evi1) (evar_filter evi1) (Array.to_list args1) ty + let subfilter env ccl filter newfilter args = let vars = collect_vars ccl in let (filter, _, _, newargs) = diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 3652768531..54fc072659 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -62,6 +62,16 @@ type conv_fun = val evar_define : conv_fun -> ?choose:bool -> env -> evar_map -> existential -> constr -> evar_map +val materialize_evar_from_sign : + (env -> evar_map -> existential -> constr -> evar_map) -> + env -> evar_map -> int -> + named_context_val -> bool list -> constr list -> types -> + evar_map * constr * existential + +val solve_evar_evar : + (env -> evar_map -> existential -> constr -> evar_map) -> + env -> evar_map -> existential -> existential -> evar_map + (** {6 Evars/Metas switching...} *) (** [evars_to_metas] generates new metavariables for each non dependent diff --git a/test-suite/bugs/closed/shouldsucceed/2615.v b/test-suite/bugs/closed/shouldsucceed/2615.v index 005491637d..54e1a07cc8 100644 --- a/test-suite/bugs/closed/shouldsucceed/2615.v +++ b/test-suite/bugs/closed/shouldsucceed/2615.v @@ -6,3 +6,9 @@ Inductive foo : forall A, A -> Prop := Lemma bar A B f : foo (A -> B) f -> forall x : A, foo B (f x). Fail induction 1. +(* Whether these examples should succeed with a non-dependent return predicate + or fail because there is well-typed return predicate dependent in f + is questionable. As of 25 oct 2011, they succeed *) +refine (fun p => match p with _ => _ end). +Undo. +refine (fun p => match p with foo_intro _ _ => _ end). |