michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/unifier): crash when unifying constraints of the form (pr t =?= s)

Browse source 
where pr is a projection and t is a stuck term

see issue #737
This commit is contained in:
Leonardo de Moura 2015-07-24 11:47:37 -07:00
parent 0f2c0b6512
commit 5c7a20e5bd
2 changed files with 10 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
library/data/real/basic.lean
View file

@ -644,8 +644,7 @@ theorem mul_bound_helper {s t : seq} (Hs : regular s) (Ht : regular t) (a b c :
apply rat.le.trans,
apply rat.mul_le_mul_of_nonneg_right,
apply pceil_helper Hn,
repeat (apply rat.mul_pos | apply rat.add_pos | apply rat_of_pnat_is_pos | apply inv_pos),
--repeat (apply rat.mul_pos | apply rat.add_pos | apply inv_pos | apply rat_of_pnat_is_pos),
repeat (apply rat.mul_pos | apply rat.add_pos | apply inv_pos | apply rat_of_pnat_is_pos),
apply rat.le_of_lt,
apply rat.add_pos,
apply rat.mul_pos,
@ -654,7 +653,7 @@ theorem mul_bound_helper {s t : seq} (Hs : regular s) (Ht : regular t) (a b c :
repeat apply inv_pos,
apply rat.mul_pos,
apply rat.add_pos,
apply inv_pos,apply inv_pos, -- repeat apply inv_pos,
repeat apply inv_pos,
apply rat_of_pnat_is_pos,
have H : (rat_of_pnat (K s) * (b⁻¹ + c⁻¹) + (a⁻¹ + c⁻¹) * rat_of_pnat (K t)) ≠ 0, begin
apply rat.ne_of_gt,
@ -693,7 +692,7 @@ theorem mul_bound_helper {s t : seq} (Hs : regular s) (Ht : regular t) (a b c :
apply rat.le_of_lt,
apply rat.mul_pos,
apply rat.add_pos,
apply inv_pos,apply inv_pos, -- repeat apply inv_pos,
repeat apply inv_pos,
apply rat_of_pnat_is_pos,
apply rat.le_of_lt,
apply inv_pos

8
src/library/unifier.cpp
View file

@ -1498,7 +1498,13 @@ struct unifier_fn {
set_conflict(j);
return false;
}
expr meta = *m_tc->is_stuck(pr_args[mkidx]);
auto stuck_it = m_tc->is_stuck(pr_args[mkidx]);
if (!stuck_it) {
// TODO(Lean): normalize, and try is_stuck again?
// We don't do it because it seems there is very little gain, and it may negatively affect performance.
return false;
}
expr meta = *stuck_it;
lean_assert(is_meta(meta));
buffer<expr> meta_args;
expr const & mvar = get_app_args(meta, meta_args);