From 0c185fc4ab25cc22ce6c4947892db8ef6cb36896 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 29 Oct 2014 08:57:34 -0700 Subject: [PATCH] fix(library/tactic): add relax_main_opaque flag to proof_state objects, closes #274 --- src/frontends/lean/elaborator.cpp | 11 ++++++++--- src/frontends/lean/elaborator.h | 2 ++ src/frontends/lean/util.cpp | 3 ++- src/library/tactic/apply_tactic.cpp | 22 +++++++++++----------- src/library/tactic/apply_tactic.h | 4 ++-- src/library/tactic/elaborate.cpp | 4 ++-- src/library/tactic/proof_state.cpp | 23 +++++++++++++---------- src/library/tactic/proof_state.h | 19 ++++++++++++++----- 8 files changed, 54 insertions(+), 34 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 3e898c155..b1fb2f6ff 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -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; diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 6aef63a43..c9ac94738 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -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. diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index fe2b30657..733269515 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -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); }); } diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index a9fe63399..cbe26953d 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -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 & 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 tc(mk_type_checker(env, ngen.mk_child(), relax_main_opaque)); + std::shared_ptr 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 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 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 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); }); } diff --git a/src/library/tactic/apply_tactic.h b/src/library/tactic/apply_tactic.h index 5a269694b..145238fc2 100644 --- a/src/library/tactic/apply_tactic.h +++ b/src/library/tactic/apply_tactic.h @@ -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(); diff --git a/src/library/tactic/elaborate.cpp b/src/library/tactic/elaborate.cpp index b33d2b1df..52439f628 100644 --- a/src/library/tactic/elaborate.cpp +++ b/src/library/tactic/elaborate.cpp @@ -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 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(); diff --git a/src/library/tactic/proof_state.cpp b/src/library/tactic/proof_state.cpp index 91d8b0592..4a7f537ce 100644 --- a/src/library/tactic/proof_state.cpp +++ b/src/library/tactic/proof_state.cpp @@ -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) { diff --git a/src/library/tactic/proof_state.h b/src/library/tactic/proof_state.h index 7a5189666..999d377f0 100644 --- a/src/library/tactic/proof_state.h +++ b/src/library/tactic/proof_state.h @@ -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 some_proof_state(proof_state const & s) { return some(s); } inline optional none_proof_state() { return optional (); } -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(goal const & g)> f); io_state_stream const & operator<<(io_state_stream const & out, proof_state const & s);