feat(library/aliases): add support for alias overloading

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

src/library/aliases.cpp

@@ -12,13 +12,20 @@ Author: Leonardo de Moura
 #include "library/expr_lt.h"
 #include "library/kernel_bindings.h"
 #include "library/aliases.h"
-#include "library/io_state_stream.h"
 #include "library/placeholder.h"
 
 namespace lean {
 struct aliases_ext : public environment_extension {
-    rb_map<name, 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;
+    void add_alias(name const & a, expr const & e) {
+        auto it = m_aliases.find(a);
+        if (it)
+            m_aliases.insert(a, list<expr>(e, *it));
+        else
+            m_aliases.insert(a, list<expr>(e));
+        m_inv_aliases.insert(e, a);
+    }
 };
 
 struct aliases_ext_reg {
@@ -33,31 +40,20 @@ static environment update(environment const & env, aliases_ext const & ext) {
     return env.update(g_ext.m_ext_id, std::make_shared<aliases_ext>(ext));
 }
 
-static void check_name(environment const & env, name const & a, io_state const & ios) {
-    if (get_extension(env).m_aliases.contains(a))
-        diagnostic(env, ios) << "alias '" << a << "' shadows existing alias\n";
-    if (env.find(a))
-        diagnostic(env, ios) << "alias '" << a << "' shadows existing declaration\n";
-}
-
-environment add_alias(environment const & env, name const & a, expr const & e, io_state const & ios) {
-    check_name(env, a, ios);
+environment add_alias(environment const & env, name const & a, expr const & e) {
     aliases_ext ext = get_extension(env);
-    ext.m_aliases.insert(a, e);
-    ext.m_inv_aliases.insert(e, a);
+    ext.add_alias(a, e);
     return update(env, ext);
 }
 
-environment add_aliases(environment const & env, name const & prefix, name const & new_prefix, io_state const & ios) {
+environment add_aliases(environment const & env, name const & prefix, name const & new_prefix) {
     aliases_ext ext = get_extension(env);
     env.for_each([&](declaration const & d) {
             if (is_prefix_of(prefix, d.get_name())) {
                 name a        = d.get_name().replace_prefix(prefix, new_prefix);
-                check_name(env, a, ios);
                 levels ls     = map2<level>(d.get_univ_params(), [](name const &) { return mk_level_placeholder(); });
                 expr c        = mk_constant(d.get_name(), ls);
-                ext.m_aliases.insert(a, c);
-                ext.m_inv_aliases.insert(c, a);
+                ext.add_alias(a, c);
             }
         });
     return update(env, ext);
@@ -68,23 +64,21 @@ optional<name> is_aliased(environment const & env, expr const & t) {
     return it ? optional<name>(*it) : optional<name>();
 }
 
-optional<expr> get_alias(environment const & env, name const & n) {
+list<expr> get_aliases(environment const & env, name const & n) {
     auto it = get_extension(env).m_aliases.find(n);
-    return it ? optional<expr>(*it) : optional<expr>();
+    return it ? *it : list<expr>();
 }
 
 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), to_io_state_ext(L, 4)));
+    return push_environment(L, add_alias(to_environment(L, 1), to_name_ext(L, 2), to_expr(L, 3)));
 }
 
 static int add_aliases(lua_State * L) {
     int nargs = lua_gettop(L);
     if (nargs == 2) {
-        return push_environment(L, add_aliases(to_environment(L, 1), to_name_ext(L, 2), name(), get_io_state(L)));
-    } else if (nargs == 3) {
-        return push_environment(L, add_aliases(to_environment(L, 1), to_name_ext(L, 2), to_name_ext(L, 3), get_io_state(L)));
+        return push_environment(L, add_aliases(to_environment(L, 1), to_name_ext(L, 2), name()));
     } else {
-        return push_environment(L, add_aliases(to_environment(L, 1), to_name_ext(L, 2), to_name_ext(L, 3), to_io_state(L, 4)));
+        return push_environment(L, add_aliases(to_environment(L, 1), to_name_ext(L, 2), to_name_ext(L, 3)));
     }
 }
 
@@ -92,14 +86,14 @@ static int is_aliased(lua_State * L) {
     return push_optional_name(L, is_aliased(to_environment(L, 1), to_expr(L, 2)));
 }
 
-static int get_alias(lua_State * L) {
-    return push_optional_expr(L, get_alias(to_environment(L, 1), to_name_ext(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)));
 }
 
 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_alias,   "get_alias");
+    SET_GLOBAL_FUN(get_aliases, "get_aliases");
 }
 }

src/library/aliases.h

@@ -8,7 +8,6 @@ Author: Leonardo de Moura
 #include <utility>
 #include "util/lua.h"
 #include "kernel/environment.h"
-#include "library/io_state.h"
 
 namespace lean {
 /**
@@ -16,7 +15,7 @@ namespace lean {
     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, io_state const & ios);
+environment add_alias(environment const & env, name const & a, expr const & e);
 /**
    \brief Create an alias for each declaration named <tt>prefix.rest</tt>.
    The alias for <tt>prefix.rest</tt> is <tt>new_prefix.rest</tt>.
@@ -24,13 +23,13 @@ environment add_alias(environment const & env, name const & a, expr const & e, i
 
    \remark \c new_prefix may be the anonymous name.
 */
-environment add_aliases(environment const & env, name const & prefix, name const & new_prefix, io_state const & ios);
+environment add_aliases(environment const & env, name const & prefix, name const & new_prefix);
 
 /** \brief If \c t is aliased in \c env, then return its name. Otherwise, return none. */
 optional<name> is_aliased(environment const & env, expr const & t);
 
-/** \brief Return expression associated with the given alias. */
-optional<expr> get_alias(environment const & env, name const & n);
+/** \brief Return expressions associated with the given alias. */
+list<expr> get_aliases(environment const & env, name const & n);
 
 void open_aliases(lua_State * L);
 }

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