From 56305e46723cb619aaba96ad2160e4962f1114e4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 14 Aug 2013 14:00:30 -0700
Subject: [PATCH] Add sanitize_names for (local) contexts

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

diff --git a/src/kernel/context.cpp b/src/kernel/context.cpp
index ff75dc88b..7913712f8 100644
--- a/src/kernel/context.cpp
+++ b/src/kernel/context.cpp
@@ -5,10 +5,36 @@ 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"
 #include "expr_formatter.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);
+}
+
 format pp(expr_formatter & fmt, context const & c) {
     if (c) {
         format r;
diff --git a/src/kernel/context.h b/src/kernel/context.h
index d621acd55..535cb9c93 100644
--- a/src/kernel/context.h
+++ b/src/kernel/context.h
@@ -35,6 +35,19 @@ inline context extend(context const & c, name const & n, expr const & d) {
 inline bool 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()); }
+
 class expr_formatter;
 format pp(expr_formatter & f, context const & c);
 std::ostream & operator<<(std::ostream & out, context const & c);
diff --git a/src/tests/kernel/occurs.cpp b/src/tests/kernel/occurs.cpp
index 6ce9c20ab..c5a4b963c 100644
--- a/src/tests/kernel/occurs.cpp
+++ b/src/tests/kernel/occurs.cpp
@@ -38,8 +38,19 @@ static void tst1() {
     lean_assert(!occurs(f(b), c));
 }
 
+static void tst2() {
+    expr f = Const("f");
+    expr a = Const("a");
+    expr b = Const("b");
+    context c;
+    c = extend(c, "a", Type());
+    std::cout << sanitize_names(c, f(a)) << "\n";
+    std::cout << sanitize_names(c, f(b)) << "\n";
+}
+
 int main() {
     continue_on_violation(true);
     tst1();
+    tst2();
     return has_violations() ? 1 : 0;
 }