feat(elaborator): add trace objects for elaborator

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

src/kernel/metavar.cpp

@@ -166,6 +166,21 @@ void metavar_env::assign(expr const & m, expr const & t, trace const & tr) {
     assign(metavar_name(m), t, tr);
 }
 
+struct found_unassigned{};
+name metavar_env::find_unassigned_metavar() const {
+    name r;
+    try {
+        m_metavar_types.for_each([&](name const & m, expr const &) {
+                if (!m_substitution.is_assigned(m)) {
+                    r = m;
+                    throw found_unassigned();
+                }
+            });
+    } catch (found_unassigned &) {
+    }
+    return r;
+}
+
 expr instantiate_metavars(expr const & e, substitution const & s) {
     if (!has_metavar(e)) {
         return e;

src/kernel/metavar.h

@@ -24,6 +24,11 @@ class substitution {
 public:
     substitution();
 
+    friend void swap(substitution & s1, substitution & s2) {
+        swap(s1.m_subst, s2.m_subst);
+        std::swap(s1.m_size, s2.m_size);
+    }
+
     /**
        \brief Return the number of assigned metavariables in this substitution.
     */
@@ -101,6 +106,15 @@ public:
     metavar_env(name const & prefix);
     metavar_env();
 
+    friend void swap(metavar_env & a, metavar_env & b) {
+        swap(a.m_name_generator,   b.m_name_generator);
+        swap(a.m_substitution,     b.m_substitution);
+        swap(a.m_metavar_types,    b.m_metavar_types);
+        swap(a.m_metavar_contexts, b.m_metavar_contexts);
+        swap(a.m_metavar_traces,   b.m_metavar_traces);
+        std::swap(a.m_timestamp,   b.m_timestamp);
+    }
+
     /**
        \brief The timestamp is increased whenever this environment is
        updated.
@@ -178,6 +192,13 @@ public:
        \pre is_metavar(m)
     */
     expr get_subst(expr const & m) const { return m_substitution.get_subst(m); }
+
+    /**
+       \brief Return a unassigned metavariable (if one exists). Only metavariables
+       that have types are considered. Return the anonymous name if all metavariables (with types)
+       are assigned.
+    */
+    name find_unassigned_metavar() const;
 };
 
 /**

src/kernel/trace.cpp

@@ -9,6 +9,31 @@ Author: Leonardo de Moura
 #include "kernel/trace.h"
 
 namespace lean {
+void trace_cell::add_pos_info(format & r, expr const & e, pos_info_provider const * p) {
+    if (!p || !e)
+        return;
+    format f = p->pp(e);
+    if (!f)
+        return;
+    r += f;
+    r += space();
+}
+
+format trace_cell::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children) const {
+    format r;
+    add_pos_info(r, get_main_expr(), p);
+    r += pp_header(fmt, opts);
+    if (display_children) {
+        buffer<trace_cell *> children;
+        get_children(children);
+        unsigned indent = get_pp_indent(opts);
+        for (trace_cell * child : children) {
+            r += nest(indent, compose(line(), child->pp(fmt, opts, p, display_children)));
+        }
+    }
+    return r;
+}
+
 bool trace::has_children() const {
     buffer<trace_cell *> r;
     get_children(r);

src/kernel/trace.h

@@ -25,10 +25,13 @@ class trace;
 class trace_cell {
     MK_LEAN_RC();
     void dealloc() { delete this; }
+protected:
+    static void add_pos_info(format & r, expr const & e, pos_info_provider const * p);
 public:
     trace_cell():m_rc(0) {}
     virtual ~trace_cell() {}
-    virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children) const = 0;
+    virtual format pp_header(formatter const & fmt, options const & opts) const = 0;
+    virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children) const;
     virtual void get_children(buffer<trace_cell*> & r) const = 0;
     virtual expr const & get_main_expr() const { return expr::null(); }
     bool is_shared() const { return get_rc() > 1; }

src/kernel/type_checker_trace.cpp

@@ -8,24 +8,13 @@ Author: Leonardo de Moura
 
 namespace lean {
 
-void add_pos_info(format & r, expr const & e, pos_info_provider const * p) {
-    if (!p)
-        return;
-    format f = p->pp(e);
-    if (!f)
-        return;
-    r += f;
-    r += space();
-}
-
 function_expected_trace_cell::~function_expected_trace_cell() {
 }
 
-format function_expected_trace_cell::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool) const {
+format function_expected_trace_cell::pp_header(formatter const & fmt, options const & opts) const {
     unsigned indent = get_pp_indent(opts);
     format expr_fmt = fmt(m_ctx, m_app, false, opts);
     format r;
-    add_pos_info(r, get_main_expr(), p);
     r += format("Function expected at");
     r += nest(indent, compose(line(), expr_fmt));
     return r;
@@ -41,10 +30,9 @@ expr const & function_expected_trace_cell::get_main_expr() const {
 app_type_match_trace_cell::~app_type_match_trace_cell() {
 }
 
-format app_type_match_trace_cell::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool) const {
+format app_type_match_trace_cell::pp_header(formatter const & fmt, options const & opts) const {
     unsigned indent = get_pp_indent(opts);
     format r;
-    add_pos_info(r, get_main_expr(), p);
     r += format("Type of argument ");
     r += format(m_i);
     r += format(" must be convertible to the expected type in the application of");
@@ -70,11 +58,10 @@ expr const & app_type_match_trace_cell::get_main_expr() const {
 type_expected_trace_cell::~type_expected_trace_cell() {
 }
 
-format type_expected_trace_cell::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool) const {
+format type_expected_trace_cell::pp_header(formatter const & fmt, options const & opts) const {
     unsigned indent = get_pp_indent(opts);
     format expr_fmt = fmt(m_ctx, m_type, false, opts);
     format r;
-    add_pos_info(r, get_main_expr(), p);
     r += format("Type expected at");
     r += nest(indent, compose(line(), expr_fmt));
     return r;
@@ -90,9 +77,8 @@ expr const & type_expected_trace_cell::get_main_expr() const {
 def_type_match_trace_cell::~def_type_match_trace_cell() {
 }
 
-format def_type_match_trace_cell::pp(formatter const &, options const &, pos_info_provider const * p, bool) const {
+format def_type_match_trace_cell::pp_header(formatter const &, options const &) const {
     format r;
-    add_pos_info(r, get_main_expr(), p);
     r += format("Type of definition '");
     r += format(get_name());
     r += format("' must be convertible to expected type.");

src/kernel/type_checker_trace.h

@@ -27,7 +27,7 @@ class function_expected_trace_cell : public trace_cell {
 public:
     function_expected_trace_cell(context const & c, expr const & app):m_ctx(c), m_app(app) {}
     virtual ~function_expected_trace_cell();
-    virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children) const;
+    virtual format pp_header(formatter const & fmt, options const & opts) const;
     virtual void get_children(buffer<trace_cell*> &) const;
     virtual expr const & get_main_expr() const;
     context const & get_context() const { return m_ctx; }
@@ -52,7 +52,7 @@ class app_type_match_trace_cell : public trace_cell {
 public:
     app_type_match_trace_cell(context const & c, expr const & a, unsigned i):m_ctx(c), m_app(a), m_i(i) {}
     virtual ~app_type_match_trace_cell();
-    virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children) const;
+    virtual format pp_header(formatter const & fmt, options const & opts) const;
     virtual void get_children(buffer<trace_cell*> &) const;
     virtual expr const & get_main_expr() const;
     context const & get_context() const { return m_ctx; }
@@ -75,7 +75,7 @@ class type_expected_trace_cell : public trace_cell {
 public:
     type_expected_trace_cell(context const & c, expr const & t):m_ctx(c), m_type(t) {}
     virtual ~type_expected_trace_cell();
-    virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children) const;
+    virtual format pp_header(formatter const & fmt, options const & opts) const;
     virtual void get_children(buffer<trace_cell*> &) const;
     virtual expr const & get_main_expr() const;
     context const & get_context() const { return m_ctx; }
@@ -112,7 +112,7 @@ class def_type_match_trace_cell : public trace_cell {
 public:
     def_type_match_trace_cell(context const & c, name const & n, expr const & v):m_ctx(c), m_name(n), m_value(v) {}
     virtual ~def_type_match_trace_cell();
-    virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children) const;
+    virtual format pp_header(formatter const & fmt, options const & opts) const;
     virtual void get_children(buffer<trace_cell*> &) const;
     virtual expr const & get_main_expr() const;
     context const & get_context() const { return m_ctx; }

src/kernel/unification_constraint.h

@@ -47,6 +47,7 @@ public:
     trace const & get_trace() const { return m_trace; }
     context const & get_context() const { return m_ctx; }
     virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_trace) const = 0;
+    void set_trace(trace const & t) { lean_assert(!m_trace); m_trace = t; }
 };
 
 class unification_constraint {
@@ -74,6 +75,9 @@ public:
         return m_ptr->pp(fmt, opts, p, include_trace);
     }
 
+    trace const & get_trace() const { lean_assert(m_ptr); return m_ptr->get_trace(); }
+    void set_trace(trace const & t) { lean_assert(!get_trace()); lean_assert(m_ptr); m_ptr->set_trace(t); }
+
     friend unification_constraint mk_eq_constraint(context const & c, expr const & lhs, expr const & rhs, trace const & t);
     friend unification_constraint mk_convertible_constraint(context const & c, expr const & from, expr const & to, trace const & t);
     friend unification_constraint mk_max_constraint(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, trace const & t);

src/library/elaborator/CMakeLists.txt

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

src/library/elaborator/elaborator.cpp

@@ -4,55 +4,407 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <memory>
+#include <vector>
 #include "util/pdeque.h"
 #include "kernel/formatter.h"
+#include "library/light_checker.h"
 #include "library/elaborator/elaborator.h"
+#include "library/elaborator/elaborator_trace.h"
 
 namespace lean {
+static name g_x_name("x");
+
 class elaborator::imp {
     typedef pdeque<unification_constraint> cnstr_queue;
 
     struct state {
-        unsigned    m_id;
         metavar_env m_menv;
         cnstr_queue m_queue;
+
+        state(metavar_env const & menv, unsigned num_cnstrs, unification_constraint const * cnstrs):
+            m_menv(menv) {
+            for (unsigned i = 0; i < num_cnstrs; i++)
+                m_queue.push_back(cnstrs[i]);
+        }
+
+        state(metavar_env const & menv, cnstr_queue const & q):
+            m_menv(menv),
+            m_queue(q) {
+        }
     };
 
-    environment const &                m_env;
+    /**
-    std::shared_ptr<synthesizer>       m_synthesizer;
+       \brief Base class for case splits performed by the elaborator.
-    std::shared_ptr<elaborator_plugin> m_plugin;
+    */
-    bool                               m_interrupted;
+    struct case_split {
-public:
+        trace              m_curr_assumption; // trace object used to justify current split
-    imp(environment const & env, metavar_env const &, unsigned num_cnstrs, unification_constraint const * cnstrs,
+        state              m_prev_state;
-        std::shared_ptr<synthesizer> const & s, std::shared_ptr<elaborator_plugin> const & p):
+        std::vector<trace> m_failed_traces;   // traces/justifications for failed branches
-        m_env(env),
-        m_synthesizer(s),
-        m_plugin(p) {
-        m_interrupted = false;
 
-        formatter fmt = mk_simple_formatter();
+        case_split(state const & prev_state):m_prev_state(prev_state) {}
-        for (unsigned i = 0; i < num_cnstrs; i++) {
+        virtual ~case_split() {}
-            std::cout << cnstrs[i].pp(fmt, options(), nullptr, true) << "\n";
+
+        virtual bool next(imp & owner) = 0;
+    };
+
+    /**
+       \brief Case-split object for choice constraints.
+    */
+    struct choice_case_split : public case_split {
+        unsigned               m_idx;
+        unification_constraint m_choice;
+
+        choice_case_split(unification_constraint const & c, state const & prev_state):
+            case_split(prev_state),
+            m_idx(0),
+            m_choice(c) {
+        }
+
+        virtual ~choice_case_split() {}
+
+        virtual bool next(imp & owner) {
+            return owner.next_choice_case(*this);
+        }
+    };
+
+    /**
+       \brief Case split object for higher-order matching
+    */
+    struct ho_match_case_split : public case_split {
+        unification_constraint m_constraint;
+        unsigned               m_idx;    // current alternative
+        std::vector<state>     m_states; // set of alternatives
+
+        ho_match_case_split(unification_constraint const & cnstr, unsigned num_states, state const * states, state const & prev_state):
+            case_split(prev_state),
+            m_constraint(cnstr),
+            m_idx(0),
+            m_states(states, states + num_states) {
+        }
+
+        virtual ~ho_match_case_split() {}
+
+        virtual bool next(imp & owner) {
+            return owner.next_ho_case(*this);
+        }
+    };
+
+    struct synthesizer_case_split : public case_split {
+        expr                                 m_metavar;
+        std::unique_ptr<synthesizer::result> m_alternatives;
+
+        synthesizer_case_split(expr const & m, std::unique_ptr<synthesizer::result> & r, state const & prev_state):
+            case_split(prev_state),
+            m_metavar(m),
+            m_alternatives(std::move(r)) {
+        }
+
+        virtual ~synthesizer_case_split() {}
+    };
+
+    struct plugin_case_split : public case_split {
+        unification_constraint                     m_constraint;
+        std::unique_ptr<elaborator_plugin::result> m_alternatives;
+
+        plugin_case_split(unification_constraint const & cnstr, std::unique_ptr<elaborator_plugin::result> & r, state const & prev_state):
+            case_split(prev_state),
+            m_constraint(cnstr),
+            m_alternatives(std::move(r)) {
+        }
+
+        virtual ~plugin_case_split() {}
+
+        virtual bool next(imp & owner) {
+            return owner.next_plugin_case(*this);
+        }
+    };
+
+    environment const &                      m_env;
+    light_checker                            m_type_infer;
+    state                                    m_state;
+    std::vector<std::unique_ptr<case_split>> m_case_splits;
+    std::shared_ptr<synthesizer>             m_synthesizer;
+    std::shared_ptr<elaborator_plugin>       m_plugin;
+    unsigned                                 m_next_id;
+    unsigned                                 m_delayed;
+    trace                                    m_conflict;
+    bool                                     m_interrupted;
+
+
+    // options
+    bool                                     m_use_traces;
+    bool                                     m_use_beta;
+    bool                                     m_use_normalizer;
+
+    void set_options(options const &) {
+        m_use_traces     = true;
+        m_use_beta       = true;
+        m_use_normalizer = true;
+    }
+
+    void reset_delayed() {
+        m_delayed = 0;
+    }
+
+    trace mk_assumption() {
+        unsigned id = m_next_id;
+        m_next_id++;
+        return trace(new assumption_trace(id));
+    }
+
+    bool process(unification_constraint const & c) {
+        switch (c.kind()) {
+        case unification_constraint_kind::Eq:          return process_eq(c);
+        case unification_constraint_kind::Convertible: return process_convertible(c);
+        case unification_constraint_kind::Max:         return process_max(c);
+        case unification_constraint_kind::Choice:      return process_choice(c);
+        }
+        lean_unreachable();
+        return true;
+    }
+
+    bool process_eq(unification_constraint const & c) {
+        return process_eq_convertible(get_context(c), eq_lhs(c), eq_rhs(c), c);
+    }
+
+    bool process_convertible(unification_constraint const & c) {
+        return process_eq_convertible(get_context(c), convertible_from(c), convertible_to(c), c);
+   }
+
+    bool process_eq_convertible(context const & ctx, expr const & from, expr const & to, unification_constraint const & c) {
+        bool eq = is_eq(c);
+        if (from == to) {
+            reset_delayed();
+            return true;
+        }
+
+        // TODO(Leo)
+
+        if (is_type(from) && is_type(to)) {
+            if ((!eq && m_env.is_ge(ty_level(to), ty_level(from))) || (eq && from == to)) {
+                reset_delayed();
+                return true;
+            } else {
+                m_conflict = trace(new unification_failure_trace(c));
+                return false;
+            }
+        }
+
+        if (is_pi(from) && is_pi(to)) {
+            trace new_trace(new destruct_trace(c));
+            m_state.m_queue.push_front(mk_eq_constraint(ctx, abst_domain(from), abst_domain(to), new_trace));
+            context new_ctx = extend(ctx, abst_name(from), abst_domain(from));
+            if (eq)
+                m_state.m_queue.push_front(mk_eq_constraint(new_ctx, abst_body(from), abst_body(to), new_trace));
+            else
+                m_state.m_queue.push_front(mk_convertible_constraint(new_ctx, abst_body(from), abst_body(to), new_trace));
+            reset_delayed();
+            return true;
+        }
+
+
+        return true;
+   }
+
+
+    bool process_max(unification_constraint const &) {
+        // TODO(Leo)
+         return true;
+   }
+
+    bool process_choice(unification_constraint const &) {
+        // TODO(Leo)
+        return true;
+    }
+
+    void resolve_conflict() {
+        lean_assert(m_conflict);
+        while (!m_case_splits.empty()) {
+            std::unique_ptr<case_split> & d = m_case_splits.back();
+            if (depends_on(m_conflict, d->m_curr_assumption)) {
+                d->m_failed_traces.push_back(m_conflict);
+                if (d->next(*this)) {
+                    m_conflict = trace();
+                    return;
+                }
+            }
+            m_case_splits.pop_back();
+        }
+        throw elaborator_exception(m_conflict);
+    }
+
+    /**
+        \brief Return a unassigned metavariable in the current state.
+        Return the anonymous name if the state does not contain unassigned metavariables.
+    */
+    name find_unassigned_metavar() const {
+        return m_state.m_menv.find_unassigned_metavar();
+    }
+
+    /** \brief Return true if \c a is of the form <tt>(?m ...)</tt> */
+    bool is_meta_app(expr const & a) {
+        return is_app(a) && is_metavar(arg(a, 0));
+    }
+
+    /** \brief Return true iff \c a is a metavariable and has a meta context. */
+    bool is_metavar_with_context(expr const & a) {
+        return is_metavar(a) && has_local_context(a);
+    }
+
+    /** \brief Return true if \c a is of the form <tt>(?m[...] ...)</tt> */
+    bool is_meta_app_with_context(expr const & a) {
+        return is_meta_app(a) && has_local_context(arg(a, 0));
+    }
+
+    expr mk_lambda(name const & n, expr const & d, expr const & b) {
+        return ::lean::mk_lambda(n, d, b);
+    }
+
+    /**
+       \brief Create the term (fun (x_0 : types[0]) ... (x_{n-1} : types[n-1]) body)
+    */
+    expr mk_lambda(buffer<expr> const & types, expr const & body) {
+        expr r = body;
+        unsigned i = types.size();
+        while (i > 0) {
+            --i;
+            r = mk_lambda(name(g_x_name, i), types[i], r);
+        }
+        return r;
+    }
+
+    bool next_choice_case(choice_case_split & s) {
+        unification_constraint & choice = s.m_choice;
+        unsigned idx = s.m_idx;
+        if (idx < choice_size(choice)) {
+            s.m_idx++;
+            s.m_curr_assumption = mk_assumption();
+            m_state = s.m_prev_state;
+            m_state.m_queue.push_front(mk_eq_constraint(get_context(choice), choice_mvar(choice), choice_ith(choice, idx), s.m_curr_assumption));
+            s.m_idx++;
+            return true;
+        } else {
+            m_conflict = trace(new unification_failure_by_cases_trace(choice, s.m_failed_traces.size(), s.m_failed_traces.data()));
+            return false;
         }
     }
 
+    bool next_ho_case(ho_match_case_split &) {
+#if 0
+        unification_constraint & cnstr = s.m_constraint;
+        context const & ctx = get_context(cnstr);
+        expr const & a      = eq_lhs(cnstr);
+        expr const & b      = eq_rhs(cnstr);
+        lean_assert(is_meta_app(a));
+        lean_assert(!has_local_context(arg(a, 0)));
+        lean_assert(!is_meta_app(b));
+        expr f_a       = arg(a, 0);
+        lean_assert(is_metavar(f_a));
+        unsigned num_a = num_args(a);
+
+
+
+        // unification_constraints_wrapper ucw;
+        buffer<expr> arg_types;
+        for (unsigned i = 1; i < num_a; i++) {
+            arg_types.push_back(m_type_infer(arg(a, i), ctx, &s, &ucw));
+        }
+#endif
+        return true;
+    }
+
+    bool next_plugin_case(plugin_case_split & s) {
+        try {
+            s.m_curr_assumption = mk_assumption();
+            std::pair<metavar_env, list<unification_constraint>> r = s.m_alternatives->next(s.m_curr_assumption);
+            m_state.m_queue     = s.m_prev_state.m_queue;
+            m_state.m_menv      = r.first;
+            for (auto c : r.second) {
+                m_state.m_queue.push_front(c);
+            }
+            return true;
+        } catch (exception & ex) {
+            m_conflict = trace(new unification_failure_by_cases_trace(s.m_constraint, s.m_failed_traces.size(), s.m_failed_traces.data()));
+            return false;
+        }
+    }
+
+public:
+    imp(environment const & env, metavar_env const & menv, unsigned num_cnstrs, unification_constraint const * cnstrs,
+        options const & opts, std::shared_ptr<synthesizer> const & s, std::shared_ptr<elaborator_plugin> const & p):
+        m_env(env),
+        m_type_infer(env),
+        m_state(menv, num_cnstrs, cnstrs),
+        m_synthesizer(s),
+        m_plugin(p) {
+        set_options(opts);
+        m_next_id     = 0;
+        m_delayed     = 0;
+        m_interrupted = false;
+
+        display(std::cout);
+    }
+
     substitution next() {
-        // TODO(Leo)
+        check_interrupted(m_interrupted);
-        return substitution();
+        if (m_conflict)
+            throw elaborator_exception(m_conflict);
+        if (!m_case_splits.empty()) {
+            buffer<trace> assumptions;
+            for (std::unique_ptr<case_split> const & cs : m_case_splits)
+                assumptions.push_back(cs->m_curr_assumption);
+            m_conflict = trace(new next_solution_trace(assumptions.size(), assumptions.data()));
+            resolve_conflict();
+        }
+        reset_delayed();
+        while (true) {
+            check_interrupted(m_interrupted);
+            cnstr_queue & q = m_state.m_queue;
+            if (q.empty()) {
+                name m = find_unassigned_metavar();
+                if (m) {
+                    // TODO(Leo)
+                    // erase the following line, and implement interface with synthesizer
+                    return m_state.m_menv.get_substitutions();
+                } else {
+                    return m_state.m_menv.get_substitutions();
+                }
+            } else {
+                unification_constraint c = q.front();
+                q.pop_front();
+                if (!process(c)) {
+                    resolve_conflict();
+                }
+            }
+        }
     }
 
     void interrupt() {
         m_interrupted = true;
+        m_type_infer.set_interrupt(true);
     }
+
+    void display(std::ostream & out) const {
+        m_state.m_menv.get_substitutions().for_each([&](name const & m, expr const & e) {
+                out << m << " <- " << e << "\n";
+            });
+        formatter fmt = mk_simple_formatter();
+        for (auto c : m_state.m_queue) {
+            out << c.pp(fmt, options(), nullptr, false) << "\n";
+        }
+    }
+
 };
 
 elaborator::elaborator(environment const & env,
                        metavar_env const & menv,
                        unsigned num_cnstrs,
                        unification_constraint const * cnstrs,
+                       options const & opts,
                        std::shared_ptr<synthesizer> const & s,
                        std::shared_ptr<elaborator_plugin> const & p):
-    m_ptr(new imp(env, menv, num_cnstrs, cnstrs, s, p)) {
+    m_ptr(new imp(env, menv, num_cnstrs, cnstrs, opts, s, p)) {
 }
 
 elaborator::elaborator(environment const & env,

src/library/elaborator/elaborator.h

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include "util/sexpr/options.h"
 #include "kernel/expr.h"
 #include "kernel/environment.h"
 #include "kernel/metavar.h"
@@ -41,21 +42,23 @@ public:
                metavar_env const & menv,
                unsigned num_cnstrs,
                unification_constraint const * cnstrs,
+               options const & opts = options(),
                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,
+               options const & opts = options(),
                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(env, menv, cnstrs.size(), cnstrs.begin(), opts, s, p) {}
 
     elaborator(environment const & env,
                metavar_env const & menv,
                context const & ctx, expr const & lhs, expr const & rhs);
 
-   ~elaborator();
+    ~elaborator();
 
     substitution next();
     void interrupt();

src/library/elaborator/elaborator_exception.h

@@ -21,4 +21,6 @@ public:
     virtual char const * what() const noexcept { return "elaborator exception"; }
     trace const & get_trace() const { return m_trace; }
 };
+
+
 }

src/library/elaborator/elaborator_plugin.h

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <memory>
+#include <utility>
 #include "util/list.h"
 #include "kernel/environment.h"
 #include "kernel/context.h"
@@ -16,7 +17,7 @@ class elaborator_plugin {
 public:
     virtual ~elaborator_plugin() {}
 
-   /** \brief The plugin produces a "result" object that can generates the sequence of possible solutions. */
+    /** \brief The plugin produces a "result" object that can generates the sequence of possible solutions. */
     class result {
     public:
         virtual ~result() {}
@@ -26,7 +27,7 @@ public:
             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;
+        virtual std::pair<metavar_env, list<unification_constraint>> next(trace const & assumption) = 0;
         /** \brief Interrupt the computation for the next solution. */
         virtual void interrupt() = 0;
     };

src/library/elaborator/elaborator_trace.cpp

@@ -0,0 +1,158 @@
+/*
+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_trace.h"
+
+namespace lean {
+static void push_back(buffer<trace_cell*> & r, trace const & t) {
+    if (t)
+        r.push_back(t.raw());
+}
+
+template<typename T>
+static void append(buffer<trace_cell*> & r, T const & s) {
+    for (auto t : s)
+        push_back(r, t);
+}
+
+// -------------------------
+// Assumptions
+// -------------------------
+assumption_trace::assumption_trace(unsigned idx):m_idx(idx) {
+}
+void assumption_trace::get_children(buffer<trace_cell*> &) const {
+}
+expr const & assumption_trace::get_main_expr() const {
+    return expr::null();
+}
+format assumption_trace::pp_header(formatter const &, options const &) const {
+    return format{format("assumption"), space(), format(m_idx)};
+}
+
+// -------------------------
+// Propagation trace
+// -------------------------
+propagation_trace::propagation_trace(unification_constraint const & c):
+    m_constraint(c) {
+}
+propagation_trace::~propagation_trace() {
+}
+void propagation_trace::get_children(buffer<trace_cell*> & r) const {
+    push_back(r, m_constraint.get_trace());
+}
+expr const & propagation_trace::get_main_expr() const {
+    return expr::null();
+}
+format propagation_trace::pp_header(formatter const & fmt, options const & opts) const {
+    format r;
+    unsigned indent = get_pp_indent(opts);
+    r += format(get_prop_name());
+    r += nest(indent, compose(line(), get_constraint().pp(fmt, opts, nullptr, false)));
+    return r;
+}
+
+// -------------------------
+// Unification failure (by cases)
+// -------------------------
+unification_failure_by_cases_trace::unification_failure_by_cases_trace(unification_constraint const & c, unsigned num, trace const * cs):
+    unification_failure_trace(c),
+    m_cases(cs, cs + num) {
+}
+unification_failure_by_cases_trace::~unification_failure_by_cases_trace() {
+}
+void unification_failure_by_cases_trace::get_children(buffer<trace_cell*> & r) const {
+    push_back(r, get_constraint().get_trace());
+    append(r, m_cases);
+}
+
+// -------------------------
+// Substitution trace
+// -------------------------
+substitution_trace::substitution_trace(unification_constraint const & c, trace const & t):
+    propagation_trace(c),
+    m_assignment_trace(t) {
+}
+substitution_trace::~substitution_trace() {
+}
+void substitution_trace::get_children(buffer<trace_cell*> & r) const {
+    propagation_trace::get_children(r);
+    push_back(r, m_assignment_trace);
+}
+
+multi_substitution_trace::multi_substitution_trace(unification_constraint const & c, unsigned num, trace const * ts):
+    propagation_trace(c),
+    m_assignment_traces(ts, ts + num) {
+}
+multi_substitution_trace::~multi_substitution_trace() {
+}
+void multi_substitution_trace::get_children(buffer<trace_cell*> & r) const {
+    propagation_trace::get_children(r);
+    append(r, m_assignment_traces);
+}
+
+// -------------------------
+// Synthesis trace objects
+// -------------------------
+synthesis_trace::synthesis_trace(context const & ctx, expr const & mvar, expr const & type, unsigned num, trace const * substs):
+    m_context(ctx),
+    m_mvar(mvar),
+    m_type(type),
+    m_substitution_traces(substs, substs + num) {
+}
+synthesis_trace::~synthesis_trace() {
+}
+format synthesis_trace::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_trace::get_children(buffer<trace_cell*> & r) const {
+    append(r, m_substitution_traces);
+}
+expr const & synthesis_trace::get_main_expr() const {
+    return m_mvar;
+}
+
+char const * synthesis_failure_trace::get_label() const {
+    return "Failed to synthesize expression of type for";
+}
+synthesis_failure_trace::synthesis_failure_trace(context const & ctx, expr const & mvar, expr const & type, trace const & tr, unsigned num, trace const * substs):
+    synthesis_trace(ctx, mvar, type, num, substs),
+    m_trace(tr) {
+}
+synthesis_failure_trace::~synthesis_failure_trace() {
+}
+void synthesis_failure_trace::get_children(buffer<trace_cell*> & r) const {
+    synthesis_trace::get_children(r);
+    push_back(r, m_trace);
+}
+
+char const * synthesized_assignment_trace::get_label() const {
+    return "Synthesized assignment for";
+}
+
+// -------------------------
+// Next solution trace
+// -------------------------
+next_solution_trace::next_solution_trace(unsigned num, trace const * as):
+    m_assumptions(as, as + num) {
+}
+next_solution_trace::~next_solution_trace() {
+}
+format next_solution_trace::pp_header(formatter const &, options const &) const {
+    return format("next solution");
+}
+void next_solution_trace::get_children(buffer<trace_cell*> & r) const {
+    append(r, m_assumptions);
+}
+expr const & next_solution_trace::get_main_expr() const {
+    return expr::null();
+}
+}

src/library/elaborator/elaborator_trace.h

@@ -0,0 +1,194 @@
+/*
+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 <vector>
+#include "kernel/trace.h"
+#include "kernel/unification_constraint.h"
+
+namespace lean {
+/**
+   \brief Base class for trace objects used to justify case-splits.
+*/
+class assumption_trace : public trace_cell {
+    unsigned m_idx;
+public:
+    assumption_trace(unsigned idx);
+    virtual void get_children(buffer<trace_cell*> &) const;
+    virtual expr const & get_main_expr() const;
+    virtual format pp_header(formatter const &, options const &) const;
+};
+
+/**
+   \brief Base class for justifying propagations and failures
+*/
+class propagation_trace : public trace_cell {
+    unification_constraint m_constraint;
+protected:
+    /** \brief Auxiliary method used by pp_header to label a propagation step, subclasses must redefine it. */
+    virtual char const * get_prop_name() const = 0;
+public:
+    propagation_trace(unification_constraint const & c);
+    virtual ~propagation_trace();
+    virtual void get_children(buffer<trace_cell*> & r) const;
+    virtual expr const & get_main_expr() const;
+    virtual format pp_header(formatter const &, options const &) const;
+    unification_constraint const & get_constraint() const { return m_constraint; }
+};
+
+/**
+   \brief Trace object used to mark that a particular unification constraint could not be solved.
+*/
+class unification_failure_trace : public propagation_trace {
+protected:
+    virtual char const * get_prop_name() const { return "Failed to solve"; }
+public:
+    unification_failure_trace(unification_constraint const & c):propagation_trace(c) {}
+};
+
+/**
+   \brief Trace object created for justifying that a constraint that
+   generated a case-split does not have a solution. Each case-split
+   corresponds to a different way of solving the constraint.
+*/
+class unification_failure_by_cases_trace : public unification_failure_trace {
+    std::vector<trace> m_cases; // why each case failed
+public:
+    unification_failure_by_cases_trace(unification_constraint const & c, unsigned num, trace const * cs);
+    virtual ~unification_failure_by_cases_trace();
+    virtual void get_children(buffer<trace_cell*> & r) const;
+};
+
+/**
+   \brief Trace object used to justify a metavar assignment.
+*/
+class assignment_trace : public propagation_trace {
+protected:
+    virtual char const * get_prop_name() const { return "Assignment"; }
+public:
+    assignment_trace(unification_constraint const & c):propagation_trace(c) {}
+};
+
+/**
+   \brief Trace object used to justify simple structural steps when processing unification
+   constraints. For example, given the constraint
+
+   <tt>ctx |- (f a) == (f b)</tt>
+
+   where \c f is a variable, we must have
+
+   <tt>ctx |- a == b</tt>
+
+   The justification for the latter is a destruct trace based on the former.
+*/
+class destruct_trace : public propagation_trace {
+protected:
+    virtual char const * get_prop_name() const { return "Destruct/Decompose"; }
+public:
+    destruct_trace(unification_constraint const & c):propagation_trace(c) {}
+};
+
+/**
+   \brief Trace object used to justify a normalization step such as.
+
+   <tt>ctx |- (fun x : T, x) a == b</tt>
+   ==>
+   <tt>ctx |- a == b</tt>
+*/
+class normalize_trace : public propagation_trace {
+protected:
+    virtual char const * get_prop_name() const { return "Normalize"; }
+public:
+    normalize_trace(unification_constraint const & c):propagation_trace(c) {}
+};
+
+/**
+   \brief Trace object used to justify a new constraint obtained by substitution.
+*/
+class substitution_trace : public propagation_trace {
+    trace                  m_assignment_trace;
+protected:
+    virtual char const * get_prop_name() const { return "Substitution"; }
+public:
+    substitution_trace(unification_constraint const & c, trace const & t);
+    virtual ~substitution_trace();
+    virtual void get_children(buffer<trace_cell*> & r) const;
+};
+
+/**
+   \brief Trace object used to justify a new constraint obtained by multiple substitution.
+*/
+class multi_substitution_trace : public propagation_trace {
+    std::vector<trace>    m_assignment_traces;
+protected:
+    virtual char const * get_prop_name() const { return "Substitution"; }
+public:
+    multi_substitution_trace(unification_constraint const & c, unsigned num, trace const * ts);
+    virtual ~multi_substitution_trace();
+    virtual void get_children(buffer<trace_cell*> & r) const;
+};
+
+/**
+   \brief Base class for synthesis_failure_trace and synthesized_assignment_trace
+*/
+class synthesis_trace : public trace_cell {
+    context            m_context;
+    expr               m_mvar;
+    expr               m_type;
+    std::vector<trace> m_substitution_traces; // trace objects justifying the assignments used to instantiate \c m_type and \c m_context.
+protected:
+    virtual char const * get_label() const = 0;
+public:
+    synthesis_trace(context const & ctx, expr const & mvar, expr const & type, unsigned num, trace const * substs);
+    virtual ~synthesis_trace();
+    virtual format pp_header(formatter const &, options const &) const;
+    virtual void get_children(buffer<trace_cell*> & r) const;
+    virtual expr const & get_main_expr() const;
+};
+
+/**
+   \brief Trace object for justifying why a synthesis step failed.
+   A synthesis step is of the form
+
+   <tt>ctx |- ?mvar : type</tt>
+
+   Before invoking the synthesizer, the elaborator substitutes the
+   metavariables in \c ctx and \c type with their corresponding assignments.
+*/
+class synthesis_failure_trace : public synthesis_trace {
+    trace              m_trace;  // trace object produced by the synthesizer
+protected:
+    virtual char const * get_label() const;
+public:
+    synthesis_failure_trace(context const & ctx, expr const & mvar, expr const & type, trace const & tr, unsigned num, trace const * substs);
+    virtual ~synthesis_failure_trace();
+    virtual void get_children(buffer<trace_cell*> & r) const;
+};
+
+/**
+   \brief Trace object used to justify a metavar assignment produced by a synthesizer.
+*/
+class synthesized_assignment_trace : public synthesis_trace {
+protected:
+    virtual char const * get_label() const;
+public:
+    synthesized_assignment_trace(context const & ctx, expr const & mvar, expr const & type, unsigned num, trace const * substs):
+        synthesis_trace(ctx, mvar, type, num, substs) {
+    }
+};
+
+/**
+    \brief Trace object used to justify that we are moving to the next solution.
+*/
+class next_solution_trace : public trace_cell {
+    std::vector<trace> m_assumptions; // Set of assumptions used to derive last solution
+public:
+    next_solution_trace(unsigned num, trace const * as);
+    virtual ~next_solution_trace();
+    virtual format pp_header(formatter const &, options const &) const;
+    virtual void get_children(buffer<trace_cell*> & r) const;
+    virtual expr const & get_main_expr() const;
+};
+};

src/util/name.h

@@ -71,6 +71,7 @@ public:
     bool is_anonymous() const { return kind() == name_kind::ANONYMOUS; }
     bool is_string() const    { return kind() == name_kind::STRING; }
     bool is_numeral() const   { return kind() == name_kind::NUMERAL; }
+    operator bool() const     { return !is_anonymous(); }
     unsigned get_numeral() const;
     /**
        \brief If the tail of the given hierarchical name is a string, then it returns this string.
@@ -93,6 +94,10 @@ public:
     friend std::ostream & operator<<(std::ostream & out, name const & n);
     /** \brief Concatenate the two given names. */
     friend name operator+(name const & n1, name const & n2);
+
+    friend void swap(name & a, name & b) {
+        std::swap(a.m_ptr, b.m_ptr);
+    }
 };
 struct name_hash { unsigned operator()(name const & n) const { return n.hash(); } };
 struct name_eq { bool operator()(name const & n1, name const & n2) const { return n1 == n2; } };

src/util/name_generator.h

@@ -23,5 +23,10 @@ public:
 
     /** \brief Return a unique name modulo \c prefix. */
     name next() { name r(m_prefix, m_next_idx); m_next_idx++; return r; }
+
+    friend void swap(name_generator & a, name_generator & b) {
+        swap(a.m_prefix, b.m_prefix);
+        std::swap(a.m_next_idx, b.m_next_idx);
+    }
 };
 }

