michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/tactic): remove cex_builder and 'precision' for proof_state's

Browse source 
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 <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-30 08:48:01 -07:00
parent 8d584e54da
commit c2ab31113f
7 changed files with 14 additions and 144 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/tactic/CMakeLists.txt
View file

@ -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)

4
src/library/tactic/apply_tactic.cpp
View file

@ -39,9 +39,7 @@ bool collect_simple_metas(expr const & e, buffer<expr> & 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();

40
src/library/tactic/cex_builder.cpp
View file

@ -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<counterexample> 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<counterexample> 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;
});
}
}

24
src/library/tactic/cex_builder.h
View file

@ -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 <functional>
#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<counterexample(name const &, optional<counterexample> 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);
}

39
src/library/tactic/proof_state.cpp
View file

@ -42,16 +42,6 @@ optional<name> get_ith_goal_name(goals const & gs, unsigned i) {
return optional<name>();
}
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<optional<goal>(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<expr>(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<expr> 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<int>(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<counterexample> 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<proof_state_tostring>},
{"pp", safe_function<proof_state_pp>},
{"get_precision", safe_function<proof_state_get_precision>},
{"get_goals", safe_function<proof_state_get_goals>},
{"pb", safe_function<proof_state_apply_proof_builder>},
{"cb", safe_function<proof_state_apply_cex_builder>},
{"precision", safe_function<proof_state_get_precision>},
{"goals", safe_function<proof_state_get_goals>},
{"is_proof_final_state", safe_function<proof_state_is_proof_final_state>},
{"is_final_state", safe_function<proof_state_is_final_state>},
{"to_proof", safe_function<to_proof>},
{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");
}
}

34
src/library/tactic/proof_state.h
View file

@ -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<name, goal> named_goal;
@ -20,47 +19,26 @@ typedef list<named_goal> goals;
/** \brief Return the name of the i-th goal, return none if i == 0 or i > size(g) */
optional<name> 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<expr> m_init_locals;
public:
proof_state(precision prec, goals const & gs, proof_builder const & pb, cex_builder const & cb,
name_generator const & ngen, list<expr> const & ls = list<expr>()):
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<expr> const & ls = list<expr>()):
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<expr> const & ls = list<expr>()):
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<expr> 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<name> get_ith_goal_name(unsigned i) const { return ::lean::get_ith_goal_name(get_goals(), i); }

15
src/library/tactic/tactic.cpp
View file

@ -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<std::pair<name, name>> 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<counterexample> 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);
});
}
}