diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index 25940fd1d4..3d5a60558f 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -103,19 +103,6 @@ class elaborator::imp { } }; - struct synthesizer_case_split : public case_split { - expr m_metavar; - lazy_list m_alternatives; - - synthesizer_case_split(expr const & m, lazy_list const & r, state const & prev_state): - case_split(prev_state), - m_metavar(m), - m_alternatives(r) { - } - - virtual ~synthesizer_case_split() {} - }; - struct plugin_case_split : public case_split { unification_constraint m_constraint; std::unique_ptr m_alternatives; @@ -138,7 +125,6 @@ class elaborator::imp { 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; int m_quota; @@ -1410,12 +1396,11 @@ class elaborator::imp { 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): + options const & opts, std::shared_ptr const & p): m_env(env), m_type_inferer(env), m_normalizer(env), m_state(menv, num_cnstrs, cnstrs), - m_synthesizer(s), m_plugin(p) { set_options(opts); m_next_id = 0; @@ -1446,7 +1431,7 @@ public: check_interrupted(); cnstr_queue & q = m_state.m_queue; if (q.empty() || m_quota < - static_cast(q.size()) - 10) { - // TODO(Leo): implement interface with synthesizer + // TODO(Leo): improve exit condition return m_state.m_menv; } else { unification_constraint c = q.front(); @@ -1478,9 +1463,8 @@ elaborator::elaborator(environment const & env, 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, opts, s, p)) { + m_ptr(new imp(env, menv, num_cnstrs, cnstrs, opts, p)) { } elaborator::elaborator(environment const & env, diff --git a/src/library/elaborator/elaborator.h b/src/library/elaborator/elaborator.h index ded5fd124e..7150e1692d 100644 --- a/src/library/elaborator/elaborator.h +++ b/src/library/elaborator/elaborator.h @@ -11,24 +11,22 @@ Author: Leonardo de Moura #include "kernel/metavar.h" #include "kernel/unification_constraint.h" #include "library/elaborator/elaborator_plugin.h" -#include "library/elaborator/synthesizer.h" +#include "library/elaborator/elaborator_exception.h" namespace lean { /** - \brief Elaborator is the main object used to fill "holes" in Lean. + \brief Elaborator fills "holes" in Lean using unification based + method. This is essentially a generalizationof the ML type inference + algorithm. + 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). + plugins 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 elaborator can be customized using plugins that are invoked + whenever the elaborator does not know how to solve a unification + constraint. The result is a sequence of substitutions. Each substitution represents a different way of filling the holes. @@ -43,16 +41,14 @@ public: 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(), opts, s, p) {} + elaborator(env, menv, cnstrs.size(), cnstrs.begin(), opts, p) {} elaborator(environment const & env, metavar_env const & menv, diff --git a/src/library/elaborator/elaborator_justification.cpp b/src/library/elaborator/elaborator_justification.cpp index dc803db4d9..934436671f 100644 --- a/src/library/elaborator/elaborator_justification.cpp +++ b/src/library/elaborator/elaborator_justification.cpp @@ -97,51 +97,6 @@ void typeof_mvar_justification::get_children(buffer & r) co push_back(r, m_justification); } -// ------------------------- -// Synthesis justification objects -// ------------------------- -synthesis_justification::synthesis_justification(context const & ctx, expr const & mvar, expr const & type, unsigned num, justification const * substs): - m_context(ctx), - m_mvar(mvar), - m_type(type), - m_substitution_justifications(substs, substs + num) { -} -synthesis_justification::~synthesis_justification() { -} -format synthesis_justification::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_justification::get_children(buffer & r) const { - append(r, m_substitution_justifications); -} -optional synthesis_justification::get_main_expr() const { - return some_expr(m_mvar); -} - -char const * synthesis_failure_justification::get_label() const { - return "Failed to synthesize expression of type for"; -} -synthesis_failure_justification::synthesis_failure_justification(context const & ctx, expr const & mvar, expr const & type, justification const & tr, unsigned num, justification const * substs): - synthesis_justification(ctx, mvar, type, num, substs), - m_justification(tr) { -} -synthesis_failure_justification::~synthesis_failure_justification() { -} -void synthesis_failure_justification::get_children(buffer & r) const { - synthesis_justification::get_children(r); - push_back(r, m_justification); -} - -char const * synthesized_assignment_justification::get_label() const { - return "Synthesized assignment for"; -} - // ------------------------- // Next solution justification // ------------------------- diff --git a/src/library/elaborator/elaborator_justification.h b/src/library/elaborator/elaborator_justification.h index 298baa4d63..acf6836aad 100644 --- a/src/library/elaborator/elaborator_justification.h +++ b/src/library/elaborator/elaborator_justification.h @@ -153,55 +153,6 @@ public: virtual void get_children(buffer & r) const; }; -/** - \brief Base class for synthesis_failure_justification and synthesized_assignment_justification -*/ -class synthesis_justification : public justification_cell { - context m_context; - expr m_mvar; - expr m_type; - std::vector m_substitution_justifications; // justification objects justifying the assignments used to instantiate \c m_type and \c m_context. -protected: - virtual char const * get_label() const = 0; -public: - synthesis_justification(context const & ctx, expr const & mvar, expr const & type, unsigned num, justification const * substs); - virtual ~synthesis_justification(); - virtual format pp_header(formatter const &, options const &) const; - virtual void get_children(buffer & r) const; - virtual optional get_main_expr() const; -}; - -/** - \brief Justification 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_justification : public synthesis_justification { - justification m_justification; // justification object produced by the synthesizer -protected: - virtual char const * get_label() const; -public: - synthesis_failure_justification(context const & ctx, expr const & mvar, expr const & type, justification const & tr, unsigned num, justification const * substs); - virtual ~synthesis_failure_justification(); - virtual void get_children(buffer & r) const; -}; - -/** - \brief Justification object used to justify a metavar assignment produced by a synthesizer. -*/ -class synthesized_assignment_justification : public synthesis_justification { -protected: - virtual char const * get_label() const; -public: - synthesized_assignment_justification(context const & ctx, expr const & mvar, expr const & type, unsigned num, justification const * substs): - synthesis_justification(ctx, mvar, type, num, substs) { - } -}; - /** \brief Justification object used to justify that we are moving to the next solution. */ diff --git a/src/library/elaborator/synthesizer.h b/src/library/elaborator/synthesizer.h deleted file mode 100644 index 8d50bb1978..0000000000 --- a/src/library/elaborator/synthesizer.h +++ /dev/null @@ -1,28 +0,0 @@ -/* -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/lazy_list.h" -#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 Return a sequence of expressions - of type \c type in the given environment and context. - */ - virtual lazy_list operator()(environment const & env, context const & ctx, expr const & type) = 0; -}; -}