michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/scoped_ext): sections are just "nameless" namespaces

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-11 17:35:59 -07:00
parent 158682219f
commit 78b8a67015
4 changed files with 21 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/decl_cmds.cpp
View file

@ -153,7 +153,7 @@ optional<binder_info> 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());

14
src/library/aliases.cpp
View file

@ -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<list<name>> m_aliases;
name_map<name> m_inv_aliases;
name_map<name> m_level_aliases;
name_map<name> 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;
}

6
src/library/scoped_ext.cpp
View file

@ -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;

15
src/library/scoped_ext.h
View file

@ -37,9 +37,8 @@ bool has_open_scopes(environment const & env);
name const & get_namespace(environment const & env);
list<name> 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<typename Config, bool TransientSection = false>
template<typename Config>
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 Config, bool TransientSection>
typename scoped_ext<Config, TransientSection>::reg * scoped_ext<Config, TransientSection>::g_ext = nullptr;
template<typename Config>
typename scoped_ext<Config>::reg * scoped_ext<Config>::g_ext = nullptr;
void initialize_scoped_ext();
void finalize_scoped_ext();