diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index 036abbb3e..c1f062f78 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -104,13 +104,13 @@ class elaborator::imp { }; struct synthesizer_case_split : public case_split { - expr m_metavar; - std::unique_ptr m_alternatives; + expr m_metavar; + lazy_list m_alternatives; - synthesizer_case_split(expr const & m, std::unique_ptr & r, state const & prev_state): + synthesizer_case_split(expr const & m, lazy_list const & r, state const & prev_state): case_split(prev_state), m_metavar(m), - m_alternatives(std::move(r)) { + m_alternatives(r) { } virtual ~synthesizer_case_split() {} diff --git a/src/library/elaborator/synthesizer.h b/src/library/elaborator/synthesizer.h index fccccb0f3..8d50bb197 100644 --- a/src/library/elaborator/synthesizer.h +++ b/src/library/elaborator/synthesizer.h @@ -6,6 +6,7 @@ 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" @@ -18,19 +19,10 @@ 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. */ - }; - /** - \brief Return an object for computing a sequence of expressions + \brief Return 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; + virtual lazy_list operator()(environment const & env, context const & ctx, expr const & type) = 0; }; }