feat(library): add namespace management

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

src/library/CMakeLists.txt

@@ -2,7 +2,7 @@ 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
-  private.cpp placeholder.cpp aliases.cpp)
+  private.cpp placeholder.cpp aliases.cpp scope.cpp)
 # fo_unify.cpp hop_match.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})

src/library/kernel_bindings.h

@@ -23,7 +23,7 @@ UDATA_DEFS(substitution)
 UDATA_DEFS(io_state)
 int push_optional_expr(lua_State * L, optional<expr> const & e);
 int push_optional_justification(lua_State * L, optional<justification> const & j);
-int push_optional_definition(lua_State * L, optional<definition> const & d);
+int push_optional_declaration(lua_State * L, optional<declaration> const & e);
 /**
    \brief Return the formatter object associated with the given Lua State.
    This procedure checks for options at:

src/library/register_module.h

@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "library/private.h"
 #include "library/placeholder.h"
 #include "library/aliases.h"
+#include "library/scope.h"
 // #include "library/fo_unify.h"
 // #include "library/hop_match.h"
 
@@ -23,6 +24,7 @@ inline void open_core_module(lua_State * L) {
     open_private(L);
     open_placeholder(L);
     open_aliases(L);
+    open_scope(L);
     // open_fo_unify(L);
     // open_hop_match(L);
 }

src/library/scope.cpp

@@ -0,0 +1,118 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <memory>
+#include "util/list.h"
+#include "library/scope.h"
+#include "library/kernel_bindings.h"
+
+namespace lean {
+struct scope_ext : public environment_extension {
+    enum class scope_kind { Namespace, Section };
+    struct section {
+        environment m_prev_env;
+    };
+    list<name>       m_namespaces;
+    list<section>    m_sections;
+    list<scope_kind> m_scope_kinds;
+    scope_ext() {}
+};
+
+struct scope_ext_reg {
+    unsigned m_ext_id;
+    scope_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<scope_ext>()); }
+};
+
+static scope_ext_reg g_ext;
+static scope_ext const & get_extension(environment const & env) {
+    return static_cast<scope_ext const &>(env.get_extension(g_ext.m_ext_id));
+}
+static environment update(environment const & env, scope_ext const & ext) {
+    return env.update(g_ext.m_ext_id, std::make_shared<scope_ext>(ext));
+}
+
+environment begin_section_scope(environment const & env) {
+    // TODO(Leo)
+    return env;
+}
+
+environment begin_namespace_scope(environment const & env, char const * n) {
+    scope_ext ext = get_extension(env);
+    ext.m_scope_kinds = list<scope_ext::scope_kind>(scope_ext::scope_kind::Namespace, ext.m_scope_kinds);
+    ext.m_namespaces  = list<name>(name(get_namespace(env), n), ext.m_namespaces);
+    return update(env, ext);
+}
+
+environment end_scope(environment const & env) {
+    scope_ext ext = get_extension(env);
+    if (is_nil(ext.m_scope_kinds))
+        throw exception("environment does not have open scopes");
+    switch (head(ext.m_scope_kinds)) {
+    case scope_ext::scope_kind::Namespace:
+        ext.m_namespaces = tail(ext.m_namespaces);
+        break;
+    case scope_ext::scope_kind::Section:
+        // TODO(Leo)
+        break;
+    }
+    ext.m_scope_kinds = tail(ext.m_scope_kinds);
+    return update(env, ext);
+}
+
+name const & get_namespace(environment const & env) {
+    scope_ext const & ext = get_extension(env);
+    if (is_nil(ext.m_namespaces))
+        return name::anonymous();
+    else
+        return head(ext.m_namespaces);
+}
+
+optional<declaration> find(environment const & env, name const & n) {
+    scope_ext const & ext = get_extension(env);
+    for (auto const & p : ext.m_namespaces) {
+        name full_name = p + n;
+        if (auto d = env.find(full_name)) {
+            return d;
+        }
+    }
+    return env.find(n);
+}
+
+name get_name_in_namespace(environment const & env, name const & n) {
+    if (auto d = env.find(n)) {
+        scope_ext const & ext = get_extension(env);
+        for (auto const & p : ext.m_namespaces) {
+            if (is_prefix_of(p, n)) {
+                name r = n.replace_prefix(p, name());
+                if (auto d2 = find(env, r)) {
+                    if (is_eqp(*d, *d2))
+                        return r;
+                }
+                return n;
+            }
+        }
+    }
+    return n;
+}
+
+static int begin_section_scope(lua_State * L) { return push_environment(L, begin_section_scope(to_environment(L, 1))); }
+static int begin_namespace_scope(lua_State * L) { return push_environment(L, begin_namespace_scope(to_environment(L, 1), lua_tostring(L, 2))); }
+static int end_scope(lua_State * L) { return push_environment(L, end_scope(to_environment(L, 1))); }
+static int get_namespace(lua_State * L) { return push_name(L, get_namespace(to_environment(L, 1))); }
+static int get_name_in_namespace(lua_State * L) {
+    return push_name(L, get_name_in_namespace(to_environment(L, 1), to_name_ext(L, 2)));
+}
+static int find_decl(lua_State * L) { return push_optional_declaration(L, find(to_environment(L, 1), to_name_ext(L, 2))); }
+
+void open_scope(lua_State * L) {
+    SET_GLOBAL_FUN(begin_section_scope,   "begin_section_scope");
+    SET_GLOBAL_FUN(begin_namespace_scope, "begin_namespace_scope");
+    SET_GLOBAL_FUN(end_scope,             "end_scope");
+    SET_GLOBAL_FUN(get_namespace,         "get_namespace");
+    SET_GLOBAL_FUN(get_name_in_namespace, "get_name_in_namespace");
+    SET_GLOBAL_FUN(find_decl,             "find_decl");
+}
+}

src/library/scope.h

@@ -0,0 +1,49 @@
+/*
+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 <string>
+#include "util/lua.h"
+#include "kernel/environment.h"
+
+namespace lean {
+/**
+   \brief Create a section scope. When a section is closed all definitions and theorems are relativized with
+   respect to var_decls and axioms. That is, var_decls and axioms become new arguments for the definitions and axioms.
+*/
+environment begin_section_scope(environment const & env);
+
+/**
+   \brief Create a namespace scope. A namespace is just a mechanism
+   for appending the prefix n to declarations added to the
+   environment.
+*/
+environment begin_namespace_scope(environment const & env, char const * n);
+
+/**
+   \brief End/close a scoped created using \c begin_section_scope or \c begin_namespace_scope.
+   Throws an exception if there is no open scope.
+*/
+environment end_scope(environment const & env);
+
+/**
+   \brief Return the current namespace for \c env. The namespace is composed by the sequence
+   of names provided to \c begin_namespace_scope.
+*/
+name const & get_namespace(environment const & env);
+
+/**
+   \brief Return the name of \c n in the current namespace of \c env.
+   Example: if the current namespace is <tt>foo.bar</tt> and \c n is <tt>foo.bar.bla.1</tt>, then
+   the result is <tt>bla.1</tt>.
+*/
+name get_name_in_namespace(environment const & env, name const & n);
+
+/** \brief Find a declaration named \c n in \c env by taking the active namespaces into account. */
+optional<declaration> find(environment const & env, name const & n);
+
+void open_scope(lua_State * L);
+}

