From a2817c364424e6901e5bb26e30c410916d65dd64 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 13 Nov 2018 15:01:57 -0800 Subject: [PATCH] refactor(library/compiler): move closed term cache to separate module --- src/library/compiler/CMakeLists.txt | 3 +- src/library/compiler/closed_term_cache.cpp | 85 ++++++++++++++++++++++ src/library/compiler/closed_term_cache.h | 14 ++++ src/library/compiler/extract_closed.cpp | 70 ++---------------- src/library/compiler/extract_closed.h | 2 - src/library/compiler/init_module.cpp | 6 +- 6 files changed, 109 insertions(+), 71 deletions(-) create mode 100644 src/library/compiler/closed_term_cache.cpp create mode 100644 src/library/compiler/closed_term_cache.h diff --git a/src/library/compiler/CMakeLists.txt b/src/library/compiler/CMakeLists.txt index 62eb33729a..3f282eafe5 100644 --- a/src/library/compiler/CMakeLists.txt +++ b/src/library/compiler/CMakeLists.txt @@ -3,4 +3,5 @@ add_library(compiler OBJECT ## New compiler util.cpp lcnf.cpp csimp.cpp elim_dead_let.cpp cse.cpp erase_irrelevant.cpp specialize.cpp compiler.cpp lambda_lifting.cpp extract_closed.cpp - simp_app_args.cpp llnf.cpp ll_infer_type.cpp reduce_arity.cpp ir.cpp) + simp_app_args.cpp llnf.cpp ll_infer_type.cpp reduce_arity.cpp + closed_term_cache.cpp ir.cpp) diff --git a/src/library/compiler/closed_term_cache.cpp b/src/library/compiler/closed_term_cache.cpp new file mode 100644 index 0000000000..a7cbb5f8e8 --- /dev/null +++ b/src/library/compiler/closed_term_cache.cpp @@ -0,0 +1,85 @@ +/* +Copyright (c) 2018 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "library/module.h" +#include "library/util.h" + +namespace lean { +/* Cache closed term => global constant. + TODO(Leo): use the to be implemented new module system. */ +struct closed_term_ext : public environment_extension { + typedef rb_expr_map cache; + cache m_cache; +}; + +struct closed_term_ext_reg { + unsigned m_ext_id; + closed_term_ext_reg() { m_ext_id = environment::register_extension(std::make_shared()); } +}; + +static closed_term_ext_reg * g_ext = nullptr; +static closed_term_ext const & get_extension(environment const & env) { + return static_cast(env.get_extension(g_ext->m_ext_id)); +} +static environment update(environment const & env, closed_term_ext const & ext) { + return env.update(g_ext->m_ext_id, std::make_shared(ext)); +} + +/* Support for old module manager. + Remark: this code will be deleted in the future */ +struct ct_cache_modification : public modification { + LEAN_MODIFICATION("ctc") + + expr m_expr; + name m_name; + + ct_cache_modification(expr const & e, name const & n): m_expr(e), m_name(n) {} + + void perform(environment & env) const override { + closed_term_ext ext = get_extension(env); + ext.m_cache.insert(m_expr, m_name); + env = update(env, ext); + } + + void serialize(serializer & s) const override { + s << m_expr << m_name; + } + + static std::shared_ptr deserialize(deserializer & d) { + expr e; name n; + d >> e >> n; + return std::make_shared(e, n); + } +}; + +optional get_closed_term_name(environment const & env, expr const & e) { + lean_assert(!has_fvars(e)); + lean_assert(!has_loose_bvars(e)); + closed_term_ext const & ext = get_extension(env); + if (name const * c = ext.m_cache.find(e)) { + return optional(*c); + } else { + return optional(); + } +} + +environment cache_closed_term_name(environment const & env, expr const & e, name const & n) { + closed_term_ext ext = get_extension(env); + ext.m_cache.insert(e, n); + environment new_env = module::add(env, std::make_shared(e, n)); + return update(new_env, ext); +} + +void initialize_closed_term_cache() { + g_ext = new closed_term_ext_reg(); + ct_cache_modification::init(); +} + +void finalize_closed_term_cache() { + ct_cache_modification::finalize(); + delete g_ext; +} +} diff --git a/src/library/compiler/closed_term_cache.h b/src/library/compiler/closed_term_cache.h new file mode 100644 index 0000000000..1f495d7b3d --- /dev/null +++ b/src/library/compiler/closed_term_cache.h @@ -0,0 +1,14 @@ +/* +Copyright (c) 2018 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "kernel/environment.h" +namespace lean { +optional get_closed_term_name(environment const & env, expr const & e); +environment cache_closed_term_name(environment const & env, expr const & e, name const & n); +void initialize_closed_term_cache(); +void finalize_closed_term_cache(); +} diff --git a/src/library/compiler/extract_closed.cpp b/src/library/compiler/extract_closed.cpp index 171208df5a..60fb284f4a 100644 --- a/src/library/compiler/extract_closed.cpp +++ b/src/library/compiler/extract_closed.cpp @@ -8,62 +8,14 @@ Author: Leonardo de Moura #include "kernel/instantiate.h" #include "kernel/expr_maps.h" #include "kernel/for_each_fn.h" -#include "library/module.h" #include "library/trace.h" #include "library/compiler/util.h" +#include "library/compiler/closed_term_cache.h" #include "library/compiler/reduce_arity.h" namespace lean { -/* Cache closed term => global constant. - TODO(Leo): use the to be implemented new module system. */ -struct extract_closed_ext : public environment_extension { - typedef rb_expr_map cache; - cache m_cache; -}; - -struct extract_closed_ext_reg { - unsigned m_ext_id; - extract_closed_ext_reg() { m_ext_id = environment::register_extension(std::make_shared()); } -}; - -static extract_closed_ext_reg * g_ext = nullptr; -static extract_closed_ext const & get_extension(environment const & env) { - return static_cast(env.get_extension(g_ext->m_ext_id)); -} -static environment update(environment const & env, extract_closed_ext const & ext) { - return env.update(g_ext->m_ext_id, std::make_shared(ext)); -} - -/* Support for old module manager. - Remark: this code will be deleted in the future */ -struct ec_cache_modification : public modification { - LEAN_MODIFICATION("ecc") - - expr m_expr; - name m_name; - - ec_cache_modification(expr const & e, name const & n): m_expr(e), m_name(n) {} - - void perform(environment & env) const override { - extract_closed_ext ext = get_extension(env); - ext.m_cache.insert(m_expr, m_name); - env = update(env, ext); - } - - void serialize(serializer & s) const override { - s << m_expr << m_name; - } - - static std::shared_ptr deserialize(deserializer & d) { - expr e; name n; - d >> e >> n; - return std::make_shared(e, n); - } -}; - class extract_closed_fn { environment m_env; - extract_closed_ext m_ext; name_generator m_ngen; local_ctx m_lctx; buffer m_new_decls; @@ -258,13 +210,12 @@ class extract_closed_fn { collect_deps(e, fvars); e = m_lctx.mk_lambda(fvars, e); lean_assert(!has_loose_bvars(e)); - if (name const * c = m_ext.m_cache.find(e)) { + if (optional c = get_closed_term_name(m_env, e)) { return mk_constant(*c); } name c = next_name(); m_new_decls.push_back(comp_decl(c, e)); - m_ext.m_cache.insert(e, c); - m_env = module::add(env(), std::make_shared(e, c)); + m_env = cache_closed_term_name(m_env, e, c); return mk_constant(c); } @@ -314,7 +265,7 @@ class extract_closed_fn { public: extract_closed_fn(environment const & env): - m_env(env), m_ext(get_extension(env)) { + m_env(env) { } pair operator()(comp_decl const & d) { @@ -330,8 +281,7 @@ public: m_base_name = d.fst(); expr new_v = visit(v, true); comp_decl new_d(d.fst(), new_v); - environment new_env = update(env(), m_ext); - return mk_pair(new_env, comp_decls(new_d, comp_decls(m_new_decls))); + return mk_pair(env(), comp_decls(new_d, comp_decls(m_new_decls))); } }; @@ -348,14 +298,4 @@ pair extract_closed(environment env, comp_decls const & } return mk_pair(env, r); } - -void initialize_extract_closed() { - g_ext = new extract_closed_ext_reg(); - ec_cache_modification::init(); -} - -void finalize_extract_closed() { - ec_cache_modification::finalize(); - delete g_ext; -} } diff --git a/src/library/compiler/extract_closed.h b/src/library/compiler/extract_closed.h index 67310c3164..dfab5eb6d3 100644 --- a/src/library/compiler/extract_closed.h +++ b/src/library/compiler/extract_closed.h @@ -9,6 +9,4 @@ Author: Leonardo de Moura #include "library/compiler/util.h" namespace lean { pair extract_closed(environment env, comp_decls const & ds); -void initialize_extract_closed(); -void finalize_extract_closed(); } diff --git a/src/library/compiler/init_module.cpp b/src/library/compiler/init_module.cpp index 578f98b805..b6d4b0d9b4 100644 --- a/src/library/compiler/init_module.cpp +++ b/src/library/compiler/init_module.cpp @@ -9,8 +9,8 @@ Author: Leonardo de Moura #include "library/compiler/elim_dead_let.h" #include "library/compiler/cse.h" #include "library/compiler/specialize.h" -#include "library/compiler/extract_closed.h" #include "library/compiler/llnf.h" +#include "library/compiler/closed_term_cache.h" #include "library/compiler/ir.h" #include "library/compiler/compiler.h" @@ -21,7 +21,7 @@ void initialize_compiler_module() { initialize_elim_dead_let(); initialize_cse(); initialize_specialize(); - initialize_extract_closed(); + initialize_closed_term_cache(); initialize_llnf(); initialize_ir(); initialize_compiler(); @@ -31,7 +31,7 @@ void finalize_compiler_module() { finalize_compiler(); finalize_ir(); finalize_llnf(); - finalize_extract_closed(); + finalize_closed_term_cache(); finalize_specialize(); finalize_cse(); finalize_elim_dead_let();