From 022ec07048962ccd33ffdbcdc06adcb7fb09924f Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 2 Mar 2015 13:08:59 +0100 Subject: Fix bug #4097. --- pretyping/evarsolve.ml | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index f355d9a725..db7f6f6772 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -179,23 +179,24 @@ let restrict_instance evd evk filter argsv = let noccur_evar env evd evk c = let cache = ref Int.Set.empty (* cache for let-ins *) in - let rec occur_rec k c = + let rec occur_rec (k, env as acc) c = match kind_of_term c with | Evar (evk',args' as ev') -> (match safe_evar_value evd ev' with - | Some c -> occur_rec k c + | Some c -> occur_rec acc c | None -> if Evar.equal evk evk' then raise Occur - else Array.iter (occur_rec k) args') + else Array.iter (occur_rec acc) args') | Rel i when i > k -> if not (Int.Set.mem (i-k) !cache) then (match pi2 (Environ.lookup_rel (i-k) env) with | None -> () - | Some b -> cache := Int.Set.add (i-k) !cache; occur_rec k (lift i b)) - | Proj (p,c) -> occur_rec k (Retyping.expand_projection env evd p c []) - | _ -> iter_constr_with_binders succ occur_rec k c + | Some b -> cache := Int.Set.add (i-k) !cache; occur_rec acc (lift i b)) + | Proj (p,c) -> occur_rec acc (Retyping.expand_projection env evd p c []) + | _ -> iter_constr_with_full_binders (fun rd (k,env) -> (succ k, push_rel rd env)) + occur_rec acc c in - try occur_rec 0 c; true with Occur -> false + try occur_rec (0,env) c; true with Occur -> false (***************************************) (* Managing chains of local definitons *) -- cgit v1.2.3 From e77f178e60918f14eacd1ec0364a491d4cfd0f3f Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 3 Mar 2015 00:48:34 +0100 Subject: Fix bug introduced by my last commit, forgetting to adjust de Bruijn index lookup. --- pretyping/evarsolve.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping') diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index db7f6f6772..99d83a0e88 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -189,7 +189,7 @@ let noccur_evar env evd evk c = else Array.iter (occur_rec acc) args') | Rel i when i > k -> if not (Int.Set.mem (i-k) !cache) then - (match pi2 (Environ.lookup_rel (i-k) env) with + (match pi2 (Environ.lookup_rel i env) with | None -> () | Some b -> cache := Int.Set.add (i-k) !cache; occur_rec acc (lift i b)) | Proj (p,c) -> occur_rec acc (Retyping.expand_projection env evd p c []) -- cgit v1.2.3 From ac62cda8a4f488b94033b108c37556877232137a Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 3 Mar 2015 09:41:51 +0100 Subject: Fix bug #4101, noccur_evar's expand_projection can legitimately fail when called from w_unify, so we protect it. --- pretyping/evarsolve.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'pretyping') diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 99d83a0e88..bfd19c6c7d 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -192,7 +192,13 @@ let noccur_evar env evd evk c = (match pi2 (Environ.lookup_rel i env) with | None -> () | Some b -> cache := Int.Set.add (i-k) !cache; occur_rec acc (lift i b)) - | Proj (p,c) -> occur_rec acc (Retyping.expand_projection env evd p c []) + | Proj (p,c) -> + let c = + try Retyping.expand_projection env evd p c [] + with Retyping.RetypeError _ -> + (* Can happen when called from w_unify which doesn't assign evars/metas + eagerly enough *) c + in occur_rec acc c | _ -> iter_constr_with_full_binders (fun rd (k,env) -> (succ k, push_rel rd env)) occur_rec acc c in -- cgit v1.2.3 From 51b4d0cdad77f2874bd481dabd32e0772563dc3f Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 3 Mar 2015 15:47:24 +0100 Subject: Fix bug #4103: forgot to allow unfolding projections of cofixpoints like cases, in some cases. --- pretyping/reductionops.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'pretyping') diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 09eb38bd12..21f13a51f1 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -994,7 +994,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = | CoFix cofix -> if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then match Stack.strip_app stack with - |args, (Stack.Case(ci, _, lf,_)::s') -> + |args, ((Stack.Case _ |Stack.Proj _)::s') -> reduce_and_refold_cofix whrec env cst_l cofix stack |_ -> fold () else fold () @@ -1073,7 +1073,7 @@ let local_whd_state_gen flags sigma = | CoFix cofix -> if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then match Stack.strip_app stack with - |args, (Stack.Case(ci, _, lf,_)::s') -> + |args, ((Stack.Case _ | Stack.Proj _)::s') -> whrec (contract_cofix cofix, stack) |_ -> s else s -- cgit v1.2.3 From 2d3916766d3f145643a994aa83174c98394d5baa Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 3 Mar 2015 21:45:42 +0100 Subject: Fix bug #3590, keeping evars that are not turned into named metas by pattern_of_constr in an evar_map, as they can appear in the context of said named metas, which is used by change. Not sure what to do in the PEvar case, which never matches anyway according to Constr_matching.matches. --- pretyping/patternops.ml | 49 +++++++++++++++++++++++++++++------------------- pretyping/patternops.mli | 3 ++- 2 files changed, 32 insertions(+), 20 deletions(-) (limited to 'pretyping') diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index c49bec9aec..009b7323e4 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -123,6 +123,8 @@ let head_of_constr_reference c = match kind_of_term c with let pattern_of_constr env sigma t = let ctx = ref [] in + let keep = ref Evar.Set.empty in + let remove = ref Evar.Set.empty in let rec pattern_of_constr env t = match kind_of_term t with | Rel n -> PRel n @@ -141,28 +143,35 @@ let pattern_of_constr env sigma t = | App (f,a) -> (match match kind_of_term f with - Evar (evk,args as ev) -> - (match snd (Evd.evar_source evk sigma) with - Evar_kinds.MatchingVar (true,id) -> - ctx := (id,None,Evarutil.nf_evar sigma (existential_type sigma ev))::!ctx; - Some id - | _ -> None) - | _ -> None - with - | Some n -> PSoApp (n,Array.to_list (Array.map (pattern_of_constr env) a)) - | None -> PApp (pattern_of_constr env f,Array.map (pattern_of_constr env) a)) + | Evar (evk,args as ev) -> + (match snd (Evd.evar_source evk sigma) with + Evar_kinds.MatchingVar (true,id) -> + let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in + ctx := (id,None,ty)::!ctx; + keep := Evar.Set.union (evars_of_term ty) !keep; + remove := Evar.Set.add evk !remove; + Some id + | _ -> None) + | _ -> None + with + | Some n -> PSoApp (n,Array.to_list (Array.map (pattern_of_constr env) a)) + | None -> PApp (pattern_of_constr env f,Array.map (pattern_of_constr env) a)) | Const (sp,u) -> PRef (ConstRef (constant_of_kn(canonical_con sp))) | Ind (sp,u) -> PRef (canonical_gr (IndRef sp)) | Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp)) | Proj (p, c) -> pattern_of_constr env (Retyping.expand_projection env sigma p c []) | Evar (evk,ctxt as ev) -> - (match snd (Evd.evar_source evk sigma) with - | Evar_kinds.MatchingVar (b,id) -> - ctx := (id,None,Evarutil.nf_evar sigma (existential_type sigma ev))::!ctx; - assert (not b); PMeta (Some id) - | Evar_kinds.GoalEvar -> PEvar (evk,Array.map (pattern_of_constr env) ctxt) - | _ -> PMeta None) + remove := Evar.Set.add evk !remove; + (match snd (Evd.evar_source evk sigma) with + | Evar_kinds.MatchingVar (b,id) -> + let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in + ctx := (id,None,ty)::!ctx; + keep := Evar.Set.union (evars_of_term ty) !keep; + assert (not b); PMeta (Some id) + | Evar_kinds.GoalEvar -> + PEvar (evk,Array.map (pattern_of_constr env) ctxt) + | _ -> PMeta None) | Case (ci,p,a,br) -> let cip = { cip_style = ci.ci_pp_info.style; @@ -178,9 +187,11 @@ let pattern_of_constr env sigma t = | Fix f -> PFix f | CoFix f -> PCoFix f in let p = pattern_of_constr env t in + let remove = Evar.Set.diff !remove !keep in + let sigma = Evar.Set.fold (fun ev acc -> Evd.remove acc ev) remove sigma in (* side-effect *) (* Warning: the order of dependencies in ctx is not ensured *) - (!ctx,p) + (sigma,!ctx,p) (* To process patterns, we need a translation without typing at all. *) @@ -220,7 +231,7 @@ let instantiate_pattern env sigma lvar c = ctx in let c = substl inst c in - snd (pattern_of_constr env sigma c) + pi3 (pattern_of_constr env sigma c) with Not_found (* List.index failed *) -> let vars = List.map_filter (function Name id -> Some id | _ -> None) vars in @@ -245,7 +256,7 @@ let rec subst_pattern subst pat = | PRef ref -> let ref',t = subst_global subst ref in if ref' == ref then pat else - snd (pattern_of_constr (Global.env()) Evd.empty t) + pi3 (pattern_of_constr (Global.env()) Evd.empty t) | PVar _ | PEvar _ | PRel _ -> pat diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index cf02421c24..9e72280fe2 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -39,7 +39,8 @@ val head_of_constr_reference : Term.constr -> global_reference a pattern; currently, no destructor (Cases, Fix, Cofix) and no existential variable are allowed in [c] *) -val pattern_of_constr : Environ.env -> Evd.evar_map -> constr -> named_context * constr_pattern +val pattern_of_constr : Environ.env -> Evd.evar_map -> constr -> + Evd.evar_map * named_context * constr_pattern (** [pattern_of_glob_constr l c] translates a term [c] with metavariables into a pattern; variables bound in [l] are replaced by the pattern to which they -- cgit v1.2.3 From 85fc5f90c52a755d1b64640f4f0b3421979c0fe8 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 4 Mar 2015 00:32:58 +0100 Subject: Fix bug #3532, providing universe inconsistency information when a unification fails due to that, during a conversion step. --- pretyping/evarconv.ml | 23 +++++++++++++++-------- pretyping/reductionops.ml | 5 +++-- pretyping/reductionops.mli | 6 ++++-- 3 files changed, 22 insertions(+), 12 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 616ceeabdc..f388f90057 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -324,18 +324,25 @@ let rec evar_conv_x ts env evd pbty term1 term2 = Note: incomplete heuristic... *) let ground_test = if is_ground_term evd term1 && is_ground_term evd term2 then ( - let evd, b = - try infer_conv ~pb:pbty ~ts:(fst ts) env evd term1 term2 - with Univ.UniverseInconsistency _ -> evd, false + let evd, e = + try + let evd, b = infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts) + env evd term1 term2 + in + if b then evd, None + else evd, Some (ConversionFailed (env,term1,term2)) + with Univ.UniverseInconsistency e -> evd, Some (UnifUnivInconsistency e) in - if b then Some (evd, true) - else if is_ground_env evd env then Some (evd, false) - else None) + match e with + | None -> Some (evd, e) + | Some e -> + if is_ground_env evd env then Some (evd, Some e) + else None) else None in match ground_test with - | Some (evd, true) -> Success evd - | Some (evd, false) -> UnifFailure (evd,ConversionFailed (env,term1,term2)) + | Some (evd, None) -> Success evd + | Some (evd, Some e) -> UnifFailure (evd,e) | None -> (* Until pattern-unification is used consistently, use nohdbeta to not destroy beta-redexes that can be used for 1st-order unification *) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 21f13a51f1..dd671f111e 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1293,7 +1293,8 @@ let sigma_univ_state = { Reduction.compare = sigma_compare_sorts; Reduction.compare_instances = sigma_compare_instances } -let infer_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = +let infer_conv ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) + env sigma x y = try let b, sigma = let b, cstrs = @@ -1315,7 +1316,7 @@ let infer_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y sigma', true with | Reduction.NotConvertible -> sigma, false - | Univ.UniverseInconsistency _ -> sigma, false + | Univ.UniverseInconsistency _ when catch_incon -> sigma, false | e when is_anomaly e -> error "Conversion test raised an anomaly" (********************************************************************) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index d4f061c5be..1df2a73b2e 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -268,9 +268,11 @@ val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> con (** [infer_fconv] Adds necessary universe constraints to the evar map. pb defaults to CUMUL and ts to a full transparent state. + @raises UniverseInconsistency iff catch_incon is set to false, + otherwise returns false in that case. *) -val infer_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> constr -> constr -> - evar_map * bool +val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> + env -> evar_map -> constr -> constr -> evar_map * bool (** {6 Special-Purpose Reduction Functions } *) -- cgit v1.2.3