From 67f4698593ea63763e8f3f460ee6d68f55c232ee Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 7 Mar 2019 12:48:16 -0800
Subject: [PATCH] feat(library/compiler): do not generate code for decls that
 have irrelevant types

We were generating hundreds of definitions that just return
`lean::box(0)`.
---
 src/library/compiler/compiler.cpp |  6 +++++-
 src/library/compiler/compiler.h   |  2 +-
 src/library/compiler/lcnf.cpp     | 19 +------------------
 src/library/compiler/util.cpp     |  5 +++++
 src/library/compiler/util.h       |  1 +
 5 files changed, 13 insertions(+), 20 deletions(-)

diff --git a/src/library/compiler/compiler.cpp b/src/library/compiler/compiler.cpp
index 3289ca0420..43f0a203d9 100644
--- a/src/library/compiler/compiler.cpp
+++ b/src/library/compiler/compiler.cpp
@@ -136,10 +136,14 @@ bool is_main_fn_type(expr const & type) {
     }
 }
 
-environment compile(environment const & env, options const & opts, names const & cs) {
+environment compile(environment const & env, options const & opts, names cs) {
     if (!is_codegen_enabled(opts))
         return env;
 
+    /* Do not generate code for irrelevant decls */
+    cs = filter(cs, [&](name const & c) { return !is_irrelevant_type(env, env.get(c).get_type());});
+    if (empty(cs)) return env;
+
     for (name const & c : cs) {
         if (is_main_fn(env, c) && !is_main_fn_type(env.get(c).get_type())) {
             throw exception("invalid `main` function, it must have type `list string -> io uint32`");
diff --git a/src/library/compiler/compiler.h b/src/library/compiler/compiler.h
index 03919e34d3..16c1fe8b3b 100644
--- a/src/library/compiler/compiler.h
+++ b/src/library/compiler/compiler.h
@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include "kernel/environment.h"
 namespace lean {
-environment compile(environment const & env, options const & opts, names const & cs);
+environment compile(environment const & env, options const & opts, names cs);
 inline environment compile(environment const & env, options const & opts, name const & c) {
     return compile(env, opts, names(c));
 }
diff --git a/src/library/compiler/lcnf.cpp b/src/library/compiler/lcnf.cpp
index 1056f02a1c..5fd6fabd57 100644
--- a/src/library/compiler/lcnf.cpp
+++ b/src/library/compiler/lcnf.cpp
@@ -317,25 +317,8 @@ public:
         default:
             break;
         }
-
         if (is_lc_proof(e)) return false;
-
-        type_checker tc(m_st, m_lctx);
-        e_type = tc.whnf(e_type);
-        if (is_sort(e_type)) {
-            return false;
-        } else if (tc.is_prop(e_type)) {
-            return false;
-        } else if (is_pi(e_type)) {
-            /* Functions that return types are not relevant */
-            flet<local_ctx> save_lctx(m_lctx, m_lctx);
-            while (is_pi(e_type)) {
-                expr fvar = m_lctx.mk_local_decl(ngen(), binding_name(e_type), binding_domain(e_type));
-                e_type = whnf(instantiate(binding_body(e_type), fvar));
-            }
-            if (is_sort(e_type))
-                return false;
-        }
+        if (is_irrelevant_type(m_st, m_lctx, e_type)) return false;
         return true;
     }
 
diff --git a/src/library/compiler/util.cpp b/src/library/compiler/util.cpp
index 0599b4d8b2..4e92dc53df 100644
--- a/src/library/compiler/util.cpp
+++ b/src/library/compiler/util.cpp
@@ -434,6 +434,11 @@ bool is_irrelevant_type(type_checker::state & st, local_ctx lctx, expr const & t
     return false;
 }
 
+bool is_irrelevant_type(environment const & env, expr const & type) {
+    type_checker::state st(env);
+    return is_irrelevant_type(st, local_context(), type);
+}
+
 void collect_used(expr const & e, name_hash_set & S) {
     if (!has_fvar(e)) return;
     for_each(e, [&](expr const & e, unsigned) {
diff --git a/src/library/compiler/util.h b/src/library/compiler/util.h
index 9a6d3460a7..c968aab3f7 100644
--- a/src/library/compiler/util.h
+++ b/src/library/compiler/util.h
@@ -148,6 +148,7 @@ inline bool is_runtime_builtin_type(expr const & e) {
 bool is_runtime_scalar_type(name const & n);
 
 bool is_irrelevant_type(type_checker::state & st, local_ctx lctx, expr const & type);
+bool is_irrelevant_type(environment const & env, expr const & type);
 
 void collect_used(expr const & e, name_hash_set & S);
 /* Return true iff `e` contains a free variable in `s` */