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

fix(library/tactic): compilation warning

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-29 10:35:14 -08:00
parent 98897b467d
commit 18eb9e427f
3 changed files with 14 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/parser.cpp
View file

@ -1063,7 +1063,7 @@ class parser::imp {
next();
if (id == g_apply) {
auto tac_pos = pos();
optional<tactic> t;
tactic t;
if (curr() == scanner::token::ScriptBlock) {
parse_script_expr();
m_script_state->apply([&](lua_State * L) {
@ -1084,7 +1084,7 @@ class parser::imp {
lua_pop(L, 1);
});
}
lazy_list<proof_state> seq = (*t)(m_frontend, m_frontend.get_state(), s);
lazy_list<proof_state> seq = t(m_frontend, m_frontend.get_state(), s);
auto r = seq.pull();
if (r) {
s = r->first;

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

@ -302,8 +302,9 @@ DECL_UDATA(tactic)
ORELSE(assumption_tactic(), conj_tactic())
*/
tactic to_tactic_ext(lua_State * L, int i) {
tactic t;
if (is_tactic(L, i)) {
return to_tactic(L, i);
t = to_tactic(L, i);
} else if (lua_isfunction(L, i)) {
try {
lua_pushvalue(L, i);
@ -312,15 +313,17 @@ tactic to_tactic_ext(lua_State * L, int i) {
throw_tactic_expected(i);
}
if (is_tactic(L, -1)) {
tactic t = to_tactic(L, -1);
t = to_tactic(L, -1);
lua_pop(L, 1);
return t;
} else {
throw_tactic_expected(i);
}
} else {
throw_tactic_expected(i);
}
if (!t)
throw exception(sstream() << "arg #" << i << " must be a nonnull tactic");
return t;
}
static void check_ios(io_state * ios) {

7
src/library/tactic/tactic.h
View file

@ -69,15 +69,20 @@ class tactic {
protected:
tactic_cell * m_ptr;
public:
tactic():m_ptr(nullptr) {}
explicit tactic(tactic_cell * ptr):m_ptr(ptr) { if (m_ptr) m_ptr->inc_ref(); }
tactic(tactic const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
tactic(tactic && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
~tactic() { if (m_ptr) m_ptr->dec_ref(); }
operator bool() const { return m_ptr != nullptr; }
friend void swap(tactic & a, tactic & b) { std::swap(a.m_ptr, b.m_ptr); }
tactic & operator=(tactic const & s);
tactic & operator=(tactic && s);
proof_state_seq operator()(environment const & env, io_state const & io, proof_state const & s) const { return m_ptr->operator()(env, io, s); }
proof_state_seq operator()(environment const & env, io_state const & io, proof_state const & s) const {
lean_assert(m_ptr);
return m_ptr->operator()(env, io, s);
}
solve_result solve(environment const & env, io_state const & io, proof_state const & s);
solve_result solve(environment const & env, io_state const & io, context const & ctx, expr const & t);