feat(frontends/lean): connect new elaborator to frontend

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

src/frontends/lean/builtin_cmds.cpp

@@ -71,7 +71,7 @@ environment end_scoped_cmd(parser & p) {
 environment check_cmd(parser & p) {
     expr e   = p.parse_expr();
     level_param_names ls = to_level_param_names(collect_univ_params(e));
-    e = p.elaborate(e, ls);
+    e = p.elaborate(e);
     expr type = type_checker(p.env()).check(e, ls);
     p.regular_stream() << e << " : " << type << endl;
     return p.env();

src/frontends/lean/calc.cpp

@@ -17,6 +17,7 @@ Author: Leonardo de Moura
 #include "library/module.h"
 #include "library/choice.h"
 #include "library/placeholder.h"
+#include "library/explicit.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/util.h"
 
@@ -212,7 +213,7 @@ static void decode_expr(expr const & e, buffer<calc_pred> & preds, pos_info cons
 
 // Create (op _ _ ... _)
 static expr mk_op_fn(parser & p, name const & op, unsigned num_placeholders, pos_info const & pos) {
-    expr r = p.save_pos(mark_explicit(mk_constant(op)), pos);
+    expr r = p.save_pos(mk_explicit(mk_constant(op)), pos);
     while (num_placeholders > 0) {
         num_placeholders--;
         r = p.mk_app(r, p.save_pos(mk_expr_placeholder(), pos), pos);

src/frontends/lean/decl_cmds.cpp

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "library/aliases.h"
 #include "library/private.h"
 #include "library/locals.h"
+#include "library/explicit.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/util.h"
 
@@ -140,7 +141,7 @@ environment variable_cmd_core(parser & p, bool is_axiom) {
         update_univ_parameters(ls_buffer, collect_univ_params(type), p);
         ls = to_list(ls_buffer.begin(), ls_buffer.end());
     }
-    type = p.elaborate(type, ls);
+    type = p.elaborate(type);
     return declare_var(p, p.env(), n, ls, type, is_axiom, bi, pos);
 }
 environment variable_cmd(parser & p) {
@@ -249,7 +250,7 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque) {
         buffer<expr> section_args;
         for (auto const & p : section_ps)
             section_args.push_back(p.m_local);
-        expr ref = mk_app(mark_explicit(mk_constant(real_n, section_ls)), section_args);
+        expr ref = mk_app(mk_explicit(mk_constant(real_n, section_ls)), section_args);
         p.add_local_expr(n, ref);
     } else {
         if (real_n != n)
@@ -257,12 +258,12 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque) {
     }
     if (is_theorem) {
         // TODO(Leo): delay theorems
-        auto type_value = p.elaborate(type, value, ls);
+        auto type_value = p.elaborate(n, type, value);
         type  = type_value.first;
         value = type_value.second;
         env = module::add(env, check(env, mk_theorem(real_n, ls, type, value)));
     } else {
-        auto type_value = p.elaborate(type, value, ls);
+        auto type_value = p.elaborate(n, type, value);
         type  = type_value.first;
         value = type_value.second;
         env = module::add(env, check(env, mk_definition(env, real_n, ls, type, value, is_opaque)));
@@ -296,7 +297,7 @@ static environment variables_cmd(parser & p) {
     expr type = p.parse_expr();
     parse_close_binder_info(p, bi);
     level_param_names ls = to_level_param_names(collect_univ_params(type));
-    type = p.elaborate(type, ls);
+    type = p.elaborate(type);
     environment env = p.env();
     for (auto id : ids)
         env = declare_var(p, env, id, ls, type, true, bi, pos);

src/frontends/lean/elaborator.cpp

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <vector>
 #include "util/flet.h"
 #include "util/list_fn.h"
+#include "util/lazy_list_fn.h"
 #include "util/sstream.h"
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
@@ -30,39 +31,15 @@ class elaborator {
 
     environment    m_env;
     io_state       m_ios;
-    cache          m_cache;
+    unifier_plugin m_plugin;
     name_generator m_ngen;
     type_checker   m_tc;
     substitution   m_subst;
     context        m_ctx;
+    cache          m_cache;
     justification  m_accumulated; // accumulate justification of eagerly used substitutions
     constraints    m_constraints;
 
-public:
-    elaborator(environment const & env, io_state const & ios, name_generator const & ngen,
-               substitution const & s = substitution(), context const & ctx = context()):
-        m_env(env), m_ios(ios), m_ngen(ngen),
-        m_tc(env, m_ngen.mk_child(), [=](constraint const & c) { add_cnstr(c); }),
-        m_subst(s), m_ctx(ctx) {
-    }
-
-    expr mk_local(name const & n, expr const & t) { return ::lean::mk_local(m_ngen.next(), n, t); }
-    expr infer_type(expr const & e) { return m_tc.infer(e); }
-    expr whnf(expr const & e) { return m_tc.whnf(e); }
-
-    /** \brief Clear constraint buffer \c m_constraints, and associated datastructures
-        \c m_subst and \c m_accumulated.
-
-        \remark \c m_subst contains solutions obtained by eagerly solving the "easy" constraints
-        in \c m_subst, and \c m_accumulated store the justifications of all substitutions eagerly
-        applied.
-    */
-    void clear_constraints() {
-        m_constraints.clear();
-        m_subst = substitution();
-        m_accumulated = justification();
-    }
-
     /**
         \brief Auxiliary object for creating backtracking points.
 
@@ -93,6 +70,71 @@ public:
         }
     };
 
+    struct choice_elaborator {
+        elaborator & m_elab;
+        expr         m_choice;
+        context      m_ctx;
+        substitution m_subst;
+        unsigned     m_idx;
+        choice_elaborator(elaborator & elab, expr const & c, context const & ctx, substitution const & s):
+            m_elab(elab), m_choice(c), m_ctx(ctx), m_subst(s), m_idx(0) {
+        }
+
+        optional<a_choice> next() {
+            while (m_idx < get_num_choices(m_choice)) {
+                expr const & c = get_choice(m_choice, m_idx);
+                m_idx++;
+                try {
+                    scope s(m_elab, m_ctx, m_subst);
+                    expr r = m_elab.visit(c);
+                    justification j = m_elab.m_accumulated;
+                    list<constraint> cs = to_list(m_elab.m_constraints.begin(), m_elab.m_constraints.end());
+                    return optional<a_choice>(r, j, cs);
+                } catch (exception &) {}
+            }
+            return optional<a_choice>();
+        }
+    };
+
+    lazy_list<a_choice> choose(std::shared_ptr<choice_elaborator> const & c) {
+        return mk_lazy_list<a_choice>([=]() {
+                auto s = c->next();
+                if (s)
+                    return some(mk_pair(*s, choose(c)));
+                else
+                    return lazy_list<a_choice>::maybe_pair();
+            });
+    }
+
+public:
+    elaborator(environment const & env, io_state const & ios, name_generator const & ngen,
+               substitution const & s = substitution(), context const & ctx = context()):
+        m_env(env), m_ios(ios),
+        m_plugin([](constraint const &, name_generator const &) { return lazy_list<list<constraint>>(); }),
+        m_ngen(ngen), m_tc(env, m_ngen.mk_child(), [=](constraint const & c) { add_cnstr(c); },
+                           mk_default_converter(m_env, optional<module_idx>(0))),
+        m_subst(s), m_ctx(ctx) {
+    }
+
+    expr mk_local(name const & n, expr const & t) { return ::lean::mk_local(m_ngen.next(), n, t); }
+    expr infer_type(expr const & e) {
+        lean_assert(closed(e));
+        return m_tc.infer(e); }
+    expr whnf(expr const & e) { return m_tc.whnf(e); }
+
+    /** \brief Clear constraint buffer \c m_constraints, and associated datastructures
+        \c m_subst and \c m_accumulated.
+
+        \remark \c m_subst contains solutions obtained by eagerly solving the "easy" constraints
+        in \c m_subst, and \c m_accumulated store the justifications of all substitutions eagerly
+        applied.
+    */
+    void clear_constraints() {
+        m_constraints.clear();
+        m_subst = substitution();
+        m_accumulated = justification();
+    }
+
     void add_cnstr_core(constraint const & c) {
         m_constraints.push_back(c);
     }
@@ -246,10 +288,10 @@ public:
     expr visit_choice(expr const & e, optional<expr> const & t) {
         lean_assert(is_choice(e));
         // Possible optimization: try to lookahead and discard some of the alternatives.
-        expr m  = mk_meta(t, e.get_tag());
+        expr m      = mk_meta(t, e.get_tag());
-        auto choice_fn = [=](expr const &, substitution const & /* s */, name_generator const & /* ngen */) {
+        context ctx = m_ctx;
-            // TODO(Leo)
+        auto choice_fn = [=](expr const & /* t */, substitution const & s, name_generator const & /* ngen */) {
-            return lazy_list<a_choice>();
+            return choose(std::make_shared<choice_elaborator>(*this, e, ctx, s));
         };
         justification j = mk_justification("overloading", some_expr(e));
         add_cnstr(mk_choice_cnstr(m, choice_fn, false, j));
@@ -460,17 +502,85 @@ public:
         if (is_explicit(e)) {
             r    = visit_core(get_explicit_arg(e));
         } else {
-            tag  g      = e.get_tag();
+            r    = visit_core(e);
-            expr r_type = whnf(infer_type(r));
+            if (!is_lambda(r)) {
-            expr imp_arg;
+                tag  g      = e.get_tag();
-            while (is_pi(r_type) && binding_info(r_type).is_implicit()) {
+                expr r_type = whnf(infer_type(r));
-                imp_arg = mk_meta(some_expr(binding_domain(r_type)), g);
+                expr imp_arg;
-                r       = mk_app(r, imp_arg, g);
+                while (is_pi(r_type) && binding_info(r_type).is_implicit()) {
-                r_type  = whnf(instantiate(binding_body(r_type), imp_arg));
+                    imp_arg = mk_meta(some_expr(binding_domain(r_type)), g);
+                    r       = mk_app(r, imp_arg, g);
+                    r_type  = whnf(instantiate(binding_body(r_type), imp_arg));
+                }
             }
         }
         m_cache.insert(e, r);
         return r;
     }
+
+    lazy_list<substitution> solve() {
+        buffer<constraint> cs;
+        cs.append(m_constraints);
+        m_constraints.clear();
+        // for (auto c : cs) { std::cout << "   " << c << "\n"; }
+        return unify(m_env, cs.size(), cs.data(), m_ngen.mk_child(), m_plugin,
+                     true, get_unifier_max_steps(m_ios.get_options()));
+    }
+
+    expr operator()(expr const & e) {
+        // std::cout << "e: " << e << "\n";
+        expr r  = visit(e);
+        auto p  = solve().pull();
+        lean_assert(p);
+        // std::cout << "r: " << r << "\n";
+        substitution s = p->first;
+        // std::cout << "sol: " << s.instantiate_metavars_wo_jst(r) << "\n";
+        return s.instantiate_metavars_wo_jst(r);
+    }
+
+    std::pair<expr, expr> operator()(expr const & t, expr const & v, name const & n) {
+        // std::cout << "t:   " << t   << "\n";
+        // std::cout << "v:   " << v   << "\n";
+        expr r_t      = visit(t);
+        // std::cout << "r_t: " << r_t << "\n";
+        expr r_v      = visit(v);
+        // std::cout << "r_v: " << r_v << "\n";
+        expr r_v_type = infer_type(r_v);
+        environment env = m_env;
+        justification j = mk_justification(v, [=](formatter const & fmt, options const & o, substitution const & subst) {
+                return pp_def_type_mismatch(fmt, env, o, n,
+                                            subst.instantiate_metavars_wo_jst(r_t),
+                                            subst.instantiate_metavars_wo_jst(r_v_type));
+            });
+        if (!m_tc.is_def_eq(r_v_type, r_t, j)) {
+            throw_kernel_exception(env, v,
+                                   [=](formatter const & fmt, options const & o) {
+                                       return pp_def_type_mismatch(fmt, env, o, n, r_t, r_v_type);
+                                   });
+        }
+
+        auto p  = solve().pull();
+        lean_assert(p);
+        substitution s = p->first;
+        // std::cout << "sol: " << s.instantiate_metavars_wo_jst(r_t) << "\n";
+        // std::cout << "     " << s.instantiate_metavars_wo_jst(r_v) << "\n";
+        return mk_pair(s.instantiate_metavars_wo_jst(r_t),
+                       s.instantiate_metavars_wo_jst(r_v));
+    }
 };
+
+static name g_tmp_prefix = name::mk_internal_unique_name();
+
+expr elaborate(environment const & env, io_state const & ios, expr const & e, name_generator const & ngen,
+               substitution const & s, list<parameter> const & ctx) {
+    return elaborator(env, ios, ngen, s, ctx)(e);
+}
+
+expr elaborate(environment const & env, io_state const & ios, expr const & e) {
+    return elaborate(env, ios, e, name_generator(g_tmp_prefix), substitution(), list<parameter>());
+}
+
+std::pair<expr, expr> elaborate(environment const & env, io_state const & ios, name const & n, expr const & t, expr const & v) {
+    return elaborator(env, ios, name_generator(g_tmp_prefix))(t, v, n);
+}
 }

src/frontends/lean/inductive_cmd.cpp

@@ -14,6 +14,7 @@ Author: Leonardo de Moura
 #include "library/locals.h"
 #include "library/placeholder.h"
 #include "library/aliases.h"
+#include "library/explicit.h"
 #include "frontends/lean/decl_cmds.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/parser.h"
@@ -161,7 +162,7 @@ static void set_result_universes(buffer<inductive_decl> & decls, level_param_nam
 static environment create_alias(environment const & env, name const & full_id, name const & id, levels const & section_leves,
                                 buffer<parameter> const & section_params, parser & p) {
     if (in_section(env)) {
-        expr r = mark_explicit(mk_constant(full_id, section_leves));
+        expr r = mk_explicit(mk_constant(full_id, section_leves));
         for (unsigned i = 0; i < section_params.size(); i++)
             r = mk_app(r, section_params[i].m_local);
         p.add_local_expr(id, r);

src/frontends/lean/parser.cpp

@@ -28,6 +28,7 @@ Author: Leonardo de Moura
 #include "library/error_handling/error_handling.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/notation_cmd.h"
+#include "frontends/lean/elaborator.h"
 
 #ifndef LEAN_DEFAULT_PARSER_SHOW_ERRORS
 #define LEAN_DEFAULT_PARSER_SHOW_ERRORS true
@@ -542,13 +543,12 @@ expr parser::mk_Type() {
     }
 }
 
-expr parser::elaborate(expr const & e, level_param_names const &) {
+expr parser::elaborate(expr const & e) {
-    // TODO(Leo):
+    return ::lean::elaborate(m_env, m_ios, e);
-    return e;
 }
 
-std::pair<expr, expr> parser::elaborate(expr const & t, expr const & v, level_param_names const &) {
+std::pair<expr, expr> parser::elaborate(name const & n, expr const & t, expr const & v) {
-    return mk_pair(t, v);
+    return ::lean::elaborate(m_env, m_ios, n, t, v);
 }
 
 /** \brief Parse <tt>ID ':' expr</tt>, where the expression represents the type of the identifier. */

src/frontends/lean/parser.h

@@ -262,8 +262,8 @@ public:
     */
     struct no_undef_id_error_scope { parser & m_p; bool m_old; no_undef_id_error_scope(parser &); ~no_undef_id_error_scope(); };
 
-    expr elaborate(expr const & e, level_param_names const &);
+    expr elaborate(expr const & e);
-    std::pair<expr, expr> elaborate(expr const & t, expr const & v, level_param_names const &);
+    std::pair<expr, expr> elaborate(name const & n, expr const & t, expr const & v);
 
     /** parse all commands in the input stream */
     bool operator()() { return parse_commands(); }

src/frontends/lean/util.cpp

@@ -18,11 +18,4 @@ void check_in_section(parser const & p) {
     if (!in_section(p.env()))
         throw exception(sstream() << "invalid command, it must be used in a section");
 }
-
-// Wrap \c e with the "explicit macro", the idea is to inform the elaborator
-// preprocessor, that we do not need create metavariables for implicit arguments
-expr mark_explicit(expr const & e) {
-    // TODO(Leo)
-    return e;
-}
 }

src/frontends/lean/util.h

@@ -10,5 +10,4 @@ namespace lean {
 class parser;
 void check_atomic(name const & n);
 void check_in_section(parser const & p);
-expr mark_explicit(expr const & e);
 }

src/library/unifier.h

@@ -20,6 +20,9 @@ Author: Leonardo de Moura
 #endif
 
 namespace lean {
+unsigned get_unifier_max_steps(options const & opts);
+bool get_unifier_use_exceptions(options const & opts);
+
 enum class unify_status { Solved, Failed, Unsupported };
 /**
     \brief Handle the easy-cases: first-order unification, higher-order patterns, identical terms, and terms without metavariables.

tests/lean/calc1.lean.expected.out

@@ -1,4 +1,4 @@
 le_eq_trans a d e (le_trans a c d (eq_le_trans a b c H1 H2) H3) H4 : le a e
 calc1.lean:38:10: error: invalid 'calc' expression, transitivity rule is not defined for current step
 le_lt_trans b c d H2 H5 : lt b d
-choice (le2_trans b d e (le2_trans b c d H2 H3) H4) (le_trans b d e (le_trans b c d H2 H3) H4)
+choice ((@ le2_trans) b d e ((@ le2_trans) b c d H2 H3) H4) ((@ le_trans) b d e ((@ le_trans) b c d H2 H3) H4)

tests/lean/run/e1.lean

@@ -0,0 +1,15 @@
+definition Bool [inline] : Type.{1} := Type.{0}
+variable eq : forall {A : Type}, A → A → Bool
+variable N : Type.{1}
+variables a b c : N
+infix `=` 50 := eq
+check a = b
+
+variable f : Bool → N → N
+variable g : N → N → N
+precedence `+`:50
+infixl + := f
+infixl + := g
+check a + b + c
+variable p : Bool
+check p + a + b + c

tests/lean/t6.lean.expected.out

@@ -1,3 +1,3 @@
-id.{2} : Pi {A : Type.{2}} (a : A), A
+id.{2} ?2.1 : ?2.1 -> ?2.1
-refl.{1} : Pi {A : Type} (R : A -> A -> Bool), Bool
+refl.{1} ?2.1 : (?2.1 -> ?2.1 -> Bool) -> Bool
-symm.{1} : Pi {A : Type} (R : A -> A -> Bool), Bool
+symm.{1} ?2.1 : (?2.1 -> ?2.1 -> Bool) -> Bool

tests/lean/t7.lean.expected.out

@@ -1,5 +1,5 @@
-id.{2} : Pi {A : Type.{2}} (a : A), A
+id.{2} ?2.1 : ?2.1 -> ?2.1
-trans.{1} : Pi {A : Type} (R : A -> A -> Bool), Bool
+trans.{1} ?2.1 : (?2.1 -> ?2.1 -> Bool) -> Bool
-symm.{1} : Pi {A : Type} (R : A -> A -> Bool), Bool
+symm.{1} ?2.1 : (?2.1 -> ?2.1 -> Bool) -> Bool
-equivalence.{1} : Pi {A : Type} (R : A -> A -> Bool), Bool
+equivalence.{1} ?2.1 : (?2.1 -> ?2.1 -> Bool) -> Bool
 fun {A : Type.{l_1}} (R : A -> A -> Bool), (and (and (private.3808308840.refl.{l_1} A R) (symm.{l_1} A R)) (trans.{l_1} A R))