From 384cf04efd4b46853ed3a61eb4237a40c0764338 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 15 Dec 2016 13:06:25 -0800 Subject: [PATCH] refactor(library/aliases,frontends/lean/local_ref_info): merge aliases and local_ref_info modules --- src/frontends/lean/CMakeLists.txt | 2 +- src/frontends/lean/init_module.cpp | 3 -- src/frontends/lean/local_ref_info.cpp | 77 --------------------------- src/frontends/lean/local_ref_info.h | 14 ----- src/frontends/lean/parser.cpp | 5 +- src/frontends/lean/pp.cpp | 3 +- src/library/aliases.cpp | 19 +++++++ src/library/aliases.h | 6 +++ 8 files changed, 29 insertions(+), 100 deletions(-) delete mode 100644 src/frontends/lean/local_ref_info.cpp delete mode 100644 src/frontends/lean/local_ref_info.h diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index d3a4585713..55004d234f 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -4,7 +4,7 @@ parser.cpp parser_pos_provider.cpp builtin_cmds.cpp builtin_exprs.cpp notation_cmd.cpp calc.cpp decl_cmds.cpp util.cpp inductive_cmds.cpp dependencies.cpp pp.cpp structure_cmd.cpp structure_instance.cpp -init_module.cpp type_util.cpp local_ref_info.cpp decl_attributes.cpp +init_module.cpp type_util.cpp decl_attributes.cpp opt_cmd.cpp prenum.cpp print_cmd.cpp elaborator.cpp elaborator_exception.cpp match_expr.cpp local_context_adapter.cpp decl_util.cpp definition_cmds.cpp brackets.cpp tactic_notation.cpp info_manager.cpp json.cpp) diff --git a/src/frontends/lean/init_module.cpp b/src/frontends/lean/init_module.cpp index 38a01abe8e..2c038d02b2 100644 --- a/src/frontends/lean/init_module.cpp +++ b/src/frontends/lean/init_module.cpp @@ -16,7 +16,6 @@ Author: Leonardo de Moura #include "frontends/lean/token_table.h" #include "frontends/lean/scanner.h" #include "frontends/lean/pp.h" -#include "frontends/lean/local_ref_info.h" #include "frontends/lean/decl_cmds.h" #include "frontends/lean/prenum.h" #include "frontends/lean/elaborator.h" @@ -41,7 +40,6 @@ void initialize_frontend_lean_module() { initialize_inductive_cmds(); initialize_structure_instance(); initialize_pp(); - initialize_local_ref_info(); initialize_decl_cmds(); initialize_match_expr(); initialize_elaborator(); @@ -54,7 +52,6 @@ void finalize_frontend_lean_module() { finalize_elaborator(); finalize_match_expr(); finalize_decl_cmds(); - finalize_local_ref_info(); finalize_pp(); finalize_structure_instance(); finalize_inductive_cmds(); diff --git a/src/frontends/lean/local_ref_info.cpp b/src/frontends/lean/local_ref_info.cpp deleted file mode 100644 index daf56fcded..0000000000 --- a/src/frontends/lean/local_ref_info.cpp +++ /dev/null @@ -1,77 +0,0 @@ -/* -Copyright (c) 2015 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include "library/scoped_ext.h" - -namespace lean { -/* -When we declare a definition in a section, we create an alias for it that fixes the parameters in -universe parameters. We have to store the number of parameters and universes that have been fixed -to be able to correctly pretty print terms. -*/ -struct local_ref_entry { - name m_name; - expr m_ref; - local_ref_entry() {} - local_ref_entry(name const & n, expr const & ref): - m_name(n), m_ref(ref) {} -}; - -static name * g_local_ref_name = nullptr; -static std::string * g_key = nullptr; - -struct local_ref_config { - typedef name_map state; - typedef local_ref_entry entry; - - static void add_entry(environment const &, io_state const &, state & s, entry const & e) { - s.insert(e.m_name, e.m_ref); - } - static name const & get_class_name() { - return *g_local_ref_name; - } - static std::string const & get_serialization_key() { - return *g_key; - } - static void write_entry(serializer &, entry const &) { - lean_unreachable(); - } - static entry read_entry(deserializer &) { - lean_unreachable(); - } - static optional get_fingerprint(entry const &) { - return optional(); - } -}; - -template class scoped_ext; -typedef scoped_ext local_ref_ext; - -environment save_local_ref_info(environment const & env, name const & n, expr const & ref) { - bool persistent = false; - return local_ref_ext::add_entry(env, get_dummy_ios(), local_ref_entry(n, ref), persistent); -} - -optional get_local_ref_info(environment const & env, name const & n) { - if (auto r = local_ref_ext::get_state(env).find(n)) - return some_expr(*r); - else - return none_expr(); -} - -void initialize_local_ref_info() { - g_local_ref_name = new name("localrefinfo"); - g_key = new std::string("localrefinfo"); - local_ref_ext::initialize(); -} - -void finalize_local_ref_info() { - local_ref_ext::finalize(); - delete g_local_ref_name; - delete g_key; -} -} diff --git a/src/frontends/lean/local_ref_info.h b/src/frontends/lean/local_ref_info.h deleted file mode 100644 index 2866036b64..0000000000 --- a/src/frontends/lean/local_ref_info.h +++ /dev/null @@ -1,14 +0,0 @@ -/* -Copyright (c) 2015 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once - -namespace lean { -environment save_local_ref_info(environment const & env, name const & n, expr const & ref); -optional get_local_ref_info(environment const & env, name const & n); -void initialize_local_ref_info(); -void finalize_local_ref_info(); -} diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 8318cf81e3..39ed53364e 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -56,7 +56,6 @@ Author: Leonardo de Moura #include "frontends/lean/notation_cmd.h" #include "frontends/lean/parser_pos_provider.h" #include "frontends/lean/update_environment_exception.h" -#include "frontends/lean/local_ref_info.h" #include "frontends/lean/opt_cmd.h" #include "frontends/lean/builtin_cmds.h" #include "frontends/lean/prenum.h" @@ -568,12 +567,12 @@ environment parser::add_local_ref(environment const & env, name const & n, expr if (is_explicit(f)) f = get_explicit_arg(f); if (is_constant(f)) { - return save_local_ref_info(env, const_name(f), ref); + return ::lean::add_local_ref(env, const_name(f), ref); } else { return env; } } else if (is_constant(ref) && const_levels(ref)) { - return save_local_ref_info(env, const_name(ref), ref); + return ::lean::add_local_ref(env, const_name(ref), ref); } else { return env; } diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index cc66c92099..e9ccc73422 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -45,7 +45,6 @@ Author: Leonardo de Moura #include "frontends/lean/token_table.h" #include "frontends/lean/builtin_exprs.h" #include "frontends/lean/parser_config.h" -#include "frontends/lean/local_ref_info.h" #include "frontends/lean/scanner.h" namespace lean { @@ -455,7 +454,7 @@ static local_ref_kind check_local_ref(environment const & env, expr const & e, u expr const & rfn = get_app_fn(e); if (!is_constant(rfn)) return NotLocalRef; - auto ref = get_local_ref_info(env, const_name(rfn)); + auto ref = get_local_ref(env, const_name(rfn)); if (!ref) return NotLocalRef; if (is_as_atomic(*ref)) diff --git a/src/library/aliases.cpp b/src/library/aliases.cpp index 0052c54206..243ace1a70 100644 --- a/src/library/aliases.cpp +++ b/src/library/aliases.cpp @@ -28,6 +28,7 @@ struct aliases_ext : public environment_extension { name_map m_inv_aliases; name_map m_level_aliases; name_map m_inv_level_aliases; + name_map m_local_refs; state():m_in_section(false) {} void add_expr_alias(name const & a, name const & e, bool overwrite) { @@ -76,6 +77,10 @@ struct aliases_ext : public environment_extension { add_expr_alias(a, e, overwrite); } + void add_local_ref(name const & a, expr const & ref) { + m_state.m_local_refs.insert(a, ref); + } + void push(bool in_section) { m_scopes = cons(m_state, m_scopes); m_state.m_in_section = in_section; @@ -140,6 +145,20 @@ list get_expr_aliases(environment const & env, name const & n) { return ptr_to_list(get_extension(env).m_state.m_aliases.find(n)); } +environment add_local_ref(environment const & env, name const & a, expr const & ref) { + aliases_ext ext = get_extension(env); + ext.add_local_ref(a, ref); + return update(env, ext); +} + +optional get_local_ref(environment const & env, name const & n) { + aliases_ext const & ext = get_extension(env); + if (auto r = ext.m_state.m_local_refs.find(n)) + return some_expr(*r); + else + return none_expr(); +} + static void check_no_shadow(environment const & env, name const & a) { if (env.is_universe(a)) throw exception(sstream() << "universe level alias '" << a << "' shadows existing global universe level"); diff --git a/src/library/aliases.h b/src/library/aliases.h index c22f39fe52..7fe71efdae 100644 --- a/src/library/aliases.h +++ b/src/library/aliases.h @@ -56,6 +56,12 @@ bool is_exception(name const & n, name const & prefix, unsigned num_exceptions, void for_each_expr_alias(environment const & env, std::function const &)> const & fn); +/* When we declare a definition in a section, we create an alias for it that fixes the parameters in + universe parameters. */ +environment add_local_ref(environment const & env, name const & a, expr const & ref); + +optional get_local_ref(environment const & env, name const & n); + void initialize_aliases(); void finalize_aliases(); }