diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp index 9e07787162..9e5f43422a 100644 --- a/src/kernel/metavar.cpp +++ b/src/kernel/metavar.cpp @@ -67,6 +67,10 @@ void metavar_env::assign(unsigned midx, expr const & v) { m_env[midx] = data(v, p->m_type, p->m_ctx); } +context const & metavar_env::get_context(unsigned midx) const { + return m_env[midx].m_ctx; +} + expr instantiate(expr const & s, meta_ctx const & ctx, metavar_env const & env) { if (ctx) { expr r = instantiate(s, tail(ctx), env); diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h index f2bb5e8aef..d301cfe3c8 100644 --- a/src/kernel/metavar.h +++ b/src/kernel/metavar.h @@ -110,6 +110,11 @@ public: */ void assign(unsigned midx, expr const & t); + /** + \brief Return the context associated with a metavariable. + */ + context const & get_context(unsigned midx) const; + /** \brief Return true if this environment contains the given metavariable diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp index 5a805d1dbc..a876851f03 100644 --- a/src/kernel/normalizer.cpp +++ b/src/kernel/normalizer.cpp @@ -362,16 +362,22 @@ public: 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 (!menv) + return false; + new_given = instantiate_metavars(new_given, *menv); + 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; + if (up) { + up->add_is_convertible(ctx, new_given, new_expected); + return true; + } else { + return false; + } } } set_menv(menv); diff --git a/src/kernel/replace.h b/src/kernel/replace.h index b64d37f7fc..6d0bfe684f 100644 --- a/src/kernel/replace.h +++ b/src/kernel/replace.h @@ -23,10 +23,10 @@ public: \brief Functional for applying F to the subexpressions of a given expression. The signature of \c F is - unsigned, expr -> expr + expr const &, unsigned -> expr F is invoked for each subexpression \c s of the input expression e. - In a call F(n, s), n is the scope level, i.e., the number of + In a call F(s, n), n is the scope level, i.e., the number of bindings operators that enclosing \c s. P is a "post-processing" functional object that is applied to each diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index b83eac0e56..26fe2bc08e 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "util/scoped_map.h" +#include "util/flet.h" #include "kernel/type_checker.h" #include "kernel/environment.h" #include "kernel/kernel_exception.h" @@ -12,16 +13,21 @@ Author: Leonardo de Moura #include "kernel/instantiate.h" #include "kernel/builtin.h" #include "kernel/free_vars.h" +#include "kernel/metavar.h" namespace lean { +static name g_x_name("x"); /** \brief Auxiliary functional object used to implement infer_type. */ class type_checker::imp { typedef scoped_map cache; - environment const & m_env; - cache m_cache; - normalizer m_normalizer; - volatile bool m_interrupted; + environment const & m_env; + cache m_cache; + normalizer m_normalizer; + metavar_env * m_menv; + unsigned m_menv_timestamp; + unification_problems * m_up; + volatile bool m_interrupted; expr lookup(context const & c, unsigned i) { auto p = lookup_ext(c, i); @@ -37,26 +43,48 @@ 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)); + // 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_context(r)) { + // r contains lift/inst operations, so we put the constraint in m_up + m_up->add_eq(ctx, r, p); + } else { + m_menv->assign(r, p); + } + return p; + } throw function_expected_exception(m_env, ctx, s); } -public: - imp(environment const & env): - m_env(env), - m_normalizer(env) { - m_interrupted = false; - } - - level infer_universe(expr const & t, context const & ctx) { - expr u = m_normalizer(infer_type(t, ctx), ctx); + level infer_universe_core(expr const & t, context const & ctx) { + expr u = m_normalizer(infer_type_core(t, ctx), ctx); if (is_type(u)) return ty_level(u); if (u == Bool) return level(); + if (is_metavar(u) && m_up) { + lean_assert(!m_menv->is_assigned(u)); + // 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_context(u)) + m_up->add_eq(ctx, u, Type()); + else + m_menv->assign(u, Type()); + return level(); + } throw type_expected_exception(m_env, ctx, t); } - expr infer_type(expr const & e, context const & ctx) { + expr infer_type_core(expr const & e, context const & ctx) { check_interrupted(m_interrupted); bool shared = false; if (is_shared(e)) { @@ -69,10 +97,11 @@ public: expr r; switch (e.kind()) { case expr_kind::MetaVar: - // TODO(Leo) The following code should be unreachable in the current implementation. - // It will be needed when we implement the new elaborator. - lean_unreachable(); - return e; + if (m_menv && m_up) { + return m_menv->get_type(e, *m_up); + } else { + throw kernel_exception(m_env, "unexpected metavariable occurrence"); + } case expr_kind::Constant: r = m_env.get_object(const_name(e)).get_type(); break; @@ -87,14 +116,14 @@ public: lean_assert(num >= 2); buffer arg_types; for (unsigned i = 0; i < num; i++) { - arg_types.push_back(infer_type(arg(e, i), ctx)); + arg_types.push_back(infer_type_core(arg(e, i), ctx)); } expr f_t = check_pi(arg_types[0], e, ctx); unsigned i = 1; while (true) { expr const & c = arg(e, i); expr const & c_t = arg_types[i]; - if (!m_normalizer.is_convertible(c_t, abst_domain(f_t), ctx)) + if (!is_convertible_core(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); @@ -112,40 +141,40 @@ public: break; } case expr_kind::Eq: - infer_type(eq_lhs(e), ctx); - infer_type(eq_rhs(e), ctx); + infer_type_core(eq_lhs(e), ctx); + infer_type_core(eq_rhs(e), ctx); r = mk_bool_type(); break; case expr_kind::Lambda: { - infer_universe(abst_domain(e), ctx); + infer_universe_core(abst_domain(e), ctx); expr t; { cache::mk_scope sc(m_cache); - t = infer_type(abst_body(e), extend(ctx, abst_name(e), abst_domain(e))); + t = infer_type_core(abst_body(e), extend(ctx, abst_name(e), abst_domain(e))); } r = mk_pi(abst_name(e), abst_domain(e), t); break; } case expr_kind::Pi: { - level l1 = infer_universe(abst_domain(e), ctx); + level l1 = infer_universe_core(abst_domain(e), ctx); level l2; { cache::mk_scope sc(m_cache); - l2 = infer_universe(abst_body(e), extend(ctx, abst_name(e), abst_domain(e))); + l2 = infer_universe_core(abst_body(e), extend(ctx, abst_name(e), abst_domain(e))); } r = mk_type(max(l1, l2)); break; } case expr_kind::Let: { - expr lt = infer_type(let_value(e), ctx); + expr lt = infer_type_core(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(lt, let_type(e), ctx)) + infer_universe_core(let_type(e), ctx); // check if it is really a type + if (!is_convertible_core(lt, let_type(e), ctx)) throw def_type_mismatch_exception(m_env, ctx, let_name(e), let_type(e), let_value(e), lt); } { cache::mk_scope sc(m_cache); - expr t = infer_type(let_body(e), extend(ctx, let_name(e), lt, let_value(e))); + expr t = infer_type_core(let_body(e), extend(ctx, let_name(e), lt, let_value(e))); r = instantiate(t, let_value(e)); } break; @@ -169,8 +198,50 @@ public: return r; } - bool is_convertible(expr const & t1, expr const & t2, context const & ctx) { - return m_normalizer.is_convertible(t1, t2, ctx); + bool is_convertible_core(expr const & t1, expr const & t2, context const & ctx) { + return m_normalizer.is_convertible(t1, t2, ctx, m_menv, m_up); + } + + 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 + if (m_menv && m_menv->get_timestamp() > m_menv_timestamp) { + clear(); + m_menv_timestamp = m_menv->get_timestamp(); + } + } else { + clear(); + m_menv = menv; + m_menv_timestamp = m_menv ? m_menv->get_timestamp() : 0; + } + } + +public: + imp(environment const & env): + m_env(env), + m_normalizer(env) { + m_menv = nullptr; + m_menv_timestamp = 0; + m_up = nullptr; + m_interrupted = false; + } + + level infer_universe(expr const & t, context const & ctx, metavar_env * menv, unification_problems * up) { + set_menv(menv); + flet 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_menv(menv); + flet 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_menv(menv); + flet set(m_up, up); + return is_convertible_core(t1, t2, ctx); } void set_interrupt(bool flag) { @@ -190,11 +261,17 @@ 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) { return m_ptr->infer_type(e, ctx); } -level type_checker::infer_universe(expr const & e, context const & ctx) { return m_ptr->infer_universe(e, ctx); } +expr type_checker::infer_type(expr const & e, context const & ctx, metavar_env * menv, unification_problems * up) { + return m_ptr->infer_type(e, ctx, menv, up); +} +level type_checker::infer_universe(expr const & e, context const & ctx, metavar_env * menv, unification_problems * up) { + return m_ptr->infer_universe(e, ctx, menv, up); +} void type_checker::clear() { m_ptr->clear(); } void type_checker::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); } -bool type_checker::is_convertible(expr const & t1, expr const & t2, context const & ctx) { return m_ptr->is_convertible(t1, t2, ctx); } +bool type_checker::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); +} normalizer & type_checker::get_normalizer() { return m_ptr->get_normalizer(); } expr infer_type(expr const & e, environment const & env, context const & ctx) { diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index 5c87f59791..884b620a24 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -12,6 +12,8 @@ Author: Leonardo de Moura namespace lean { class environment; class normalizer; +class metavar_env; +class unification_problems; /** \brief Lean Type Checker. It can also be used to infer types, universes and check whether a type \c A is convertible to a type \c B. @@ -23,10 +25,19 @@ public: type_checker(environment const & env); ~type_checker(); - expr infer_type(expr const & e, context const & ctx = context()); - level infer_universe(expr const & e, context const & ctx = context()); - void check(expr const & e, context const & ctx = context()) { infer_type(e, ctx); } - bool is_convertible(expr const & t1, expr const & t2, context const & ctx = context()); + expr infer_type(expr const & e, context const & ctx = context(), + metavar_env * menv = nullptr, unification_problems * up = nullptr); + + level infer_universe(expr const & e, context const & ctx = context(), + metavar_env * menv = nullptr, unification_problems * up = nullptr); + + void check(expr const & e, context const & ctx = context(), + metavar_env * menv = nullptr, unification_problems * up = nullptr) { + infer_type(e, ctx, menv, up); + } + + bool is_convertible(expr const & t1, expr const & t2, context const & ctx = context(), + metavar_env * menv = nullptr, unification_problems * up = nullptr); void clear(); diff --git a/src/library/placeholder.cpp b/src/library/placeholder.cpp index 2df1401a32..dc63673aba 100644 --- a/src/library/placeholder.cpp +++ b/src/library/placeholder.cpp @@ -5,7 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "kernel/occurs.h" +#include "kernel/metavar.h" +#include "kernel/expr_maps.h" +#include "kernel/replace.h" #include "library/placeholder.h" +#include "library/replace_using_ctx.h" namespace lean { static name g_placeholder_name("_"); @@ -20,4 +24,19 @@ bool is_placeholder(expr const & e) { bool has_placeholder(expr const & e) { return occurs(mk_placholder(), e); } + +expr replace_placeholders_with_metavars(expr const & e, metavar_env & menv, expr_map * trace) { + auto f = [&](expr const & e, context const & ctx, unsigned offset) -> expr { + if (is_placeholder(e)) { + return menv.mk_metavar(ctx); + } else { + return e; + } + }; + auto p = [&](expr const & s, expr const & t) { + if (trace) + (*trace)[t] = s; + }; + return replace_using_ctx_fn(f, p)(e); +} } diff --git a/src/library/placeholder.h b/src/library/placeholder.h index 28ec542e90..55e5553449 100644 --- a/src/library/placeholder.h +++ b/src/library/placeholder.h @@ -6,8 +6,10 @@ Author: Leonardo de Moura */ #pragma once #include "kernel/expr.h" +#include "kernel/expr_maps.h" namespace lean { +class metavar_env; /** \brief Return a new placeholder expression. To be able to track location, a new constant for each placeholder. @@ -23,4 +25,11 @@ bool is_placeholder(expr const & e); \brief Return true iff the given expression contains placeholders. */ bool has_placeholder(expr const & e); + +/** + \brief Replace the placeholders in \c e with fresh metavariables from menv. + if \c trace is not null, then for each new expression \c t created based on + \c s, we store (*trace)[t] = s. We say this is traceability information. +*/ +expr replace_placeholders_with_metavars(expr const & e, metavar_env & menv, expr_map * trace = nullptr); } diff --git a/src/library/replace_using_ctx.h b/src/library/replace_using_ctx.h new file mode 100644 index 0000000000..db3f6931b4 --- /dev/null +++ b/src/library/replace_using_ctx.h @@ -0,0 +1,99 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "util/scoped_map.h" +#include "kernel/replace.h" + +namespace lean { +/** + \brief Functional for applying F to the subexpressions of a given expression. + + The signature of \c F is + expr const &, context const & ctx, unsigned n -> expr + + F is invoked for each subexpression \c s of the input expression e. + In a call F(s, c, n), \c c is the context where \c s occurs, + and \c n is the size of \c c. + + P is a "post-processing" functional object that is applied to each + pair (old, new) +*/ +template +class replace_using_ctx_fn { + static_assert(std::is_same::type, expr>::value, + "replace_using_ctx_fn: return type of F is not expr"); + typedef scoped_map cache; + cache m_cache; + F m_f; + P m_post; + + expr apply(expr const & e, context const & ctx, unsigned offset) { + bool shared = false; + if (is_shared(e)) { + shared = true; + auto it = m_cache.find(e); + if (it != m_cache.end()) + return it->second; + } + + expr r = m_f(e, ctx, offset); + if (is_eqp(e, r)) { + switch (e.kind()) { + case expr_kind::Type: case expr_kind::Value: case expr_kind::Constant: + case expr_kind::Var: case expr_kind::MetaVar: + break; + case expr_kind::App: + r = update_app(e, [=](expr const & c) { return apply(c, ctx, offset); }); + break; + case expr_kind::Eq: + r = update_eq(e, [=](expr const & l, expr const & r) { return std::make_pair(apply(l, ctx, offset), apply(r, ctx, offset)); }); + break; + case expr_kind::Lambda: + case expr_kind::Pi: + r = update_abst(e, [=](expr const & t, expr const & b) { + expr new_t = apply(t, ctx, offset); + expr new_b; + { + cache::mk_scope sc(m_cache); + new_b = apply(b, extend(ctx, abst_name(e), new_t), offset + 1); + } + return std::make_pair(new_t, new_b); + }); + break; + case expr_kind::Let: + r = update_let(e, [=](expr const & t, expr const & v, expr const & b) { + expr new_t = t ? apply(t, ctx, offset) : expr(); + expr new_v = apply(v, ctx, offset); + expr new_b; + { + cache::mk_scope sc(m_cache); + new_b = apply(b, extend(ctx, abst_name(e), new_t, new_v), offset+1); + } + return std::make_tuple(new_t, new_v, new_b); + }); + break; + } + } + + if (shared) + m_cache.insert(std::make_pair(e, r)); + + m_post(e, r); + return r; + } + +public: + replace_using_ctx_fn(F const & f, P const & p = P()): + m_f(f), + m_post(p) { + } + + expr operator()(expr const & e, context const & ctx = context()) { + return apply(e, ctx, ctx.size()); + } +}; +} diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp index b73dad4c61..bf50588489 100644 --- a/src/tests/kernel/metavar.cpp +++ b/src/tests/kernel/metavar.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include #include #include #include @@ -14,22 +15,35 @@ Author: Leonardo de Moura #include "kernel/free_vars.h" #include "kernel/normalizer.h" #include "kernel/environment.h" +#include "kernel/type_checker.h" #include "library/printer.h" +#include "library/placeholder.h" 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; + typedef std::tuple constraint; + typedef std::vector constraints; + constraints m_eqs; + constraints m_type_of_eqs; + constraints 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; } + virtual void add_eq(context const & ctx, expr const & lhs, expr const & rhs) { m_eqs.push_back(constraint(ctx, lhs, rhs)); } + virtual void add_type_of_eq(context const & ctx, expr const & n, expr const & t) { m_type_of_eqs.push_back(constraint(ctx, n, t)); } + virtual void add_is_convertible(context const & ctx, expr const & t1, expr const & t2) { m_is_convertible_cnstrs.push_back(constraint(ctx, t1, t2)); } + constraints const & eqs() const { return m_eqs; } + constraints const & type_of_eqs() const { return m_type_of_eqs; } + constraints const & is_convertible_cnstrs() const { return m_is_convertible_cnstrs; } + friend std::ostream & operator<<(std::ostream & out, unification_problems_dbg const & up) { + 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"; + for (auto c : up.m_is_convertible_cnstrs) + std::cout << std::get<0>(c) << " |- " << std::get<1>(c) << " --> " << std::get<2>(c) << "\n"; + return out; + } }; static void tst1() { @@ -56,7 +70,7 @@ static void tst1() { lean_assert(u.eqs().empty()); lean_assert(u.type_of_eqs().size() == 2); for (auto p : u.type_of_eqs()) { - std::cout << "typeof(" << p.first << ") == " << p.second << "\n"; + std::cout << "typeof(" << std::get<1>(p) << ") == " << std::get<2>(p) << "\n"; } expr f = Const("f"); expr a = Const("a"); @@ -446,6 +460,43 @@ static void tst21() { add_lift(m1, 1, 7)); } +#define _ mk_placholder() + +static void tst22() { + metavar_env menv; + expr f = Const("f"); + expr x = Const("x"); + expr N = Const("N"); + expr F = f(Fun({x, N}, f(_, x)), _); + std::cout << F << "\n"; + std::cout << replace_placeholders_with_metavars(F, menv) << "\n"; + lean_assert(menv.contains(0)); + lean_assert(menv.contains(1)); + lean_assert(!menv.contains(2)); + lean_assert(menv.get_context(0).size() == 1); + lean_assert(lookup(menv.get_context(0), 0).get_domain() == N); + lean_assert(menv.get_context(1).size() == 0); +} + +static void tst23() { + environment env; + metavar_env menv; + unification_problems_dbg up; + type_checker checker(env); + expr N = Const("N"); + expr f = Const("f"); + expr a = Const("a"); + env.add_var("N", Type()); + env.add_var("f", N >> (N >> N)); + env.add_var("a", N); + expr x = Const("x"); + expr F0 = f(Fun({x, N}, f(_, x))(a), _); + expr F1 = replace_placeholders_with_metavars(F0, menv); + std::cout << F1 << "\n"; + std::cout << checker.infer_type(F1, context(), &menv, &up) << "\n"; + std::cout << up << "\n"; +} + int main() { tst1(); tst2(); @@ -468,5 +519,7 @@ int main() { tst19(); tst20(); tst21(); + tst22(); + tst23(); return has_violations() ? 1 : 0; }