From 490a116baab82f32c5512f15774bb7281792ee91 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 24 Jun 2016 15:16:57 -0700 Subject: [PATCH] refactor(library): remove abstract_expr and abstract_expr_manager modules --- src/library/CMakeLists.txt | 4 +- src/library/abstract_expr.cpp | 316 ------------------- src/library/abstract_expr.h | 24 -- src/library/abstract_expr_manager.cpp | 141 --------- src/library/abstract_expr_manager.h | 31 -- src/library/proof_irrel_expr_manager.cpp | 126 -------- src/library/proof_irrel_expr_manager.h | 31 -- src/library/tactic/CMakeLists.txt | 2 +- src/library/tactic/abstract_expr_tactics.cpp | 38 --- src/library/tactic/abstract_expr_tactics.h | 11 - src/library/tactic/init_module.cpp | 3 - tests/lean/run/ahash1.lean | 35 -- tests/lean/run/aweight1.lean | 30 -- 13 files changed, 3 insertions(+), 789 deletions(-) delete mode 100644 src/library/abstract_expr.cpp delete mode 100644 src/library/abstract_expr.h delete mode 100644 src/library/abstract_expr_manager.cpp delete mode 100644 src/library/abstract_expr_manager.h delete mode 100644 src/library/proof_irrel_expr_manager.cpp delete mode 100644 src/library/proof_irrel_expr_manager.h delete mode 100644 src/library/tactic/abstract_expr_tactics.cpp delete mode 100644 src/library/tactic/abstract_expr_tactics.h delete mode 100644 tests/lean/run/ahash1.lean delete mode 100644 tests/lean/run/aweight1.lean diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 80b6cdf759..4de05017b4 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -13,7 +13,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp aux_recursors.cpp norm_num.cpp trace.cpp attribute_manager.cpp error_handling.cpp unification_hint.cpp local_context.cpp metavar_context.cpp type_context.cpp export_decl.cpp lazy_abstraction.cpp - fun_info.cpp congr_lemma.cpp abstract_expr.cpp defeq_canonizer.cpp + fun_info.cpp congr_lemma.cpp defeq_canonizer.cpp # Legacy -- The following files will be eventually deleted normalize.cpp justification.cpp constraint.cpp metavar.cpp choice.cpp locals.cpp unifier.cpp match.cpp class_instance_resolution.cpp old_type_context.cpp @@ -21,6 +21,6 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp old_util.cpp let.cpp metavar_closure.cpp old_local_context.cpp choice_iterator.cpp tmp_type_context.cpp - # abstract_expr_manager.cpp light_lt_manager.cpp + # light_lt_manager.cpp # proof_irrel_expr_manager.cpp ) diff --git a/src/library/abstract_expr.cpp b/src/library/abstract_expr.cpp deleted file mode 100644 index f71eaf23db..0000000000 --- a/src/library/abstract_expr.cpp +++ /dev/null @@ -1,316 +0,0 @@ -/* -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "util/hash.h" -#include "util/interrupt.h" -#include "kernel/expr_maps.h" -#include "kernel/instantiate.h" -#include "library/abstract_expr.h" -#include "library/cache_helper.h" -#include "library/fun_info.h" - -namespace lean { -struct abstract_expr_cache { - environment m_env; - expr_map m_hash_cache; - expr_map m_weight_cache; - abstract_expr_cache(environment const & env):m_env(env) {} - environment const & env() const { return m_env; } -}; - -/* The abstract_expr_cache does not depend on the transparency mode */ -typedef transparencyless_cache_compatibility_helper -abstract_expr_cache_helper; - -MK_THREAD_LOCAL_GET_DEF(abstract_expr_cache_helper, get_aech); - -abstract_expr_cache & get_abstract_cache_for(type_context const & ctx) { - return get_aech().get_cache_for(ctx); -} - -#define EASY_HASH(e) { \ - switch (e.kind()) { \ - case expr_kind::Constant: case expr_kind::Local: \ - case expr_kind::Meta: case expr_kind::Sort: \ - case expr_kind::Var: \ - return e.hash(); \ - default: \ - break; \ - } \ -} - -struct abstract_fn { - type_context & m_ctx; - buffer m_locals; - type_context::transparency_scope m_scope; - - static void check_system() { ::lean::check_system("abstract expression operator"); } - - abstract_fn(type_context & ctx): - m_ctx(ctx), - m_scope(m_ctx, transparency_mode::All) {} - - expr instantiate_locals(expr const & e) { - return instantiate_rev(e, m_locals.size(), m_locals.data()); - } - - expr push_local(name const & pp_name, expr const & type) { - expr l = m_ctx.push_local(pp_name, instantiate_locals(type)); - m_locals.push_back(l); - return l; - } - - expr push_let(name const & pp_name, expr const & type, expr const & value) { - expr l = m_ctx.push_let(pp_name, instantiate_locals(type), instantiate_locals(value)); - m_locals.push_back(l); - return l; - } - - void pop() { - m_locals.pop_back(); - } -}; - -struct abstract_hash_fn : public abstract_fn { - expr_map & m_cache; - abstract_hash_fn(type_context & ctx): - abstract_fn(ctx), - m_cache(get_abstract_cache_for(ctx).m_hash_cache) { - } - - unsigned hash(expr const & e) { - EASY_HASH(e); - - auto it = m_cache.find(e); - if (it != m_cache.end()) - return it->second; - - check_system(); - - unsigned r = 0; - - switch (e.kind()) { - case expr_kind::Constant: case expr_kind::Local: - case expr_kind::Meta: case expr_kind::Sort: - case expr_kind::Var: - lean_unreachable(); - case expr_kind::Lambda: - case expr_kind::Pi: - r = hash(binding_domain(e)); - push_local(binding_name(e), binding_domain(e)); - r = ::lean::hash(r, hash(binding_body(e))); - pop(); - break; - case expr_kind::Let: - r = ::lean::hash(hash(let_type(e)), hash(let_value(e))); - push_let(let_name(e), let_type(e), let_value(e)); - r = ::lean::hash(r, hash(let_body(e))); - pop(); - break; - case expr_kind::Macro: - r = lean::hash(macro_num_args(e), [&](unsigned i) { return hash(macro_arg(e, i)); }, - macro_def(e).hash()); - break; - case expr_kind::App: - buffer args; - expr const & f = get_app_args(e, args); - r = hash(f); - fun_info info = get_fun_info(m_ctx, instantiate_locals(f), args.size()); - unsigned i = 0; - for (param_info const & pinfo : info.get_params_info()) { - lean_assert(i < args.size()); - if (!pinfo.is_inst_implicit() && !pinfo.is_prop()) { - r = ::lean::hash(r, hash(args[i])); - } - i++; - } - /* Remark: the property (i == args.size()) does not necessarily hold here. - This can happen whenever the arity of f depends on its arguments. */ - break; - } - m_cache.insert(mk_pair(e, r)); - return r; - } - - unsigned operator()(expr const & e) { - return hash(e); - } -}; - -unsigned abstract_hash(type_context & ctx, expr const & e) { - EASY_HASH(e); - return abstract_hash_fn(ctx)(e); -} - -#define EASY_WEIGHT(e) { \ - switch (e.kind()) { \ - case expr_kind::Constant: case expr_kind::Local: \ - case expr_kind::Meta: case expr_kind::Sort: \ - case expr_kind::Var: \ - return 1; \ - default: \ - break; \ - } \ -} - -/* TODO(Leo): this class is too similar to abstract_hash_fn, both are folding expr. - We should try to merge both implementations. */ -struct abstract_weight_fn : public abstract_fn { - expr_map & m_cache; - abstract_weight_fn(type_context & ctx): - abstract_fn(ctx), - m_cache(get_abstract_cache_for(ctx).m_weight_cache) {} - - unsigned weight(expr const & e) { - EASY_WEIGHT(e); - - auto it = m_cache.find(e); - if (it != m_cache.end()) - return it->second; - - check_system(); - - unsigned r = 0; - - switch (e.kind()) { - case expr_kind::Constant: case expr_kind::Local: - case expr_kind::Meta: case expr_kind::Sort: - case expr_kind::Var: - lean_unreachable(); - case expr_kind::Lambda: - case expr_kind::Pi: - r = weight(binding_domain(e)); - push_local(binding_name(e), binding_domain(e)); - r += weight(binding_body(e)); - pop(); - break; - case expr_kind::Let: - r = weight(let_type(e)); - r += weight(let_value(e)); - push_let(let_name(e), let_type(e), let_value(e)); - r += weight(let_body(e)); - pop(); - break; - case expr_kind::Macro: - r = 0; - for (unsigned i = 0; i < macro_num_args(e); i++) - r += weight(macro_arg(e, i)); - break; - case expr_kind::App: - buffer args; - expr const & f = get_app_args(e, args); - r = weight(f); - fun_info info = get_fun_info(m_ctx, instantiate_locals(f), args.size()); - unsigned i = 0; - for (param_info const & pinfo : info.get_params_info()) { - lean_assert(i < args.size()); - if (!pinfo.is_inst_implicit() && !pinfo.is_prop()) { - r += weight(args[i]); - } - i++; - } - /* Remark: the property (i == args.size()) does not necessarily hold here. - This can happen whenever the arity of f depends on its arguments. */ - break; - } - m_cache.insert(mk_pair(e, r)); - return r; - } - - unsigned operator()(expr const & e) { - return weight(e); - } -}; - -unsigned abstract_weight(type_context & ctx, expr const & e) { - EASY_WEIGHT(e); - return abstract_weight_fn(ctx)(e); -} - -struct abstract_eq_fn : public abstract_fn { - abstract_eq_fn(type_context & ctx): - abstract_fn(ctx) {} - - bool equal(expr const & a, expr const & b) { - if (is_eqp(a, b)) - return true; - if (abstract_hash(m_ctx, a) != abstract_hash(m_ctx, b)) - return false; - if (a.kind() != b.kind()) - return false; - - switch (a.kind()) { - case expr_kind::Var: - case expr_kind::Constant: - case expr_kind::Meta: - case expr_kind::Sort: - case expr_kind::Local: - return a == b; - case expr_kind::Lambda: - case expr_kind::Pi: - check_system(); - if (!equal(binding_domain(a), binding_domain(b))) - return false; - push_local(binding_name(a), binding_domain(a)); - if (!equal(binding_body(a), binding_body(b))) - return false; - pop(); - return true; - case expr_kind::Let: - check_system(); - if (!equal(let_type(a), let_type(b)) || - !equal(let_value(a), let_value(b))) - return false; - push_let(let_name(a), let_type(a), let_value(a)); - if (!equal(let_body(a), let_body(b))) - return false; - pop(); - return true; - case expr_kind::Macro: - if (macro_def(a) != macro_def(b) || macro_num_args(a) != macro_num_args(b)) - return false; - check_system(); - for (unsigned i = 0; i < macro_num_args(a); i++) { - if (!equal(macro_arg(a, i), macro_arg(b, i))) - return false; - } - return true; - case expr_kind::App: - check_system(); - buffer a_args; - buffer b_args; - expr const & a_fn = get_app_args(a, a_args); - expr const & b_fn = get_app_args(b, b_args); - if (a_args.size() != b_args.size() || - !equal(a_fn, b_fn)) - return false; - fun_info info = get_fun_info(m_ctx, instantiate_locals(a_fn), a_args.size()); - unsigned i = 0; - for (param_info const & pinfo : info.get_params_info()) { - lean_assert(i < a_args.size()); - lean_assert(i < b_args.size()); - if (!pinfo.is_inst_implicit() && !pinfo.is_prop() && !equal(a_args[i], b_args[i])) - return false; - i++; - } - /* Remark: the property (i == a_args.size()) does not necessarily hold here. - This can happen whenever the arity of f depends on its arguments. */ - return true; - } - lean_unreachable(); // LCOV_EXCL_LINE - } - - bool operator()(expr const & a, expr const & b) { - return equal(a, b); - } -}; - -bool abstract_eq(type_context & ctx, expr const & a, expr const & b) { - if (is_eqp(a, b)) - return true; - return abstract_eq_fn(ctx)(a, b); -} -} diff --git a/src/library/abstract_expr.h b/src/library/abstract_expr.h deleted file mode 100644 index f028ec56bb..0000000000 --- a/src/library/abstract_expr.h +++ /dev/null @@ -1,24 +0,0 @@ -/* -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "library/type_context.h" - -namespace lean { -/** \brief Return a hash code for \c e that ignores instance parameters - (and proofs) in \c e. - - Example: the following two instances have the same hashcode - (@add nat nat_has_add a b) - (@add nat (add_monoid_has_add nat nat_is_monoid) a b) */ -unsigned abstract_hash(type_context & ctx, expr const & e); -/** \brief Weight function that ignores the type class instances in \c e. */ -unsigned abstract_weight(type_context & ctx, expr const & e); -/** \brief Equality function that ignores type class instances. */ -bool abstract_eq(type_context & ctx, expr const & e1, expr const & e2); -/** \brief Less than function that ignores type class instances. */ -bool abstract_lt(type_context & ctx, expr const & e1, expr const & e2); -} diff --git a/src/library/abstract_expr_manager.cpp b/src/library/abstract_expr_manager.cpp deleted file mode 100644 index 67cf4bedfc..0000000000 --- a/src/library/abstract_expr_manager.cpp +++ /dev/null @@ -1,141 +0,0 @@ -/* -Copyright (c) 2015 Daniel Selsam. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Daniel Selsam -*/ -#include "library/abstract_expr_manager.h" -#include "kernel/instantiate.h" -#include "util/safe_arith.h" -#include "util/list_fn.h" - -namespace lean { - -unsigned abstract_expr_manager::hash(expr const & e) { - unsigned h; - switch (e.kind()) { - case expr_kind::Constant: - case expr_kind::Local: - case expr_kind::Meta: - case expr_kind::Sort: - case expr_kind::Var: - case expr_kind::Macro: - return e.hash(); - case expr_kind::Lambda: - case expr_kind::Pi: - h = hash(binding_domain(e)); - // Remark binding_domain(e) may contain de-bruijn variables. - // We can instantiate them eagerly as we do here, or lazily. - // The lazy approach is potentially more efficient, but we would have - // to use something more sophisticated than an instantiate_rev at expr_kind::App - m_locals.push_back(instantiate_rev(m_tctx.mk_tmp_local(binding_domain(e)), m_locals.size(), m_locals.data())); - h = ::lean::hash(h, hash(binding_body(e))); - m_locals.pop_back(); - return h; - case expr_kind::Let: - // Let-expressions must be unfolded before invoking this method - lean_unreachable(); - case expr_kind::App: - buffer args; - expr const & f = get_app_args(e, args); - unsigned prefix_sz = m_congr_lemma_manager.get_specialization_prefix_size(instantiate_rev(f, m_locals.size(), m_locals.data()), args.size()); - expr new_f = e; - unsigned rest_sz = args.size() - prefix_sz; - for (unsigned i = 0; i < rest_sz; i++) - new_f = app_fn(new_f); - new_f = instantiate_rev(new_f, m_locals.size(), m_locals.data()); - optional congr = m_congr_lemma_manager.mk_congr(new_f, rest_sz); - h = hash(new_f); - if (!congr) { - for (unsigned i = prefix_sz; i < args.size(); i++) { - h = ::lean::hash(h, hash(args[i])); - } - } else { - lean_assert(length(congr->get_arg_kinds()) == rest_sz); - unsigned i = prefix_sz; - for_each(congr->get_arg_kinds(), [&](congr_arg_kind const & c_kind) { - if (c_kind != congr_arg_kind::Cast) { - h = ::lean::hash(h, hash(args[i])); - } - i++; - }); - } - return h; - } - lean_unreachable(); -} - -bool abstract_expr_manager::is_equal(expr const & a, expr const & b) { - if (is_eqp(a, b)) return true; - if (a.kind() != b.kind()) return false; - if (is_var(a)) return var_idx(a) == var_idx(b); - bool is_eq; - switch (a.kind()) { - case expr_kind::Var: - lean_unreachable(); // LCOV_EXCL_LINE - case expr_kind::Constant: case expr_kind::Sort: - return a == b; - case expr_kind::Meta: case expr_kind::Local: - return mlocal_name(a) == mlocal_name(b) && is_equal(mlocal_type(a), mlocal_type(b)); - case expr_kind::Lambda: case expr_kind::Pi: - if (!is_equal(binding_domain(a), binding_domain(b))) return false; - // see comment at abstract_expr_manager::hash - m_locals.push_back(instantiate_rev(m_tctx.mk_tmp_local(binding_domain(a)), m_locals.size(), m_locals.data())); - is_eq = is_equal(binding_body(a), binding_body(b)); - m_locals.pop_back(); - return is_eq; - case expr_kind::Let: - // Let-expressions must be unfolded before invoking this method - lean_unreachable(); - case expr_kind::Macro: - if (macro_def(a) != macro_def(b) || macro_num_args(a) != macro_num_args(b)) - return false; - for (unsigned i = 0; i < macro_num_args(a); i++) { - if (!is_equal(macro_arg(a, i), macro_arg(b, i))) - return false; - } - return true; - case expr_kind::App: - buffer a_args, b_args; - expr const & f_a = get_app_args(a, a_args); - expr const & f_b = get_app_args(b, b_args); - if (!is_equal(f_a, f_b)) - return false; - if (a_args.size() != b_args.size()) - return false; - unsigned prefix_sz = m_congr_lemma_manager.get_specialization_prefix_size(instantiate_rev(f_a, m_locals.size(), m_locals.data()), a_args.size()); - for (unsigned i = 0; i < prefix_sz; i++) { - if (!is_equal(a_args[i], b_args[i])) - return false; - } - expr new_f_a = a; - unsigned rest_sz = a_args.size() - prefix_sz; - for (unsigned i = 0; i < rest_sz; i++) { - new_f_a = app_fn(new_f_a); - } - new_f_a = instantiate_rev(new_f_a, m_locals.size(), m_locals.data()); - optional congr = m_congr_lemma_manager.mk_congr(new_f_a, rest_sz); - bool not_equal = false; - if (!congr) { - for (unsigned i = prefix_sz; i < a_args.size(); ++i) { - if (!is_equal(a_args[i], b_args[i])) { - not_equal = true; - break; - } - } - } else { - lean_assert(length(congr->get_arg_kinds()) == rest_sz); - unsigned i = prefix_sz; - for_each(congr->get_arg_kinds(), [&](congr_arg_kind const & c_kind) { - if (not_equal) - return; - if (c_kind != congr_arg_kind::Cast && !is_equal(a_args[i], b_args[i])) { - not_equal = true; - } - i++; - }); - } - return !not_equal; - } - lean_unreachable(); // LCOV_EXCL_LINE -} -} diff --git a/src/library/abstract_expr_manager.h b/src/library/abstract_expr_manager.h deleted file mode 100644 index a66cbeffe7..0000000000 --- a/src/library/abstract_expr_manager.h +++ /dev/null @@ -1,31 +0,0 @@ -/* -Copyright (c) 2015 Daniel Selsam. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Daniel Selsam -*/ -#pragma once -#include -#include "kernel/expr.h" -#include "library/old_type_context.h" -#include "library/congr_lemma_manager.h" - -namespace lean { - -/** \brief Abstract expression manager, to allow comparing expressions while ignoring subsingletons. */ - -class abstract_expr_manager { - /* The [congr_lemma_manager] cannot handle [Var]s since it needs to infer types, and we do not - want to instantiate eagerly for performance reasons. Therefore we track the context ourselves, - and only instantiate on the expressions we pass to the [congr_lemma_manager], which we - expect to be very small in general. */ - std::vector m_locals; - old_type_context & m_tctx; - congr_lemma_manager & m_congr_lemma_manager; -public: - abstract_expr_manager(congr_lemma_manager & c_lemma_manager): - m_tctx(c_lemma_manager.ctx()), m_congr_lemma_manager(c_lemma_manager) {} - unsigned hash(expr const & e); - bool is_equal(expr const & a, expr const & b); -}; - -} diff --git a/src/library/proof_irrel_expr_manager.cpp b/src/library/proof_irrel_expr_manager.cpp deleted file mode 100644 index e3993cfd3e..0000000000 --- a/src/library/proof_irrel_expr_manager.cpp +++ /dev/null @@ -1,126 +0,0 @@ -/* -Copyright (c) 2015 Daniel Selsam. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Daniel Selsam -*/ -#include "library/proof_irrel_expr_manager.h" -#include "kernel/instantiate.h" -#include "util/safe_arith.h" -#include "util/list_fn.h" - -namespace lean { - -unsigned proof_irrel_expr_manager::hash(expr const & e) { - unsigned h; - switch (e.kind()) { - case expr_kind::Constant: - case expr_kind::Local: - case expr_kind::Meta: - case expr_kind::Sort: - case expr_kind::Var: - case expr_kind::Macro: - return e.hash(); - case expr_kind::Let: - // Let-expressions must be unfolded before invoking this method - lean_unreachable(); - case expr_kind::Lambda: - case expr_kind::Pi: - h = hash(binding_domain(e)); - // Remark binding_domain(e) may contain de-bruijn variables. - // We can instantiate them eagerly as we do here, or lazily. - // The lazy approach is potentially more efficient, but we would have - // to use something more sophisticated than an instantiate_rev at expr_kind::App - m_locals.push_back(instantiate_rev(m_tctx.mk_tmp_local(binding_domain(e)), m_locals.size(), m_locals.data())); - h = ::lean::hash(h, hash(binding_body(e))); - m_locals.pop_back(); - return h; - case expr_kind::App: - buffer args; - expr const & f = get_app_args(e, args); - unsigned prefix_sz = m_fun_info_manager.get_specialization_prefix_size(instantiate_rev(f, m_locals.size(), m_locals.data()), args.size()); - expr new_f = e; - unsigned rest_sz = args.size() - prefix_sz; - for (unsigned i = 0; i < rest_sz; i++) - new_f = app_fn(new_f); - new_f = instantiate_rev(new_f, m_locals.size(), m_locals.data()); - h = hash(new_f); - fun_info info = m_fun_info_manager.get(new_f, rest_sz); - lean_assert(length(info.get_params_info()) == rest_sz); - unsigned i = prefix_sz; - for_each(info.get_params_info(), [&](param_info const & p_info) { - if (!p_info.is_prop()) { - h = ::lean::hash(h, hash(args[i])); - } - i++; - }); - return h; - } - lean_unreachable(); -} - -bool proof_irrel_expr_manager::is_equal(expr const & a, expr const & b) { - if (is_eqp(a, b)) return true; - if (a.kind() != b.kind()) return false; - if (is_var(a)) return var_idx(a) == var_idx(b); - bool is_eq; - switch (a.kind()) { - case expr_kind::Var: - lean_unreachable(); // LCOV_EXCL_LINE - case expr_kind::Constant: case expr_kind::Sort: - return a == b; - case expr_kind::Meta: case expr_kind::Local: - return mlocal_name(a) == mlocal_name(b) && is_equal(mlocal_type(a), mlocal_type(b)); - case expr_kind::Let: - // Let-expressions must be unfolded before invoking this method - lean_unreachable(); - case expr_kind::Lambda: case expr_kind::Pi: - if (!is_equal(binding_domain(a), binding_domain(b))) return false; - // see comment at proof_irrel_expr_manager::hash - m_locals.push_back(instantiate_rev(m_tctx.mk_tmp_local(binding_domain(a)), m_locals.size(), m_locals.data())); - is_eq = is_equal(binding_body(a), binding_body(b)); - m_locals.pop_back(); - return is_eq; - case expr_kind::Macro: - if (macro_def(a) != macro_def(b) || macro_num_args(a) != macro_num_args(b)) - return false; - for (unsigned i = 0; i < macro_num_args(a); i++) { - if (!is_equal(macro_arg(a, i), macro_arg(b, i))) - return false; - } - return true; - case expr_kind::App: - buffer a_args, b_args; - expr const & f_a = get_app_args(a, a_args); - expr const & f_b = get_app_args(b, b_args); - if (!is_equal(f_a, f_b)) - return false; - if (a_args.size() != b_args.size()) - return false; - unsigned prefix_sz = m_fun_info_manager.get_specialization_prefix_size(instantiate_rev(f_a, m_locals.size(), m_locals.data()), a_args.size()); - for (unsigned i = 0; i < prefix_sz; i++) { - if (!is_equal(a_args[i], b_args[i])) - return false; - } - expr new_f_a = a; - unsigned rest_sz = a_args.size() - prefix_sz; - for (unsigned i = 0; i < rest_sz; i++) { - new_f_a = app_fn(new_f_a); - } - new_f_a = instantiate_rev(new_f_a, m_locals.size(), m_locals.data()); - fun_info info = m_fun_info_manager.get(new_f_a, rest_sz); - bool not_equal = false; - lean_assert(length(info.get_params_info()) == rest_sz); - unsigned i = prefix_sz; - for_each(info.get_params_info(), [&](param_info const & p_info) { - if (not_equal) - return; - if (!p_info.is_prop() && !is_equal(a_args[i], b_args[i])) { - not_equal = true; - } - i++; - }); - return !not_equal; - } - lean_unreachable(); // LCOV_EXCL_LINE -} -} diff --git a/src/library/proof_irrel_expr_manager.h b/src/library/proof_irrel_expr_manager.h deleted file mode 100644 index 5732a1830b..0000000000 --- a/src/library/proof_irrel_expr_manager.h +++ /dev/null @@ -1,31 +0,0 @@ -/* -Copyright (c) 2015 Daniel Selsam. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Daniel Selsam -*/ -#pragma once -#include -#include "kernel/expr.h" -#include "library/old_type_context.h" -#include "library/fun_info_manager.h" - -namespace lean { - -/** \brief Proof-irrelevant expression manager, to allow comparing expressions while ignoring proofs. */ - -class proof_irrel_expr_manager { - /* The [fun_info_manager] cannot handle [Var]s since it needs to infer types, and we do not - want to instantiate eagerly for performance reasons. Therefore we track the context ourselves, - and only instantiate on the expressions we pass to the [fun_info_manager], which we - expect to be very small in general. */ - std::vector m_locals; - old_type_context & m_tctx; - fun_info_manager & m_fun_info_manager; -public: - proof_irrel_expr_manager(fun_info_manager & f_info_manager): - m_tctx(f_info_manager.ctx()), m_fun_info_manager(f_info_manager) {} - unsigned hash(expr const & e); - bool is_equal(expr const & a, expr const & b); -}; - -} diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index 79ed0a1b78..54ee2a64f4 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -2,5 +2,5 @@ add_library(tactic OBJECT tactic_state.cpp intro_tactic.cpp revert_tactic.cpp rename_tactic.cpp clear_tactic.cpp app_builder_tactics.cpp subst_tactic.cpp exact_tactic.cpp change_tactic.cpp assert_tactic.cpp apply_tactic.cpp - fun_info_tactics.cpp congr_lemma_tactics.cpp abstract_expr_tactics.cpp + fun_info_tactics.cpp congr_lemma_tactics.cpp elaborate.cpp init_module.cpp) diff --git a/src/library/tactic/abstract_expr_tactics.cpp b/src/library/tactic/abstract_expr_tactics.cpp deleted file mode 100644 index 645c65276c..0000000000 --- a/src/library/tactic/abstract_expr_tactics.cpp +++ /dev/null @@ -1,38 +0,0 @@ -/* -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "library/abstract_expr.h" -#include "library/vm/vm_expr.h" -#include "library/vm/vm_nat.h" -#include "library/tactic/tactic_state.h" - -namespace lean { -vm_obj tactic_abstract_hash(vm_obj const & e, vm_obj const & s) { - type_context_scope ctx(s); - unsigned h = abstract_hash(ctx, to_expr(e)) % LEAN_MAX_SMALL_NAT; - return mk_tactic_success(mk_vm_simple(h), to_tactic_state(s)); -} - -vm_obj tactic_abstract_weight(vm_obj const & e, vm_obj const & s) { - type_context_scope ctx(s); - unsigned h = abstract_weight(ctx, to_expr(e)) % LEAN_MAX_SMALL_NAT; - return mk_tactic_success(mk_vm_simple(h), to_tactic_state(s)); -} - -vm_obj tactic_abstract_eq(vm_obj const & e1, vm_obj const & e2, vm_obj const & s) { - type_context_scope ctx(s); - bool r = abstract_eq(ctx, to_expr(e1), to_expr(e2)); - return mk_tactic_success(mk_vm_bool(r), to_tactic_state(s)); -} - -void initialize_abstract_expr_tactics() { - DECLARE_VM_BUILTIN(name({"tactic", "abstract_hash"}), tactic_abstract_hash); - DECLARE_VM_BUILTIN(name({"tactic", "abstract_weight"}), tactic_abstract_weight); - DECLARE_VM_BUILTIN(name({"tactic", "abstract_eq"}), tactic_abstract_eq); -} -void finalize_abstract_expr_tactics() { -} -} diff --git a/src/library/tactic/abstract_expr_tactics.h b/src/library/tactic/abstract_expr_tactics.h deleted file mode 100644 index e7c2803714..0000000000 --- a/src/library/tactic/abstract_expr_tactics.h +++ /dev/null @@ -1,11 +0,0 @@ -/* -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -namespace lean { -void initialize_abstract_expr_tactics(); -void finalize_abstract_expr_tactics(); -} diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp index cff53ca73a..927db5a4cd 100644 --- a/src/library/tactic/init_module.cpp +++ b/src/library/tactic/init_module.cpp @@ -17,7 +17,6 @@ Author: Leonardo de Moura #include "library/tactic/apply_tactic.h" #include "library/tactic/fun_info_tactics.h" #include "library/tactic/congr_lemma_tactics.h" -#include "library/tactic/abstract_expr_tactics.h" #include "library/tactic/elaborate.h" #include "library/tactic/defeq_simplifier/init_module.h" @@ -36,14 +35,12 @@ void initialize_tactic_module() { initialize_apply_tactic(); initialize_fun_info_tactics(); initialize_congr_lemma_tactics(); - initialize_abstract_expr_tactics(); initialize_elaborate(); initialize_defeq_simplifier_module(); } void finalize_tactic_module() { finalize_defeq_simplifier_module(); finalize_elaborate(); - finalize_abstract_expr_tactics(); finalize_congr_lemma_tactics(); finalize_fun_info_tactics(); finalize_apply_tactic(); diff --git a/tests/lean/run/ahash1.lean b/tests/lean/run/ahash1.lean deleted file mode 100644 index 34e4f21620..0000000000 --- a/tests/lean/run/ahash1.lean +++ /dev/null @@ -1,35 +0,0 @@ -open tactic bool - -constant nat_has_add1 : has_add nat -constant nat_has_add2 : has_add nat - -example (a b : nat) - (H1 : @add nat nat_has_add1 a b = 0) - (H2 : @add nat nat_has_add2 a b = 0) - (H3 : @add nat nat_has_add1 b a = 0) - : true := -by do - h₁ ← get_local "H1" >>= infer_type >>= abstract_hash, - h₂ ← get_local "H2" >>= infer_type >>= abstract_hash, - h₃ ← get_local "H3" >>= infer_type >>= abstract_hash, - trace $ to_string h₁ + " " + to_string h₂ + " " + to_string h₃, - if h₁ ≠ h₂ then fail "ERROR" else skip, - if h₁ = h₃ then fail "UNEXPECTED" else skip, - constructor - -example (a b : nat) - (H1 : ∀ d c : nat, @add nat nat_has_add1 a b = c + d) - (H2 : ∀ d c : nat, @add nat nat_has_add2 a b = c + d) - (H3 : ∀ d c : nat, @add nat nat_has_add1 a b = d + d) - : true := -by do - get_local "H1" >>= infer_type >>= abstract_hash >>= trace, - get_local "H2" >>= infer_type >>= abstract_hash >>= trace, - H1 ← get_local "H1" >>= infer_type, - H2 ← get_local "H2" >>= infer_type, - H3 ← get_local "H3" >>= infer_type, - abstract_eq H1 H2 >>= trace, - abstract_eq H1 H3 >>= trace, - abstract_eq H1 H2 >>= (λ b, when (b = ff) (fail "ERROR1")), - abstract_eq H1 H3 >>= (λ b, when (b = tt) (fail "ERROR2")), - constructor diff --git a/tests/lean/run/aweight1.lean b/tests/lean/run/aweight1.lean deleted file mode 100644 index d30048ae2c..0000000000 --- a/tests/lean/run/aweight1.lean +++ /dev/null @@ -1,30 +0,0 @@ -import data.nat -open tactic nat decidable - -constant nat_has_add1 : has_add nat -constant nat_has_add2 : nat → has_add nat - -constant foo (a : nat) : a > 0 → Prop - -set_option pp.all true - -example (a b : nat) - (H1 : @add nat nat_has_add1 a b = 0) - (H2 : @add nat (nat_has_add2 (0 + a + b)) a b = 0) - (H3 : @add nat nat_has_add1 b (a + b) = 0) - (H4 : foo (succ (succ (succ zero))) dec_trivial) - (H5 : foo (succ (succ (succ zero))) sorry) - : true := -by do - h₁ ← get_local "H1" >>= infer_type >>= abstract_weight, - h₂ ← get_local "H2" >>= infer_type >>= abstract_weight, - h₃ ← get_local "H3" >>= infer_type >>= abstract_weight, - h₄ ← get_local "H4" >>= infer_type >>= abstract_weight, - h₅ ← get_local "H5" >>= infer_type >>= abstract_weight, - trace $ to_string h₁ + " " + to_string h₂ + " " + to_string h₃, - trace $ to_string h₄ + " " + to_string h₅, - get_local "H4" >>= infer_type >>= trace, - get_local "H5" >>= infer_type >>= trace, - if h₁ ≠ h₂ then fail "ERROR" else skip, - if h₁ = h₃ then fail "ERROR" else skip, - constructor