From 9935cbc3d7e25406dfdd7aefcf34aa9ab441f98a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 2 Jan 2016 20:05:44 -0800 Subject: [PATCH] feat(library/blast/blast): communicate assigned metavariables back to tactic framework We need this feature to be able to solve (input) goals containing metavariables using blast. See new test for example. --- src/library/blast/blast.cpp | 59 +++++++++++++++++++++--------- src/library/blast/blast.h | 4 +- src/library/blast/blast_tactic.cpp | 9 ++++- tests/lean/run/blast_meta.lean | 13 +++++++ 4 files changed, 63 insertions(+), 22 deletions(-) create mode 100644 tests/lean/run/blast_meta.lean diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp index 1dcac51017..d722dff5bf 100644 --- a/src/library/blast/blast.cpp +++ b/src/library/blast/blast.cpp @@ -474,7 +474,7 @@ class blastenv { m_initial_context = to_list(ctx); } - name_map mk_uref2uvar() { + name_map mk_uref2uvar() const { name_map r; m_uvar2uref.for_each([&](name const & uvar_id, level const & uref) { lean_assert(is_uref(uref)); @@ -483,7 +483,7 @@ class blastenv { return r; } - name_map mk_mref2meta() { + name_map mk_mref2meta() const { name_map r; m_mvar2meta_mref.for_each([&](name const &, pair const & p) { lean_assert(is_mref(p.second)); @@ -492,7 +492,7 @@ class blastenv { return r; } - level restore_uvars(level const & l, name_map const & uref2uvar) { + level restore_uvars(level const & l, name_map const & uref2uvar) const { return replace(l, [&](level const & l) { if (is_meta(l)) { if (auto uvar = uref2uvar.find(meta_id(l))) @@ -502,16 +502,12 @@ class blastenv { }); } - levels restore_uvars(levels const & ls, name_map const & uref2uvar) { + levels restore_uvars(levels const & ls, name_map const & uref2uvar) const { return map(ls, [&](level const & l) { return restore_uvars(l, uref2uvar); }); } /* Convert uref's and mref's back into tactic metavariables */ - expr restore_uvars_mvars(expr const & e) { - if (m_uvar2uref.empty()) - return e; - name_map uref2uvar = mk_uref2uvar(); - name_map mref2meta = mk_mref2meta(); + expr restore_uvars_mvars(expr const & e, name_map const & uref2uvar, name_map const & mref2meta) const { return replace(e, [&](expr const & e, unsigned) { if (is_mref(e)) { if (auto m = mref2meta.find(mlocal_name(e))) { @@ -529,7 +525,11 @@ class blastenv { }); } - expr to_tactic_proof(expr const & pr) { + level to_tactic_univ(level const & l, name_map const & uref2uvar) { + return restore_uvars(m_curr_state.instantiate_urefs(l), uref2uvar); + } + + expr to_tactic_expr(expr const & pr, name_map const & uref2uvar, name_map const & mref2meta) { // When a proof is found we must // 1- Remove all occurrences of href's from pr expr pr1 = unfold_hypotheses_ge(m_curr_state, pr, 0); @@ -537,11 +537,34 @@ class blastenv { // and convert unassigned meta-variables back into // tactic meta-variables. expr pr2 = m_curr_state.instantiate_urefs_mrefs(pr1); - expr pr3 = restore_uvars_mvars(pr2); - // TODO(Leo): - // 3- The external tactic meta-variables that have been instantiated - // by blast must also be communicated back to the tactic framework. - return pr3; + return restore_uvars_mvars(pr2, uref2uvar, mref2meta); + } + + + /* The external tactic meta-variables that have been instantiated + by blast must also be communicated back to the tactic framework. */ + constraint_seq mk_cnstrs_for_assignments(name_map const & uref2uvar, name_map const & mref2meta) { + constraint_seq r; + justification j = mk_justification("assigned by blast"); + m_uvar2uref.for_each([&](name const & uvar_id, level const & uref) { + lean_assert(is_uref(uref)); + if (auto v = m_curr_state.get_uref_assignment(uref)) { + r += mk_level_eq_cnstr(mk_meta_univ(uvar_id), to_tactic_univ(*v, uref2uvar), j); + } + }); + m_mvar2meta_mref.for_each([&](name const &, pair const & p) { + lean_assert(is_mref(p.second)); + if (auto v = m_curr_state.get_mref_assignment(p.second)) { + r += mk_eq_cnstr(p.first, to_tactic_expr(*v, uref2uvar, mref2meta), j); + } + }); + return r; + } + + pair to_tactic_proof(expr const & pr) { + name_map uref2uvar = mk_uref2uvar(); + name_map mref2meta = mk_mref2meta(); + return mk_pair(to_tactic_expr(pr, uref2uvar, mref2meta), mk_cnstrs_for_assignments(uref2uvar, mref2meta)); } public: @@ -597,7 +620,7 @@ public: init_classical_flag(); } - expr operator()(goal const & g) { + pair operator()(goal const & g) { init_state(g); if (auto r = apply_strategy()) { return to_tactic_proof(*r); @@ -1244,8 +1267,8 @@ expr internalize(expr const & e) { return g_blastenv->internalize(e); } } -expr blast_goal(environment const & env, io_state const & ios, list const & ls, list const & ds, - goal const & g) { +pair blast_goal(environment const & env, io_state const & ios, list const & ls, list const & ds, + goal const & g) { scoped_expr_caching scope1(true); blast::blastenv b(env, ios, ls, ds); blast::scope_blastenv scope2(b); diff --git a/src/library/blast/blast.h b/src/library/blast/blast.h index 4ea0e0a953..cf231077f9 100644 --- a/src/library/blast/blast.h +++ b/src/library/blast/blast.h @@ -251,8 +251,8 @@ public: \remark This procedure should only be used for **debugging purposes**. */ expr internalize(expr const & e); } -expr blast_goal(environment const & env, io_state const & ios, list const & ls, list const & ds, - goal const & g); +pair blast_goal(environment const & env, io_state const & ios, list const & ls, list const & ds, + goal const & g); void initialize_blast(); void finalize_blast(); } diff --git a/src/library/blast/blast_tactic.cpp b/src/library/blast/blast_tactic.cpp index 8bbdfb1407..b9c16ab58b 100644 --- a/src/library/blast/blast_tactic.cpp +++ b/src/library/blast/blast_tactic.cpp @@ -19,11 +19,16 @@ tactic mk_blast_tactic(list const & ls, list const & ds) { } goal const & g = head(gs); try { - expr pr = blast_goal(env, ios, ls, ds, g); + pair pr_cs = blast_goal(env, ios, ls, ds, g); + expr pr = pr_cs.first; + constraint_seq cs = pr_cs.second; goals new_gs = tail(gs); substitution new_subst = s.get_subst(); assign(new_subst, g, pr); - return some_proof_state(proof_state(s, new_gs, new_subst)); + proof_state new_ps(s, new_gs, new_subst); + if (solve_constraints(env, ios, new_ps, cs)) + return some_proof_state(new_ps); + return none_proof_state(); } catch (blast_exception & ex) { throw_tactic_exception_if_enabled(s, ex.what()); return none_proof_state(); diff --git a/tests/lean/run/blast_meta.lean b/tests/lean/run/blast_meta.lean new file mode 100644 index 0000000000..be6ccb0b02 --- /dev/null +++ b/tests/lean/run/blast_meta.lean @@ -0,0 +1,13 @@ +constant p : nat → nat → Prop + +constant p_trans : ∀ a b c, p a b → p b c → p a c + +definition lemma1 (a b c d : nat) : a = d → p b c → p a b → p a c := +begin + intros, + apply p_trans, + blast, + blast +end + +print lemma1