feat(frontends/lean): add 'export' command

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

src/emacs/lean-syntax.el

@@ -11,7 +11,7 @@
   '("import" "abbreviation" "opaque_hint" "tactic_hint" "definition" "renaming"
     "inline" "hiding" "exposing" "parameter" "parameters" "begin" "proof" "qed" "conjecture"
     "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem"
-    "context" "open" "as" "axiom" "inductive" "with" "structure" "universe" "alias" "help" "environment"
+    "context" "open" "as" "export" "axiom" "inductive" "with" "structure" "universe" "alias" "help" "environment"
     "options" "precedence" "postfix" "prefix" "calc_trans" "calc_subst" "calc_refl"
     "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end"
     "private" "using" "namespace" "builtin" "including" "instance" "class" "section"

src/frontends/lean/builtin_cmds.cpp

@@ -13,6 +13,7 @@ Author: Leonardo de Moura
 #include "library/io_state_stream.h"
 #include "library/scoped_ext.h"
 #include "library/aliases.h"
+#include "library/protected.h"
 #include "library/locals.h"
 #include "library/coercion.h"
 #include "library/opaque_hints.h"
@@ -182,14 +183,30 @@ static void check_identifier(parser & p, environment const & env, name const & n
         throw parser_error(sstream() << "invalid 'open' command, unknown declaration '" << full_id << "'", p.pos());
 }
 
