feat(elaborator): add new elaborator interface

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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}")

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 & ) {}
+old_elaborator::old_elaborator(frontend const & ) {}
-elaborator::~elaborator() {}
+old_elaborator::~old_elaborator() {}
-expr elaborator::operator()(expr const & e) { return e; }
+expr old_elaborator::operator()(expr const & e) { return e; }
-expr elaborator::operator()(expr const & e, expr const & /* expected_type */) { return e; }
+expr old_elaborator::operator()(expr const & e, expr const & /* expected_type */) { return e; }
-expr const & elaborator::get_original(expr const & e) const { return e; }
+expr const & old_elaborator::get_original(expr const & e) const { return e; }
-void elaborator::set_interrupt(bool ) {}
+void old_elaborator::set_interrupt(bool ) {}
-void elaborator::clear() {}
+void old_elaborator::clear() {}
-environment const & elaborator::get_environment() const {
+environment const & old_elaborator::get_environment() const {
     static thread_local environment g_env;
     return g_env;
 }
-void elaborator::display(std::ostream & ) const {}
+void old_elaborator::display(std::ostream & ) const {}
-format elaborator::pp(formatter &, options const &) const { return format(); }
+format old_elaborator::pp(formatter &, options const &) const { return format(); }
-void elaborator::print(imp * ptr) { lean_assert(ptr); }
+void old_elaborator::print(imp * ptr) { lean_assert(ptr); }
-bool elaborator::has_constraints() const { return false; }
+bool old_elaborator::has_constraints() const { return false; }
 }

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<imp> m_ptr;
     static void print(imp * ptr);
 public:
-    explicit elaborator(frontend const & fe);
+    explicit old_elaborator(frontend const & fe);
-    ~elaborator();
+    ~old_elaborator();
 
     expr operator()(expr const & e);
     expr operator()(expr const & e, expr const & expected_type);

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<expr> 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;

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) {}
+    old_elaborator_exception(old_elaborator const & elb, context const & ctx, expr const & e):m_elb(elb), m_context(ctx), m_expr(e) {}
-    virtual ~elaborator_exception() noexcept {}
+    virtual ~old_elaborator_exception() noexcept {}
-    elaborator const & get_elaborator() const { return m_elb; }
+    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<expr> m_args;
     std::vector<expr> 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<expr> const & args, std::vector<expr> 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<expr> m_fs;
     std::vector<expr> m_f_types;
     std::vector<expr> m_args;
     std::vector<expr> 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);
+regular const & operator<<(regular const & out, old_elaborator_exception const & ex);
-diagnostic const & operator<<(diagnostic const & out, elaborator_exception const & ex);
+diagnostic const & operator<<(diagnostic const & out, old_elaborator_exception const & ex);
 }

src/frontends/lean/parser.cpp

@@ -117,7 +117,7 @@ class parser::imp {
     typedef buffer<std::tuple<pos_info, name, expr, bool>> 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);

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 {

src/library/elaborator/CMakeLists.txt

@@ -0,0 +1,2 @@
+add_library(elaborator elaborator.cpp)
+target_link_libraries(elaborator ${LEAN_LIBS})

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<synthesizer>       m_synthesizer;
+    std::shared_ptr<elaborator_plugin> m_plugin;
+    bool                               m_interrupted;
+public:
+    imp(environment const & env, metavar_env const &, unsigned, unification_constraint const *,
+        std::shared_ptr<synthesizer> const & s, std::shared_ptr<elaborator_plugin> 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<synthesizer> const & s,
+                       std::shared_ptr<elaborator_plugin> 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();
+}
+}

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<imp> m_ptr;
+public:
+    elaborator(environment const & env,
+               metavar_env const & menv,
+               unsigned num_cnstrs,
+               unification_constraint const * cnstrs,
+               std::shared_ptr<synthesizer> const & s = std::shared_ptr<synthesizer>(),
+               std::shared_ptr<elaborator_plugin> const & p = std::shared_ptr<elaborator_plugin>());
+
+    elaborator(environment const & env,
+               metavar_env const & menv,
+               std::initializer_list<unification_constraint> const & cnstrs,
+               std::shared_ptr<synthesizer> const & s = std::shared_ptr<synthesizer>(),
+               std::shared_ptr<elaborator_plugin> const & p = std::shared_ptr<elaborator_plugin>()):
+        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();
+};
+}

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; }
+};
+}

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 <memory>
+#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<metavar_env, list<unification_constraint>> 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<result> operator()(environment const & env, metavar_env const & menv, unification_constraint const & cnstr) = 0;
+};
+}

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 <memory>
+#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<result> operator()(environment const & env, context const & ctx, expr const & type) = 0;
+};
+}

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);
 }