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

refactor(library/compiler/llnf): replace is_runtime_builtin_cnstr with just is_builtin_constant

Browse source
This commit is contained in:
Sebastian Ullrich 2019-02-05 13:57:25 +01:00 • committed by Leonardo de Moura
parent 11860a65eb
commit 34110945f2
3 changed files with 2 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -527,7 +527,7 @@ class to_llnf_fn {
buffer<expr> args;
expr const & k = get_app_args(e, args);
lean_assert(is_constant(k));
if (is_runtime_builtin_cnstr(const_name(k))) {
if (is_builtin_constant(const_name(k))) {
/* Optimization is not applicable to runtime builtin constructors. */
return e;
}
@ -764,7 +764,7 @@ class to_llnf_fn {
buffer<expr> args;
expr const & k = get_app_args(e, args);
lean_assert(is_constant(k));
if (is_runtime_builtin_cnstr(const_name(k)))
if (is_builtin_constant(const_name(k)))
return visit_app_default(e);
constructor_val k_val = env().get(const_name(k)).to_constructor_val();
cnstr_info k_info = get_cnstr_info(const_name(k));

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

@ -413,22 +413,6 @@ bool is_runtime_scalar_type(name const & n) {
n == get_usize_name();
}
bool is_runtime_builtin_cnstr(name const & n) {
// TODO(Leo): add array type constructors, task constructor,
// universe level constructors, and expression constructors.
/* Remark: we don't need to include `nat.zero` and `nat.zero` because
they are converted into literals or addition. */
return
n == get_thunk_mk_name() ||
n == get_string_mk_name() ||
n == get_string_iterator_mk_name() ||
n == get_int_of_nat_name() ||
n == get_int_neg_succ_of_nat_name() ||
n == get_lean_name_mk_numeral_name() ||
n == get_lean_name_mk_string_name();
}
bool is_irrelevant_type(type_checker::state & st, local_ctx lctx, expr const & type) {
if (is_sort(type) || type_checker(st, lctx).is_prop(type))
return true;

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

@ -146,9 +146,6 @@ inline bool is_runtime_builtin_type(expr const & e) {
/* Return true if `n` is the name of a type that is treated as a scalar type by the code generator. */
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);
bool is_irrelevant_type(type_checker::state & st, local_ctx lctx, expr const & type);
void collect_used(expr const & e, name_hash_set & S);