From 7854158751d237745c028dbf67bb4417618cb41a Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Thu, 3 Dec 2015 14:33:11 -0800 Subject: [PATCH] fix(library/abstract_expr_manager): only squash Cast subsingletons --- src/frontends/lean/builtin_cmds.cpp | 4 ++- src/library/abstract_expr_manager.cpp | 42 +++++++++++++++++++-------- src/library/abstract_expr_manager.h | 10 +++---- src/library/blast/blast.cpp | 2 +- 4 files changed, 39 insertions(+), 19 deletions(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 1e0271b9f..1ff4d103a 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -1469,8 +1469,10 @@ static environment normalizer_cmd(parser & p) { static environment abstract_expr_cmd(parser & p) { unsigned o = p.parse_small_nat(); default_type_context ctx(p.env(), p.ios()); + app_builder builder(p.env(), p.ios()); fun_info_manager fun_info(ctx); - abstract_expr_manager ae_manager(fun_info); + congr_lemma_manager congr_lemma(builder, fun_info); + abstract_expr_manager ae_manager(fun_info, congr_lemma); flycheck_information info(p.regular_stream()); if (info.enabled()) p.display_information_pos(p.cmd_pos()); diff --git a/src/library/abstract_expr_manager.cpp b/src/library/abstract_expr_manager.cpp index f5466f975..ac33482a7 100644 --- a/src/library/abstract_expr_manager.cpp +++ b/src/library/abstract_expr_manager.cpp @@ -25,13 +25,19 @@ unsigned abstract_expr_manager::hash(expr const & e) { buffer args; expr f = get_app_args(e, args); fun_info f_info = m_fun_info_manager.get(f, args.size()); + optional f_congr = m_congr_lemma_manager.mk_congr(f, args.size()); unsigned h = hash(f); - int i = -1; - for_each(f_info.get_params_info(), [&](param_info const & p_info) { - i++; - if (p_info.is_subsingleton()) return; - h = ::lean::hash(h, hash(args[i])); - }); + if (!f_congr) { + for (expr const & arg : args) h = ::lean::hash(h, hash(arg)); + } else { + int i = -1; + for_each2(f_info.get_params_info(), f_congr->get_arg_kinds(), + [&](param_info const & p_info, congr_arg_kind const & c_kind) { + i++; + if (p_info.is_subsingleton() && c_kind == congr_arg_kind::Cast) return; + h = ::lean::hash(h, hash(args[i])); + }); + } return h; } lean_unreachable(); @@ -66,13 +72,25 @@ bool abstract_expr_manager::is_equal(expr const & a, expr const & b) { if (!is_equal(f_a, f_b)) return false; if (a_args.size() != b_args.size()) return false; fun_info f_info = m_fun_info_manager.get(f_a, a_args.size()); - int i = -1; + optional f_congr = m_congr_lemma_manager.mk_congr(f_a, a_args.size()); bool not_equal = false; - for_each(f_info.get_params_info(), [&](param_info const & p_info) { - i++; - if (p_info.is_subsingleton()) return; - if (!is_equal(a_args[i], b_args[i])) not_equal = true; - }); + if (!f_congr) { + for (unsigned i = 0; i < a_args.size(); ++i) { + if (!is_equal(a_args[i], b_args[i])) { + not_equal = true; + break; + } + } + } else { + int i = -1; + for_each2(f_info.get_params_info(), f_congr->get_arg_kinds(), + [&](param_info const & p_info, congr_arg_kind const & c_kind) { + if (not_equal) return; + i++; + if (p_info.is_subsingleton() && c_kind == congr_arg_kind::Cast) return; + if (!is_equal(a_args[i], b_args[i])) not_equal = true; + }); + } return !not_equal; } lean_unreachable(); // LCOV_EXCL_LINE diff --git a/src/library/abstract_expr_manager.h b/src/library/abstract_expr_manager.h index 3b560b0ab..9e1fa86bc 100644 --- a/src/library/abstract_expr_manager.h +++ b/src/library/abstract_expr_manager.h @@ -6,18 +6,18 @@ Author: Daniel Selsam #pragma once #include "kernel/expr.h" #include "library/fun_info_manager.h" +#include "library/congr_lemma_manager.h" namespace lean { /** \brief Abstract expression manager, to allow comparing expressions while ignoring subsingletons. */ class abstract_expr_manager { - fun_info_manager & m_fun_info_manager; - + fun_info_manager & m_fun_info_manager; + congr_lemma_manager & m_congr_lemma_manager; public: - abstract_expr_manager(fun_info_manager & f_info_manager): - m_fun_info_manager(f_info_manager) { } - + abstract_expr_manager(fun_info_manager & f_info_manager, congr_lemma_manager & c_lemma_manager): + m_fun_info_manager(f_info_manager), 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/blast/blast.cpp b/src/library/blast/blast.cpp index 654d53ee0..335bfe8c6 100644 --- a/src/library/blast/blast.cpp +++ b/src/library/blast/blast.cpp @@ -475,7 +475,7 @@ public: m_app_builder(*m_tmp_ctx), m_fun_info_manager(*m_tmp_ctx), m_congr_lemma_manager(m_app_builder, m_fun_info_manager), - m_abstract_expr_manager(m_fun_info_manager), + m_abstract_expr_manager(m_fun_info_manager, m_congr_lemma_manager), m_light_lt_manager(env), m_rel_getter(mk_relation_info_getter(env)), m_refl_getter(mk_refl_info_getter(env)),