feat(library/aliases): add level aliases

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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<expr> new_as;
         for (auto const & e : as)

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 <tt>F</tt> to each level expressions. */
 class for_each_level_fn {

src/library/aliases.cpp

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include <utility>
 #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, list<expr>, name_quick_cmp> m_aliases;
+    rb_map<name, list<expr>, name_quick_cmp>  m_aliases;
-    rb_map<expr, name,       expr_quick_cmp> m_inv_aliases;
+    rb_map<expr, name,       expr_quick_cmp>  m_inv_aliases;
+    rb_map<name, level,      name_quick_cmp>  m_level_aliases;
+    rb_map<level, name,      level_quick_cmp> 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<expr>(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<name> is_aliased(environment const & env, expr const & t) {
     return it ? optional<name>(*it) : optional<name>();
 }
 
-list<expr> get_aliases(environment const & env, name const & n) {
+list<expr> get_alias_exprs(environment const & env, name const & n) {
     auto it = get_extension(env).m_aliases.find(n);
     return it ? *it : list<expr>();
 }
 
+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<name> is_aliased(environment const & env, level const & l) {
+    auto it = get_extension(env).m_inv_level_aliases.find(l);
+    return it ? optional<name>(*it) : optional<name>();
+}
+
+optional<level> 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<level>();
+}
+
 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) {
+static int get_alias_exprs(lua_State * L) {
-    return push_list_expr(L, get_aliases(to_environment(L, 1), to_name_ext(L, 2)));
+    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_alias,       "add_alias");
-    SET_GLOBAL_FUN(add_aliases, "add_aliases");
+    SET_GLOBAL_FUN(add_aliases,     "add_aliases");
-    SET_GLOBAL_FUN(is_aliased,  "is_aliased");
+    SET_GLOBAL_FUN(is_aliased,      "is_aliased");
-    SET_GLOBAL_FUN(get_aliases, "get_aliases");
+    SET_GLOBAL_FUN(get_alias_exprs, "get_alias_exprs");
+    SET_GLOBAL_FUN(get_alias_level, "get_alias_level");
 }
 }

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. */
-    \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.
-*/
 environment add_alias(environment const & env, name const & a, expr const & e);
 /**
    \brief Create an alias for each declaration named <tt>prefix.rest</tt>.
@@ -29,7 +25,20 @@ environment add_aliases(environment const & env, name const & prefix, name const
 optional<name> is_aliased(environment const & env, expr const & t);
 
 /** \brief Return expressions associated with the given alias. */
-list<expr> get_aliases(environment const & env, name const & n);
+list<expr> 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<name> is_aliased(environment const & env, level const & l);
+
+/** \brief Return the level associated with the given alias. */
+optional<level> get_alias_level(environment const & env, name const & n);
 
 void open_aliases(lua_State * L);
 }

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<level> const & e);
 int push_optional_expr(lua_State * L, optional<expr> const & e);
 int push_optional_justification(lua_State * L, optional<justification> const & j);
 int push_optional_declaration(lua_State * L, optional<declaration> const & e);

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_alias_exprs(env, {"natural", "zero"}):head() == zero)
-assert(get_aliases(env, {"natural", "nat"}):head() == nat)
+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())
+print(get_alias_exprs(env, "list_rec"):head())
-assert(not get_aliases(env, "list_rec"):is_nil())
+assert(not get_alias_exprs(env, "list_rec"):is_nil())
-assert(not get_aliases(env, {"lst", "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_alias_exprs(env, {"l", "list"}):head())
-print(get_aliases(env, {"l", "cons"}):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_alias_exprs(env, "z"):head() == zero)
-assert(get_aliases(env, "zz"):is_nil())
+assert(get_alias_exprs(env, "zz"):is_nil())

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"))