diff --git a/src/library/blast/CMakeLists.txt b/src/library/blast/CMakeLists.txt index 37af36449..e4749b7f1 100644 --- a/src/library/blast/CMakeLists.txt +++ b/src/library/blast/CMakeLists.txt @@ -1,2 +1,2 @@ -add_library(blast OBJECT expr.cpp state.cpp blast.cpp - blast_tactic.cpp init_module.cpp simplifier.cpp assumption.cpp intros.cpp) +add_library(blast OBJECT expr.cpp state.cpp blast.cpp blast_tactic.cpp + init_module.cpp simplifier.cpp assumption.cpp intros.cpp proof_expr.cpp) diff --git a/src/library/blast/assumption.cpp b/src/library/blast/assumption.cpp index e19ae45c5..5e7ba005c 100644 --- a/src/library/blast/assumption.cpp +++ b/src/library/blast/assumption.cpp @@ -18,12 +18,7 @@ optional assumption_action() { }); if (!hidx) return none_expr(); - // TODO(Leo): cleanup hypothesis const * h = s.get_hypothesis_decl(*hidx); - if (h->get_value()) { - return some_expr(*h->get_value()); - } else { - return some_expr(mk_href(*hidx)); - } + return some_expr(h->get_self()); } }} diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp index 14de70231..a192f1f0f 100644 --- a/src/library/blast/blast.cpp +++ b/src/library/blast/blast.cpp @@ -23,6 +23,7 @@ Author: Leonardo de Moura #include "library/blast/blast.h" #include "library/blast/assumption.h" #include "library/blast/intros.h" +#include "library/blast/proof_expr.h" #include "library/blast/blast_exception.h" #ifndef LEAN_DEFAULT_BLAST_MAX_DEPTH @@ -494,43 +495,18 @@ class blastenv { return none_expr(); } - struct to_tactic_proof_fn : public replace_visitor { - state & m_state; - - virtual expr visit_local(expr const & e) { - // TODO(Leo): cleanup - if (is_href(e)) { - hypothesis const * h = m_state.get_hypothesis_decl(e); - if (auto r = h->get_value()) { - return visit(*r); - } - } - return replace_visitor::visit_local(e); - } - - virtual expr visit_meta(expr const & e) { - lean_assert(is_mref(e)); - expr v = m_state.instantiate_urefs_mrefs(e); - if (v == e) { - return v; - } else { - return replace_visitor::visit_meta(v); - } - } - - to_tactic_proof_fn(state & s): - m_state(s) {} - }; - expr to_tactic_proof(expr const & pr) { - // TODO(Leo): when a proof is found we must - // 1- (done) remove all occurrences of href's from pr - // 2- (done) replace mrefs with their assignments, + // 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); + // 2- Replace mrefs with their assignments, // and convert unassigned meta-variables back into // tactic meta-variables. + expr pr2 = m_curr_state.instantiate_urefs_mrefs(pr1); + // TODO(Leo): // 3- The external tactic meta-variables that have been instantiated // by blast must also be communicated back to the tactic framework. - return to_tactic_proof_fn(m_curr_state)(pr); + return pr2; } public: diff --git a/src/library/blast/hypothesis.h b/src/library/blast/hypothesis.h index 345e22309..373241c05 100644 --- a/src/library/blast/hypothesis.h +++ b/src/library/blast/hypothesis.h @@ -28,6 +28,7 @@ class hypothesis { unsigned m_dep_depth; // dependency depth unsigned m_proof_depth; // proof depth when the hypothesis was created hypothesis_idx_set m_deps; // hypotheses used by the type and/or value of this hypothesis. + expr m_self; expr m_type; optional m_value; // justification for this object. // Remark: if blast::is_local(m_value) is true, then the hypothesis is an assumption @@ -38,6 +39,7 @@ public: unsigned get_dep_depth() const { return m_dep_depth; } unsigned get_proof_depth() const { return m_proof_depth; } hypothesis_idx_set const & get_backward_deps() const { return m_deps; } + expr const & get_self() const { return m_self; } expr const & get_type() const { return m_type; } optional const & get_value() const { return m_value; } /** \brief Return true iff this hypothesis depends on \c h. */ diff --git a/src/library/blast/intros.cpp b/src/library/blast/intros.cpp index 8ae1ec726..1d4ece5ad 100644 --- a/src/library/blast/intros.cpp +++ b/src/library/blast/intros.cpp @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include "kernel/abstract.h" #include "kernel/instantiate.h" #include "library/blast/blast.h" +#include "library/blast/proof_expr.h" namespace lean { namespace blast { @@ -14,7 +15,7 @@ struct intros_proof_step_cell : public proof_step_cell { list m_new_hs; virtual ~intros_proof_step_cell() {} virtual optional resolve(state & s, expr const & pr) const { - expr new_pr = s.mk_lambda(m_new_hs, pr); + expr new_pr = mk_proof_lambda(s, m_new_hs, unfold_hypotheses_ge(s, pr)); return some_expr(new_pr); } }; diff --git a/src/library/blast/proof_expr.cpp b/src/library/blast/proof_expr.cpp new file mode 100644 index 000000000..1b12f4ca7 --- /dev/null +++ b/src/library/blast/proof_expr.cpp @@ -0,0 +1,50 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "library/replace_visitor.h" +#include "library/blast/blast.h" +#include "library/blast/proof_expr.h" + +namespace lean { +namespace blast { +expr to_proof_expr(expr const & e) { + return e; +} + +struct unfold_hypotheses_ge_fn : public replace_visitor { + state const & m_state; + unsigned m_depth; + + unfold_hypotheses_ge_fn(state const & s, unsigned d): + m_state(s), m_depth(d) {} + + virtual expr visit_local(expr const & e) { + if (is_href(e)) { + hypothesis const * h = m_state.get_hypothesis_decl(e); + if (h->get_proof_depth() >= m_depth && h->get_value()) { + return visit(*h->get_value()); + } + } + return replace_visitor::visit_local(e); + } +}; + +expr unfold_hypotheses_ge(state const & s, expr const & pr, unsigned d) { + return unfold_hypotheses_ge_fn(s, d)(pr); +} + +expr mk_proof_lambda(state const & s, list const & hs, expr const & pr) { + return s.mk_lambda(hs, pr); +} + +expr mk_proof_app(name const & fname, unsigned nargs, expr const * args) { + return get_app_builder().mk_app(fname, nargs, args); +} + +expr mk_proof_app(expr const & f, unsigned nargs, expr const * args) { + return mk_app(f, nargs, args); +} +}} diff --git a/src/library/blast/proof_expr.h b/src/library/blast/proof_expr.h new file mode 100644 index 000000000..a1cbd02a8 --- /dev/null +++ b/src/library/blast/proof_expr.h @@ -0,0 +1,35 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "library/blast/state.h" + +namespace lean { +namespace blast { +/* + This module provides a thin layer for creating proof terms at proof-step resolve. + The idea is to allow us to refactor the code in the future, and implement + more efficient ways of representing proof terms. + + One current performance bottleneck is unfold_hypotheses_ge. +*/ + +/** \brief This is currently a noop. */ +expr to_proof_expr(expr const & e); + +/** \brief Unfold hrefs occurring in \c pr that have a value and were created + at proof depth >= d */ +expr unfold_hypotheses_ge(state const & s, expr const & pr, unsigned d); +inline expr unfold_hypotheses_ge(state const & s, expr const & pr) { + return unfold_hypotheses_ge(s, pr, s.get_proof_depth()); +} + +/** \brief Create an lambda abstraction. */ +expr mk_proof_lambda(state const & s, list const & hs, expr const & pr); + +/** \brief Create an application using the app_builder */ +expr mk_proof_app(name const & fname, unsigned nargs, expr const * args); +expr mk_proof_app(expr const & f, unsigned nargs, expr const * args); +}} diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp index e522cad63..98183cecb 100644 --- a/src/library/blast/state.cpp +++ b/src/library/blast/state.cpp @@ -429,9 +429,11 @@ double state::compute_weight(unsigned hidx, expr const & /* type */) { expr state::mk_hypothesis(unsigned new_hidx, name const & n, expr const & type, optional const & value) { hypothesis new_h; + expr r = mk_href(new_hidx); new_h.m_name = n; new_h.m_type = type; new_h.m_value = value; + new_h.m_self = r; new_h.m_proof_depth = m_proof_depth; add_deps(new_h, new_hidx); m_hyp_decls.insert(new_hidx, new_h); @@ -439,7 +441,7 @@ expr state::mk_hypothesis(unsigned new_hidx, name const & n, expr const & type, m_assumption.insert(new_hidx); double w = compute_weight(new_hidx, type); m_todo_queue.insert(w, new_hidx); - return blast::mk_href(new_hidx); + return r; } expr state::mk_hypothesis(name const & n, expr const & type, expr const & value) {