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

fix(type_checker): fix inconsistent cache bug in type_checker, add tests that expose the problem

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-10-01 19:20:53 -07:00
parent 2089d12bd0
commit aa5be3262f
2 changed files with 41 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/kernel/type_checker.cpp
View file

@ -24,6 +24,7 @@ class type_checker::imp {
environment const & m_env;
cache m_cache;
normalizer m_normalizer;
context m_ctx;
metavar_env * m_menv;
unsigned m_menv_timestamp;
unification_problems * m_up;
@ -202,6 +203,13 @@ class type_checker::imp {
return m_normalizer.is_convertible(t1, t2, ctx, m_menv, m_up);
}
void set_ctx(context const & ctx) {
if (!is_eqp(m_ctx, ctx)) {
clear();
m_ctx = ctx;
}
}
void set_menv(metavar_env * menv) {
if (m_menv == menv) {
// Check whether m_menv has been updated since the last time the normalizer has been invoked
@ -227,18 +235,21 @@ public:
}
level infer_universe(expr const & t, context const & ctx, metavar_env * menv, unification_problems * up) {
set_ctx(ctx);
set_menv(menv);
flet<unification_problems*> set(m_up, up);
return infer_universe_core(t, ctx);
}
expr infer_type(expr const & e, context const & ctx, metavar_env * menv, unification_problems * up) {
set_ctx(ctx);
set_menv(menv);
flet<unification_problems*> set(m_up, up);
return infer_type_core(e, ctx);
}
bool is_convertible(expr const & t1, expr const & t2, context const & ctx, metavar_env * menv, unification_problems * up) {
set_ctx(ctx);
set_menv(menv);
flet<unification_problems*> set(m_up, up);
return is_convertible_core(t1, t2, ctx);
@ -252,6 +263,7 @@ public:
void clear() {
m_cache.clear();
m_normalizer.clear();
m_ctx = context();
m_menv = nullptr;
m_menv_timestamp = 0;
}

29
src/tests/kernel/type_checker.cpp
View file

@ -267,6 +267,34 @@ static void tst14() {
}
}
static void tst15() {
environment env;
import_all(env);
context ctx1, ctx2;
expr A = Const("A");
expr vec1 = Const("vec1");
expr vec2 = Const("vec2");
env.add_var("vec1", Int >> (Type() >> Type()));
env.add_var("vec2", Real >> (Type() >> Type()));
ctx1 = extend(ctx1, "x", Int, iVal(1));
ctx1 = extend(ctx1, "f", Pi({A, Int}, vec1(A, Int)));
ctx2 = extend(ctx2, "x", Real, rVal(2));
ctx2 = extend(ctx2, "f", Pi({A, Real}, vec2(A, Real)));
expr F = Var(0)(Var(1));
expr F_copy = F;
type_checker checker(env);
std::cout << checker.infer_type(F, ctx1) << "\n";
lean_assert_eq(checker.infer_type(F, ctx1), vec1(Var(1), Int));
lean_assert_eq(checker.infer_type(F, ctx2), vec2(Var(1), Real));
lean_assert(is_eqp(checker.infer_type(F, ctx2), checker.infer_type(F, ctx2)));
lean_assert(is_eqp(checker.infer_type(F, ctx1), checker.infer_type(F, ctx1)));
expr r = checker.infer_type(F, ctx1);
checker.clear();
lean_assert(!is_eqp(r, checker.infer_type(F, ctx1)));
r = checker.infer_type(F, ctx1);
lean_assert(is_eqp(r, checker.infer_type(F, ctx1)));
}
int main() {
tst1();
tst2();
@ -282,5 +310,6 @@ int main() {
tst12();
tst13();
tst14();
tst15();
return has_violations() ? 1 : 0;
}