feat(frontends/lean/parser): add basic tactic support in the frontend

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

src/frontends/lean/frontend_elaborator.cpp

@@ -420,7 +420,7 @@ public:
         }
     }
 
-    std::pair<expr, expr> elaborate(name const & n, expr const & t, expr const & e) {
+    std::tuple<expr, expr, metavar_env> elaborate(name const & n, expr const & t, expr const & e) {
         // std::cout << "Elaborate " << t << " : " << e << "\n";
         clear();
         expr new_t = preprocessor(*this)(t);
@@ -436,9 +436,11 @@ public:
             //    std::cout << c.pp(fmt, options(), nullptr, false) << "\n";
             // }
             metavar_env new_menv = elaborate_core();
-            return mk_pair(instantiate_metavars(new_t, new_menv), instantiate_metavars(new_e, new_menv));
+            return std::make_tuple(instantiate_metavars(new_t, new_menv),
+                                   instantiate_metavars(new_e, new_menv),
+                                   new_menv);
         } else {
-            return mk_pair(new_t, new_e);
+            return std::make_tuple(new_t, new_e, metavar_env());
         }
     }
 
@@ -471,7 +473,9 @@ public:
 frontend_elaborator::frontend_elaborator(frontend const & fe):m_ptr(new imp(fe)) {}
 frontend_elaborator::~frontend_elaborator() {}
 expr frontend_elaborator::operator()(expr const & e) { return m_ptr->elaborate(e); }
-std::pair<expr, expr> frontend_elaborator::operator()(name const & n, expr const & t, expr const & e) { return m_ptr->elaborate(n, t, e); }
+std::tuple<expr, expr, metavar_env> frontend_elaborator::operator()(name const & n, expr const & t, expr const & e) {
+    return m_ptr->elaborate(n, t, e);
+}
 expr const & frontend_elaborator::get_original(expr const & e) const { return m_ptr->get_original(e); }
 void frontend_elaborator::clear() { m_ptr->clear(); }
 environment const & frontend_elaborator::get_environment() const { return m_ptr->get_environment(); }

src/frontends/lean/frontend_elaborator.h

@@ -35,7 +35,7 @@ public:
        This information is used by the elaborator. The result is a new
        elaborated type and expression.
     */
