diff --git a/src/library/blast/CMakeLists.txt b/src/library/blast/CMakeLists.txt index 6dd17c393..d0f3d1fba 100644 --- a/src/library/blast/CMakeLists.txt +++ b/src/library/blast/CMakeLists.txt @@ -1 +1,2 @@ -add_library(blast OBJECT expr.cpp state.cpp blast.cpp blast_tactic.cpp init_module.cpp) +add_library(blast OBJECT expr.cpp branch.cpp state.cpp blast.cpp + blast_tactic.cpp init_module.cpp) diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp index f8efba515..2bf538a06 100644 --- a/src/library/blast/blast.cpp +++ b/src/library/blast/blast.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 "kernel/type_checker.h" #include "library/replace_visitor.h" #include "library/blast/expr.h" @@ -31,16 +32,16 @@ level to_blast_level(level const & l) { } class context { - environment m_env; - io_state m_ios; - name_set m_lemma_hints; - name_set m_unfold_hints; + environment m_env; + io_state m_ios; + name_set m_lemma_hints; + name_set m_unfold_hints; + name_map m_mvar2mref; // map goal metavariables to blast mref's class to_blast_expr_fn : public replace_visitor { type_checker m_tc; state & m_state; - // We map each metavariable to a metavariable application that contains only pairwise - // distinct local constants (that have been converted into lrefs). + // We map each metavariable to a metavariable application and the mref associated with it. name_map> & m_mvar2meta_mref; name_map & m_local2lref; @@ -90,38 +91,49 @@ class context { get_app_args(meta_mref->first, decl_args); if (decl_args.size() > args.size()) throw_unsupported_metavar_occ(e); + // Make sure the the current metavariable application prefix matches the one + // found before. for (unsigned i = 0; i < decl_args.size(); i++) { - lean_assert(is_local(decl_args[i])); - if (!is_local(args[i]) || mlocal_name(args[i]) != mlocal_name(decl_args[i])) + if (is_local(decl_args[i])) { + if (!is_local(args[i]) || mlocal_name(args[i]) != mlocal_name(decl_args[i])) + throw_unsupported_metavar_occ(e); + } else if (decl_args[i] != args[i]) { throw_unsupported_metavar_occ(e); + } } return mk_mref_app(meta_mref->second, args.size() - decl_args.size(), args.data() + decl_args.size()); } else { unsigned i = 0; - hypothesis_set ctx; - // find prefix of pair-wise distinct local constants that have already been processed. + hypothesis_idx_buffer ctx; + // Find prefix that contains only closed terms. for (; i < args.size(); i++) { - if (!is_local(args[i])) + if (!closed(args[i])) break; + if (!is_local(args[i])) { + // Ignore arguments that are not local constants. + // In the blast tactic we only support higher-order patterns. + continue; + } expr const & l = args[i]; if (!std::all_of(args.begin(), args.begin() + i, - [&](expr const & prev) { return mlocal_name(prev) != mlocal_name(l); })) - break; - if (auto lref = m_local2lref.find(mlocal_name(l))) { - ctx.insert(lref_index(*lref)); - } else { - break; + [&](expr const & prev) { return mlocal_name(prev) != mlocal_name(l); })) { + // Local has already been processed + continue; } + auto lref = m_local2lref.find(mlocal_name(l)); + if (!lref) { + // One of the arguments is a local constant that is not in m_local2lref + throw_unsupported_metavar_occ(e); + } + ctx.push_back(lref_index(*lref)); } unsigned prefix_sz = i; expr aux = e; for (; i < args.size(); i++) aux = app_fn(aux); lean_assert(is_meta(aux)); - expr type = visit(m_tc.infer(aux).first); - unsigned mref_index = m_state.add_metavar_decl(metavar_decl(ctx, type)); - expr mref = blast::mk_mref(mref_index); - m_mvar2meta_mref.insert(mlocal_name(mvar), mk_pair(aux, mref)); + expr type = visit(m_tc.infer(aux).first); + expr mref = m_state.mk_metavar(ctx, type); return mk_mref_app(mref, args.size() - prefix_sz, args.data() + prefix_sz); } } @@ -157,16 +169,21 @@ class context { } public: - to_blast_expr_fn(environment const & env, state & s, name_map> & mvar2meta_mref, - name_map & local2lref): + to_blast_expr_fn(environment const & env, state & s, + name_map> & mvar2meta_mref, name_map & local2lref): m_tc(env), m_state(s), m_mvar2meta_mref(mvar2meta_mref), m_local2lref(local2lref) {} }; + void init_mvar2mref(name_map> & m) { + m.for_each([&](name const & n, pair const & p) { + m_mvar2mref.insert(n, p.second); + }); + } + state to_state(goal const & g) { state s; - branch b; name_map> mvar2meta_mref; - name_map local2lref; + name_map local2lref; to_blast_expr_fn to_blast_expr(m_env, s, mvar2meta_mref, local2lref); buffer hs; g.get_hyps(hs); @@ -175,7 +192,7 @@ class context { // TODO(Leo): create hypothesis using new_type } expr new_target = to_blast_expr(g.get_type()); - // TODO(Leo): create branch and store in the state. + init_mvar2mref(mvar2meta_mref); return s; } diff --git a/src/library/blast/branch.cpp b/src/library/blast/branch.cpp new file mode 100644 index 000000000..f8d4b9160 --- /dev/null +++ b/src/library/blast/branch.cpp @@ -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/branch.h" + +namespace lean { +namespace blast { +void branch::fix_hypothesis(unsigned idx) { + auto h = m_context.find(idx); + lean_assert(h); + hypothesis new_h(*h); + new_h.mark_fixed(); + m_context.insert(idx, new_h); +} + +struct hypothesis_depth_lt { + branch const & m_branch; + hypothesis_depth_lt(branch const & b): m_branch(b) {} + bool operator()(unsigned hidx1, unsigned hidx2) const { + hypothesis const * h1 = m_branch.get(hidx1); + hypothesis const * h2 = m_branch.get(hidx2); + return h1 && h2 && h1->get_depth() < h2->get_depth() && (h1->get_depth() == h2->get_depth() && hidx1 < hidx2); + } +}; + +void branch::get_sorted_hypotheses(hypothesis_idx_buffer & r) { + m_context.for_each([&](unsigned hidx, hypothesis const &) { + r.push_back(hidx); + }); + std::sort(r.begin(), r.end(), hypothesis_depth_lt(*this)); +} +}} diff --git a/src/library/blast/branch.h b/src/library/blast/branch.h index bf41e6c8e..b9fa3058f 100644 --- a/src/library/blast/branch.h +++ b/src/library/blast/branch.h @@ -14,14 +14,26 @@ namespace blast { typedef rb_tree metavar_set; class branch { - typedef rb_map context; + typedef rb_map context; + typedef rb_map dependencies; friend class state; unsigned m_next; context m_context; + dependencies m_forward_deps; expr m_target; 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. */ + void fix_hypothesis(unsigned idx); + void fix_hypothesis(expr const & e) { + lean_assert(is_lref(e)); + fix_hypothesis(lref_index(e)); + } 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); hypothesis const * get(unsigned idx) const { return m_context.find(idx); } hypothesis const * get(expr const & e) const { lean_assert(is_lref(e)); diff --git a/src/library/blast/expr.cpp b/src/library/blast/expr.cpp index 033e5e68f..00f1c0cab 100644 --- a/src/library/blast/expr.cpp +++ b/src/library/blast/expr.cpp @@ -204,6 +204,14 @@ unsigned lref_index(expr const & e) { return mlocal_name(e).get_numeral(); } +bool has_lref(expr const & e) { + return has_local(e); +} + +bool has_mref(expr const & e) { + return has_expr_metavar(e); +} + expr mk_var(unsigned idx) { lean_assert(g_var_array); lean_assert(g_expr_table); diff --git a/src/library/blast/expr.h b/src/library/blast/expr.h index beb702297..08f50bfdf 100644 --- a/src/library/blast/expr.h +++ b/src/library/blast/expr.h @@ -71,6 +71,10 @@ bool is_lref(expr const & e); unsigned lref_index(expr const & e); bool is_mref(expr const & e); unsigned mref_index(expr const & e); +/** \brief Return true iff \c e contain lref's */ +bool has_lref(expr const & e); +/** \brief Return true iff \c e contain mref's */ +bool has_mref(expr const & e); level update_succ(level const & l, level const & new_arg); level update_max(level const & l, level const & new_lhs, level const & new_rhs); diff --git a/src/library/blast/hypothesis.h b/src/library/blast/hypothesis.h index a5e4138f7..61eeb0c93 100644 --- a/src/library/blast/hypothesis.h +++ b/src/library/blast/hypothesis.h @@ -15,26 +15,28 @@ class hypothesis; class branch; class state; -typedef rb_tree hypothesis_set; +typedef rb_tree hypothesis_idx_set; +typedef list hypothesis_idx_list; +typedef buffer hypothesis_idx_buffer; class hypothesis { friend class branch; - name m_name; // for pretty printing - bool m_active; - unsigned m_depth; - hypothesis_set m_backward_deps; - hypothesis_set m_forward_deps; - expr m_type; - optional m_value; - optional m_justification; + name m_name; // for pretty printing + unsigned m_active:1; + unsigned m_fixed:1; // occurs in the type of a metavariable, so we should not update its type. + unsigned m_depth; + hypothesis_idx_set m_deps; // hypotheses used by the type and/or value of this hypothesis. + expr m_type; + optional m_value; + optional m_justification; public: - hypothesis():m_active(0), m_depth(0) {} + hypothesis():m_active(true), m_fixed(false), m_depth(0) {} bool is_active() const { return m_active; } unsigned get_depth() const { return m_depth; } - hypothesis_set const & get_backward_deps() const { return m_backward_deps; } - hypothesis_set const & get_forward_deps() const { return m_forward_deps; } + hypothesis_idx_set const & get_backward_deps() const { return m_deps; } expr const & get_type() const { return m_type; } optional const & get_value() const { return m_value; } optional const & get_justification() const { return m_justification; } + void mark_fixed() { m_fixed = true; } }; }} diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp index 20f1789fe..637ca2100 100644 --- a/src/library/blast/state.cpp +++ b/src/library/blast/state.cpp @@ -4,15 +4,36 @@ 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/state.h" namespace lean { namespace blast { state::state():m_next_mref_index(0) {} -unsigned state::add_metavar_decl(metavar_decl const & decl) { - unsigned r = m_next_mref_index; + +expr state::mk_metavar(hypothesis_idx_buffer const & ctx, expr const & type) { + hypothesis_idx_set ctx_as_set; + for (unsigned const & hidx : ctx) + ctx_as_set.insert(hidx); + for_each(type, [&](expr const & e, unsigned) { + if (!has_lref(e)) + return false; + if (is_lref(e)) { + lean_assert(ctx_as_set.contains(lref_index(e))); + m_main.fix_hypothesis(e); + return false; + } + return true; // continue search + }); + unsigned idx = m_next_mref_index; m_next_mref_index++; - m_metavar_decls.insert(r, decl); - return r; + m_metavar_decls.insert(idx, metavar_decl(to_list(ctx), ctx_as_set, type)); + return blast::mk_mref(idx); +} + +expr state::mk_metavar(expr const & type) { + hypothesis_idx_buffer ctx; + m_main.get_sorted_hypotheses(ctx); + return mk_metavar(ctx, type); } }} diff --git a/src/library/blast/state.h b/src/library/blast/state.h index 40da27051..e4574f951 100644 --- a/src/library/blast/state.h +++ b/src/library/blast/state.h @@ -13,11 +13,13 @@ Author: Leonardo de Moura namespace lean { namespace blast { class metavar_decl { - hypothesis_set m_context; - expr m_type; + hypothesis_idx_list m_context; + hypothesis_idx_set m_context_as_set; + expr m_type; public: metavar_decl() {} - metavar_decl(hypothesis_set const & c, expr const & t):m_context(c), m_type(t) {} + metavar_decl(hypothesis_idx_list const & c, hypothesis_idx_set const & s, expr const & t): + m_context(c), m_context_as_set(s), m_type(t) {} }; class state { @@ -27,9 +29,19 @@ class state { typedef rb_map assignment; metavar_decls m_metavar_decls; assignment m_assignment; + branch m_main; + + unsigned add_metavar_decl(metavar_decl const & decl); + public: state(); - unsigned add_metavar_decl(metavar_decl const & decl); + /** \brief Create a new metavariable using the given type and context. + \pre ctx must be a subset of the hypotheses in the main branch. */ + expr mk_metavar(hypothesis_idx_buffer const & ctx, expr const & type); + /** \brief Create a new metavariable using the given type. + The context of this metavariable will be all hypotheses occurring in the main branch. */ + expr mk_metavar(expr const & 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)); } };