-// open [class] id (as id)? (id ...) (renaming id->id id->id) (hiding id ... id)
-environment open_cmd(parser & p) {
+// add id as an abbreviation for d
+static environment add_abbrev(environment const & env, name const & id, name const & d) {
+    declaration decl = env.get(d);
+    buffer<level> ls;
+    for (name const & l : decl.get_univ_params())
+        ls.push_back(mk_param_univ(l));
+    expr value  = mk_constant(d, to_list(ls.begin(), ls.end()));
+    bool opaque = false;
+    name const & ns = get_namespace(env);
+    name full_id    = ns + id;
+    environment new_env = module::add(env, check(env, mk_definition(env, full_id, decl.get_univ_params(), decl.get_type(), value, opaque)));
+    if (full_id != id)
+        new_env = add_expr_alias_rec(new_env, id, full_id);
+    return new_env;
+}
+
+// open/export [class] id (as id)? (id ...) (renaming id->id id->id) (hiding id ... id)
+environment open_export_cmd(parser & p, bool open) {
     environment env = p.env();
     while (true) {
         name cls = parse_class(p);
         bool decls = cls.is_anonymous() || cls == g_decls || cls == g_declarations;
         auto pos   = p.pos();
-        name ns    = p.check_id_next("invalid 'open' command, identifier expected");
+        name ns    = p.check_id_next("invalid 'open/export' command, identifier expected");
         optional<name> real_ns = to_valid_namespace_name(env, ns);
         if (!real_ns)
             throw parser_error(sstream() << "invalid namespace name '" << ns << "'", pos);
@@ -197,9 +214,12 @@ environment open_cmd(parser & p) {
         name as;
         if (p.curr_is_token_or_id(g_as)) {
             p.next();
-            as = p.check_id_next("invalid 'open' command, identifier expected");
+            as = p.check_id_next("invalid 'open/export' command, identifier expected");
         }
+        if (open)
             env = using_namespace(env, p.ios(), ns, cls);
+        else
+            env = export_namespace(env, p.ios(), ns, cls);
         if (decls) {
             // Remark: we currently to not allow renaming and hiding of universe levels
             buffer<name> exceptions;
@@ -211,11 +231,14 @@ environment open_cmd(parser & p) {
                     while (p.curr_is_identifier()) {
                         name from_id = p.get_name_val();
                         p.next();
-                        p.check_token_next(g_arrow, "invalid 'open' command renaming, '->' expected");
-                        name to_id = p.check_id_next("invalid 'open' command renaming, identifier expected");
+                        p.check_token_next(g_arrow, "invalid 'open/export' command renaming, '->' expected");
+                        name to_id = p.check_id_next("invalid 'open/export' command renaming, identifier expected");
                         check_identifier(p, env, ns, from_id);
                         exceptions.push_back(from_id);
+                        if (open)
                             env = add_expr_alias(env, as+to_id, ns+from_id);
+                        else
+                            env = add_abbrev(env, as+to_id, ns+from_id);
                     }
                 } else if (p.curr_is_token_or_id(g_hiding)) {
                     p.next();
@@ -231,23 +254,43 @@ environment open_cmd(parser & p) {
                         name id = p.get_name_val();
                         p.next();
                         check_identifier(p, env, ns, id);
+                        if (open)
                             env = add_expr_alias(env, as+id, ns+id);
+                        else
+                            env = add_abbrev(env, as+id, ns+id);
                     }
                 } else {
-                    throw parser_error("invalid 'open' command option, identifier, 'hiding' or 'renaming' expected", p.pos());
+                    throw parser_error("invalid 'open/export' command option, identifier, 'hiding' or 'renaming' expected", p.pos());
                 }
                 if (found_explicit && !exceptions.empty())
-                    throw parser_error("invalid 'open' command option, mixing explicit and implicit 'open' options", p.pos());
-                p.check_token_next(g_rparen, "invalid 'open' command option, ')' expected");
+                    throw parser_error("invalid 'open/export' command option, mixing explicit and implicit 'open/export' options", p.pos());
+                p.check_token_next(g_rparen, "invalid 'open/export' command option, ')' expected");
             }
-            if (!found_explicit)
+            if (!found_explicit) {
+                if (open) {
                     env = add_aliases(env, ns, as, exceptions.size(), exceptions.data());
+                } else {
+                    environment new_env = env;
+                    env.for_each_declaration([&](declaration const & d) {
+                            if (!is_protected(env, d.get_name()) &&
+                                is_prefix_of(ns, d.get_name()) &&
+                                !is_exception(d.get_name(), ns, exceptions.size(), exceptions.data())) {
+                                name new_id = d.get_name().replace_prefix(ns, as);
+                                if (!new_id.is_anonymous())
+                                    new_env = add_abbrev(new_env, new_id, d.get_name());
+                            }
+                        });
+                    env = new_env;
+                }
+            }
         }
         if (!p.curr_is_token(g_lbracket) && !p.curr_is_identifier())
             break;
     }
     return env;
 }
+environment open_cmd(parser & p) { return open_export_cmd(p, true); }
+environment export_cmd(parser & p) { return open_export_cmd(p, false); }
 
 environment coercion_cmd(parser & p) {
     auto pos = p.pos();
@@ -310,6 +353,7 @@ environment erase_cache_cmd(parser & p) {
 cmd_table init_cmd_table() {
     cmd_table r;
     add_cmd(r, cmd_info("open",         "create aliases for declarations, and use objects defined in other namespaces", open_cmd));
+    add_cmd(r, cmd_info("export",       "create abbreviations for declarations, and export objects defined in other namespaces", export_cmd));
     add_cmd(r, cmd_info("set_option",   "set configuration option", set_option_cmd));
     add_cmd(r, cmd_info("exit",         "exit", exit_cmd));
     add_cmd(r, cmd_info("print",        "print a string", print_cmd));

src/frontends/lean/token_table.cpp

@@ -78,7 +78,7 @@ token_table init_token_table() {
                                "abbreviation", "opaque_hint", "evaluate", "check", "print", "end", "namespace", "section", "import",
                                "abbreviation", "inductive", "record", "renaming", "extends", "structure", "module", "universe",
                                "precedence", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context",
-                               "exit", "set_option", "open", "calc_subst", "calc_refl", "calc_trans", "tactic_hint",
+                               "exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "tactic_hint",
                                "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class", "#erase_cache", nullptr};
 
     pair<char const *, char const *> aliases[] =

src/library/aliases.cpp

@@ -98,6 +98,11 @@ struct aliases_ext : public environment_extension {
         return env;
     }
 
+    static environment export_namespace(environment const & env, io_state const &, name const &) {
+        // do nothing, aliases are treated in a special way in the frontend.
+        return env;
+    }
+
     static environment push_scope(environment const & env, scope_kind k) {
         aliases_ext ext = get_extension(env);
         ext.push(k != scope_kind::Namespace);
@@ -119,7 +124,9 @@ static name g_aliases("aliases");
 struct aliases_ext_reg {
     unsigned m_ext_id;
     aliases_ext_reg() {
-        register_scoped_ext(g_aliases, aliases_ext::using_namespace, aliases_ext::push_scope, aliases_ext::pop_scope);
+        register_scoped_ext(g_aliases,
+                            aliases_ext::using_namespace, aliases_ext::export_namespace,
+                            aliases_ext::push_scope, aliases_ext::pop_scope);
         m_ext_id = environment::register_extension(std::make_shared<aliases_ext>());
     }
 };
@@ -175,7 +182,7 @@ optional<name> get_level_alias(environment const & env, name const & n) {
 }
 
 // Return true iff \c n is (prefix + ex) for some ex in exceptions
-static bool is_exception(name const & n, name const & prefix, unsigned num_exceptions, name const * exceptions) {
+bool is_exception(name const & n, name const & prefix, unsigned num_exceptions, name const * exceptions) {
     return std::any_of(exceptions, exceptions + num_exceptions, [&](name const & ex) { return (prefix + ex) == n; });
 }
 

src/library/aliases.h

@@ -50,6 +50,8 @@ optional<name> get_level_alias(environment const & env, name const & n);
 environment add_aliases(environment const & env, name const & prefix, name const & new_prefix,
                         unsigned num_exceptions = 0, name const * exceptions = nullptr);
 
+bool is_exception(name const & n, name const & prefix, unsigned num_exceptions, name const * exceptions);
+
 void for_each_expr_alias(environment const & env, std::function<void(name const &, list<name> const &)> const & fn);
 
 void open_aliases(lua_State * L);

src/library/scoped_ext.cpp

@@ -12,7 +12,7 @@ Author: Leonardo de Moura
 #include "library/kernel_bindings.h"
 
 namespace lean {
-typedef std::tuple<name, using_namespace_fn, push_scope_fn, pop_scope_fn> entry;
+typedef std::tuple<name, using_namespace_fn, export_namespace_fn, push_scope_fn, pop_scope_fn> entry;
 typedef std::vector<entry> scoped_exts;
 
 static scoped_exts & get_exts() {
@@ -22,8 +22,8 @@ static scoped_exts & get_exts() {
     return *exts;
 }
 
-void register_scoped_ext(name const & c, using_namespace_fn use, push_scope_fn push, pop_scope_fn pop) {
-    get_exts().emplace_back(c, use, push, pop);
+void register_scoped_ext(name const & c, using_namespace_fn use, export_namespace_fn ex, push_scope_fn push, pop_scope_fn pop) {
+    get_exts().emplace_back(c, use, ex, push, pop);
 }
 
 struct scope_mng_ext : public environment_extension {
@@ -74,6 +74,15 @@ environment using_namespace(environment const & env, io_state const & ios, name
     return r;
 }
 
+environment export_namespace(environment const & env, io_state const & ios, name const & n, name const & c) {
+    environment r = env;
+    for (auto const & t : get_exts()) {
+        if (c.is_anonymous() || c == std::get<0>(t))
+            r = std::get<2>(t)(r, ios, n);
+    }
+    return r;
+}
+
 optional<name> to_valid_namespace_name(environment const & env, name const & n) {
     scope_mng_ext const & ext = get_extension(env);
     if (ext.m_namespace_set.contains(n))
@@ -102,7 +111,7 @@ environment push_scope(environment const & env, io_state const & ios, scope_kind
     ext.m_scope_kinds = cons(k, ext.m_scope_kinds);
     environment r = update(env, ext);
     for (auto const & t : get_exts()) {
-        r = std::get<2>(t)(r, k);
+        r = std::get<3>(t)(r, k);
     }
     if (k == scope_kind::Namespace)
         r = using_namespace(r, ios, n);
@@ -136,7 +145,7 @@ environment pop_scope(environment const & env, name const & n) {
     ext.m_scope_kinds = tail(ext.m_scope_kinds);
     environment r = update(env, ext);
     for (auto const & t : get_exts()) {
-        r = std::get<3>(t)(r, k);
+        r = std::get<4>(t)(r, k);
     }
     return r;
 }

src/library/scoped_ext.h

@@ -17,12 +17,17 @@ Author: Leonardo de Moura
 namespace lean {
 enum class scope_kind { Namespace, Section, Context };
 typedef environment (*using_namespace_fn)(environment const &, io_state const &, name const &);
+typedef environment (*export_namespace_fn)(environment const &, io_state const &, name const &);
 typedef environment (*push_scope_fn)(environment const &, scope_kind);
 typedef environment (*pop_scope_fn)(environment const &, scope_kind);
 
-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. */
+void register_scoped_ext(name const & n, using_namespace_fn use, export_namespace_fn ex, 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 objects from "class" \c c are considered. */
 environment using_namespace(environment const & env, io_state const & ios, name const & n, name const & c = name());
+/** \brief Export objects defined in the namespace \c n to current namespace.
+    If \c c is not the anonymous name, then only objects from "class" \c c are considered. */
+environment export_namespace(environment const & env, io_state const & ios, name const & n, name const & c = name());
+
 /** \brief Create a new scope, all scoped extensions are notified. */
 environment push_scope(environment const & env, io_state const & ios, scope_kind k, name const & n = name());
 /** \brief Delete the most recent scope, all scoped extensions are notified. */
@@ -119,6 +124,19 @@ public:
         return r;
     }
 
+    environment export_namespace(environment env, io_state const & ios, name const & n) const {
+        if (auto it = m_entries.find(n)) {
+            buffer<entry> entries;
+            to_buffer(*it, entries);
+            unsigned i = entries.size();
+            while (i > 0) {
+                --i;
+                env = add_entry(env, ios, entries[i]);
+            }
+        }
+        return env;
+    }
+
     scoped_ext push() const {
         scoped_ext r(*this);
         r.m_scopes     = cons(m_state, r.m_scopes);
@@ -136,7 +154,7 @@ public:
     struct reg {
         unsigned m_ext_id;
         reg() {
-            register_scoped_ext(get_class_name(), using_namespace_fn, push_fn, pop_fn);
+            register_scoped_ext(get_class_name(), using_namespace_fn, export_namespace_fn, push_fn, pop_fn);
             register_module_object_reader(get_serialization_key(), reader);
             m_ext_id = environment::register_extension(std::make_shared<scoped_ext>());
         }
@@ -152,6 +170,9 @@ 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 export_namespace_fn(environment const & env, io_state const & ios, name const & n) {
+        return get(env).export_namespace(env, ios, n);
+    }
     static environment push_fn(environment const & env, scope_kind k) {
         if (k != scope_kind::Section || TransientSection)
             return update(env, get(env).push());

tests/lean/run/export.lean

@@ -0,0 +1,18 @@
+import data.nat
+
+variables a b : nat.nat
+
+namespace boo
+  export nat
+  check a + b
+  check nat.add
+  check boo.add
+  check add
+end boo
+
+check boo.nat_rec
+
+open boo
+check a + b
+check boo.nat_rec
+check nat_rec

tests/lean/t14.lean.expected.out

@@ -4,7 +4,7 @@ t14.lean:12:8: error: unknown identifier 'c'
 a : foo.A
 x : foo.A
 t14.lean:19:8: error: unknown identifier 'c'
-t14.lean:23:26: error: invalid 'open' command option, mixing explicit and implicit 'open' options
+t14.lean:23:26: error: invalid 'open/export' command option, mixing explicit and implicit 'open/export' options
 a : A
 c : A
 A : Type