From 3f751c170b05cf323a2afcbb3b9cf4fe60a5331b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 28 Sep 2015 17:39:30 -0700 Subject: [PATCH] feat(library/blast): finish goal -> state translation --- src/library/blast/blast.cpp | 4 +- src/library/blast/branch.cpp | 94 +++++++++++++++++++++++++++++++ src/library/blast/branch.h | 27 +++++++-- src/library/blast/init_module.cpp | 7 ++- src/library/blast/state.h | 17 ++++++ 5 files changed, 140 insertions(+), 9 deletions(-) diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp index 2bf538a06..7cbe2af99 100644 --- a/src/library/blast/blast.cpp +++ b/src/library/blast/blast.cpp @@ -188,10 +188,12 @@ class context { buffer hs; g.get_hyps(hs); for (expr const & h : hs) { + lean_assert(is_local(h)); expr new_type = to_blast_expr(mlocal_type(h)); - // TODO(Leo): create hypothesis using new_type + s.add_hypothesis(local_pp_name(h), new_type, none_expr(), some_expr(h)); } expr new_target = to_blast_expr(g.get_type()); + s.set_target(new_target); init_mvar2mref(mvar2meta_mref); return s; } diff --git a/src/library/blast/branch.cpp b/src/library/blast/branch.cpp index f8d4b9160..2b339c808 100644 --- a/src/library/blast/branch.cpp +++ b/src/library/blast/branch.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "kernel/for_each_fn.h" #include "library/blast/branch.h" namespace lean { @@ -32,4 +33,97 @@ void branch::get_sorted_hypotheses(hypothesis_idx_buffer & r) { }); std::sort(r.begin(), r.end(), hypothesis_depth_lt(*this)); } + +void branch::add_forward_dep(unsigned hidx_user, unsigned hidx_provider) { + if (auto s = m_forward_deps.find(hidx_provider)) { + if (!s->contains(hidx_user)) { + hypothesis_idx_set new_s(*s); + new_s.insert(hidx_user); + m_forward_deps.insert(hidx_provider, new_s); + } + } else { + hypothesis_idx_set new_s; + new_s.insert(hidx_user); + m_forward_deps.insert(hidx_provider, new_s); + } +} + +void branch::add_deps(expr const & e, hypothesis & h_user, unsigned hidx_user) { + if (!has_lref(e) && !has_mref(e)) + return; // nothing to be done + for_each(e, [&](expr const & l, unsigned) { + if (!has_lref(l) && !has_mref(l)) { + return false; + } else if (is_lref(l)) { + unsigned hidx_provider = lref_index(l); + hypothesis const * h_provider = get(hidx_provider); + lean_assert(h_provider); + if (h_user.m_depth <= h_provider->m_depth) + h_user.m_depth = h_provider->m_depth + 1; + if (!h_user.m_deps.contains(hidx_provider)) { + h_user.m_deps.insert(hidx_provider); + add_forward_dep(hidx_user, hidx_provider); + } + return false; + } else if (is_mref(l)) { + m_mvars.insert(mref_index(l)); + return false; + } else { + return true; + } + }); +} + +void branch::add_deps(hypothesis & h_user, unsigned hidx_user) { + add_deps(h_user.m_type, h_user, hidx_user); + if (h_user.m_value) + add_deps(*h_user.m_value, h_user, hidx_user); +} + +expr branch::add_hypothesis(name const & n, expr const & type, optional const & value, optional const & jst) { + hypothesis new_h; + new_h.m_name = n; + new_h.m_type = type; + new_h.m_value = value; + new_h.m_justification = jst; + unsigned new_hidx = m_next; + m_next++; + add_deps(new_h, new_hidx); + m_context.insert(new_hidx, new_h); + return blast::mk_lref(new_hidx); +} + +static name * g_prefix = nullptr; + +expr branch::add_hypothesis(expr const & type, optional const & value, optional const & jst) { + return add_hypothesis(name(*g_prefix, m_next), type, value, jst); +} + +void branch::set_target(expr const & t) { + m_target = t; + m_target_deps.clear(); + if (has_lref(t) || has_mref(t)) { + for_each(t, [&](expr const & e, unsigned) { + if (!has_lref(e) && !has_mref(e)) { + return false; + } else if (is_lref(e)) { + m_target_deps.insert(lref_index(e)); + return false; + } else if (is_mref(e)) { + m_mvars.insert(mref_index(e)); + return false; + } else { + return true; + } + }); + } +} + +void initialize_branch() { + g_prefix = new name(name::mk_internal_unique_name()); +} + +void finalize_branch() { + delete g_prefix; +} }} diff --git a/src/library/blast/branch.h b/src/library/blast/branch.h index b9fa3058f..0797ccad4 100644 --- a/src/library/blast/branch.h +++ b/src/library/blast/branch.h @@ -15,13 +15,14 @@ typedef rb_tree metavar_set; class branch { typedef rb_map context; - typedef rb_map dependencies; + typedef rb_map forward_deps; friend class state; - unsigned m_next; - context m_context; - dependencies m_forward_deps; - expr m_target; - metavar_set m_mvars; + unsigned m_next; + context m_context; + forward_deps m_forward_deps; // given an entry (h -> {h_1, ..., h_n}), we have that each h_i uses h. + expr m_target; + hypothesis_idx_set m_target_deps; + metavar_set m_mvars; /** \brief Mark a hypothesis as fixed. The type/value of a fixed hypothesis cannot be modified. A hypothesis is fixed when it occurs in the type of some metavariable. */ @@ -30,14 +31,28 @@ class branch { lean_assert(is_lref(e)); fix_hypothesis(lref_index(e)); } + + void add_forward_dep(unsigned hidx_user, unsigned hidx_provider); + void add_deps(expr const & e, hypothesis & h_user, unsigned hidx_user); + void add_deps(hypothesis & h_user, unsigned hidx_user); + public: branch():m_next(0) {} /** \brief Store in \c r the hypotheses in this branch sorted by depth */ void get_sorted_hypotheses(hypothesis_idx_buffer & r); + + expr add_hypothesis(name const & n, expr const & type, optional const & value, optional const & jst); + expr add_hypothesis(expr const & type, optional const & value, optional const & jst); + + void set_target(expr const & t); + hypothesis const * get(unsigned idx) const { return m_context.find(idx); } hypothesis const * get(expr const & e) const { lean_assert(is_lref(e)); return get(lref_index(e)); } }; + +void initialize_branch(); +void finalize_branch(); }} diff --git a/src/library/blast/init_module.cpp b/src/library/blast/init_module.cpp index c2f021ab7..db2812a59 100644 --- a/src/library/blast/init_module.cpp +++ b/src/library/blast/init_module.cpp @@ -5,18 +5,21 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "library/blast/expr.h" +#include "library/blast/branch.h" #include "library/blast/blast.h" #include "library/blast/blast_tactic.h" namespace lean { void initialize_blast_module() { blast::initialize_expr(); + blast::initialize_branch(); initialize_blast(); initialize_blast_tactic(); } void finalize_blast_module() { - blast::finalize_expr(); - finalize_blast(); finalize_blast_tactic(); + finalize_blast(); + blast::finalize_branch(); + blast::finalize_expr(); } } diff --git a/src/library/blast/state.h b/src/library/blast/state.h index e4574f951..f9aac5421 100644 --- a/src/library/blast/state.h +++ b/src/library/blast/state.h @@ -42,7 +42,24 @@ public: The context of this metavariable will be all hypotheses occurring in the main branch. */ expr mk_metavar(expr const & type); + /** \brief Add a new hypothesis to the main branch */ + expr add_hypothesis(name const & n, expr const & type, optional const & value, optional const & jst) { + return m_main.add_hypothesis(n, type, value, jst); + } + + /** \brief Add a new hypothesis to the main branch */ + expr add_hypothesis(expr const & type, optional const & value, optional const & jst) { + return m_main.add_hypothesis(type, value, jst); + } + + /** \brief Set target (aka conclusion, aka type of the goal, aka type of the term that must be synthesize in this branch) + of the main branch */ + void set_target(expr const & type) { + return m_main.set_target(type); + } + metavar_decl const * get_metavar_decl(unsigned idx) const { return m_metavar_decls.find(idx); } + metavar_decl const * get_metavar_decl(expr const & e) const { return get_metavar_decl(mref_index(e)); } }; }}