src/util/splay_map.h

@@ -30,7 +30,7 @@ public:
                                    int>::value,
                       "The return type of CMP()(k1, k2) is not int.");
     }
-    void swap(splay_map & m) { m_map.swap(m.m_map); }
+    friend void swap(splay_map & a, splay_map & b) { swap(a.m_map, b.m_map); }
     bool empty() const { return m_map.empty(); }
     void clear() { m_map.clear(); }
     bool is_eqp(splay_map const & m) const { return m_map.is_eqp(m); }

src/util/splay_tree.h

@@ -328,7 +328,7 @@ public:
     /** \brief O(1) move */
     splay_tree & operator=(splay_tree && s) { LEAN_MOVE_REF(splay_tree, s); }
 
-    void swap(splay_tree & t) { std::swap(m_ptr, t.m_ptr); }
+    friend void swap(splay_tree & t1, splay_tree & t2) { std::swap(t1.m_ptr, t2.m_ptr); }
 
     /** \brief Return true iff this splay tree is empty. */
     bool empty() const { return m_ptr == nullptr; }
@@ -394,16 +394,16 @@ public:
             splay_tree left(*this, m_ptr->m_left);
             splay_tree right(*this, m_ptr->m_right);
             if (left.empty()) {
-                swap(right);
+                swap(*this, right);
             } else if (right.empty()) {
-                swap(left);
+                swap(*this, left);
             } else {
                 clear();
                 left.pull_max();
                 lean_assert(left.m_ptr->m_right == nullptr);
                 right.m_ptr->inc_ref();
                 left.m_ptr->m_right = right.m_ptr;
-                swap(left);
+                swap(*this, left);
             }
         }
     }