From 028bf36152dd5a0e30fa97d2ef25a56d75afe150 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 12 Dec 2016 08:23:37 -0800
Subject: [PATCH] feat(library/compiler): eliminate unused let declarations

---
 src/library/compiler/CMakeLists.txt       |  2 +-
 src/library/compiler/elim_unused_lets.cpp | 59 +++++++++++++++++++++++
 src/library/compiler/elim_unused_lets.h   | 11 +++++
 src/library/compiler/preprocess.cpp       |  4 ++
 4 files changed, 75 insertions(+), 1 deletion(-)
 create mode 100644 src/library/compiler/elim_unused_lets.cpp
 create mode 100644 src/library/compiler/elim_unused_lets.h

diff --git a/src/library/compiler/CMakeLists.txt b/src/library/compiler/CMakeLists.txt
index c0c3c86609..eb4f114e22 100644
--- a/src/library/compiler/CMakeLists.txt
+++ b/src/library/compiler/CMakeLists.txt
@@ -2,4 +2,4 @@ add_library(compiler OBJECT util.cpp eta_expansion.cpp simp_pr1_rec.cpp preproce
   compiler_step_visitor.cpp elim_recursors.cpp comp_irrelevant.cpp
   inliner.cpp rec_fn_macro.cpp erase_irrelevant.cpp reduce_arity.cpp
   lambda_lifting.cpp simp_inductive.cpp nat_value.cpp
-  vm_compiler.cpp cse.cpp init_module.cpp)
+  vm_compiler.cpp cse.cpp elim_unused_lets.cpp init_module.cpp)
diff --git a/src/library/compiler/elim_unused_lets.cpp b/src/library/compiler/elim_unused_lets.cpp
new file mode 100644
index 0000000000..4c471caa7f
--- /dev/null
+++ b/src/library/compiler/elim_unused_lets.cpp
@@ -0,0 +1,59 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "kernel/instantiate.h"
+#include "library/locals.h"
+#include "library/compiler/procedure.h"
+#include "library/compiler/compiler_step_visitor.h"
+
+namespace lean {
+class elim_unused_lets_fn : public compiler_step_visitor {
+
+    virtual expr visit_lambda(expr const & e) override {
+        type_context::tmp_locals locals(m_ctx);
+        expr t = e;
+        while (is_lambda(t)) {
+            expr d = instantiate_rev(binding_domain(t), locals.size(), locals.data());
+            locals.push_local(binding_name(t), d, binding_info(t));
+            t = binding_body(t);
+        }
+        t = instantiate_rev(t, locals.size(), locals.data());
+        t = visit(t);
+        return copy_tag(e, locals.mk_lambda(t));
+    }
+
+    virtual expr visit_let(expr const & e) override {
+        type_context::tmp_locals locals(m_ctx);
+        collected_locals used_locals;
+        expr t = e;
+        while (is_let(t)) {
+            expr d = instantiate_rev(let_type(t), locals.size(), locals.data());
+            expr v = visit(instantiate_rev(let_value(t), locals.size(), locals.data()));
+            collect_locals(d, used_locals);
+            collect_locals(v, used_locals);
+            locals.push_let(let_name(t), d, v);
+            t = let_body(t);
+        }
+        t = instantiate_rev(t, locals.size(), locals.data());
+        t = visit(t);
+        collect_locals(t, used_locals);
+        buffer<expr> new_locals;
+        for (expr const & l : locals.as_buffer()) {
+            if (used_locals.contains(l))
+                new_locals.push_back(l);
+        }
+        return copy_tag(e, m_ctx.mk_lambda(new_locals, t));
+    }
+public:
+    elim_unused_lets_fn(environment const & env):compiler_step_visitor(env) {}
+};
+
+void elim_unused_lets(environment const & env, buffer<procedure> & procs) {
+    elim_unused_lets_fn fn(env);
+    for (auto & proc : procs)
+        proc.m_code = fn(proc.m_code);
+}
+}
diff --git a/src/library/compiler/elim_unused_lets.h b/src/library/compiler/elim_unused_lets.h
new file mode 100644
index 0000000000..0aa93c143f
--- /dev/null
+++ b/src/library/compiler/elim_unused_lets.h
@@ -0,0 +1,11 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "library/compiler/procedure.h"
+namespace lean {
+void elim_unused_lets(environment const & env, buffer<procedure> & procs);
+}
diff --git a/src/library/compiler/preprocess.cpp b/src/library/compiler/preprocess.cpp
index 5bac517793..ca7aaba54a 100644
--- a/src/library/compiler/preprocess.cpp
+++ b/src/library/compiler/preprocess.cpp
@@ -32,6 +32,7 @@ Author: Leonardo de Moura
 #include "library/compiler/reduce_arity.h"
 #include "library/compiler/lambda_lifting.h"
 #include "library/compiler/simp_inductive.h"
+#include "library/compiler/elim_unused_lets.h"
 #include "library/compiler/cse.h"
 
 namespace lean {
@@ -227,6 +228,8 @@ public:
         lean_trace(name({"compiler", "lambda_lifting"}), tout() << "\n"; display(procs););
         simp_inductive(m_env, procs);
         lean_trace(name({"compiler", "simplify_inductive"}), tout() << "\n"; display(procs););
+        elim_unused_lets(m_env, procs);
+        lean_trace(name({"compiler", "elim_unused_lets"}), tout() << "\n"; display(procs););
         cse(m_env, procs);
         lean_trace(name({"compiler", "cse"}), tout() << "\n"; display(procs););
         lean_trace(name({"compiler", "preprocess"}), tout() << "\n"; display(procs););
@@ -249,6 +252,7 @@ void initialize_preprocess() {
     register_trace_class({"compiler", "reduce_arity"});
     register_trace_class({"compiler", "lambda_lifting"});
     register_trace_class({"compiler", "simplify_inductive"});
+    register_trace_class({"compiler", "elim_unused_lets"});
     register_trace_class({"compiler", "cse"});
     register_trace_class({"compiler", "preprocess"});
     g_tmp_prefix = new name(name::mk_internal_unique_name());