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

@@ -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;
 }

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; }
+};
+}