From 73bbf67702491e70337fda5e212a15acbc9cc2f9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 28 Nov 2013 19:00:48 -0800
Subject: [PATCH] refactor(library/elaborator): simplify synthesizer interface

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/elaborator/elaborator.cpp |  8 ++++----
 src/library/elaborator/synthesizer.h  | 14 +++-----------
 2 files changed, 7 insertions(+), 15 deletions(-)

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<synthesizer::result> m_alternatives;
+        expr             m_metavar;
+        lazy_list<expr>  m_alternatives;
 
-        synthesizer_case_split(expr const & m, std::unique_ptr<synthesizer::result> & r, state const & prev_state):
+        synthesizer_case_split(expr const & m, lazy_list<expr> 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 <memory>
+#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<result> operator()(environment const & env, context const & ctx, expr const & type) = 0;
+    virtual lazy_list<expr> operator()(environment const & env, context const & ctx, expr const & type) = 0;
 };
 }