From e14814d4bf6910668285cde10b0c15c936a040cb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 3 Sep 2014 15:01:13 -0700 Subject: [PATCH] feat(frontends/lean): add '[protected]' modifier Signed-off-by: Leonardo de Moura --- src/frontends/lean/decl_cmds.cpp | 17 ++++++-- src/frontends/lean/token_table.cpp | 2 +- src/library/CMakeLists.txt | 3 +- src/library/aliases.cpp | 7 +++- src/library/protected.cpp | 57 ++++++++++++++++++++++++++ src/library/protected.h | 15 +++++++ tests/lean/protected.lean | 10 +++++ tests/lean/protected.lean.expected.out | 2 + 8 files changed, 105 insertions(+), 8 deletions(-) create mode 100644 src/library/protected.cpp create mode 100644 src/library/protected.h create mode 100644 tests/lean/protected.lean create mode 100644 tests/lean/protected.lean.expected.out diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 5ddc7aa7d..07e03fe4e 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/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) { diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 08d7aae7c..7cab355ea 100644 --- a/src/frontends/lean/token_table.cpp +++ b/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", diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 1b9c66efe..4e20e6e54 100644 --- a/src/library/CMakeLists.txt +++ b/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}) diff --git a/src/library/aliases.cpp b/src/library/aliases.cpp index a11794764..92dc6a005 100644 --- a/src/library/aliases.cpp +++ b/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"); diff --git a/src/library/protected.cpp b/src/library/protected.cpp new file mode 100644 index 000000000..ba87849d8 --- /dev/null +++ b/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 +#include +#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()); } +}; + +static protected_ext_reg g_ext; +static protected_ext const & get_extension(environment const & env) { + return static_cast(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(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 &, + std::function &) { + 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); +} +} diff --git a/src/library/protected.h b/src/library/protected.h new file mode 100644 index 000000000..a11fbea4f --- /dev/null +++ b/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); +} diff --git a/tests/lean/protected.lean b/tests/lean/protected.lean new file mode 100644 index 000000000..e0ab83a02 --- /dev/null +++ b/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 diff --git a/tests/lean/protected.lean.expected.out b/tests/lean/protected.lean.expected.out new file mode 100644 index 000000000..ab504a802 --- /dev/null +++ b/tests/lean/protected.lean.expected.out @@ -0,0 +1,2 @@ +protected.lean:9:6: error: unknown identifier 'C' +D : Prop