From dae86c2ffa52f72d369ef8403d31e5e7372bdfc5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 28 Nov 2013 21:08:12 -0800 Subject: [PATCH] feat(frontends/lean/parser): add basic tactic support in the frontend Signed-off-by: Leonardo de Moura --- src/frontends/lean/frontend_elaborator.cpp | 12 ++- src/frontends/lean/frontend_elaborator.h | 2 +- src/frontends/lean/parser.cpp | 110 ++++++++++++++++++++- src/kernel/context.h | 2 +- src/kernel/metavar.cpp | 2 +- src/library/tactic/goal.cpp | 13 ++- src/library/tactic/proof_state.cpp | 12 +++ src/library/tactic/proof_state.h | 4 + 8 files changed, 140 insertions(+), 17 deletions(-) diff --git a/src/frontends/lean/frontend_elaborator.cpp b/src/frontends/lean/frontend_elaborator.cpp index d1b0eaec6..afe510421 100644 --- a/src/frontends/lean/frontend_elaborator.cpp +++ b/src/frontends/lean/frontend_elaborator.cpp @@ -420,7 +420,7 @@ public: } } - std::pair elaborate(name const & n, expr const & t, expr const & e) { + std::tuple 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 frontend_elaborator::operator()(name const & n, expr const & t, expr const & e) { return m_ptr->elaborate(n, t, e); } +std::tuple 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(); } diff --git a/src/frontends/lean/frontend_elaborator.h b/src/frontends/lean/frontend_elaborator.h index 3f22055c9..c9789d5ff 100644 --- a/src/frontends/lean/frontend_elaborator.h +++ b/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 operator()(name const & n, expr const & t, expr const & e); + std::tuple operator()(name const & n, expr const & t, expr const & e); /** \brief If \c e is an expression instantiated by the elaborator, then it diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 141c71087..55511f982 100644 --- a/src/frontends/lean/parser.cpp +++ b/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 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> 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 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 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 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 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); - expr type = type_val_pair.first; - expr val = type_val_pair.second; + auto r = m_elaborator(id, pre_type, pre_val); + expr type = std::get<0>(r); + 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; diff --git a/src/kernel/context.h b/src/kernel/context.h index 0963e7e91..92058bc4b 100644 --- a/src/kernel/context.h +++ b/src/kernel/context.h @@ -31,11 +31,11 @@ public: */ class context { list m_list; - explicit context(list 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 const & l):m_list(l) {} context_entry const & lookup(unsigned vidx) const; std::pair lookup_ext(unsigned vidx) const; bool empty() const { return is_nil(m_list); } diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp index 3b851d08a..6c23de869 100644 --- a/src/kernel/metavar.cpp +++ b/src/kernel/metavar.cpp @@ -275,7 +275,7 @@ public: }; expr instantiate_metavars(expr const & e, metavar_env const & menv, buffer & jsts) { - if (!has_metavar(e)) { + if (!e || !has_metavar(e)) { return e; } else { return instantiate_metavars_proc(menv, jsts)(e); diff --git a/src/library/tactic/goal.cpp b/src/library/tactic/goal.cpp index a78d59247..92e8cbc47 100644 --- a/src/library/tactic/goal.cpp +++ b/src/library/tactic/goal.cpp @@ -107,7 +107,8 @@ std::pair to_goal(environment const & env, context const & buffer entries; for (auto const & e : ctx) entries.push_back(e); - buffer hypotheses; // normalized names and types of the entries processed so far + std::reverse(entries.begin(), entries.end()); + buffer hypotheses; // normalized names and types of the entries processed so far buffer bodies; // normalized bodies of the entries processed so far std::vector 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 to_goal(environment const & env, context const & return e; }; replace_fn replacer(replace_vars); - auto it = entries.end(); - auto begin = entries.begin(); - while (it != begin) { - --it; + auto it = entries.begin(); + auto end = entries.end(); + for (; it != end; ++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 to_goal(environment const & env, context const & } } expr conclusion = replacer(t); - std::reverse(consts.begin(), consts.end()); - return mk_pair(goal(reverse_to_list(hypotheses.begin(), hypotheses.end()), conclusion), + return mk_pair(goal(to_list(hypotheses.begin(), hypotheses.end()), conclusion), goal_proof_fn(std::move(consts))); } diff --git a/src/library/tactic/proof_state.cpp b/src/library/tactic/proof_state.cpp index 3f6f53473..96821bcc8 100644 --- a/src/library/tactic/proof_state.cpp +++ b/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) { diff --git a/src/library/tactic/proof_state.h b/src/library/tactic/proof_state.h index 2a2e8857b..8bcfeaec8 100644 --- a/src/library/tactic/proof_state.h +++ b/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);