From c2ab31113f213575d3e96c9d38c047d5028300bf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 30 Jun 2014 08:48:01 -0700 Subject: [PATCH] refactor(library/tactic): remove cex_builder and 'precision' for proof_state's These two features make sense for solvers, but not in a general purpose tactic framework for building proofs like the one in Lean. In most cases, we cannot build a counterexample anyway. These two features should be added in a custom framework for combining preprocessing techniques like in Z3. Signed-off-by: Leonardo de Moura --- src/library/tactic/CMakeLists.txt | 2 +- src/library/tactic/apply_tactic.cpp | 4 +-- src/library/tactic/cex_builder.cpp | 40 ----------------------------- src/library/tactic/cex_builder.h | 24 ----------------- src/library/tactic/proof_state.cpp | 39 +++------------------------- src/library/tactic/proof_state.h | 34 +++++------------------- src/library/tactic/tactic.cpp | 15 ++--------- 7 files changed, 14 insertions(+), 144 deletions(-) delete mode 100644 src/library/tactic/cex_builder.cpp delete mode 100644 src/library/tactic/cex_builder.h diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index 776f1e244..8019741a4 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -1,4 +1,4 @@ -add_library(tactic goal.cpp cex_builder.cpp proof_builder.cpp proof_state.cpp +add_library(tactic goal.cpp proof_builder.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 f6d4e28a3..35716c9ca 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -39,9 +39,7 @@ bool collect_simple_metas(expr const & e, buffer & result) { tactic apply_tactic(expr const & e) { return tactic([=](environment const & env, io_state const & ios, proof_state const & s) { - precision prec = s.get_precision(); - if ((prec != precision::Precise && prec != precision::Over) || empty(s.get_goals())) { - // it is pointless to apply this tactic, since it will produce UnderOver + if (s.is_final_state()) { return proof_state_seq(); } goals const & gs = s.get_goals(); diff --git a/src/library/tactic/cex_builder.cpp b/src/library/tactic/cex_builder.cpp deleted file mode 100644 index c1c3e59e2..000000000 --- a/src/library/tactic/cex_builder.cpp +++ /dev/null @@ -1,40 +0,0 @@ -/* -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 -*/ -#include "util/sstream.h" -#include "util/script_state.h" -#include "util/luaref.h" -#include "library/kernel_bindings.h" -#include "library/tactic/cex_builder.h" - -namespace lean { -cex_builder mk_cex_builder_for(name const & gname) { - return cex_builder([=](name const & n, optional const & cex, substitution const &) -> counterexample { - if (n != gname || !cex) - throw exception(sstream() << "failed to build counterexample for '" << gname << "' goal"); - return *cex; - }); -} - -cex_builder to_cex_builder(lua_State * L, int idx) { - luaL_checktype(L, idx, LUA_TFUNCTION); // user-fun - luaref f(L, idx); - return cex_builder([=](name const & n, optional const & cex, substitution const & s) { - lua_State * L = f.get_state(); - f.push(); - push_name(L, n); - if (cex) - push_environment(L, *cex); - else - lua_pushnil(L); - push_substitution(L, s); - pcall(L, 3, 1, 0); - environment r = to_environment(L, -1); - lua_pop(L, 1); - return r; - }); -} -} diff --git a/src/library/tactic/cex_builder.h b/src/library/tactic/cex_builder.h deleted file mode 100644 index 6df4a1937..000000000 --- a/src/library/tactic/cex_builder.h +++ /dev/null @@ -1,24 +0,0 @@ -/* -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 -*/ -#pragma once -#include -#include "util/lua.h" -#include "util/name.h" -#include "util/optional.h" -#include "kernel/environment.h" -#include "kernel/metavar.h" - -namespace lean { -/** \brief In Lean, a counter-example is encoded using an environment object. */ -typedef environment counterexample; -typedef std::function const &, substitution const &)> cex_builder; -/** \brief Return a counterexample builder that expects a counterexample for the given goal. */ -cex_builder mk_cex_builder_for(name const & gname); - -/** \brief Convert a Lua function on position \c idx (on the Lua stack) to a cex_builder_fn */ -cex_builder to_cex_builder(lua_State * L, int idx); -} diff --git a/src/library/tactic/proof_state.cpp b/src/library/tactic/proof_state.cpp index d3724807e..67d49efb0 100644 --- a/src/library/tactic/proof_state.cpp +++ b/src/library/tactic/proof_state.cpp @@ -42,16 +42,6 @@ optional get_ith_goal_name(goals const & gs, unsigned i) { return optional(); } -precision mk_union(precision p1, precision p2) { - if (p1 == p2) return p1; - else if (p1 == precision::Precise) return p2; - else if (p2 == precision::Precise) return p1; - else return precision::UnderOver; -} - -bool trust_proof(precision p) { return p == precision::Precise || p == precision::Over; } -bool trust_cex(precision p) { return p == precision::Precise || p == precision::Under; } - 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); @@ -83,10 +73,6 @@ goals map_goals(proof_state const & s, std::function(name const & }); } -bool proof_state::is_proof_final_state() const { - return empty(get_goals()) && trust_proof(get_precision()); -} - void proof_state::get_goal_names(name_set & r) const { for (auto const & p : get_goals()) r.insert(p.first); @@ -121,7 +107,7 @@ static proof_state to_proof_state(environment const * env, expr const & mvar, na 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); + return proof_state(gs, mk_init_proof_builder(init_ls), ngen, init_ls); } static name g_tmp_prefix = name::mk_internal_unique_name(); @@ -145,7 +131,7 @@ io_state_stream const & operator<<(io_state_stream const & out, proof_state cons } optional to_proof(proof_state const & s) { - if (s.is_proof_final_state()) { + if (s.is_final_state()) { substitution a; proof_map m; return some_expr(s.get_pb()(m, a)); @@ -274,18 +260,11 @@ static int proof_state_tostring(lua_State * L) { 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_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_is_proof_final_state(lua_State * L) { return push_boolean(L, to_proof_state(L, 1).is_proof_final_state()); } +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); proof_state & s = to_proof_state(L, 1); @@ -305,13 +284,10 @@ static const struct luaL_Reg proof_state_m[] = { {"__gc", proof_state_gc}, // never throws {"__tostring", safe_function}, {"pp", safe_function}, - {"get_precision", safe_function}, {"get_goals", safe_function}, {"pb", safe_function}, - {"cb", safe_function}, - {"precision", safe_function}, {"goals", safe_function}, - {"is_proof_final_state", safe_function}, + {"is_final_state", safe_function}, {"to_proof", safe_function}, {0, 0} }; @@ -333,12 +309,5 @@ void open_proof_state(lua_State * L) { SET_GLOBAL_FUN(proof_state_pred, "is_proof_state"); SET_GLOBAL_FUN(mk_proof_state, "proof_state"); SET_GLOBAL_FUN(to_proof_state, "to_proof_state"); - - lua_newtable(L); - SET_ENUM("Precise", precision::Precise); - SET_ENUM("Over", precision::Over); - SET_ENUM("Under", precision::Under); - SET_ENUM("UnderOver", precision::UnderOver); - lua_setglobal(L, "precision"); } } diff --git a/src/library/tactic/proof_state.h b/src/library/tactic/proof_state.h index 843d1e6c3..b92adaac4 100644 --- a/src/library/tactic/proof_state.h +++ b/src/library/tactic/proof_state.h @@ -12,7 +12,6 @@ Author: Leonardo de Moura #include "util/name_set.h" #include "library/tactic/goal.h" #include "library/tactic/proof_builder.h" -#include "library/tactic/cex_builder.h" namespace lean { typedef std::pair named_goal; @@ -20,47 +19,26 @@ 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); -enum class precision { - Precise, - Under, // counter-examples can be trusted - Over, // proofs can be trusted - UnderOver // proof_state is garbage: it was produced using under and over approximation steps. -}; - -precision mk_union(precision p1, precision p2); -bool trust_proof(precision p); -bool trust_cex(precision p); - class proof_state { - precision m_precision; goals m_goals; proof_builder m_proof_builder; - cex_builder m_cex_builder; name_generator m_ngen; list m_init_locals; public: - proof_state(precision prec, goals const & gs, proof_builder const & pb, cex_builder 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 const & pb, cex_builder 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 const & pb, cex_builder const & cb): - proof_state(s.m_precision, gs, pb, cb, s.m_ngen, s.m_init_locals) {} + 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(s.m_precision, gs, pb, s.m_cex_builder, ngen, s.m_init_locals) {} + 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_precision, s.m_goals, s.m_proof_builder, s.m_cex_builder, ngen, s.m_init_locals) {} - precision get_precision() const { return m_precision; } + proof_state(s.m_goals, s.m_proof_builder, ngen, s.m_init_locals) {} goals const & get_goals() const { return m_goals; } proof_builder const & get_pb() const { return m_proof_builder; } - cex_builder 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 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); } diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp index e47b94c04..040fed695 100644 --- a/src/library/tactic/tactic.cpp +++ b/src/library/tactic/tactic.cpp @@ -221,8 +221,7 @@ proof_state_seq focus_core(tactic const & t, name const & gname, environment con 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); }); - cex_builder cb = mk_cex_builder_for(gname); - proof_state new_s(s, goals(p), pb, cb); // new state with singleton goal + 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; @@ -254,17 +253,7 @@ proof_state_seq focus_core(tactic const & t, name const & gname, environment con m1.insert(gname, pb2(m2, a)); return pb1(m1, a); }); - cex_builder cb1 = s.get_cb(); - cex_builder cb2 = s2.get_cb(); - cex_builder new_cb = cex_builder( - [=](name const & n, optional const & cex, substitution const & a) -> counterexample { - for (auto p : renamed_goals) { - if (p.second == n) - return cb2(p.first, cex, a); - } - return cb1(n, cex, a); - }); - return proof_state(s2, new_gs, new_pb, new_cb); + return proof_state(s2, new_gs, new_pb); }); } }