michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/fun_info_manager): collect additional information

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-07 11:02:32 -08:00
parent 809168c05b
commit 7d588636a1
2 changed files with 32 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

39
src/library/fun_info_manager.cpp
View file

@ -16,6 +16,23 @@ fun_info_manager::fun_info_manager(type_context & ctx):
m_ctx(ctx) {
}
list<unsigned> fun_info_manager::collect_deps(expr const & e, buffer<expr> const & locals) {
buffer<unsigned> deps;
for_each(e, [&](expr const & e, unsigned) {
if (m_ctx.is_tmp_local(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);
}
return has_local(e); // continue the search only if e has locals
});
std::sort(deps.begin(), deps.end());
return to_list(deps);
}
auto fun_info_manager::get(expr const & e) -> fun_info {
if (auto r = m_fun_info.find(e))
return *r;
@ -28,28 +45,16 @@ auto fun_info_manager::get(expr const & e) -> fun_info {
bool is_prop = m_ctx.is_prop(local_type);
// TODO(Leo): check if the following line is a performance bottleneck.
bool is_sub = is_prop;
bool is_dep = !closed(binding_body(type));
expr new_type = m_ctx.whnf(instantiate(binding_body(type), local));
if (!is_sub)
is_sub = static_cast<bool>(m_ctx.mk_subsingleton_instance(local_type));
buffer<unsigned> deps;
for_each(local_type, [&](expr const & e, unsigned) {
if (m_ctx.is_tmp_local(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);
}
return has_local(e); // continue the search only if e has locals
});
std::sort(deps.begin(), deps.end());
locals.push_back(local);
info.emplace_back(binding_info(type).is_implicit(),
binding_info(type).is_inst_implicit(),
is_prop, is_sub, to_list(deps));
type = m_ctx.whnf(instantiate(binding_body(type), local));
is_prop, is_sub, is_dep, collect_deps(local_type, locals));
type = new_type;
}
fun_info r(info.size(), to_list(info));
fun_info r(info.size(), to_list(info), collect_deps(type, locals));
m_fun_info.insert(e, r);
return r;
}

14
src/library/fun_info_manager.h
View file

@ -14,31 +14,37 @@ class param_info {
unsigned m_inst_implicit:1;
unsigned m_prop:1;
unsigned m_subsingleton:1;
unsigned m_is_dep:1; // true if rest depends on this parameter
list<unsigned> m_deps; // previous arguments it depends on
public:
param_info(bool imp, bool inst_imp, bool prop, bool sub, list<unsigned> const & deps):
m_implicit(imp), m_inst_implicit(inst_imp), m_prop(prop), m_subsingleton(sub), m_deps(deps) {}
param_info(bool imp, bool inst_imp, bool prop, bool sub, bool is_dep, list<unsigned> const & deps):
m_implicit(imp), m_inst_implicit(inst_imp), m_prop(prop), m_subsingleton(sub),
m_is_dep(is_dep), m_deps(deps) {}
list<unsigned> const & get_dependencies() const { return m_deps; }
bool is_prop() const { return m_prop; }
bool is_implicit() const { return m_implicit; }
bool is_inst_implicit() const { return m_inst_implicit; }
bool is_subsingleton() const { return m_subsingleton; }
bool is_dep() const { return m_is_dep; }
};
class fun_info {
unsigned m_arity;
list<param_info> m_params_info;
list<unsigned> m_deps;
public:
fun_info():m_arity(0) {}
fun_info(unsigned arity, list<param_info> const & info):m_arity(arity), m_params_info(info) {}
fun_info(unsigned arity, list<param_info> const & info, list<unsigned> const & deps):
m_arity(arity), m_params_info(info), m_deps(deps) {}
unsigned get_arity() const { return m_arity; }
list<param_info> const & get_params_info() const { return m_params_info; }
list<unsigned> const & get_dependencies() const { return m_deps; }
};
class fun_info_manager {
type_context & m_ctx;
rb_map<expr, fun_info, expr_quick_cmp> m_fun_info;
list<unsigned> collect_deps(expr const & e, buffer<expr> const & locals);
public:
fun_info_manager(type_context & ctx);
type_context & ctx() { return m_ctx; }