From d7ed1560a9e3ed57e9905f6c6e179818abc9f2d4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 26 Sep 2013 14:20:11 -0700
Subject: [PATCH] feat(name_generator): add name_generator for unique names
 modulo a prefix

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/tests/util/name.cpp   | 13 +++++++++++++
 src/util/name_generator.h | 27 +++++++++++++++++++++++++++
 2 files changed, 40 insertions(+)
 create mode 100644 src/util/name_generator.h

diff --git a/src/tests/util/name.cpp b/src/tests/util/name.cpp
index 0513cf461..e487aeba6 100644
--- a/src/tests/util/name.cpp
+++ b/src/tests/util/name.cpp
@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <sstream>
 #include "util/test.h"
 #include "util/name.h"
+#include "util/name_generator.h"
 using namespace lean;
 
 static void tst1() {
@@ -112,6 +113,17 @@ static void tst8() {
     std::cout << u1 << " " << u2 << "\n";
 }
 
+static void tst9() {
+    name_generator g("a");
+    lean_assert(g.prefix() == "a");
+    name n0 = g.next();
+    name n1 = g.next();
+    name a0(name("a"), 0u);
+    name a1(name("a"), 1u);
+    lean_assert(n0 == a0);
+    lean_assert(n1 == a1);
+}
+
 int main() {
     tst1();
     tst2();
@@ -121,5 +133,6 @@ int main() {
     tst6();
     tst7();
     tst8();
+    tst9();
     return has_violations() ? 1 : 0;
 }
diff --git a/src/util/name_generator.h b/src/util/name_generator.h
new file mode 100644
index 000000000..86a5de9d8
--- /dev/null
+++ b/src/util/name_generator.h
@@ -0,0 +1,27 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "util/name.h"
+
+namespace lean {
+/**
+   \brief A generator of unique names modulo a prefix.
+   If the prefix is unique (i.e., it is not the prefix of any other name in the system), then
+   all generated names are unique.
+*/
+class name_generator {
+    name     m_prefix;
+    unsigned m_next_idx;
+public:
+    name_generator(name const & prefix):m_prefix(prefix), m_next_idx(0) { lean_assert(!prefix.is_anonymous()); }
+
+    name const & prefix() const { return m_prefix; }
+
+    /** \brief Return a unique name modulo \c prefix. */
+    name next() { name r(m_prefix, m_next_idx); m_next_idx++; return r; }
+};
+}