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

refactor(library/tactic/cex_builder): simplify cex_builder

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-27 07:14:33 -07:00
parent b4e4c4d610
commit d84b745241
3 changed files with 29 additions and 128 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)
add_library(tactic goal.cpp cex_builder.cpp)
# proof_builder.cpp cex_builder.cpp
# proof_state.cpp tactic.cpp boolean_tactics.cpp apply_tactic.cpp

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

@ -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,78 +8,33 @@ Author: Leonardo de Moura
#include "util/script_state.h"
#include "util/luaref.h"
#include "library/kernel_bindings.h"
#include "library/tactic/proof_builder.h"
#include "library/tactic/cex_builder.h"
namespace lean {
cex_builder & cex_builder::operator=(cex_builder const & s) { LEAN_COPY_REF(s); }
cex_builder & cex_builder::operator=(cex_builder && s) { LEAN_MOVE_REF(s); }
cex_builder mk_cex_builder_for(name const & gname) {
return mk_cex_builder(
[=](name const & n, optional<counterexample> const & cex, assignment const &) -> counterexample {
cex_builder_fn mk_cex_builder_for(name const & gname) {
return cex_builder_fn([=](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;
});
}
DECL_UDATA(cex_builder)
static int mk_cex_builder(lua_State * L) {
script_state::weak_ref S = to_script_state(L).to_weak_ref();
luaL_checktype(L, 1, LUA_TFUNCTION); // user-fun
luaref ref(L, 1);
return push_cex_builder(L,
mk_cex_builder([=](name const & n, optional<counterexample> const & cex, assignment const & a) -> counterexample {
script_state S_copy(S);
optional<environment> r;
S_copy.exec_protected([&]() {
ref.push(); // push user-fun on the stack
push_name(L, n);
if (cex)
push_environment(L, *cex);
else
lua_pushnil(L);
push_assignment(L, a);
pcall(L, 3, 1, 0);
r = to_environment(L, -1);
lua_pop(L, 1);
});
return *r;
}));
}
static int cex_builder_call_core(lua_State * L, cex_builder b, name n, optional<counterexample> cex, assignment a) {
script_state S = to_script_state(L);
optional<environment> env;
S.exec_unprotected([&]() {
env = b(n, cex, a);
cex_builder_fn to_cex_builder(lua_State * L, int idx) {
luaL_checktype(L, idx, LUA_TFUNCTION); // user-fun
luaref f(L, idx);
return cex_builder_fn([=](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;
});
return push_environment(L, *env);
}
static int cex_builder_call(lua_State * L) {
if (is_environment(L, 3)) {
return cex_builder_call_core(L, to_cex_builder(L, 1), to_name_ext(L, 2), optional<counterexample>(to_environment(L, 3)), to_assignment(L, 4));
} else {
return cex_builder_call_core(L, to_cex_builder(L, 1), to_name_ext(L, 2), optional<counterexample>(), to_assignment(L, 4));
}
}
static const struct luaL_Reg cex_builder_m[] = {
{"__gc", cex_builder_gc}, // never throws
{"__call", safe_function<cex_builder_call>},
{0, 0}
};
void open_cex_builder(lua_State * L) {
luaL_newmetatable(L, cex_builder_mt);
lua_pushvalue(L, -1);
lua_setfield(L, -2, "__index");
setfuncs(L, cex_builder_m, 0);
SET_GLOBAL_FUN(cex_builder_pred, "is_cex_builder");
SET_GLOBAL_FUN(mk_cex_builder, "cex_builder");
}
}

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

@ -1,78 +1,24 @@
/*
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
*/
#pragma once
#include <algorithm>
#include <functional>
#include "util/lua.h"
#include "util/debug.h"
#include "util/name.h"
#include "util/rc.h"
#include "util/optional.h"
#include "kernel/expr.h"
#include "kernel/environment.h"
#include "library/tactic/assignment.h"
#include "kernel/metavar.h"
namespace lean {
/**
\brief In Lean, a counter-example is encoded using an environment object.
*/
/** \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_fn;
/** \brief Return a counterexample builder that expects a counterexample for the given goal. */
cex_builder_fn mk_cex_builder_for(name const & gname);
/**
\brief Base class for functors that build a counterexample for the main goal based on
a counterexample for a subgoal.
*/
class cex_builder_cell {
void dealloc() { delete this; }
MK_LEAN_RC();
public:
cex_builder_cell():m_rc(0) {}
virtual ~cex_builder_cell() {}
virtual counterexample operator()(name const & n, optional<counterexample> const & cex, assignment const & a) const = 0;
};
template<typename F>
class cex_builder_tpl : public cex_builder_cell {
F m_f;
public:
cex_builder_tpl(F && f):m_f(f) {}
virtual counterexample operator()(name const & n, optional<counterexample> const & cex, assignment const & a) const {
return m_f(n, cex, a);
}
};
/**
\brief Smart pointer for a counterexample builder functor.
*/
class cex_builder {
protected:
cex_builder_cell * m_ptr;
public:
cex_builder():m_ptr(nullptr) {}
explicit cex_builder(cex_builder_cell * ptr):m_ptr(ptr) { lean_assert(m_ptr); m_ptr->inc_ref(); }
cex_builder(cex_builder const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
cex_builder(cex_builder && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
~cex_builder() { if (m_ptr) m_ptr->dec_ref(); }
friend void swap(cex_builder & a, cex_builder & b) { std::swap(a.m_ptr, b.m_ptr); }
cex_builder & operator=(cex_builder const & s);
cex_builder & operator=(cex_builder && s);
counterexample operator()(name const & n, optional<counterexample> const & cex, assignment const & a) const { return m_ptr->operator()(n, cex, a); }
};
template<typename F>
cex_builder mk_cex_builder(F && f) {
return cex_builder(new cex_builder_tpl<F>(std::forward<F>(f)));
}
/**
\brief Return a counterexample builder that expects a counterexample for the given goal.
*/
cex_builder mk_cex_builder_for(name const & gname);
UDATA_DEFS(cex_builder)
void open_cex_builder(lua_State * L);
/** \brief Convert a Lua function on position \c idx (on the Lua stack) to a cex_builder_fn */
cex_builder_fn to_cex_builder(lua_State * L, int idx);
}