From 6f03df871bdefb27920df209827e4154e1af2e8d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 6 Nov 2018 14:38:39 -0800
Subject: [PATCH] chore(library/compiler): remove `whnf_upto_runtime_type`

It is not needed anymore.
---
 src/library/compiler/erase_irrelevant.cpp |  7 +------
 src/library/compiler/llnf.cpp             |  2 +-
 src/library/compiler/util.cpp             | 13 -------------
 src/library/compiler/util.h               |  1 -
 4 files changed, 2 insertions(+), 21 deletions(-)

diff --git a/src/library/compiler/erase_irrelevant.cpp b/src/library/compiler/erase_irrelevant.cpp
index a71c6605af..e468212b93 100644
--- a/src/library/compiler/erase_irrelevant.cpp
+++ b/src/library/compiler/erase_irrelevant.cpp
@@ -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))
diff --git a/src/library/compiler/llnf.cpp b/src/library/compiler/llnf.cpp
index 6a402000d1..d770c0c2b6 100644
--- a/src/library/compiler/llnf.cpp
+++ b/src/library/compiler/llnf.cpp
@@ -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;
diff --git a/src/library/compiler/util.cpp b/src/library/compiler/util.cpp
index b017aea0a1..559064c7f3 100644
--- a/src/library/compiler/util.cpp
+++ b/src/library/compiler/util.cpp
@@ -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()  ||
diff --git a/src/library/compiler/util.h b/src/library/compiler/util.h
index b0c8da55a3..38d03cf02e 100644
--- a/src/library/compiler/util.h
+++ b/src/library/compiler/util.h
@@ -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);