fix(library/tactic): add relax_main_opaque flag to proof_state objects, closes #274

This commit is contained in:
Leonardo de Moura 2014-10-29 08:57:34 -07:00
parent a2ef835809
commit 0c185fc4ab
8 changed files with 54 additions and 34 deletions

View file

@ -108,7 +108,10 @@ expr elaborator::mk_local(name const & n, expr const & t, binder_info const & bi
void elaborator::register_meta(expr const & meta) {
lean_assert(is_meta(meta));
m_mvar2meta.insert(mlocal_name(get_app_fn(meta)), meta);
name const & n = mlocal_name(get_app_fn(meta));
m_mvar2meta.insert(n, meta);
if (m_relax_main_opaque)
m_relaxed_mvars.insert(n);
}
/** \brief Convert the metavariable to the metavariable application that captures
@ -1058,7 +1061,8 @@ void elaborator::solve_unassigned_mvar(substitution & subst, expr mvar, name_set
expr type = m_tc[m_relax_main_opaque]->infer(*meta).first;
// first solve unassigned metavariables in type
type = solve_unassigned_mvars(subst, type, visited);
proof_state ps = to_proof_state(*meta, type, subst, m_ngen.mk_child());
bool relax_main_opaque = m_relaxed_mvars.contains(mlocal_name(mvar));
proof_state ps = to_proof_state(*meta, type, subst, m_ngen.mk_child(), relax_main_opaque);
if (auto pre_tac = get_pre_tactic_for(subst, mvar, visited)) {
if (is_begin_end_annotation(*pre_tac)) {
try_using_begin_end(subst, mvar, ps, *pre_tac);
@ -1109,7 +1113,8 @@ void elaborator::display_unassigned_mvars(expr const & e, substitution const & s
expr meta = tmp_s.instantiate(*it);
expr meta_type = tmp_s.instantiate(type_checker(env()).infer(meta).first);
goal g(meta, meta_type);
proof_state ps(goals(g), s, m_ngen, constraints());
bool relax = true;
proof_state ps(goals(g), s, m_ngen, constraints(), relax);
display_unsolved_proof_state(e, ps, "don't know how to synthesize placeholder");
}
return false;

View file

@ -35,6 +35,8 @@ class elaborator : public coercion_info_manager {
local_context m_context; // current local context: a list of local constants
local_context m_full_context; // superset of m_context, it also contains non-contextual locals.
mvar2meta m_mvar2meta;
// Set of metavariable that where created when m_relax_main_opaque flag is set to true.
name_set m_relaxed_mvars;
cache m_cache;
// The following vector contains sorts that we should check
// whether the computed universe is too specific or not.

View file

@ -322,7 +322,8 @@ justification mk_failed_to_synthesize_jst(environment const & env, expr const &
substitution tmp(subst);
expr new_m = instantiate_meta(m, tmp);
expr new_type = type_checker(env).infer(new_m).first;
proof_state ps = to_proof_state(new_m, new_type, name_generator("dontcare"));
bool relax_main_opaque = true; // this value doesn't really matter for pretty printing
proof_state ps = to_proof_state(new_m, new_type, name_generator("dontcare"), relax_main_opaque);
return format("failed to synthesize placeholder") + line() + ps.pp(fmt);
});
}

View file

@ -55,12 +55,12 @@ enum subgoals_action_kind { IgnoreSubgoals, AddRevSubgoals, AddSubgoals };
static proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s,
expr const & _e, buffer<constraint> & cs,
bool add_meta, subgoals_action_kind subgoals_action, bool relax_main_opaque) {
bool add_meta, subgoals_action_kind subgoals_action) {
goals const & gs = s.get_goals();
if (empty(gs))
return proof_state_seq();
name_generator ngen = s.get_ngen();
std::shared_ptr<type_checker> tc(mk_type_checker(env, ngen.mk_child(), relax_main_opaque));
std::shared_ptr<type_checker> tc(mk_type_checker(env, ngen.mk_child(), s.relax_main_opaque()));
goal g = head(gs);
goals tail_gs = tail(gs);
expr t = g.get_type();
@ -86,7 +86,7 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const
}
}
metavar_closure cls(t);
cls.mk_constraints(s.get_subst(), justification(), relax_main_opaque);
cls.mk_constraints(s.get_subst(), justification(), s.relax_main_opaque());
pair<bool, constraint_seq> dcs = tc->is_def_eq(t, e_t);
if (!dcs.first)
return proof_state_seq();
@ -123,17 +123,17 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const
}
}
}
return proof_state(new_gs, new_subst, new_ngen, postponed);
return proof_state(s, new_gs, new_subst, new_ngen, postponed);
});
}
static proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & e,
bool add_meta, subgoals_action_kind subgoals_action, bool relax_main_opaque) {
bool add_meta, subgoals_action_kind subgoals_action) {
buffer<constraint> cs;
return apply_tactic_core(env, ios, s, e, cs, add_meta, subgoals_action, relax_main_opaque);
return apply_tactic_core(env, ios, s, e, cs, add_meta, subgoals_action);
}
tactic eassumption_tactic(bool relax_main_opaque) {
tactic eassumption_tactic() {
return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
goals const & gs = s.get_goals();
if (empty(gs))
@ -143,13 +143,13 @@ tactic eassumption_tactic(bool relax_main_opaque) {
buffer<expr> hs;
get_app_args(g.get_meta(), hs);
for (expr const & h : hs) {
r = append(r, apply_tactic_core(env, ios, s, h, false, IgnoreSubgoals, relax_main_opaque));
r = append(r, apply_tactic_core(env, ios, s, h, false, IgnoreSubgoals));
}
return r;
});
}
tactic apply_tactic(elaborate_fn const & elab, expr const & e, bool rev, bool relax_main_opaque) {
tactic apply_tactic(elaborate_fn const & elab, expr const & e, bool rev) {
return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
goals const & gs = s.get_goals();
if (empty(gs))
@ -162,8 +162,8 @@ tactic apply_tactic(elaborate_fn const & elab, expr const & e, bool rev, bool re
new_e = ecs.first;
to_buffer(ecs.second, cs);
to_buffer(s.get_postponed(), cs);
proof_state new_s(s.get_goals(), s.get_subst(), ngen, constraints());
return apply_tactic_core(env, ios, new_s, new_e, cs, true, rev ? AddRevSubgoals : AddSubgoals, relax_main_opaque);
proof_state new_s(s, ngen, constraints());
return apply_tactic_core(env, ios, new_s, new_e, cs, true, rev ? AddRevSubgoals : AddSubgoals);
});
}

View file

@ -8,8 +8,8 @@ Author: Leonardo de Moura
#include "util/lua.h"
#include "library/tactic/elaborate.h"
namespace lean {
tactic apply_tactic(elaborate_fn const & fn, expr const & e, bool rev_goals = false, bool relax_main_opaque = true);
tactic eassumption_tactic(bool relax_main_opaque = true);
tactic apply_tactic(elaborate_fn const & fn, expr const & e, bool rev_goals = false);
tactic eassumption_tactic();
void open_apply_tactic(lua_State * L);
void initialize_apply_tactic();
void finalize_apply_tactic();

View file

@ -22,7 +22,7 @@ bool solve_constraints(environment const & env, io_state const & ios, proof_stat
if (auto p = rseq.pull()) {
substitution new_subst = p->first.first;
constraints new_postponed = p->first.second;
ps = proof_state(ps.get_goals(), new_subst, ngen, new_postponed);
ps = proof_state(ps, ps.get_goals(), new_subst, ngen, new_postponed);
return true;
} else {
return false;
@ -62,7 +62,7 @@ optional<expr> elaborate_with_respect_to(environment const & env, io_state const
substitution new_subst = p->first.first;
constraints new_postponed = p->first.second;
new_e = new_subst.instantiate(new_e);
s = proof_state(gs, new_subst, ngen, new_postponed);
s = proof_state(s, gs, new_subst, ngen, new_postponed);
return some_expr(new_e);
} else {
return none_expr();

View file

@ -30,9 +30,9 @@ bool get_proof_state_goal_names(options const & opts) {
return opts.get_bool(*g_proof_state_goal_names, LEAN_PROOF_STATE_GOAL_NAMES);
}
proof_state::proof_state(goals const & gs, substitution const & s,
name_generator const & ngen, constraints const & postponed):
m_goals(gs), m_subst(s), m_ngen(ngen), m_postponed(postponed) {
proof_state::proof_state(goals const & gs, substitution const & s, name_generator const & ngen,
constraints const & postponed, bool relax_main_opaque):
m_goals(gs), m_subst(s), m_ngen(ngen), m_postponed(postponed), m_relax_main_opaque(relax_main_opaque) {
if (std::any_of(gs.begin(), gs.end(),
[&](goal const & g) { return s.is_assigned(g.get_mvar()); })) {
m_goals = filter(gs, [&](goal const & g) { return !s.is_assigned(g.get_mvar()); });
@ -77,12 +77,13 @@ io_state_stream const & operator<<(io_state_stream const & out, proof_state cons
return out;
}
proof_state to_proof_state(expr const & meta, expr const & type, substitution const & subst, name_generator ngen) {
return proof_state(goals(goal(meta, type)), subst, ngen, constraints());
proof_state to_proof_state(expr const & meta, expr const & type, substitution const & subst, name_generator ngen,
bool relax_main_opaque) {
return proof_state(goals(goal(meta, type)), subst, ngen, constraints(), relax_main_opaque);
}
proof_state to_proof_state(expr const & meta, expr const & type, name_generator ngen) {
return to_proof_state(meta, type, substitution(), ngen);
proof_state to_proof_state(expr const & meta, expr const & type, name_generator ngen, bool relax_main_opaque) {
return to_proof_state(meta, type, substitution(), ngen, relax_main_opaque);
}
DECL_UDATA(goals)
@ -165,8 +166,9 @@ static int mk_proof_state(lua_State * L) {
} else if (nargs == 3 && is_proof_state(L, 1)) {
return push_proof_state(L, proof_state(to_proof_state(L, 1), to_goals(L, 2), to_substitution(L, 3)));
} else if (nargs == 3) {
bool relax_main_opaque = true;
return push_proof_state(L, proof_state(to_goals(L, 1), to_substitution(L, 2), to_name_generator(L, 3),
constraints()));
constraints(), relax_main_opaque));
} else {
throw exception("proof_state invalid number of arguments");
}
@ -175,10 +177,11 @@ static int mk_proof_state(lua_State * L) {
static name * g_tmp_prefix = nullptr;
static int to_proof_state(lua_State * L) {
int nargs = lua_gettop(L);
bool relax_main_opaque = true;
if (nargs == 2)
return push_proof_state(L, to_proof_state(to_expr(L, 1), to_expr(L, 2), name_generator(*g_tmp_prefix)));
return push_proof_state(L, to_proof_state(to_expr(L, 1), to_expr(L, 2), name_generator(*g_tmp_prefix), relax_main_opaque));
else
return push_proof_state(L, to_proof_state(to_expr(L, 1), to_expr(L, 2), to_name_generator(L, 3)));
return push_proof_state(L, to_proof_state(to_expr(L, 1), to_expr(L, 2), to_name_generator(L, 3), relax_main_opaque));
}
static int proof_state_tostring(lua_State * L) {

View file

@ -20,23 +20,31 @@ class proof_state {
substitution m_subst;
name_generator m_ngen;
constraints m_postponed;
bool m_relax_main_opaque;
public:
proof_state(goals const & gs, substitution const & s, name_generator const & ngen, constraints const & postponed);
proof_state(goals const & gs, substitution const & s, name_generator const & ngen, constraints const & postponed,
bool relax_main_opaque);
proof_state(proof_state const & s, goals const & gs, substitution const & subst, name_generator const & ngen,
constraints const & postponed):
proof_state(gs, subst, ngen, postponed, s.relax_main_opaque()) {}
proof_state(proof_state const & s, goals const & gs, substitution const & subst, name_generator const & ngen):
proof_state(gs, subst, ngen, s.m_postponed) {}
proof_state(gs, subst, ngen, s.m_postponed, s.m_relax_main_opaque) {}
proof_state(proof_state const & s, goals const & gs, substitution const & subst):
proof_state(s, gs, subst, s.m_ngen) {}
proof_state(proof_state const & s, goals const & gs, name_generator const & ngen):
proof_state(s, gs, s.m_subst, 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, constraints const & postponed):
proof_state(s.m_goals, s.m_subst, ngen, postponed, s.m_relax_main_opaque) {}
proof_state(proof_state const & s, name_generator const & ngen):
proof_state(s.m_goals, s.m_subst, ngen, s.m_postponed) {}
proof_state(s, ngen, s.m_postponed) {}
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; }
constraints const & get_postponed() const { return m_postponed; }
bool relax_main_opaque() const { return m_relax_main_opaque; }
/** \brief Return true iff this state does not have any goals left */
bool is_final_state() const { return empty(m_goals); }
@ -46,8 +54,9 @@ public:
inline optional<proof_state> some_proof_state(proof_state const & s) { return some(s); }
inline optional<proof_state> none_proof_state() { return optional<proof_state> (); }
proof_state to_proof_state(expr const & meta, expr const & type, substitution const & subst, name_generator ngen);
proof_state to_proof_state(expr const & meta, expr const & type, name_generator ngen);
proof_state to_proof_state(expr const & meta, expr const & type, substitution const & subst, name_generator ngen,
bool relax_main_opaque);
proof_state to_proof_state(expr const & meta, expr const & type, name_generator ngen, bool relax_main_opaque);
goals map_goals(proof_state const & s, std::function<optional<goal>(goal const & g)> f);
io_state_stream const & operator<<(io_state_stream const & out, proof_state const & s);