From 2f29ff70d7837e65a3172f64124ef20cef158ec2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 18 Sep 2013 20:46:00 -0700 Subject: [PATCH] Implement higher-order unification Signed-off-by: Leonardo de Moura --- src/frontends/lean/elaborator.cpp | 14 +- src/kernel/metavar.cpp | 60 +++- src/kernel/metavar.h | 34 ++- src/kernel/type_checker.cpp | 6 +- src/library/ho_unifier.cpp | 447 +++++++++++++++++++++++++++++- src/library/ho_unifier.h | 27 +- src/library/light_checker.cpp | 61 +++- src/library/light_checker.h | 4 +- src/library/reduce.cpp | 17 ++ src/library/reduce.h | 1 + src/tests/kernel/metavar.cpp | 13 + src/tests/library/CMakeLists.txt | 3 + src/tests/library/ho_unifier.cpp | 40 +++ 13 files changed, 660 insertions(+), 67 deletions(-) create mode 100644 src/tests/library/ho_unifier.cpp diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 3b6d1cb0e9..c81183d381 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -211,7 +211,7 @@ class elaborator::imp { } } else if (has_assigned_metavar(e)) { return check_pi(instantiate(e), ctx, s, s_ctx); - } else if (is_metavar(e) && !has_context(e)) { + } else if (is_metavar(e) && !has_meta_context(e)) { // e is a unassigned metavariable that must be a Pi, // then we can assign it to (Pi x : A, B x), where // A and B are fresh metavariables @@ -551,7 +551,7 @@ class elaborator::imp { } void solve_mvar(expr const & m, expr const & t, constraint const & c) { - lean_assert(is_metavar(m) && !has_context(m)); + lean_assert(is_metavar(m) && !has_meta_context(m)); unsigned midx = metavar_idx(m); if (m_metavars[midx].m_assignment) { m_constraints.push_back(constraint(m_metavars[midx].m_assignment, t, c)); @@ -577,7 +577,7 @@ class elaborator::imp { \brief Temporary hack until we build the new elaborator. */ bool is_lift(expr const & e, expr & c, unsigned & s, unsigned & n) { - if (!is_metavar(e) || !has_context(e)) + if (!is_metavar(e) || !has_meta_context(e)) return false; meta_ctx const & ctx = metavar_ctx(e); meta_entry const & entry = head(ctx); @@ -596,7 +596,7 @@ class elaborator::imp { \brief Temporary hack until we build the new elaborator. */ bool is_inst(expr const & e, expr & c, unsigned & s, expr & v) { - if (!is_metavar(e) || !has_context(e)) + if (!is_metavar(e) || !has_meta_context(e)) return false; meta_ctx const & ctx = metavar_ctx(e); meta_entry const & entry = head(ctx); @@ -612,7 +612,7 @@ class elaborator::imp { } bool solve_meta(expr const & e, expr const & t, constraint const & c) { - lean_assert(has_context(e)); + lean_assert(has_meta_context(e)); expr const & m = e; unsigned midx = metavar_idx(m); unsigned i, s, n; @@ -667,10 +667,10 @@ class elaborator::imp { if (lhs == rhs || (!has_metavar(lhs) && !has_metavar(rhs))) { // do nothing delayed = 0; - } else if (is_metavar(lhs) && !has_context(lhs)) { + } else if (is_metavar(lhs) && !has_meta_context(lhs)) { delayed = 0; solve_mvar(lhs, rhs, c); - } else if (is_metavar(rhs) && !has_context(rhs)) { + } else if (is_metavar(rhs) && !has_meta_context(rhs)) { delayed = 0; solve_mvar(rhs, lhs, c); } else if (is_metavar(lhs) || is_metavar(rhs)) { diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp index 9e5f43422a..f751095894 100644 --- a/src/kernel/metavar.cpp +++ b/src/kernel/metavar.cpp @@ -24,13 +24,17 @@ void metavar_env::inc_timestamp() { metavar_env::metavar_env():m_timestamp(0) {} -expr metavar_env::mk_metavar(context const & ctx) { +expr metavar_env::mk_metavar(expr const & type, context const & ctx) { inc_timestamp(); unsigned midx = m_env.size(); - m_env.push_back(data(ctx)); + m_env.push_back(data(type, ctx)); return ::lean::mk_metavar(midx); } +expr metavar_env::mk_metavar(context const & ctx) { + return mk_metavar(expr(), ctx); +} + bool metavar_env::contains(unsigned midx) const { return midx < m_env.size(); } @@ -39,10 +43,23 @@ bool metavar_env::is_assigned(unsigned midx) const { return m_env[midx].m_subst; } -expr metavar_env::get_subst(unsigned midx) const { +expr metavar_env::get_subst_core(unsigned midx) const { return m_env[midx].m_subst; } +expr metavar_env::get_subst(unsigned midx) const { + expr r = m_env[midx].m_subst; + if (r && has_assigned_metavar(r, *this)) { + r = instantiate_metavars(r, *this); + expr t = m_env[midx].m_type; + context ctx = m_env[midx].m_ctx; + const_cast(this)->m_env[midx] = data(r, t, ctx); + return r; + } else { + return r; + } +} + expr metavar_env::get_type(unsigned midx, unification_problems & up) { auto p = m_env[midx]; expr t = p->m_type; @@ -60,6 +77,10 @@ expr metavar_env::get_type(unsigned midx, unification_problems & up) { } } +expr metavar_env::get_type(unsigned midx) const { + return m_env[midx].m_type; +} + void metavar_env::assign(unsigned midx, expr const & v) { inc_timestamp(); lean_assert(!is_assigned(midx)); @@ -96,13 +117,7 @@ expr metavar_env::get_subst(expr const & m) const { expr metavar_env::get_type(expr const & m, unification_problems & up) { expr s = get_type(metavar_idx(m), up); - lean_assert(is_metavar(s)); - lean_assert(!metavar_ctx(s)); - meta_ctx const & ctx = metavar_ctx(m); - if (ctx) - return ::lean::mk_metavar(metavar_idx(s), ctx); - else - return s; + return instantiate(s, metavar_ctx(m), *this); } void metavar_env::assign(expr const & m, expr const & t) { @@ -166,15 +181,34 @@ expr add_inst(expr const & m, unsigned s, expr const & v) { return mk_metavar(metavar_idx(m), add_inst(metavar_ctx(m), s, v)); } -bool has_context(expr const & m) { +bool has_meta_context(expr const & m) { return metavar_ctx(m); } -expr pop_context(expr const & m) { - lean_assert(has_context(m)); +expr pop_meta_context(expr const & m) { + lean_assert(has_meta_context(m)); return mk_metavar(metavar_idx(m), tail(metavar_ctx(m))); } +struct found_assigned {}; +bool has_assigned_metavar(expr const & e, metavar_env const & menv) { + if (!has_metavar(e)) { + return false; + } else { + auto proc = [&](expr const & n, unsigned offset) { + if (is_metavar(n) && menv.contains(n) && menv.is_assigned(n)) + throw found_assigned(); + }; + for_each_fn visitor(proc); + try { + visitor(e); + return false; + } catch (found_assigned&) { + return true; + } + } +} + /** \brief Auxiliary exception used to sign that a metavariable was found in an expression. diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h index d301cfe3c8..109e24fe6c 100644 --- a/src/kernel/metavar.h +++ b/src/kernel/metavar.h @@ -46,7 +46,7 @@ class metavar_env { expr m_subst; expr m_type; context m_ctx; - data(context const & ctx):m_ctx(ctx) {} + data(expr const & t, context const & ctx):m_type(t), m_ctx(ctx) {} data(expr const & s, expr const & t, context const & ctx):m_subst(s), m_type(t), m_ctx(ctx) {} }; pvector m_env; @@ -61,11 +61,21 @@ public: */ unsigned get_timestamp() const { return m_timestamp; } + /** + \brief Return the number of metavariables in this metavar_env. + */ + unsigned size() const { return m_env.size(); } + /** \brief Create new metavariable in this environment. */ expr mk_metavar(context const & ctx = context()); + /** + \brief Create a new metavariable with the given type and context. + */ + expr mk_metavar(expr const & type, context const & ctx = context()); + /** \brief Return true if this environment contains a metavariable with id \c midx. That is, it has an entry of the form @@ -91,6 +101,8 @@ public: */ expr get_subst(unsigned midx) const; + expr get_subst_core(unsigned midx) const; + /** \brief Return the type of the metavariable with id \c midx in this environment. @@ -103,6 +115,12 @@ public: */ expr get_type(unsigned midx, unification_problems & up); + /** + \brief Return type of the metavariable with id \c midx in this environment. + If the metavariable is not associated with any type, then return the null expression. + */ + expr get_type(unsigned midx) const; + /** \brief Assign the metavariable with id \c midx to the term \c t. @@ -192,19 +210,27 @@ meta_ctx add_inst(meta_ctx const & ctx, unsigned s, expr const & v); \pre is_metavar(m) */ -bool has_context(expr const & m); +bool has_meta_context(expr const & m); /** \brief Return the same metavariable, but the head of the context is removed. \pre is_metavar(m) - \pre has_context(m) + \pre has_meta_context(m) */ -expr pop_context(expr const & m); +expr pop_meta_context(expr const & m); + +/** + \brief Return true iff \c e has a metavariable that is assigned in menv. +*/ +bool has_assigned_metavar(expr const & e, metavar_env const & menv); /** \brief Return true iff \c e contains the metavariable with index \c midx. The substitutions in \c menv are taken into account. */ bool has_metavar(expr const & e, unsigned midx, metavar_env const & menv = metavar_env()); +inline bool has_metavar(expr const & e, expr const & m, metavar_env const & menv = metavar_env()) { + return has_metavar(e, metavar_idx(m), menv); +} } diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 26fe2bc08e..0954b669d9 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -50,7 +50,7 @@ class type_checker::imp { 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)) { + 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 { @@ -75,7 +75,7 @@ class type_checker::imp { // 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)) + if (has_meta_context(u)) m_up->add_eq(ctx, u, Type()); else m_menv->assign(u, Type()); @@ -252,6 +252,8 @@ public: void clear() { m_cache.clear(); m_normalizer.clear(); + m_menv = nullptr; + m_menv_timestamp = 0; } normalizer & get_normalizer() { diff --git a/src/library/ho_unifier.cpp b/src/library/ho_unifier.cpp index b3410d9610..c62d59e349 100644 --- a/src/library/ho_unifier.cpp +++ b/src/library/ho_unifier.cpp @@ -4,39 +4,462 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include +#include "util/pvector.h" +#include "util/pdeque.h" +#include "util/exception.h" #include "kernel/environment.h" +#include "kernel/free_vars.h" +#include "kernel/instantiate.h" +#include "kernel/normalizer.h" +#include "library/light_checker.h" +#include "library/reduce.h" +#include "library/update_expr.h" #include "library/ho_unifier.h" +#include "library/printer.h" namespace lean { +static name g_x_name("x"); class ho_unifier::imp { + typedef std::tuple constraint; + typedef pdeque cqueue; // constraint queue + struct state { + unsigned m_id; + metavar_env m_subst; + cqueue m_queue; + state(unsigned id, metavar_env const & menv, cqueue const & q): + m_id(id), m_subst(menv), m_queue(q) {} + }; + typedef std::vector state_stack; + environment m_env; + normalizer m_normalizer; + light_checker m_type_infer; + state_stack m_state_stack; + unsigned m_delayed; + unsigned m_next_state_id; + bool m_ho; // true if used higher-order volatile bool m_interrupted; + static metavar_env & subst_of(state & s) { return s.m_subst; } + static cqueue & queue_of(state & s) { return s.m_queue; } + + state mk_state(metavar_env const & s, cqueue const & q) { + unsigned id = m_next_state_id; + m_next_state_id++; + return state(id, s, q); + } + + void reset_delayed() { + m_delayed = 0; + } + + /** + \brief Add a constraint to the state in the top of the state_stack + */ + void add_constraint(context const & ctx, expr const & l, expr const & r) { + lean_assert(!m_state_stack.empty()); + state & s = m_state_stack.back(); + queue_of(s).push_front(constraint(ctx, l, r)); + reset_delayed(); + } + + /** + \brief Add a constraint to the state in the top of the state_stack, + but put the constraint in the end of the queue, and increase the m_delayed counter. + */ + void postpone_constraint(context const & ctx, expr const & l, expr const & r) { + lean_assert(!m_state_stack.empty()); + state & s = m_state_stack.back(); + queue_of(s).push_back(constraint(ctx, l, r)); + m_delayed++; + } + + void init(context const & ctx, expr const & l, expr const & r, metavar_env const & menv) { + m_next_state_id = 0; + m_ho = false; + m_state_stack.clear(); + m_state_stack.push_back(mk_state(menv, cqueue())); + add_constraint(ctx, l, r); + } + + metavar_env cleanup_subst(metavar_env const & s, unsigned num_input_metavars) { + // eliminate auxiliary metavariables + if (!m_ho) { + return s; + } else { + metavar_env new_s; + for (unsigned i = 0; i < num_input_metavars; i++) { + new_s.mk_metavar(s.get_type(i), s.get_context(i)); + expr subst = s.get_subst(i); + if (subst) + new_s.assign(i, subst); + } + return new_s; + } + } + + list save_result(list const & r, metavar_env const & s, residue const & rs, unsigned num_input_metavars) { + return cons(result(cleanup_subst(s, num_input_metavars), rs), r); + } + + /** + Process a == b when: + 1- \c a is an assigned metavariable + 2- \c a is a unassigned metavariable without a metavariable context. + 3- \c a is a unassigned metavariable of the form ?m[lift:s:n, ...], and \c b does not have + a free variable in the range [s, s+n). + 4- \c a is an application of the form (?m ...) where ?m is an assigned metavariable. + */ + enum status { Solved, Failed, Continue }; + status process_metavar(expr & a, expr & b, metavar_env & s) { + if (is_metavar(a)) { + if (s.is_assigned(a)) { + // Case 1 + a = s.get_subst(a); + } else if (!has_meta_context(a)) { + // Case 2 + if (has_metavar(b, a, s)) { + return Failed; + } else { + s.assign(a, b); + reset_delayed(); + return Solved; + } + } else { + meta_entry const & me = head(metavar_ctx(a)); + if (me.is_lift() && !has_free_var(b, me.s(), me.s() + me.n())) { + // Case 3 + b = lower_free_vars(b, me.s() + me.n(), me.n()); + a = pop_meta_context(a); + } + } + } + + if (is_app(a) && is_metavar(arg(a, 0)) && s.is_assigned(arg(a, 0))) { + // Case 4 + a = update_app(a, 0, s.get_subst(arg(a, 0))); + } + return Continue; + } + + /** \brief Unfold let-expression */ + void process_let(expr & a) { + if (is_let(a)) + a = instantiate(let_body(a), let_value(a)); + } + + /** \brief Unfold constants */ + void process_constant(expr & a) { + if (is_constant(a)) { + object const & obj = m_env.find_object(const_name(a)); + if (obj && obj.is_definition() && !obj.is_opaque()) + a = obj.get_value(); + } + } + + /** \brief Replace variables by their definition if the context contains it. */ + void process_var(context const & ctx, expr & a) { + if (is_var(a)) { + try { + context_entry const & e = lookup(ctx, var_idx(a)); + if (e.get_body()) + a = e.get_body(); + } catch (exception&) { + } + } + } + + /** \brief Applies simple unfolding steps */ + void process_simple(context const & ctx, expr & a) { + process_let(a); + process_constant(a); + process_var(ctx, a); + } + + /** \brief Process the application's function using \c process_simple */ + void process_app_function(context const & ctx, expr & a) { + if (is_app(a)) { + expr f = arg(a, 0); + process_simple(ctx, f); + a = update_app(a, 0, f); + } + } + + /** \brief Creates a subproblem based on the application arguments */ + bool process_app_args(context const & ctx, expr const & a, expr const & b, unsigned start) { + lean_assert(is_app(a) && is_app(b)); + if (num_args(a) != num_args(b)) { + return false; + } else { + for (unsigned i = 1; i < num_args(a); i++) { + add_constraint(ctx, arg(a, i), arg(b, i)); + } + return true; + } + } + + /** + Process a constraint ctx |- a = b, where \c a and \c b + are applications and the function is the same. + That is, arg(a, 0) == arg(b, 0) + + \pre is_app(a) && is_app(b) && arg(a, 0) == arg(b, 0) + */ + bool process_easy_app(context const & ctx, expr const & a, expr const & b) { + lean_assert(is_app(a) && is_app(b) && arg(a, 0) == arg(b, 0)); + return process_app_args(ctx, a, b, 1); + } + + /** \brief Return true if \c a is of the form (?m ...) */ + bool is_meta_app(expr const & a) { + return is_app(a) && is_metavar(arg(a, 0)); + } + + /** + Auxiliary class for invoking m_type_infer. + If it creates a new unfication problem we mark m_failed to true. + add_eq can be easily supported, but we need to extend ho_unifier API to be able + to support add_type_of_eq and add_is_convertible. + The m_type_infer only invokes add_type_of_eq when it needs to ask for the type + of a metavariable that does not have a type yet. + One possible workaround it o make sure that every metavariable has an associated type + before invoking ho_unifier. + */ + class unification_problems_wrapper : public unification_problems { + bool m_failed; + public: + unification_problems_wrapper():m_failed(false) {} + virtual void add_eq(context const & ctx, expr const & lhs, expr const & rhs) { m_failed = true; } + virtual void add_type_of_eq(context const & ctx, expr const & n, expr const & t) { m_failed = true; } + virtual void add_is_convertible(context const & ctx, expr const & t1, expr const & t2) { m_failed = true; } + bool failed() const { return m_failed; } + }; + + /** + \brief Process a constraint ctx |- a = b where \c a is of the form (?m ...). + We perform a "case split" using "projection" or "imitation". See Huet&Lang's paper on higher order matching + for further details. + */ + bool process_meta_app(context const & ctx, expr const & a, expr const & b) { + lean_assert(is_meta_app(a)); + lean_assert(!is_meta_app(b)); + m_ho = true; // using higher-order matching + expr f_a = arg(a, 0); + lean_assert(is_metavar(f_a)); + state top_state = m_state_stack.back(); + cqueue q = queue_of(top_state); + metavar_env s = subst_of(top_state); + unsigned midx = metavar_idx(f_a); + unsigned num_a = num_args(a); + unification_problems_wrapper upw; + buffer arg_types; + for (unsigned i = 1; i < num_a; i++) { + arg_types.push_back(m_type_infer(arg(a, i), ctx, &s, &upw)); + } + // clear the cache since we don't want a reference to s inside of m_type_infer + m_type_infer.clear(); + if (upw.failed()) + return false; + m_state_stack.pop_back(); + // add projections + for (unsigned i = 1; i < num_a; i++) { + expr proj = mk_var(i - 1); + for (unsigned j = 1; j < num_a; j++) + proj = mk_lambda(name(g_x_name, j), arg_types[j - 1], proj); + cqueue new_q = q; + new_q.push_front(constraint(ctx, arg(a, i), b)); + metavar_env new_s = s; + new_s.assign(midx, proj); + m_state_stack.push_back(mk_state(new_s, new_q)); + } + // add imitation + metavar_env new_s = s; + cqueue new_q = q; + if (is_app(b)) { + expr f_b = arg(b, 0); + unsigned num_b = num_args(b); + buffer imitation_args; // arguments for the imitation + imitation_args.push_back(f_b); + for (unsigned i = 1; i < num_b; i++) { + expr h_i = new_s.mk_metavar(ctx); + buffer h_app_var_args; + buffer h_app_subst_args; + h_app_var_args.push_back(h_i); + h_app_subst_args.push_back(h_i); + for (unsigned j = 1; j < num_a; j++) { + h_app_var_args.push_back(mk_var(num_a - j - 1)); + h_app_subst_args.push_back(arg(a, j)); + } + imitation_args.push_back(mk_app(h_app_var_args.size(), h_app_var_args.data())); + new_q.push_front(constraint(ctx, mk_app(h_app_subst_args.size(), h_app_subst_args.data()), arg(b, i))); + } + expr imitation = mk_app(imitation_args.size(), imitation_args.data()); + for (unsigned j = 1; j < num_a; j++) + imitation = mk_lambda(name(g_x_name, j), arg_types[j - 1], imitation); + new_s.assign(midx, imitation); + m_state_stack.push_back(mk_state(new_s, new_q)); + } else { + // TODO(Leo) handle eq like we handle applications + // make f_a the constant function + expr imitation = lift_free_vars(b, 0, num_a - 1); + for (unsigned j = 1; j < num_a; j++) + imitation = mk_lambda(name(g_x_name, j), arg_types[j - 1], imitation); + new_s.assign(midx, imitation); + m_state_stack.push_back(mk_state(new_s, new_q)); + } + reset_delayed(); + return true; + } + + /** + \brief Process the constraint \c c. Return true if the constraint was processed or postponed, and false + if it failed to solve the constraint. + */ + bool process(constraint const & c, metavar_env & s) { + context ctx = std::get<0>(c); + expr const & old_a = std::get<1>(c); + expr const & old_b = std::get<2>(c); + expr a = old_a; + expr b = old_b; + if (a == b) { + reset_delayed(); + return true; + } + if (is_app(a) && is_app(b) && arg(a, 0) == arg(b, 0)) + return process_easy_app(ctx, a, b); + status r; + r = process_metavar(a, b, s); + if (r != Continue) { return r == Solved; } + r = process_metavar(b, a, s); + if (r != Continue) { return r == Solved; } + process_simple(ctx, a); + process_simple(ctx, b); + process_app_function(ctx, a); + process_app_function(ctx, b); + if ((is_app(a) && !is_eqp(a, old_a)) || (is_app(b) && !is_eqp(b, old_b))) { + // some progress was made + add_constraint(ctx, a, b); + return true; + } + a = head_beta_reduce(a); + b = head_beta_reduce(b); + if ((is_metavar(a) && has_meta_context(a)) || + (is_metavar(b) && has_meta_context(b))) { + // a or b is a metavariable that has a metavariable context associated with it. + // postpone + postpone_constraint(ctx, a, b); + return true; + } + if (!is_app(a) && !is_app(b)) { + if (a.kind() != b.kind()) + return false; + switch (a.kind()) { + case expr_kind::Constant: case expr_kind::Var: case expr_kind::Value: case expr_kind::Type: + return false; + case expr_kind::Eq: + add_constraint(ctx, eq_lhs(a), eq_lhs(b)); + add_constraint(ctx, eq_rhs(a), eq_rhs(b)); + return true; + case expr_kind::Lambda: case expr_kind::Pi: + add_constraint(ctx, abst_domain(a), abst_domain(b)); + add_constraint(extend(ctx, abst_name(a), abst_domain(a)), abst_body(a), abst_body(b)); + return true; + case expr_kind::Let: case expr_kind::MetaVar: case expr_kind::App: + lean_unreachable(); + return false; + } + } + + if (is_meta_app(a)) { + if (is_meta_app(b)) { + postpone_constraint(ctx, a, b); + return true; + } else { + return process_meta_app(ctx, a, b); + return true; + } + } else if (is_meta_app(b)) { + lean_assert(!is_meta_app(b)); + return process_meta_app(ctx, b, a); + } + + if (!is_eqp(a, old_a) || !is_eqp(b, old_b)) { + // some progress was made + add_constraint(ctx, a, b); + return true; + } + + expr norm_a = m_normalizer(a, ctx, &s); + expr norm_b = m_normalizer(b, ctx, &s); + if (norm_a.kind() != norm_b.kind()) + return false; + if (is_app(norm_a)) { + return process_app_args(ctx, norm_a, norm_b, 0); + } else if (a == norm_a && b == norm_b) { + return false; + } else { + // some progress was made + add_constraint(ctx, norm_a, norm_b); + return true; + } + } + public: - imp(environment const & env):m_env(env) { + imp(environment const & env):m_env(env), m_normalizer(env), m_type_infer(env) { m_interrupted = false; - // TODO(Leo) + m_delayed = 0; } - bool unify(context const & ctx, expr const & l, expr const & r, metavar_env & menv, unification_problems & up) { - // TODO(Leo) - return false; - } - - void clear() { - // TODO(Leo) + list unify(context const & ctx, expr const & a, expr const & b, metavar_env const & menv) { + unsigned num_metavars = menv.size(); + init(ctx, a, b, menv); + list r; + while (!m_state_stack.empty()) { + check_interrupted(m_interrupted); + state & top_state = m_state_stack.back(); + cqueue & cq = queue_of(top_state); + unsigned cq_size = cq.size(); + if (cq.empty()) { + // no constraints left to be solved + r = save_result(r, subst_of(top_state), residue(), num_metavars); + m_state_stack.pop_back(); + } else { + // try cq_sz times to find a constraint that can be processed + constraint c = cq.front(); + // std::cout << "solving (" << top_state.m_id << ") " << std::get<1>(c) << " === " << std::get<2>(c) << "\n"; + cq.pop_front(); + if (!process(c, subst_of(top_state))) { + // state can't be solved + reset_delayed(); + m_state_stack.pop_back(); + } + if (m_delayed > cq_size) { + // None of the constraints could be processed. + // So, we save the remaining constraints as a residue + residue rs; + for (auto c : cq) + rs = cons(c, rs); + r = save_result(r, subst_of(top_state), rs, num_metavars); + reset_delayed(); + m_state_stack.pop_back(); + } + } + } + return r; } void set_interrupt(bool flag) { m_interrupted = flag; + m_normalizer.set_interrupt(flag); + m_type_infer.set_interrupt(flag); } }; ho_unifier::ho_unifier(environment const & env):m_ptr(new imp(env)) {} ho_unifier::~ho_unifier() {} -void ho_unifier::clear() { m_ptr->clear(); } void ho_unifier::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); } -bool ho_unifier::operator()(context const & ctx, expr const & l, expr const & r, metavar_env & menv, unification_problems & up) { - return m_ptr->unify(ctx, l, r, menv, up); +list ho_unifier::operator()(context const & ctx, expr const & l, expr const & r, metavar_env const & menv) { + return m_ptr->unify(ctx, l, r, menv); } } diff --git a/src/library/ho_unifier.h b/src/library/ho_unifier.h index fe63011172..ef2986cbf4 100644 --- a/src/library/ho_unifier.h +++ b/src/library/ho_unifier.h @@ -6,6 +6,8 @@ Author: Leonardo de Moura */ #pragma once #include +#include +#include "util/list.h" #include "kernel/metavar.h" namespace lean { @@ -17,24 +19,21 @@ public: ho_unifier(environment const & env); ~ho_unifier(); + typedef list> residue; + typedef std::pair result; + /** - \brief Try to unify \c l and \c r in the context \c ctx using the substitution \c menv. + \brief Try to unify \c l and \c r in the context \c ctx using the input substitution \c menv. By unification, we mean we have to find an assignment for the unassigned metavariables in \c l and \c r s.t. \c l and \c r become definitionally equal. - The unifier may produce a residue: a set of unification problems that could not be solved, - and were postponed. This set of problems is stored in \c up. The caller should try to instantiate - the metavariables in the residue using other constraints, and then try to continue the unification. - Return true if the unification succeeded (modulo residue), and false if the terms can't be unified. - - @param[in] ctx The context for \c l and \c r - @param[in] l Expression to be unified with \c r - @param[in] r Expression to be unified with \c l - @param[in,out] menv Metavariable substitution. \c menv may already contain some instantiated variables when this method is invoked. - @param[out] up Delayed unification problems (aka residue), that could not be solved by the unifier. + The unifier may produce a residue: a set of unification problems + that could not be solved, and were postponed. The unifier postpones unification problems of the form + (?M1 ...) == (?M2 ...) where \c M1 and \c M2 are unassigned metavariables. + The result is a list of pairs: substitution (in the form of \c metavar_env) and residue. + Each pair is a possible solution. The resultant \c metavar_env may contain new metavariables. + The empty list represents failure. */ - bool operator()(context const & ctx, expr const & l, expr const & r, metavar_env & menv, unification_problems & up); - - void clear(); + list operator()(context const & ctx, expr const & l, expr const & r, metavar_env const & menv); void set_interrupt(bool flag); void interrupt() { set_interrupt(true); } diff --git a/src/library/light_checker.cpp b/src/library/light_checker.cpp index 9ff028e754..ec13b074a5 100644 --- a/src/library/light_checker.cpp +++ b/src/library/light_checker.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "util/flet.h" #include "util/scoped_map.h" #include "kernel/environment.h" #include "kernel/normalizer.h" @@ -11,6 +12,7 @@ Author: Leonardo de Moura #include "kernel/kernel_exception.h" #include "kernel/instantiate.h" #include "kernel/free_vars.h" +#include "kernel/metavar.h" #include "library/reduce.h" #include "library/light_checker.h" @@ -18,10 +20,13 @@ namespace lean { class light_checker::imp { typedef scoped_map cache; - environment m_env; - cache m_cache; - normalizer m_normalizer; - volatile bool m_interrupted; + environment m_env; + metavar_env * m_menv; + unsigned m_menv_timestamp; + unification_problems * m_up; + normalizer m_normalizer; + cache m_cache; + volatile bool m_interrupted; level infer_universe(expr const & t, context const & ctx) { expr u = m_normalizer(infer_type(t, ctx), ctx); @@ -53,21 +58,29 @@ class light_checker::imp { return instantiate(t, num_args(e)-1, &arg(e, 1)); } -public: - imp(environment const & env): - m_env(env), - m_normalizer(env) { - m_interrupted = false; + 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) { + m_menv_timestamp = m_menv->get_timestamp(); + m_cache.clear(); + } + } else { + m_menv = menv; + m_cache.clear(); + m_menv_timestamp = m_menv ? m_menv->get_timestamp() : 0; + } } expr infer_type(expr const & e, context const & ctx) { // cheap cases, we do not cache results 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: { object const & obj = m_env.get_object(const_name(e)); if (obj.has_type()) @@ -152,6 +165,22 @@ public: return r; } +public: + imp(environment const & env): + m_env(env), + m_normalizer(env) { + m_interrupted = false; + m_menv = nullptr; + m_menv_timestamp = 0; + m_up = nullptr; + } + + expr operator()(expr const & e, context const & ctx, metavar_env * menv, unification_problems * up) { + set_menv(menv); + flet set(m_up, up); + return infer_type(e, ctx); + } + void set_interrupt(bool flag) { m_interrupted = flag; m_normalizer.set_interrupt(flag); @@ -160,11 +189,15 @@ public: void clear() { m_cache.clear(); m_normalizer.clear(); + m_menv = nullptr; + m_menv_timestamp = 0; } }; light_checker::light_checker(environment const & env):m_ptr(new imp(env)) {} light_checker::~light_checker() {} -expr light_checker::operator()(expr const & e, context const & ctx) { return m_ptr->infer_type(e, ctx); } +expr light_checker::operator()(expr const & e, context const & ctx, metavar_env * menv, unification_problems * up) { + return m_ptr->operator()(e, ctx, menv, up); +} void light_checker::clear() { m_ptr->clear(); } void light_checker::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); } } diff --git a/src/library/light_checker.h b/src/library/light_checker.h index 6e7c26d767..b398d0f530 100644 --- a/src/library/light_checker.h +++ b/src/library/light_checker.h @@ -11,6 +11,8 @@ Author: Leonardo de Moura namespace lean { class environment; +class metavar_env; +class unification_problems; /** \brief Functional object for "quickly" inferring the type of expressions. It does not check whether the input expression is type correct or not. @@ -28,7 +30,7 @@ public: light_checker(environment const & env); ~light_checker(); - expr operator()(expr const & e, context const & ctx = context()); + expr operator()(expr const & e, context const & ctx = context(), metavar_env * menv = nullptr, unification_problems * up = nullptr); void clear(); diff --git a/src/library/reduce.cpp b/src/library/reduce.cpp index cf2e021e07..343e0d5a75 100644 --- a/src/library/reduce.cpp +++ b/src/library/reduce.cpp @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include "kernel/instantiate.h" #include "kernel/environment.h" #include "kernel/free_vars.h" +#include "kernel/replace.h" #include "library/update_expr.h" namespace lean { @@ -43,6 +44,22 @@ expr head_beta_reduce(expr const & t) { } } +expr beta_reduce(expr t) { + auto f = [=](expr const & m, unsigned offset) -> expr { + if (is_head_beta(m)) + return head_beta_reduce(m); + else + return m; + }; + while (true) { + expr new_t = replace_fn(f)(t); + if (new_t == t) + return new_t; + else + t = new_t; + } +} + expr head_reduce(expr const & t, environment const & e, context const & c, name_set const * defs) { if (is_head_beta(t)) { return head_beta_reduce(t); diff --git a/src/library/reduce.h b/src/library/reduce.h index 4ed2c0cbcc..07b099781e 100644 --- a/src/library/reduce.h +++ b/src/library/reduce.h @@ -12,5 +12,6 @@ Author: Leonardo de Moura namespace lean { bool is_head_beta(expr const & t); expr head_beta_reduce(expr const & t); +expr beta_reduce(expr t); expr head_reduce(expr const & t, environment const & e, context const & c = context(), name_set const * defs = nullptr); } diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp index bf50588489..bf1dba7dc3 100644 --- a/src/tests/kernel/metavar.cpp +++ b/src/tests/kernel/metavar.cpp @@ -497,6 +497,18 @@ static void tst23() { std::cout << up << "\n"; } +static void tst24() { + metavar_env menv; + expr m1 = menv.mk_metavar(); + expr m2 = menv.mk_metavar(); + expr f = Const("f"); + expr a = Const("a"); + menv.assign(m1, f(m2)); + menv.assign(m2, a); + lean_assert(instantiate_metavars(f(m1), menv) == f(f(a))); + std::cout << instantiate_metavars(f(m1), menv) << "\n"; +} + int main() { tst1(); tst2(); @@ -521,5 +533,6 @@ int main() { tst21(); tst22(); tst23(); + tst24(); return has_violations() ? 1 : 0; } diff --git a/src/tests/library/CMakeLists.txt b/src/tests/library/CMakeLists.txt index 1302291b32..c6b40f2e76 100644 --- a/src/tests/library/CMakeLists.txt +++ b/src/tests/library/CMakeLists.txt @@ -1,3 +1,6 @@ add_executable(light_checker light_checker.cpp) target_link_libraries(light_checker ${EXTRA_LIBS}) add_test(light_checker ${CMAKE_CURRENT_BINARY_DIR}/light_checker) +add_executable(ho_unifier ho_unifier.cpp) +target_link_libraries(ho_unifier ${EXTRA_LIBS}) +add_test(ho_unifier ${CMAKE_CURRENT_BINARY_DIR}/ho_unifier) diff --git a/src/tests/library/ho_unifier.cpp b/src/tests/library/ho_unifier.cpp new file mode 100644 index 0000000000..5a1d360056 --- /dev/null +++ b/src/tests/library/ho_unifier.cpp @@ -0,0 +1,40 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "util/test.h" +#include "kernel/environment.h" +#include "library/ho_unifier.h" +#include "library/printer.h" +#include "library/reduce.h" +using namespace lean; + +void tst1() { + environment env; + metavar_env menv; + ho_unifier unify(env); + expr N = Const("N"); + env.add_var("N", Type()); + env.add_var("f", N >> (N >> N)); + env.add_var("a", N); + env.add_var("b", N); + expr f = Const("f"); + expr x = Const("x"); + expr a = Const("a"); + expr b = Const("b"); + expr m1 = menv.mk_metavar(); + expr m2 = menv.mk_metavar(); + expr l = m1(b); + expr r = f(b, f(a, b)); + for (auto sol : unify(context(), l, r, menv)) { + std::cout << m1 << " -> " << beta_reduce(sol.first.get_subst(m1)) << "\n"; + std::cout << "--------------\n"; + } +} + +int main() { + tst1(); + return has_violations() ? 1 : 0; +}