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

Fix bug in the type checker (when type checking terms with meta-variables).

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-22 19:12:19 -07:00
parent 1647e44510
commit 46d6c41835
2 changed files with 44 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/kernel/type_checker.cpp
View file

@ -43,18 +43,17 @@ class type_checker::imp {
expr r = m_normalizer(e, ctx);
if (is_pi(r))
return r;
if (is_metavar(r) && m_menv && m_up) {
lean_assert(!m_menv->is_assigned(r));
if (has_metavar(r) && m_menv && m_up) {
// Create two fresh variables A and B,
// and assign r == (Pi(x : A), B x)
expr A = m_menv->mk_metavar(ctx);
expr B = m_menv->mk_metavar(ctx);
expr p = mk_pi(g_x_name, A, B(Var(0)));
if (has_meta_context(r)) {
// r contains lift/inst operations, so we put the constraint in m_up
m_up->add_eq(ctx, r, p);
} else {
if (is_metavar(r) && !has_meta_context(r)) {
// cheap case
m_menv->assign(r, p);
} else {
m_up->add_eq(ctx, r, p);
}
return p;
}
@ -67,18 +66,19 @@ class type_checker::imp {
return ty_level(u);
if (u == Bool)
return level();
if (is_metavar(u) && m_up) {
lean_assert(!m_menv->is_assigned(u));
if (has_metavar(u) && m_menv && m_up) {
// Remark: in the current implementation we don't have level constraints and variables
// in the unification problem set. So, we assume the metavariable is in level 0.
// This is a crude approximation that works most of the time.
// A better solution is consists in creating a fresh universe level k and
// associate the constraint that u == Type k.
// Later the constraint must be solved in the elaborator.
if (has_meta_context(u))
m_up->add_eq(ctx, u, Type());
else
if (is_metavar(u) && !has_meta_context(u)) {
// cheap case
m_menv->assign(u, Type());
} else {
m_up->add_eq(ctx, u, Type());
}
return level();
}
throw type_expected_exception(m_env, ctx, t);
@ -136,7 +136,7 @@ class type_checker::imp {
r = f_t;
break;
}
check_pi(f_t, e, ctx);
f_t = check_pi(f_t, e, ctx);
}
break;
}

34
src/tests/kernel/metavar.cpp
View file

@ -39,13 +39,24 @@ public:
for (auto c : up.m_eqs)
std::cout << std::get<0>(c) << " |- " << std::get<1>(c) << " == " << std::get<2>(c) << "\n";
for (auto c : up.m_type_of_eqs)
std::cout << std::get<0>(c) << " |- typeof(" << std::get<1>(c) << ") == " << std::get<2>(c) << "\n";
std::cout << std::get<0>(c) << " |- " << std::get<1>(c) << " : " << std::get<2>(c) << "\n";
for (auto c : up.m_is_convertible_cnstrs)
std::cout << std::get<0>(c) << " |- " << std::get<1>(c) << " --> " << std::get<2>(c) << "\n";
std::cout << std::get<0>(c) << " |- " << std::get<1>(c) << " == " << std::get<2>(c) << "\n";
return out;
}
};
std::ostream & operator<<(std::ostream & out, metavar_env const & env) {
bool first = true;
for (unsigned i = 0; i < env.size(); i++) {
if (env.is_assigned(i)) {
if (first) first = false; else out << "\n";
out << "?M" << i << " <- " << env.get_subst(i);
}
}
return out;
}
static void tst1() {
unification_problems_dbg u;
metavar_env menv;
@ -509,6 +520,24 @@ static void tst24() {
std::cout << instantiate_metavars(f(m1), menv) << "\n";
}
static void tst25() {
environment env;
metavar_env menv;
unification_problems_dbg up;
type_checker checker(env);
expr N = Const("N");
expr a = Const("a");
expr b = Const("b");
env.add_var("N", Type());
env.add_var("a", N);
env.add_var("b", N);
expr m = menv.mk_metavar();
expr F = m(a, b);
std::cout << checker.infer_type(F, context(), &menv, &up) << "\n";
std::cout << menv << "\n";
std::cout << up << "\n";
}
int main() {
tst1();
tst2();
@ -534,5 +563,6 @@ int main() {
tst22();
tst23();
tst24();
tst25();
return has_violations() ? 1 : 0;
}