From f9a90b992064cb145eeefa178eaf88921db1ecd7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 3 Sep 2014 18:37:01 -0700 Subject: [PATCH] feat(frontends/lean): add 'export' command Signed-off-by: Leonardo de Moura --- src/emacs/lean-syntax.el | 2 +- src/frontends/lean/builtin_cmds.cpp | 72 +++++++++++++++++++++++------ src/frontends/lean/token_table.cpp | 2 +- src/library/aliases.cpp | 11 ++++- src/library/aliases.h | 2 + src/library/scoped_ext.cpp | 19 ++++++-- src/library/scoped_ext.h | 27 +++++++++-- tests/lean/run/export.lean | 18 ++++++++ tests/lean/t14.lean.expected.out | 2 +- 9 files changed, 128 insertions(+), 27 deletions(-) create mode 100644 tests/lean/run/export.lean diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 5066af1e2..c150341c0 100644 --- a/src/emacs/lean-syntax.el +++ b/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" diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index b0a68e082..3d99405cf 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/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 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 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"); } - env = using_namespace(env, p.ios(), ns, cls); + 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 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); - env = add_expr_alias(env, as+to_id, ns+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); - env = add_expr_alias(env, as+id, 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 (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 (!found_explicit) - env = add_aliases(env, ns, as, exceptions.size(), exceptions.data()); } 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)); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 858a53555..f17f8fd0c 100644 --- a/src/frontends/lean/token_table.cpp +++ b/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 aliases[] = diff --git a/src/library/aliases.cpp b/src/library/aliases.cpp index 91e2939a7..fab56e2b8 100644 --- a/src/library/aliases.cpp +++ b/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()); } }; @@ -175,7 +182,7 @@ optional 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; }); } diff --git a/src/library/aliases.h b/src/library/aliases.h index 1d310f6c3..0daf3371d 100644 --- a/src/library/aliases.h +++ b/src/library/aliases.h @@ -50,6 +50,8 @@ optional 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 const &)> const & fn); void open_aliases(lua_State * L); diff --git a/src/library/scoped_ext.cpp b/src/library/scoped_ext.cpp index e7574f4a2..30a532c28 100644 --- a/src/library/scoped_ext.cpp +++ b/src/library/scoped_ext.cpp @@ -12,7 +12,7 @@ Author: Leonardo de Moura #include "library/kernel_bindings.h" namespace lean { -typedef std::tuple entry; +typedef std::tuple entry; typedef std::vector 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 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; } diff --git a/src/library/scoped_ext.h b/src/library/scoped_ext.h index e4bb41272..265500572 100644 --- a/src/library/scoped_ext.h +++ b/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 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()); } @@ -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()); diff --git a/tests/lean/run/export.lean b/tests/lean/run/export.lean new file mode 100644 index 000000000..ec1516267 --- /dev/null +++ b/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 diff --git a/tests/lean/t14.lean.expected.out b/tests/lean/t14.lean.expected.out index 5178e571e..7d7753c38 100644 --- a/tests/lean/t14.lean.expected.out +++ b/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