feat(library): add support for creating 'private/hidden' names

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/library/CMakeLists.txt

@@ -1,7 +1,8 @@
 add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
   kernel_bindings.cpp io_state_stream.cpp bin_app.cpp
   resolve_macro.cpp kernel_serializer.cpp max_sharing.cpp
-  normalize.cpp shared_environment.cpp module.cpp coercion.cpp)
+  normalize.cpp shared_environment.cpp module.cpp coercion.cpp
+  private.cpp)
 # placeholder.cpp fo_unify.cpp hop_match.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})

src/library/private.cpp

@@ -0,0 +1,90 @@
+/*
+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 <utility>
+#include <string>
+#include "util/hash.h"
+#include "library/private.h"
+#include "library/module.h"
+#include "library/kernel_bindings.h"
+
+namespace lean {
+struct private_ext : public environment_extension {
+    unsigned                           m_counter;
+    rb_map<name, name, name_quick_cmp> m_hidden_map;
+    private_ext():m_counter(0) {}
+};
+
+struct private_ext_reg {
+    unsigned m_ext_id;
+    private_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<private_ext>()); }
+};
+
+static private_ext_reg g_ext;
+static private_ext const & get_extension(environment const & env) {
+    return static_cast<private_ext const &>(env.get_extension(g_ext.m_ext_id));
+}
+static environment update(environment const & env, private_ext const & ext) {
+    return env.update(g_ext.m_ext_id, std::make_shared<private_ext>(ext));
+}
+
+static name g_private("private");
+static std::string g_prv_key("prv");
+
+std::pair<environment, name> add_private_name(environment const & env, name const & n, optional<unsigned> const & extra_hash) {
+    private_ext ext = get_extension(env);
+    unsigned h      = hash(n.hash(), ext.m_counter);
+    if (extra_hash)
+        h = hash(h, *extra_hash);
+    name r = name(g_private, h) + n;
+    ext.m_hidden_map.insert(r, n);
+    ext.m_counter++;
+    environment new_env = update(env, ext);
+    new_env = module::add(new_env, g_prv_key, [=](serializer & s) { s << n << r; });
+    return mk_pair(new_env, r);
+}
+
+static void private_reader(deserializer & d, module_idx, shared_environment & senv,
+                           std::function<void(asynch_update_fn const &)> &,
+                           std::function<void(delayed_update_fn const &)> &) {
+    name n, h;
+    d >> n >> h;
+    senv.update([=](environment const & env) -> environment {
+            private_ext ext = get_extension(env);
+            ext.m_hidden_map.insert(h, n);
+            ext.m_counter++;
+            return update(env, ext);
+        });
+}
+
+register_module_object_reader_fn g_private_reader(g_prv_key, private_reader);
+
+optional<name> is_private_name(environment const & env, name const & n) {
+    auto it = get_extension(env).m_hidden_map.find(n);
+    if (it)
+        return optional<name>(*it);
+    else
+        return optional<name>();
+}
+
+static int add_private_name(lua_State * L) {
+    int nargs = lua_gettop(L);
+    optional<unsigned> h;
+    if (nargs > 2)
+        h = lua_tonumber(L, 3);
+    auto p = add_private_name(to_environment(L, 1), to_name_ext(L, 2), h);
+    push_environment(L, p.first);
+    push_name(L, p.second);
+    return 2;
+}
+
+static int is_private_name(lua_State * L) { return push_optional_name(L, is_private_name(to_environment(L, 1), to_name_ext(L, 2))); }
+
+void open_private(lua_State * L) {
+    SET_GLOBAL_FUN(add_private_name, "add_private_name");
+    SET_GLOBAL_FUN(is_private_name, "is_private_name");
+}
+}

src/library/private.h

@@ -0,0 +1,34 @@
+/*
+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 <utility>
+#include "util/optional.h"
+#include "util/lua.h"
+#include "kernel/environment.h"
+
+namespace lean {
+/**
+   \brief This is an auxiliary function used to simulate private declarations. Whenever we want to create a "private"
+   declaration, this module creates an internal "hidden" name that is not accessible to users.
+   In principle, users can access the internal names if they want by applying themselves the procedure used to create
+   the "hidden" names.
+
+   The optional \c base_hash can be used to influence the "hidden" name associated with \c n.
+
+   The mapping between \c n and the "hidden" name is saved  in the .olean files.
+*/
+std::pair<environment, name> add_private_name(environment const & env, name const & n, optional<unsigned> const & base_hash);
+
+/**
+   \brief If n is a "private" name in \c env created using \c
+   add_private_name, then return the "hidden" name associated with it.
+   Otherwise, return none.
+*/
+optional<name> is_private_name(environment const & env, name const & n);
+
+void open_private(lua_State * L);
+}

src/library/register_module.h

@@ -9,6 +9,8 @@ Author: Leonardo de Moura
 #include "library/kernel_bindings.h"
 #include "library/resolve_macro.h"
 #include "library/coercion.h"
+#include "library/private.h"
+
 // #include "library/fo_unify.h"
 // #include "library/hop_match.h"
 // #include "library/placeholder.h"
@@ -18,6 +20,7 @@ inline void open_core_module(lua_State * L) {
     open_kernel_module(L);
     open_resolve_macro(L);
     open_coercion(L);
+    open_private(L);
     // open_fo_unify(L);
     // open_placeholder(L);
     // open_hop_match(L);

tests/lua/prv.lua

@@ -0,0 +1,24 @@
+local env = environment()
+env, n1 = add_private_name(env, "foo")
+print(n1)
+env, n2 = add_private_name(env, "foo")
+print(n2)
+env, n3 = add_private_name(env, {"foo", "bla"})
+print(n3)
+assert(n1 ~= n2)
+assert(n1 ~= n3)
+assert(n2 ~= n3)
+assert(is_private_name(env, n1))
+assert(is_private_name(env, n1) == name("foo"))
+assert(is_private_name(env, n2) == name("foo"))
+assert(is_private_name(env, n3) == name("foo", "bla"))
+
+env:export("prv_mod.olean")
+local env2 = import_modules("prv_mod")
+assert(is_private_name(env2, n1) == name("foo"))
+assert(is_private_name(env2, n2) == name("foo"))
+assert(is_private_name(env2, n3) == name("foo", "bla"))
+env2, n4 = add_private_name(env2, "foo")
+print(n4)
+assert(n1 ~= n4)
+assert(not is_private_name(env, n4))