max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove old fun_info module

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-27 09:21:21 -07:00
parent c841f83c04
commit 95acb5cf3a
6 changed files with 1 additions and 463 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/CMakeLists.txt
View file

@ -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

56
src/library/abstract_context_cache.h
View file

@ -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<expr> 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<fun_info> get_fun_info(transparency_mode, expr const &) = 0;
virtual void set_fun_info(transparency_mode, expr const &, fun_info const &) = 0;
virtual optional<fun_info> 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<unsigned> 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<ss_param_infos> get_subsingleton_info(transparency_mode, expr const &) = 0;
virtual void set_subsingleton_info(transparency_mode, expr const &, ss_param_infos const &) = 0;
virtual optional<ss_param_infos> 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<ss_param_infos> 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<app_builder_info> get_app_builder_info(expr const &, unsigned) = 0;
virtual void set_app_builder_info(expr const &, unsigned, app_builder_info const &) = 0;
virtual optional<app_builder_info> get_app_builder_info(expr const &, list<bool> const &) = 0;
virtual void set_app_builder_info(expr const &, list<bool> 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<expr> 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<fun_info> get_fun_info(transparency_mode, expr const &) override { return optional<fun_info>(); }
virtual void set_fun_info(transparency_mode, expr const &, fun_info const &) override {}
virtual optional<fun_info> get_fun_info_nargs(transparency_mode, expr const &, unsigned) override { return optional<fun_info>(); }
virtual void set_fun_info_nargs(transparency_mode, expr const &, unsigned, fun_info const &) override {}
virtual optional<unsigned> get_specialization_prefix_size(transparency_mode, expr const &, unsigned) override { return optional<unsigned>(); }
virtual void set_specialization_prefix_size(transparency_mode, expr const &, unsigned, unsigned) override {}
virtual optional<ss_param_infos> get_subsingleton_info(transparency_mode, expr const &) override { return optional<ss_param_infos>(); }
virtual void set_subsingleton_info(transparency_mode, expr const &, ss_param_infos const &) override {}
virtual optional<ss_param_infos> get_subsingleton_info_nargs(transparency_mode, expr const &, unsigned) override { return optional<ss_param_infos>(); }
virtual void set_subsingleton_info_nargs(transparency_mode, expr const &, unsigned, ss_param_infos const &) override {}
virtual optional<ss_param_infos> get_specialized_subsingleton_info_nargs(transparency_mode, expr const &, unsigned) override { return optional<ss_param_infos>(); }
virtual void set_specialization_subsingleton_info_nargs(transparency_mode, expr const &, unsigned, ss_param_infos const &) override {}
/* Cache support for app_builder */
virtual optional<app_builder_info> get_app_builder_info(expr const &, unsigned) override { return optional<app_builder_info>(); }
virtual void set_app_builder_info(expr const &, unsigned, app_builder_info const &) override {}
virtual optional<app_builder_info> get_app_builder_info(expr const &, list<bool> const &) override { return optional<app_builder_info>(); }
virtual void set_app_builder_info(expr const &, list<bool> const &, app_builder_info const &) override {}
};
void initialize_abstract_context_cache();

295
src/library/fun_info.cpp
View file

@ -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 <algorithm>
#include <limits>
#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<unsigned> collect_deps(expr const & type, buffer<expr> const & locals, buffer<param_info> & pinfos) {
buffer<unsigned> 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<unsigned> get_core(type_context_old & ctx,
expr const & fn, buffer<param_info> & 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<param_info> pinfos;
auto result_deps = get_core(ctx, e, pinfos, std::numeric_limits<unsigned>::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<param_info> 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<ss_param_info> & 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<bool>(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<ss_param_info> ssinfos;
get_ss_core(ctx, e, ssinfos, std::numeric_limits<unsigned>::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<ss_param_info> 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<param_info> const & pinfos, buffer<ss_param_info> 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<expr> 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<param_info> pinfos;
to_buffer(info.get_params_info(), pinfos);
buffer<ss_param_info> 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<param_info> pinfos;
to_buffer(info.get_params_info(), pinfos);
buffer<ss_param_info> 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<expr> 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<ss_param_info> 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;
}
}

107
src/library/fun_info.h
View file

@ -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<unsigned> m_back_deps; // previous arguments it depends on
public:
param_info(bool imp, bool inst_imp, bool prop, bool has_fwd_deps, list<unsigned> 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<unsigned> 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<param_info> m_params_info;
list<unsigned> m_result_deps; // resulting type dependencies
public:
fun_info():m_arity(0) {}
fun_info(unsigned arity, list<param_info> const & info, list<unsigned> const & result_deps):
m_arity(arity), m_params_info(info), m_result_deps(result_deps) {}
unsigned get_arity() const { return m_arity; }
list<param_info> const & get_params_info() const { return m_params_info; }
list<unsigned> 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_info> ss_param_infos;
list<ss_param_info> get_subsingleton_info(type_context_old & ctx, expr const & fn);
list<ss_param_info> 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<ss_param_info> 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();
}

3
src/library/init_module.cpp
View file

@ -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();

1
src/library/type_context.cpp
View file

@ -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"