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

refactor(library/compiler): add is_enum_type auxiliary function

Browse source
This commit is contained in:
Leonardo de Moura 2018-11-06 14:10:06 -08:00
parent f404c5c446
commit e63721958b
3 changed files with 27 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/library/compiler/llnf.cpp
View file

@ -163,33 +163,13 @@ class to_llnf_fn {
name_generator & ngen() { return m_st.ngen(); }
optional<unsigned> is_enum_type_core(name const & I) {
constant_info info = env().get(I);
if (!info.is_inductive()) return optional<unsigned>();
unsigned n = 0;
for (name const & c : info.to_inductive_val().get_cnstrs()) {
if (is_pi(env().get(c).get_type()))
return optional<unsigned>();
if (n == std::numeric_limits<unsigned>::max())
return optional<unsigned>();
n++;
}
if (n < (1u << 8)) {
return optional<unsigned>(1);
} else if (n < (1u << 16)) {
return optional<unsigned>(2);
} else {
return optional<unsigned>(4);
}
}
optional<unsigned> is_enum_type(expr const & type) {
expr const & I = get_app_fn(type);
if (!is_constant(I)) return optional<unsigned>();
auto it = m_enum_cache.find(const_name(I));
if (it != m_enum_cache.end())
return it->second;
optional<unsigned> r = is_enum_type_core(const_name(I));
optional<unsigned> r = ::lean::is_enum_type(env(), const_name(I));
m_enum_cache.insert(mk_pair(const_name(I), r));
return r;
}

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

@ -19,6 +19,26 @@ Author: Leonardo de Moura
#include "library/compiler/util.h"
namespace lean {
optional<unsigned> is_enum_type(environment const & env, name const & I) {
constant_info info = env.get(I);
if (!info.is_inductive()) return optional<unsigned>();
unsigned n = 0;
for (name const & c : info.to_inductive_val().get_cnstrs()) {
if (is_pi(env.get(c).get_type()))
return optional<unsigned>();
if (n == std::numeric_limits<unsigned>::max())
return optional<unsigned>();
n++;
}
if (n < (1u << 8)) {
return optional<unsigned>(1);
} else if (n < (1u << 16)) {
return optional<unsigned>(2);
} else {
return optional<unsigned>(4);
}
}
unsigned get_num_nested_lambdas(expr e) {
unsigned r = 0;
while (is_lambda(e)) {

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

@ -14,6 +14,12 @@ Author: Leonardo de Moura
#include "library/util.h"
namespace lean {
/* Return the `some(n)` if `I` is the name of an inductive datatype that contains only constructors with 0-arguments,
and `n` is `1`, `2` or `4`, i.e., the number of bytes that should be used to store a value of this type.
Otherwise, it return `none`.
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);
/* A "compiler" declaration `x := e` */
typedef pair_ref<name, expr> comp_decl;
typedef list_ref<comp_decl> comp_decls;