From 78b8a67015dfe0e201ac4052ddff74b8cdc0cd67 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 11 Oct 2014 17:35:59 -0700 Subject: [PATCH] refactor(library/scoped_ext): sections are just "nameless" namespaces --- src/frontends/lean/decl_cmds.cpp | 2 +- src/library/aliases.cpp | 14 +++++++------- src/library/scoped_ext.cpp | 6 ++++++ src/library/scoped_ext.h | 15 +++++++-------- 4 files changed, 21 insertions(+), 16 deletions(-) diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 047d6183bb..39c8775c2c 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -153,7 +153,7 @@ optional parse_binder_info(parser & p, variable_kind k) { } static void check_variable_kind(parser & p, variable_kind k) { - if (in_section_or_context(p.env())) { + if (in_context(p.env())) { if (k == variable_kind::Axiom || k == variable_kind::Constant) throw parser_error("invalid declaration, 'constant/axiom' cannot be used in sections/contexts", p.pos()); diff --git a/src/library/aliases.cpp b/src/library/aliases.cpp index 2552c9ecd8..0fa8bb7842 100644 --- a/src/library/aliases.cpp +++ b/src/library/aliases.cpp @@ -25,12 +25,12 @@ static environment update(environment const & env, aliases_ext const & ext); struct aliases_ext : public environment_extension { struct state { - bool m_in_section_or_context; + bool m_in_context; name_map> m_aliases; name_map m_inv_aliases; name_map m_level_aliases; name_map m_inv_level_aliases; - state():m_in_section_or_context(false) {} + state():m_in_context(false) {} void add_expr_alias(name const & a, name const & e) { auto it = m_aliases.find(a); @@ -63,7 +63,7 @@ struct aliases_ext : public environment_extension { } else { state s = head(scopes); s.add_expr_alias(a, e); - if (s.m_in_section_or_context) { + if (s.m_in_context) { return cons(s, add_expr_alias_rec_core(tail(scopes), a, e)); } else { return cons(s, tail(scopes)); @@ -72,16 +72,16 @@ struct aliases_ext : public environment_extension { } void add_expr_alias_rec(name const & a, name const & e) { - if (m_state.m_in_section_or_context) { + if (m_state.m_in_context) { m_scopes = add_expr_alias_rec_core(m_scopes, a, e); } else { add_expr_alias(a, e); } } - void push(bool in_section_or_context) { + void push(bool in_context) { m_scopes = cons(m_state, m_scopes); - m_state.m_in_section_or_context = in_section_or_context; + m_state.m_in_context = in_context; } void pop() { @@ -107,7 +107,7 @@ struct aliases_ext : public environment_extension { aliases_ext ext = get_extension(env); ext.push(k != scope_kind::Namespace); environment new_env = update(env, ext); - if (!::lean::in_section_or_context(new_env)) + if (!::lean::in_context(new_env)) new_env = add_aliases(new_env, get_namespace(new_env), name()); return new_env; } diff --git a/src/library/scoped_ext.cpp b/src/library/scoped_ext.cpp index 9252455ee2..600aa2ab3e 100644 --- a/src/library/scoped_ext.cpp +++ b/src/library/scoped_ext.cpp @@ -60,6 +60,10 @@ bool in_context(environment const & env) { return !is_nil(ext.m_scope_kinds) && head(ext.m_scope_kinds) == scope_kind::Context; } +bool in_section(environment const & env) { + return in_section_or_context(env) && !in_context(env); +} + environment using_namespace(environment const & env, io_state const & ios, name const & n, name const & c) { environment r = env; for (auto const & t : get_exts()) { @@ -94,6 +98,8 @@ static std::string * g_new_namespace_key = nullptr; environment push_scope(environment const & env, io_state const & ios, scope_kind k, name const & n) { if (k == scope_kind::Namespace && in_section_or_context(env)) throw exception("invalid namespace declaration, a namespace cannot be declared inside a section or context"); + if (k == scope_kind::Section && in_context(env)) + throw exception("invalid section declaration, a section cannot be declared inside a context"); name new_n = get_namespace(env); if (k == scope_kind::Namespace) new_n = new_n + n; diff --git a/src/library/scoped_ext.h b/src/library/scoped_ext.h index 86b6d75538..a32d34d8c4 100644 --- a/src/library/scoped_ext.h +++ b/src/library/scoped_ext.h @@ -37,9 +37,8 @@ bool has_open_scopes(environment const & env); name const & get_namespace(environment const & env); list const & get_namespaces(environment const & env); -bool in_section_or_context(environment const & env); bool in_context(environment const & env); -inline bool in_section(environment const & env) { return in_section_or_context(env) && !in_context(env); } +bool in_section(environment const & env); /** \brief Check if \c n may be a reference to a namespace, if it is return it. The procedure checks if \c n is a registered namespace, if it is not, it tries @@ -58,7 +57,7 @@ void open_scoped_ext(lua_State * L); \brief Auxilary template used to simplify the creation of environment extensions that support the scope */ -template +template class scoped_ext : public environment_extension { typedef typename Config::state state; typedef typename Config::entry entry; @@ -182,13 +181,13 @@ public: return get(env).export_namespace(env, ios, n); } static environment push_fn(environment const & env, scope_kind k) { - if (k != scope_kind::Section || TransientSection) + if (k != scope_kind::Section) return update(env, get(env).push()); else return env; } static environment pop_fn(environment const & env, scope_kind k) { - if (k != scope_kind::Section || TransientSection) + if (k != scope_kind::Section) return update(env, get(env).pop()); else return env; @@ -200,7 +199,7 @@ public: if (auto h = get_fingerprint(e)) { env = update_fingerprint(env, *h); } - if ((!TransientSection && in_context(env)) || (TransientSection && in_section_or_context(env))) { + if (in_context(env)) { return update(env, get(env)._add_tmp_entry(env, ios, e)); } else { name n = get_namespace(env); @@ -231,8 +230,8 @@ public: } }; -template -typename scoped_ext::reg * scoped_ext::g_ext = nullptr; +template +typename scoped_ext::reg * scoped_ext::g_ext = nullptr; void initialize_scoped_ext(); void finalize_scoped_ext();