From 1062dcbbea0a82eea365594660d17cd25ff34701 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 11 Sep 2019 13:04:08 -0700
Subject: [PATCH] refactor(src/library/compiler/erase_irrelevant): move
 `has_trivial_structure` to `util`

---
 src/library/compiler/erase_irrelevant.cpp | 35 +----------------------
 src/library/compiler/util.cpp             | 25 ++++++++++++++++
 src/library/compiler/util.h               |  4 +++
 3 files changed, 30 insertions(+), 34 deletions(-)

diff --git a/src/library/compiler/erase_irrelevant.cpp b/src/library/compiler/erase_irrelevant.cpp
index 38d2489b91..3a4f2b325a 100644
--- a/src/library/compiler/erase_irrelevant.cpp
+++ b/src/library/compiler/erase_irrelevant.cpp
@@ -18,7 +18,6 @@ class erase_irrelevant_fn {
     local_ctx            m_lctx;
     buffer<expr>         m_let_fvars;
     buffer<let_entry>    m_let_entries;
-    name_map<list<bool>> m_constructor_info;
     name                 m_x;
     unsigned             m_next_idx{1};
     expr_map<bool>       m_irrelevant_cache;
@@ -37,40 +36,8 @@ class erase_irrelevant_fn {
         return type_checker(m_st, m_lctx).infer(e);
     }
 
-    void get_constructor_info(name const & n, buffer<bool> & rel_fields) {
-        if (auto r = m_constructor_info.find(n)) {
-            to_buffer(*r, rel_fields);
-        } else {
-            get_constructor_relevant_fields(env(), n, rel_fields);
-            m_constructor_info.insert(n, to_list(rel_fields));
-        }
-    }
-
-    /* Return (some idx) iff inductive datatype `I_name` is safe, has only one constructor,
-       and this constructor has only one relevant field, `idx` is the field position. */
     optional<unsigned> has_trivial_structure(name const & I_name) {
-        if (is_runtime_builtin_type(I_name))
-            return optional<unsigned>();
-        inductive_val I_val = env().get(I_name).to_inductive_val();
-        if (I_val.is_unsafe())
-            return optional<unsigned>();
-        if (I_val.get_ncnstrs() != 1)
-            return optional<unsigned>();
-        buffer<bool> rel_fields;
-        get_constructor_info(head(I_val.get_cnstrs()), rel_fields);
-        /* The following #pragma is to disable a bogus g++ 4.9 warning at `optional<unsigned> r` */
-        #if defined(__GNUC__) && !defined(__CLANG__)
-        #pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
-        #endif
-        optional<unsigned> result;
-        for (unsigned i = 0; i < rel_fields.size(); i++) {
-            if (rel_fields[i]) {
-                if (result)
-                    return optional<unsigned>();
-                result = i;
-            }
-        }
-        return result;
+        return ::lean::has_trivial_structure(env(), I_name);
     }
 
     expr mk_runtime_type(expr e) {
diff --git a/src/library/compiler/util.cpp b/src/library/compiler/util.cpp
index 555e3af251..cc790b0e62 100644
--- a/src/library/compiler/util.cpp
+++ b/src/library/compiler/util.cpp
@@ -433,6 +433,31 @@ bool depends_on(expr const & e, name_hash_set const & s) {
     return found;
 }
 
+optional<unsigned> has_trivial_structure(environment const & env, name const & I_name) {
+    if (is_runtime_builtin_type(I_name))
+        return optional<unsigned>();
+    inductive_val I_val = env.get(I_name).to_inductive_val();
+    if (I_val.is_unsafe())
+        return optional<unsigned>();
+    if (I_val.get_ncnstrs() != 1)
+        return optional<unsigned>();
+    buffer<bool> rel_fields;
+    get_constructor_relevant_fields(env, head(I_val.get_cnstrs()), rel_fields);
+    /* The following #pragma is to disable a bogus g++ 4.9 warning at `optional<unsigned> r` */
+    #if defined(__GNUC__) && !defined(__CLANG__)
+    #pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
+    #endif
+    optional<unsigned> result;
+    for (unsigned i = 0; i < rel_fields.size(); i++) {
+        if (rel_fields[i]) {
+            if (result)
+                return optional<unsigned>();
+            result = i;
+        }
+    }
+    return result;
+}
+
 expr mk_runtime_type(type_checker::state & st, local_ctx const & lctx, expr e) {
     try {
         type_checker tc(st, lctx);
diff --git a/src/library/compiler/util.h b/src/library/compiler/util.h
index 0f5d3e5e59..97aeff61af 100644
--- a/src/library/compiler/util.h
+++ b/src/library/compiler/util.h
@@ -134,6 +134,10 @@ bool is_enf_object_type(expr const & e);
 bool is_llnf_void_type(expr const & e);
 bool is_llnf_unboxed_type(expr const & type);
 
+/* Return (some idx) iff inductive datatype `I_name` is safe, has only one constructor,
+   and this constructor has only one relevant field, `idx` is the field position. */
+optional<unsigned> has_trivial_structure(environment const & env, name const & I_name);
+
 expr mk_runtime_type(type_checker::state & st, local_ctx const & lctx, expr e);
 
 // =======================================