From 1548ffabb1fc3e8b720bb6dbe323332b6468368b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 3 Oct 2013 15:02:07 -0700 Subject: [PATCH] feat(elaborator): add new elaborator interface Signed-off-by: Leonardo de Moura --- src/CMakeLists.txt | 2 + src/frontends/lean/elaborator.cpp | 24 +++---- src/frontends/lean/elaborator.h | 6 +- src/frontends/lean/elaborator_exception.cpp | 8 +-- src/frontends/lean/elaborator_exception.h | 44 ++++++------- src/frontends/lean/parser.cpp | 10 ++- src/kernel/unification_constraint.cpp | 2 +- src/library/elaborator/CMakeLists.txt | 2 + src/library/elaborator/elaborator.cpp | 59 +++++++++++++++++ src/library/elaborator/elaborator.h | 63 +++++++++++++++++++ src/library/elaborator/elaborator_exception.h | 24 +++++++ src/library/elaborator/elaborator_plugin.h | 40 ++++++++++++ src/library/elaborator/synthesizer.h | 37 +++++++++++ src/tests/frontends/lean/implicit_args.cpp | 2 +- 14 files changed, 277 insertions(+), 46 deletions(-) create mode 100644 src/library/elaborator/CMakeLists.txt create mode 100644 src/library/elaborator/elaborator.cpp create mode 100644 src/library/elaborator/elaborator.h create mode 100644 src/library/elaborator/elaborator_exception.h create mode 100644 src/library/elaborator/elaborator_plugin.h create mode 100644 src/library/elaborator/synthesizer.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 840843762..43f61e333 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -135,6 +135,8 @@ add_subdirectory(library/all) set(LEAN_LIBS ${LEAN_LIBS} alllib) add_subdirectory(library/rewriter) set(LEAN_LIBS ${LEAN_LIBS} rewriter) +add_subdirectory(library/elaborator) +set(LEAN_LIBS ${LEAN_LIBS} elaborator) add_subdirectory(frontends/lean) set(LEAN_LIBS ${LEAN_LIBS} lean_frontend) set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread ${LEAN_EXTRA_LINKER_FLAGS}") diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 6a6795bfa..5ce0d7445 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -52,19 +52,19 @@ expr const & get_choice(expr const & e, unsigned i) { return arg(eq_rhs(e), i); } -elaborator::elaborator(frontend const & ) {} -elaborator::~elaborator() {} -expr elaborator::operator()(expr const & e) { return e; } -expr elaborator::operator()(expr const & e, expr const & /* expected_type */) { return e; } -expr const & elaborator::get_original(expr const & e) const { return e; } -void elaborator::set_interrupt(bool ) {} -void elaborator::clear() {} -environment const & elaborator::get_environment() const { +old_elaborator::old_elaborator(frontend const & ) {} +old_elaborator::~old_elaborator() {} +expr old_elaborator::operator()(expr const & e) { return e; } +expr old_elaborator::operator()(expr const & e, expr const & /* expected_type */) { return e; } +expr const & old_elaborator::get_original(expr const & e) const { return e; } +void old_elaborator::set_interrupt(bool ) {} +void old_elaborator::clear() {} +environment const & old_elaborator::get_environment() const { static thread_local environment g_env; return g_env; } -void elaborator::display(std::ostream & ) const {} -format elaborator::pp(formatter &, options const &) const { return format(); } -void elaborator::print(imp * ptr) { lean_assert(ptr); } -bool elaborator::has_constraints() const { return false; } +void old_elaborator::display(std::ostream & ) const {} +format old_elaborator::pp(formatter &, options const &) const { return format(); } +void old_elaborator::print(imp * ptr) { lean_assert(ptr); } +bool old_elaborator::has_constraints() const { return false; } } diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index a8204f05c..7efa9f7c0 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -16,13 +16,13 @@ class frontend; in terms left by the user. This is the main module resposible for computing the value of implicit arguments. */ -class elaborator { +class old_elaborator { class imp; std::shared_ptr m_ptr; static void print(imp * ptr); public: - explicit elaborator(frontend const & fe); - ~elaborator(); + explicit old_elaborator(frontend const & fe); + ~old_elaborator(); expr operator()(expr const & e); expr operator()(expr const & e, expr const & expected_type); diff --git a/src/frontends/lean/elaborator_exception.cpp b/src/frontends/lean/elaborator_exception.cpp index ac21c5158..8919ecc31 100644 --- a/src/frontends/lean/elaborator_exception.cpp +++ b/src/frontends/lean/elaborator_exception.cpp @@ -9,7 +9,7 @@ Author: Leonardo de Moura #include "frontends/lean/elaborator.h" namespace lean { -format pp_elaborator_state(formatter fmt, elaborator const & elb, options const & opts) { +format pp_elaborator_state(formatter fmt, old_elaborator const & elb, options const & opts) { unsigned indent = get_pp_indent(opts); format r; if (elb.has_constraints()) { @@ -33,7 +33,7 @@ format pp(formatter fmt, context const & ctx, std::vector const & exprs, s return r; } -format elaborator_exception::pp(formatter const & fmt, options const & opts) const { +format old_elaborator_exception::pp(formatter const & fmt, options const & opts) const { unsigned indent = get_pp_indent(opts); format expr_fmt = fmt(get_context(), get_expr(), false, opts); format r; @@ -102,13 +102,13 @@ format unification_type_mismatch_exception::pp(formatter const & fmt, options co return r; } -regular const & operator<<(regular const & out, elaborator_exception const & ex) { +regular const & operator<<(regular const & out, old_elaborator_exception const & ex) { options const & opts = out.m_state.get_options(); out.m_state.get_regular_channel().get_stream() << mk_pair(ex.pp(out.m_state.get_formatter(), opts), opts); return out; } -diagnostic const & operator<<(diagnostic const & out, elaborator_exception const & ex) { +diagnostic const & operator<<(diagnostic const & out, old_elaborator_exception const & ex) { options const & opts = out.m_state.get_options(); out.m_state.get_diagnostic_channel().get_stream() << mk_pair(ex.pp(out.m_state.get_formatter(), opts), opts); return out; diff --git a/src/frontends/lean/elaborator_exception.h b/src/frontends/lean/elaborator_exception.h index 547a4e162..9055ebfa5 100644 --- a/src/frontends/lean/elaborator_exception.h +++ b/src/frontends/lean/elaborator_exception.h @@ -17,39 +17,39 @@ namespace lean { \remark We reuse kernel exceptions to sign type errors during elaboration. Perhaps we should wrap them as elaborator exceptions. */ -class elaborator_exception : public exception { +class old_elaborator_exception : public exception { protected: - elaborator m_elb; + old_elaborator m_elb; context m_context; expr m_expr; public: - elaborator_exception(elaborator const & elb, context const & ctx, expr const & e):m_elb(elb), m_context(ctx), m_expr(e) {} - virtual ~elaborator_exception() noexcept {} - elaborator const & get_elaborator() const { return m_elb; } + old_elaborator_exception(old_elaborator const & elb, context const & ctx, expr const & e):m_elb(elb), m_context(ctx), m_expr(e) {} + virtual ~old_elaborator_exception() noexcept {} + old_elaborator const & get_elaborator() const { return m_elb; } expr const & get_expr() const { return m_expr; } context const & get_context() const { return m_context; } virtual format pp(formatter const & fmt, options const & opts) const; }; -class invalid_placeholder_exception : public elaborator_exception { +class invalid_placeholder_exception : public old_elaborator_exception { public: - invalid_placeholder_exception(elaborator const & elb, context const & ctx, expr const & e):elaborator_exception(elb, ctx, e) {} + invalid_placeholder_exception(old_elaborator const & elb, context const & ctx, expr const & e):old_elaborator_exception(elb, ctx, e) {} virtual char const * what() const noexcept { return "invalid placeholder occurrence, placeholder cannot be used as application head"; } }; -class unsolved_placeholder_exception : public elaborator_exception { +class unsolved_placeholder_exception : public old_elaborator_exception { public: - unsolved_placeholder_exception(elaborator const & elb, context const & ctx, expr const & e):elaborator_exception(elb, ctx, e) {} + unsolved_placeholder_exception(old_elaborator const & elb, context const & ctx, expr const & e):old_elaborator_exception(elb, ctx, e) {} virtual char const * what() const noexcept { return "unsolved placeholder"; } }; -class unification_app_mismatch_exception : public elaborator_exception { +class unification_app_mismatch_exception : public old_elaborator_exception { std::vector m_args; std::vector m_types; public: - unification_app_mismatch_exception(elaborator const & elb, context const & ctx, expr const & s, + unification_app_mismatch_exception(old_elaborator const & elb, context const & ctx, expr const & s, std::vector const & args, std::vector const & types): - elaborator_exception(elb, ctx, s), + old_elaborator_exception(elb, ctx, s), m_args(args), m_types(types) {} virtual ~unification_app_mismatch_exception() {} @@ -59,14 +59,14 @@ public: virtual format pp(formatter const & fmt, options const & opts) const; }; -class unification_type_mismatch_exception : public elaborator_exception { +class unification_type_mismatch_exception : public old_elaborator_exception { expr m_processed_expr; expr m_expected_type; expr m_given_type; public: - unification_type_mismatch_exception(elaborator const & elb, context const & ctx, expr const & s, + unification_type_mismatch_exception(old_elaborator const & elb, context const & ctx, expr const & s, expr const & processed, expr const & expected, expr const & given): - elaborator_exception(elb, ctx, s), m_processed_expr(processed), m_expected_type(expected), m_given_type(given) {} + old_elaborator_exception(elb, ctx, s), m_processed_expr(processed), m_expected_type(expected), m_given_type(given) {} virtual ~unification_type_mismatch_exception() {} expr const & get_processed_expr() const { return m_processed_expr; } expr const & get_expected_type() const { return m_expected_type; } @@ -75,16 +75,16 @@ public: virtual format pp(formatter const & fmt, options const & opts) const; }; -class overload_exception : public elaborator_exception { +class overload_exception : public old_elaborator_exception { std::vector m_fs; std::vector m_f_types; std::vector m_args; std::vector m_arg_types; public: - overload_exception(elaborator const & elb, context const & ctx, expr const & s, + overload_exception(old_elaborator const & elb, context const & ctx, expr const & s, unsigned num_fs, expr const * fs, expr const * ftypes, unsigned num_args, expr const * args, expr const * argtypes): - elaborator_exception(elb, ctx, s), + old_elaborator_exception(elb, ctx, s), m_fs(fs, fs + num_fs), m_f_types(ftypes, ftypes + num_fs), m_args(args, args + num_args), @@ -100,7 +100,7 @@ public: class no_overload_exception : public overload_exception { public: - no_overload_exception(elaborator const & elb, context const & ctx, expr const & s, + no_overload_exception(old_elaborator const & elb, context const & ctx, expr const & s, unsigned num_fs, expr const * fs, expr const * ftypes, unsigned num_args, expr const * args, expr const * argtypes): overload_exception(elb, ctx, s, num_fs, fs, ftypes, num_args, args, argtypes) {} @@ -109,13 +109,13 @@ public: class ambiguous_overload_exception : public overload_exception { public: - ambiguous_overload_exception(elaborator const & elb, context const & ctx, expr const & s, + ambiguous_overload_exception(old_elaborator const & elb, context const & ctx, expr const & s, unsigned num_fs, expr const * fs, expr const * ftypes, unsigned num_args, expr const * args, expr const * argtypes): overload_exception(elb, ctx, s, num_fs, fs, ftypes, num_args, args, argtypes) {} virtual char const * what() const noexcept { return "ambiguous overloads"; } }; -regular const & operator<<(regular const & out, elaborator_exception const & ex); -diagnostic const & operator<<(diagnostic const & out, elaborator_exception const & ex); +regular const & operator<<(regular const & out, old_elaborator_exception const & ex); +diagnostic const & operator<<(diagnostic const & out, old_elaborator_exception const & ex); } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 7f3f1cd8c..74905d8e1 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -117,7 +117,7 @@ class parser::imp { typedef buffer> bindings_buffer; frontend m_frontend; scanner m_scanner; - elaborator m_elaborator; + old_elaborator m_elaborator; scanner::token m_curr; bool m_use_exceptions; bool m_interactive; @@ -1502,20 +1502,24 @@ class parser::imp { return display_error_pos(m_last_cmd_pos); } } + void display_error(char const * msg, unsigned line, unsigned pos) { display_error_pos(line, pos); regular(m_frontend) << " " << msg << endl; sync(); } + void display_error(char const * msg) { display_error(msg, m_scanner.get_line(), m_scanner.get_pos()); } + void display_error(kernel_exception const & ex) { display_error_pos(m_elaborator.get_original(ex.get_main_expr())); regular(m_frontend) << " " << ex << endl; sync(); } - void display_error(elaborator_exception const & ex) { + + void display_error(old_elaborator_exception const & ex) { display_error_pos(m_elaborator.get_original(ex.get_expr())); regular(m_frontend) << " " << ex << endl; sync(); @@ -1582,7 +1586,7 @@ public: display_error(ex); if (m_use_exceptions) throw; - } catch (elaborator_exception & ex) { + } catch (old_elaborator_exception & ex) { m_found_errors = true; if (m_show_errors) display_error(ex); diff --git a/src/kernel/unification_constraint.cpp b/src/kernel/unification_constraint.cpp index b1abed8af..8987de571 100644 --- a/src/kernel/unification_constraint.cpp +++ b/src/kernel/unification_constraint.cpp @@ -24,7 +24,7 @@ static format add_context(formatter const & fmt, options const & opts, context c } static format add_trace(formatter const & fmt, options const & opts, format const & body, trace const & tr, bool include_trace) { - if (include_trace) { + if (tr && include_trace) { unsigned indent = get_pp_indent(opts); return format{body, line(), format("Trace:"), nest(indent, compose(line(), tr.pp(fmt, opts)))}; } else { diff --git a/src/library/elaborator/CMakeLists.txt b/src/library/elaborator/CMakeLists.txt new file mode 100644 index 000000000..28bc51375 --- /dev/null +++ b/src/library/elaborator/CMakeLists.txt @@ -0,0 +1,2 @@ +add_library(elaborator elaborator.cpp) +target_link_libraries(elaborator ${LEAN_LIBS}) diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp new file mode 100644 index 000000000..f7ad3d24a --- /dev/null +++ b/src/library/elaborator/elaborator.cpp @@ -0,0 +1,59 @@ +/* +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.h" + +namespace lean { +class elaborator::imp { + 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, unification_constraint const *, + std::shared_ptr const & s, std::shared_ptr const & p): + m_env(env), + m_synthesizer(s), + m_plugin(p) { + m_interrupted = false; + } + + substitution next() { + // TODO(Leo) + return substitution(); + } + + void interrupt() { + m_interrupted = true; + } +}; + +elaborator::elaborator(environment const & env, + metavar_env const & menv, + unsigned num_cnstrs, + unification_constraint const * cnstrs, + std::shared_ptr const & s, + std::shared_ptr const & p): + m_ptr(new imp(env, menv, num_cnstrs, cnstrs, s, p)) { +} + +elaborator::elaborator(environment const & env, + metavar_env const & menv, + context const & ctx, expr const & lhs, expr const & rhs): + elaborator(env, menv, { mk_eq_constraint(ctx, lhs, rhs, trace()) }) { +} + +elaborator::~elaborator() { +} + +substitution elaborator::next() { + return m_ptr->next(); +} + +void elaborator::interrupt() { + m_ptr->interrupt(); +} +} diff --git a/src/library/elaborator/elaborator.h b/src/library/elaborator/elaborator.h new file mode 100644 index 000000000..c73dc0eee --- /dev/null +++ b/src/library/elaborator/elaborator.h @@ -0,0 +1,63 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "kernel/expr.h" +#include "kernel/environment.h" +#include "kernel/metavar.h" +#include "kernel/unification_constraint.h" +#include "library/elaborator/elaborator_plugin.h" +#include "library/elaborator/synthesizer.h" + +namespace lean { +/** + \brief Elaborator is the main object used to fill "holes" in Lean. + Each hole is represented using a metavariable. This object is + responsible for solving the easy "holes" and invoking external + plugins/synthesizers for filling the other ones. It is also + responsible for managing the search space (i.e., managing the + backtracking search). + + The elaborator can be customized using: + + 1) Elaborator plugins. They are invoked whenever the elaborator + does not know how to solve a unification constraint. + + 2) Synthesizers. They are invoked whenever the elaborator does not + have unification constraints for inferring a particular hole. + + The result is a sequence of substitutions. Each substitution + represents a different way of filling the holes. +*/ +class elaborator { +public: + class imp; + std::shared_ptr m_ptr; +public: + elaborator(environment const & env, + metavar_env const & menv, + unsigned num_cnstrs, + unification_constraint const * cnstrs, + 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, + 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(environment const & env, + metavar_env const & menv, + context const & ctx, expr const & lhs, expr const & rhs); + + ~elaborator(); + + substitution next(); + void interrupt(); +}; +} diff --git a/src/library/elaborator/elaborator_exception.h b/src/library/elaborator/elaborator_exception.h new file mode 100644 index 000000000..ee1ae18e5 --- /dev/null +++ b/src/library/elaborator/elaborator_exception.h @@ -0,0 +1,24 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "util/exception.h" +#include "kernel/trace.h" + +namespace lean { +/** + \brief Elaborator and related components store the reason for + failure in trace objects. +*/ +class elaborator_exception : public exception { + trace m_trace; +public: + elaborator_exception(trace const & tr):m_trace(tr) {} + virtual ~elaborator_exception() {} + 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 new file mode 100644 index 000000000..5bed23efa --- /dev/null +++ b/src/library/elaborator/elaborator_plugin.h @@ -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 +*/ +#pragma once +#include +#include "util/list.h" +#include "kernel/environment.h" +#include "kernel/context.h" +#include "kernel/unification_constraint.h" + +namespace lean { +class elaborator_plugin { +public: + virtual ~elaborator_plugin() {} + + /** \brief The plugin produces a "result" object that can generates the sequence of possible solutions. */ + class result { + public: + virtual ~result() {} + /** + \brief Return the next possible solution. An elaborator_exception is throw in case of failure. + + 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; + /** \brief Interrupt the computation for the next solution. */ + virtual void interrupt() = 0; + }; + + /** + \brief Ask plugin to solve the constraint \c cnstr in the given + environment and metavar environment. + */ + virtual std::unique_ptr operator()(environment const & env, metavar_env const & menv, unification_constraint const & cnstr) = 0; +}; +} diff --git a/src/library/elaborator/synthesizer.h b/src/library/elaborator/synthesizer.h new file mode 100644 index 000000000..197ba128d --- /dev/null +++ b/src/library/elaborator/synthesizer.h @@ -0,0 +1,37 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include "kernel/environment.h" +#include "kernel/context.h" +#include "library/elaborator/elaborator_exception.h" + +namespace lean { +/** + \brief A synthesizer generates a sequence of expressions of a given type. +*/ +class synthesizer { +public: + virtual ~synthesizer() {} + + /** \brief The synthesizer produces a "result" object that can generates the sequence of possible solutions. */ + class result { + public: + virtual ~result() {} + /** \brief Return the next possible solution. An elaborator_exception is throw in case of failure. */ + virtual expr next() = 0; + /** \brief Interrupt the computation for the next solution. */ + virtual void interrupt() = 0; + }; + + /** + \brief Return an object for computing a sequence of expressions + of type \c type in the given environment and context. + */ + virtual std::unique_ptr operator()(environment const & env, context const & ctx, expr const & type) = 0; +}; +} diff --git a/src/tests/frontends/lean/implicit_args.cpp b/src/tests/frontends/lean/implicit_args.cpp index 2212ea510..ea4aab3ce 100644 --- a/src/tests/frontends/lean/implicit_args.cpp +++ b/src/tests/frontends/lean/implicit_args.cpp @@ -20,7 +20,7 @@ Author: Leonardo de Moura using namespace lean; expr elaborate(expr const & e, frontend const & env) { - elaborator elb(env); + old_elaborator elb(env); return elb(e); }