From c16951aba6cfe2067e8ac78167d82517500bb087 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 7 Jul 2014 15:40:32 -0700 Subject: [PATCH] fix(library/aliases): aliasing behavior The new test '../../tests/lean/run/alias3.lean' demonstrates the issue being fixed. Signed-off-by: Leonardo de Moura --- library/standard/pair.lean | 2 +- src/frontends/lean/decl_cmds.cpp | 5 +-- src/frontends/lean/inductive_cmd.cpp | 10 ++--- src/library/aliases.cpp | 64 ++++++++++++++++++++++------ src/library/aliases.h | 6 +++ src/library/scoped_ext.cpp | 6 ++- src/library/scoped_ext.h | 8 ++-- tests/lean/run/alias3.lean | 26 +++++++++++ 8 files changed, 99 insertions(+), 28 deletions(-) create mode 100644 tests/lean/run/alias3.lean diff --git a/library/standard/pair.lean b/library/standard/pair.lean index e46243b7c..bc6f135f6 100644 --- a/library/standard/pair.lean +++ b/library/standard/pair.lean @@ -27,7 +27,7 @@ section := pair_rec (λ x y, refl (mk_pair x y)) p end -instance pair.pair_inhabited +instance pair_inhabited precedence `×`:30 infixr × := pair diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index f41589a2d..820df0c90 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -273,10 +273,9 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) { levels section_ls = collect_section_levels(ls, p); expr ref = mk_app(mk_explicit(mk_constant(real_n, section_ls)), section_ps); p.add_local_expr(n, ref); - } else { - if (real_n != n) - env = add_alias(env, n, mk_constant(real_n)); } + if (real_n != n) + env = add_decl_alias(env, n, mk_constant(real_n)); level_param_names new_ls; if (is_theorem) { // TODO(Leo): delay theorems diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp index 20a84decc..065cda287 100644 --- a/src/frontends/lean/inductive_cmd.cpp +++ b/src/frontends/lean/inductive_cmd.cpp @@ -498,18 +498,16 @@ struct inductive_cmd_fn { } /** \brief Create an alias for the fully qualified name \c full_id. */ - environment create_alias(environment const & env, name const & full_id, levels const & section_leves, buffer const & section_params) { + environment create_alias(environment env, name const & full_id, levels const & section_leves, buffer const & section_params) { name id(full_id.get_string()); if (in_section(env)) { expr r = mk_explicit(mk_constant(full_id, section_leves)); r = mk_app(r, section_params); m_p.add_local_expr(id, r); - return env; - } else if (full_id != id) { - return add_alias(env, id, mk_constant(full_id)); - } else { - return env; } + if (full_id != id) + env = add_decl_alias(env, id, mk_constant(full_id)); + return env; } /** \brief Add aliases for the inductive datatype, introduction and elimination rules */ diff --git a/src/library/aliases.cpp b/src/library/aliases.cpp index 0bfe9ab96..8d5e39c71 100644 --- a/src/library/aliases.cpp +++ b/src/library/aliases.cpp @@ -24,21 +24,28 @@ static environment update(environment const & env, aliases_ext const & ext); struct aliases_ext : public environment_extension { struct state { + bool m_in_section; rb_map, name_quick_cmp> m_aliases; rb_map m_inv_aliases; rb_map m_level_aliases; rb_map m_inv_level_aliases; + state():m_in_section(false) {} + + void add_alias(name const & a, expr const & e) { + auto it = m_aliases.find(a); + if (it) + m_aliases.insert(a, list(e, filter(*it, [&](expr const & t) { return t != e; }))); + else + m_aliases.insert(a, list(e)); + m_inv_aliases.insert(e, a); + } }; + state m_state; list m_scopes; void add_alias(name const & a, expr const & e) { - auto it = m_state.m_aliases.find(a); - if (it) - m_state.m_aliases.insert(a, list(e, filter(*it, [&](expr const & t) { return t != e; }))); - else - m_state.m_aliases.insert(a, list(e)); - m_state.m_inv_aliases.insert(e, a); + m_state.add_alias(a, e); } void add_alias(name const & a, level const & l) { @@ -49,8 +56,31 @@ struct aliases_ext : public environment_extension { m_state.m_inv_level_aliases.insert(l, a); } - void push() { + list add_decl_alias_core(list const & scopes, name const & a, expr const & e) { + if (empty(scopes)) { + return scopes; + } else { + state s = head(scopes); + s.add_alias(a, e); + if (s.m_in_section) { + return cons(s, add_decl_alias_core(tail(scopes), a, e)); + } else { + return cons(s, tail(scopes)); + } + } + } + + void add_decl_alias(name const & a, expr const & e) { + if (m_state.m_in_section) { + m_scopes = add_decl_alias_core(m_scopes, a, e); + } else { + add_alias(a, e); + } + } + + void push(bool in_section) { m_scopes = list(m_state, m_scopes); + m_state.m_in_section = in_section; } void pop() { @@ -63,16 +93,16 @@ struct aliases_ext : public environment_extension { return env; } - static environment push_scope(environment const & env) { + static environment push_scope(environment const & env, bool in_section) { aliases_ext ext = get_extension(env); - ext.push(); + ext.push(in_section); environment new_env = update(env, ext); - if (!in_section(new_env)) + if (!::lean::in_section(new_env)) new_env = add_aliases(new_env, get_namespace(new_env), name()); return new_env; } - static environment pop_scope(environment const & env) { + static environment pop_scope(environment const & env, bool) { aliases_ext ext = get_extension(env); ext.pop(); return update(env, ext); @@ -102,6 +132,12 @@ environment add_alias(environment const & env, name const & a, expr const & e) { return update(env, ext); } +environment add_decl_alias(environment const & env, name const & a, expr const & e) { + aliases_ext ext = get_extension(env); + ext.add_decl_alias(a, e); + return update(env, ext); +} + optional is_aliased(environment const & env, expr const & t) { auto it = get_extension(env).m_state.m_inv_aliases.find(t); return it ? optional(*it) : optional(); @@ -112,9 +148,13 @@ list get_alias_exprs(environment const & env, name const & n) { return it ? *it : list(); } -environment add_alias(environment const & env, name const & a, level const & l) { +static void check_no_shadow(environment const & env, name const & a) { if (env.is_universe(a)) throw exception(sstream() << "universe level alias '" << a << "' shadows existing global universe level"); +} + +environment add_alias(environment const & env, name const & a, level const & l) { + check_no_shadow(env, a); aliases_ext ext = get_extension(env); ext.add_alias(a, l); return update(env, ext); diff --git a/src/library/aliases.h b/src/library/aliases.h index 37cc2e214..6e4e9de99 100644 --- a/src/library/aliases.h +++ b/src/library/aliases.h @@ -12,6 +12,12 @@ Author: Leonardo de Moura namespace lean { /** \brief Add the alias \c a for expression \c e. \c e must not have free variables. */ environment add_alias(environment const & env, name const & a, expr const & e); +/** + \brief Add alias \c a for expression \c e, and also add it to all parent scopes + until in a namespace scope. +*/ +environment add_decl_alias(environment const & env, name const & a, expr const & e); + /** \brief If \c t is aliased in \c env, then return its name. Otherwise, return none. */ optional is_aliased(environment const & env, expr const & t); diff --git a/src/library/scoped_ext.cpp b/src/library/scoped_ext.cpp index 3e1856d53..99cfdb543 100644 --- a/src/library/scoped_ext.cpp +++ b/src/library/scoped_ext.cpp @@ -64,13 +64,14 @@ environment using_namespace(environment const & env, io_state const & ios, name environment push_scope(environment const & env, io_state const & ios, name const & n) { if (!n.is_anonymous() && in_section(env)) throw exception("invalid namespace declaration, a namespace cannot be declared inside a section"); + bool in_section = n.is_anonymous(); name new_n = get_namespace(env) + n; scope_mng_ext ext = get_extension(env); ext.m_namespaces = list(new_n, ext.m_namespaces); ext.m_in_section = list(n.is_anonymous(), ext.m_in_section); environment r = update(env, ext); for (auto const & t : get_exts()) { - r = std::get<2>(t)(r); + r = std::get<2>(t)(r, in_section); } if (!n.is_anonymous()) r = using_namespace(r, ios, n); @@ -81,11 +82,12 @@ environment pop_scope(environment const & env) { scope_mng_ext ext = get_extension(env); if (is_nil(ext.m_namespaces)) throw exception("invalid end of scope, there are no open namespaces/sections"); + bool in_section = head(ext.m_in_section); ext.m_namespaces = tail(ext.m_namespaces); ext.m_in_section = tail(ext.m_in_section); environment r = update(env, ext); for (auto const & t : get_exts()) { - r = std::get<3>(t)(r); + r = std::get<3>(t)(r, in_section); } return r; } diff --git a/src/library/scoped_ext.h b/src/library/scoped_ext.h index 352803afa..10725d4a5 100644 --- a/src/library/scoped_ext.h +++ b/src/library/scoped_ext.h @@ -16,8 +16,8 @@ Author: Leonardo de Moura namespace lean { typedef environment (*using_namespace_fn)(environment const &, io_state const &, name const &); -typedef environment (*push_scope_fn)(environment const &); -typedef environment (*pop_scope_fn)(environment const &); +typedef environment (*push_scope_fn)(environment const &, bool); +typedef environment (*pop_scope_fn)(environment const &, bool); void register_scoped_ext(name const & n, using_namespace_fn use, push_scope_fn push, pop_scope_fn pop); /** \brief Use objects defined in the namespace \c n, if \c c is not the anonymous name, then only object from "class" \c c are considered. */ @@ -137,10 +137,10 @@ public: static environment using_namespace_fn(environment const & env, io_state const & ios, name const & n) { return update(env, get(env).using_namespace(env, ios, n)); } - static environment push_fn(environment const & env) { + static environment push_fn(environment const & env, bool) { return update(env, get(env).push()); } - static environment pop_fn(environment const & env) { + static environment pop_fn(environment const & env, bool) { return update(env, get(env).pop()); } static environment register_entry(environment const & env, io_state const & ios, name const & n, entry const & e) { diff --git a/tests/lean/run/alias3.lean b/tests/lean/run/alias3.lean new file mode 100644 index 000000000..399e019e3 --- /dev/null +++ b/tests/lean/run/alias3.lean @@ -0,0 +1,26 @@ +import logic + +namespace N1 + section + section + variable A : Type + definition foo (a : A) : Bool := true + check foo + end + check foo + end + check foo +end +check N1.foo + +namespace N2 + section + parameter A : Type + inductive list : Type := + | nil {} : list + | cons : A → list → list + check list + end + check list +end +check N2.list