From b270fb0030891fca9d479ba4e9dbc436941eaf5c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 10 Dec 2013 15:55:46 -0800 Subject: [PATCH] refactor(library/elaborator): remove synthesizer Synthesizer is not part of the elaborator anymore. The elaborator fills the "easy" holes. The remaining holes are filled using different techniques (e.g., tactic framework) that are independent of the elaborator. Signed-off-by: Leonardo de Moura --- src/library/elaborator/elaborator.cpp | 22 ++------- src/library/elaborator/elaborator.h | 26 +++++----- .../elaborator/elaborator_justification.cpp | 45 ----------------- .../elaborator/elaborator_justification.h | 49 ------------------- src/library/elaborator/synthesizer.h | 28 ----------- 5 files changed, 14 insertions(+), 156 deletions(-) delete mode 100644 src/library/elaborator/synthesizer.h 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; -}; -}