From a1710aeeb9d0ba0e73f6a83b7b16a60eacdcce2f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 15 Oct 2013 17:32:02 -0700 Subject: [PATCH] feat(elaborator): add trace objects for elaborator Signed-off-by: Leonardo de Moura --- src/kernel/metavar.cpp | 15 + src/kernel/metavar.h | 21 + src/kernel/trace.cpp | 25 ++ src/kernel/trace.h | 5 +- src/kernel/type_checker_trace.cpp | 22 +- src/kernel/type_checker_trace.h | 8 +- src/kernel/unification_constraint.h | 4 + src/library/elaborator/CMakeLists.txt | 2 +- src/library/elaborator/elaborator.cpp | 388 +++++++++++++++++- src/library/elaborator/elaborator.h | 7 +- src/library/elaborator/elaborator_exception.h | 2 + src/library/elaborator/elaborator_plugin.h | 5 +- src/library/elaborator/elaborator_trace.cpp | 158 +++++++ src/library/elaborator/elaborator_trace.h | 194 +++++++++ src/util/name.h | 5 + src/util/name_generator.h | 5 + src/util/splay_map.h | 2 +- src/util/splay_tree.h | 8 +- 18 files changed, 825 insertions(+), 51 deletions(-) create mode 100644 src/library/elaborator/elaborator_trace.cpp create mode 100644 src/library/elaborator/elaborator_trace.h diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp index ea631a340..02f6178ea 100644 --- a/src/kernel/metavar.cpp +++ b/src/kernel/metavar.cpp @@ -166,6 +166,21 @@ void metavar_env::assign(expr const & m, expr const & t, trace const & tr) { assign(metavar_name(m), t, tr); } +struct found_unassigned{}; +name metavar_env::find_unassigned_metavar() const { + name r; + try { + m_metavar_types.for_each([&](name const & m, expr const &) { + if (!m_substitution.is_assigned(m)) { + r = m; + throw found_unassigned(); + } + }); + } catch (found_unassigned &) { + } + return r; +} + expr instantiate_metavars(expr const & e, substitution const & s) { if (!has_metavar(e)) { return e; diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h index 546ce01a7..27f33560b 100644 --- a/src/kernel/metavar.h +++ b/src/kernel/metavar.h @@ -24,6 +24,11 @@ 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); + } + /** \brief Return the number of assigned metavariables in this substitution. */ @@ -101,6 +106,15 @@ 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); + } + /** \brief The timestamp is increased whenever this environment is updated. @@ -178,6 +192,13 @@ public: \pre is_metavar(m) */ expr get_subst(expr const & m) const { return m_substitution.get_subst(m); } + + /** + \brief Return a unassigned metavariable (if one exists). Only metavariables + that have types are considered. Return the anonymous name if all metavariables (with types) + are assigned. + */ + name find_unassigned_metavar() const; }; /** diff --git a/src/kernel/trace.cpp b/src/kernel/trace.cpp index 381afd512..6f22cee76 100644 --- a/src/kernel/trace.cpp +++ b/src/kernel/trace.cpp @@ -9,6 +9,31 @@ Author: Leonardo de Moura #include "kernel/trace.h" namespace lean { +void trace_cell::add_pos_info(format & r, expr const & e, pos_info_provider const * p) { + if (!p || !e) + return; + format f = p->pp(e); + if (!f) + return; + r += f; + r += space(); +} + +format trace_cell::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children) const { + format r; + add_pos_info(r, get_main_expr(), p); + r += pp_header(fmt, opts); + if (display_children) { + buffer children; + get_children(children); + unsigned indent = get_pp_indent(opts); + for (trace_cell * child : children) { + r += nest(indent, compose(line(), child->pp(fmt, opts, p, display_children))); + } + } + return r; +} + bool trace::has_children() const { buffer r; get_children(r); diff --git a/src/kernel/trace.h b/src/kernel/trace.h index 1d706c780..f14a627e9 100644 --- a/src/kernel/trace.h +++ b/src/kernel/trace.h @@ -25,10 +25,13 @@ class trace; class trace_cell { MK_LEAN_RC(); void dealloc() { delete this; } +protected: + static void add_pos_info(format & r, expr const & e, pos_info_provider const * p); public: trace_cell():m_rc(0) {} virtual ~trace_cell() {} - virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children) const = 0; + virtual format pp_header(formatter const & fmt, options const & opts) const = 0; + virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children) const; virtual void get_children(buffer & r) const = 0; virtual expr const & get_main_expr() const { return expr::null(); } bool is_shared() const { return get_rc() > 1; } diff --git a/src/kernel/type_checker_trace.cpp b/src/kernel/type_checker_trace.cpp index c4e88a88c..b23acf9da 100644 --- a/src/kernel/type_checker_trace.cpp +++ b/src/kernel/type_checker_trace.cpp @@ -8,24 +8,13 @@ Author: Leonardo de Moura namespace lean { -void add_pos_info(format & r, expr const & e, pos_info_provider const * p) { - if (!p) - return; - format f = p->pp(e); - if (!f) - return; - r += f; - r += space(); -} - function_expected_trace_cell::~function_expected_trace_cell() { } -format function_expected_trace_cell::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool) const { +format function_expected_trace_cell::pp_header(formatter const & fmt, options const & opts) const { unsigned indent = get_pp_indent(opts); format expr_fmt = fmt(m_ctx, m_app, false, opts); format r; - add_pos_info(r, get_main_expr(), p); r += format("Function expected at"); r += nest(indent, compose(line(), expr_fmt)); return r; @@ -41,10 +30,9 @@ expr const & function_expected_trace_cell::get_main_expr() const { app_type_match_trace_cell::~app_type_match_trace_cell() { } -format app_type_match_trace_cell::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool) const { +format app_type_match_trace_cell::pp_header(formatter const & fmt, options const & opts) const { unsigned indent = get_pp_indent(opts); format r; - add_pos_info(r, get_main_expr(), p); r += format("Type of argument "); r += format(m_i); r += format(" must be convertible to the expected type in the application of"); @@ -70,11 +58,10 @@ expr const & app_type_match_trace_cell::get_main_expr() const { type_expected_trace_cell::~type_expected_trace_cell() { } -format type_expected_trace_cell::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool) const { +format type_expected_trace_cell::pp_header(formatter const & fmt, options const & opts) const { unsigned indent = get_pp_indent(opts); format expr_fmt = fmt(m_ctx, m_type, false, opts); format r; - add_pos_info(r, get_main_expr(), p); r += format("Type expected at"); r += nest(indent, compose(line(), expr_fmt)); return r; @@ -90,9 +77,8 @@ expr const & type_expected_trace_cell::get_main_expr() const { def_type_match_trace_cell::~def_type_match_trace_cell() { } -format def_type_match_trace_cell::pp(formatter const &, options const &, pos_info_provider const * p, bool) const { +format def_type_match_trace_cell::pp_header(formatter const &, options const &) const { format r; - add_pos_info(r, get_main_expr(), p); r += format("Type of definition '"); r += format(get_name()); r += format("' must be convertible to expected type."); diff --git a/src/kernel/type_checker_trace.h b/src/kernel/type_checker_trace.h index e492da23b..0dcdcc864 100644 --- a/src/kernel/type_checker_trace.h +++ b/src/kernel/type_checker_trace.h @@ -27,7 +27,7 @@ class function_expected_trace_cell : public trace_cell { public: function_expected_trace_cell(context const & c, expr const & app):m_ctx(c), m_app(app) {} virtual ~function_expected_trace_cell(); - virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children) const; + virtual format pp_header(formatter const & fmt, options const & opts) const; virtual void get_children(buffer &) const; virtual expr const & get_main_expr() const; context const & get_context() const { return m_ctx; } @@ -52,7 +52,7 @@ class app_type_match_trace_cell : public trace_cell { public: app_type_match_trace_cell(context const & c, expr const & a, unsigned i):m_ctx(c), m_app(a), m_i(i) {} virtual ~app_type_match_trace_cell(); - virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children) const; + virtual format pp_header(formatter const & fmt, options const & opts) const; virtual void get_children(buffer &) const; virtual expr const & get_main_expr() const; context const & get_context() const { return m_ctx; } @@ -75,7 +75,7 @@ class type_expected_trace_cell : public trace_cell { public: type_expected_trace_cell(context const & c, expr const & t):m_ctx(c), m_type(t) {} virtual ~type_expected_trace_cell(); - virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children) const; + virtual format pp_header(formatter const & fmt, options const & opts) const; virtual void get_children(buffer &) const; virtual expr const & get_main_expr() const; context const & get_context() const { return m_ctx; } @@ -112,7 +112,7 @@ class def_type_match_trace_cell : public trace_cell { public: def_type_match_trace_cell(context const & c, name const & n, expr const & v):m_ctx(c), m_name(n), m_value(v) {} virtual ~def_type_match_trace_cell(); - virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children) const; + virtual format pp_header(formatter const & fmt, options const & opts) const; virtual void get_children(buffer &) const; virtual expr const & get_main_expr() const; context const & get_context() const { return m_ctx; } diff --git a/src/kernel/unification_constraint.h b/src/kernel/unification_constraint.h index 53dfe1fc6..acdad3302 100644 --- a/src/kernel/unification_constraint.h +++ b/src/kernel/unification_constraint.h @@ -47,6 +47,7 @@ public: trace const & get_trace() const { return m_trace; } context const & get_context() const { return m_ctx; } virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_trace) const = 0; + void set_trace(trace const & t) { lean_assert(!m_trace); m_trace = t; } }; class unification_constraint { @@ -74,6 +75,9 @@ public: return m_ptr->pp(fmt, opts, p, include_trace); } + trace const & get_trace() const { lean_assert(m_ptr); return m_ptr->get_trace(); } + void set_trace(trace const & t) { lean_assert(!get_trace()); lean_assert(m_ptr); m_ptr->set_trace(t); } + friend unification_constraint mk_eq_constraint(context const & c, expr const & lhs, expr const & rhs, trace const & t); friend unification_constraint mk_convertible_constraint(context const & c, expr const & from, expr const & to, trace const & t); friend unification_constraint mk_max_constraint(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, trace const & t); diff --git a/src/library/elaborator/CMakeLists.txt b/src/library/elaborator/CMakeLists.txt index 28bc51375..cf1d33dd8 100644 --- a/src/library/elaborator/CMakeLists.txt +++ b/src/library/elaborator/CMakeLists.txt @@ -1,2 +1,2 @@ -add_library(elaborator elaborator.cpp) +add_library(elaborator elaborator.cpp elaborator_trace.cpp) target_link_libraries(elaborator ${LEAN_LIBS}) diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index 5e9e26fd9..62f596487 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -4,55 +4,407 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include +#include #include "util/pdeque.h" #include "kernel/formatter.h" +#include "library/light_checker.h" #include "library/elaborator/elaborator.h" +#include "library/elaborator/elaborator_trace.h" namespace lean { +static name g_x_name("x"); + class elaborator::imp { typedef pdeque cnstr_queue; struct state { - unsigned m_id; metavar_env m_menv; cnstr_queue m_queue; + + state(metavar_env const & menv, unsigned num_cnstrs, unification_constraint const * cnstrs): + m_menv(menv) { + for (unsigned i = 0; i < num_cnstrs; i++) + m_queue.push_back(cnstrs[i]); + } + + state(metavar_env const & menv, cnstr_queue const & q): + m_menv(menv), + m_queue(q) { + } }; - environment const & m_env; - std::shared_ptr m_synthesizer; - std::shared_ptr m_plugin; - bool m_interrupted; -public: - imp(environment const & env, metavar_env const &, unsigned num_cnstrs, unification_constraint const * cnstrs, - std::shared_ptr const & s, std::shared_ptr const & p): - m_env(env), - m_synthesizer(s), - m_plugin(p) { - m_interrupted = false; + /** + \brief Base class for case splits performed by the elaborator. + */ + struct case_split { + trace m_curr_assumption; // trace object used to justify current split + state m_prev_state; + std::vector m_failed_traces; // traces/justifications for failed branches - formatter fmt = mk_simple_formatter(); - for (unsigned i = 0; i < num_cnstrs; i++) { - std::cout << cnstrs[i].pp(fmt, options(), nullptr, true) << "\n"; + case_split(state const & prev_state):m_prev_state(prev_state) {} + virtual ~case_split() {} + + virtual bool next(imp & owner) = 0; + }; + + /** + \brief Case-split object for choice constraints. + */ + struct choice_case_split : public case_split { + unsigned m_idx; + unification_constraint m_choice; + + choice_case_split(unification_constraint const & c, state const & prev_state): + case_split(prev_state), + m_idx(0), + m_choice(c) { + } + + virtual ~choice_case_split() {} + + virtual bool next(imp & owner) { + return owner.next_choice_case(*this); + } + }; + + /** + \brief Case split object for higher-order matching + */ + struct ho_match_case_split : public case_split { + unification_constraint m_constraint; + unsigned m_idx; // current alternative + std::vector m_states; // set of alternatives + + ho_match_case_split(unification_constraint const & cnstr, unsigned num_states, state const * states, state const & prev_state): + case_split(prev_state), + m_constraint(cnstr), + m_idx(0), + m_states(states, states + num_states) { + } + + virtual ~ho_match_case_split() {} + + virtual bool next(imp & owner) { + return owner.next_ho_case(*this); + } + }; + + struct synthesizer_case_split : public case_split { + expr m_metavar; + std::unique_ptr m_alternatives; + + synthesizer_case_split(expr const & m, std::unique_ptr & r, state const & prev_state): + case_split(prev_state), + m_metavar(m), + m_alternatives(std::move(r)) { + } + + virtual ~synthesizer_case_split() {} + }; + + struct plugin_case_split : public case_split { + unification_constraint m_constraint; + std::unique_ptr m_alternatives; + + plugin_case_split(unification_constraint const & cnstr, std::unique_ptr & r, state const & prev_state): + case_split(prev_state), + m_constraint(cnstr), + m_alternatives(std::move(r)) { + } + + virtual ~plugin_case_split() {} + + virtual bool next(imp & owner) { + return owner.next_plugin_case(*this); + } + }; + + environment const & m_env; + light_checker m_type_infer; + 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; + 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; + } + + trace mk_assumption() { + unsigned id = m_next_id; + m_next_id++; + 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; + } + + 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); + } + + 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; + } + + 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 a unassigned metavariable in the current state. + Return the anonymous name if the state does not contain unassigned metavariables. + */ + name find_unassigned_metavar() const { + return m_state.m_menv.find_unassigned_metavar(); + } + + /** \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)); + } + + /** \brief Return true iff \c a is a metavariable and has a meta context. */ + 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) { + return is_meta_app(a) && has_local_context(arg(a, 0)); + } + + expr mk_lambda(name const & n, expr const & d, expr const & b) { + return ::lean::mk_lambda(n, d, b); + } + + /** + \brief Create the term (fun (x_0 : types[0]) ... (x_{n-1} : types[n-1]) body) + */ + expr mk_lambda(buffer const & types, expr const & body) { + expr r = body; + unsigned i = types.size(); + while (i > 0) { + --i; + r = mk_lambda(name(g_x_name, i), types[i], r); + } + return r; + } + + bool next_choice_case(choice_case_split & s) { + unification_constraint & choice = s.m_choice; + unsigned idx = s.m_idx; + if (idx < choice_size(choice)) { + 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)); + s.m_idx++; + return true; + } else { + m_conflict = trace(new unification_failure_by_cases_trace(choice, s.m_failed_traces.size(), s.m_failed_traces.data())); + return false; } } + bool next_ho_case(ho_match_case_split &) { +#if 0 + unification_constraint & cnstr = s.m_constraint; + context const & ctx = get_context(cnstr); + expr const & a = eq_lhs(cnstr); + expr const & b = eq_rhs(cnstr); + lean_assert(is_meta_app(a)); + lean_assert(!has_local_context(arg(a, 0))); + lean_assert(!is_meta_app(b)); + expr f_a = arg(a, 0); + lean_assert(is_metavar(f_a)); + unsigned num_a = num_args(a); + + + + // unification_constraints_wrapper ucw; + buffer arg_types; + for (unsigned i = 1; i < num_a; i++) { + arg_types.push_back(m_type_infer(arg(a, i), ctx, &s, &ucw)); + } +#endif + return true; + } + + bool next_plugin_case(plugin_case_split & s) { + try { + s.m_curr_assumption = mk_assumption(); + std::pair> r = s.m_alternatives->next(s.m_curr_assumption); + 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); + } + return true; + } catch (exception & ex) { + m_conflict = trace(new unification_failure_by_cases_trace(s.m_constraint, s.m_failed_traces.size(), s.m_failed_traces.data())); + return false; + } + } + +public: + imp(environment const & env, metavar_env const & menv, unsigned num_cnstrs, unification_constraint const * cnstrs, + options const & opts, std::shared_ptr const & s, std::shared_ptr const & p): + m_env(env), + m_type_infer(env), + m_state(menv, num_cnstrs, cnstrs), + m_synthesizer(s), + m_plugin(p) { + set_options(opts); + m_next_id = 0; + m_delayed = 0; + m_interrupted = false; + + display(std::cout); + } + substitution next() { - // TODO(Leo) - return substitution(); + check_interrupted(m_interrupted); + if (m_conflict) + throw elaborator_exception(m_conflict); + if (!m_case_splits.empty()) { + buffer assumptions; + for (std::unique_ptr const & cs : m_case_splits) + assumptions.push_back(cs->m_curr_assumption); + m_conflict = trace(new next_solution_trace(assumptions.size(), assumptions.data())); + resolve_conflict(); + } + reset_delayed(); + while (true) { + check_interrupted(m_interrupted); + cnstr_queue & q = m_state.m_queue; + if (q.empty()) { + name m = find_unassigned_metavar(); + if (m) { + // TODO(Leo) + // erase the following line, and implement interface with synthesizer + return m_state.m_menv.get_substitutions(); + } else { + return m_state.m_menv.get_substitutions(); + } + } else { + unification_constraint c = q.front(); + q.pop_front(); + if (!process(c)) { + resolve_conflict(); + } + } + } } void interrupt() { m_interrupted = true; + m_type_infer.set_interrupt(true); } + + 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"; + } + } + }; elaborator::elaborator(environment const & env, metavar_env const & menv, unsigned num_cnstrs, unification_constraint const * cnstrs, + options const & opts, std::shared_ptr const & s, std::shared_ptr const & p): - m_ptr(new imp(env, menv, num_cnstrs, cnstrs, s, p)) { + m_ptr(new imp(env, menv, num_cnstrs, cnstrs, opts, s, p)) { } elaborator::elaborator(environment const & env, diff --git a/src/library/elaborator/elaborator.h b/src/library/elaborator/elaborator.h index c73dc0eee..a79a38990 100644 --- a/src/library/elaborator/elaborator.h +++ b/src/library/elaborator/elaborator.h @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once +#include "util/sexpr/options.h" #include "kernel/expr.h" #include "kernel/environment.h" #include "kernel/metavar.h" @@ -41,21 +42,23 @@ public: metavar_env const & menv, unsigned num_cnstrs, unification_constraint const * cnstrs, + options const & opts = options(), std::shared_ptr const & s = std::shared_ptr(), std::shared_ptr const & p = std::shared_ptr()); elaborator(environment const & env, metavar_env const & menv, std::initializer_list const & cnstrs, + options const & opts = options(), std::shared_ptr const & s = std::shared_ptr(), std::shared_ptr const & p = std::shared_ptr()): - elaborator(env, menv, cnstrs.size(), cnstrs.begin(), s, p) {} + elaborator(env, menv, cnstrs.size(), cnstrs.begin(), opts, s, p) {} elaborator(environment const & env, metavar_env const & menv, context const & ctx, expr const & lhs, expr const & rhs); - ~elaborator(); + ~elaborator(); substitution next(); void interrupt(); diff --git a/src/library/elaborator/elaborator_exception.h b/src/library/elaborator/elaborator_exception.h index ee1ae18e5..3c07bbf8e 100644 --- a/src/library/elaborator/elaborator_exception.h +++ b/src/library/elaborator/elaborator_exception.h @@ -21,4 +21,6 @@ public: virtual char const * what() const noexcept { return "elaborator exception"; } trace const & get_trace() const { return m_trace; } }; + + } diff --git a/src/library/elaborator/elaborator_plugin.h b/src/library/elaborator/elaborator_plugin.h index 5bed23efa..e8d7316ff 100644 --- a/src/library/elaborator/elaborator_plugin.h +++ b/src/library/elaborator/elaborator_plugin.h @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #pragma once #include +#include #include "util/list.h" #include "kernel/environment.h" #include "kernel/context.h" @@ -16,7 +17,7 @@ class elaborator_plugin { public: virtual ~elaborator_plugin() {} - /** \brief The plugin produces a "result" object that can generates the sequence of possible solutions. */ + /** \brief The plugin produces a "result" object that can generates the sequence of possible solutions. */ class result { public: virtual ~result() {} @@ -26,7 +27,7 @@ public: Each result is represented by a pair: the new metavariable environment and a new list of constraints to be solved. */ - virtual std::pair> next() = 0; + virtual std::pair> next(trace const & assumption) = 0; /** \brief Interrupt the computation for the next solution. */ virtual void interrupt() = 0; }; diff --git a/src/library/elaborator/elaborator_trace.cpp b/src/library/elaborator/elaborator_trace.cpp new file mode 100644 index 000000000..b327b2779 --- /dev/null +++ b/src/library/elaborator/elaborator_trace.cpp @@ -0,0 +1,158 @@ +/* +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 "library/elaborator/elaborator_trace.h" + +namespace lean { +static void push_back(buffer & r, trace const & t) { + if (t) + r.push_back(t.raw()); +} + +template +static void append(buffer & r, T const & s) { + for (auto t : s) + push_back(r, t); +} + +// ------------------------- +// Assumptions +// ------------------------- +assumption_trace::assumption_trace(unsigned idx):m_idx(idx) { +} +void assumption_trace::get_children(buffer &) const { +} +expr const & assumption_trace::get_main_expr() const { + return expr::null(); +} +format assumption_trace::pp_header(formatter const &, options const &) const { + return format{format("assumption"), space(), format(m_idx)}; +} + +// ------------------------- +// Propagation trace +// ------------------------- +propagation_trace::propagation_trace(unification_constraint const & c): + m_constraint(c) { +} +propagation_trace::~propagation_trace() { +} +void propagation_trace::get_children(buffer & r) const { + push_back(r, m_constraint.get_trace()); +} +expr const & propagation_trace::get_main_expr() const { + return expr::null(); +} +format propagation_trace::pp_header(formatter const & fmt, options const & opts) const { + format r; + unsigned indent = get_pp_indent(opts); + r += format(get_prop_name()); + r += nest(indent, compose(line(), get_constraint().pp(fmt, opts, nullptr, false))); + return r; +} + +// ------------------------- +// Unification failure (by cases) +// ------------------------- +unification_failure_by_cases_trace::unification_failure_by_cases_trace(unification_constraint const & c, unsigned num, trace const * cs): + unification_failure_trace(c), + m_cases(cs, cs + num) { +} +unification_failure_by_cases_trace::~unification_failure_by_cases_trace() { +} +void unification_failure_by_cases_trace::get_children(buffer & r) const { + push_back(r, get_constraint().get_trace()); + append(r, m_cases); +} + +// ------------------------- +// Substitution trace +// ------------------------- +substitution_trace::substitution_trace(unification_constraint const & c, trace const & t): + propagation_trace(c), + m_assignment_trace(t) { +} +substitution_trace::~substitution_trace() { +} +void substitution_trace::get_children(buffer & r) const { + propagation_trace::get_children(r); + push_back(r, m_assignment_trace); +} + +multi_substitution_trace::multi_substitution_trace(unification_constraint const & c, unsigned num, trace const * ts): + propagation_trace(c), + m_assignment_traces(ts, ts + num) { +} +multi_substitution_trace::~multi_substitution_trace() { +} +void multi_substitution_trace::get_children(buffer & r) const { + propagation_trace::get_children(r); + append(r, m_assignment_traces); +} + +// ------------------------- +// Synthesis trace objects +// ------------------------- +synthesis_trace::synthesis_trace(context const & ctx, expr const & mvar, expr const & type, unsigned num, trace const * substs): + m_context(ctx), + m_mvar(mvar), + m_type(type), + m_substitution_traces(substs, substs + num) { +} +synthesis_trace::~synthesis_trace() { +} +format synthesis_trace::pp_header(formatter const & fmt, options const & opts) const { + format r; + r += format(get_label()); + r += space(); + r += fmt(m_context, m_mvar, false, opts); + unsigned indent = get_pp_indent(opts); + r += nest(indent, compose(line(), fmt(m_context, m_type, true, opts))); + return r; +} +void synthesis_trace::get_children(buffer & r) const { + append(r, m_substitution_traces); +} +expr const & synthesis_trace::get_main_expr() const { + return m_mvar; +} + +char const * synthesis_failure_trace::get_label() const { + return "Failed to synthesize expression of type for"; +} +synthesis_failure_trace::synthesis_failure_trace(context const & ctx, expr const & mvar, expr const & type, trace const & tr, unsigned num, trace const * substs): + synthesis_trace(ctx, mvar, type, num, substs), + m_trace(tr) { +} +synthesis_failure_trace::~synthesis_failure_trace() { +} +void synthesis_failure_trace::get_children(buffer & r) const { + synthesis_trace::get_children(r); + push_back(r, m_trace); +} + +char const * synthesized_assignment_trace::get_label() const { + return "Synthesized assignment for"; +} + +// ------------------------- +// Next solution trace +// ------------------------- +next_solution_trace::next_solution_trace(unsigned num, trace const * as): + m_assumptions(as, as + num) { +} +next_solution_trace::~next_solution_trace() { +} +format next_solution_trace::pp_header(formatter const &, options const &) const { + return format("next solution"); +} +void next_solution_trace::get_children(buffer & r) const { + append(r, m_assumptions); +} +expr const & next_solution_trace::get_main_expr() const { + return expr::null(); +} +} diff --git a/src/library/elaborator/elaborator_trace.h b/src/library/elaborator/elaborator_trace.h new file mode 100644 index 000000000..ab8e65a9e --- /dev/null +++ b/src/library/elaborator/elaborator_trace.h @@ -0,0 +1,194 @@ +/* +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 +#include "kernel/trace.h" +#include "kernel/unification_constraint.h" + +namespace lean { +/** + \brief Base class for trace objects used to justify case-splits. +*/ +class assumption_trace : public trace_cell { + unsigned m_idx; +public: + assumption_trace(unsigned idx); + virtual void get_children(buffer &) const; + virtual expr const & get_main_expr() const; + virtual format pp_header(formatter const &, options const &) const; +}; + +/** + \brief Base class for justifying propagations and failures +*/ +class propagation_trace : public trace_cell { + unification_constraint m_constraint; +protected: + /** \brief Auxiliary method used by pp_header to label a propagation step, subclasses must redefine it. */ + virtual char const * get_prop_name() const = 0; +public: + propagation_trace(unification_constraint const & c); + virtual ~propagation_trace(); + virtual void get_children(buffer & r) const; + virtual expr const & get_main_expr() const; + virtual format pp_header(formatter const &, options const &) const; + unification_constraint const & get_constraint() const { return m_constraint; } +}; + +/** + \brief Trace object used to mark that a particular unification constraint could not be solved. +*/ +class unification_failure_trace : public propagation_trace { +protected: + virtual char const * get_prop_name() const { return "Failed to solve"; } +public: + unification_failure_trace(unification_constraint const & c):propagation_trace(c) {} +}; + +/** + \brief Trace object created for justifying that a constraint that + generated a case-split does not have a solution. Each case-split + corresponds to a different way of solving the constraint. +*/ +class unification_failure_by_cases_trace : public unification_failure_trace { + std::vector m_cases; // why each case failed +public: + unification_failure_by_cases_trace(unification_constraint const & c, unsigned num, trace const * cs); + virtual ~unification_failure_by_cases_trace(); + virtual void get_children(buffer & r) const; +}; + +/** + \brief Trace object used to justify a metavar assignment. +*/ +class assignment_trace : public propagation_trace { +protected: + virtual char const * get_prop_name() const { return "Assignment"; } +public: + assignment_trace(unification_constraint const & c):propagation_trace(c) {} +}; + +/** + \brief Trace object used to justify simple structural steps when processing unification + constraints. For example, given the constraint + + ctx |- (f a) == (f b) + + where \c f is a variable, we must have + + ctx |- a == b + + The justification for the latter is a destruct trace based on the former. +*/ +class destruct_trace : public propagation_trace { +protected: + virtual char const * get_prop_name() const { return "Destruct/Decompose"; } +public: + destruct_trace(unification_constraint const & c):propagation_trace(c) {} +}; + +/** + \brief Trace object used to justify a normalization step such as. + + ctx |- (fun x : T, x) a == b + ==> + ctx |- a == b +*/ +class normalize_trace : public propagation_trace { +protected: + virtual char const * get_prop_name() const { return "Normalize"; } +public: + normalize_trace(unification_constraint const & c):propagation_trace(c) {} +}; + +/** + \brief Trace object used to justify a new constraint obtained by substitution. +*/ +class substitution_trace : public propagation_trace { + trace m_assignment_trace; +protected: + virtual char const * get_prop_name() const { return "Substitution"; } +public: + substitution_trace(unification_constraint const & c, trace const & t); + virtual ~substitution_trace(); + virtual void get_children(buffer & r) const; +}; + +/** + \brief Trace object used to justify a new constraint obtained by multiple substitution. +*/ +class multi_substitution_trace : public propagation_trace { + std::vector m_assignment_traces; +protected: + virtual char const * get_prop_name() const { return "Substitution"; } +public: + multi_substitution_trace(unification_constraint const & c, unsigned num, trace const * ts); + virtual ~multi_substitution_trace(); + virtual void get_children(buffer & r) const; +}; + +/** + \brief Base class for synthesis_failure_trace and synthesized_assignment_trace +*/ +class synthesis_trace : public trace_cell { + context m_context; + expr m_mvar; + expr m_type; + std::vector m_substitution_traces; // trace objects justifying the assignments used to instantiate \c m_type and \c m_context. +protected: + virtual char const * get_label() const = 0; +public: + synthesis_trace(context const & ctx, expr const & mvar, expr const & type, unsigned num, trace const * substs); + virtual ~synthesis_trace(); + virtual format pp_header(formatter const &, options const &) const; + virtual void get_children(buffer & r) const; + virtual expr const & get_main_expr() const; +}; + +/** + \brief Trace object for justifying why a synthesis step failed. + A synthesis step is of the form + + ctx |- ?mvar : type + + Before invoking the synthesizer, the elaborator substitutes the + metavariables in \c ctx and \c type with their corresponding assignments. +*/ +class synthesis_failure_trace : public synthesis_trace { + trace m_trace; // trace object produced by the synthesizer +protected: + virtual char const * get_label() const; +public: + synthesis_failure_trace(context const & ctx, expr const & mvar, expr const & type, trace const & tr, unsigned num, trace const * substs); + virtual ~synthesis_failure_trace(); + virtual void get_children(buffer & r) const; +}; + +/** + \brief Trace object used to justify a metavar assignment produced by a synthesizer. +*/ +class synthesized_assignment_trace : public synthesis_trace { +protected: + virtual char const * get_label() const; +public: + synthesized_assignment_trace(context const & ctx, expr const & mvar, expr const & type, unsigned num, trace const * substs): + synthesis_trace(ctx, mvar, type, num, substs) { + } +}; + +/** + \brief Trace object used to justify that we are moving to the next solution. +*/ +class next_solution_trace : public trace_cell { + std::vector m_assumptions; // Set of assumptions used to derive last solution +public: + next_solution_trace(unsigned num, trace const * as); + virtual ~next_solution_trace(); + virtual format pp_header(formatter const &, options const &) const; + virtual void get_children(buffer & r) const; + virtual expr const & get_main_expr() const; +}; +}; diff --git a/src/util/name.h b/src/util/name.h index dc71f5c8e..2acdec752 100644 --- a/src/util/name.h +++ b/src/util/name.h @@ -71,6 +71,7 @@ public: bool is_anonymous() const { return kind() == name_kind::ANONYMOUS; } bool is_string() const { return kind() == name_kind::STRING; } bool is_numeral() const { return kind() == name_kind::NUMERAL; } + operator bool() const { return !is_anonymous(); } unsigned get_numeral() const; /** \brief If the tail of the given hierarchical name is a string, then it returns this string. @@ -93,6 +94,10 @@ public: friend std::ostream & operator<<(std::ostream & out, name const & n); /** \brief Concatenate the two given names. */ friend name operator+(name const & n1, name const & n2); + + friend void swap(name & a, name & b) { + std::swap(a.m_ptr, b.m_ptr); + } }; struct name_hash { unsigned operator()(name const & n) const { return n.hash(); } }; struct name_eq { bool operator()(name const & n1, name const & n2) const { return n1 == n2; } }; diff --git a/src/util/name_generator.h b/src/util/name_generator.h index 86a5de9d8..93788e98a 100644 --- a/src/util/name_generator.h +++ b/src/util/name_generator.h @@ -23,5 +23,10 @@ public: /** \brief Return a unique name modulo \c prefix. */ name next() { name r(m_prefix, m_next_idx); m_next_idx++; return r; } + + friend void swap(name_generator & a, name_generator & b) { + swap(a.m_prefix, b.m_prefix); + std::swap(a.m_next_idx, b.m_next_idx); + } }; } diff --git a/src/util/splay_map.h b/src/util/splay_map.h index 6ca0760f5..de68f7cc0 100644 --- a/src/util/splay_map.h +++ b/src/util/splay_map.h @@ -30,7 +30,7 @@ public: int>::value, "The return type of CMP()(k1, k2) is not int."); } - void swap(splay_map & m) { m_map.swap(m.m_map); } + friend void swap(splay_map & a, splay_map & b) { swap(a.m_map, b.m_map); } bool empty() const { return m_map.empty(); } void clear() { m_map.clear(); } bool is_eqp(splay_map const & m) const { return m_map.is_eqp(m); } diff --git a/src/util/splay_tree.h b/src/util/splay_tree.h index 8e2d96167..2c65f2cb3 100644 --- a/src/util/splay_tree.h +++ b/src/util/splay_tree.h @@ -328,7 +328,7 @@ public: /** \brief O(1) move */ splay_tree & operator=(splay_tree && s) { LEAN_MOVE_REF(splay_tree, s); } - void swap(splay_tree & t) { std::swap(m_ptr, t.m_ptr); } + friend void swap(splay_tree & t1, splay_tree & t2) { std::swap(t1.m_ptr, t2.m_ptr); } /** \brief Return true iff this splay tree is empty. */ bool empty() const { return m_ptr == nullptr; } @@ -394,16 +394,16 @@ public: splay_tree left(*this, m_ptr->m_left); splay_tree right(*this, m_ptr->m_right); if (left.empty()) { - swap(right); + swap(*this, right); } else if (right.empty()) { - swap(left); + swap(*this, left); } else { clear(); left.pull_max(); lean_assert(left.m_ptr->m_right == nullptr); right.m_ptr->inc_ref(); left.m_ptr->m_right = right.m_ptr; - swap(left); + swap(*this, left); } } }