From 2016e1bce548ffba3936319f452453313e46442f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 25 Jan 2019 12:51:32 -0800
Subject: [PATCH] feat(library/compiler/llnf): unique names for lambda
 arguments

---
 src/library/compiler/llnf.cpp | 8 ++++----
 src/library/compiler/llnf.h   | 2 ++
 2 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/library/compiler/llnf.cpp b/src/library/compiler/llnf.cpp
index 9a4a79956d..3e33e0a895 100644
--- a/src/library/compiler/llnf.cpp
+++ b/src/library/compiler/llnf.cpp
@@ -446,7 +446,7 @@ class to_llnf_fn {
         buffer<expr> binding_fvars;
         while (is_lambda(e)) {
             lean_assert(!has_loose_bvars(binding_domain(e)));
-            expr new_fvar = m_lctx.mk_local_decl(ngen(), binding_name(e), binding_domain(e), binding_info(e));
+            expr new_fvar = m_lctx.mk_local_decl(ngen(), next_name(), binding_domain(e), binding_info(e));
             binding_fvars.push_back(new_fvar);
             e = binding_body(e);
         }
@@ -924,7 +924,7 @@ public:
     }
 };
 
-static expr get_constant_ll_type(environment const & env, name const & c) {
+expr get_constant_ll_type(environment const & env, name const & c) {
     if (optional<expr> type = get_builtin_constant_ll_type(c)) {
         return *type;
     } else {
@@ -1111,7 +1111,7 @@ class explicit_boxing_fn {
         buffer<expr> binding_fvars;
         while (is_lambda(e)) {
             lean_assert(!has_loose_bvars(binding_domain(e)));
-            expr new_fvar = m_lctx.mk_local_decl(ngen(), binding_name(e), binding_domain(e), binding_info(e));
+            expr new_fvar = m_lctx.mk_local_decl(ngen(), next_name(), binding_domain(e), binding_info(e));
             binding_fvars.push_back(new_fvar);
             e = binding_body(e);
         }
@@ -1842,7 +1842,7 @@ class explicit_rc_fn {
         unsigned i = 0;
         while (is_lambda(e)) {
             lean_assert(!has_loose_bvars(binding_domain(e)));
-            expr new_fvar = m_lctx.mk_local_decl(ngen(), binding_name(e), binding_domain(e), binding_info(e));
+            expr new_fvar = m_lctx.mk_local_decl(ngen(), next_name(), binding_domain(e), binding_info(e));
             lean_assert(i < borrowed.size());
             if (borrowed[i])
                 m_borrowed.insert(fvar_name(new_fvar));
diff --git a/src/library/compiler/llnf.h b/src/library/compiler/llnf.h
index bb4811ecc2..9f6f0765f3 100644
--- a/src/library/compiler/llnf.h
+++ b/src/library/compiler/llnf.h
@@ -41,6 +41,8 @@ inline bool is_llnf_sset(expr const & e) { unsigned d1, d2, d3; return is_llnf_s
 inline bool is_llnf_uset(expr const & e) { unsigned d; return is_llnf_uset(e, d); }
 inline bool is_llnf_box(expr const & e) { unsigned n; return is_llnf_box(e, n); }
 
+expr get_constant_ll_type(environment const & env, name const & c);
+
 void initialize_llnf();
 void finalize_llnf();
 }