From b13851ba13c9e2065175963fa7505a5731186bc4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 23 Aug 2014 12:39:59 -0700 Subject: [PATCH] feat(frontends/lean): add kind and type to index, closes #89 Signed-off-by: Leonardo de Moura --- src/frontends/lean/decl_cmds.cpp | 17 ++++++++++++----- src/frontends/lean/inductive_cmd.cpp | 25 ++++++++++++++++++++++--- src/frontends/lean/parser.cpp | 5 +++-- src/frontends/lean/parser.h | 6 +++++- src/library/declaration_index.cpp | 20 +++++++++++++------- src/library/declaration_index.h | 8 +++++--- src/shell/lean.cpp | 5 +++-- 7 files changed, 63 insertions(+), 23 deletions(-) diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 9e24f7dd2..a1449edb6 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -71,6 +71,9 @@ void update_univ_parameters(buffer & ls_buffer, name_set const & found, pa }); } +static name g_axiom("axiom"); +static name g_variable("variable"); + static environment declare_var(parser & p, environment env, name const & n, level_param_names const & ls, expr const & type, bool is_axiom, optional const & _bi, pos_info const & pos) { @@ -82,11 +85,13 @@ static environment declare_var(parser & p, environment env, } else { name const & ns = get_namespace(env); name full_n = ns + n; - p.add_decl_index(full_n, pos); - if (is_axiom) + if (is_axiom) { env = module::add(env, check(env, mk_axiom(full_n, ls, type))); - else + p.add_decl_index(full_n, pos, g_axiom, type); + } else { env = module::add(env, check(env, mk_var_decl(full_n, ls, type))); + p.add_decl_index(full_n, pos, g_variable, type); + } if (!ns.is_anonymous()) env = add_expr_alias(env, n, full_n); return env; @@ -269,8 +274,6 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) { real_n = ns + n; } - p.add_decl_index(real_n, n_pos); - if (in_section(env)) { buffer section_ps; collect_section_locals(type, value, p, section_ps); @@ -297,6 +300,8 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) { cd = check(env, mk_theorem(real_n, c_ls, c_type, c_value)); else cd = check(env, mk_definition(env, real_n, c_ls, c_type, c_value, modifiers.m_is_opaque)); + if (!modifiers.m_is_private) + p.add_decl_index(real_n, n_pos, p.get_cmd_token(), c_type); env = module::add(env, *cd); found_cached = true; } catch (exception&) {} @@ -322,6 +327,8 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) { env = module::add(env, check(env, mk_definition(env, real_n, new_ls, type, value, modifiers.m_is_opaque))); p.cache_definition(real_n, pre_type, pre_value, new_ls, type, value); } + if (!modifiers.m_is_private) + p.add_decl_index(real_n, n_pos, p.get_cmd_token(), type); } if (real_n != n) diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp index 285c736e2..2752d490a 100644 --- a/src/frontends/lean/inductive_cmd.cpp +++ b/src/frontends/lean/inductive_cmd.cpp @@ -53,6 +53,10 @@ intro_rule update_intro_rule(intro_rule const & r, expr const & t) { static name g_tmp_prefix = name::mk_internal_unique_name(); +static name g_inductive("inductive"); +static name g_intro("intro"); +static name g_recursor("recursor"); + struct inductive_cmd_fn { typedef std::unique_ptr type_checker_ptr; parser & m_p; @@ -68,6 +72,8 @@ struct inductive_cmd_fn { level m_u; // temporary auxiliary global universe used for inferring the result universe of an inductive datatype declaration. bool m_infer_result_universe; name_set m_relaxed_implicit_infer; // set of introduction rules where we do not use strict implicit parameter infererence + typedef std::tuple decl_info; + buffer m_decl_info; // auxiliary buffer used to populate declaration_index inductive_cmd_fn(parser & p):m_p(p) { m_env = p.env(); @@ -97,9 +103,12 @@ struct inductive_cmd_fn { name id = m_p.check_id_next("invalid declaration, identifier expected"); check_atomic(id); name full_id = m_namespace + id; - m_p.add_decl_index(full_id, m_pos); - if (!is_intro) - m_p.add_decl_index(mk_rec_name(full_id), m_pos); + if (is_intro) { + m_decl_info.emplace_back(full_id, g_intro, m_pos); + } else { + m_decl_info.emplace_back(full_id, g_inductive, m_pos); + m_decl_info.emplace_back(mk_rec_name(full_id), g_recursor, m_pos); + } return full_id; } @@ -547,6 +556,15 @@ struct inductive_cmd_fn { out << "\n"; } + void update_declaration_index(environment const & env) { + name n, k; pos_info p; + for (auto const & info : m_decl_info) { + std::tie(n, k, p) = info; + expr type = env.get(n).get_type(); + m_p.add_decl_index(n, p, k, type); + } + } + environment operator()() { parser::no_undef_id_error_scope err_scope(m_p); buffer decls; @@ -566,6 +584,7 @@ struct inductive_cmd_fn { } level_param_names ls = to_list(m_levels.begin(), m_levels.end()); environment env = module::add_inductive(m_p.env(), ls, m_num_params, to_list(decls.begin(), decls.end())); + update_declaration_index(env); return add_aliases(env, ls, section_params, decls); } }; diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 1973331cf..c6c4617c6 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -121,9 +121,9 @@ optional> parser::find_cached_definiti return optional>(); } -void parser::add_decl_index(name const & n, pos_info const & pos) { +void parser::add_decl_index(name const & n, pos_info const & pos, name const & k, expr const & t) { if (m_index) - m_index->add_decl(get_stream_name(), pos, n); + m_index->add_decl(get_stream_name(), pos, n, k, t); } void parser::add_ref_index(name const & n, pos_info const & pos) { @@ -1105,6 +1105,7 @@ void parser::parse_command() { lean_assert(curr() == scanner::token_kind::CommandKeyword); m_last_cmd_pos = pos(); name const & cmd_name = get_token_info().value(); + m_cmd_token = get_token_info().token(); if (auto it = cmds().find(cmd_name)) { next(); m_env = it->get_fn()(*this); diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index d1ff53dc0..864eb62d0 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -98,6 +98,9 @@ class parser { // index support declaration_index * m_index; + // curr command token + name m_cmd_token; + void display_warning_pos(unsigned line, unsigned pos); void display_warning_pos(pos_info p); void display_error_pos(unsigned line, unsigned pos); @@ -191,7 +194,7 @@ public: bool collecting_info() const { return m_info_manager; } void set_index(declaration_index * i) { m_index = i; } - void add_decl_index(name const & n, pos_info const & pos); + 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); environment const & env() const { return m_env; } @@ -215,6 +218,7 @@ public: pos_info pos_of(expr const & e, pos_info default_pos); pos_info pos_of(expr const & e) { return pos_of(e, pos()); } pos_info cmd_pos() const { return m_last_cmd_pos; } + name const & get_cmd_token() const { return m_cmd_token; } void set_line(unsigned p) { return m_scanner.set_line(p); } expr mk_app(expr fn, expr arg, pos_info const & p); diff --git a/src/library/declaration_index.cpp b/src/library/declaration_index.cpp index 80374cdaa..0760d85fa 100644 --- a/src/library/declaration_index.cpp +++ b/src/library/declaration_index.cpp @@ -8,18 +8,24 @@ Author: Leonardo de Moura #include "library/declaration_index.h" namespace lean { -void declaration_index::add_decl(std::string const fname, pos_info const & p, name const & n) { - m_entries.emplace_back(entry_kind::Declaration, fname, p, n); +void declaration_index::add_decl(std::string const fname, pos_info const & p, name const & n, name const & k, expr const & t) { + m_entries.emplace_back(entry_kind::Declaration, fname, p, n, k, t); } void declaration_index::add_ref(std::string const fname, pos_info const & p, name const & n) { - m_entries.emplace_back(entry_kind::Reference, fname, p, n); + m_entries.emplace_back(entry_kind::Reference, fname, p, n, name(), expr()); } -void declaration_index::save(std::ostream & out) const { - entry_kind k; std::string fname; pos_info p; name n; +void declaration_index::save(io_state_stream const & out) const { + entry_kind k; std::string fname; pos_info p; name n, dk; expr t; for (auto const & e : m_entries) { - std::tie(k, fname, p, n) = e; + std::tie(k, fname, p, n, dk, t) = e; out << (k == entry_kind::Declaration ? "d" : "r") << "|" << fname << "|" << p.first - << "|" << p.second << "|" << n << std::endl; + << "|" << p.second << "|" << n; + if (k == entry_kind::Declaration) { + out << "|" << dk << "|"; + options const & opts = out.get_options(); + out.get_stream() << mk_pair(flatten(out.get_formatter()(t)), opts); + } + out << endl; } } } diff --git a/src/library/declaration_index.h b/src/library/declaration_index.h index e776eb69b..1bd3656ce 100644 --- a/src/library/declaration_index.h +++ b/src/library/declaration_index.h @@ -10,17 +10,19 @@ Author: Leonardo de Moura #include #include #include "util/name.h" +#include "kernel/expr.h" #include "kernel/pos_info_provider.h" +#include "library/io_state_stream.h" namespace lean { /** \brief Datastructure for storing where a given declaration was defined. */ class declaration_index { enum class entry_kind { Declaration, Reference }; - typedef std::tuple entry; + typedef std::tuple entry; std::vector m_entries; public: - void add_decl(std::string const fname, pos_info const & p, name const & n); + void add_decl(std::string const fname, pos_info const & p, name const & n, name const & k, expr const & t); void add_ref(std::string const fname, pos_info const & p, name const & n); - void save(std::ostream & out) const; + void save(io_state_stream const & out) const; }; } diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 57b92307f..752929678 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -303,8 +303,9 @@ int main(int argc, char ** argv) { cache.save(out); } if (gen_index) { - std::ofstream out(index_name); - index.save(out); + std::shared_ptr out(new lean::file_output_channel(index_name.c_str())); + ios.set_regular_channel(out); + index.save(regular(env, ios)); } if (export_objects && (permissive || ok)) { std::ofstream out(output, std::ofstream::binary);