diff --git a/src/frontends/lean/frontend_elaborator.cpp b/src/frontends/lean/frontend_elaborator.cpp index 4956b2af9..13e3de263 100644 --- a/src/frontends/lean/frontend_elaborator.cpp +++ b/src/frontends/lean/frontend_elaborator.cpp @@ -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) { diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index e357b8254..cae6f3743 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -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 & uc) { + expr infer_type(expr const & e, context const & ctx, metavar_env * menv, buffer * uc) { set_ctx(ctx); set_menv(menv); - flet set_uc(m_uc, &uc); + flet 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 & uc) { +expr type_checker::infer_type(expr const & e, context const & ctx, metavar_env * menv, buffer * uc) { return m_ptr->infer_type(e, ctx, menv, uc); } expr type_checker::infer_type(expr const & e, context const & ctx) { - buffer 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); diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index b208f54c0..e6b74a650 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -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 & new_constraints); + expr infer_type(expr const & e, context const & ctx, metavar_env * menv, buffer * new_constraints); /** \brief Return the type of \c e in the context \c ctx. diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index 03ef0b7dc..8150b4b6c 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -360,7 +360,7 @@ class elaborator::imp { m_state.m_menv.assign(m, v, jst); if (menv.has_type(m)) { buffer 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 arg_types; buffer 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); } diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index f674f981b..23355c129 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -69,7 +69,7 @@ static optional 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); diff --git a/src/library/type_inferer.cpp b/src/library/type_inferer.cpp index 7e674d421..b363ec860 100644 --- a/src/library/type_inferer.cpp +++ b/src/library/type_inferer.cpp @@ -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 & uc) { + expr operator()(expr const & e, context const & ctx, metavar_env * menv, buffer * uc) { set_ctx(ctx); set_menv(menv); - flet set(m_uc, &uc); + flet 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 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 & uc) { +expr type_inferer::operator()(expr const & e, context const & ctx, metavar_env * menv, buffer * uc) { return m_ptr->operator()(e, ctx, menv, uc); } expr type_inferer::operator()(expr const & e, context const & ctx) { - buffer 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(); } diff --git a/src/library/type_inferer.h b/src/library/type_inferer.h index 4e2c4a568..84d1a9e77 100644 --- a/src/library/type_inferer.h +++ b/src/library/type_inferer.h @@ -31,9 +31,9 @@ public: type_inferer(environment const & env); ~type_inferer(); - expr operator()(expr const & e, context const & ctx, metavar_env * menv, buffer & uc); + expr operator()(expr const & e, context const & ctx, metavar_env * menv, buffer * 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(); }; diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp index 06ad8a67c..ec18b690a 100644 --- a/src/tests/kernel/metavar.cpp +++ b/src/tests/kernel/metavar.cpp @@ -474,7 +474,7 @@ static void tst23() { buffer 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"; } diff --git a/src/tests/library/elaborator/elaborator.cpp b/src/tests/library/elaborator/elaborator.cpp index f1248629d..deb94dc2e 100644 --- a/src/tests/library/elaborator/elaborator.cpp +++ b/src/tests/library/elaborator/elaborator.cpp @@ -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 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"; diff --git a/src/tests/library/type_inferer.cpp b/src/tests/library/type_inferer.cpp index ec53d3bed..443fed6be 100644 --- a/src/tests/library/type_inferer.cpp +++ b/src/tests/library/type_inferer.cpp @@ -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"; }