From 7ff791eb9f4d23faab3c97d0970e2262132e4acd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 30 Nov 2013 10:22:57 -0800
Subject: [PATCH] feat(util/name_set): add mk_unique (with respect to a
 name_set)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/tests/util/name.cpp | 12 ++++++++++++
 src/util/CMakeLists.txt |  6 +++---
 src/util/name_set.cpp   | 20 ++++++++++++++++++++
 src/util/name_set.h     |  5 +++++
 4 files changed, 40 insertions(+), 3 deletions(-)
 create mode 100644 src/util/name_set.cpp

diff --git a/src/tests/util/name.cpp b/src/tests/util/name.cpp
index 1032cfa9b..8becec283 100644
--- a/src/tests/util/name.cpp
+++ b/src/tests/util/name.cpp
@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "util/test.h"
 #include "util/name.h"
 #include "util/name_generator.h"
+#include "util/name_set.h"
 using namespace lean;
 
 static void tst1() {
@@ -146,6 +147,16 @@ static void tst11() {
     lean_assert(n2 == name("a"));
 }
 
+static void tst12() {
+    name_set s;
+    s.insert(name("foo"));
+    s.insert(name(name("foo"), 1));
+    s.insert(name("bla"));
+    lean_assert(mk_unique(s, name("boo")) == name("boo"));
+    lean_assert(mk_unique(s, name("bla")) == name(name("bla"), 1));
+    lean_assert(mk_unique(s, name("foo")) == name(name("foo"), 2));
+}
+
 int main() {
     tst1();
     tst2();
@@ -158,5 +169,6 @@ int main() {
     tst9();
     tst10();
     tst11();
+    tst12();
     return has_violations() ? 1 : 0;
 }
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index 17fe157ca..3d09b4622 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -1,6 +1,6 @@
-add_library(util trace.cpp debug.cpp name.cpp exception.cpp
-  interrupt.cpp hash.cpp escaped.cpp bit_tricks.cpp safe_arith.cpp
-  ascii.cpp memory.cpp shared_mutex.cpp realpath.cpp
+add_library(util trace.cpp debug.cpp name.cpp name_set.cpp
+  exception.cpp interrupt.cpp hash.cpp escaped.cpp bit_tricks.cpp
+  safe_arith.cpp ascii.cpp memory.cpp shared_mutex.cpp realpath.cpp
   script_state.cpp script_exception.cpp splay_map.cpp lua.cpp
   luaref.cpp)
 
diff --git a/src/util/name_set.cpp b/src/util/name_set.cpp
new file mode 100644
index 000000000..03d3df124
--- /dev/null
+++ b/src/util/name_set.cpp
@@ -0,0 +1,20 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "util/name_set.h"
+
+namespace lean {
+name mk_unique(name_set const & s, name const & suggestion) {
+    name n = suggestion;
+    int i  = 1;
+    while (true) {
+        if (s.find(n) == s.end())
+            return n;
+        n = name(suggestion, i);
+        i++;
+    }
+}
+}
diff --git a/src/util/name_set.h b/src/util/name_set.h
index c4ef2bcc8..e28a05a44 100644
--- a/src/util/name_set.h
+++ b/src/util/name_set.h
@@ -9,4 +9,9 @@ Author: Leonardo de Moura
 #include "util/name.h"
 namespace lean {
 typedef std::unordered_set<name, name_hash, name_eq> name_set;
+/**
+   \brief Make a name that does not occur in \c s, based on
+   the given suggestion.
+*/
+name mk_unique(name_set const & s, name const & suggestion);
 }