From 34110945f276f4b64bc7b77b037db15abc581dc7 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 5 Feb 2019 13:57:25 +0100
Subject: [PATCH] refactor(library/compiler/llnf): replace
 `is_runtime_builtin_cnstr` with just `is_builtin_constant`

---
 src/library/compiler/llnf.cpp |  4 ++--
 src/library/compiler/util.cpp | 16 ----------------
 src/library/compiler/util.h   |  3 ---
 3 files changed, 2 insertions(+), 21 deletions(-)

diff --git a/src/library/compiler/llnf.cpp b/src/library/compiler/llnf.cpp
index b16f5e6245..806bf9acd4 100644
--- a/src/library/compiler/llnf.cpp
+++ b/src/library/compiler/llnf.cpp
@@ -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));
diff --git a/src/library/compiler/util.cpp b/src/library/compiler/util.cpp
index 3096f8c325..8cbab39e36 100644
--- a/src/library/compiler/util.cpp
+++ b/src/library/compiler/util.cpp
@@ -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;
diff --git a/src/library/compiler/util.h b/src/library/compiler/util.h
index 33495b750a..09ce3915ce 100644
--- a/src/library/compiler/util.h
+++ b/src/library/compiler/util.h
@@ -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);