-    std::pair<expr, expr> operator()(name const & n, expr const & t, expr const & e);
+    std::tuple<expr, expr, metavar_env> operator()(name const & n, expr const & t, expr const & e);
 
     /**
         \brief If \c e is an expression instantiated by the elaborator, then it

src/frontends/lean/parser.cpp

@@ -30,11 +30,17 @@ Author: Leonardo de Moura
 #include "kernel/kernel_exception.h"
 #include "kernel/expr_maps.h"
 #include "kernel/printer.h"
+#include "kernel/metavar.h"
+#include "kernel/for_each_fn.h"
+#include "library/expr_lt.h"
+#include "library/type_inferer.h"
 #include "library/arith/arith.h"
 #include "library/io_state.h"
 #include "library/placeholder.h"
 #include "library/kernel_bindings.h"
 #include "library/elaborator/elaborator_exception.h"
+#include "library/tactic/proof_state.h"
+#include "library/tactic/tactic.h"
 #include "frontends/lean/frontend.h"
 #include "frontends/lean/frontend_elaborator.h"
 #include "frontends/lean/parser.h"
@@ -85,6 +91,8 @@ static name g_env_kwd("Environment");
 static name g_import_kwd("Import");
 static name g_help_kwd("Help");
 static name g_coercion_kwd("Coercion");
+static name g_apply("apply");
+static name g_done("done");
 /** \brief Table/List with all builtin command keywords */
 static list<name> g_command_keywords = {g_definition_kwd, g_variable_kwd, g_variables_kwd, g_theorem_kwd, g_axiom_kwd, g_universe_kwd, g_eval_kwd,
                                         g_show_kwd, g_check_kwd, g_infix_kwd, g_infixl_kwd, g_infixr_kwd, g_notation_kwd, g_echo_kwd,
@@ -123,6 +131,7 @@ class parser::imp {
     frontend &          m_frontend;
     scanner             m_scanner;
     frontend_elaborator m_elaborator;
+    type_inferer        m_type_inferer;
     scanner::token      m_curr;
     bool                m_use_exceptions;
     bool                m_interactive;
@@ -241,6 +250,8 @@ class parser::imp {
     void check_rcurly_next(char const * msg) { check_next(scanner::token::RightCurlyBracket, msg); }
     /** \brief Throws a parser error if the current token is not ':='. If it is, move to the next token. */
     void check_assign_next(char const * msg) { check_next(scanner::token::Assign, msg); }
+    /** \brief Throws a parser error if the current token is not '.'. If it is, move to the next token. */
+    void check_period_next(char const * msg) { check_next(scanner::token::Period, msg); }
 
     /**
         \brief Throws a parser error if the current token is not a
@@ -1036,6 +1047,90 @@ class parser::imp {
             m_frontend.mark_implicit_arguments(n, imp_args.size(), imp_args.data());
     }
 
+    expr parse_tactic(proof_state s) {
+        proof_state ini = s;
+        std::vector<lazy_list<proof_state>> stack;
+        while (true) {
+            auto p = pos();
+            name id = check_identifier_next("invalid tactic, identifier expected");
+            if (id == g_apply) {
+                auto tac_name_pos = pos();
+                name tac_name = check_identifier_next("invalid apply command, identifier expected");
+                optional<tactic> t;
+                m_script_state->apply([&](lua_State * L) {
+                        lua_getglobal(L, tac_name.to_string().c_str());
+                        if (lua_type(L, -1) != LUA_TFUNCTION && !is_tactic(L, -1))
+                            throw parser_error(sstream() << "unknown tactic '" << tac_name << "'", tac_name_pos);
+                        if (lua_type(L, -1) == LUA_TFUNCTION) {
+                            pcall(L, 0, 1, 0);
+                            if (!is_tactic(L, -1))
+                                throw parser_error(sstream() << "invalid function '" << tac_name << "', it does not return a tactic", tac_name_pos);
+                        }
+                        t = to_tactic(L, -1);
+                        lua_pop(L, 1);
+                    });
+                lazy_list<proof_state> seq = (*t)(m_frontend, m_frontend.get_state(), s);
+                auto r = seq.pull();
+                if (r) {
+                    s = r->first;
+                    stack.push_back(r->second);
+                } else {
+                    diagnostic(m_frontend) << "current state:\n" << s << endl;
+                    throw parser_error(sstream() << "tactic '" << tac_name << "' failed", tac_name_pos);
+                }
+            } else if (id == g_done) {
+                if (s.is_proof_final_state()) {
+                    assignment a(s.get_menv());
+                    proof_map  m;
+                    expr pr = s.get_proof_builder()(m, a);
+                    return pr;
+                } else {
+                    diagnostic(m_frontend) << "final state:\n" << s << endl;
+                    throw exception("failed to synthesize proof object using given tactic");
+                }
+            } else {
+                throw parser_error(sstream() << "invalid tactical proof, unknown command '" << id << "'", p);
+            }
+        }
+    }
+
+    expr parse_tactic(expr const & type, expr const & val, metavar_env & menv) {
+        check_period_next("invalid theorem, '.' expected before tactical proof");
+        if (is_metavar(val)) {
+            // simple case
+            proof_state s = to_proof_state(m_frontend, context(), type);
+            return parse_tactic(s);
+        } else {
+            buffer<expr> mvars;
+            for_each(val, [&](expr const & e, unsigned) {
+                    if (is_metavar(e)) {
+                        mvars.push_back(e);
+                    }
+                    return true;
+                });
+            std::sort(mvars.begin(), mvars.end(), [](expr const & e1, expr const & e2) { return is_lt(e1, e2, false); });
+            for (auto mvar : mvars) {
+                expr    mvar_type = instantiate_metavars(menv.get_type(mvar), menv);
+                if (!m_type_inferer.is_proposition(mvar_type))
+                    throw exception("failed to synthesize metavar, its type is not a proposition");
+                if (has_metavar(mvar_type))
+                    throw exception("failed to synthesize metavar, its type contains metavariables");
+                buffer<context_entry> new_entries;
+                for (auto e : menv.get_context(mvar)) {
+                    new_entries.emplace_back(e.get_name(),
+                                             instantiate_metavars(e.get_domain(), menv),
+                                             instantiate_metavars(e.get_body(), menv));
+                }
+                context mvar_ctx(to_list(new_entries.begin(), new_entries.end()));
+                proof_state s = to_proof_state(m_frontend, mvar_ctx, mvar_type);
+                expr mvar_val = parse_tactic(s);
+                if (mvar_val)
+                    menv.assign(mvar, mvar_val);
+            }
+            return instantiate_metavars(val, menv);
+        }
+    }
+
     /** \brief Auxiliary method used for parsing definitions and theorems. */
     void parse_def_core(bool is_definition) {
         next();
@@ -1062,9 +1157,17 @@ class parser::imp {
             pre_type  = mk_abstraction(false, bindings, type_body);
             pre_val   = mk_abstraction(true, bindings, val_body);
         }
-        auto type_val_pair = m_elaborator(id, pre_type, pre_val);
+        auto r = m_elaborator(id, pre_type, pre_val);
-        expr type = type_val_pair.first;
+        expr type = std::get<0>(r);
-        expr val  = type_val_pair.second;
+        expr val  = std::get<1>(r);
+        metavar_env menv = std::get<2>(r);
+        if (has_metavar(type))
+            throw exception("invalid definition, type still contains metavariables after elaboration");
+        if (!is_definition && has_metavar(val)) {
+            val = parse_tactic(type, val, menv);
+        }
+        if (has_metavar(val))
+            throw exception("invalid definition, value still contains metavariables after elaboration");
         if (is_definition) {
             m_frontend.add_definition(id, type, val);
             if (m_verbose)
@@ -1609,6 +1712,7 @@ public:
         m_frontend(fe),
         m_scanner(in),
         m_elaborator(fe),
+        m_type_inferer(fe),
         m_use_exceptions(use_exceptions),
         m_interactive(interactive) {
         m_script_state = S;

src/kernel/context.h

@@ -31,11 +31,11 @@ public:
 */
 class context {
     list<context_entry> m_list;
-    explicit context(list<context_entry> const & l):m_list(l) {}
 public:
     context() {}
     context(context const & c, name const & n, expr const & d):m_list(context_entry(n, d), c.m_list) {}
     context(context const & c, name const & n, expr const & d, expr const & b):m_list(context_entry(n, d, b), c.m_list) {}
+    explicit context(list<context_entry> const & l):m_list(l) {}
     context_entry const & lookup(unsigned vidx) const;
     std::pair<context_entry const &, context> lookup_ext(unsigned vidx) const;
     bool empty() const { return is_nil(m_list); }

src/kernel/metavar.cpp

@@ -275,7 +275,7 @@ public:
 };
 
 expr instantiate_metavars(expr const & e, metavar_env const & menv, buffer<justification> & jsts) {
-    if (!has_metavar(e)) {
+    if (!e || !has_metavar(e)) {
         return e;
     } else {
         return instantiate_metavars_proc(menv, jsts)(e);

src/library/tactic/goal.cpp

@@ -107,7 +107,8 @@ std::pair<goal, goal_proof_fn> to_goal(environment const & env, context const &
     buffer<context_entry> entries;
     for (auto const & e : ctx)
         entries.push_back(e);
-    buffer<hypothesis> hypotheses;  // normalized names and types of the entries processed so far
+    std::reverse(entries.begin(), entries.end());
+    buffer<hypothesis> hypotheses;             // normalized names and types of the entries processed so far
     buffer<expr> bodies;                       // normalized bodies of the entries processed so far
     std::vector<expr> consts;                  // cached consts[i] == mk_constant(names[i], hypotheses[i])
     auto replace_vars = [&](expr const & e, unsigned offset) -> expr {
@@ -128,10 +129,9 @@ std::pair<goal, goal_proof_fn> to_goal(environment const & env, context const &
         return e;
     };
     replace_fn<decltype(replace_vars)> replacer(replace_vars);
-    auto it    = entries.end();
+    auto it  = entries.begin();
-    auto begin = entries.begin();
+    auto end = entries.end();
-    while (it != begin) {
+    for (; it != end; ++it) {
-        --it;
         auto const & e = *it;
         name n = mk_unique_name(used_names, e.get_name());
         expr d = replacer(e.get_domain());
@@ -148,8 +148,7 @@ std::pair<goal, goal_proof_fn> to_goal(environment const & env, context const &
         }
     }
     expr conclusion = replacer(t);
-    std::reverse(consts.begin(), consts.end());
+    return mk_pair(goal(to_list(hypotheses.begin(), hypotheses.end()), conclusion),
-    return mk_pair(goal(reverse_to_list(hypotheses.begin(), hypotheses.end()), conclusion),
                    goal_proof_fn(std::move(consts)));
 }
 

src/library/tactic/proof_state.cpp

@@ -70,6 +70,18 @@ proof_state to_proof_state(environment const & env, context const & ctx, expr co
     return proof_state(goals(mk_pair(g_main, g)), metavar_env(), pr_builder, cex_builder);
 }
 
+regular const & operator<<(regular const & out, proof_state & s) {
+    options const & opts = out.m_io_state.get_options();
+    out.m_io_state.get_regular_channel().get_stream() << mk_pair(s.pp(out.m_io_state.get_formatter(), opts), opts);
+    return out;
+}
+
+diagnostic const & operator<<(diagnostic const & out, proof_state & s) {
+    options const & opts = out.m_io_state.get_options();
+    out.m_io_state.get_diagnostic_channel().get_stream() << mk_pair(s.pp(out.m_io_state.get_formatter(), opts), opts);
+    return out;
+}
+
 DECL_UDATA(goals)
 
 static int mk_goals(lua_State * L) {

src/library/tactic/proof_state.h

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "util/rc.h"
 #include "util/interrupt.h"
 #include "util/optional.h"
+#include "library/io_state.h"
 #include "library/tactic/goal.h"
 #include "library/tactic/proof_builder.h"
 #include "library/tactic/cex_builder.h"
@@ -97,6 +98,9 @@ goals map_goals(proof_state const & s, F && f) {
         });
 }
 
+regular const & operator<<(regular const & out, proof_state & s);
+diagnostic const & operator<<(diagnostic const & out, proof_state & s);
+
 UDATA_DEFS_CORE(goals)
 UDATA_DEFS(proof_state)
 void open_proof_state(lua_State * L);