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

refactor(library/tactic): simplify proof_state

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-01 18:02:17 -07:00
parent 7abe2e7242
commit 2df92b0701
2 changed files with 6 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -69,7 +69,7 @@ proof_state to_proof_state(expr const & mvar, name_generator ngen) {
}
expr meta = mk_app(mvar, ls);
goals gs(goal(meta, t));
return proof_state(gs, substitution(), ngen, meta);
return proof_state(gs, substitution(), ngen);
}
static name g_tmp_prefix = name::mk_internal_unique_name();
@ -163,7 +163,7 @@ static int mk_proof_state(lua_State * L) {
} else if (nargs == 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_substitution(L, 3), to_name_generator(L, 4)));
return push_proof_state(L, proof_state(to_goals(L, 1), to_substitution(L, 2), to_name_generator(L, 3)));
} else {
throw exception("proof_state invalid number of arguments");
}
@ -191,7 +191,6 @@ 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_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);
@ -212,7 +211,6 @@ static const struct luaL_Reg proof_state_m[] = {
{"pp", safe_function<proof_state_pp>},
{"goals", safe_function<proof_state_get_goals>},
{"subst", safe_function<proof_state_get_subst>},
{"initial", safe_function<proof_state_get_initial>},
{"ngen", safe_function<proof_state_get_ngen>},
{"is_final_state", safe_function<proof_state_is_final_state>},
{0, 0}

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

@ -18,24 +18,16 @@ class proof_state {
goals m_goals;
substitution m_subst;
name_generator m_ngen;
// 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, 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(goals const & gs, substitution const & s, name_generator const & ngen):
m_goals(gs), m_subst(s), m_ngen(ngen) {}
proof_state(proof_state const & s, goals const & gs, substitution const & subst):proof_state(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) {}
proof_state(proof_state const & s, name_generator const & ngen):proof_state(s.m_goals, s.m_subst, ngen) {}
goals const & get_goals() const { return m_goals; }
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); }