From 30b19c314a6bd0bf566a1b1671d2469a5fcae102 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 17 Sep 2013 07:15:47 -0700 Subject: [PATCH] Add basic support for metavariables at is_convertible. Swap is_convertible arguments to make it more intuitive. Signed-off-by: Leonardo de Moura --- src/frontends/lean/elaborator.cpp | 6 ++-- src/kernel/environment.cpp | 2 +- src/kernel/metavar.cpp | 22 +++++++++------ src/kernel/metavar.h | 7 +++++ src/kernel/normalizer.cpp | 47 ++++++++++++++++++++++--------- src/kernel/normalizer.h | 7 +++-- src/kernel/type_checker.cpp | 4 +-- src/tests/kernel/metavar.cpp | 3 ++ 8 files changed, 68 insertions(+), 30 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 1f2f3ae53..3b6d1cb0e 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -283,7 +283,7 @@ class elaborator::imp { expr expected = abst_domain(f_t); expr given = types[i]; if (!has_metavar(expected) && !has_metavar(given)) { - if (is_convertible(expected, given, ctx)) { + if (is_convertible(given, expected, ctx)) { // compatible } else if (m_frontend.get_coercion(given, expected, ctx)) { // compatible if using coercion @@ -403,7 +403,7 @@ class elaborator::imp { info_ref r = mk_app_mismatch_info(e, ctx, args.size(), args.data(), types.data()); m_constraints.push_back(constraint(expected, given, ctx, r)); } else { - if (!is_convertible(expected, given, ctx)) { + if (!is_convertible(given, expected, ctx)) { expr coercion = m_frontend.get_coercion(given, expected, ctx); if (coercion) { modified = true; @@ -459,7 +459,7 @@ class elaborator::imp { info_ref r = mk_expected_type_info(let_value(e), v_p.first, expected, given, ctx); m_constraints.push_back(constraint(expected, given, ctx, r)); } else { - if (!is_convertible(expected, given, ctx)) { + if (!is_convertible(given, expected, ctx)) { expr coercion = m_frontend.get_coercion(given, expected, ctx); if (coercion) { v_p.first = mk_app(coercion, v_p.first); diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 618b48246..bc47eaa78 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -224,7 +224,7 @@ struct environment::imp { void check_type(name const & n, expr const & t, expr const & v, environment const & env) { m_type_checker.infer_universe(t); expr v_t = m_type_checker.infer_type(v); - if (!m_type_checker.is_convertible(t, v_t)) + if (!m_type_checker.is_convertible(v_t, t)) throw def_type_mismatch_exception(env, n, t, v, v_t); } diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp index b0c88131e..9e0778716 100644 --- a/src/kernel/metavar.cpp +++ b/src/kernel/metavar.cpp @@ -107,15 +107,19 @@ void metavar_env::assign(expr const & m, expr const & t) { } expr instantiate_metavars(expr const & e, metavar_env const & env) { - auto f = [=](expr const & m, unsigned offset) -> expr { - if (is_metavar(m) && env.contains(m)) { - expr s = env.get_subst(m); - return s ? s : m; - } else { - return m; - } - }; - return replace_fn(f)(e); + if (!has_metavar(e)) { + return e; + } else { + auto f = [=](expr const & m, unsigned offset) -> expr { + if (is_metavar(m) && env.contains(m)) { + expr s = env.get_subst(m); + return s ? s : m; + } else { + return m; + } + }; + return replace_fn(f)(e); + } } meta_ctx add_lift(meta_ctx const & ctx, unsigned s, unsigned n) { diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h index af365dac4..f2bb5e8ae 100644 --- a/src/kernel/metavar.h +++ b/src/kernel/metavar.h @@ -16,6 +16,7 @@ namespace lean { It store two kinds of problems: 1. ctx |- lhs == rhs 2. ctx |- typeof(n) == t + 3. ctx |- t1 is_convertible_to t2 */ class unification_problems { public: @@ -28,6 +29,12 @@ public: \brief Add a new unification problem of the form ctx |- typeof(n) == t */ virtual void add_type_of_eq(context const & ctx, expr const & n, expr const & t) = 0; + /** + \brief Add a new problem of the form ctx |- t1 is_convertible_to t2 + + \remark ctx |- t1 == t2 implies ctx |- t1 is_convertible_to t2 + */ + virtual void add_is_convertible(context const & ctx, expr const & t1, expr const & t2) = 0; }; /** diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp index eab691bf5..5a805d1db 100644 --- a/src/kernel/normalizer.cpp +++ b/src/kernel/normalizer.cpp @@ -292,12 +292,12 @@ class normalizer::imp { return r; } - bool is_convertible_core(expr const & expected, expr const & given) { - if (expected == given) { + bool is_convertible_core(expr const & given, expr const & expected) { + if (given == expected) { return true; } else { - expr const * e = &expected; expr const * g = &given; + expr const * e = &expected; while (true) { if (is_type(*e) && is_type(*g)) { if (m_env.is_ge(ty_level(*e), ty_level(*g))) @@ -308,8 +308,8 @@ class normalizer::imp { return true; if (is_pi(*e) && is_pi(*g) && abst_domain(*e) == abst_domain(*g)) { - e = &abst_body(*e); g = &abst_body(*g); + e = &abst_body(*e); } else { return false; } @@ -355,14 +355,31 @@ public: return reify(normalize(e, value_stack(), k), k); } - bool is_convertible(expr const & expected, expr const & given, context const & ctx) { - if (is_convertible_core(expected, given)) + bool is_convertible(expr const & given, expr const & expected, context const & ctx, + metavar_env * menv, unification_problems * up) { + if (is_convertible_core(given, expected)) return true; + expr new_given = given; + expr new_expected = expected; + if (has_metavar(new_given) || has_metavar(new_expected)) { + expr new_given = instantiate_metavars(new_given, *menv); + expr new_expected = instantiate_metavars(new_expected, *menv); + if (is_convertible_core(new_given, new_expected)) + return true; + if (has_metavar(new_given) || has_metavar(new_expected)) { + // Very conservative approach, just postpone the problem. + // We may also try to normalize new_given and new_expected even if + // they contain metavariables. + up->add_is_convertible(ctx, new_given, new_expected); + return true; + } + } + set_menv(menv); set_ctx(ctx); - unsigned k = m_ctx.size(); - expr e_n = reify(normalize(expected, value_stack(), k), k); - expr g_n = reify(normalize(given, value_stack(), k), k); - return is_convertible_core(e_n, g_n); + unsigned k = m_ctx.size(); + new_given = reify(normalize(new_given, value_stack(), k), k); + new_expected = reify(normalize(new_expected, value_stack(), k), k); + return is_convertible_core(new_given, new_expected); } void clear() { m_ctx = context(); m_cache.clear(); m_menv = nullptr; m_menv_timestamp = 0; } @@ -374,15 +391,19 @@ normalizer::normalizer(environment const & env):normalizer(env, std::numeric_lim normalizer::normalizer(environment const & env, options const & opts):normalizer(env, get_normalizer_max_depth(opts)) {} normalizer::~normalizer() {} expr normalizer::operator()(expr const & e, context const & ctx, metavar_env const * menv) { return (*m_ptr)(e, ctx, menv); } -bool normalizer::is_convertible(expr const & t1, expr const & t2, context const & ctx) { return m_ptr->is_convertible(t1, t2, ctx); } +bool normalizer::is_convertible(expr const & t1, expr const & t2, context const & ctx, + metavar_env * menv, unification_problems * up) { + return m_ptr->is_convertible(t1, t2, ctx, menv, up); +} void normalizer::clear() { m_ptr->clear(); } void normalizer::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); } expr normalize(expr const & e, environment const & env, context const & ctx, metavar_env const * menv) { return normalizer(env)(e, ctx, menv); } -bool is_convertible(expr const & expected, expr const & given, environment const & env, context const & ctx) { - return normalizer(env).is_convertible(expected, given, ctx); +bool is_convertible(expr const & given, expr const & expected, environment const & env, context const & ctx, + metavar_env * menv, unification_problems * up) { + return normalizer(env).is_convertible(given, expected, ctx, menv, up); } } diff --git a/src/kernel/normalizer.h b/src/kernel/normalizer.h index bfcf0d9de..f8c522a38 100644 --- a/src/kernel/normalizer.h +++ b/src/kernel/normalizer.h @@ -14,6 +14,7 @@ namespace lean { class environment; class options; class metavar_env; +class unification_problems; /** \brief Functional object for normalizing expressions */ class normalizer { class imp; @@ -25,7 +26,8 @@ public: ~normalizer(); expr operator()(expr const & e, context const & ctx = context(), metavar_env const * menv = nullptr); - bool is_convertible(expr const & t1, expr const & t2, context const & ctx = context()); + bool is_convertible(expr const & t1, expr const & t2, context const & ctx = context(), + metavar_env * menv = nullptr, unification_problems * up = nullptr); void clear(); @@ -35,5 +37,6 @@ public: }; /** \brief Normalize \c e using the environment \c env and context \c ctx */ expr normalize(expr const & e, environment const & env, context const & ctx = context(), metavar_env const * menv = nullptr); -bool is_convertible(expr const & t1, expr const & t2, environment const & env, context const & ctx = context()); +bool is_convertible(expr const & t1, expr const & t2, environment const & env, context const & ctx = context(), + metavar_env * menv = nullptr, unification_problems * up = nullptr); } diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 589585dbe..e55cba6d9 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -94,7 +94,7 @@ public: while (true) { expr const & c = arg(e, i); expr const & c_t = arg_types[i]; - if (!m_normalizer.is_convertible(abst_domain(f_t), c_t, ctx)) + if (!m_normalizer.is_convertible(c_t, abst_domain(f_t), ctx)) throw app_type_mismatch_exception(m_env, ctx, e, arg_types.size(), arg_types.data()); if (closed(abst_body(f_t))) f_t = abst_body(f_t); @@ -140,7 +140,7 @@ public: expr lt = infer_type(let_value(e), ctx); if (let_type(e)) { infer_universe(let_type(e), ctx); // check if it is really a type - if (!m_normalizer.is_convertible(let_type(e), lt, ctx)) + if (!m_normalizer.is_convertible(lt, let_type(e), ctx)) throw def_type_mismatch_exception(m_env, ctx, let_name(e), let_type(e), let_value(e), lt); } { diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp index bbf49a92d..b73dad4c6 100644 --- a/src/tests/kernel/metavar.cpp +++ b/src/tests/kernel/metavar.cpp @@ -20,13 +20,16 @@ using namespace lean; class unification_problems_dbg : public unification_problems { std::vector> m_eqs; std::vector> m_type_of_eqs; + std::vector> m_is_convertible_cnstrs; public: unification_problems_dbg() {} virtual ~unification_problems_dbg() {} virtual void add_eq(context const &, expr const & lhs, expr const & rhs) { m_eqs.push_back(mk_pair(lhs, rhs)); } virtual void add_type_of_eq(context const &, expr const & n, expr const & t) { m_type_of_eqs.push_back(mk_pair(n, t)); } + virtual void add_is_convertible(context const &, expr const & t1, expr const & t2) { m_is_convertible_cnstrs.push_back(mk_pair(t1, t2)); } std::vector> const & eqs() const { return m_eqs; } std::vector> const & type_of_eqs() const { return m_type_of_eqs; } + std::vector> const & is_convertible_cnstrs() const { return m_is_convertible_cnstrs; } }; static void tst1() {