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

feat(library/compiler/erase_irrelevant): convert enumeration types into uint* types

Browse source
This commit is contained in:
Leonardo de Moura 2018-11-06 16:01:46 -08:00
parent 83ebacb8af
commit 8af0c85d4f
3 changed files with 34 additions and 8 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,7 +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::unordered_map<name, optional<expr>, name_hash> is_enum_cache;
typedef std::tuple<name, expr, expr> let_entry;
type_checker::state m_st;
local_ctx m_lctx;
@ -48,11 +48,14 @@ class erase_irrelevant_fn {
}
}
bool is_enum_type(name const & I) {
optional<expr> 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));
optional<unsigned> nbytes = lean::is_enum_type(env(), I);
if (!nbytes) return none_expr();
optional<expr> r = to_uint_type(*nbytes);
if (!r) return none_expr();
m_is_enum_cache.insert(mk_pair(I, r));
return r;
}
@ -95,8 +98,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 if (optional<expr> uint = is_enum_type(c))
return *uint;
else
return mk_enf_object_type();
} else if (!atomic_only && is_app_of(e, get_array_name(), 1)) {

27
src/library/compiler/util.cpp
View file

@ -40,6 +40,21 @@ optional<unsigned> is_enum_type(environment const & env, name const & I) {
}
}
static expr * g_uint8 = nullptr;
static expr * g_uint16 = nullptr;
static expr * g_uint32 = nullptr;
static expr * g_uint64 = nullptr;
optional<expr> to_uint_type(unsigned nbytes) {
switch (nbytes) {
case 1: return some_expr(*g_uint8);
case 2: return some_expr(*g_uint16);
case 4: return some_expr(*g_uint32);
case 8: return some_expr(*g_uint64);
default: return none_expr();
}
}
unsigned get_num_nested_lambdas(expr e) {
unsigned r = 0;
while (is_lambda(e)) {
@ -363,9 +378,7 @@ bool is_runtime_scalar_type(name const & n) {
n == get_uint16_name() ||
n == get_uint32_name() ||
n == get_uint64_name() ||
n == get_usize_name() ||
n == get_bool_name() ||
n == get_unit_name();
n == get_usize_name();
}
bool is_runtime_builtin_cnstr(name const & n) {
@ -409,6 +422,10 @@ void initialize_compiler_util() {
g_neutral_expr = new expr(mk_constant("_neutral_"));
g_unreachable_expr = new expr(mk_constant("_unreachable_"));
g_object_type = new expr(mk_constant("_obj_"));
g_uint8 = new expr(mk_constant(get_uint8_name()));
g_uint16 = new expr(mk_constant(get_uint16_name()));
g_uint32 = new expr(mk_constant(get_uint32_name()));
g_uint64 = new expr(mk_constant(get_uint64_name()));
register_system_attribute(basic_attribute::with_check(
"inline", "mark definition to always be inlined",
@ -447,5 +464,9 @@ void finalize_compiler_util() {
delete g_neutral_expr;
delete g_unreachable_expr;
delete g_object_type;
delete g_uint8;
delete g_uint16;
delete g_uint32;
delete g_uint64;
}
}

2
src/library/compiler/util.h
View file

@ -20,6 +20,8 @@ namespace lean {
Remark: if the inductive datatype `I` has more than `2^32` constructors (very unlikely), the result is also `none`. */
optional<unsigned> is_enum_type(environment const & env, name const & I);
optional<expr> to_uint_type(unsigned nbytes);
/* A "compiler" declaration `x := e` */
typedef pair_ref<name, expr> comp_decl;
typedef list_ref<comp_decl> comp_decls;