From af01e7fea81a6d45d506098de664c48df3829845 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 4 Dec 2015 17:34:56 -0800 Subject: [PATCH] chore(library/blast): remove "leftover" file used in the old blast architecture --- src/library/blast/CMakeLists.txt | 2 +- src/library/blast/blast.cpp | 91 ++++++++++++++++- src/library/blast/blast.h | 37 +++++++ src/library/blast/expr.cpp | 105 -------------------- src/library/blast/expr.h | 47 --------- src/library/blast/hypothesis.cpp | 14 +++ src/library/blast/hypothesis.h | 6 +- src/library/blast/init_module.cpp | 3 - src/library/blast/simplifier/simplifier.cpp | 1 - src/library/blast/state.cpp | 42 ++++++++ src/library/blast/state.h | 34 ++----- 11 files changed, 196 insertions(+), 186 deletions(-) delete mode 100644 src/library/blast/expr.cpp delete mode 100644 src/library/blast/expr.h create mode 100644 src/library/blast/hypothesis.cpp diff --git a/src/library/blast/CMakeLists.txt b/src/library/blast/CMakeLists.txt index 7d3ca2ed3..0edb3b9fa 100644 --- a/src/library/blast/CMakeLists.txt +++ b/src/library/blast/CMakeLists.txt @@ -1,4 +1,4 @@ -add_library(blast OBJECT expr.cpp state.cpp blast.cpp blast_tactic.cpp +add_library(blast OBJECT hypothesis.cpp state.cpp blast.cpp blast_tactic.cpp init_module.cpp proof_expr.cpp options.cpp choice_point.cpp util.cpp gexpr.cpp revert.cpp strategy.cpp congruence_closure.cpp trace.cpp imp_extension.cpp) diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp index dd4a9b06e..4511b00b2 100644 --- a/src/library/blast/blast.cpp +++ b/src/library/blast/blast.cpp @@ -22,7 +22,6 @@ Author: Leonardo de Moura #include "library/projection.h" #include "library/scoped_ext.h" #include "library/tactic/goal.h" -#include "library/blast/expr.h" #include "library/blast/state.h" #include "library/blast/blast.h" #include "library/blast/proof_expr.h" @@ -36,7 +35,9 @@ Author: Leonardo de Moura namespace lean { namespace blast { static name * g_prefix = nullptr; +static name * g_ref_prefix = nullptr; static name * g_tmp_prefix = nullptr; +static expr * g_dummy_type = nullptr; // dummy type for href/mref class imp_extension_manager { std::vector > m_entries; @@ -74,6 +75,9 @@ class blastenv { environment m_env; io_state m_ios; name_generator m_ngen; + unsigned m_next_uref_idx{0}; + unsigned m_next_mref_idx{0}; + unsigned m_next_href_idx{0}; tmp_local_generator m_tmp_local_generator; list m_initial_context; // for setting type_context local instances name_set m_lemma_hints; @@ -484,7 +488,6 @@ public: m_unfold_macro_pred([](expr const &) { return true; }), m_tctx(*this), m_normalizer(m_tctx) { - init_uref_mref_href_idxs(); clear_choice_points(); } @@ -707,6 +710,24 @@ public: optional get_relation_info(name const & rop) const { return m_rel_getter(rop); } + + unsigned mk_uref_idx() { + unsigned r = m_next_uref_idx; + m_next_uref_idx++; + return r; + } + + unsigned mk_mref_idx() { + unsigned r = m_next_mref_idx; + m_next_mref_idx++; + return r; + } + + unsigned mk_href_idx() { + unsigned r = m_next_href_idx; + m_next_href_idx++; + return r; + } }; LEAN_THREAD_PTR(blastenv, g_blastenv); @@ -717,6 +738,68 @@ public: ~scope_blastenv() { g_blastenv = m_prev_blastenv; } }; +level mk_uref(unsigned idx) { + return lean::mk_meta_univ(name(*g_ref_prefix, idx)); +} + +bool is_uref(level const & l) { + return is_meta(l) && meta_id(l).is_numeral(); +} + +unsigned uref_index(level const & l) { + lean_assert(is_uref(l)); + return meta_id(l).get_numeral(); +} + +expr mk_href(unsigned idx) { + return lean::mk_local(name(*g_ref_prefix, idx), *g_dummy_type); +} + +bool is_href(expr const & e) { + return lean::is_local(e) && mlocal_type(e) == *g_dummy_type; +} + +expr mk_mref(unsigned idx) { + return mk_metavar(name(*g_ref_prefix, idx), *g_dummy_type); +} + +bool is_mref(expr const & e) { + return is_metavar(e) && mlocal_type(e) == *g_dummy_type; +} + +unsigned mref_index(expr const & e) { + lean_assert(is_mref(e)); + return mlocal_name(e).get_numeral(); +} + +unsigned href_index(expr const & e) { + lean_assert(is_href(e)); + return mlocal_name(e).get_numeral(); +} + +bool has_href(expr const & e) { + return lean::has_local(e); +} + +bool has_mref(expr const & e) { + return lean::has_expr_metavar(e); +} + +unsigned mk_uref_idx() { + lean_assert(g_blastenv); + return g_blastenv->mk_uref_idx(); +} + +unsigned mk_mref_idx() { + lean_assert(g_blastenv); + return g_blastenv->mk_mref_idx(); +} + +unsigned mk_href_idx() { + lean_assert(g_blastenv); + return g_blastenv->mk_href_idx(); +} + environment const & env() { lean_assert(g_blastenv); return g_blastenv->get_env(); @@ -1056,11 +1139,15 @@ optional blast_goal(environment const & env, io_state const & ios, list tmp_type_context_ptr; namespace blast { +/** \brief Create a blast-state universe meta-variable */ +level mk_uref(unsigned idx); +/** \brief Return true iff \c l is a blast-state universe meta-variable */ +bool is_uref(level const & l); +/** \brief Return the index of the given blast-state universe meta-variable */ +unsigned uref_index(level const & l); + +/** \brief Create a blast-state hypothesis (reference). + \remark these references are local constants, but they do **not** store their types */ +expr mk_href(unsigned idx); +/** \brief Create a blast-state meta-variable (reference). + \remark these references are local constants, but they do **not** store their types */ +expr mk_mref(unsigned idx); + +/** \brief Return true iff \c e is a hypothesis reference */ +bool is_href(expr const & e); +/** \brief Return the index of the given hypothesis reference */ +unsigned href_index(expr const & e); +/** \brief Return true iff \c e is a blast-state meta-variable (reference) */ +bool is_mref(expr const & e); +/** \brief Return the index of the given blast-state meta-variable (reference) */ +unsigned mref_index(expr const & e); +/** \brief Return true iff \c e contain href's */ +bool has_href(expr const & e); +/** \brief Return true iff \c e contain mref's */ +bool has_mref(expr const & e); +/** \brief Return true if \c is a local constant, but it is not a hypothesis reference */ +inline bool is_local_non_href(expr const & e) { return is_local(e) && !is_href(e); } + +/** \brief Return the a fresh index for uref/mref/href. + \remark It is implemented using thread local storage. */ +unsigned mk_uref_idx(); +unsigned mk_mref_idx(); +unsigned mk_href_idx(); + +inline level mk_fresh_uref() { return mk_uref(mk_uref_idx()); } + /** \brief Return the thread local environment being used by the blast tactic. */ environment const & env(); /** \brief Return the thread local io_state being used by the blast tactic. */ diff --git a/src/library/blast/expr.cpp b/src/library/blast/expr.cpp deleted file mode 100644 index 0abeebfc7..000000000 --- a/src/library/blast/expr.cpp +++ /dev/null @@ -1,105 +0,0 @@ -/* -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 -#include -#include "util/interrupt.h" -#include "kernel/expr_eq_fn.h" -#include "kernel/replace_cache.h" -#include "kernel/cache_stack.h" -#include "kernel/instantiate_univ_cache.h" -#include "library/blast/expr.h" - -namespace lean { -namespace blast { -static name * g_prefix = nullptr; -static expr * g_dummy_type = nullptr; // dummy type for href/mref - -level mk_uref(unsigned idx) { - return lean::mk_meta_univ(name(*g_prefix, idx)); -} - -bool is_uref(level const & l) { - return is_meta(l) && meta_id(l).is_numeral(); -} - -unsigned uref_index(level const & l) { - lean_assert(is_uref(l)); - return meta_id(l).get_numeral(); -} - -expr mk_href(unsigned idx) { - return lean::mk_local(name(*g_prefix, idx), *g_dummy_type); -} - -bool is_href(expr const & e) { - return lean::is_local(e) && mlocal_type(e) == *g_dummy_type; -} - -expr mk_mref(unsigned idx) { - return mk_metavar(name(*g_prefix, idx), *g_dummy_type); -} - -bool is_mref(expr const & e) { - return is_metavar(e) && mlocal_type(e) == *g_dummy_type; -} - -unsigned mref_index(expr const & e) { - lean_assert(is_mref(e)); - return mlocal_name(e).get_numeral(); -} - -unsigned href_index(expr const & e) { - lean_assert(is_href(e)); - return mlocal_name(e).get_numeral(); -} - -bool has_href(expr const & e) { - return lean::has_local(e); -} - -bool has_mref(expr const & e) { - return lean::has_expr_metavar(e); -} - -LEAN_THREAD_VALUE(unsigned, m_next_uref_idx, 0); -LEAN_THREAD_VALUE(unsigned, m_next_mref_idx, 0); -LEAN_THREAD_VALUE(unsigned, m_next_href_idx, 0); - -unsigned mk_uref_idx() { - unsigned r = m_next_uref_idx; - m_next_uref_idx++; - return r; -} - -unsigned mk_mref_idx() { - unsigned r = m_next_mref_idx; - m_next_mref_idx++; - return r; -} - -unsigned mk_href_idx() { - unsigned r = m_next_href_idx; - m_next_href_idx++; - return r; -} - -void init_uref_mref_href_idxs() { - m_next_uref_idx = 0; - m_next_mref_idx = 0; - m_next_href_idx = 0; -} - -void initialize_expr() { - g_prefix = new name(name::mk_internal_unique_name()); - g_dummy_type = new expr(mk_constant(*g_prefix)); -} - -void finalize_expr() { - delete g_prefix; - delete g_dummy_type; -} -}} diff --git a/src/library/blast/expr.h b/src/library/blast/expr.h deleted file mode 100644 index fe20321f3..000000000 --- a/src/library/blast/expr.h +++ /dev/null @@ -1,47 +0,0 @@ -/* -Copyright (c) 2015 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "kernel/expr.h" -#include "kernel/declaration.h" - -namespace lean { -namespace blast { -level mk_uref(unsigned idx); - -bool is_uref(level const & l); -unsigned uref_index(level const & l); - -// mk_href and mk_mref are helper functions for creating hypotheses and meta-variables used in the blast tactic. -// Remark: the local constants and metavariables manipulated by the blast tactic do **not** store their types. -expr mk_href(unsigned idx); -expr mk_mref(unsigned idx); - -bool is_href(expr const & e); -unsigned href_index(expr const & e); -bool is_mref(expr const & e); -unsigned mref_index(expr const & e); -/** \brief Return true iff \c e contain href's */ -bool has_href(expr const & e); -/** \brief Return true iff \c e contain mref's */ -bool has_mref(expr const & e); - -inline bool is_local_non_href(expr const & e) { return is_local(e) && !is_href(e); } - -/** \brief Return the a fresh index for uref/mref/href. - \remark It is implemented using thread local storage. */ -unsigned mk_uref_idx(); -unsigned mk_mref_idx(); -unsigned mk_href_idx(); -/** \brief Reset thread local counters */ -void init_uref_mref_href_idxs(); - -inline level mk_fresh_uref() { return mk_uref(mk_uref_idx()); } - -void initialize_expr(); -void finalize_expr(); -} -} diff --git a/src/library/blast/hypothesis.cpp b/src/library/blast/hypothesis.cpp new file mode 100644 index 000000000..a380b5713 --- /dev/null +++ b/src/library/blast/hypothesis.cpp @@ -0,0 +1,14 @@ +/* +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/hypothesis.h" +#include "library/blast/blast.h" + +namespace lean { +namespace blast { +bool hypothesis::depends_on(expr const & h) const { return m_deps.contains(href_index(h)); } +bool hypothesis::is_assumption() const { return !m_value || is_local_non_href(*m_value); } +}} diff --git a/src/library/blast/hypothesis.h b/src/library/blast/hypothesis.h index af0409f76..b33af5727 100644 --- a/src/library/blast/hypothesis.h +++ b/src/library/blast/hypothesis.h @@ -7,7 +7,7 @@ Author: Leonardo de Moura #pragma once #include "util/rc.h" #include "util/rb_map.h" -#include "library/blast/expr.h" +#include "kernel/expr.h" namespace lean { namespace blast { @@ -51,8 +51,8 @@ public: 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. */ - bool depends_on(expr const & h) const { return m_deps.contains(href_index(h)); } - bool is_assumption() const { return !m_value || is_local_non_href(*m_value); } + bool depends_on(expr const & h) const; + bool is_assumption() const; }; class hypothesis_idx_buffer_set { diff --git a/src/library/blast/init_module.cpp b/src/library/blast/init_module.cpp index ae9670b92..87ea22136 100644 --- a/src/library/blast/init_module.cpp +++ b/src/library/blast/init_module.cpp @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "library/blast/expr.h" #include "library/blast/state.h" #include "library/blast/blast.h" #include "library/blast/blast_tactic.h" @@ -19,7 +18,6 @@ Author: Leonardo de Moura namespace lean { void initialize_blast_module() { blast::initialize_options(); - blast::initialize_expr(); blast::initialize_state(); initialize_blast(); blast::initialize_simplifier_module(); @@ -40,7 +38,6 @@ void finalize_blast_module() { blast::finalize_simplifier_module(); finalize_blast(); blast::finalize_state(); - blast::finalize_expr(); blast::finalize_options(); } } diff --git a/src/library/blast/simplifier/simplifier.cpp b/src/library/blast/simplifier/simplifier.cpp index 9b9caaa2e..38517e97f 100644 --- a/src/library/blast/simplifier/simplifier.cpp +++ b/src/library/blast/simplifier/simplifier.cpp @@ -10,7 +10,6 @@ #include "library/expr_lt.h" #include "library/class_instance_resolution.h" #include "library/relation_manager.h" -#include "library/blast/expr.h" #include "library/blast/blast_exception.h" #include "library/blast/blast.h" #include "library/blast/simplifier/simplifier.h" diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp index 5242bc631..4b4857526 100644 --- a/src/library/blast/state.cpp +++ b/src/library/blast/state.cpp @@ -20,6 +20,10 @@ namespace blast { static name * g_prefix = nullptr; static name * g_H = nullptr; +bool metavar_decl::contains_href(expr const & h) const { + return contains_href(href_index(h)); +} + bool metavar_decl::restrict_context_using(metavar_decl const & other) { buffer to_erase; m_assumptions.for_each([&](unsigned hidx) { @@ -140,6 +144,10 @@ branch & branch::operator=(branch s) { state::state() {} +metavar_decl const * state::get_metavar_decl(expr const & e) const { + return get_metavar_decl(mref_index(e)); +} + expr state::mk_metavar(hypothesis_idx_set const & c, expr const & type) { unsigned midx = mk_mref_idx(); m_metavar_decls.insert(midx, metavar_decl(c, type)); @@ -157,6 +165,32 @@ expr state::mk_metavar(expr const & type) { return state::mk_metavar(get_assumptions(), type); } +bool state::is_uref_assigned(level const & l) const { + return m_uassignment.contains(uref_index(l)); +} + +/* u := l */ +void state::assign_uref(level const & u, level const & l) { + m_uassignment.insert(uref_index(u), l); +} + +level const * state::get_uref_assignment(level const & l) const { + return m_uassignment.find(uref_index(l)); +} + +bool state::is_mref_assigned(expr const & e) const { + lean_assert(is_mref(e)); + return m_eassignment.contains(mref_index(e)); +} + +expr const * state::get_mref_assignment(expr const & e) const { + return m_eassignment.find(mref_index(e)); +} + +void state::assign_mref(expr const & m, expr const & e) { + m_eassignment.insert(mref_index(m), e); +} + void state::restrict_mref_context_using(expr const & mref1, expr const & mref2) { metavar_decl const * d1 = m_metavar_decls.find(mref_index(mref1)); metavar_decl const * d2 = m_metavar_decls.find(mref_index(mref2)); @@ -167,6 +201,10 @@ void state::restrict_mref_context_using(expr const & mref1, expr const & mref2) m_metavar_decls.insert(mref_index(mref1), new_d1); } +hypothesis const & state::get_hypothesis_decl(expr const & h) const { + return get_hypothesis_decl(href_index(h)); +} + expr state::to_kernel_expr(expr const & e, hypothesis_idx_map & hidx2local, metavar_idx_map & midx2meta) const { return lean::replace(e, [&](expr const & e) { if (is_href(e)) { @@ -812,6 +850,10 @@ void state::set_target(expr const & t) { } } +bool state::target_depends_on(expr const & h) const { + return target_depends_on(href_index(h)); +} + struct expand_hrefs_fn : public replace_visitor { state const & m_state; list const & m_hrefs; diff --git a/src/library/blast/state.h b/src/library/blast/state.h index a639bfa74..83f8f7aab 100644 --- a/src/library/blast/state.h +++ b/src/library/blast/state.h @@ -31,7 +31,7 @@ public: m_assumptions(a), m_type(t) {} /** \brief Return true iff \c h is in the context of the this metavar declaration */ bool contains_href(unsigned hidx) const { return m_assumptions.contains(hidx); } - bool contains_href(expr const & h) const { return contains_href(href_index(h)); } + bool contains_href(expr const & h) const; expr const & get_type() const { return m_type; } /** \brief Make sure the declaration context of this declaration is a subset of \c other. \remark Return true iff the context has been modified. */ @@ -231,7 +231,7 @@ public: in the current branch. */ expr mk_metavar(expr const & type); metavar_decl const * get_metavar_decl(hypothesis_idx 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)); } + metavar_decl const * get_metavar_decl(expr const & e) const; /************************ Save/Restore branch @@ -284,7 +284,7 @@ public: bool hidx_depends_on(hypothesis_idx hidx_user, hypothesis_idx hidx_provider) const; hypothesis const & get_hypothesis_decl(hypothesis_idx hidx) const { auto h = m_branch.m_hyp_decls.find(hidx); lean_assert(h); return *h; } - hypothesis const & get_hypothesis_decl(expr const & h) const { return get_hypothesis_decl(href_index(h)); } + hypothesis const & get_hypothesis_decl(expr const & h) const; void for_each_hypothesis(std::function const & fn) const { m_branch.m_hyp_decls.for_each(fn); } optional find_active_hypothesis(std::function const & fn) const { // NOLINT @@ -349,7 +349,7 @@ public: expr const & get_target() const { return m_branch.m_target; } /** \brief Return true iff the target depends on the given hypothesis */ bool target_depends_on(hypothesis_idx hidx) const { return m_branch.m_target_deps.contains(hidx); } - bool target_depends_on(expr const & h) const { return target_depends_on(href_index(h)); } + bool target_depends_on(expr const & h) const; /************************ Proof steps @@ -395,40 +395,26 @@ public: Assignment management *************************/ - bool is_uref_assigned(level const & l) const { - return m_uassignment.contains(uref_index(l)); - } - + bool is_uref_assigned(level const & l) const; /* u := l */ - void assign_uref(level const & u, level const & l) { - m_uassignment.insert(uref_index(u), l); - } + void assign_uref(level const & u, level const & l); - level const * get_uref_assignment(level const & l) const { - return m_uassignment.find(uref_index(l)); - } + level const * get_uref_assignment(level const & l) const; /** \brief Make sure the metavariable declaration context of mref1 is a subset of the metavariable declaration context of mref2. */ void restrict_mref_context_using(expr const & mref1, expr const & mref2); - bool is_mref_assigned(expr const & e) const { - lean_assert(is_mref(e)); - return m_eassignment.contains(mref_index(e)); - } + bool is_mref_assigned(expr const & e) const; /** \brief Return true iff \c l contains an assigned uref */ bool has_assigned_uref(level const & l) const; bool has_assigned_uref(levels const & ls) const; - expr const * get_mref_assignment(expr const & e) const { - return m_eassignment.find(mref_index(e)); - } + expr const * get_mref_assignment(expr const & e) const; /* m := e */ - void assign_mref(expr const & m, expr const & e) { - m_eassignment.insert(mref_index(m), e); - } + void assign_mref(expr const & m, expr const & e); /** \brief Return true if \c e contains an assigned mref or uref */ bool has_assigned_uref_mref(expr const & e) const;