michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/abstract_expr_manager): only squash Cast subsingletons

Browse source
This commit is contained in:
Daniel Selsam 2015-12-03 14:33:11 -08:00 committed by Leonardo de Moura
parent 6e478696d2
commit 7854158751
4 changed files with 39 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/builtin_cmds.cpp
View file

@ -1469,8 +1469,10 @@ static environment normalizer_cmd(parser & p) {
static environment abstract_expr_cmd(parser & p) { static environment abstract_expr_cmd(parser & p) {
unsigned o = p.parse_small_nat(); unsigned o = p.parse_small_nat();
default_type_context ctx(p.env(), p.ios()); default_type_context ctx(p.env(), p.ios());
app_builder builder(p.env(), p.ios());
fun_info_manager fun_info(ctx); 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()); flycheck_information info(p.regular_stream());
if (info.enabled()) p.display_information_pos(p.cmd_pos()); if (info.enabled()) p.display_information_pos(p.cmd_pos());

42
src/library/abstract_expr_manager.cpp
View file

@ -25,13 +25,19 @@ unsigned abstract_expr_manager::hash(expr const & e) {
buffer<expr> args; buffer<expr> args;
expr f = get_app_args(e, args); expr f = get_app_args(e, args);
fun_info f_info = m_fun_info_manager.get(f, args.size()); fun_info f_info = m_fun_info_manager.get(f, args.size());
optional<congr_lemma> f_congr = m_congr_lemma_manager.mk_congr(f, args.size());
unsigned h = hash(f); unsigned h = hash(f);
int i = -1; if (!f_congr) {
for_each(f_info.get_params_info(), [&](param_info const & p_info) { for (expr const & arg : args) h = ::lean::hash(h, hash(arg));
i++; } else {
if (p_info.is_subsingleton()) return; int i = -1;
h = ::lean::hash(h, hash(args[i])); 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; return h;
} }
lean_unreachable(); 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 (!is_equal(f_a, f_b)) return false;
if (a_args.size() != b_args.size()) 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()); fun_info f_info = m_fun_info_manager.get(f_a, a_args.size());
int i = -1; optional<congr_lemma> f_congr = m_congr_lemma_manager.mk_congr(f_a, a_args.size());
bool not_equal = false; bool not_equal = false;
for_each(f_info.get_params_info(), [&](param_info const & p_info) { if (!f_congr) {
i++; for (unsigned i = 0; i < a_args.size(); ++i) {
if (p_info.is_subsingleton()) return; if (!is_equal(a_args[i], b_args[i])) {
if (!is_equal(a_args[i], b_args[i])) not_equal = true; 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; return !not_equal;
} }
lean_unreachable(); // LCOV_EXCL_LINE lean_unreachable(); // LCOV_EXCL_LINE

10
src/library/abstract_expr_manager.h
View file

@ -6,18 +6,18 @@ Author: Daniel Selsam
#pragma once #pragma once
#include "kernel/expr.h" #include "kernel/expr.h"
#include "library/fun_info_manager.h" #include "library/fun_info_manager.h"
#include "library/congr_lemma_manager.h"
namespace lean { namespace lean {
/** \brief Abstract expression manager, to allow comparing expressions while ignoring subsingletons. */ /** \brief Abstract expression manager, to allow comparing expressions while ignoring subsingletons. */
class abstract_expr_manager { 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: public:
abstract_expr_manager(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_fun_info_manager(f_info_manager), m_congr_lemma_manager(c_lemma_manager) { }
unsigned hash(expr const & e); unsigned hash(expr const & e);
bool is_equal(expr const & a, expr const & b); bool is_equal(expr const & a, expr const & b);
}; };

2
src/library/blast/blast.cpp
View file

@ -475,7 +475,7 @@ public:
m_app_builder(*m_tmp_ctx), m_app_builder(*m_tmp_ctx),
m_fun_info_manager(*m_tmp_ctx), m_fun_info_manager(*m_tmp_ctx),
m_congr_lemma_manager(m_app_builder, m_fun_info_manager), 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_light_lt_manager(env),
m_rel_getter(mk_relation_info_getter(env)), m_rel_getter(mk_relation_info_getter(env)),
m_refl_getter(mk_refl_info_getter(env)), m_refl_getter(mk_refl_info_getter(env)),