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

refactor(library/abstract_expr_manager): remove fun_info_manager

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

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

@ -1472,7 +1472,7 @@ static environment abstract_expr_cmd(parser & p) {
app_builder builder(p.env(), p.ios());
fun_info_manager fun_info(ctx);
congr_lemma_manager congr_lemma(builder, fun_info);
abstract_expr_manager ae_manager(fun_info, congr_lemma);
abstract_expr_manager ae_manager(congr_lemma);
flycheck_information info(p.regular_stream());
if (info.enabled()) p.display_information_pos(p.cmd_pos());

24
src/library/abstract_expr_manager.cpp
View file

@ -24,18 +24,16 @@ unsigned abstract_expr_manager::hash(expr const & e) {
case expr_kind::App:
buffer<expr> args;
expr f = get_app_args(e, args);
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);
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]));
for_each(f_congr->get_arg_kinds(), [&](congr_arg_kind const & c_kind) {
i++;
if (c_kind == congr_arg_kind::Cast) return;
h = ::lean::hash(h, hash(args[i]));
});
}
return h;
@ -71,7 +69,6 @@ bool abstract_expr_manager::is_equal(expr const & a, expr const & b) {
expr 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;
fun_info f_info = m_fun_info_manager.get(f_a, a_args.size());
optional<congr_lemma> f_congr = m_congr_lemma_manager.mk_congr(f_a, a_args.size());
bool not_equal = false;
if (!f_congr) {
@ -83,13 +80,12 @@ bool abstract_expr_manager::is_equal(expr const & a, expr const & b) {
}
} 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;
});
for_each(f_congr->get_arg_kinds(), [&](congr_arg_kind const & c_kind) {
if (not_equal) return;
i++;
if (c_kind == congr_arg_kind::Cast) return;
if (!is_equal(a_args[i], b_args[i])) not_equal = true;
});
}
return !not_equal;
}

4
src/library/abstract_expr_manager.h
View file

@ -13,11 +13,9 @@ namespace lean {
/** \brief Abstract expression manager, to allow comparing expressions while ignoring subsingletons. */
class abstract_expr_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, congr_lemma_manager & c_lemma_manager):
m_fun_info_manager(f_info_manager), m_congr_lemma_manager(c_lemma_manager) { }
abstract_expr_manager(congr_lemma_manager & c_lemma_manager): m_congr_lemma_manager(c_lemma_manager) {}
unsigned hash(expr const & e);
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_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_congr_lemma_manager),
m_abstract_expr_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)),