diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index fa3282552..be66b5881 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -1,6 +1,6 @@ -add_library(tactic goal.cpp cex_builder.cpp proof_builder.cpp) +add_library(tactic goal.cpp cex_builder.cpp proof_builder.cpp proof_state.cpp) -# proof_state.cpp tactic.cpp apply_tactic.cpp +# tactic.cpp apply_tactic.cpp # simplify_tactic.cpp) target_link_libraries(tactic ${LEAN_LIBS}) diff --git a/src/library/tactic/proof_builder.h b/src/library/tactic/proof_builder.h index 9f6379e6d..c2c8318bb 100644 --- a/src/library/tactic/proof_builder.h +++ b/src/library/tactic/proof_builder.h @@ -28,5 +28,6 @@ proof_builder_fn add_proofs(proof_builder_fn const & pb, list #include "util/sstream.h" -#include "kernel/kernel.h" +#include "util/interrupt.h" #include "kernel/type_checker.h" +#include "kernel/instantiate.h" +#include "kernel/abstract.h" #include "library/io_state_stream.h" #include "library/kernel_bindings.h" #include "library/tactic/proof_state.h" @@ -16,18 +18,25 @@ Author: Leonardo de Moura #define LEAN_PROOF_STATE_GOAL_NAMES false #endif +#ifndef LEAN_PROOF_STATE_MINIMIZE_CONTEXTUAL +#define LEAN_PROOF_STATE_MINIMIZE_CONTEXTUAL true +#endif + namespace lean { -static name g_proof_state_goal_names {"tactic", "proof_state", "goal_names"}; +static name g_proof_state_goal_names {"tactic", "goal_names"}; +static name g_proof_state_minimize_contextual {"tactic", "mimimize_contextual"}; RegisterBoolOption(g_proof_state_goal_names, LEAN_PROOF_STATE_GOAL_NAMES, "(tactic) display goal names when pretty printing proof state"); -bool get_proof_state_goal_names(options const & opts) { - return opts.get_bool(g_proof_state_goal_names, LEAN_PROOF_STATE_GOAL_NAMES); +RegisterBoolOption(g_proof_state_minimize_contextual, LEAN_PROOF_STATE_MINIMIZE_CONTEXTUAL, + "(tactic) only hypotheses, that are not propositions, are marked as 'contextual'"); +bool get_proof_state_goal_names(options const & opts) { return opts.get_bool(g_proof_state_goal_names, LEAN_PROOF_STATE_GOAL_NAMES); } +bool get_proof_state_minimize_contextual(options const & opts) { + return opts.get_bool(g_proof_state_minimize_contextual, LEAN_PROOF_STATE_MINIMIZE_CONTEXTUAL); } optional get_ith_goal_name(goals const & gs, unsigned i) { unsigned j = 1; for (auto const & p : gs) { - if (i == j) - return some(p.first); + if (i == j) return some(p.first); j++; } return optional(); @@ -40,125 +49,120 @@ precision mk_union(precision p1, precision p2) { else return precision::UnderOver; } -bool trust_proof(precision p) { - return p == precision::Precise || p == precision::Over; -} +bool trust_proof(precision p) { return p == precision::Precise || p == precision::Over; } +bool trust_cex(precision p) { return p == precision::Precise || p == precision::Under; } -bool trust_cex(precision p) { - return p == precision::Precise || p == precision::Under; -} - -format proof_state::pp(formatter const & fmt, options const & opts) const { +format proof_state::pp(environment const & env, formatter const & fmt, options const & opts) const { bool show_goal_names = get_proof_state_goal_names(opts); unsigned indent = get_pp_indent(opts); format r; bool first = true; for (auto const & p : get_goals()) { - if (first) - first = false; - else - r += line(); + if (first) first = false; else r += line(); if (show_goal_names) { - r += group(format{format(p.first), colon(), nest(indent, compose(line(), p.second.pp(fmt, opts)))}); + r += group(format{format(p.first), colon(), nest(indent, compose(line(), p.second.pp(env, fmt, opts)))}); } else { - r += p.second.pp(fmt, opts); + r += p.second.pp(env, fmt, opts); } } - if (first) { - r = format("no goals"); - } + if (first) r = format("no goals"); return r; } +goals map_goals(proof_state const & s, std::function(name const & gn, goal const & g)> const & f) { + return map_filter(s.get_goals(), [=](std::pair const & in, std::pair & out) -> bool { + check_interrupted(); + optional new_goal = f(in.first, in.second); + if (new_goal) { + out.first = in.first; + out.second = *new_goal; + return true; + } else { + return false; + } + }); +} + bool proof_state::is_proof_final_state() const { return empty(get_goals()) && trust_proof(get_precision()); } -bool proof_state::is_cex_final_state() const { - if (length(get_goals()) == 1 && trust_cex(get_precision())) { - goal const & g = head(get_goals()).second; - return is_false(g.get_conclusion()) && empty(g.get_hypotheses()); - } else { - return false; - } -} - void proof_state::get_goal_names(name_set & r) const { - for (auto const & p : get_goals()) { + for (auto const & p : get_goals()) r.insert(p.first); - } -} - -name arg_to_hypothesis_name(name const & n, expr const & d, ro_environment const & env, context const & ctx, optional const & menv) { - if (is_default_arrow_var_name(n) && is_proposition(d, env, ctx, to_ro_menv(menv))) - return name("H"); - else - return n; } static name g_main("main"); - -proof_state to_proof_state(ro_environment const & env, context ctx, expr t) { - list> extra_binders; - while (is_pi(t)) { - name vname = arg_to_hypothesis_name(abst_name(t), abst_domain(t), env, ctx); - extra_binders.emplace_front(vname, abst_domain(t)); - ctx = extend(ctx, vname, abst_domain(t)); - t = abst_body(t); - } - auto gfn = to_goal(env, ctx, t); - goal g = gfn.first; - goal_proof_fn fn = gfn.second; - proof_builder pr_builder = mk_proof_builder( - [=](proof_map const & m, assignment const &) -> expr { - expr pr = fn(find(m, g_main)); - for (auto p : extra_binders) - pr = mk_lambda(p.first, p.second, pr); - return pr; +proof_builder_fn mk_init_proof_builder(list const & locals) { + return proof_builder_fn([=](proof_map const & m, substitution const &) -> expr { + expr r = find(m, g_main); + for (expr const & l : locals) + r = Fun(l, r); + return r; }); - cex_builder cex_builder = mk_cex_builder_for(g_main); - return proof_state(goals(mk_pair(g_main, g)), metavar_env(), pr_builder, cex_builder); +} + +static proof_state to_proof_state(environment const * env, expr const & mvar, name_generator ngen) { + if (!is_metavar(mvar)) + throw exception("invalid 'to_proof_state', argument is not a metavariable"); + optional tc; + if (env) + tc.emplace(*env, ngen.mk_child()); + expr t = mlocal_type(mvar); + list init_ls; + hypotheses hs; + while (is_pi(t)) { + expr l = mk_local(ngen.next(), binding_name(t), binding_domain(t)); + bool c = true; + if (tc) + c = !tc->is_prop(binding_domain(t)); + hs = hypotheses(hypothesis(l, c), hs); + t = instantiate(binding_body(t), l); + init_ls = list(l, init_ls); + } + goals gs(mk_pair(g_main, goal(hs, t))); + return proof_state(gs, mk_init_proof_builder(init_ls), mk_cex_builder_for(g_main), ngen, init_ls); +} + +static name g_tmp_prefix = name::mk_internal_unique_name(); +proof_state to_proof_state(expr const & mvar, name_generator const & ngen) { return to_proof_state(nullptr, mvar, ngen); } +proof_state to_proof_state(expr const & mvar) { return to_proof_state(mvar, name_generator(g_tmp_prefix)); } +proof_state to_proof_state(environment const & env, expr const & mvar, name_generator const & ngen, options const & opts) { + bool min_ctx = get_proof_state_minimize_contextual(opts) && env.impredicative(); + if (!min_ctx) + return to_proof_state(mvar, ngen); + else + return to_proof_state(&env, mvar, ngen); +} +proof_state to_proof_state(environment const & env, expr const & meta, options const & opts) { + return to_proof_state(env, meta, name_generator(g_tmp_prefix), opts); } io_state_stream const & operator<<(io_state_stream const & out, proof_state & s) { options const & opts = out.get_options(); - out.get_stream() << mk_pair(s.pp(out.get_formatter(), opts), opts); + out.get_stream() << mk_pair(s.pp(out.get_environment(), out.get_formatter(), opts), opts); return out; } DECL_UDATA(goals) static int mk_goals(lua_State * L) { - int nargs = lua_gettop(L); - if (nargs == 0) { - return push_goals(L, goals()); - } else if (nargs == 1) { - // convert a Lua table of the form {{n_1, g_1}, ..., {n_n, g_n}} into a goal list - goals gs; - int len = objlen(L, 1); - for (int i = len; i >= 1; i--) { - lua_pushinteger(L, i); - lua_gettable(L, 1); // now table {n_i, g_i} is on the top - if (!lua_istable(L, -1) || objlen(L, -1) != 2) - throw exception("arg #1 must be of the form '{{name, goal}, ...}'"); - lua_pushinteger(L, 1); - lua_gettable(L, -2); - name n_i = to_name_ext(L, -1); - lua_pop(L, 1); // remove n_i from the stack - lua_pushinteger(L, 2); - lua_gettable(L, -2); - goal g_i = to_goal(L, -1); - lua_pop(L, 2); // remove the g_i and table {n_i, g_i} from the stack - gs = goals(mk_pair(n_i, g_i), gs); - } - return push_goals(L, gs); - } else if (nargs == 2) { - return push_goals(L, goals(mk_pair(to_name_ext(L, 1), to_goal(L, 2)), goals())); - } else if (nargs == 3) { - return push_goals(L, goals(mk_pair(to_name_ext(L, 1), to_goal(L, 2)), to_goals(L, 3))); - } else { - throw exception("goals functions expects 0 (empty list), 2 (name & goal for singleton goal list), or 3 (name & goal & goal list) arguments"); + int i = lua_gettop(L); + goals r; + if (i > 0 && is_goals(L, i)) { + r = to_goals(L, i); + i--; } + while (i > 0) { + lua_rawgeti(L, i, 1); + lua_rawgeti(L, i, 2); + if (!(lua_isstring(L, -2) || is_name(L, -2)) || !is_goal(L, -1)) + throw exception(sstream() << "arg #" << i << " must be a pair: name, goal"); + r = goals(mk_pair(to_name_ext(L, -2), to_goal(L, -1)), r); + lua_pop(L, 2); + i--; + } + return push_goals(L, r); } static int goals_is_nil(lua_State * L) { @@ -225,76 +229,65 @@ DECL_UDATA(proof_state) static int mk_proof_state(lua_State * L) { int nargs = lua_gettop(L); - if (nargs == 0) { - return push_proof_state(L, proof_state()); - } else if (nargs == 4) { - return push_proof_state(L, proof_state(to_goals(L, 1), to_metavar_env(L, 2), to_proof_builder(L, 3), to_cex_builder(L, 4))); + if (nargs == 2) { + return push_proof_state(L, proof_state(to_proof_state(L, 1), to_goals(L, 2))); } else if (nargs == 3) { return push_proof_state(L, proof_state(to_proof_state(L, 1), to_goals(L, 2), to_proof_builder(L, 3))); + } else if (nargs == 4) { + return push_proof_state(L, proof_state(to_proof_state(L, 1), to_goals(L, 2), to_proof_builder(L, 3), to_name_generator(L, 4))); } else { - throw exception("proof_state expectes 0, 3, or 4 arguments"); + throw exception("proof_state invalid number of arguments"); } } static int to_proof_state(lua_State * L) { - return push_proof_state(L, to_proof_state(to_environment(L, 1), to_context(L, 2), to_expr(L, 3))); + int nargs = lua_gettop(L); + if (nargs == 1) + return push_proof_state(L, to_proof_state(to_expr(L, 1))); + else if (nargs == 2 && is_expr(L, 1)) + return push_proof_state(L, to_proof_state(to_expr(L, 1), to_name_generator(L, 2))); + else if (nargs == 2) + return push_proof_state(L, to_proof_state(to_environment(L, 1), to_expr(L, 2))); + else if (nargs == 3) + return push_proof_state(L, to_proof_state(to_environment(L, 1), to_expr(L, 2), to_options(L, 3))); + else + return push_proof_state(L, to_proof_state(to_environment(L, 1), to_expr(L, 2), to_name_generator(L, 3), to_options(L, 4))); } static int proof_state_tostring(lua_State * L) { std::ostringstream out; proof_state & s = to_proof_state(L, 1); - formatter fmt = get_global_formatter(L); - options opts = get_global_options(L); - out << mk_pair(s.pp(fmt, opts), opts); + environment env = get_global_environment(L); + formatter fmt = get_global_formatter(L); + options opts = get_global_options(L); + out << mk_pair(s.pp(env, fmt, opts), opts); lua_pushstring(L, out.str().c_str()); return 1; } -static int proof_state_get_precision(lua_State * L) { - lua_pushinteger(L, static_cast(to_proof_state(L, 1).get_precision())); - return 1; +static int proof_state_get_precision(lua_State * L) { return push_integer(L, static_cast(to_proof_state(L, 1).get_precision())); } +static int proof_state_get_goals(lua_State * L) { return push_goals(L, to_proof_state(L, 1).get_goals()); } +static int proof_state_apply_proof_builder(lua_State * L) { + return push_expr(L, to_proof_state(L, 1).get_pb()(to_proof_map(L, 2), to_substitution(L, 3))); } - -static int proof_state_get_goals(lua_State * L) { - return push_goals(L, to_proof_state(L, 1).get_goals()); +static int proof_state_apply_cex_builder(lua_State * L) { + optional cex; + if (!lua_isnil(L, 3)) + cex = to_environment(L, 3); + return push_environment(L, to_proof_state(L, 1).get_cb()(to_name_ext(L, 2), cex, to_substitution(L, 4))); } - -static int proof_state_get_menv(lua_State * L) { - // Remark: I use copy to make sure Lua code cannot change the metavar_env in the proof_state - return push_metavar_env(L, to_proof_state(L, 1).get_menv().copy()); -} - -static int proof_state_get_proof_builder(lua_State * L) { - return push_proof_builder(L, to_proof_state(L, 1).get_proof_builder()); -} - -static int proof_state_get_cex_builder(lua_State * L) { - return push_cex_builder(L, to_proof_state(L, 1).get_cex_builder()); -} - -static int proof_state_is_proof_final_state(lua_State * L) { - lua_pushboolean(L, to_proof_state(L, 1).is_proof_final_state()); - return 1; -} - -static int proof_state_is_cex_final_state(lua_State * L) { - lua_pushboolean(L, to_proof_state(L, 1).is_cex_final_state()); - return 1; -} - +static int proof_state_is_proof_final_state(lua_State * L) { return push_boolean(L, to_proof_state(L, 1).is_proof_final_state()); } static int proof_state_pp(lua_State * L) { int nargs = lua_gettop(L); proof_state & s = to_proof_state(L, 1); - if (nargs == 1) { - return push_format(L, s.pp(get_global_formatter(L), get_global_options(L))); - } else if (nargs == 2) { - if (is_formatter(L, 2)) - return push_format(L, s.pp(to_formatter(L, 2), get_global_options(L))); - else - return push_format(L, s.pp(get_global_formatter(L), to_options(L, 2))); - } else { - return push_format(L, s.pp(to_formatter(L, 2), to_options(L, 3))); - } + if (nargs == 1) + return push_format(L, s.pp(get_global_environment(L), get_global_formatter(L), get_global_options(L))); + else if (nargs == 2) + return push_format(L, s.pp(to_environment(L, 2), get_global_formatter(L), get_global_options(L))); + else if (nargs == 3) + return push_format(L, s.pp(to_environment(L, 2), to_formatter(L, 3), get_global_options(L))); + else + return push_format(L, s.pp(to_environment(L, 2), to_formatter(L, 3), to_options(L, 4))); } static const struct luaL_Reg proof_state_m[] = { @@ -303,16 +296,11 @@ static const struct luaL_Reg proof_state_m[] = { {"pp", safe_function}, {"get_precision", safe_function}, {"get_goals", safe_function}, - {"get_menv", safe_function}, - {"get_proof_builder", safe_function}, - {"get_cex_builder", safe_function}, + {"pb", safe_function}, + {"cb", safe_function}, {"precision", safe_function}, {"goals", safe_function}, - {"menv", safe_function}, - {"proof_builder", safe_function}, - {"cex_builder", safe_function}, {"is_proof_final_state", safe_function}, - {"is_cex_final_state", safe_function}, {0, 0} }; diff --git a/src/library/tactic/proof_state.h b/src/library/tactic/proof_state.h index 583de731e..3a745dc90 100644 --- a/src/library/tactic/proof_state.h +++ b/src/library/tactic/proof_state.h @@ -1,5 +1,5 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura @@ -8,22 +8,15 @@ Author: Leonardo de Moura #include #include #include "util/lua.h" -#include "util/rc.h" -#include "util/interrupt.h" #include "util/optional.h" #include "util/name_set.h" -#include "kernel/io_state.h" #include "library/tactic/goal.h" #include "library/tactic/proof_builder.h" #include "library/tactic/cex_builder.h" namespace lean { typedef list> goals; -/** - \brief Return the name of the i-th goal. - - \remark Return none if i == 0 or i > size(g) -*/ +/** \brief Return the name of the i-th goal, return none if i == 0 or i > size(g) */ optional get_ith_goal_name(goals const & gs, unsigned i); enum class precision { @@ -38,97 +31,52 @@ bool trust_proof(precision p); bool trust_cex(precision p); class proof_state { - struct cell { - MK_LEAN_RC(); - precision m_precision; - goals m_goals; - ro_metavar_env m_menv; - proof_builder m_proof_builder; - cex_builder m_cex_builder; - void dealloc() { delete this; } - cell():m_rc(1) {} - cell(precision prec, goals const & gs, ro_metavar_env const & menv, proof_builder const & p, cex_builder const & c): - m_rc(1), m_precision(prec), m_goals(gs), m_menv(menv), m_proof_builder(p), m_cex_builder(c) {} - cell(goals const & gs, ro_metavar_env const & menv, proof_builder const & p, cex_builder const & c): - m_rc(1), m_precision(precision::Precise), m_goals(gs), m_menv(menv), m_proof_builder(p), m_cex_builder(c) {} - }; - cell * m_ptr; + precision m_precision; + goals m_goals; + proof_builder_fn m_proof_builder; + cex_builder_fn m_cex_builder; + name_generator m_ngen; + list m_init_locals; public: - proof_state():m_ptr(new cell()) {} - proof_state(proof_state const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); } - proof_state(proof_state && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; } - proof_state(goals const & gs, ro_metavar_env const & menv, proof_builder const & p, cex_builder const & c): - m_ptr(new cell(gs, menv, p, c)) {} - proof_state(precision prec, goals const & gs, ro_metavar_env const & menv, proof_builder const & p, cex_builder const & c): - m_ptr(new cell(prec, gs, menv, p, c)) {} - proof_state(proof_state const & s, goals const & gs, proof_builder const & p): - m_ptr(new cell(s.get_precision(), gs, s.m_ptr->m_menv, p, s.get_cex_builder())) {} - proof_state(proof_state const & s, goals const & gs): - m_ptr(new cell(s.get_precision(), gs, s.m_ptr->m_menv, s.get_proof_builder(), s.get_cex_builder())) {} - proof_state(proof_state const & s, goals const & gs, proof_builder const & p, cex_builder const & c): - m_ptr(new cell(s.get_precision(), gs, s.m_ptr->m_menv, p, c)) {} - ~proof_state() { if (m_ptr) m_ptr->dec_ref(); } - friend void swap(proof_state & a, proof_state & b) { std::swap(a.m_ptr, b.m_ptr); } - proof_state & operator=(proof_state const & s) { LEAN_COPY_REF(s); } - proof_state & operator=(proof_state && s) { LEAN_MOVE_REF(s); } - precision get_precision() const { lean_assert(m_ptr); return m_ptr->m_precision; } - goals const & get_goals() const { lean_assert(m_ptr); return m_ptr->m_goals; } - ro_metavar_env const & get_menv() const { lean_assert(m_ptr); return m_ptr->m_menv; } - proof_builder const & get_proof_builder() const { lean_assert(m_ptr); return m_ptr->m_proof_builder; } - cex_builder const & get_cex_builder() const { lean_assert(m_ptr); return m_ptr->m_cex_builder; } - /** - \brief Return true iff this state does not have any goals left, and - the precision is \c Precise or \c Over - */ + proof_state(precision prec, goals const & gs, proof_builder_fn const & pb, cex_builder_fn const & cb, + name_generator const & ngen, list const & ls = list()): + m_precision(prec), m_goals(gs), m_proof_builder(pb), m_cex_builder(cb), m_ngen(ngen), m_init_locals(ls) {} + proof_state(goals const & gs, proof_builder_fn const & pb, cex_builder_fn const & cb, + name_generator const & ngen, list const & ls = list()): + proof_state(precision::Precise, gs, pb, cb, ngen, ls) {} + proof_state(proof_state const & s, goals const & gs, proof_builder_fn const & pb, name_generator const & ngen): + proof_state(s.m_precision, gs, pb, s.m_cex_builder, ngen, s.m_init_locals) {} + proof_state(proof_state const & s, goals const & gs, proof_builder_fn const & pb):proof_state(s, gs, pb, s.m_ngen) {} + proof_state(proof_state const & s, goals const & gs):proof_state(s, gs, s.m_proof_builder) {} + precision get_precision() const { return m_precision; } + goals const & get_goals() const { return m_goals; } + proof_builder_fn const & get_pb() const { return m_proof_builder; } + cex_builder_fn const & get_cb() const { return m_cex_builder; } + name_generator const & ngen() const { return m_ngen; } + list const & get_init_locals() const { return m_init_locals; } + /** \brief Return true iff this state does not have any goals left, and the precision is \c Precise or \c Over */ bool is_proof_final_state() const; - /** - \brief Return true iff this state has only one goal of the form |- false, - and the precision is \c Precise or \c Under - */ - bool is_cex_final_state() const; - /** - \brief Store in \c r the goal names - */ + /** \brief Store in \c r the goal names */ void get_goal_names(name_set & r) const; - optional get_ith_goal_name(unsigned i) const { return ::lean::get_ith_goal_name(get_goals(), i); } - - format pp(formatter const & fmt, options const & opts) const; + format pp(environment const & env, formatter const & fmt, options const & opts) const; }; -proof_state to_proof_state(ro_environment const & env, context ctx, expr t); - -inline optional some_proof_state(proof_state const & s, goals const & gs, proof_builder const & p) { - return some(proof_state(s, gs, p)); -} +inline optional some_proof_state(proof_state const & s) { return some(s); } inline optional none_proof_state() { return optional (); } -template -goals map_goals(proof_state const & s, F && f) { - return map_filter(s.get_goals(), [=](std::pair const & in, std::pair & out) -> bool { - check_interrupted(); - optional new_goal = f(in.first, in.second); - if (new_goal) { - out.first = in.first; - out.second = *new_goal; - return true; - } else { - return false; - } - }); -} - -io_state_stream const & operator<<(io_state_stream const & out, proof_state & s); - +/** \brief Create a proof state for a metavariable \c mvar */ +proof_state to_proof_state(expr const & mvar, name_generator const & ngen); +proof_state to_proof_state(expr const & mvar); /** - \brief Return a name based on \c n that is suitable to be used as a hypothesis name - It basically renames \c n to 'H' if \c d is a proposition and \c n is the default arrow binder name. + \brief Similar to the previous \c to_proof_state functions, but when \c opts contains tactic.minimize_context, and + Type.{0} in \c env is impredicative, then only hypothesis that are not prositions are marked as "contextual". */ -name arg_to_hypothesis_name(name const & n, expr const & d, ro_environment const & env, context const & ctx, - optional const & menv = none_menv()); -inline name arg_to_hypothesis_name(name const & n, expr const & d, ro_environment const & env, context const & ctx, metavar_env const & menv) { - return arg_to_hypothesis_name(n, d, env, ctx, some_menv(menv)); -} +proof_state to_proof_state(environment const & env, expr const & mvar, name_generator const & ngen, options const & opts = options()); +proof_state to_proof_state(environment const & env, expr const & mvar, options const & opts = options()); + +goals map_goals(proof_state const & s, std::function(name const & gn, goal const & g)> const & f); +io_state_stream const & operator<<(io_state_stream const & out, proof_state & s); UDATA_DEFS_CORE(goals) UDATA_DEFS(proof_state) diff --git a/src/library/tactic/register_module.h b/src/library/tactic/register_module.h index fe32e7bfd..16438b9fa 100644 --- a/src/library/tactic/register_module.h +++ b/src/library/tactic/register_module.h @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include "util/script_state.h" #include "library/tactic/goal.h" #include "library/tactic/proof_builder.h" -// #include "library/tactic/proof_state.h" +#include "library/tactic/proof_state.h" // #include "library/tactic/tactic.h" // #include "library/tactic/apply_tactic.h" // #include "library/tactic/simplify_tactic.h" @@ -17,7 +17,7 @@ namespace lean { inline void open_tactic_module(lua_State * L) { open_goal(L); open_proof_builder(L); - // open_proof_state(L); + open_proof_state(L); // open_tactic(L); // open_apply_tactic(L); // open_simplify_tactic(L); diff --git a/tests/lua/proof_state1.lua b/tests/lua/proof_state1.lua new file mode 100644 index 000000000..992865c0c --- /dev/null +++ b/tests/lua/proof_state1.lua @@ -0,0 +1,19 @@ +local env = environment() +local A = Local("A", Type) +env = add_decl(env, mk_var_decl("eq", Pi(A, mk_arrow(A, A, Bool)))) +local eq = Const("eq") +local a = Local("a", A) +local b = Local("b", A) +local H = Local("H", eq(A, a, b)) +local m = mk_metavar("m", Pi({A, a, b, H}, eq(A, a, b))) +print(to_proof_state(m)) +local s = to_proof_state(m) +local n, g = s:goals():head() +local hs = g:hyps() +local h = hs:head() +local pm = proof_map() +pm:insert("main", h) +local r = s:pb(pm, substitution()) +print(r) +assert(env:infer_type(r) == env:infer_type(m)) +