feat(library): add module for implementing aliases and 'using' command

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

src/kernel/abstract.h

@@ -46,7 +46,9 @@ expr Fun(std::initializer_list<std::pair<expr const &, expr const &>> const & l,
 /** \brief Create a lambda-expression by abstracting the given local constants over b */
 expr Fun(unsigned num, expr const * locals, expr const & b);
 template<typename T> expr Fun(T const & locals, expr const & b) { return Fun(locals.size(), locals.data(), b); }
-inline expr Fun(expr const & local, expr const & b) { return Fun(1, &local, b); }
+inline expr Fun(expr const & local, expr const & b, binder_info const & bi = binder_info()) {
+    return Fun(local_pp_name(local), mlocal_type(local), abstract(b, local), bi);
+}
 
 /**
    \brief Create a Pi expression (pi (x : t) b), the term b is abstracted using abstract(b, constant(x)).

src/library/CMakeLists.txt

@@ -2,7 +2,7 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
   kernel_bindings.cpp io_state_stream.cpp bin_app.cpp
   resolve_macro.cpp kernel_serializer.cpp max_sharing.cpp
   normalize.cpp shared_environment.cpp module.cpp coercion.cpp
-  private.cpp placeholder.cpp)
+  private.cpp placeholder.cpp aliases.cpp)
 # fo_unify.cpp hop_match.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})

src/library/aliases.cpp

@@ -0,0 +1,186 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <utility>
+#include "util/rb_map.h"
+#include "util/name_generator.h"
+#include "kernel/abstract.h"
+#include "kernel/instantiate.h"
+#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<expr, name, expr_quick_cmp> m_inv_aliases;
+};
+
+struct aliases_ext_reg {
+    unsigned m_ext_id;
+    aliases_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<aliases_ext>()); }
+};
+static aliases_ext_reg g_ext;
+static aliases_ext const & get_extension(environment const & env) {
+    return static_cast<aliases_ext const &>(env.get_extension(g_ext.m_ext_id));
+}
+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);
+    aliases_ext ext = get_extension(env);
+    ext.m_aliases.insert(a, e);
+    ext.m_inv_aliases.insert(e, a);
+    return update(env, ext);
+}
+
+environment add_aliases(environment const & env, name const & prefix, optional<name> const & new_prefix, io_state const & ios) {
+    return add_aliases(env, prefix, new_prefix, 0, nullptr, ios);
+}
+
+static name replace_prefix(name const & n, name const & prefix, optional<name> const & new_prefix) {
+    if (n == prefix)
+        return new_prefix ? *new_prefix : name();
+    name p = replace_prefix(n.get_prefix(), prefix, new_prefix);
+    if (n.is_string())
+        return name(p, n.get_string());
+    else
+        return name(p, n.get_numeral());
+}
+
+static optional<expr> get_fix_param(unsigned num_fix_params, std::pair<name, expr> const * fix_params, name const & n) {
+    for (unsigned i = 0; i < num_fix_params; i++) {
+        if (fix_params[i].first == n)
+            return some_expr(fix_params[i].second);
+    }
+    return none_expr();
+}
+
+static name g_local_name = name::mk_internal_unique_name();
+
+environment add_aliases(environment const & env, name const & prefix, optional<name> const & new_prefix,
+                        unsigned num_fix_params, std::pair<name, expr> const * fix_params, io_state const & ios) {
+    aliases_ext ext = get_extension(env);
+    env.for_each([&](declaration const & d) {
+            if (is_prefix_of(prefix, d.get_name())) {
+                name a        = replace_prefix(d.get_name(), prefix, new_prefix);
+                check_name(env, a, ios);
+                levels ls     = map2<level>(d.get_params(), [](name const &) { return mk_level_placeholder(); });
+                expr c        = mk_constant(d.get_name(), ls);
+                if (num_fix_params > 0) {
+                    expr t = d.get_type();
+                    buffer<expr>        locals;
+                    buffer<binder_info> infos;
+                    buffer<expr>        args;
+                    name_generator      ngen(g_local_name);
+                    bool found_free = false;
+                    bool found_fix  = false;
+                    bool easy       = true;
+                    while (is_pi(t)) {
+                        if (auto p = get_fix_param(num_fix_params, fix_params, binding_name(t))) {
+                            args.push_back(*p);
+                            if (found_free)
+                                easy = false;
+                            found_fix = true;
+                            t = instantiate(binding_body(t), *p);
+                        } else {
+                            found_free = true;
+                            expr l = mk_local(ngen.next(), binding_name(t), binding_domain(t));
+                            infos.push_back(binding_info(t));
+                            locals.push_back(l);
+                            args.push_back(l);
+                            t = instantiate(binding_body(t), l);
+                        }
+                    }
+                    if (found_fix) {
+                        if (easy) {
+                            args.shrink(args.size() - locals.size());
+                            c = mk_app(c, args);
+                        } else {
+                            c = mk_app(c, args);
+                            unsigned i = locals.size();
+                            while (i > 0) {
+                                --i;
+                                c = Fun(locals[i], c, infos[i]);
+                            }
+                        }
+                    }
+                }
+                ext.m_aliases.insert(a, c);
+                ext.m_inv_aliases.insert(c, a);
+            }
+        });
+    return update(env, ext);
+}
+
+optional<name> is_aliased(environment const & env, expr const & t) {
+    auto it = get_extension(env).m_inv_aliases.find(t);
+    return it ? optional<name>(*it) : optional<name>();
+}
+
+optional<expr> get_alias(environment const & env, name const & n) {
+    auto it = get_extension(env).m_aliases.find(n);
+    return it ? optional<expr>(*it) : optional<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)));
+}
+
+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), optional<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_optional_name(L, 3), get_io_state(L)));
+    } else if (nargs == 4 && is_io_state(L, 4)) {
+        return push_environment(L, add_aliases(to_environment(L, 1), to_name_ext(L, 2), to_optional_name(L, 3), to_io_state(L, 4)));
+    } else {
+        buffer<std::pair<name, expr>> fix_params;
+        luaL_checktype(L, 4, LUA_TTABLE);
+        int sz = objlen(L, 4);
+        for (int i = 1; i <= sz; i++) {
+            lua_rawgeti(L, 4, i);
+            luaL_checktype(L, -1, LUA_TTABLE);
+            lua_rawgeti(L, -1, 1);
+            name n = to_name_ext(L, -1);
+            lua_pop(L, 1);
+            lua_rawgeti(L, -1, 2);
+            expr e = to_expr(L, -1);
+            lua_pop(L, 2);
+            fix_params.emplace_back(n, e);
+        }
+        return push_environment(L, add_aliases(to_environment(L, 1), to_name_ext(L, 2), to_optional_name(L, 3),
+                                               fix_params.size(), fix_params.data(), to_io_state_ext(L, 5)));
+    }
+}
+
+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)));
+}
+
+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");
+}
+}

src/library/aliases.h

@@ -0,0 +1,42 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include <utility>
+#include "util/lua.h"
+#include "kernel/environment.h"
+#include "library/io_state.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.
+*/
+environment add_alias(environment const & env, name const & a, expr const & e, io_state const & ios);
+/**
+   \brief Create an alias for each declaration named <tt>prefix.rest</tt>. If \c new_prefix is not none,
+   then the alias for <tt>prefix.rest</tt> is <tt>new_prefix.rest</tt>. Otherwise, it is just \c rest.
+   Warning messages are generated if the new aliases shadow existing aliases and/or declarations.
+*/
+environment add_aliases(environment const & env, name const & prefix, optional<name> const & new_prefix, io_state const & ios);
+/**
+   \brief Create an alias for each declaration named <tt>prefix.rest</tt>, the alias will also fix the value of parameters
+   in \c fix_params. The argument \c fix_params is a sequence of pairs <tt>(name, expr)</tt>, where the \c name is the
+   name of the parameter to be fixed.
+   Warning messages are generated if the new aliases shadow existing aliases and/or declarations.
+*/
+environment add_aliases(environment const & env, name const & prefix, optional<name> const & new_prefix,
+                        unsigned num_fix_params, std::pair<name, expr> const * fix_params, io_state const & ios);
+
+/** \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);
+
+void open_aliases(lua_State * L);
+}

src/library/register_module.h

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "library/coercion.h"
 #include "library/private.h"
 #include "library/placeholder.h"
+#include "library/aliases.h"
 // #include "library/fo_unify.h"
 // #include "library/hop_match.h"
 
@@ -21,6 +22,7 @@ inline void open_core_module(lua_State * L) {
     open_coercion(L);
     open_private(L);
     open_placeholder(L);
+    open_aliases(L);
     // open_fo_unify(L);
     // open_hop_match(L);
 }

tests/lua/alias1.lua

@@ -0,0 +1,61 @@
+local env = environment()
+
+local env      = environment()
+local l        = mk_param_univ("l")
+local A        = Const("A")
+local U_l      = mk_sort(l)
+local U_l1     = mk_sort(max_univ(l, 1)) -- Make sure U_l1 is not Bool/Prop
+local nat      = Const({"nat", "nat"})
+local vec_l    = Const({"vec", "vec"}, {l})  -- vec.{l}
+local zero     = Const({"nat", "zero"})
+local succ     = Const({"nat", "succ"})
+local one      = succ(zero)
+local list_l   = Const({"list", "list"}, {l}) -- list.{l}
+
+env = add_inductive(env,
+                    name("nat", "nat"), Type,
+                    name("nat", "zero"), nat,
+                    name("nat", "succ"), mk_arrow(nat, nat))
+
+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(is_aliased(env, nat) == name("natural", "nat"))
+
+env = add_inductive(env,
+                    name("list", "list"), {l}, 1, Pi(A, U_l, U_l1),
+                    name("list", "nil"),  Pi({{A, U_l, true}}, list_l(A)),
+                    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"}))
+env = add_aliases(env, "list")
+print(get_alias(env, "list_rec"))
+assert(get_alias(env, "list_rec"))
+assert(get_alias(env, {"lst", "list_rec"}))
+
+env = add_aliases(env, "list", "lnat", {{"A", nat}})
+print(get_alias(env, {"lnat", "list"}))
+print(get_alias(env, {"lnat", "cons"}))
+assert(get_alias(env, {"lnat", "cons"}) == Const({"list", "cons"}, { mk_level_placeholder() })(nat))
+
+local A = Local("A", mk_sort(1))
+local R = Local("R", mk_arrow(A, A, Bool))
+local a = Local("a", A)
+local b = Local("b", A)
+
+env = add_decl(env, mk_var_decl({"foo", "pred"}, Pi({A, R, a, b}, Bool)))
+env = add_aliases(env, "foo", nil, {{"A", nat}, {"a", zero}})
+local Rn = Local("R", mk_arrow(nat, nat, Bool))
+local bn = Local("b", nat)
+local a1 = get_alias(env, "pred")
+local a2 = Fun({Rn, bn}, Const({"foo", "pred"})(nat, Rn, zero, bn))
+print(a1)
+print(a2)
+assert(a1 == a2)
+env = add_aliases(env, "foo", nil, {{"A", nat}, {"a", zero}, {"b", one}})
+print(get_alias(env, "pred"))
+env = add_alias(env, "z", zero)
+assert(get_alias(env, "z") == zero)
+assert(not get_alias(env, "zz"))