From 0fbfef8eb0e1003f42ca9fc29a0512fe64f6950a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 16 Aug 2013 18:37:01 -0700
Subject: [PATCH] Remove sanitize_names from kernel

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/context.cpp      | 39 +++++++++++++------------------------
 src/kernel/context.h        | 12 ------------
 src/tests/kernel/occurs.cpp |  3 ---
 3 files changed, 13 insertions(+), 41 deletions(-)

diff --git a/src/kernel/context.cpp b/src/kernel/context.cpp
index 843573a593..a3a75814d4 100644
--- a/src/kernel/context.cpp
+++ b/src/kernel/context.cpp
@@ -5,35 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "context.h"
-#include "occurs.h"
 #include "exception.h"
 
 namespace lean {
-context sanitize_names_core(context const & c, context const & r, unsigned sz, expr const * es) {
-    if (is_nil(c)) {
-        return c;
-    } else {
-        // Remark: if this code is a bottleneck, then we can collect
-        // all used names in r and es[sz] once and avoid the multiple
-        // calls to occurs.
-        context new_tail = sanitize_names_core(tail(c), r, sz, es);
-        context_entry const & e = head(c);
-        name const & n = e.get_name();
-        name n1    = n;
-        unsigned i = 1;
-        while (occurs(n1, r, sz, es) ||
-               std::any_of(new_tail.begin(), new_tail.end(), [&](context_entry const & e2) { return n1 == e2.get_name(); })) {
-            n1 = name(n, i);
-            i++;
-        }
-        return extend(new_tail, n1, e.get_domain(), e.get_body());
-    }
-}
-
-context sanitize_names(context const & c, unsigned sz, expr const * es) {
-    return sanitize_names_core(c, c, sz, es);
-}
-
 std::pair<context_entry const &, context const &> lookup_ext(context const & c, unsigned i) {
     context const * it1 = &c;
     while (*it1) {
@@ -55,4 +29,17 @@ context_entry const & lookup(context const & c, unsigned i) {
     }
     throw exception("unknown free variable");
 }
+
+/**
+    \brief Return a new context where the names used in the context
+    entries of \c c do not shadow constants occurring in \c c and \c es[sz].
+
+    Recall that the names in context entries are just "suggestions".
+    These names are used to name free variables in \c es[sz] (and
+    dependent entries in \c c).
+*/
+context sanitize_names(context const & c, unsigned sz, expr const * es);
+inline context sanitize_names(context const & c, expr const & e) { return sanitize_names(c, 1, &e); }
+inline context sanitize_names(context const & c, std::initializer_list<expr> const & l) { return sanitize_names(c, l.size(), l.begin()); }
+
 }
diff --git a/src/kernel/context.h b/src/kernel/context.h
index 344e541bd3..c2b97a770f 100644
--- a/src/kernel/context.h
+++ b/src/kernel/context.h
@@ -45,16 +45,4 @@ inline context extend(context const & c, name const & n, expr const & d) {
 inline bool is_empty(context const & c) {
     return is_nil(c);
 }
-
-/**
-    \brief Return a new context where the names used in the context
-    entries of \c c do not shadow constants occurring in \c c and \c es[sz].
-
-    Recall that the names in context entries are just "suggestions".
-    These names are used to name free variables in \c es[sz] (and
-    dependent entries in \c c).
-*/
-context sanitize_names(context const & c, unsigned sz, expr const * es);
-inline context sanitize_names(context const & c, expr const & e) { return sanitize_names(c, 1, &e); }
-inline context sanitize_names(context const & c, std::initializer_list<expr> const & l) { return sanitize_names(c, l.size(), l.begin()); }
 }
diff --git a/src/tests/kernel/occurs.cpp b/src/tests/kernel/occurs.cpp
index 349e8eec06..dd7d7bd20e 100644
--- a/src/tests/kernel/occurs.cpp
+++ b/src/tests/kernel/occurs.cpp
@@ -51,9 +51,6 @@ static void tst2() {
     auto p = lookup_ext(c, 0);
     lean_assert(p.first.get_name() == "a");
     lean_assert(length(p.second) == 0);
-    std::cout << sanitize_names(c, f(a));
-    lean_assert(lookup(sanitize_names(c, f(a)), 0).get_name() != name("a"));
-    std::cout << sanitize_names(c, f(b));
 }
 
 int main() {