refactor(frontends/lean): remove unnecessary code

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

src/frontends/lean/elaborator.cpp

@@ -118,12 +118,11 @@ class elaborator {
     }
 
 public:
-    elaborator(environment const & env, io_state const & ios, name_generator const & ngen,
+    elaborator(environment const & env, io_state const & ios, name_generator const & ngen, pos_info_provider * pp):
-               substitution const & s, context const & ctx, pos_info_provider * pp):
         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(), mk_default_converter(m_env, optional<module_idx>(0))),
-        m_subst(s), m_ctx(ctx), m_pos_provider(pp) {
+        m_pos_provider(pp) {
     }
 
     expr mk_local(name const & n, expr const & t, binder_info const & bi) {
@@ -668,11 +667,11 @@ public:
                     try {
                         proof_state_seq seq = (*t)(m_env, m_ios, ps);
                         if (auto r = seq.pull()) {
-                            subst = r->first.get_subst();
+                            if (!empty(r->first.get_goals())) {
-                            expr v = subst.instantiate_metavars_wo_jst(mvar);
-                            if (has_metavar(v)) {
                                 display_unsolved_proof_state(mvar, r->first, "unsolved subgoals");
                             } else {
+                                subst = r->first.get_subst();
+                                expr v = subst.instantiate_metavars_wo_jst(mvar);
                                 subst = subst.assign(mlocal_name(mvar), v);
                             }
                         } else {
@@ -759,22 +758,12 @@ public:
 
 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<expr> const & ctx, pos_info_provider * pp) {
-    return elaborator(env, ios, ngen, s, ctx, pp)(e);
-}
-
 expr elaborate(environment const & env, io_state const & ios, expr const & e, pos_info_provider * pp) {
-    return elaborate(env, ios, e, name_generator(g_tmp_prefix), substitution(), list<expr>(), pp);
+    return elaborator(env, ios, name_generator(g_tmp_prefix), pp)(e);
 }
 
 std::pair<expr, expr> elaborate(environment const & env, io_state const & ios, name const & n, expr const & t, expr const & v,
                                 pos_info_provider * pp) {
-    return elaborator(env, ios, name_generator(g_tmp_prefix), substitution(), list<expr>(), pp)(t, v, n);
+    return elaborator(env, ios, name_generator(g_tmp_prefix), pp)(t, v, n);
-}
-
-expr elaborate(environment const & env, io_state const & ios, expr const & e, expr const & expected_type, name_generator const & ngen,
-               list<expr> const & ctx, pos_info_provider * pp) {
-    return elaborator(env, ios, ngen, substitution(), ctx, pp)(e, expected_type);
 }
 }

src/frontends/lean/elaborator.h

@@ -12,10 +12,6 @@ Author: Leonardo de Moura
 #include "library/io_state.h"
 
 namespace lean {
-expr elaborate(environment const & env, io_state const & ios, expr const & e, name_generator const & ngen,
-               substitution const & s = substitution(), list<expr> const & ctx = list<expr>(), pos_info_provider * pp = nullptr);
-expr elaborate(environment const & env, io_state const & ios, expr const & e, expr const & expected_type, name_generator const & ngen,
-               list<expr> const & ctx = list<expr>(), pos_info_provider * pp = nullptr);
 expr elaborate(environment const & env, io_state const & ios, expr const & e, pos_info_provider * pp = nullptr);
 std::pair<expr, expr> elaborate(environment const & env, io_state const & ios, name const & n, expr const & t, expr const & v,
                                 pos_info_provider * pp = nullptr);

src/frontends/lean/parser.cpp

@@ -489,11 +489,6 @@ expr parser::elaborate(expr const & e) {
     return ::lean::elaborate(m_env, m_ios, e, &pp);
 }
 
-expr parser::elaborate(expr const & e, name_generator const & ngen, list<expr> const & ctx) {
-    parser_pos_provider pp(m_pos_table, get_stream_name(), m_last_cmd_pos);
-    return ::lean::elaborate(m_env, m_ios, e, ngen, substitution(), ctx, &pp);
-}
-
 expr parser::elaborate(environment const & env, expr const & e) {
     parser_pos_provider pp(m_pos_table, get_stream_name(), m_last_cmd_pos);
     return ::lean::elaborate(env, m_ios, e, &pp);

src/frontends/lean/parser.h

@@ -259,7 +259,6 @@ 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);
-    expr elaborate(expr const & e, name_generator const & ngen, list<expr> const & ctx);
     expr elaborate(environment const & env, expr const & e);
     std::pair<expr, expr> elaborate(name const & n, expr const & t, expr const & v);