max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/compiler/erase_irrelevant): preserve enumeration types

Browse source
This commit is contained in:
Leonardo de Moura 2018-11-06 14:40:32 -08:00
parent 6f03df871b
commit 9f3544aaa4
1 changed files with 13 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/library/compiler/erase_irrelevant.cpp
View file

@ -13,6 +13,7 @@ Author: Leonardo de Moura
namespace lean {
class erase_irrelevant_fn {
typedef std::unordered_map<name, bool, name_hash> is_enum_cache;
typedef std::tuple<name, expr, expr> let_entry;
type_checker::state m_st;
local_ctx m_lctx;
@ -22,6 +23,7 @@ class erase_irrelevant_fn {
name m_x;
unsigned m_next_idx{1};
expr_map<bool> m_irrelevant_cache;
is_enum_cache m_is_enum_cache;
environment & env() { return m_st.env(); }
@ -46,6 +48,15 @@ class erase_irrelevant_fn {
}
}
bool is_enum_type(name const & I) {
auto it = m_is_enum_cache.find(I);
if (it != m_is_enum_cache.end())
return it->second;
bool r = static_cast<bool>(lean::is_enum_type(env(), I));
m_is_enum_cache.insert(mk_pair(I, r));
return r;
}
/* Return (some idx) iff inductive datatype `I_name` has only one constructor,
and this constructor has only one relevant field, `idx` is the field position. */
optional<unsigned> has_trivial_structure(name const & I_name) {
@ -84,6 +95,8 @@ class erase_irrelevant_fn {
return e;
else if (c == get_char_name())
return mk_constant(get_uint32_name());
else if (is_enum_type(c))
return e;
else
return mk_enf_object_type();
} else if (!atomic_only && is_app_of(e, get_array_name(), 1)) {