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

refactor(kernel/type_checker): pass buffer<unification_constraint> as a pointer

Browse source 
The idea is to make it an optional parameter independent of metavar_env.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-07 10:27:08 -08:00
parent 5f3b9dbbbd
commit 195ea24d71
10 changed files with 40 additions and 43 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/frontends/lean/frontend_elaborator.cpp
View file

@ -408,7 +408,7 @@ public:
expr new_e = preprocessor(*this)(e);
// std::cout << "After preprocessing\n" << new_e << "\n";
if (has_metavar(new_e)) {
m_type_checker.infer_type(new_e, context(), &m_menv, m_ucs);
m_type_checker.infer_type(new_e, context(), &m_menv, &m_ucs);
// for (auto c : m_ucs) {
// formatter fmt = mk_simple_formatter();
// std::cout << c.pp(fmt, options(), nullptr, false) << "\n";
@ -427,8 +427,8 @@ public:
expr new_e = preprocessor(*this)(e);
// std::cout << "After preprocessing\n" << new_t << "\n" << new_e << "\n";
if (has_metavar(new_e) || has_metavar(new_t)) {
m_type_checker.infer_type(new_t, context(), &m_menv, m_ucs);
expr new_e_t = m_type_checker.infer_type(new_e, context(), &m_menv, m_ucs);
m_type_checker.infer_type(new_t, context(), &m_menv, &m_ucs);
expr new_e_t = m_type_checker.infer_type(new_e, context(), &m_menv, &m_ucs);
m_ucs.push_back(mk_convertible_constraint(context(), new_e_t, new_t,
mk_def_type_match_justification(context(), n, e)));
// for (auto c : m_ucs) {

15
src/kernel/type_checker.cpp
View file

@ -53,7 +53,7 @@ class type_checker::imp {
expr r = normalize(e, ctx);
if (is_pi(r))
return r;
if (has_metavar(r) && m_menv) {
if (has_metavar(r) && m_menv && m_uc) {
// Create two fresh variables A and B,
// and assign r == (Pi(x : A), B x)
expr A = m_menv->mk_metavar(ctx);
@ -76,7 +76,7 @@ class type_checker::imp {
return u;
if (is_bool(u))
return Type();
if (has_metavar(u) && m_menv) {
if (has_metavar(u) && m_menv && m_uc) {
justification jst = mk_type_expected_justification(ctx, s);
m_uc->push_back(mk_convertible_constraint(ctx, u, TypeU, jst));
return u;
@ -256,7 +256,7 @@ class type_checker::imp {
expr new_expected = normalize(expected, ctx);
if (is_convertible_core(new_given, new_expected))
return true;
if (m_menv && (has_metavar(new_given) || has_metavar(new_expected))) {
if (m_menv && m_uc && (has_metavar(new_given) || has_metavar(new_expected))) {
m_uc->push_back(mk_convertible_constraint(ctx, given, expected, mk_justification()));
return true;
}
@ -295,10 +295,10 @@ public:
m_uc = nullptr;
}
expr infer_type(expr const & e, context const & ctx, metavar_env * menv, buffer<unification_constraint> & uc) {
expr infer_type(expr const & e, context const & ctx, metavar_env * menv, buffer<unification_constraint> * uc) {
set_ctx(ctx);
set_menv(menv);
flet<unification_constraints*> set_uc(m_uc, &uc);
flet<unification_constraints*> set_uc(m_uc, uc);
return infer_type_core(e, ctx);
}
@ -333,12 +333,11 @@ public:
type_checker::type_checker(environment const & env):m_ptr(new imp(env)) {}
type_checker::~type_checker() {}
expr type_checker::infer_type(expr const & e, context const & ctx, metavar_env * menv, buffer<unification_constraint> & uc) {
expr type_checker::infer_type(expr const & e, context const & ctx, metavar_env * menv, buffer<unification_constraint> * uc) {
return m_ptr->infer_type(e, ctx, menv, uc);
}
expr type_checker::infer_type(expr const & e, context const & ctx) {
buffer<unification_constraint> uc;
return infer_type(e, ctx, nullptr, uc);
return infer_type(e, ctx, nullptr, nullptr);
}
bool type_checker::is_convertible(expr const & t1, expr const & t2, context const & ctx) {
return m_ptr->is_convertible(t1, t2, ctx);

2
src/kernel/type_checker.h
View file

@ -34,7 +34,7 @@ public:
New metavariables and unification constraints may be created by the type checker.
The new unification constraints are stored in \c new_constraints.
*/
expr infer_type(expr const & e, context const & ctx, metavar_env * menv, buffer<unification_constraint> & new_constraints);
expr infer_type(expr const & e, context const & ctx, metavar_env * menv, buffer<unification_constraint> * new_constraints);
/**
\brief Return the type of \c e in the context \c ctx.

4
src/library/elaborator/elaborator.cpp
View file

@ -360,7 +360,7 @@ class elaborator::imp {
m_state.m_menv.assign(m, v, jst);
if (menv.has_type(m)) {
buffer<unification_constraint> ucs;
expr tv = m_type_inferer(v, ctx, &menv, ucs);
expr tv = m_type_inferer(v, ctx, &menv, &ucs);
for (auto c : ucs)
push_front(c);
justification new_jst(new typeof_mvar_justification(ctx, m, menv.get_type(m), tv, jst));
@ -746,7 +746,7 @@ class elaborator::imp {
buffer<expr> arg_types;
buffer<unification_constraint> ucs;
for (unsigned i = 1; i < num_a; i++) {
arg_types.push_back(m_type_inferer(arg(a, i), ctx, &menv, ucs));
arg_types.push_back(m_type_inferer(arg(a, i), ctx, &menv, &ucs));
for (auto uc : ucs)
push_front(uc);
}

2
src/library/tactic/apply_tactic.cpp
View file

@ -69,7 +69,7 @@ static optional<proof_state> apply_tactic(environment const & env, proof_state c
l.emplace_front(mvar_sol, name());
th_type_c = instantiate(abst_body(th_type_c), mvar_sol);
} else {
if (inferer.is_proposition(abst_domain(th_type_c))) {
if (inferer.is_proposition(abst_domain(th_type_c), context(), &new_menv)) {
name new_gname(gname, new_goal_idx);
new_goal_idx++;
l.emplace_front(expr(), new_gname);

22
src/library/type_inferer.cpp
View file

@ -46,7 +46,7 @@ class type_inferer::imp {
return u;
if (is_bool(u))
return Type();
if (has_metavar(u) && m_menv) {
if (has_metavar(u) && m_menv && m_uc) {
justification jst = mk_type_expected_justification(ctx, s);
m_uc->push_back(mk_convertible_constraint(ctx, u, TypeU, jst));
return u;
@ -64,7 +64,7 @@ class type_inferer::imp {
t = m_normalizer(t, ctx);
if (is_pi(t)) {
t = abst_body(t);
} else if (has_metavar(t) && m_menv) {
} else if (has_metavar(t) && m_menv && m_uc) {
// Create two fresh variables A and B,
// and assign r == (Pi(x : A), B x)
expr A = m_menv->mk_metavar(ctx);
@ -224,10 +224,10 @@ public:
m_uc = nullptr;
}
expr operator()(expr const & e, context const & ctx, metavar_env * menv, buffer<unification_constraint> & uc) {
expr operator()(expr const & e, context const & ctx, metavar_env * menv, buffer<unification_constraint> * uc) {
set_ctx(ctx);
set_menv(menv);
flet<unification_constraints*> set(m_uc, &uc);
flet<unification_constraints*> set(m_uc, uc);
return infer_type(e, ctx);
}
@ -239,9 +239,8 @@ public:
m_menv_timestamp = 0;
}
bool is_proposition(expr const & e, context const & ctx) {
buffer<unification_constraint> uc;
expr t = operator()(e, ctx, nullptr, uc);
bool is_proposition(expr const & e, context const & ctx, metavar_env * menv) {
expr t = operator()(e, ctx, menv, nullptr);
if (is_bool(t))
return true;
else
@ -250,15 +249,14 @@ public:
};
type_inferer::type_inferer(environment const & env):m_ptr(new imp(env)) {}
type_inferer::~type_inferer() {}
expr type_inferer::operator()(expr const & e, context const & ctx, metavar_env * menv, buffer<unification_constraint> & uc) {
expr type_inferer::operator()(expr const & e, context const & ctx, metavar_env * menv, buffer<unification_constraint> * uc) {
return m_ptr->operator()(e, ctx, menv, uc);
}
expr type_inferer::operator()(expr const & e, context const & ctx) {
buffer<unification_constraint> uc;
return operator()(e, ctx, nullptr, uc);
return operator()(e, ctx, nullptr, nullptr);
}
bool type_inferer::is_proposition(expr const & e, context const & ctx) {
return m_ptr->is_proposition(e, ctx);
bool type_inferer::is_proposition(expr const & e, context const & ctx, metavar_env * menv) {
return m_ptr->is_proposition(e, ctx, menv);
}
void type_inferer::clear() { m_ptr->clear(); }

4
src/library/type_inferer.h
View file

@ -31,9 +31,9 @@ public:
type_inferer(environment const & env);
~type_inferer();
expr operator()(expr const & e, context const & ctx, metavar_env * menv, buffer<unification_constraint> & uc);
expr operator()(expr const & e, context const & ctx, metavar_env * menv, buffer<unification_constraint> * uc);
expr operator()(expr const & e, context const & ctx = context());
bool is_proposition(expr const & e, context const & ctx = context());
bool is_proposition(expr const & e, context const & ctx = context(), metavar_env * menv = nullptr);
void clear();
};

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

@ -474,7 +474,7 @@ static void tst23() {
buffer<unification_constraint> up;
std::cout << F1 << "\n";
try {
std::cout << checker.infer_type(F1, context(), &menv, up) << "\n";
std::cout << checker.infer_type(F1, context(), &menv, &up) << "\n";
} catch (kernel_exception & ex) {
formatter fmt = mk_simple_formatter();
io_state st(options(), fmt);
@ -508,7 +508,7 @@ static void tst25() {
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 << checker.infer_type(F, context(), &menv, &up) << "\n";
std::cout << menv << "\n";
std::cout << up << "\n";
}
@ -554,7 +554,7 @@ static void tst26() {
expr A4 = menv.mk_metavar();
expr F = cons(A1, m1(a), cons(A2, m2(n), cons(A3, m3(b), nil(A4))));
std::cout << F << "\n";
std::cout << checker.infer_type(F, context(), &menv, up) << "\n";
std::cout << checker.infer_type(F, context(), &menv, &up) << "\n";
std::cout << menv << "\n";
std::cout << up << "\n";
}
@ -588,7 +588,7 @@ static void tst27() {
expr m2 = menv.mk_metavar();
expr F = Fun({{x, T1}, {y, T2}}, f(A1, x, y))(m1(a), m2(b));
std::cout << F << "\n";
std::cout << checker.infer_type(F, context(), &menv, up) << "\n";
std::cout << checker.infer_type(F, context(), &menv, &up) << "\n";
std::cout << menv << "\n";
std::cout << up << "\n";
}

18
src/tests/library/elaborator/elaborator.cpp
View file

@ -48,7 +48,7 @@ static void tst1() {
expr A4 = menv.mk_metavar();
expr F = cons(A1, m1(a), cons(A2, m2(n), cons(A3, m3(b), nil(A4))));
std::cout << F << "\n";
std::cout << checker.infer_type(F, context(), &menv, ucs) << "\n";
std::cout << checker.infer_type(F, context(), &menv, &ucs) << "\n";
expr int_id = Fun({a, Int}, a);
expr nat_id = Fun({a, Nat}, a);
ucs.push_back(mk_choice_constraint(context(), m1, { int_id, mk_int_to_real_fn() }, justification()));
@ -92,7 +92,7 @@ static void tst2() {
expr nat_id = Fun({a, Nat}, a);
expr F = m1(g(m2, m3(a)), m4(nVal(0)));
std::cout << F << "\n";
std::cout << checker.infer_type(F, context(), &menv, ucs) << "\n";
std::cout << checker.infer_type(F, context(), &menv, &ucs) << "\n";
ucs.push_back(mk_choice_constraint(context(), m1, { mk_nat_le_fn(), mk_int_le_fn(), mk_real_le_fn() }, justification()));
ucs.push_back(mk_choice_constraint(context(), m3, { int_id, mk_int_to_real_fn() }, justification()));
ucs.push_back(mk_choice_constraint(context(), m4, { nat_id, mk_nat_to_int_fn(), mk_nat_to_real_fn() }, justification()));
@ -135,7 +135,7 @@ static void tst3() {
expr x = Const("x");
expr F = Fun({x, m1}, m2(f(m3, x), m4(nVal(10))))(m5(a));
std::cout << F << "\n";
std::cout << checker.infer_type(F, context(), &menv, ucs) << "\n";
std::cout << checker.infer_type(F, context(), &menv, &ucs) << "\n";
ucs.push_back(mk_choice_constraint(context(), m2, { mk_nat_le_fn(), mk_int_le_fn(), mk_real_le_fn() }, justification()));
ucs.push_back(mk_choice_constraint(context(), m4, { nat_id, mk_nat_to_int_fn(), mk_nat_to_real_fn() }, justification()));
ucs.push_back(mk_choice_constraint(context(), m5, { int_id, mk_int_to_real_fn() }, justification()));
@ -180,7 +180,7 @@ static void tst4() {
expr int_id = Fun({a, Int}, a);
expr F = Fun({{x, m1}, {y, m2}}, m3(f(m4, x), f(m5, y)))(m6(a), b);
std::cout << F << "\n";
std::cout << checker.infer_type(F, context(), &menv, ucs) << "\n";
std::cout << checker.infer_type(F, context(), &menv, &ucs) << "\n";
ucs.push_back(mk_choice_constraint(context(), m3, { mk_nat_le_fn(), mk_int_le_fn(), mk_real_le_fn() }, justification()));
ucs.push_back(mk_choice_constraint(context(), m6, { int_id, mk_int_to_real_fn() }, justification()));
elaborator elb(env, menv, ucs.size(), ucs.data());
@ -222,7 +222,7 @@ static void tst5() {
expr int_id = Fun({a, Int}, a);
expr F = Fun({{x, m1}, {y, m2}}, f(m3, x, y))(m4(a), b);
std::cout << F << "\n";
std::cout << checker.infer_type(F, context(), &menv, ucs) << "\n";
std::cout << checker.infer_type(F, context(), &menv, &ucs) << "\n";
ucs.push_back(mk_choice_constraint(context(), m4, { int_id, mk_int_to_real_fn() }, justification()));
elaborator elb(env, menv, ucs.size(), ucs.data());
elb.next();
@ -259,7 +259,7 @@ static void tst6() {
env.add_axiom("H2", Eq(a, b));
expr V = Subst(m1, m2, m3, m4, H1, H2);
expr expected = Eq(f(a, f(b, b)), a);
expr given = checker.infer_type(V, context(), &menv, ucs);
expr given = checker.infer_type(V, context(), &menv, &ucs);
ucs.push_back(mk_eq_constraint(context(), expected, given, justification()));
elaborator elb(env, menv, ucs.size(), ucs.data());
metavar_env s = elb.next();
@ -273,7 +273,7 @@ static expr elaborate(expr const & e, environment const & env) {
buffer<unification_constraint> ucs;
type_checker checker(env);
expr e2 = replace_placeholders_with_metavars(e, menv);
checker.infer_type(e2, context(), &menv, ucs);
checker.infer_type(e2, context(), &menv, &ucs);
elaborator elb(env, menv, ucs.size(), ucs.data());
metavar_env s = elb.next();
return instantiate_metavars(e2, s);
@ -830,7 +830,7 @@ void tst26() {
expr m1 = menv.mk_metavar();
expr F = Eq(g(m1, a), a);
std::cout << F << "\n";
std::cout << checker.infer_type(F, context(), &menv, ucs) << "\n";
std::cout << checker.infer_type(F, context(), &menv, &ucs) << "\n";
elaborator elb(env, menv, ucs.size(), ucs.data());
metavar_env s = elb.next();
std::cout << instantiate_metavars(F, s) << "\n";
@ -865,7 +865,7 @@ void tst27() {
expr m3 = menv.mk_metavar();
expr F = Fun({f, m1}, eq(m2, g(m3, f)(a), a));
std::cout << F << "\n";
std::cout << checker.infer_type(F, context(), &menv, ucs) << "\n";
std::cout << checker.infer_type(F, context(), &menv, &ucs) << "\n";
elaborator elb(env, menv, ucs.size(), ucs.data());
metavar_env s = elb.next();
std::cout << instantiate_metavars(F, s) << "\n";

2
src/tests/library/type_inferer.cpp
View file

@ -133,7 +133,7 @@ static void tst4() {
expr A4 = menv.mk_metavar();
expr F = cons(A1, m1(a), cons(A2, m2(n), cons(A3, m3(b), nil(A4))));
std::cout << F << "\n";
std::cout << inferer(F, context(), &menv, uc) << "\n";
std::cout << inferer(F, context(), &menv, &uc) << "\n";
std::cout << uc << "\n";
}