diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 0172b18c5..5e2858441 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -549,7 +549,7 @@ expr parser::parse_id() { if (auto prv_id = user_to_hidden_name(m_env, id)) return save_pos(mk_constant(*prv_id), p); // aliases - auto as = get_aliases(m_env, id); + auto as = get_alias_exprs(m_env, id); if (!is_nil(as)) { buffer new_as; for (auto const & e : as) diff --git a/src/kernel/level.h b/src/kernel/level.h index a23eff63b..e81d86f20 100644 --- a/src/kernel/level.h +++ b/src/kernel/level.h @@ -165,6 +165,7 @@ bool has_param(levels const & ls); /** \brief An arbitrary (monotonic) total order on universe level terms. */ bool is_lt(level const & l1, level const & l2, bool use_hash); bool is_lt(levels const & as, levels const & bs, bool use_hash); +struct level_quick_cmp { int operator()(level const & l1, level const & l2) const { return is_lt(l1, l2, true) ? -1 : (l1 == l2 ? 0 : 1); } }; /** \brief Functional for applying F to each level expressions. */ class for_each_level_fn { diff --git a/src/library/aliases.cpp b/src/library/aliases.cpp index 45b480923..ecbe80839 100644 --- a/src/library/aliases.cpp +++ b/src/library/aliases.cpp @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include #include "util/rb_map.h" #include "util/name_generator.h" +#include "util/sstream.h" #include "kernel/abstract.h" #include "kernel/instantiate.h" #include "library/expr_lt.h" @@ -16,8 +17,10 @@ Author: Leonardo de Moura namespace lean { struct aliases_ext : public environment_extension { - rb_map, name_quick_cmp> m_aliases; - rb_map m_inv_aliases; + rb_map, name_quick_cmp> m_aliases; + rb_map m_inv_aliases; + rb_map m_level_aliases; + rb_map m_inv_level_aliases; void add_alias(name const & a, expr const & e) { auto it = m_aliases.find(a); if (it) @@ -26,6 +29,14 @@ struct aliases_ext : public environment_extension { m_aliases.insert(a, list(e)); m_inv_aliases.insert(e, a); } + + void add_alias(name const & a, level const & l) { + auto it = m_level_aliases.find(a); + if (it) + throw exception(sstream() << "universe level alias '" << a << "' shadows existing alias"); + m_level_aliases.insert(a, l); + m_inv_level_aliases.insert(l, a); + } }; struct aliases_ext_reg { @@ -64,13 +75,34 @@ optional is_aliased(environment const & env, expr const & t) { return it ? optional(*it) : optional(); } -list get_aliases(environment const & env, name const & n) { +list get_alias_exprs(environment const & env, name const & n) { auto it = get_extension(env).m_aliases.find(n); return it ? *it : list(); } +environment add_alias(environment const & env, name const & a, level const & l) { + if (env.is_global_level(a)) + throw exception(sstream() << "universe level alias '" << a << "' shadows existing global universe level"); + aliases_ext ext = get_extension(env); + ext.add_alias(a, l); + return update(env, ext); +} + +optional is_aliased(environment const & env, level const & l) { + auto it = get_extension(env).m_inv_level_aliases.find(l); + return it ? optional(*it) : optional(); +} + +optional get_alias_level(environment const & env, name const & n) { + auto it = get_extension(env).m_level_aliases.find(n); + return it ? some_level(*it) : optional(); +} + static int add_alias(lua_State * L) { - return push_environment(L, add_alias(to_environment(L, 1), to_name_ext(L, 2), to_expr(L, 3))); + if (is_expr(L, 3)) + return push_environment(L, add_alias(to_environment(L, 1), to_name_ext(L, 2), to_expr(L, 3))); + else + return push_environment(L, add_alias(to_environment(L, 1), to_name_ext(L, 2), to_level(L, 3))); } static int add_aliases(lua_State * L) { @@ -83,17 +115,25 @@ static int add_aliases(lua_State * L) { } static int is_aliased(lua_State * L) { - return push_optional_name(L, is_aliased(to_environment(L, 1), to_expr(L, 2))); + if (is_expr(L, 2)) + return push_optional_name(L, is_aliased(to_environment(L, 1), to_expr(L, 2))); + else + return push_optional_name(L, is_aliased(to_environment(L, 1), to_level(L, 2))); } -static int get_aliases(lua_State * L) { - return push_list_expr(L, get_aliases(to_environment(L, 1), to_name_ext(L, 2))); +static int get_alias_exprs(lua_State * L) { + return push_list_expr(L, get_alias_exprs(to_environment(L, 1), to_name_ext(L, 2))); +} + +static int get_alias_level(lua_State * L) { + return push_optional_level(L, get_alias_level(to_environment(L, 1), to_name_ext(L, 2))); } void open_aliases(lua_State * L) { - SET_GLOBAL_FUN(add_alias, "add_alias"); - SET_GLOBAL_FUN(add_aliases, "add_aliases"); - SET_GLOBAL_FUN(is_aliased, "is_aliased"); - SET_GLOBAL_FUN(get_aliases, "get_aliases"); + SET_GLOBAL_FUN(add_alias, "add_alias"); + SET_GLOBAL_FUN(add_aliases, "add_aliases"); + SET_GLOBAL_FUN(is_aliased, "is_aliased"); + SET_GLOBAL_FUN(get_alias_exprs, "get_alias_exprs"); + SET_GLOBAL_FUN(get_alias_level, "get_alias_level"); } } diff --git a/src/library/aliases.h b/src/library/aliases.h index dfc47368d..248839fc2 100644 --- a/src/library/aliases.h +++ b/src/library/aliases.h @@ -10,11 +10,7 @@ Author: Leonardo de Moura #include "kernel/environment.h" namespace lean { -/** - \brief Add the alias \c a for expression \c e. \c e must not have - free variables. Warning messages are generated if the new alias shadows - existing aliases and/or declarations. -*/ +/** \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 Create an alias for each declaration named prefix.rest. @@ -29,7 +25,20 @@ environment add_aliases(environment const & env, name const & prefix, name const optional is_aliased(environment const & env, expr const & t); /** \brief Return expressions associated with the given alias. */ -list get_aliases(environment const & env, name const & n); +list get_alias_exprs(environment const & env, name const & n); + +/** + \brief Add the alias \c a for the level expression \c l. An error is generated if the new alias shadows + existing aliases and/or declarations. We don't have "choice" construct for universe + levels. +*/ +environment add_alias(environment const & env, name const & a, level const & l); + +/** \brief If \c l is aliased in \c env, then return its name. Otherwise, return none. */ +optional is_aliased(environment const & env, level const & l); + +/** \brief Return the level associated with the given alias. */ +optional get_alias_level(environment const & env, name const & n); void open_aliases(lua_State * L); } diff --git a/src/library/kernel_bindings.h b/src/library/kernel_bindings.h index 11c717021..f8fcfd4db 100644 --- a/src/library/kernel_bindings.h +++ b/src/library/kernel_bindings.h @@ -21,6 +21,7 @@ UDATA_DEFS(justification) UDATA_DEFS(constraint) UDATA_DEFS(substitution) UDATA_DEFS(io_state) +int push_optional_level(lua_State * L, optional const & e); int push_optional_expr(lua_State * L, optional const & e); int push_optional_justification(lua_State * L, optional const & j); int push_optional_declaration(lua_State * L, optional const & e); diff --git a/tests/lua/alias1.lua b/tests/lua/alias1.lua index a42f2a76b..effb80822 100644 --- a/tests/lua/alias1.lua +++ b/tests/lua/alias1.lua @@ -19,8 +19,8 @@ env = add_inductive(env, env:for_each(function(d) print(d:name()) end) env = add_aliases(env, "nat", "natural") -assert(get_aliases(env, {"natural", "zero"}):head() == zero) -assert(get_aliases(env, {"natural", "nat"}):head() == nat) +assert(get_alias_exprs(env, {"natural", "zero"}):head() == zero) +assert(get_alias_exprs(env, {"natural", "nat"}):head() == nat) assert(is_aliased(env, nat) == name("natural", "nat")) env = add_inductive(env, @@ -29,15 +29,15 @@ env = add_inductive(env, name("list", "cons"), Pi({{A, U_l, true}}, mk_arrow(A, list_l(A), list_l(A)))) env = add_aliases(env, "list", "lst") -print(not get_aliases(env, {"lst", "list_rec"}):is_nil()) +print(not get_alias_exprs(env, {"lst", "list_rec"}):is_nil()) env = add_aliases(env, "list") -print(get_aliases(env, "list_rec"):head()) -assert(not get_aliases(env, "list_rec"):is_nil()) -assert(not get_aliases(env, {"lst", "list_rec"}):is_nil()) +print(get_alias_exprs(env, "list_rec"):head()) +assert(not get_alias_exprs(env, "list_rec"):is_nil()) +assert(not get_alias_exprs(env, {"lst", "list_rec"}):is_nil()) env = add_aliases(env, "list", "l") -print(get_aliases(env, {"l", "list"}):head()) -print(get_aliases(env, {"l", "cons"}):head()) +print(get_alias_exprs(env, {"l", "list"}):head()) +print(get_alias_exprs(env, {"l", "cons"}):head()) local A = Local("A", mk_sort(1)) local R = Local("R", mk_arrow(A, A, Bool)) @@ -45,5 +45,5 @@ local a = Local("a", A) local b = Local("b", A) env = add_alias(env, "z", zero) -assert(get_aliases(env, "z"):head() == zero) -assert(get_aliases(env, "zz"):is_nil()) +assert(get_alias_exprs(env, "z"):head() == zero) +assert(get_alias_exprs(env, "zz"):is_nil()) diff --git a/tests/lua/alias2.lua b/tests/lua/alias2.lua new file mode 100644 index 000000000..442bdda41 --- /dev/null +++ b/tests/lua/alias2.lua @@ -0,0 +1,12 @@ +local env = environment() + +local env = environment() +local l = mk_param_univ("l") +local u = mk_global_univ("u") +env = add_alias(env, "m", max_univ(l, u)) +env = add_alias(env, "l1", max_univ(l, 1)) +assert(is_aliased(env, max_univ(l, u)) == name("m")) +assert(not is_aliased(env, max_univ(u, l))) +assert(get_alias_level(env, "m") == max_univ(l, u)) +assert(get_alias_level(env, "l1") == max_univ(l, 1)) +assert(not get_alias_level(env, "l2"))