From 7c7726a798caa6b506a727703de24d2bb5bb3956 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 7 Jul 2015 17:04:45 +0200 Subject: Univs: bug fix. Missing universe substitutions of mind_params_ctxt when typechecking cases, which appeared only when let-ins were used. --- pretyping/inductiveops.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'pretyping') diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 90aa8000a8..cb091f2d6f 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -322,7 +322,8 @@ let instantiate_params t args sign = let get_constructor ((ind,u as indu),mib,mip,params) j = assert (j <= Array.length mip.mind_consnames); let typi = mis_nf_constructor_type (indu,mib,mip) j in - let typi = instantiate_params typi params mib.mind_params_ctxt in + let ctx = Vars.subst_instance_context u mib.mind_params_ctxt in + let typi = instantiate_params typi params ctx in let (args,ccl) = decompose_prod_assum typi in let (_,allargs) = decompose_app ccl in let vargs = List.skipn (List.length params) allargs in -- cgit v1.2.3 From 1bf30962d7cd5732393d7722ae6d263d4c812ec8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 9 Jul 2015 10:32:17 +0200 Subject: Make retyping of projections more resilient to wrong environment. Unfortunately, it seems that retyping can be called in ill-typed terms and/or in the wrong environment. This was broken for projections by my commit a51cce369b9c634a93120092d4c7685a242d55b1 --- pretyping/retyping.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'pretyping') diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 743bc3b19b..fb55265526 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -126,9 +126,11 @@ let retype ?(polyprop=true) sigma = | App(f,args) -> strip_outer_cast (subst_type env sigma (type_of env f) (Array.to_list args)) - | Proj (p,c) -> + | Proj (p,c) -> let ty = type_of env c in - Inductiveops.type_of_projection_knowing_arg env sigma p c ty + (try + Inductiveops.type_of_projection_knowing_arg env sigma p c ty + with Invalid_argument _ -> retype_error BadRecursiveType) | Cast (c,_, t) -> t | Sort _ | Prod _ -> mkSort (sort_of env cstr) -- cgit v1.2.3 From 9c732a5c878bac2592cb397aca3d17cfefdcd023 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 10 Jul 2015 01:13:59 +0200 Subject: Option -type-in-type: added support in checker and making it contaminating in vo files (this was not done yet in 24d0027f0 and 090fffa57b). Reused field "engagement" to carry information about both impredicativity of set and type in type. For the record: maybe some further checks to do around the sort of the inductive types in coqchk? --- pretyping/nativenorm.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'pretyping') diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index b4b6b8aab8..2432b8d291 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -150,14 +150,12 @@ let sort_of_product env domsort rangsort = | (Prop _, Prop Pos) -> rangsort (* Product rule (Type,Set,?) *) | (Type u1, Prop Pos) -> - begin match engagement env with - | Some ImpredicativeSet -> + if is_impredicative_set env then (* Rule is (Type,Set,Set) in the Set-impredicative calculus *) rangsort - | _ -> + else (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *) Type (sup u1 type0_univ) - end (* Product rule (Prop,Type_i,Type_i) *) | (Prop Pos, Type u2) -> Type (sup type0_univ u2) (* Product rule (Prop,Type_i,Type_i) *) -- cgit v1.2.3 From 2aaced1d2486deb901ea0a5b134ef28273dda67f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 10 Jul 2015 01:17:56 +0200 Subject: Continuing handling of NoCoercion after df6e64fd28 and 4944b5e72. Commit df6e64fd28 let apply_coercion raise NoCoercion untrapped by inh_app_fun. Commit 4944b5e72 caught NoCoercion but missed re-attempting inserting a coercion after resolving instances of type classes. This fixes MathClasses (while preserving fix of part of from 4944b5e72 and fixes of HoTT_coq_014.v from df6e64fd28). --- pretyping/classops.mli | 4 ++-- pretyping/coercion.ml | 18 ++++++++++-------- 2 files changed, 12 insertions(+), 10 deletions(-) (limited to 'pretyping') diff --git a/pretyping/classops.mli b/pretyping/classops.mli index c421b4505b..e2bb2d1a00 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -78,9 +78,9 @@ val coercion_value : coe_index -> (unsafe_judgment * bool * bool) Univ.in_univer (** {6 Lookup functions for coercion paths } *) -val lookup_path_between_class : cl_index * cl_index -> inheritance_path -(** @raise Not_found when no such path exists *) +(** @raise Not_found in the following functions when no path exists *) +val lookup_path_between_class : cl_index * cl_index -> inheritance_path val lookup_path_between : env -> evar_map -> types * types -> types * types * inheritance_path val lookup_path_to_fun_from : env -> evar_map -> types -> diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 6765ca130b..e61e52c178 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -345,7 +345,7 @@ let saturate_evd env evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~split:false ~fail:false env evd -(* appliquer le chemin de coercions p à hj *) +(* Apply coercion path from p to hj; raise NoCoercion if not applicable *) let apply_coercion env sigma p hj typ_cl = try let j,t,evd = @@ -367,7 +367,8 @@ let apply_coercion env sigma p hj typ_cl = with NoCoercion as e -> raise e | e when Errors.noncritical e -> anomaly (Pp.str "apply_coercion") -let inh_app_fun env evd j = +(* Try to coerce to a funclass; raise NoCoercion if not possible *) +let inh_app_fun_core env evd j = let t = whd_betadeltaiota env evd j.uj_type in match kind_of_term t with | Prod (_,_,_) -> (evd,j) @@ -387,16 +388,17 @@ let inh_app_fun env evd j = (!evdref, res) with NoSubtacCoercion | NoCoercion -> (evd,j) - else (evd, j) + else raise NoCoercion +(* Try to coerce to a funclass; returns [j] if no coercion is applicable *) let inh_app_fun resolve_tc env evd j = - try inh_app_fun env evd j + try inh_app_fun_core env evd j with - | Not_found when not resolve_tc + | NoCoercion when not resolve_tc || not !use_typeclasses_for_conversion -> (evd, j) - | Not_found -> - try inh_app_fun env (saturate_evd env evd) j - with Not_found -> (evd, j) + | NoCoercion -> + try inh_app_fun_core env (saturate_evd env evd) j + with NoCoercion -> (evd, j) let inh_tosort_force loc env evd j = try -- cgit v1.2.3 From 93579407f5795c117d6c6f1399396b690f80d723 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 16 Jul 2015 09:32:36 +0200 Subject: Fixing anomaly #3743 while printing an error message involving evar constraints. Indeed, the name of a bound variable was lost when unifying under a Prod in evarconv. The error message for "Unable to satisfy the following constraints" is still to be improved though. --- pretyping/evarconv.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 97b1b16455..64d1345c1f 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -726,12 +726,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty UnifFailure (evd,UnifUnivInconsistency p) | e when Errors.noncritical e -> UnifFailure (evd,NotSameHead)) - | Prod (n,c1,c'1), Prod (_,c2,c'2) when app_empty -> + | Prod (n1,c1,c'1), Prod (n2,c2,c'2) when app_empty -> ise_and evd [(fun i -> evar_conv_x ts env i CONV c1 c2); (fun i -> let c = nf_evar i c1 in - evar_conv_x ts (push_rel (n,None,c) env) i pbty c'1 c'2)] + let na = Nameops.name_max n1 n2 in + evar_conv_x ts (push_rel (na,None,c) env) i pbty c'1 c'2)] | Rel x1, Rel x2 -> if Int.equal x1 x2 then -- cgit v1.2.3 From 3bcc96d5ab6571a7810b68c340af7aa195ef76f4 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 16 Jul 2015 09:44:54 +0200 Subject: Continuing 93579407, spotting other potential sources of anomaly because of the name of a bound variable lost when unifying under a binder in evarconv. --- pretyping/evarconv.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 64d1345c1f..bb07bf0563 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -552,13 +552,14 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | MaybeFlexible v1, MaybeFlexible v2 -> begin match kind_of_term term1, kind_of_term term2 with - | LetIn (na,b1,t1,c'1), LetIn (_,b2,t2,c'2) -> + | LetIn (na1,b1,t1,c'1), LetIn (na2,b2,t2,c'2) -> let f1 i = ise_and i [(fun i -> evar_conv_x ts env i CONV b1 b2); (fun i -> let b = nf_evar i b1 in let t = nf_evar i t1 in + let na = Nameops.name_max na1 na2 in evar_conv_x ts (push_rel (na,Some b,t) env) i pbty c'1 c'2); (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] and f2 i = @@ -666,13 +667,14 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty end | Rigid, Rigid when isLambda term1 && isLambda term2 -> - let (na,c1,c'1) = destLambda term1 in - let (_,c2,c'2) = destLambda term2 in + let (na1,c1,c'1) = destLambda term1 in + let (na2,c2,c'2) = destLambda term2 in assert app_empty; ise_and evd [(fun i -> evar_conv_x ts env i CONV c1 c2); (fun i -> let c = nf_evar i c1 in + let na = Nameops.name_max na1 na2 in evar_conv_x ts (push_rel (na,None,c) env) i CONV c'1 c'2)] | Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2 -- cgit v1.2.3 From e4aa8f13680a81ec7e2ebe1281b20d5791d13440 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 16 Jul 2015 19:21:35 +0200 Subject: Fix universe instantiation with canonical structures. Patch by Matthieu Sozeau. Fixes #3819: "Error: Unsatisfied constraints" due to canonical structure inference --- pretyping/recordops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping') diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 6dc0d1f3c2..7fde7b7ac4 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -190,7 +190,7 @@ let cs_pattern_of_constr t = (* Intended to always succeed *) let compute_canonical_projections (con,ind) = let env = Global.env () in - let ctx = Environ.constant_context env con in + let ctx = Univ.instantiate_univ_context (Environ.constant_context env con) in let u = Univ.UContext.instance ctx in let v = (mkConstU (con,u)) in let ctx = Univ.ContextSet.of_context ctx in -- cgit v1.2.3 From 8591217a89f0b71e8175752dc55c42a5b89fccec Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 16 Jul 2015 20:21:58 +0200 Subject: Fixing bug #4240 (closure_of_filter was not ensuring refinement of former filter after 48509b61 and 3cd718c, because filtered let-ins were not any longer preserved). --- pretyping/evarsolve.ml | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'pretyping') diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index bfd19c6c7d..b2cf21b818 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -157,6 +157,7 @@ let restrict_evar_key evd evk filter candidates = end (* Restrict an applied evar and returns its restriction in the same context *) +(* (the filter is assumed to be at least stronger than the original one) *) let restrict_applied_evar evd (evk,argsv) filter candidates = let evd,newevk = restrict_evar_key evd evk filter candidates in let newargsv = match filter with @@ -885,6 +886,9 @@ let filter_candidates evd evk filter candidates_update = else UpdateWith l' +(* Given a filter refinement for the evar [evk], restrict it so that + dependencies are preserved *) + let closure_of_filter evd evk = function | None -> None | Some filter -> @@ -892,8 +896,11 @@ let closure_of_filter evd evk = function let vars = collect_vars (Evarutil.nf_evar evd (evar_concl evi)) in let test b (id,c,_) = b || Idset.mem id vars || match c with None -> false | Some c -> not (isRel c || isVar c) in let newfilter = Filter.map_along test filter (evar_context evi) in + (* Now ensure that restriction is at least what is was originally *) + let newfilter = Option.cata (Filter.map_along (&&) newfilter) newfilter (Filter.repr (evar_filter evi)) in if Filter.equal newfilter (evar_filter evi) then None else Some newfilter +(* The filter is assumed to be at least stronger than the original one *) let restrict_hyps evd evk filter candidates = (* What to do with dependencies? Assume we have x:A, y:B(x), z:C(x,y) |- ?e:T(x,y,z) and restrict on y. -- cgit v1.2.3 From 0b3a335219e161dc04f6734e9ee4f7c08cde6cd5 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 16 Jul 2015 21:34:08 +0200 Subject: Fixing #4177 (find_projectable was liable to ask to instantiate an evar twice). This is a bug in a pretty old code, showing also in 8.3 and 8.4. --- pretyping/evarsolve.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'pretyping') diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index b2cf21b818..ac1692f451 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -694,7 +694,8 @@ let rec find_projectable_vars with_evars aliases sigma y subst = (* Then test if [idc] is (indirectly) bound in [subst] to some evar *) (* projectable on [y] *) if with_evars then - let idcl' = List.filter (fun (c,_,id) -> isEvar c) idcl in + let f (c,_,id) = isEvar c && is_undefined sigma (fst (destEvar c)) in + let idcl' = List.filter f idcl in match idcl' with | [c,_,id] -> begin -- cgit v1.2.3 From e0d36d4afd7f38eb6816b92d03ecc2d2f7dc8d3f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 16 Jul 2015 22:08:31 +0200 Subject: Slight improvement in naming anonymous variables in error messages: using closer naming strategies for naming variables in make_all_name_different and when contracting trivial letins. Not sure what the best policy is. Maybe the contraction process should not invent names at al and let make_all_name_different do the job. Maybe pretyping should name all rels which it pushes to environment (with cases.ml paying attention to avoid clash). The problem shows for instance with a PretypeError (... env, ... , ActualTypeNotCoercible (NotClean (... env ...)) message with two copies of env which we don't if they are the same but which have to share same names for similar rendering of the rels! This was revealed e.g. by the error message of #4177. --- pretyping/namegen.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'pretyping') diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml index 5aca11ae61..a88c2e20e3 100644 --- a/pretyping/namegen.ml +++ b/pretyping/namegen.ml @@ -278,6 +278,7 @@ let make_all_name_different env = let avoid = ref (ids_of_named_context (named_context env)) in process_rel_context (fun (na,c,t) newenv -> + let na = named_hd newenv t na in let id = next_name_away na !avoid in avoid := id::!avoid; push_rel (Name id,c,t) newenv) -- cgit v1.2.3 From fdd6a17b272995237c9f95fc465bb1ff6871bedc Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 16 Jul 2015 22:53:10 +0200 Subject: Refining 71def2f8 on too strong occur-check limiting evar-evar unification in tactics. The relaxing of occur-check was ok but was leading trivial problems of the form ?X[?Meta] = ?X[?Meta] to enter a complex Evar-ization into ?X[?Meta] = ?X[?Y], ?Meta:=?Y which consider_remaining_unif_problems was not any more able to deal with. Doing quick: treat the trivial cases ?X[args] = ?X[args] in an ad hoc way, so that it behaves as if the occur-check had not been restricted. --- pretyping/unification.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'pretyping') diff --git a/pretyping/unification.ml b/pretyping/unification.ml index b5fe5d0b6d..24e06007e9 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -676,7 +676,11 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb | Evar (evk,_ as ev), Evar (evk',_) when not (Evar.Set.mem evk flags.frozen_evars) && Evar.equal evk evk' -> - sigma,metasubst,((curenv,ev,cN)::evarsubst) + let sigma',b = constr_cmp cv_pb sigma flags cM cN in + if b then + sigma',metasubst,evarsubst + else + sigma,metasubst,((curenv,ev,cN)::evarsubst) | Evar (evk,_ as ev), _ when not (Evar.Set.mem evk flags.frozen_evars) && not (occur_evar evk cN) -> -- cgit v1.2.3