From ff725b83291d2dcfbf8064e898b3dd0b68408546 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 17 Sep 2018 19:56:35 -0700
Subject: [PATCH] feat(library/compiler): simplify cheap beta reduction

The LCNF format contained may `let`-declarations of the form
```
x : (fun y, c) a := t
```
where `c` does not depend on `y`.
We reduce them to
```
x : c := t
```
---
 src/library/compiler/csimp.cpp |  2 +-
 src/library/compiler/lcnf.cpp  |  2 +-
 src/library/compiler/util.cpp  | 18 ++++++++++++++++++
 src/library/compiler/util.h    |  4 ++++
 4 files changed, 24 insertions(+), 2 deletions(-)

diff --git a/src/library/compiler/csimp.cpp b/src/library/compiler/csimp.cpp
index 1fdc968ecb..9bb7279249 100644
--- a/src/library/compiler/csimp.cpp
+++ b/src/library/compiler/csimp.cpp
@@ -63,7 +63,7 @@ class csimp_fn {
         if (is_atom(e)) {
             return e;
         } else {
-            expr type = infer_type(e);
+            expr type = head_beta_const_fn(infer_type(e));
             expr fvar = m_lctx.mk_local_decl(ngen(), next_name(), type, e);
             m_fvars.push_back(fvar);
             return fvar;
diff --git a/src/library/compiler/lcnf.cpp b/src/library/compiler/lcnf.cpp
index 5a00a6fb22..87b59cb41c 100644
--- a/src/library/compiler/lcnf.cpp
+++ b/src/library/compiler/lcnf.cpp
@@ -48,7 +48,7 @@ public:
     }
 
     expr mk_let_decl(expr const & e) {
-        expr type = infer_type(e);
+        expr type = head_beta_const_fn(infer_type(e));
         /* Remark: we use `m_x.append_after(m_next_idx)` instead of `name(m_x, m_next_idx)`
            because the resulting name is confusing during debugging: it looks like a projection application.
            We should replace it with `name(m_x, m_next_idx)` when the compiler code gets more stable. */
diff --git a/src/library/compiler/util.cpp b/src/library/compiler/util.cpp
index 9f4fbc6765..b711a8ec4f 100644
--- a/src/library/compiler/util.cpp
+++ b/src/library/compiler/util.cpp
@@ -9,6 +9,24 @@ Author: Leonardo de Moura
 #include "library/constants.h"
 
 namespace lean {
+expr head_beta_const_fn(expr const & e) {
+    if (!is_app(e)) return e;
+    expr fn = get_app_fn(e);
+    if (!is_lambda(fn)) return e;
+    buffer<expr> args;
+    get_app_args(e, args);
+    unsigned i = 0;
+    while (is_lambda(fn) && i < args.size()) {
+        expr const & body = binding_body(fn);
+        if (has_loose_bvars(body))
+            break;
+        i++;
+        fn = body;
+    }
+    if (i == 0) return e;
+    return mk_app(fn, args.size() - i, args.data() + i);
+}
+
 bool is_cases_on_recursor(environment const & env, name const & n) {
     return ::lean::is_aux_recursor(env, n) && n.get_string() == "cases_on";
 }
diff --git a/src/library/compiler/util.h b/src/library/compiler/util.h
index 76048c1e44..1758718d87 100644
--- a/src/library/compiler/util.h
+++ b/src/library/compiler/util.h
@@ -11,6 +11,10 @@ Author: Leonardo de Moura
 #include "library/util.h"
 
 namespace lean {
+/* If `e` is of the form `(fun x, t) a` return `head_beta_const_fn(t)` if `t` does not depend on `x`,
+   and `e` otherwise. */
+expr head_beta_const_fn(expr const & e);
+
 /* Return true if the given argument is mdata relevant to the compiler
 
    Remark: we currently don't keep any metadata in the compiler. */