From 95acb5cf3aebd0687e0159ede5a1d0f0ccc35aa9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 27 Oct 2020 09:21:21 -0700 Subject: [PATCH] chore: remove old `fun_info` module --- src/library/CMakeLists.txt | 2 +- src/library/abstract_context_cache.h | 56 ----- src/library/fun_info.cpp | 295 --------------------------- src/library/fun_info.h | 107 ---------- src/library/init_module.cpp | 3 - src/library/type_context.cpp | 1 - 6 files changed, 1 insertion(+), 463 deletions(-) delete mode 100644 src/library/fun_info.cpp delete mode 100644 src/library/fun_info.h diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index d2d33ee38b..1b65db9a93 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -6,7 +6,7 @@ add_library(library OBJECT expr_lt.cpp io_state.cpp pp_options.cpp projection.cpp idx_metavar.cpp aux_recursors.cpp trace.cpp local_context.cpp metavar_context.cpp - type_context.cpp fun_info.cpp + type_context.cpp locals.cpp messages.cpp message_builder.cpp check.cpp profiling.cpp time_task.cpp abstract_context_cache.cpp diff --git a/src/library/abstract_context_cache.h b/src/library/abstract_context_cache.h index ce3cbf3672..df5394dba0 100644 --- a/src/library/abstract_context_cache.h +++ b/src/library/abstract_context_cache.h @@ -9,7 +9,6 @@ Author: Leonardo de Moura #include "kernel/expr.h" #include "kernel/declaration.h" #include "library/projection.h" -#include "library/fun_info.h" namespace lean { #define LEAN_NUM_TRANSPARENCY_MODES 3 @@ -198,33 +197,6 @@ public: virtual optional get_whnf(transparency_mode, expr const &) = 0; virtual void set_whnf(transparency_mode, expr const &, expr const &) = 0; - /* Cache support for fun_info module */ - - virtual optional get_fun_info(transparency_mode, expr const &) = 0; - virtual void set_fun_info(transparency_mode, expr const &, fun_info const &) = 0; - - virtual optional get_fun_info_nargs(transparency_mode, expr const &, unsigned) = 0; - virtual void set_fun_info_nargs(transparency_mode, expr const &, unsigned, fun_info const &) = 0; - - virtual optional get_specialization_prefix_size(transparency_mode, expr const &, unsigned) = 0; - virtual void set_specialization_prefix_size(transparency_mode, expr const &, unsigned, unsigned) = 0; - - virtual optional get_subsingleton_info(transparency_mode, expr const &) = 0; - virtual void set_subsingleton_info(transparency_mode, expr const &, ss_param_infos const &) = 0; - - virtual optional get_subsingleton_info_nargs(transparency_mode, expr const &, unsigned) = 0; - virtual void set_subsingleton_info_nargs(transparency_mode, expr const &, unsigned, ss_param_infos const &) = 0; - - virtual optional get_specialized_subsingleton_info_nargs(transparency_mode, expr const &, unsigned) = 0; - virtual void set_specialization_subsingleton_info_nargs(transparency_mode, expr const &, unsigned, ss_param_infos const &) = 0; - - /* Cache support for app_builder */ - - virtual optional get_app_builder_info(expr const &, unsigned) = 0; - virtual void set_app_builder_info(expr const &, unsigned, app_builder_info const &) = 0; - - virtual optional get_app_builder_info(expr const &, list const &) = 0; - virtual void set_app_builder_info(expr const &, list const &, app_builder_info const &) = 0; }; /* Dummy implementation of the abstract_context_cache interface that does not do cache anything but configuration options. */ @@ -275,34 +247,6 @@ public: virtual optional get_whnf(transparency_mode, expr const &) override { return none_expr(); } virtual void set_whnf(transparency_mode, expr const &, expr const &) override {} - - /* Cache support for fun_info module */ - - virtual optional get_fun_info(transparency_mode, expr const &) override { return optional(); } - virtual void set_fun_info(transparency_mode, expr const &, fun_info const &) override {} - - virtual optional get_fun_info_nargs(transparency_mode, expr const &, unsigned) override { return optional(); } - virtual void set_fun_info_nargs(transparency_mode, expr const &, unsigned, fun_info const &) override {} - - virtual optional get_specialization_prefix_size(transparency_mode, expr const &, unsigned) override { return optional(); } - virtual void set_specialization_prefix_size(transparency_mode, expr const &, unsigned, unsigned) override {} - - virtual optional get_subsingleton_info(transparency_mode, expr const &) override { return optional(); } - virtual void set_subsingleton_info(transparency_mode, expr const &, ss_param_infos const &) override {} - - virtual optional get_subsingleton_info_nargs(transparency_mode, expr const &, unsigned) override { return optional(); } - virtual void set_subsingleton_info_nargs(transparency_mode, expr const &, unsigned, ss_param_infos const &) override {} - - virtual optional get_specialized_subsingleton_info_nargs(transparency_mode, expr const &, unsigned) override { return optional(); } - virtual void set_specialization_subsingleton_info_nargs(transparency_mode, expr const &, unsigned, ss_param_infos const &) override {} - - /* Cache support for app_builder */ - - virtual optional get_app_builder_info(expr const &, unsigned) override { return optional(); } - virtual void set_app_builder_info(expr const &, unsigned, app_builder_info const &) override {} - - virtual optional get_app_builder_info(expr const &, list const &) override { return optional(); } - virtual void set_app_builder_info(expr const &, list const &, app_builder_info const &) override {} }; void initialize_abstract_context_cache(); diff --git a/src/library/fun_info.cpp b/src/library/fun_info.cpp deleted file mode 100644 index 96345c97b3..0000000000 --- a/src/library/fun_info.cpp +++ /dev/null @@ -1,295 +0,0 @@ -/* -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include "kernel/for_each_fn.h" -#include "kernel/instantiate.h" -#include "kernel/abstract.h" -#include "kernel/expr_maps.h" -#include "library/trace.h" -#include "library/util.h" -#include "library/constants.h" -#include "library/expr_unsigned_map.h" -#include "library/fun_info.h" -#include "library/cache_helper.h" - -namespace lean { -static name * g_fun_info = nullptr; - -#define lean_trace_fun_info(Code) lean_trace(*g_fun_info, Code) - -static bool is_fun_info_trace_enabled() { - return is_trace_class_enabled(*g_fun_info); -} - -void initialize_fun_info() { - g_fun_info = new name("fun_info"); - mark_persistent(g_fun_info->raw()); - register_trace_class(*g_fun_info); -} - -void finalize_fun_info() { - delete g_fun_info; -} - -/* Return the list of dependencies for the given type. - If it depends on local i, then it also sets pinfos[i].set_has_fwd_deps(); - */ -static list collect_deps(expr const & type, buffer const & locals, buffer & pinfos) { - buffer deps; - for_each(type, [&](expr const & e, unsigned) { - if (is_local_or_fvar(e)) { - unsigned idx; - for (idx = 0; idx < locals.size(); idx++) - if (locals[idx] == e) - break; - if (idx < locals.size() && std::find(deps.begin(), deps.end(), idx) == deps.end()) { - deps.push_back(idx); - pinfos[idx].set_has_fwd_deps(); - } - } - return has_local(e); // continue the search only if e has locals - }); - std::sort(deps.begin(), deps.end()); - return to_list(deps); -} - -/* Store parameter info for fn in \c pinfos and return the dependencies of the resulting type. */ -static list get_core(type_context_old & ctx, - expr const & fn, buffer & pinfos, - unsigned max_args) { - expr type = ctx.relaxed_try_to_pi(ctx.infer(fn)); - type_context_old::tmp_locals locals(ctx); - unsigned i = 0; - while (is_pi(type)) { - if (i == max_args) - break; - expr local_type = consume_auto_opt_param(binding_domain(type)); - expr local = locals.push_local(binding_name(type), local_type, binding_info(type)); - expr new_type = ctx.relaxed_try_to_pi(instantiate(binding_body(type), local)); - bool is_prop = ctx.is_prop(local_type); - bool is_dep = false; /* it is set by collect_deps */ - binder_info bi = binding_info(type); - pinfos.emplace_back(is_implicit(bi), - is_inst_implicit(bi), - is_prop, is_dep, collect_deps(local_type, locals.as_buffer(), pinfos)); - type = new_type; - i++; - } - return collect_deps(type, locals.as_buffer(), pinfos); -} - -fun_info get_fun_info(type_context_old & ctx, expr const & e) { - abstract_context_cache & cache = ctx.get_cache(); - if (auto r = cache.get_fun_info(ctx.mode(), e)) - return *r; - buffer pinfos; - auto result_deps = get_core(ctx, e, pinfos, std::numeric_limits::max()); - fun_info r(pinfos.size(), to_list(pinfos), result_deps); - cache.set_fun_info(ctx.mode(), e, r); - return r; -} - -fun_info get_fun_info(type_context_old & ctx, expr const & e, unsigned nargs) { - abstract_context_cache & cache = ctx.get_cache(); - if (auto r = cache.get_fun_info_nargs(ctx.mode(), e, nargs)) - return *r; - buffer pinfos; - auto result_deps = get_core(ctx, e, pinfos, nargs); - fun_info r(pinfos.size(), to_list(pinfos), result_deps); - cache.set_fun_info_nargs(ctx.mode(), e, nargs, r); - return r; -} - -/* Store subsingleton parameter info for fn in \c ssinfos */ -static void get_ss_core(type_context_old & ctx, expr const & fn, buffer & ssinfos, - unsigned max_args) { - expr type = ctx.relaxed_try_to_pi(ctx.infer(fn)); - type_context_old::tmp_locals locals(ctx); - unsigned i = 0; - while (is_pi(type)) { - if (i == max_args) - break; - expr local = locals.push_local_from_binding(type); - expr local_type = ctx.infer(local); - expr new_type = ctx.relaxed_try_to_pi(instantiate(binding_body(type), local)); - bool spec = false; - bool is_prop = ctx.is_prop(local_type); - bool is_sub = is_prop; - if (!is_sub) { - // TODO(Leo): check if the following line is a performance bottleneck. - is_sub = static_cast(ctx.mk_subsingleton_instance(local_type)); - } - ssinfos.emplace_back(spec, is_sub); - type = new_type; - i++; - } -} - -ss_param_infos get_subsingleton_info(type_context_old & ctx, expr const & e) { - abstract_context_cache & cache = ctx.get_cache(); - if (auto r = cache.get_subsingleton_info(ctx.mode(), e)) - return *r; - buffer ssinfos; - get_ss_core(ctx, e, ssinfos, std::numeric_limits::max()); - ss_param_infos r = to_list(ssinfos); - cache.set_subsingleton_info(ctx.mode(), e, r); - return r; -} - -ss_param_infos get_subsingleton_info(type_context_old & ctx, expr const & e, unsigned nargs) { - abstract_context_cache & cache = ctx.get_cache(); - if (auto r = cache.get_subsingleton_info_nargs(ctx.mode(), e, nargs)) - return *r; - buffer ssinfos; - get_ss_core(ctx, e, ssinfos, nargs); - ss_param_infos r = to_list(ssinfos); - cache.set_subsingleton_info_nargs(ctx.mode(), e, nargs, r); - return r; -} - -/* Return true if there is j s.t. ssinfos[j] is marked as subsingleton, - and it dependends of argument i */ -static bool has_nonsubsingleton_fwd_dep(unsigned i, buffer const & pinfos, buffer const & ssinfos) { - lean_assert(pinfos.size() == ssinfos.size()); - for (unsigned j = i+1; j < pinfos.size(); j++) { - if (ssinfos[j].is_subsingleton()) - continue; - auto const & back_deps = pinfos[j].get_back_deps(); - if (std::find(back_deps.begin(), back_deps.end(), i) != back_deps.end()) { - return true; - } - } - return false; -} - -static void trace_if_unsupported(type_context_old & ctx, expr const & fn, - buffer const & args, unsigned prefix_sz, ss_param_infos const & result) { - lean_assert(args.size() >= length(result)); - if (!is_fun_info_trace_enabled()) - return; - fun_info info = get_fun_info(ctx, fn, args.size()); - buffer pinfos; - to_buffer(info.get_params_info(), pinfos); - buffer ssinfos; - to_buffer(get_subsingleton_info(ctx, fn, args.size()), ssinfos); - lean_assert(pinfos.size() == ssinfos.size()); - /* Check if all remaining arguments are nondependent or - dependent (but all forward dependencies are subsingletons) */ - unsigned i = prefix_sz; - for (; i < pinfos.size(); i++) { - param_info const & pinfo = pinfos[i]; - if (!pinfo.has_fwd_deps()) - continue; /* nondependent argument */ - if (has_nonsubsingleton_fwd_dep(i, pinfos, ssinfos)) - break; /* failed i-th argument has a forward dependent that is not a prop nor a subsingleton */ - } - if (i == pinfos.size()) - return; // It is *cheap* case - - /* Expensive case */ - /* We generate a trace message IF it would be possible to compute more precise information. - That is, there is an argument that is a proposition and/or subsingleton, but - the corresponding pinfo is not a marked a prop/subsingleton. - */ - i = 0; - for (ss_param_info const & ssinfo : result) { - if (ssinfo.is_subsingleton()) - continue; - expr arg_type = ctx.infer(args[i]); - if (ctx.mk_subsingleton_instance(arg_type)) { - lean_trace_fun_info( - tout() << "approximating function information for '" << fn - << "', this may affect the effectiveness of the simplifier and congruence closure modules, " - << "more precise information can be efficiently computed if all parameters are moved to the " - << "beginning of the function\n";); - return; - } - i++; - } -} - -unsigned get_specialization_prefix_size(type_context_old & ctx, expr const & fn, unsigned nargs) { - /* - We say a function is "cheap" if it is of the form: - - a) 0 or more dependent parameters p s.t. there is at least one forward dependency x : C[p] - which is not a proposition nor a subsingleton. - - b) followed by 0 or more nondependent parameter and/or a dependent parameter - s.t. all forward dependencies are propositions and subsingletons. - - We have a caching mechanism for the "cheap" case. - The cheap case cover many commonly used functions - - eq : Pi {A : Type} (x y : A), Prop - add : Pi {A : Type} [s : has_add A] (x y : A), A - inv : Pi {A : Type} [s : has_inv A] (x : A) (h : invertible x), A - - but it doesn't cover - - p : Pi {A : Type} (x : A) {B : Type} (y : B), Prop - - I don't think this is a big deal since we can write it as: - - p : Pi {A : Type} {B : Type} (x : A) (y : B), Prop - - Therefore, we ignore the non-cheap cases, and pretend they are "cheap". - If tracing is enabled, we produce a tracing message whenever we find - a non-cheap case. - - This procecure returns the size of group a) - */ - abstract_context_cache & cache = ctx.get_cache(); - if (auto r = cache.get_specialization_prefix_size(ctx.mode(), fn, nargs)) - return *r; - fun_info info = get_fun_info(ctx, fn, nargs); - buffer pinfos; - to_buffer(info.get_params_info(), pinfos); - buffer ssinfos; - to_buffer(get_subsingleton_info(ctx, fn, nargs), ssinfos); - lean_assert(pinfos.size() == ssinfos.size()); - /* Compute "prefix": 0 or more parameters s.t. - at lest one forward dependency is not a proposition or a subsingleton */ - unsigned i = 0; - for (; i < pinfos.size(); i++) { - param_info const & pinfo = pinfos[i]; - if (!pinfo.has_fwd_deps()) - break; - /* search for forward dependency that is not a proposition nor a subsingleton */ - if (!has_nonsubsingleton_fwd_dep(i, pinfos, ssinfos)) - break; - } - unsigned prefix_sz = i; - cache.set_specialization_prefix_size(ctx.mode(), fn, nargs, prefix_sz); - return prefix_sz; -} - -ss_param_infos get_specialized_subsingleton_info(type_context_old & ctx, expr const & a) { - lean_assert(is_app(a)); - buffer args; - expr const & fn = get_app_args(a, args); - unsigned prefix_sz = get_specialization_prefix_size(ctx, fn, args.size()); - unsigned num_rest_args = args.size() - prefix_sz; - expr g = a; - for (unsigned i = 0; i < num_rest_args; i++) - g = app_fn(g); - abstract_context_cache & cache = ctx.get_cache(); - if (auto r = cache.get_specialized_subsingleton_info_nargs(ctx.mode(), g, num_rest_args)) - return *r; - buffer ssinfos; - get_ss_core(ctx, fn, ssinfos, prefix_sz); - for (unsigned i = 0; i < prefix_sz; i++) { - ssinfos[i].set_specialized(); - } - get_ss_core(ctx, g, ssinfos, num_rest_args); - ss_param_infos r = to_list(ssinfos); - cache.set_specialization_subsingleton_info_nargs(ctx.mode(), g, num_rest_args, r); - trace_if_unsupported(ctx, fn, args, prefix_sz, r); - return r; -} -} diff --git a/src/library/fun_info.h b/src/library/fun_info.h deleted file mode 100644 index 4f7739f295..0000000000 --- a/src/library/fun_info.h +++ /dev/null @@ -1,107 +0,0 @@ -/* -Copyright (c) 2016 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/expr.h" - -namespace lean { -class type_context_old; - -/** \brief Function parameter information. */ -class param_info { - unsigned m_implicit:1; - unsigned m_inst_implicit:1; - unsigned m_prop:1; - unsigned m_has_fwd_deps:1; // true if rest depends on this parameter - list m_back_deps; // previous arguments it depends on -public: - param_info(bool imp, bool inst_imp, bool prop, bool has_fwd_deps, list const & back_deps): - m_implicit(imp), m_inst_implicit(inst_imp), m_prop(prop), - m_has_fwd_deps(has_fwd_deps), m_back_deps(back_deps) {} - list const & get_back_deps() const { return m_back_deps; } - bool is_implicit() const { return m_implicit; } - bool is_inst_implicit() const { return m_inst_implicit; } - bool is_prop() const { return m_prop; } - bool has_fwd_deps() const { return m_has_fwd_deps; } - void set_has_fwd_deps() { m_has_fwd_deps = true; } -}; - -/** \brief Function information produced by get_fun_info procedures. */ -class fun_info { - unsigned m_arity; - list m_params_info; - list m_result_deps; // resulting type dependencies -public: - fun_info():m_arity(0) {} - fun_info(unsigned arity, list const & info, list const & result_deps): - m_arity(arity), m_params_info(info), m_result_deps(result_deps) {} - unsigned get_arity() const { return m_arity; } - list const & get_params_info() const { return m_params_info; } - list const & get_result_deps() const { return m_result_deps; } -}; - -fun_info get_fun_info(type_context_old & ctx, expr const & fn); -/** \brief Return information assuming the function has only nargs. - \pre nargs <= get_fun_info(ctx, fn).get_arity() */ -fun_info get_fun_info(type_context_old & ctx, expr const & fn, unsigned nargs); - -/** \brief Subsingleton parameter information */ -class subsingleton_param_info { - /* m_specialized is true if the result of fun_info has been specifialized - using this argument. - For example, consider the function - - f : Pi (A : Type), A -> A - - Now, suppse we request get_specialize fun_info for the application - - f unit a - - fun_info_manager returns two param_info objects: - 1) m_specialized = true - 2) m_subsingleton = true - - Note that, in general, the second argument of f is not a subsingleton, - but it is in this particular case/specialization. - - \remark This bit is only set if it is a dependent parameter (i.e., m_is_dep is true). - - Moreover, we only set m_specialized IF another parameter - becomes a subsingleton or proposition. */ - unsigned short m_specialized; - unsigned short m_subsingleton; -public: - subsingleton_param_info(bool spec, bool ss): - m_specialized(spec), m_subsingleton(ss) {} - bool specialized() const { return m_specialized; } - bool is_subsingleton() const { return m_subsingleton; } - void set_specialized() { m_specialized = true; } -}; - -typedef subsingleton_param_info ss_param_info; -typedef list ss_param_infos; - -list get_subsingleton_info(type_context_old & ctx, expr const & fn); -list get_subsingleton_info(type_context_old & ctx, expr const & fn, unsigned nargs); -/** \brief Return subsingleton parameter information for the function application. - This is more precise than \c get_subsingleton_info for dependent functions. - - Example: given (f : Pi (A : Type), A -> A), \c get_specialized_fun_info for - - f unit b - - returns a \c fun_info with two param_info - 1) m_specialized = true - 2) m_subsingleton = true - - The second argument is marked as subsingleton only because the resulting information - is taking into account the first argument. */ -list get_specialized_subsingleton_info(type_context_old & ctx, expr const & app); -unsigned get_specialization_prefix_size(type_context_old & ctx, expr const & fn, unsigned nargs); - -void initialize_fun_info(); -void finalize_fun_info(); -} diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index 00e97023bf..c79685a0e9 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -20,7 +20,6 @@ Author: Leonardo de Moura #include "library/type_context.h" #include "library/local_context.h" #include "library/metavar_context.h" -#include "library/fun_info.h" #include "library/check.h" #include "library/profiling.h" #include "library/time_task.h" @@ -58,7 +57,6 @@ void initialize_library_module() { initialize_class(); initialize_library_util(); initialize_pp_options(); - initialize_fun_info(); initialize_abstract_context_cache(); initialize_type_context(); initialize_check(); @@ -70,7 +68,6 @@ void finalize_library_module() { finalize_check(); finalize_type_context(); finalize_abstract_context_cache(); - finalize_fun_info(); finalize_pp_options(); finalize_library_util(); finalize_class(); diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 4452e8cfaf..ecb651ff0e 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -27,7 +27,6 @@ Author: Leonardo de Moura #include "library/type_context.h" #include "library/locals.h" #include "library/aux_recursors.h" -#include "library/fun_info.h" #include "library/num.h" #include "library/check.h" #include "library/aux_match.h"