From c532dcfaac442f443bcef16253022064429c810b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 4 Sep 2014 09:30:25 -0700 Subject: [PATCH] feat(library/declaration_index): add 'a|abbreviation-name|declaration-name' entries in .ilean files --- src/frontends/lean/builtin_cmds.cpp | 9 +++++---- src/frontends/lean/parser.cpp | 5 +++++ src/frontends/lean/parser.h | 1 + src/library/declaration_index.cpp | 6 ++++++ src/library/declaration_index.h | 7 +++++-- 5 files changed, 22 insertions(+), 6 deletions(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 3d99405cf..3627171f0 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -184,7 +184,7 @@ static void check_identifier(parser & p, environment const & env, name const & n } // add id as an abbreviation for d -static environment add_abbrev(environment const & env, name const & id, name const & d) { +static environment add_abbrev(parser & p, environment const & env, name const & id, name const & d) { declaration decl = env.get(d); buffer ls; for (name const & l : decl.get_univ_params()) @@ -193,6 +193,7 @@ static environment add_abbrev(environment const & env, name const & id, name con bool opaque = false; name const & ns = get_namespace(env); name full_id = ns + id; + p.add_abbrev_index(full_id, d); 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); @@ -238,7 +239,7 @@ environment open_export_cmd(parser & p, bool open) { if (open) env = add_expr_alias(env, as+to_id, ns+from_id); else - env = add_abbrev(env, as+to_id, ns+from_id); + env = add_abbrev(p, env, as+to_id, ns+from_id); } } else if (p.curr_is_token_or_id(g_hiding)) { p.next(); @@ -257,7 +258,7 @@ environment open_export_cmd(parser & p, bool open) { if (open) env = add_expr_alias(env, as+id, ns+id); else - env = add_abbrev(env, as+id, ns+id); + env = add_abbrev(p, env, as+id, ns+id); } } else { throw parser_error("invalid 'open/export' command option, identifier, 'hiding' or 'renaming' expected", p.pos()); @@ -277,7 +278,7 @@ environment open_export_cmd(parser & p, bool open) { !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()); + new_env = add_abbrev(p, new_env, new_id, d.get_name()); } }); env = new_env; diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 3466e0371..329114d36 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -132,6 +132,11 @@ void parser::add_ref_index(name const & n, pos_info const & pos) { m_index->add_ref(get_stream_name(), pos, n); } +void parser::add_abbrev_index(name const & a, name const & d) { + if (m_index) + m_index->add_abbrev(a, d); +} + bool parser::are_info_lines_valid(unsigned start_line, unsigned end_line) const { if (!m_info_manager) return true; // we are not tracking info diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 45e484b19..30a124312 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -198,6 +198,7 @@ public: void set_index(declaration_index * i) { m_index = i; } void add_decl_index(name const & n, pos_info const & pos, name const & k, expr const & t); void add_ref_index(name const & n, pos_info const & pos); + void add_abbrev_index(name const & a, name const & d); environment const & env() const { return m_env; } io_state const & ios() const { return m_ios; } diff --git a/src/library/declaration_index.cpp b/src/library/declaration_index.cpp index 3d6452516..0b4e850e4 100644 --- a/src/library/declaration_index.cpp +++ b/src/library/declaration_index.cpp @@ -11,6 +11,9 @@ namespace lean { void declaration_index::add_decl(std::string const fname, pos_info const & p, name const & n, name const & k, expr const & t) { m_decls.insert(n, decl(fname, p, k, t)); } +void declaration_index::add_abbrev(name const & n, name const & d) { + m_abbrevs.emplace_back(n, d); +} void declaration_index::add_ref(std::string const fname, pos_info const & p, name const & n) { m_refs.emplace_back(fname, p, n); } @@ -24,6 +27,9 @@ void declaration_index::save(io_state_stream const & out) const { out.get_stream() << mk_pair(flatten(out.get_formatter()(t)), opts); out << endl; }); + for (auto const & a : m_abbrevs) { + out << "a" << "|" << a.first << "|" << a.second << endl; + } for (auto const & r : m_refs) { std::tie(fname, p, n) = r; out << "r" << "|" << fname << "|" << p.first << "|" << p.second << "|" << n << endl; diff --git a/src/library/declaration_index.h b/src/library/declaration_index.h index 0e7fed4bf..015d7bbdf 100644 --- a/src/library/declaration_index.h +++ b/src/library/declaration_index.h @@ -20,10 +20,13 @@ namespace lean { class declaration_index { typedef std::tuple decl; typedef std::tuple ref; - name_map m_decls; - std::vector m_refs; + typedef pair abbrev; + name_map m_decls; + std::vector m_abbrevs; + std::vector m_refs; public: void add_decl(std::string const fname, pos_info const & p, name const & n, name const & k, expr const & t); + void add_abbrev(name const & n, name const & d); void add_ref(std::string const fname, pos_info const & p, name const & n); void save(io_state_stream const & out) const; };