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

chore(library/compiler): remove whnf_upto_runtime_type

Browse source 
It is not needed anymore.
This commit is contained in:
Leonardo de Moura 2018-11-06 14:38:39 -08:00
parent e63721958b
commit 6f03df871b
4 changed files with 2 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -75,14 +75,9 @@ class erase_irrelevant_fn {
return type_checker(m_st, m_lctx).is_prop(e);
}
expr whnf_type(expr const & e) {
type_checker tc(m_st, m_lctx);
return whnf_upto_runtime_type(tc, e);
}
expr mk_runtime_type(expr e, bool atomic_only = false) {
try {
e = whnf_type(e);
e = type_checker(m_st, m_lctx).whnf(e);
if (is_constant(e)) {
name const & c = const_name(e);
if (is_runtime_scalar_type(c))

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

@ -193,7 +193,7 @@ class to_llnf_fn {
result.push_back(field_info());
} else if (m_unboxed) {
type_checker tc(m_st, lctx);
ftype = whnf_upto_runtime_type(tc, ftype);
ftype = tc.whnf(ftype);
if (optional<unsigned> sz = is_builtin_scalar(ftype)) {
result.push_back(field_info(next_offset, *sz));
next_offset += *sz;

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

@ -356,19 +356,6 @@ bool is_runtime_builtin_type(name const & n) {
n == get_int_name();
}
expr whnf_upto_runtime_type(type_checker & tc, expr e) {
while (true) {
expr e1 = tc.whnf_core(e);
if (is_runtime_builtin_type(e1))
return e1;
if (auto next_e = tc.unfold_definition(e1)) {
e = *next_e;
} else {
return e;
}
}
}
bool is_runtime_scalar_type(name const & n) {
return
n == get_uint8_name() ||

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

@ -141,7 +141,6 @@ bool is_runtime_scalar_type(name const & n);
/* Return true if `n` is the name of a constructor with builtin support in the code generator. */
bool is_runtime_builtin_cnstr(name const & n);
expr whnf_upto_runtime_type(type_checker & tc, expr e);
bool is_irrelevant_type(type_checker::state & st, local_ctx lctx, expr const & type);
void collect_used(expr const & e, std::unordered_set<name, name_hash> & S);