tests/lua/namespace1.lua

@@ -0,0 +1,23 @@
+local env = environment()
+env = begin_namespace_scope(env, "foo")
+assert(get_namespace(env) == name("foo"))
+env = add_decl(env, mk_var_decl(name(get_namespace(env), "nat"), Type))
+env = add_decl(env, mk_var_decl(name(get_namespace(env), "int"), Type))
+env = begin_namespace_scope(env, "bar")
+assert(get_namespace(env) == name("foo", "bar"))
+assert(find_decl(env, "int"):name() == name("foo", "int"))
+assert(find_decl(env, "nat"):name() == name("foo", "nat"))
+env = add_decl(env, mk_var_decl(name(get_namespace(env), "int"), Type))
+assert(find_decl(env, "int"):name() == name("foo", "bar", "int"))
+assert(get_name_in_namespace(env, name("foo", "bar", "int")) == name("int"))
+assert(get_name_in_namespace(env, name("foo", "int")) == name("foo", "int")) -- it was shadowed by foo.bar.int
+assert(get_name_in_namespace(env, name("foo", "nat")) == name("nat"))
+env = end_scope(env)
+assert(get_namespace(env) == name("foo"))
+assert(get_name_in_namespace(env, name("foo", "bar", "int")) == name("bar", "int"))
+assert(get_name_in_namespace(env, name("foo", "nat")) == name("nat"))
+env = end_scope(env)
+assert(get_name_in_namespace(env, name("foo", "bar", "int")) == name("foo", "bar", "int"))
+assert(get_name_in_namespace(env, name("foo", "nat")) == name("foo", "nat"))
+check_error(function() env = end_scope(env) end)
+assert(get_namespace(env) == name())