From dc3e9a15d23522434b3f922afdf78016d0e187f2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 14 Aug 2014 18:12:12 -0700 Subject: [PATCH] refactor(library/definitions_cache): rename to definition_cache Signed-off-by: Leonardo de Moura --- src/frontends/lean/parser.cpp | 4 ++-- src/frontends/lean/parser.h | 10 +++++----- src/frontends/lean/server.h | 4 ++-- src/library/CMakeLists.txt | 2 +- ...{definitions_cache.cpp => definition_cache.cpp} | 14 +++++++------- .../{definitions_cache.h => definition_cache.h} | 4 ++-- src/shell/lean.cpp | 8 ++++---- 7 files changed, 23 insertions(+), 23 deletions(-) rename src/library/{definitions_cache.cpp => definition_cache.cpp} (92%) rename src/library/{definitions_cache.h => definition_cache.h} (97%) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 88042477a..b33253662 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1299,7 +1299,7 @@ void parser::save_type_info(expr const & e) { } bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name, bool use_exceptions, - unsigned num_threads, definitions_cache * cache, declaration_index * index) { + unsigned num_threads, definition_cache * cache, declaration_index * index) { parser p(env, ios, in, strm_name, use_exceptions, num_threads); p.set_cache(cache); p.set_index(index); @@ -1310,7 +1310,7 @@ bool parse_commands(environment & env, io_state & ios, std::istream & in, char c } bool parse_commands(environment & env, io_state & ios, char const * fname, bool use_exceptions, unsigned num_threads, - definitions_cache * cache, declaration_index * index) { + definition_cache * cache, declaration_index * index) { std::ifstream in(fname); if (in.bad() || in.fail()) throw exception(sstream() << "failed to open file '" << fname << "'"); diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 99261af4e..56f826b51 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -20,7 +20,7 @@ Author: Leonardo de Moura #include "library/io_state.h" #include "library/io_state_stream.h" #include "library/kernel_bindings.h" -#include "library/definitions_cache.h" +#include "library/definition_cache.h" #include "library/declaration_index.h" #include "frontends/lean/scanner.h" #include "frontends/lean/elaborator.h" @@ -94,7 +94,7 @@ class parser { std::vector m_pre_info_data; // type information before elaboration // cache support - definitions_cache * m_cache; + definition_cache * m_cache; // index support declaration_index * m_index; @@ -179,7 +179,7 @@ public: snapshot_vector * sv = nullptr, info_manager * im = nullptr); ~parser(); - void set_cache(definitions_cache * c) { m_cache = c; } + void set_cache(definition_cache * c) { m_cache = c; } void cache_definition(name const & n, expr const & pre_type, expr const & pre_value, level_param_names const & ls, expr const & type, expr const & value); /** \brief Try to find an elaborated definition for (n, pre_type, pre_value) in the cache */ @@ -333,8 +333,8 @@ public: }; bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name, - bool use_exceptions, unsigned num_threads, definitions_cache * cache = nullptr, + bool use_exceptions, unsigned num_threads, definition_cache * cache = nullptr, declaration_index * index = nullptr); bool parse_commands(environment & env, io_state & ios, char const * fname, bool use_exceptions, unsigned num_threads, - definitions_cache * cache = nullptr, declaration_index * index = nullptr); + definition_cache * cache = nullptr, declaration_index * index = nullptr); } diff --git a/src/frontends/lean/server.h b/src/frontends/lean/server.h index eeb6da760..2dd963cc5 100644 --- a/src/frontends/lean/server.h +++ b/src/frontends/lean/server.h @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include #include #include -#include "library/definitions_cache.h" +#include "library/definition_cache.h" #include "frontends/lean/parser.h" #include "frontends/lean/info_manager.h" @@ -40,7 +40,7 @@ class server { std::ostream & m_out; unsigned m_num_threads; snapshot m_empty_snapshot; - definitions_cache m_cache; + definition_cache m_cache; void load_file(std::string const & fname); void visit_file(std::string const & fname); diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index fba69cb70..530306043 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -7,6 +7,6 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp standard_kernel.cpp hott_kernel.cpp unifier.cpp unifier_plugin.cpp inductive_unifier_plugin.cpp explicit.cpp num.cpp string.cpp opaque_hints.cpp head_map.cpp - match.cpp definitions_cache.cpp declaration_index.cpp) + match.cpp definition_cache.cpp declaration_index.cpp) target_link_libraries(library ${LEAN_LIBS}) diff --git a/src/library/definitions_cache.cpp b/src/library/definition_cache.cpp similarity index 92% rename from src/library/definitions_cache.cpp rename to src/library/definition_cache.cpp index d03ed8cef..15d004b14 100644 --- a/src/library/definitions_cache.cpp +++ b/src/library/definition_cache.cpp @@ -7,7 +7,7 @@ Author: Leonardo de Moura #include "util/interrupt.h" #include "library/placeholder.h" #include "library/kernel_serializer.h" -#include "library/definitions_cache.h" +#include "library/definition_cache.h" namespace lean { /** \brief Similar to expr_eq_fn, but allows different placeholders @@ -118,9 +118,9 @@ public: bool operator()(expr const & a, expr const & b) { return compare(a, b); } }; -definitions_cache::definitions_cache() {} +definition_cache::definition_cache() {} -void definitions_cache::load(std::istream & in) { +void definition_cache::load(std::istream & in) { lock_guard lc(m_mutex); deserializer d(in); unsigned num; @@ -134,18 +134,18 @@ void definitions_cache::load(std::istream & in) { } } -void definitions_cache::add_core(name const & n, expr const & pre_type, expr const & pre_value, +void definition_cache::add_core(name const & n, expr const & pre_type, expr const & pre_value, level_param_names const & ls, expr const & type, expr const & value) { m_definitions.insert(n, entry(pre_type, pre_value, ls, type, value)); } -void definitions_cache::add(name const & n, expr const & pre_type, expr const & pre_value, +void definition_cache::add(name const & n, expr const & pre_type, expr const & pre_value, level_param_names const & ls, expr const & type, expr const & value) { lock_guard lc(m_mutex); add_core(n, pre_type, pre_value, ls, type, value); } -optional> definitions_cache::find(name const & n, expr const & pre_type, expr const & pre_value) { +optional> definition_cache::find(name const & n, expr const & pre_type, expr const & pre_value) { entry const * it; { lock_guard lc(m_mutex); @@ -162,7 +162,7 @@ optional> definitions_cache::find(name return optional>(); } -void definitions_cache::save(std::ostream & out) { +void definition_cache::save(std::ostream & out) { lock_guard lc(m_mutex); serializer s(out); s << m_definitions.size(); diff --git a/src/library/definitions_cache.h b/src/library/definition_cache.h similarity index 97% rename from src/library/definitions_cache.h rename to src/library/definition_cache.h index 0c90dc26f..3bd2a99f3 100644 --- a/src/library/definitions_cache.h +++ b/src/library/definition_cache.h @@ -14,14 +14,14 @@ namespace lean { /** \brief Cache for mapping definitions (type, value) before elaboration to (level_names, type, value) after elaboration. */ -class definitions_cache { +class definition_cache { typedef std::tuple entry; mutex m_mutex; name_map m_definitions; void add_core(name const & n, expr const & pre_type, expr const & pre_value, level_param_names const & ls, expr const & type, expr const & value); public: - definitions_cache(); + definition_cache(); /** \brief Add the cache entry (n, pre_type, pre_value) -> (ls, type, value) */ void add(name const & n, expr const & pre_type, expr const & pre_value, level_param_names const & ls, expr const & type, expr const & value); /** \brief Return (if available) elaborated (level_names, type, value) for (n, pre_type, pre_value). diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 5678950c2..93f4d7a29 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -24,7 +24,7 @@ Author: Leonardo de Moura #include "library/hott_kernel.h" #include "library/module.h" #include "library/io_state_stream.h" -#include "library/definitions_cache.h" +#include "library/definition_cache.h" #include "library/declaration_index.h" #include "library/error_handling/error_handling.h" #include "frontends/lean/parser.h" @@ -45,7 +45,7 @@ using lean::mk_environment; using lean::mk_hott_environment; using lean::set_environment; using lean::set_io_state; -using lean::definitions_cache; +using lean::definition_cache; using lean::pos_info; using lean::pos_info_provider; using lean::optional; @@ -247,8 +247,8 @@ int main(int argc, char ** argv) { script_state S = lean::get_thread_script_state(); set_environment set1(S, env); set_io_state set2(S, ios); - definitions_cache cache; - definitions_cache * cache_ptr = nullptr; + definition_cache cache; + definition_cache * cache_ptr = nullptr; if (use_cache) { cache_ptr = &cache; std::ifstream in(cache_name);