From 64f6601fe3613ed30fd5c6378cb4845575371d9e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 4 Oct 2014 09:15:42 -0700 Subject: [PATCH] fix(frontends/lean/proof_qed_elaborator): information about synthesized variables in a proof-qed block was being lost --- src/frontends/lean/elaborator.cpp | 7 ++- src/frontends/lean/proof_qed_elaborator.cpp | 8 ++- src/frontends/lean/proof_qed_elaborator.h | 8 ++- tests/lean/interactive/proof_qed.input | 3 + .../interactive/proof_qed.input.expected.out | 61 +++++++++++++++++++ tests/lean/interactive/proof_qed.lean | 14 +++++ 6 files changed, 97 insertions(+), 4 deletions(-) create mode 100644 tests/lean/interactive/proof_qed.input create mode 100644 tests/lean/interactive/proof_qed.input.expected.out create mode 100644 tests/lean/interactive/proof_qed.lean diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index ce625e7f2..782a92bfe 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -257,11 +257,14 @@ expr elaborator::visit_by(expr const & e, optional const & t, constraint_s expr elaborator::visit_proof_qed(expr const & e, optional const & t, constraint_seq & cs) { lean_assert(is_proof_qed_annotation(e)); + info_manager * im = nullptr; + if (infom()) + im = &m_pre_info_data; pair ecs = visit(get_annotation_arg(e)); expr m = m_full_context.mk_meta(m_ngen, t, e.get_tag()); register_meta(m); - constraint c = mk_proof_qed_cnstr(env(), m, ecs.first, ecs.second, - m_unifier_config, m_relax_main_opaque); + constraint c = mk_proof_qed_cnstr(env(), m, ecs.first, ecs.second, m_unifier_config, + im, m_relax_main_opaque); cs += c; return m; } diff --git a/src/frontends/lean/proof_qed_elaborator.cpp b/src/frontends/lean/proof_qed_elaborator.cpp index 5a739439e..3df7ccb32 100644 --- a/src/frontends/lean/proof_qed_elaborator.cpp +++ b/src/frontends/lean/proof_qed_elaborator.cpp @@ -8,12 +8,14 @@ Author: Leonardo de Moura #include "library/reducible.h" #include "library/metavar_closure.h" #include "frontends/lean/util.h" +#include "frontends/lean/info_manager.h" namespace lean { /** \brief Create a "choice" constraint that postpone the solving the constraints (cs union (m =?= e)). */ constraint mk_proof_qed_cnstr(environment const & env, expr const & m, expr const & e, - constraint_seq const & cs, unifier_config const & cfg, bool relax) { + constraint_seq const & cs, unifier_config const & cfg, + info_manager * im, bool relax) { justification j = mk_failed_to_synthesize_jst(env, m); auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s, name_generator const & _ngen) { @@ -45,6 +47,10 @@ constraint mk_proof_qed_cnstr(environment const & env, expr const & m, expr cons // we erase internal justifications return update_justification(c, j); }); + if (im) + im->instantiate(new_s); + // TODO(Leo): the solution new_s also assigns auxiliary metavariables + // that are needed to generate data for the info_manager constraints r = cls.mk_constraints(new_s, j, relax); return append(r, postponed); }; diff --git a/src/frontends/lean/proof_qed_elaborator.h b/src/frontends/lean/proof_qed_elaborator.h index c9d759f26..6d1febf4d 100644 --- a/src/frontends/lean/proof_qed_elaborator.h +++ b/src/frontends/lean/proof_qed_elaborator.h @@ -6,11 +6,17 @@ Author: Leonardo de Moura */ #pragma once #include "library/unifier.h" +#include "frontends/lean/info_manager.h" namespace lean { /** \brief Create a "choice" constraint that postpone the solving the constraints (cs union (m =?= e)). + + \remark A proof-qed block may instantiate meta-variables in the + info_manager. Thus, we provide the info_manager to make sure + this assignments are reflected on it. */ constraint mk_proof_qed_cnstr(environment const & env, expr const & m, expr const & e, - constraint_seq const & cs, unifier_config const & cfg, bool relax); + constraint_seq const & cs, unifier_config const & cfg, + info_manager * im, bool relax); } diff --git a/tests/lean/interactive/proof_qed.input b/tests/lean/interactive/proof_qed.input new file mode 100644 index 000000000..045d78dea --- /dev/null +++ b/tests/lean/interactive/proof_qed.input @@ -0,0 +1,3 @@ +VISIT proof_qed.lean +WAIT +INFO 11 \ No newline at end of file diff --git a/tests/lean/interactive/proof_qed.input.expected.out b/tests/lean/interactive/proof_qed.input.expected.out new file mode 100644 index 000000000..fd84ef4f9 --- /dev/null +++ b/tests/lean/interactive/proof_qed.input.expected.out @@ -0,0 +1,61 @@ +-- BEGINWAIT +-- ENDWAIT +-- BEGININFO +-- SYMBOL|11|4 +@ +-- ACK +-- TYPE|11|5 +∀ {A : Type} {a b c : A}, eq a b → eq b c → eq a c +-- ACK +-- IDENTIFIER|11|5 +eq.trans +-- ACK +-- TYPE|11|14 +Type +-- ACK +-- SYNTH|11|14 +A +-- ACK +-- SYMBOL|11|14 +_ +-- ACK +-- TYPE|11|16 +A +-- ACK +-- SYNTH|11|16 +a +-- ACK +-- SYMBOL|11|16 +_ +-- ACK +-- TYPE|11|18 +A +-- ACK +-- SYNTH|11|18 +b +-- ACK +-- SYMBOL|11|18 +_ +-- ACK +-- TYPE|11|20 +A +-- ACK +-- SYNTH|11|20 +c +-- ACK +-- SYMBOL|11|20 +_ +-- ACK +-- TYPE|11|22 +eq a b +-- ACK +-- IDENTIFIER|11|22 +H1 +-- ACK +-- TYPE|11|25 +eq b c +-- ACK +-- IDENTIFIER|11|25 +H2 +-- ACK +-- ENDINFO diff --git a/tests/lean/interactive/proof_qed.lean b/tests/lean/interactive/proof_qed.lean new file mode 100644 index 000000000..76839176a --- /dev/null +++ b/tests/lean/interactive/proof_qed.lean @@ -0,0 +1,14 @@ +import logic +open eq.ops +set_option pp.notation false +section + parameter {A : Type} + parameters {a b c d e : A} + theorem tst : a = b → b = c → c = d → d = e → a = e := + take H1 H2 H3 H4, + have e1 : a = c, + proof + @eq.trans _ _ _ _ H1 H2 + ∎, + e1 ⬝ H3 ⬝ H4 +end