From 4cb5f97038d155aa00e74a49b1f903daf6826481 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 1 Jul 2014 16:11:19 -0700 Subject: [PATCH] refactor(library/tactic): simplify tactic framework, no more proof builders Signed-off-by: Leonardo de Moura --- src/frontends/lean/elaborator.cpp | 19 +-- src/frontends/lean/parser.cpp | 8 + src/kernel/expr.h | 1 + src/library/tactic/CMakeLists.txt | 3 +- src/library/tactic/apply_tactic.cpp | 7 +- src/library/tactic/goal.cpp | 225 ++++++++------------------- src/library/tactic/goal.h | 78 ++++++---- src/library/tactic/proof_builder.cpp | 92 ----------- src/library/tactic/proof_builder.h | 34 ---- src/library/tactic/proof_state.cpp | 130 ++++------------ src/library/tactic/proof_state.h | 54 +++---- src/library/tactic/register_module.h | 2 - src/library/tactic/tactic.cpp | 131 ++++++---------- src/library/tactic/tactic.h | 7 +- tests/lua/goal1.lua | 14 +- tests/lua/proof_state1.lua | 13 +- 16 files changed, 240 insertions(+), 578 deletions(-) delete mode 100644 src/library/tactic/proof_builder.cpp delete mode 100644 src/library/tactic/proof_builder.h diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 19fbee347..fedb3a322 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -610,21 +610,16 @@ public: collect_metavars(e, mvars); for (auto mvar : mvars) { mvar = update_mlocal(mvar, subst.instantiate_metavars_wo_jst(mlocal_type(mvar))); - proof_state ps = to_proof_state(m_env, mvar, m_ngen.mk_child(), m_ios.get_options()); + proof_state ps = to_proof_state(mvar, m_ngen.mk_child()); if (optional t = get_tactic_for(mvar)) { proof_state_seq seq = (*t)(m_env, m_ios, ps); if (auto r = seq.pull()) { - try { - if (auto pr = to_proof(r->first)) { - subst = subst.assign(mlocal_name(mvar), *pr, justification()); - } else { - display_unsolved_proof_state(mvar, r->first, "unsolved subgoals"); - } - } catch (exception & ex) { - regular out(m_env, m_ios); - display_error_pos(out, m_pos_provider, mvar); - out << " proof generation failed\n >> "; - display_error(out, nullptr, ex); + substitution s = r->first.get_subst(); + expr v = s.instantiate_metavars_wo_jst(mvar); + if (has_metavar(v)) { + display_unsolved_proof_state(mvar, r->first, "unsolved subgoals"); + } else { + subst = subst.assign(mlocal_name(mvar), v); } } else { // tactic failed to produce any result diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 9a0b5019e..26132a42d 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -945,6 +945,9 @@ static list collect_contextual_parameters(local_expr_decls const & local_d } tactic parser::parse_exact_apply() { + parse_expr(); + return id_tactic(); +#if 0 auto p = pos(); expr e = parse_expr(); check_only_contextual_locals(e, m_local_decls, p); @@ -979,9 +982,13 @@ tactic parser::parse_exact_apply() { proof_builder new_pb = add_proof(s.get_pb(), gname, new_e); return some_proof_state(proof_state(s, new_gs, new_pb, ngen)); }); +#endif } tactic parser::parse_apply() { + parse_expr(); + return id_tactic(); +#if 0 auto p = pos(); expr e = parse_expr(); check_only_contextual_locals(e, m_local_decls, p); @@ -1000,6 +1007,7 @@ tactic parser::parse_apply() { new_e = instantiate(new_e, l); return apply_tactic(new_e)(env, ios, new_s); }); +#endif } tactic parser::parse_tactic(unsigned /* rbp */) { diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 93539cfb5..0f1f1a2cb 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -217,6 +217,7 @@ public: bool is_cast() const { return m_cast; } bool is_contextual() const { return m_contextual; } bool is_strict_implicit() const { return m_strict_implicit; } + binder_info update_contextual(bool f) const { return binder_info(m_implicit, m_cast, f, m_strict_implicit); } }; inline binder_info mk_implicit_binder_info() { return binder_info(true); } diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index 8019741a4..c0c757da9 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -1,5 +1,4 @@ -add_library(tactic goal.cpp proof_builder.cpp proof_state.cpp - tactic.cpp apply_tactic.cpp) +add_library(tactic goal.cpp proof_state.cpp tactic.cpp apply_tactic.cpp) # simplify_tactic.cpp) diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index 35716c9ca..9c0410035 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -37,8 +37,10 @@ bool collect_simple_metas(expr const & e, buffer & result) { return !failed; } -tactic apply_tactic(expr const & e) { - return tactic([=](environment const & env, io_state const & ios, proof_state const & s) { +tactic apply_tactic(expr const & /* e */) { + return tactic([=](environment const &, io_state const &, proof_state const & s) { + return s; +#if 0 if (s.is_final_state()) { return proof_state_seq(); } @@ -111,6 +113,7 @@ tactic apply_tactic(expr const & e) { }); return proof_state(s, new_gs, new_pb, new_ngen); }); +#endif }); } diff --git a/src/library/tactic/goal.cpp b/src/library/tactic/goal.cpp index 33fa14d6a..01312a8f3 100644 --- a/src/library/tactic/goal.cpp +++ b/src/library/tactic/goal.cpp @@ -10,17 +10,18 @@ Author: Leonardo de Moura #include "kernel/replace_fn.h" #include "kernel/for_each_fn.h" #include "kernel/abstract.h" +#include "kernel/type_checker.h" #include "library/kernel_bindings.h" #include "library/tactic/goal.h" namespace lean { -goal::goal(hypotheses const & hs, expr const & c):m_hypotheses(hs), m_conclusion(c) {} - -static bool is_used_pp_name(hypothesis const * begin, hypothesis const * end, name const & n) { - return std::any_of(begin, end, [&](hypothesis const & h) { return local_pp_name(h.first) == n; }); +static bool is_used_pp_name(expr const * begin, expr const * end, name const & n) { + return std::any_of(begin, end, [&](expr const & h) { + return local_pp_name(h) == n; + }); } -static expr pick_unused_pp_name(hypothesis const * begin, hypothesis const * end, expr const & l) { +static expr pick_unused_pp_name(expr const * begin, expr const * end, expr const & l) { expr r = l; unsigned i = 1; while (is_used_pp_name(begin, end, local_pp_name(r))) { @@ -42,10 +43,10 @@ static void update_local(expr & t, expr const & old_local, expr const & new_loca }); } -static void update_local(hypothesis * begin, hypothesis * end, expr & conclusion, +static void update_local(expr * begin, expr * end, expr & conclusion, expr const & old_local, expr const & new_local) { for (auto it = begin; it != end; ++it) - update_local(it->first, old_local, new_local); + update_local(*it, old_local, new_local); update_local(conclusion, old_local, new_local); } @@ -53,16 +54,15 @@ format goal::pp(environment const & env, formatter const & fmt, options const & unsigned indent = get_pp_indent(opts); bool unicode = get_pp_unicode(opts); format turnstile = unicode ? format("\u22A2") /* ⊢ */ : format("|-"); - expr conclusion = m_conclusion; - buffer tmp; - to_buffer(m_hypotheses, tmp); - std::reverse(tmp.begin(), tmp.end()); + expr conclusion = m_type; + buffer tmp; + get_app_args(m_meta, tmp); bool first = true; format r; auto end = tmp.end(); for (auto it = tmp.begin(); it != end; ++it) { if (first) first = false; else r += compose(comma(), line()); - expr l = it->first; + expr l = *it; expr new_l = pick_unused_pp_name(tmp.begin(), it, l); if (!is_eqp(l, new_l)) update_local(it+1, end, conclusion, l, new_l); @@ -73,59 +73,36 @@ format goal::pp(environment const & env, formatter const & fmt, options const & return group(r); } -expr goal::mk_meta(name const & n, expr const & type) const { - if (has_local(type)) { - bool failed = false; - name missing; - for_each(type, [&](expr const & e, unsigned) { - if (!has_local(e) || failed) return false; - if (is_local(e)) { - bool found = false; - for (hypothesis const & h : m_hypotheses) { - if (mlocal_name(h.first) == mlocal_name(e)) { - found = true; - break; - } - } - if (!found) { - failed = true; - missing = local_pp_name(e); - return false; - } - } - return true; - }); - if (failed) { - throw exception(sstream() << "invalid metavariable for goal, metavariable type contains local constant '" - << missing << "' which is not a hypothesis for this goal"); - } +expr goal::abstract(expr const & v) const { + buffer locals; + get_app_args(m_meta, locals); + return Fun(locals, v); +} + +expr goal::mk_meta(name const & n, expr const & type, bool only_contextual) const { + buffer locals; + get_app_args(m_meta, locals); + if (only_contextual) { + auto new_end = std::remove_if(locals.begin(), locals.end(), + [](expr const & l) { return !local_info(l).is_contextual(); }); + locals.shrink(locals.size() - (locals.end() - new_end)); } - expr t = type; - buffer args; - for (hypothesis const & h : m_hypotheses) { - if (h.second) { - t = Pi(h.first, t); - args.push_back(h.first); - } - } - std::reverse(args.begin(), args.end()); - return mk_app(mk_metavar(n, t), args); + expr mvar = mk_metavar(n, Pi(locals, type)); + return mk_app(mvar, locals); } goal goal::instantiate_metavars(substitution const & s) const { - hypotheses hs = map(m_hypotheses, [&](hypothesis const & h) { - return mk_pair(s.instantiate_metavars_wo_jst(h.first), h.second); - }); - expr c = s.instantiate_metavars_wo_jst(m_conclusion); - return goal(hs, c); + return goal(s.instantiate_metavars_wo_jst(m_meta), + s.instantiate_metavars_wo_jst(m_type)); } -static bool validate(expr const & r, hypotheses const & hs) { +static bool validate_locals(expr const & r, unsigned num_locals, expr const * locals) { bool failed = false; for_each(r, [&](expr const & e, unsigned) { if (!has_local(e) || failed) return false; if (is_local(e) && - !std::any_of(hs.begin(), hs.end(), [&](hypothesis const & h) { return h.first == e; })) { + !std::any_of(locals, locals + num_locals, + [&](expr const & l) { return mlocal_name(l) == mlocal_name(e); })) { failed = true; return false; } @@ -134,111 +111,34 @@ static bool validate(expr const & r, hypotheses const & hs) { return !failed; } -bool goal::validate() const { - if (!::lean::validate(m_conclusion, m_hypotheses)) +bool goal::validate_locals() const { + buffer locals; + get_app_args(m_meta, locals); + if (!::lean::validate_locals(m_type, locals.size(), locals.data())) return false; - hypotheses const * h = &m_hypotheses; - while (!is_nil(*h)) { - if (!::lean::validate(mlocal_type(head(*h).first), tail(*h))) + unsigned i = locals.size(); + while (i > 0) { + --i; + if (!::lean::validate_locals(mlocal_type(locals[i]), i, locals.data())) return false; - h = &tail(*h); } return true; } -DECL_UDATA(hypotheses) - -static int mk_hypotheses(lua_State * L) { - int i = lua_gettop(L); - hypotheses r; - if (i > 0 && is_hypotheses(L, i)) { - r = to_hypotheses(L, i); - i--; - } - while (i > 0) { - if (is_expr(L, i)) { - expr const & l = to_expr(L, i); - if (!is_local(l)) - throw exception(sstream() << "arg #" << i << " must be a local constant or a pair"); - r = hypotheses(hypothesis(l, true), r); - } else { - lua_rawgeti(L, i, 1); - lua_rawgeti(L, i, 2); - if (!is_expr(L, -2) || !is_local(to_expr(L, -2)) || !lua_isboolean(L, -1)) - throw exception(sstream() << "arg #" << i << " must be a pair: local constant, Boolean"); - r = hypotheses(hypothesis(to_expr(L, -2), lua_toboolean(L, -1)), r); - lua_pop(L, 2); - } - i--; - } - return push_hypotheses(L, r); -} - -static int hypotheses_is_nil(lua_State * L) { - lua_pushboolean(L, !to_hypotheses(L, 1)); - return 1; -} - -static int hypotheses_head(lua_State * L) { - hypotheses const & hs = to_hypotheses(L, 1); - if (!hs) - throw exception("head method expects a non-empty hypotheses list"); - push_expr(L, head(hs).first); - push_boolean(L, head(hs).second); - return 2; -} - -static int hypotheses_tail(lua_State * L) { - hypotheses const & hs = to_hypotheses(L, 1); - if (!hs) - throw exception("tail method expects a non-empty hypotheses list"); - push_hypotheses(L, tail(hs)); - return 1; -} - -static int hypotheses_next(lua_State * L) { - hypotheses & hs = to_hypotheses(L, lua_upvalueindex(1)); - if (hs) { - push_hypotheses(L, tail(hs)); - lua_replace(L, lua_upvalueindex(1)); - push_expr(L, head(hs).first); - push_boolean(L, head(hs).second); - return 2; +bool goal::validate(environment const & env) const { + if (validate_locals()) { + type_checker tc(env); + return tc.is_def_eq(tc.check(m_meta), m_type); } else { - lua_pushnil(L); - return 1; + return false; } } -static int hypotheses_items(lua_State * L) { - hypotheses & hs = to_hypotheses(L, 1); - push_hypotheses(L, hs); // upvalue(1): hypotheses - lua_pushcclosure(L, &safe_function, 1); // create closure with 1 upvalue - return 1; -} - -static int hypotheses_len(lua_State * L) { - lua_pushinteger(L, length(to_hypotheses(L, 1))); - return 1; -} - -static const struct luaL_Reg hypotheses_m[] = { - {"__gc", hypotheses_gc}, // never throws - {"__len", safe_function}, - {"size", safe_function}, - {"pairs", safe_function}, - {"is_nil", safe_function}, - {"empty", safe_function}, - {"head", safe_function}, - {"tail", safe_function}, - {0, 0} -}; - DECL_UDATA(goal) -static int mk_goal(lua_State * L) { return push_goal(L, goal(to_hypotheses(L, 1), to_expr(L, 2))); } -static int goal_hypotheses(lua_State * L) { return push_hypotheses(L, to_goal(L, 1).get_hypotheses()); } -static int goal_conclusion(lua_State * L) { return push_expr(L, to_goal(L, 1).get_conclusion()); } +static int mk_goal(lua_State * L) { return push_goal(L, goal(to_expr(L, 1), to_expr(L, 2))); } +static int goal_meta(lua_State * L) { return push_expr(L, to_goal(L, 1).get_meta()); } +static int goal_type(lua_State * L) { return push_expr(L, to_goal(L, 1).get_type()); } static int goal_tostring(lua_State * L) { std::ostringstream out; goal & g = to_goal(L, 1); @@ -249,7 +149,11 @@ static int goal_tostring(lua_State * L) { lua_pushstring(L, out.str().c_str()); return 1; } -static int goal_mk_meta(lua_State * L) { return push_expr(L, to_goal(L, 1).mk_meta(to_name_ext(L, 2), to_expr(L, 3))); } +static int goal_mk_meta(lua_State * L) { + int nargs = lua_gettop(L); + return push_expr(L, to_goal(L, 1).mk_meta(to_name_ext(L, 2), to_expr(L, 3), nargs == 4 ? lua_toboolean(L, 4) : true)); +} + static int goal_pp(lua_State * L) { int nargs = lua_gettop(L); goal & g = to_goal(L, 1); @@ -263,29 +167,28 @@ static int goal_pp(lua_State * L) { return push_format(L, g.pp(to_environment(L, 2), to_formatter(L, 3), to_options(L, 4))); } } -static int goal_validate(lua_State * L) { return push_boolean(L, to_goal(L, 1).validate()); } +static int goal_validate_locals(lua_State * L) { return push_boolean(L, to_goal(L, 1).validate_locals()); } +static int goal_validate(lua_State * L) { return push_boolean(L, to_goal(L, 1).validate(to_environment(L, 2))); } +static int goal_instantiate(lua_State * L) { return push_goal(L, to_goal(L, 1).instantiate_metavars(to_substitution(L, 2))); } +static int goal_abstract(lua_State * L) { return push_expr(L, to_goal(L, 1).abstract(to_expr(L, 2))); } +static int goal_name(lua_State * L) { return push_name(L, to_goal(L, 1).get_name()); } static const struct luaL_Reg goal_m[] = { {"__gc", goal_gc}, // never throws {"__tostring", safe_function}, - {"hypotheses", safe_function}, - {"hyps", safe_function}, - {"conclusion", safe_function}, + {"abstract", safe_function}, {"mk_meta", safe_function}, {"pp", safe_function}, {"validate", safe_function}, + {"validate_locals", safe_function}, + {"instantiate", safe_function}, + {"meta", safe_function}, + {"type", safe_function}, + {"name", safe_function}, {0, 0} }; void open_goal(lua_State * L) { - luaL_newmetatable(L, hypotheses_mt); - lua_pushvalue(L, -1); - lua_setfield(L, -2, "__index"); - setfuncs(L, hypotheses_m, 0); - - SET_GLOBAL_FUN(hypotheses_pred, "is_hypotheses"); - SET_GLOBAL_FUN(mk_hypotheses, "hypotheses"); - luaL_newmetatable(L, goal_mt); lua_pushvalue(L, -1); lua_setfield(L, -2, "__index"); diff --git a/src/library/tactic/goal.h b/src/library/tactic/goal.h index 4b6df96d8..3e1a23c8e 100644 --- a/src/library/tactic/goal.h +++ b/src/library/tactic/goal.h @@ -15,49 +15,69 @@ Author: Leonardo de Moura namespace lean { /** - \brief A hypothesis is a local variable + a flag indicating whether it is "contextual" or not. - Only contextual ones are used to build the context of new metavariables. + \brief A goal is just encoding the synthesis problem (?m l_1 .... l_n) : t + That is, we want to find a term \c ?m s.t. (?m l_1 ... l_n) has type \c t + The terms \c l_i are just local constants. + + We can convert any metavariable + ?m : Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), B[x_1, ..., x_n] + into a goal by simply creating the local constants + l_1 : A_1, ..., l_n : A_n[l_1, ..., l_{n-1}] + and then, create the goal + ?m l_1 ... l_n : B[l_1, ..., l_n] + Now, suppose we find a term \c b with type B[l_1, ... l_n], then we can simply + find \c ?m by abstracting l_1, ..., l_n + + We can check whether a goal is well formed in an environment by type checking. */ -typedef std::pair hypothesis; -typedef list hypotheses; class goal { - hypotheses m_hypotheses; - expr m_conclusion; + expr m_meta; + expr m_type; public: goal() {} - goal(hypotheses const & hs, expr const & c); - hypotheses const & get_hypotheses() const { return m_hypotheses; } - expr const & get_conclusion() const { return m_conclusion; } + goal(expr const & m, expr const & t):m_meta(m), m_type(t) {} + + expr const & get_meta() const { return m_meta; } + expr const & get_type() const { return m_type; } + + name get_name() const { return mlocal_name(get_app_fn(m_meta)); } + + expr get_mvar() const { return get_app_fn(m_meta); } + /** - \brief Create a metavarible application (m l_1 ... l_n) with type \c type, - where \c l_1 ... \c l_n are the contextual hypotheses of this goal, and - \c m is a metavariable with name \c n. + \brief Given a term \c v with type get_type(), build a lambda abstraction + that is the solution for the metavariable associated with this goal. */ - expr mk_meta(name const & n, expr const & type) const; + expr abstract(expr const & v) const; + /** - brief Return true iff this is a valid goal. - We say a goal is valid when the conclusion only contains local constants that are in hypotheses, - and each hypothesis only contains local constants that occur in the previous hypotheses. + \brief Create a metavariable application (?m l_1 ... l_n) with the given type, + and the locals from this goal. If only_contextual == true, then we only include + the local constants that are marked as contextual. */ - bool validate() const; + expr mk_meta(name const & m, expr const & type, bool only_contextual = true) const; + + /** + brief Return true iff get_type() only contains local constants that arguments + of get_meta(), and each argument of get_meta() only contains local constants + that are previous arguments. + */ + bool validate_locals() const; + + /** + \brief Return true iff \c validate_locals() return true and type of \c get_meta() in + \c env is get_type() + */ + bool validate(environment const & env) const; + + /** \brief Instatiate the metavariables in this goal using the given substitution */ goal instantiate_metavars(substitution const & s) const; + format pp(environment const & env, formatter const & fmt, options const & opts) const; }; -inline goal update(goal const & g, expr const & c) { return goal(g.get_hypotheses(), c); } -inline goal update(goal const & g, hypotheses const & hs) { return goal(hs, g.get_conclusion()); } -inline goal update(goal const & g, buffer const & hs) { return goal(to_list(hs.begin(), hs.end()), g.get_conclusion()); } -inline hypotheses add_hypothesis(expr const & l, hypotheses const & hs) { - lean_assert(is_local(l)); - return cons(hypothesis(l, true), hs); -} -inline hypotheses add_hypothesis(hypothesis const & h, hypotheses const & hs) { - return cons(h, hs); -} - io_state_stream const & operator<<(io_state_stream const & out, goal const & g); -UDATA_DEFS_CORE(hypotheses) UDATA_DEFS(goal) void open_goal(lua_State * L); } diff --git a/src/library/tactic/proof_builder.cpp b/src/library/tactic/proof_builder.cpp deleted file mode 100644 index e7d067b28..000000000 --- a/src/library/tactic/proof_builder.cpp +++ /dev/null @@ -1,92 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include "util/exception.h" -#include "util/sstream.h" -#include "util/luaref.h" -#include "library/kernel_bindings.h" -#include "library/tactic/proof_builder.h" - -namespace lean { -expr find(proof_map const & m, name const & n) { - expr const * r = m.find(n); - if (r) - return *r; - throw exception(sstream() << "proof for goal '" << n << "' not found"); -} - -proof_builder add_proofs(proof_builder const & pb, list> const & prs) { - return proof_builder([=](proof_map const & m, substitution const & s) -> expr { - proof_map new_m(m); - for (auto const & np : prs) { - new_m.insert(np.first, np.second); - } - return pb(new_m, s); - }); -} - -proof_builder add_proof(proof_builder const & pb, name const & goal_name, expr const & pr) { - return add_proofs(pb, list>(mk_pair(goal_name, pr))); -} - -DECL_UDATA(proof_map) - -static int mk_proof_map(lua_State * L) { - int nargs = lua_gettop(L); - if (nargs == 0) - return push_proof_map(L, proof_map()); - else - return push_proof_map(L, to_proof_map(L, 1)); -} - -static int proof_map_find(lua_State * L) { - return push_expr(L, find(to_proof_map(L, 1), to_name_ext(L, 2))); -} - -static int proof_map_insert(lua_State * L) { - to_proof_map(L, 1).insert(to_name_ext(L, 2), to_expr(L, 3)); - return 0; -} - -static int proof_map_erase(lua_State * L) { - to_proof_map(L, 1).erase(to_name_ext(L, 2)); - return 0; -} - -static const struct luaL_Reg proof_map_m[] = { - {"__gc", proof_map_gc}, // never throws - {"find", safe_function}, - {"insert", safe_function}, - {"erase", safe_function}, - {0, 0} -}; - -proof_builder to_proof_builder(lua_State * L, int idx) { - luaL_checktype(L, idx, LUA_TFUNCTION); // user-fun - luaref f(L, idx); - return proof_builder([=](proof_map const & m, substitution const & s) { - lua_State * L = f.get_state(); - f.push(); - push_proof_map(L, m); - push_substitution(L, s); - pcall(L, 2, 1, 0); - expr r = to_expr(L, -1); - lua_pop(L, 1); - return r; - }); -} - -void open_proof_builder(lua_State * L) { - luaL_newmetatable(L, proof_map_mt); - lua_pushvalue(L, -1); - lua_setfield(L, -2, "__index"); - setfuncs(L, proof_map_m, 0); - - SET_GLOBAL_FUN(proof_map_pred, "is_proof_map"); - SET_GLOBAL_FUN(mk_proof_map, "proof_map"); -} -} diff --git a/src/library/tactic/proof_builder.h b/src/library/tactic/proof_builder.h deleted file mode 100644 index b41d72469..000000000 --- a/src/library/tactic/proof_builder.h +++ /dev/null @@ -1,34 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -#include -#include "util/lua.h" -#include "util/name.h" -#include "util/rb_map.h" -#include "kernel/expr.h" - -namespace lean { -typedef rb_map proof_map; -/** - \brief Return the proof (of inhabitated type) for the goal named \c n in the \c proof_map \c m. - Throw an exception if \c m does not contain a proof for \c n. -*/ -expr find(proof_map const & m, name const & n); -/** - \brief A proof builder creates an inhabitant a goal type (aka - conclusion) using the inhabitants for its subgoals. -*/ -typedef std::function proof_builder; -proof_builder add_proofs(proof_builder const & pb, list> const & prs); -proof_builder add_proof(proof_builder const & pb, name const & goal_name, expr const & pr); - -/** \brief Convert a Lua function on position \c idx (on the Lua stack) into a proof_builder_fn */ -proof_builder to_proof_builder(lua_State * L, int idx); -UDATA_DEFS_CORE(proof_map) -void open_proof_builder(lua_State * L); -} diff --git a/src/library/tactic/proof_state.cpp b/src/library/tactic/proof_state.cpp index 813722f16..36c961d65 100644 --- a/src/library/tactic/proof_state.cpp +++ b/src/library/tactic/proof_state.cpp @@ -24,48 +24,32 @@ Author: Leonardo de Moura namespace lean { 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"); -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); - j++; - } - return optional(); -} 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()) { + for (auto const & g : get_goals()) { 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(env, fmt, opts)))}); + r += group(format{format(g.get_name()), colon(), nest(indent, compose(line(), g.pp(env, fmt, opts)))}); } else { - r += p.second.pp(env, fmt, opts); + r += g.pp(env, fmt, opts); } } if (first) r = format("no goals"); return r; } -goals map_goals(proof_state const & s, std::function(name const & gn, goal const & g)> f) { - return map_filter(s.get_goals(), [=](std::pair const & in, std::pair & out) -> bool { +goals map_goals(proof_state const & s, std::function(goal const & g)> f) { + return map_filter(s.get_goals(), [=](goal const & in, goal & out) -> bool { check_interrupted(); - optional new_goal = f(in.first, in.second); + optional new_goal = f(in); if (new_goal) { - out.first = in.first; - out.second = *new_goal; + out = *new_goal; return true; } else { return false; @@ -73,55 +57,24 @@ goals map_goals(proof_state const & s, std::function(name const & }); } -void proof_state::get_goal_names(name_set & r) const { - for (auto const & p : get_goals()) - r.insert(p.first); -} - -static name g_main("main"); -proof_builder mk_init_proof_builder(list const & locals) { - return proof_builder([=](proof_map const & m, substitution const &) -> expr { - expr r = find(m, g_main); - for (expr const & l : locals) - r = Fun(l, r); - return r; - }); -} - -static proof_state to_proof_state(environment const * env, expr const & mvar, name_generator ngen) { +proof_state to_proof_state(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; + buffer ls; while (is_pi(t)) { expr l = mk_local(ngen.next(), binding_name(t), binding_domain(t), binding_info(t)); - bool c = true; - if (tc) - c = !tc->is_prop(binding_domain(t)); - hs = hypotheses(hypothesis(l, c), hs); + ls.push_back(l); 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), ngen, init_ls); + expr meta = mk_app(mvar, ls); + goals gs(goal(meta, t)); + return proof_state(gs, substitution(), ngen, meta); } 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); +proof_state to_proof_state(expr const & mvar) { + return to_proof_state(mvar, name_generator(g_tmp_prefix)); } io_state_stream const & operator<<(io_state_stream const & out, proof_state const & s) { @@ -130,15 +83,6 @@ io_state_stream const & operator<<(io_state_stream const & out, proof_state cons return out; } -optional to_proof(proof_state const & s) { - if (s.is_final_state()) { - substitution a; - proof_map m; - return some_expr(s.get_pb()(m, a)); - } - return none_expr(); -} - DECL_UDATA(goals) static int mk_goals(lua_State * L) { @@ -149,12 +93,7 @@ static int mk_goals(lua_State * L) { 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); + r = goals(to_goal(L, i), r); i--; } return push_goals(L, r); @@ -169,9 +108,7 @@ static int goals_head(lua_State * L) { goals const & hs = to_goals(L, 1); if (!hs) throw exception("head method expects a non-empty goal list"); - push_name(L, head(hs).first); - push_goal(L, head(hs).second); - return 2; + return push_goal(L, head(hs)); } static int goals_tail(lua_State * L) { @@ -187,9 +124,7 @@ static int goals_next(lua_State * L) { if (hs) { push_goals(L, tail(hs)); lua_replace(L, lua_upvalueindex(1)); - push_name(L, head(hs).first); - push_goal(L, head(hs).second); - return 2; + return push_goal(L, head(hs)); } else { lua_pushnil(L); return 1; @@ -204,8 +139,7 @@ static int goals_items(lua_State * L) { } static int goals_len(lua_State * L) { - lua_pushinteger(L, length(to_goals(L, 1))); - return 1; + return push_integer(L, length(to_goals(L, 1))); } static const struct luaL_Reg goals_m[] = { @@ -227,9 +161,9 @@ static int mk_proof_state(lua_State * L) { 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))); + return push_proof_state(L, proof_state(to_proof_state(L, 1), to_goals(L, 2), to_substitution(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))); + return push_proof_state(L, proof_state(to_proof_state(L, 1), to_goals(L, 2), to_substitution(L, 3), to_name_generator(L, 4))); } else { throw exception("proof_state invalid number of arguments"); } @@ -239,14 +173,8 @@ static int to_proof_state(lua_State * L) { 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))); + return push_proof_state(L, to_proof_state(to_expr(L, 1), to_name_generator(L, 2))); } static int proof_state_tostring(lua_State * L) { @@ -261,9 +189,9 @@ static int proof_state_tostring(lua_State * L) { } 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_ngen(lua_State * L) { return push_name_generator(L, to_proof_state(L, 1).get_ngen()); } +static int proof_state_get_subst(lua_State * L) { return push_substitution(L, to_proof_state(L, 1).get_subst()); } +static int proof_state_get_initial(lua_State * L) { return push_list_expr(L, to_proof_state(L, 1).get_initial()); } static int proof_state_is_final_state(lua_State * L) { return push_boolean(L, to_proof_state(L, 1).is_final_state()); } static int proof_state_pp(lua_State * L) { int nargs = lua_gettop(L); @@ -278,17 +206,15 @@ static int proof_state_pp(lua_State * L) { return push_format(L, s.pp(to_environment(L, 2), to_formatter(L, 3), to_options(L, 4))); } -static int to_proof(lua_State * L) { return push_optional_expr(L, to_proof(to_proof_state(L, 1))); } - static const struct luaL_Reg proof_state_m[] = { {"__gc", proof_state_gc}, // never throws {"__tostring", safe_function}, {"pp", safe_function}, - {"get_goals", safe_function}, - {"pb", safe_function}, {"goals", safe_function}, + {"subst", safe_function}, + {"initial", safe_function}, + {"ngen", safe_function}, {"is_final_state", safe_function}, - {"to_proof", safe_function}, {0, 0} }; diff --git a/src/library/tactic/proof_state.h b/src/library/tactic/proof_state.h index b92adaac4..49254437e 100644 --- a/src/library/tactic/proof_state.h +++ b/src/library/tactic/proof_state.h @@ -11,37 +11,34 @@ Author: Leonardo de Moura #include "util/optional.h" #include "util/name_set.h" #include "library/tactic/goal.h" -#include "library/tactic/proof_builder.h" namespace lean { -typedef std::pair named_goal; -typedef list goals; -/** \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); - +typedef list goals; class proof_state { goals m_goals; - proof_builder m_proof_builder; + substitution m_subst; name_generator m_ngen; - list m_init_locals; + // The following term is of the form (?m l_1 ... l_n), it captures the + // metavariable this proof state is trying to synthesize, and + // the context [l_1, ..., l_n]. The context is important because it allows + // us to "reinterpret" an expression in this context. + expr m_inital; public: - proof_state(goals const & gs, proof_builder const & pb, name_generator const & ngen, list const & ls = list()): - m_goals(gs), m_proof_builder(pb), m_ngen(ngen), m_init_locals(ls) {} - proof_state(proof_state const & s, goals const & gs, proof_builder const & pb, name_generator const & ngen): - proof_state(gs, pb, ngen, s.m_init_locals) {} - proof_state(proof_state const & s, goals const & gs, proof_builder 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) {} - proof_state(proof_state const & s, name_generator const & ngen): - proof_state(s.m_goals, s.m_proof_builder, ngen, s.m_init_locals) {} + proof_state(goals const & gs, substitution const & s, name_generator const & ngen, expr const & ini): + m_goals(gs), m_subst(s), m_ngen(ngen), m_inital(ini) {} + proof_state(proof_state const & s, goals const & gs, substitution const & subst, name_generator const & ngen): + proof_state(gs, subst, ngen, s.m_inital) {} + proof_state(proof_state const & s, goals const & gs, substitution const & subst):proof_state(s, gs, subst, s.m_ngen) {} + proof_state(proof_state const & s, goals const & gs):proof_state(s, gs, s.m_subst) {} + proof_state(proof_state const & s, name_generator const & ngen):proof_state(s.m_goals, s.m_subst, ngen, s.m_inital) {} + goals const & get_goals() const { return m_goals; } - proof_builder const & get_pb() const { return m_proof_builder; } - name_generator const & ngen() const { return m_ngen; } - list const & get_init_locals() const { return m_init_locals; } + substitution const & get_subst() const { return m_subst; } + name_generator const & get_ngen() const { return m_ngen; } + expr const & get_initial() const { return m_inital; } + /** \brief Return true iff this state does not have any goals left */ bool is_final_state() const { return empty(m_goals); } - /** \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(environment const & env, formatter const & fmt, options const & opts) const; }; @@ -49,19 +46,10 @@ inline optional some_proof_state(proof_state const & s) { return so inline optional none_proof_state() { return optional (); } /** \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, name_generator ngen); proof_state to_proof_state(expr const & mvar); -/** - \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". -*/ -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()); -/** \brief Try to extract a proof from the given proof state */ -optional to_proof(proof_state const & s); - -goals map_goals(proof_state const & s, std::function(name const & gn, goal const & g)> f); +goals map_goals(proof_state const & s, std::function(goal const & g)> f); io_state_stream const & operator<<(io_state_stream const & out, proof_state const & s); UDATA_DEFS_CORE(goals) diff --git a/src/library/tactic/register_module.h b/src/library/tactic/register_module.h index 3b22b80d3..941425549 100644 --- a/src/library/tactic/register_module.h +++ b/src/library/tactic/register_module.h @@ -7,7 +7,6 @@ Author: Leonardo de Moura #pragma once #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/tactic.h" #include "library/tactic/apply_tactic.h" @@ -16,7 +15,6 @@ Author: Leonardo de Moura namespace lean { inline void open_tactic_module(lua_State * L) { open_goal(L); - open_proof_builder(L); open_proof_state(L); open_tactic(L); open_apply_tactic(L); diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp index 040fed695..eb589b61a 100644 --- a/src/library/tactic/tactic.cpp +++ b/src/library/tactic/tactic.cpp @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "util/sstream.h" #include "util/interrupt.h" #include "util/lazy_list_fn.h" +#include "util/list_fn.h" #include "kernel/instantiate.h" #include "kernel/replace_visitor.h" #include "library/kernel_bindings.h" @@ -173,105 +174,65 @@ tactic take(tactic const & t, unsigned k) { tactic assumption_tactic() { return tactic01([](environment const &, io_state const &, proof_state const & s) -> optional { - list> proofs; - goals new_gs = map_goals(s, [&](name const & gname, goal const & g) -> optional { - expr const & c = g.get_conclusion(); - optional pr; - for (auto const & p : g.get_hypotheses()) { - check_interrupted(); - if (mlocal_type(p.first) == c) { - pr = p.first; + substitution subst = s.get_subst(); + goals new_gs = map_goals(s, [&](goal const & g) -> optional { + expr const & t = g.get_type(); + optional h; + buffer locals; + get_app_args(g.get_meta(), locals); + for (auto const & l : locals) { + if (mlocal_type(l) == t) { + h = l; break; } } - if (pr) { - proofs.emplace_front(gname, *pr); + if (h) { + subst = subst.assign(g.get_mvar(), g.abstract(*h), justification()); return optional(); } else { return some(g); } }); - if (empty(proofs)) - return none_proof_state(); - return some(proof_state(s, new_gs, add_proofs(s.get_pb(), proofs))); + return some(proof_state(s, new_gs, subst)); }); } tactic beta_tactic() { return tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional { bool reduced = false; - goals new_gs = map_goals(s, [&](name const &, goal const & g) -> optional { - hypotheses new_hs = map(g.get_hypotheses(), [&](hypothesis const & h) { - expr new_h = update_mlocal(h.first, beta_reduce(mlocal_type(h.first))); - if (new_h != h.first) - reduced = true; - return hypothesis(new_h, h.second); - }); - expr const & c = g.get_conclusion(); - expr new_c = beta_reduce(c); - if (new_c != c) + goals new_gs = map_goals(s, [&](goal const & g) -> optional { + expr new_meta = beta_reduce(g.get_meta()); + expr new_type = beta_reduce(g.get_type()); + if (new_meta != g.get_meta() || new_type != g.get_type()) reduced = true; - return some(goal(new_hs, new_c)); + return some(goal(new_meta, new_type)); }); return reduced ? some(proof_state(s, new_gs)) : none_proof_state(); }); } -proof_state_seq focus_core(tactic const & t, name const & gname, environment const & env, io_state const & ios, proof_state const & s) { - for (auto const & p : s.get_goals()) { - if (p.first == gname) { - proof_builder pb = proof_builder([=](proof_map const & m, substitution const &) -> expr { return find(m, gname); }); - proof_state new_s(s, goals(p), pb); // new state with singleton goal - return map(t(env, ios, new_s), [=](proof_state const & s2) { - // we have to put back the goals that were not selected - list> renamed_goals; - goals new_gs = map_append(s.get_goals(), [&](std::pair const & p) { - if (p.first == gname) { - name_set used_names; - s.get_goal_names(used_names); - used_names.erase(gname); - return map(s2.get_goals(), [&](std::pair const & p2) -> std::pair { - name uname = mk_unique(used_names, p2.first); - used_names.insert(uname); - renamed_goals.emplace_front(p2.first, uname); - return mk_pair(uname, p2.second); - }); - } else { - return goals(p); - } - }); - proof_builder pb1 = s.get_pb(); - proof_builder pb2 = s2.get_pb(); - proof_builder new_pb = proof_builder( - [=](proof_map const & m, substitution const & a) -> expr { - proof_map m1(m); // map for pb1 - proof_map m2; // map for pb2 - for (auto p : renamed_goals) { - m2.insert(p.first, find(m, p.second)); - m1.erase(p.first); - } - m1.insert(gname, pb2(m2, a)); - return pb1(m1, a); - }); - return proof_state(s2, new_gs, new_pb); - }); - } - } - return proof_state_seq(); // tactic is not applicable -} - -tactic focus(tactic const & t, name const & gname) { - return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq { - return focus_core(t, gname, env, ios, s); +proof_state_seq focus_core(tactic const & t, unsigned i, environment const & env, io_state const & ios, proof_state const & s) { + goals gs = s.get_goals(); + if (i >= length(gs)) + return proof_state_seq(); + goal const & g = get_ith(gs, i); + proof_state new_s(s, goals(g)); // singleton goal + return map(t(env, ios, new_s), [=](proof_state const & s2) { + // we have to put back the goals that were not selected + buffer tmp; + to_buffer(gs, tmp); + buffer new_gs; + new_gs.append(i, tmp.data()); + for (auto g : s2.get_goals()) + new_gs.push_back(g); + new_gs.append(tmp.size()-i-1, tmp.data()+i+1); + return proof_state(s2, to_list(new_gs.begin(), new_gs.end())); }); } -tactic focus(tactic const & t, int i) { +tactic focus(tactic const & t, unsigned i) { return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq { - if (optional n = s.get_ith_goal_name(i)) - return focus_core(t, *n, env, ios, s); - else - return proof_state_seq(); + return focus_core(t, i, env, ios, s); }); } @@ -347,15 +308,15 @@ public: }; optional unfold_tactic_core(unfold_core_fn & fn, proof_state const & s) { - goals new_gs = map_goals(s, [&](name const &, goal const & g) -> optional { - hypotheses new_hs = map(g.get_hypotheses(), [&](hypothesis const & h) { - expr l = update_mlocal(h.first, fn(mlocal_type(h.first))); - return hypothesis(l, h.second); - }); - expr new_c = fn(g.get_conclusion()); - return some(goal(new_hs, new_c)); + bool reduced = false; + goals new_gs = map_goals(s, [&](goal const & g) -> optional { + expr new_meta = fn(g.get_meta()); + expr new_type = fn(g.get_type()); + if (new_meta != g.get_meta() || new_type != g.get_type()) + reduced = true; + return some(goal(new_meta, new_type)); }); - if (fn.unfolded()) { + if (reduced) { return some(proof_state(s, new_gs)); } else { return none_proof_state(); @@ -455,10 +416,8 @@ static int tactic_focus(lua_State * L) { int nargs = lua_gettop(L); if (nargs == 1) return push_tactic(L, focus(to_tactic(L, 1))); - else if (lua_isnumber(L, 2)) - return push_tactic(L, focus(to_tactic(L, 1), lua_tointeger(L, 2))); else - return push_tactic(L, focus(to_tactic(L, 1), to_name_ext(L, 2))); + return push_tactic(L, focus(to_tactic(L, 1), lua_tointeger(L, 2))); } static int mk_lua_tactic01(lua_State * L) { luaL_checktype(L, 1, LUA_TFUNCTION); // user-fun diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h index 4aecdf409..2419cca4c 100644 --- a/src/library/tactic/tactic.h +++ b/src/library/tactic/tactic.h @@ -118,16 +118,11 @@ typedef std::function