feat(frontends/lean): add '[protected]' modifier

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

src/frontends/lean/decl_cmds.cpp

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "library/scoped_ext.h"
 #include "library/aliases.h"
 #include "library/private.h"
+#include "library/protected.h"
 #include "library/placeholder.h"
 #include "library/locals.h"
 #include "library/explicit.h"
@@ -25,6 +26,7 @@ static name g_rcurly("}");
 static name g_colon(":");
 static name g_assign(":=");
 static name g_private("[private]");
+static name g_protected("[protected]");
 static name g_inline("[inline]");
 static name g_instance("[instance]");
 static name g_coercion("[coercion]");
@@ -159,14 +161,16 @@ environment axiom_cmd(parser & p)    {
 
 struct decl_modifiers {
     bool m_is_private;
+    bool m_is_protected;
     bool m_is_opaque;
     bool m_is_instance;
     bool m_is_coercion;
     decl_modifiers() {
-        m_is_private  = false;
-        m_is_opaque   = true;
-        m_is_instance = false;
-        m_is_coercion = false;
+        m_is_private   = false;
+        m_is_protected = false;
+        m_is_opaque    = true;
+        m_is_instance  = false;
+        m_is_coercion  = false;
     }
 
     void parse(parser & p) {
@@ -174,6 +178,9 @@ struct decl_modifiers {
             if (p.curr_is_token(g_private)) {
                 m_is_private = true;
                 p.next();
+            } else if (p.curr_is_token(g_protected)) {
+                m_is_protected = true;
+                p.next();
             } else if (p.curr_is_token(g_inline)) {
                 m_is_opaque = false;
                 p.next();
@@ -341,6 +348,8 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
         env = add_instance(env, real_n);
     if (modifiers.m_is_coercion)
         env = add_coercion(env, real_n, p.ios());
+    if (modifiers.m_is_protected)
+        env = add_protected(env, real_n);
     return env;
 }
 environment definition_cmd(parser & p) {

src/frontends/lean/token_table.cpp

@@ -74,7 +74,7 @@ token_table init_token_table() {
          {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}};
 
     char const * commands[] = {"theorem", "axiom", "variable", "definition", "coercion",
-                               "variables", "[private]", "[inline]", "[fact]", "[instance]", "[module]", "[coercion]",
+                               "variables", "[private]", "[protected]", "[inline]", "[fact]", "[instance]", "[module]", "[coercion]",
                                "abbreviation", "opaque_hint", "evaluate", "check", "print", "end", "namespace", "section", "import",
                                "abbreviation", "inductive", "record", "renaming", "extends", "structure", "module", "universe",
                                "precedence", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context",

src/library/CMakeLists.txt

@@ -8,6 +8,7 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
   unifier.cpp unifier_plugin.cpp inductive_unifier_plugin.cpp
   explicit.cpp num.cpp string.cpp opaque_hints.cpp head_map.cpp
   match.cpp definition_cache.cpp declaration_index.cpp
-  print.cpp annotation.cpp typed_expr.cpp let.cpp type_util.cpp)
+  print.cpp annotation.cpp typed_expr.cpp let.cpp type_util.cpp
+  protected.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})

src/library/aliases.cpp

@@ -16,6 +16,7 @@ Author: Leonardo de Moura
 #include "library/aliases.h"
 #include "library/placeholder.h"
 #include "library/scoped_ext.h"
+#include "library/protected.h"
 
 namespace lean {
 struct aliases_ext;
@@ -190,14 +191,16 @@ environment add_aliases(environment const & env, name const & prefix, name const
                         unsigned num_exceptions, name const * exceptions) {
     aliases_ext ext = get_extension(env);
     env.for_each_declaration([&](declaration const & d) {
-            if (is_prefix_of(prefix, d.get_name()) && !is_exception(d.get_name(), prefix, num_exceptions, exceptions)) {
+            if (!is_protected(env, d.get_name()) &&
+                is_prefix_of(prefix, d.get_name()) && !is_exception(d.get_name(), prefix, num_exceptions, exceptions)) {
                 name a        = d.get_name().replace_prefix(prefix, new_prefix);
                 if (!a.is_anonymous())
                     ext.add_expr_alias(a, d.get_name());
             }
         });
     env.for_each_universe([&](name const & u) {
-            if (is_prefix_of(prefix, u) && !is_exception(u, prefix, num_exceptions, exceptions)) {
+            if (!is_protected(env, u) &&
+                is_prefix_of(prefix, u) && !is_exception(u, prefix, num_exceptions, exceptions)) {
                 name a = u.replace_prefix(prefix, new_prefix);
                 if (env.is_universe(a))
                     throw exception(sstream() << "universe level alias '" << a << "' shadows existing global universe level");

src/library/protected.cpp

@@ -0,0 +1,57 @@
+/*
+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 <utility>
+#include <string>
+#include "util/name_set.h"
+#include "library/protected.h"
+#include "library/module.h"
+
+namespace lean {
+struct protected_ext : public environment_extension {
+    name_set m_protected; // protected declarations
+};
+
+struct protected_ext_reg {
+    unsigned m_ext_id;
+    protected_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<protected_ext>()); }
+};
+
+static protected_ext_reg g_ext;
+static protected_ext const & get_extension(environment const & env) {
+    return static_cast<protected_ext const &>(env.get_extension(g_ext.m_ext_id));
+}
+static environment update(environment const & env, protected_ext const & ext) {
+    return env.update(g_ext.m_ext_id, std::make_shared<protected_ext>(ext));
+}
+
+static std::string g_prt_key("prt");
+
+environment add_protected(environment const & env, name const & n) {
+    protected_ext ext = get_extension(env);
+    ext.m_protected.insert(n);
+    environment new_env = update(env, ext);
+    return module::add(new_env, g_prt_key, [=](serializer & s) { s << n; });
+}
+
+static void protected_reader(deserializer & d, module_idx, shared_environment & senv,
+                             std::function<void(asynch_update_fn const &)> &,
+                             std::function<void(delayed_update_fn const &)> &) {
+    name n;
+    d >> n;
+    senv.update([=](environment const & env) -> environment {
+            protected_ext ext = get_extension(env);
+            ext.m_protected.insert(n);
+            return update(env, ext);
+        });
+}
+
+register_module_object_reader_fn g_protected_reader(g_prt_key, protected_reader);
+
+bool is_protected(environment const & env, name const & n) {
+    return get_extension(env).m_protected.contains(n);
+}
+}

src/library/protected.h

@@ -0,0 +1,15 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "kernel/environment.h"
+
+namespace lean {
+/** \brief Mark \c n as protected, protected declarations are ignored by wildcard 'open' command */
+environment add_protected(environment const & env, name const & n);
+/** \brief Return true iff \c n was marked as protected in the environment \c n. */
+bool is_protected(environment const & env, name const & n);
+}

tests/lean/protected.lean

@@ -0,0 +1,10 @@
+import logic
+
+namespace foo
+  definition C [protected] := true
+  definition D := true
+end foo
+
+using foo
+check C
+check D

tests/lean/protected.lean.expected.out

@@ -0,0 +1,2 @@
+protected.lean:9:6: error: unknown identifier 'C'
+D : Prop