From 183f5a1ccf7f4a279edb819cf935bb999ee36925 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 16 Oct 2013 13:26:31 -0700 Subject: [PATCH] feat(elaborator): solve unification constraints Signed-off-by: Leonardo de Moura --- src/kernel/metavar.cpp | 40 ++ src/kernel/metavar.h | 34 +- src/library/elaborator/elaborator.cpp | 536 +++++++++++++++++++++----- src/util/name.h | 1 + src/util/name_generator.h | 1 + 5 files changed, 509 insertions(+), 103 deletions(-) diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp index 02f6178ea..e41765da2 100644 --- a/src/kernel/metavar.cpp +++ b/src/kernel/metavar.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include +#include #include "util/exception.h" #include "kernel/metavar.h" #include "kernel/replace.h" @@ -14,6 +15,11 @@ Author: Leonardo de Moura #include "kernel/for_each.h" namespace lean { +void swap(substitution & s1, substitution & s2) { + swap(s1.m_subst, s2.m_subst); + std::swap(s1.m_size, s2.m_size); +} + substitution::substitution(): m_size(0) { } @@ -76,6 +82,15 @@ expr substitution::get_subst(expr const & m) const { static name g_unique_name = name::mk_internal_unique_name(); +void swap(metavar_env & a, metavar_env & b) { + swap(a.m_name_generator, b.m_name_generator); + swap(a.m_substitution, b.m_substitution); + swap(a.m_metavar_types, b.m_metavar_types); + swap(a.m_metavar_contexts, b.m_metavar_contexts); + swap(a.m_metavar_traces, b.m_metavar_traces); + std::swap(a.m_timestamp, b.m_timestamp); +} + void metavar_env::inc_timestamp() { if (m_timestamp == std::numeric_limits::max()) { // This should not happen in real examples. We add it just to be safe. @@ -143,6 +158,31 @@ expr metavar_env::get_type(name const & m) { } } +bool metavar_env::has_type(name const & m) const { + auto e = const_cast(this)->m_metavar_types.splay_find(m); + return e; +} + +bool metavar_env::has_type(expr const & m) const { + lean_assert(is_metavar(m)); + return has_type(metavar_name(m)); +} + + +trace metavar_env::get_trace(expr const & m) const { + lean_assert(is_metavar(m)); + return get_trace(metavar_name(m)); +} + +trace metavar_env::get_trace(name const & m) const { + auto e = const_cast(this)->m_metavar_traces.splay_find(m); + if (e) { + return e->second; + } else { + return trace(); + } +} + bool metavar_env::is_assigned(name const & m) const { return m_substitution.is_assigned(m); } diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h index 27f33560b..6ed469b23 100644 --- a/src/kernel/metavar.h +++ b/src/kernel/metavar.h @@ -24,10 +24,7 @@ class substitution { public: substitution(); - friend void swap(substitution & s1, substitution & s2) { - swap(s1.m_subst, s2.m_subst); - std::swap(s1.m_size, s2.m_size); - } + friend void swap(substitution & s1, substitution & s2); /** \brief Return the number of assigned metavariables in this substitution. @@ -81,6 +78,8 @@ public: void for_each(F f) const { m_subst.for_each(f); } }; +void swap(substitution & s1, substitution & s2); + /** \brief Metavar environment. It is an auxiliary datastructure used for: @@ -106,14 +105,7 @@ public: metavar_env(name const & prefix); metavar_env(); - friend void swap(metavar_env & a, metavar_env & b) { - swap(a.m_name_generator, b.m_name_generator); - swap(a.m_substitution, b.m_substitution); - swap(a.m_metavar_types, b.m_metavar_types); - swap(a.m_metavar_contexts, b.m_metavar_contexts); - swap(a.m_metavar_traces, b.m_metavar_traces); - std::swap(a.m_timestamp, b.m_timestamp); - } + friend void swap(metavar_env & a, metavar_env & b); /** \brief The timestamp is increased whenever this environment is @@ -146,6 +138,22 @@ public: expr get_type(expr const & m); expr get_type(name const & m); + /** + \brief Return true iff \c m has a type associated with it. + \pre is_metavar(m) + */ + bool has_type(expr const & m) const; + bool has_type(name const & m) const; + + /** + \brief Return the trace/justification for an assigned metavariable. + \pre is_metavar(m) + \pre is_assigned(m) + */ + trace get_trace(expr const & m) const; + trace get_trace(name const & m) const; + + /** \brief Return true iff the metavariable named \c m is assigned in this substitution. */ @@ -201,6 +209,8 @@ public: name find_unassigned_metavar() const; }; +void swap(metavar_env & a, metavar_env & b); + /** \brief Apply the changes in \c lctx to \c a. */ diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index 62f596487..d1baf032b 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -6,9 +6,16 @@ Author: Leonardo de Moura */ #include #include +#include #include "util/pdeque.h" #include "kernel/formatter.h" +#include "kernel/free_vars.h" +#include "kernel/normalizer.h" +#include "kernel/instantiate.h" +#include "kernel/builtin.h" #include "library/light_checker.h" +#include "library/update_expr.h" +#include "library/reduce.h" #include "library/elaborator/elaborator.h" #include "library/elaborator/elaborator_trace.h" @@ -122,29 +129,28 @@ class elaborator::imp { environment const & m_env; light_checker m_type_infer; + normalizer m_normalizer; state m_state; std::vector> m_case_splits; std::shared_ptr m_synthesizer; std::shared_ptr m_plugin; unsigned m_next_id; - unsigned m_delayed; + int m_quota; trace m_conflict; bool m_interrupted; // options bool m_use_traces; - bool m_use_beta; bool m_use_normalizer; void set_options(options const &) { m_use_traces = true; - m_use_beta = true; m_use_normalizer = true; } - void reset_delayed() { - m_delayed = 0; + void reset_quota() { + m_quota = m_state.m_queue.size(); } trace mk_assumption() { @@ -153,85 +159,44 @@ class elaborator::imp { return trace(new assumption_trace(id)); } - bool process(unification_constraint const & c) { - switch (c.kind()) { - case unification_constraint_kind::Eq: return process_eq(c); - case unification_constraint_kind::Convertible: return process_convertible(c); - case unification_constraint_kind::Max: return process_max(c); - case unification_constraint_kind::Choice: return process_choice(c); - } - lean_unreachable(); - return true; + /** \brief Add given constraint to the front of the current constraint queue */ + void push_front(unification_constraint const & c) { + reset_quota(); + m_state.m_queue.push_front(c); } - bool process_eq(unification_constraint const & c) { - return process_eq_convertible(get_context(c), eq_lhs(c), eq_rhs(c), c); + /** \brief Return true iff \c m is an assigned metavariable in the current state */ + bool is_assigned(expr const & m) const { + lean_assert(is_metavar(m)); + return m_state.m_menv.is_assigned(m); } - bool process_convertible(unification_constraint const & c) { - return process_eq_convertible(get_context(c), convertible_from(c), convertible_to(c), c); - } - - bool process_eq_convertible(context const & ctx, expr const & from, expr const & to, unification_constraint const & c) { - bool eq = is_eq(c); - if (from == to) { - reset_delayed(); - return true; - } - - // TODO(Leo) - - if (is_type(from) && is_type(to)) { - if ((!eq && m_env.is_ge(ty_level(to), ty_level(from))) || (eq && from == to)) { - reset_delayed(); - return true; - } else { - m_conflict = trace(new unification_failure_trace(c)); - return false; - } - } - - if (is_pi(from) && is_pi(to)) { - trace new_trace(new destruct_trace(c)); - m_state.m_queue.push_front(mk_eq_constraint(ctx, abst_domain(from), abst_domain(to), new_trace)); - context new_ctx = extend(ctx, abst_name(from), abst_domain(from)); - if (eq) - m_state.m_queue.push_front(mk_eq_constraint(new_ctx, abst_body(from), abst_body(to), new_trace)); - else - m_state.m_queue.push_front(mk_convertible_constraint(new_ctx, abst_body(from), abst_body(to), new_trace)); - reset_delayed(); - return true; - } - - - return true; - } - - - bool process_max(unification_constraint const &) { - // TODO(Leo) - return true; - } - - bool process_choice(unification_constraint const &) { - // TODO(Leo) - return true; + /** \brief Return the substitution for an assigned metavariable */ + expr get_mvar_subst(expr const & m) const { + lean_assert(is_metavar(m)); + lean_assert(is_assigned(m)); + return m_state.m_menv.get_subst(m); } - void resolve_conflict() { - lean_assert(m_conflict); - while (!m_case_splits.empty()) { - std::unique_ptr & d = m_case_splits.back(); - if (depends_on(m_conflict, d->m_curr_assumption)) { - d->m_failed_traces.push_back(m_conflict); - if (d->next(*this)) { - m_conflict = trace(); - return; - } - } - m_case_splits.pop_back(); - } - throw elaborator_exception(m_conflict); + /** \brief Return the trace/justification for an assigned metavariable */ + trace get_mvar_trace(expr const & m) const { + lean_assert(is_metavar(m)); + lean_assert(is_assigned(m)); + return m_state.m_menv.get_trace(m); + } + + /** \brief Return the type of an metavariable */ + expr get_mvar_type(expr const & m) { + lean_assert(is_metavar(m)); + return m_state.m_menv.get_type(m); + } + + /** + \brief Return true iff \c e contains the metavariable \c m. + The substitutions in the current state are taken into account. + */ + bool has_metavar(expr const & e, expr const & m) const { + return ::lean::has_metavar(e, m, m_state.m_menv.get_substitutions()); } /** @@ -243,21 +208,26 @@ class elaborator::imp { } /** \brief Return true if \c a is of the form (?m ...) */ - bool is_meta_app(expr const & a) { + static bool is_meta_app(expr const & a) { return is_app(a) && is_metavar(arg(a, 0)); } + /** \brief Return true iff \c a is a metavariable or if \c a is an application where the function is a metavariable */ + static bool is_meta(expr const & a) { + return is_metavar(a) || is_meta_app(a); + } + /** \brief Return true iff \c a is a metavariable and has a meta context. */ - bool is_metavar_with_context(expr const & a) { + static bool is_metavar_with_context(expr const & a) { return is_metavar(a) && has_local_context(a); } /** \brief Return true if \c a is of the form (?m[...] ...) */ - bool is_meta_app_with_context(expr const & a) { + static bool is_meta_app_with_context(expr const & a) { return is_meta_app(a) && has_local_context(arg(a, 0)); } - expr mk_lambda(name const & n, expr const & d, expr const & b) { + static expr mk_lambda(name const & n, expr const & d, expr const & b) { return ::lean::mk_lambda(n, d, b); } @@ -274,6 +244,384 @@ class elaborator::imp { return r; } + /** + \brief Auxiliary method for pushing a new constraint to the constraint queue. + The new constraint is based on the constraint \c c. The constraint \c c may be a equality or convertability constraint. + The update is justified by \c new_tr. + */ + void push_updated_constraint(unification_constraint const & c, expr const & new_a, expr const & new_b, trace const & new_tr) { + lean_assert(is_eq(c) || is_convertible(c)); + context const & ctx = get_context(c); + if (is_eq(c)) + push_front(mk_eq_constraint(ctx, new_a, new_b, new_tr)); + else + push_front(mk_convertible_constraint(ctx, new_a, new_b, new_tr)); + } + + /** + \brief Auxiliary method for pushing a new constraint to the constraint queue. + The new constraint is based on the constraint \c c. The constraint \c c may be a equality or convertability constraint. + The flag \c is_lhs says if the left-hand-side or right-hand-side are being updated with \c new_a. + The update is justified by \c new_tr. + */ + void push_updated_constraint(unification_constraint const & c, bool is_lhs, expr const & new_a, trace const & new_tr) { + lean_assert(is_eq(c) || is_convertible(c)); + context const & ctx = get_context(c); + if (is_eq(c)) { + if (is_lhs) + push_front(mk_eq_constraint(ctx, new_a, eq_rhs(c), new_tr)); + else + push_front(mk_eq_constraint(ctx, eq_lhs(c), new_a, new_tr)); + } else { + if (is_lhs) + push_front(mk_convertible_constraint(ctx, new_a, convertible_to(c), new_tr)); + else + push_front(mk_convertible_constraint(ctx, convertible_from(c), new_a, new_tr)); + } + } + + /** + \brief Auxiliary method for pushing a new constraint to the constraint queue. + The new constraint is obtained from \c c by one or more normalization steps that produce \c new_a and \c new_b + */ + void push_normalized_constraint(unification_constraint const & c, expr const & new_a, expr const & new_b) { + push_updated_constraint(c, new_a, new_b, trace(new normalize_trace(c))); + } + + /** + \brief Assign \c v to \c m with justification \c tr in the current state. + */ + void assign(expr const & m, expr const & v, trace const & tr) { + lean_assert(is_metavar(m)); + metavar_env & menv = m_state.m_menv; + m_state.m_menv.assign(m, v, tr); + if (menv.has_type(m)) { + + } + } + + bool process(unification_constraint const & c) { + m_quota--; + switch (c.kind()) { + case unification_constraint_kind::Eq: return process_eq(c); + case unification_constraint_kind::Convertible: return process_convertible(c); + case unification_constraint_kind::Max: return process_max(c); + case unification_constraint_kind::Choice: return process_choice(c); + } + lean_unreachable(); + return true; + } + + bool process_eq(unification_constraint const & c) { + return process_eq_convertible(get_context(c), eq_lhs(c), eq_rhs(c), c); + } + + bool process_convertible(unification_constraint const & c) { + return process_eq_convertible(get_context(c), convertible_from(c), convertible_to(c), c); + } + + /** + Process ctx |- a == b and ctx |- 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 { Processed, Failed, Continue }; + status process_metavar(unification_constraint const & c, expr const & a, expr const & b, bool is_lhs, bool allow_assignment) { + if (is_metavar(a)) { + if (is_assigned(a)) { + // Case 1 + trace new_tr(new substitution_trace(c, get_mvar_trace(a))); + push_updated_constraint(c, is_lhs, get_mvar_subst(a), new_tr); + return Processed; + } else if (!has_local_context(a)) { + // Case 2 + if (has_metavar(b, a)) { + m_conflict = trace(new unification_failure_trace(c)); + return Failed; + } else if (allow_assignment) { + assign(a, b, trace(new assignment_trace(c))); + reset_quota(); + return Processed; + } + } else { + local_entry const & me = head(metavar_lctx(a)); + if (me.is_lift() && !has_free_var(b, me.s(), me.s() + me.n())) { + // Case 3 + trace new_tr(new substitution_trace(c, get_mvar_trace(a))); + expr new_a = pop_meta_context(a); + expr new_b = lower_free_vars(b, me.s() + me.n(), me.n()); + if (!is_lhs) + swap(new_a, new_b); + push_updated_constraint(c, new_a, new_b, new_tr); + return Processed; + } + } + } + + if (is_app(a) && is_metavar(arg(a, 0)) && is_assigned(arg(a, 0))) { + // Case 4 + trace new_tr(new substitution_trace(c, get_mvar_trace(arg(a, 0)))); + expr new_a = update_app(a, 0, get_mvar_subst(arg(a, 0))); + push_updated_constraint(c, is_lhs, new_a, new_tr); + return Processed; + } + return Continue; + } + + + /** \brief Unfold let-expression */ + void process_let(expr & a) { + if (is_let(a)) + a = instantiate(let_body(a), let_value(a)); + } + + /** \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&) { + } + } + } + + expr normalize(context const & ctx, expr const & a) { + return m_normalizer(a, ctx, &(m_state.m_menv)); + } + + void process_app(context const & ctx, expr & a) { + if (is_app(a)) { + expr f = arg(a, 0); + if (is_value(f) && m_use_normalizer) { + // if f is a semantic attachment, we keep normalizing children from + // left to right until the semantic attachment is applicable + buffer new_args; + new_args.append(num_args(a), &(arg(a, 0))); + bool modified = false; + expr r; + for (unsigned i = 1; i < new_args.size(); i++) { + expr const & curr = new_args[i]; + expr new_curr = normalize(ctx, curr); + if (curr != new_curr) { + modified = true; + new_args[i] = new_curr; + if (to_value(f).normalize(new_args.size(), new_args.data(), r)) { + a = r; + return; + } + } + } + if (modified) { + a = mk_app(new_args.size(), new_args.data()); + return; + } + } else { + process_let(f); + process_var(ctx, f); + f = head_beta_reduce(f); + a = update_app(a, 0, f); + a = head_beta_reduce(a); + } + } + } + + void process_eq(context const & ctx, expr & a) { + if (is_eq(a) && m_use_normalizer) { + a = normalize(ctx, a); + } + } + + expr normalize_step(context const & ctx, expr const & a) { + expr new_a = a; + process_let(new_a); + process_var(ctx, new_a); + process_app(ctx, new_a); + process_eq(ctx, new_a); + return new_a; + } + + int get_const_weight(expr const & a) { + lean_assert(is_constant(a)); + object const & obj = m_env.find_object(const_name(a)); + if (obj && obj.is_definition() && !obj.is_opaque()) + return obj.get_weight(); + else + return -1; + } + + /** + \brief Return a number >= 0 if \c a is a defined constant or the application of a defined constant. + In this case, the value is the weight of the definition. + */ + int get_unfolding_weight(expr const & a) { + if (is_constant(a)) + return get_const_weight(a); + else if (is_app(a) && is_constant(arg(a, 0))) + return get_const_weight(arg(a, 0)); + else + return -1; + } + + expr unfold(expr const & a) { + lean_assert(is_constant(a) || (is_app(a) && is_constant(arg(a, 0)))); + if (is_constant(a)) { + return m_env.find_object(const_name(a)).get_value(); + } else { + return update_app(a, 0, m_env.find_object(const_name(arg(a, 0))).get_value()); + } + } + + bool normalize_head(expr a, expr b, unification_constraint const & c) { + context const & ctx = get_context(c); + bool modified = false; + while (true) { + check_interrupted(m_interrupted); + expr new_a = normalize_step(ctx, a); + expr new_b = normalize_step(ctx, b); + if (new_a == a && new_b == b) { + int w_a = get_unfolding_weight(a); + int w_b = get_unfolding_weight(b); + if (w_a >= 0 || w_b >= 0) { + if (w_a >= w_b) + new_a = unfold(a); + if (w_b >= w_a) + new_b = unfold(b); + if (new_a == a && new_b == b) + break; + } else { + break; + } + } + modified = true; + a = new_a; + b = new_b; + if (a == b) { + return true; + } + } + if (modified) { + push_normalized_constraint(c, a, b); + return true; + } else { + return false; + } + } + + bool process_eq_convertible(context const & ctx, expr const & a, expr const & b, unification_constraint const & c) { + bool eq = is_eq(c); + if (a == b) { + return true; + } + + status r; + bool allow_assignment = eq; // at this point, we only assign metavariables if the constraint is an equational constraint. + r = process_metavar(c, a, b, true, allow_assignment); + if (r != Continue) { return r == Processed; } + r = process_metavar(c, b, a, false, allow_assignment); + if (r != Continue) { return r == Processed; } + + if (normalize_head(a, b, c)) { return true; } + + r = process_metavar(c, a, b, true, !is_type(b) && !is_meta(b)); + if (r != Continue) { return r == Processed; } + r = process_metavar(c, b, a, false, !is_type(a) && !is_meta(a) && a != Bool); + if (r != Continue) { return r == Processed; } + + if (a.kind() == b.kind()) { + switch (a.kind()) { + case expr_kind::Constant: case expr_kind::Var: case expr_kind::Value: + return a == b; + case expr_kind::Type: + if ((!eq && m_env.is_ge(ty_level(b), ty_level(a))) || (eq && a == b)) { + return true; + } else { + m_conflict = trace(new unification_failure_trace(c)); + return false; + } + case expr_kind::Eq: { + trace new_trace(new destruct_trace(c)); + push_front(mk_eq_constraint(ctx, eq_lhs(a), eq_lhs(b), new_trace)); + push_front(mk_eq_constraint(ctx, eq_rhs(a), eq_rhs(b), new_trace)); + return true; + } + case expr_kind::Pi: { + trace new_trace(new destruct_trace(c)); + push_front(mk_eq_constraint(ctx, abst_domain(a), abst_domain(b), new_trace)); + context new_ctx = extend(ctx, abst_name(a), abst_domain(a)); + if (eq) + push_front(mk_eq_constraint(new_ctx, abst_body(a), abst_body(b), new_trace)); + else + push_front(mk_convertible_constraint(new_ctx, abst_body(a), abst_body(b), new_trace)); + return true; + } + case expr_kind::Lambda: { + trace new_trace(new destruct_trace(c)); + push_front(mk_eq_constraint(ctx, abst_domain(a), abst_domain(b), new_trace)); + context new_ctx = extend(ctx, abst_name(a), abst_domain(a)); + push_front(mk_eq_constraint(new_ctx, abst_body(a), abst_body(b), new_trace)); + return true; + } + case expr_kind::App: + if (!is_meta_app(a) && !is_meta_app(b)) { + if (num_args(a) == num_args(b)) { + trace new_trace(new destruct_trace(c)); + for (unsigned i = 0; i < num_args(a); i++) + push_front(mk_eq_constraint(ctx, arg(a, i), arg(b, i), new_trace)); + return true; + } else { + return false; + } + } + break; + case expr_kind::Let: + lean_unreachable(); + return true; + default: + break; + } + } + + if (!is_meta(a) && !is_meta(b) && a.kind() != b.kind()) + return false; + + std::cout << "Postponed: "; display(std::cout, c); + + return true; + } + + + bool process_max(unification_constraint const &) { + // TODO(Leo) + return true; + } + + bool process_choice(unification_constraint const &) { + // TODO(Leo) + return true; + } + + void resolve_conflict() { + lean_assert(m_conflict); + while (!m_case_splits.empty()) { + std::unique_ptr & d = m_case_splits.back(); + if (depends_on(m_conflict, d->m_curr_assumption)) { + d->m_failed_traces.push_back(m_conflict); + if (d->next(*this)) { + m_conflict = trace(); + reset_quota(); + return; + } + } + m_case_splits.pop_back(); + } + throw elaborator_exception(m_conflict); + } + bool next_choice_case(choice_case_split & s) { unification_constraint & choice = s.m_choice; unsigned idx = s.m_idx; @@ -281,7 +629,7 @@ class elaborator::imp { s.m_idx++; s.m_curr_assumption = mk_assumption(); m_state = s.m_prev_state; - m_state.m_queue.push_front(mk_eq_constraint(get_context(choice), choice_mvar(choice), choice_ith(choice, idx), s.m_curr_assumption)); + push_front(mk_eq_constraint(get_context(choice), choice_mvar(choice), choice_ith(choice, idx), s.m_curr_assumption)); s.m_idx++; return true; } else { @@ -321,7 +669,7 @@ class elaborator::imp { m_state.m_queue = s.m_prev_state.m_queue; m_state.m_menv = r.first; for (auto c : r.second) { - m_state.m_queue.push_front(c); + push_front(c); } return true; } catch (exception & ex) { @@ -335,12 +683,13 @@ public: options const & opts, std::shared_ptr const & s, std::shared_ptr const & p): m_env(env), m_type_infer(env), + m_normalizer(env), m_state(menv, num_cnstrs, cnstrs), m_synthesizer(s), m_plugin(p) { set_options(opts); m_next_id = 0; - m_delayed = 0; + m_quota = 0; m_interrupted = false; display(std::cout); @@ -357,12 +706,13 @@ public: m_conflict = trace(new next_solution_trace(assumptions.size(), assumptions.data())); resolve_conflict(); } - reset_delayed(); + reset_quota(); while (true) { check_interrupted(m_interrupted); cnstr_queue & q = m_state.m_queue; if (q.empty()) { name m = find_unassigned_metavar(); + std::cout << "Queue is empty\n"; display(std::cout); if (m) { // TODO(Leo) // erase the following line, and implement interface with synthesizer @@ -372,6 +722,7 @@ public: } } else { unification_constraint c = q.front(); + std::cout << "Processing "; display(std::cout, c); q.pop_front(); if (!process(c)) { resolve_conflict(); @@ -383,18 +734,21 @@ public: void interrupt() { m_interrupted = true; m_type_infer.set_interrupt(true); + m_normalizer.set_interrupt(true); + } + + void display(std::ostream & out, unification_constraint const & c) const { + formatter fmt = mk_simple_formatter(); + out << c.pp(fmt, options(), nullptr, false) << "\n"; } void display(std::ostream & out) const { m_state.m_menv.get_substitutions().for_each([&](name const & m, expr const & e) { out << m << " <- " << e << "\n"; }); - formatter fmt = mk_simple_formatter(); - for (auto c : m_state.m_queue) { - out << c.pp(fmt, options(), nullptr, false) << "\n"; - } + for (auto c : m_state.m_queue) + display(out, c); } - }; elaborator::elaborator(environment const & env, diff --git a/src/util/name.h b/src/util/name.h index 2acdec752..abae67dc8 100644 --- a/src/util/name.h +++ b/src/util/name.h @@ -7,6 +7,7 @@ Author: Leonardo de Moura #pragma once #include #include +#include namespace lean { constexpr char const * lean_name_separator = "::"; diff --git a/src/util/name_generator.h b/src/util/name_generator.h index 93788e98a..b10813abf 100644 --- a/src/util/name_generator.h +++ b/src/util/name_generator.h @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once +#include #include "util/name.h" namespace lean {