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

feat(library/congr_lemma_manager): fallback to simple congruence theorem if needed

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-07 15:47:19 -08:00
parent 0eb0a679e8
commit 77c0866599
1 changed files with 18 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

31
src/library/congr_lemma_manager.cpp
View file

@ -37,11 +37,6 @@ class congr_lemma_manager::imp {
std::unordered_map<key, result, key_hash_fn, key_eq_fn> m_cache; std::unordered_map<key, result, key_hash_fn, key_eq_fn> m_cache;
struct failure {
unsigned m_arg_idx;
failure(unsigned i):m_arg_idx(i) {}
};
expr infer(expr const & e) { return m_ctx.infer(e); } expr infer(expr const & e) { return m_ctx.infer(e); }
expr whnf(expr const & e) { return m_ctx.whnf(e); } expr whnf(expr const & e) { return m_ctx.whnf(e); }
@ -256,15 +251,25 @@ public:
} }
} }
} }
while (true) { auto new_r = mk_congr_simp(fn, pinfos, kinds);
try { if (new_r) {
auto new_r = mk_congr_simp(fn, pinfos, kinds); m_cache.insert(mk_pair(key(fn, nargs), *new_r));
if (new_r) return new_r;
m_cache.insert(mk_pair(key(fn, nargs), *new_r)); } if (has_cast(kinds)) {
return new_r; // remove casts and try again
} catch (failure & ex) { for (unsigned i = 0; i < kinds.size(); i++) {
kinds[ex.m_arg_idx] = congr_arg_kind::Fixed; if (kinds[i] == congr_arg_kind::Cast)
kinds[i] = congr_arg_kind::Fixed;
} }
auto new_r = mk_congr_simp(fn, pinfos, kinds);
if (new_r) {
m_cache.insert(mk_pair(key(fn, nargs), *new_r));
return new_r;
} else {
return new_r;
}
} else {
return new_r;
} }
} }
}; };