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

feat(library/type_context): use new tracing infrastructure in new type class resolution procedure

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-08 14:34:20 -08:00
parent 9b69ccd2f8
commit 58ab526d44
5 changed files with 46 additions and 64 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/class_instance_resolution.cpp
View file

@ -225,6 +225,10 @@ void finalize_class_instance_resolution() {
(p : x = y) : (is_equiv (transport P p)) := ...
*/
static bool get_class_trace_instances(options const & o) {
return o.get_bool(name("trace", "class_instances"), false);
}
/** \brief Context for handling class-instance metavariable choice constraint */
struct class_instance_context {
io_state m_ios;

14
src/library/trace.cpp
View file

@ -101,19 +101,21 @@ scope_trace_inc_depth::~scope_trace_inc_depth() {
g_depth--;
}
scope_trace_init_bool_option::scope_trace_init_bool_option(name const & n, bool v) {
void scope_trace_init_bool_option::init(name const & n, bool v) {
m_old_ios = g_ios;
if (g_env && g_ios) {
m_tmp_ios = *g_ios;
options o = m_tmp_ios.get_options();
m_tmp_ios.reset(new io_state(*g_ios));
options o = m_tmp_ios->get_options();
o = o.update_if_undef(n, v);
m_tmp_ios.set_options(o);
g_ios = &m_tmp_ios;
m_tmp_ios->set_options(o);
g_ios = m_tmp_ios.get();
}
}
scope_trace_init_bool_option::~scope_trace_init_bool_option() {
g_ios = const_cast<io_state*>(m_old_ios);
if (m_tmp_ios) {
g_ios = const_cast<io_state*>(m_old_ios);
}
}
io_state_stream tout() {

35
src/library/trace.h
View file

@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include <memory>
#include "library/io_state_stream.h"
namespace lean {
@ -13,6 +14,8 @@ void register_trace_class_alias(name const & n, name const & alias);
bool is_trace_enabled();
bool is_trace_class_enabled(name const & n);
#define lean_is_trace_enabled(CName) (::lean::is_trace_enabled() && ::lean::is_trace_class_enabled(CName))
class scope_trace_env {
unsigned m_sz;
environment const * m_old_env;
@ -29,19 +32,29 @@ public:
void activate();
};
/* Temporarily set an option if it is not already set in the trace environment. */
class scope_trace_init_bool_option {
io_state const * m_old_ios;
io_state m_tmp_ios;
public:
scope_trace_init_bool_option(name const & n, bool v);
~scope_trace_init_bool_option();
};
#define LEAN_MERGE_(a,b) a##b
#define LEAN_LABEL_(a) LEAN_MERGE_(unique_name_, a)
#define LEAN_UNIQUE_NAME LEAN_LABEL_(__LINE__)
#define lean_trace_inc_depth(CName) \
scope_trace_inc_depth trace_inc_depth_helper ## __LINE__; \
scope_trace_inc_depth LEAN_UNIQUE_NAME; \
if (is_trace_enabled() && is_trace_class_enabled(name(CName))) \
trace_inc_depth_helper ## __LINE__.activate();
LEAN_UNIQUE_NAME.activate();
/* Temporarily set an option if it is not already set in the trace environment. */
class scope_trace_init_bool_option {
io_state const * m_old_ios{nullptr};
std::unique_ptr<io_state> m_tmp_ios;
public:
~scope_trace_init_bool_option();
void init(name const & opt, bool val);
};
#define lean_trace_init_bool(CName, Opt, Val) \
scope_trace_init_bool_option LEAN_UNIQUE_NAME; \
if (lean_is_trace_enabled(CName)) { \
LEAN_UNIQUE_NAME.init(Opt, Val); \
}
struct tdepth {};
struct tclass { name m_cls; tclass(name const & c):m_cls(c) {} };
@ -50,8 +63,6 @@ io_state_stream tout();
io_state_stream const & operator<<(io_state_stream const & ios, tdepth const &);
io_state_stream const & operator<<(io_state_stream const & ios, tclass const &);
#define lean_is_trace_enabled(CName) (::lean::is_trace_enabled() && ::lean::is_trace_class_enabled(CName))
#define lean_trace_plain(CName, CODE) { \
if (lean_is_trace_enabled(CName)) { \
CODE \

54
src/library/type_context.cpp
View file

@ -13,6 +13,7 @@ Author: Leonardo de Moura
#include "kernel/for_each_fn.h"
#include "kernel/inductive/inductive.h"
#include "library/trace.h"
#include "library/util.h"
#include "library/projection.h"
#include "library/normalize.h"
#include "library/replace_visitor.h"
@ -23,10 +24,6 @@ Author: Leonardo de Moura
#include "library/class.h"
#include "library/constants.h"
#ifndef LEAN_DEFAULT_CLASS_TRACE_INSTANCES
#define LEAN_DEFAULT_CLASS_TRACE_INSTANCES false
#endif
#ifndef LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH
#define LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH 32
#endif
@ -37,14 +34,9 @@ Author: Leonardo de Moura
namespace lean {
static name * g_prefix = nullptr;
static name * g_class_trace_instances = nullptr;
static name * g_class_instance_max_depth = nullptr;
static name * g_class_trans_instances = nullptr;
bool get_class_trace_instances(options const & o) {
return o.get_bool(*g_class_trace_instances, LEAN_DEFAULT_CLASS_TRACE_INSTANCES);
}
unsigned get_class_instance_max_depth(options const & o) {
return o.get_unsigned(*g_class_instance_max_depth, LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH);
}
@ -110,7 +102,6 @@ struct type_context::ext_ctx : public extension_context {
type_context::type_context(environment const & env, io_state const & ios, tmp_local_generator * gen,
bool gen_owner, bool multiple_instances):
m_env(env),
m_ios(ios),
m_ngen(*g_prefix),
m_ext_ctx(new ext_ctx(*this)),
m_local_gen(gen),
@ -124,7 +115,6 @@ type_context::type_context(environment const & env, io_state const & ios, tmp_lo
// TODO(Leo): use compilation options for setting config
m_ci_max_depth = 32;
m_ci_trans_instances = true;
m_ci_trace_instances = false;
update_options(ios.get_options());
}
@ -1371,34 +1361,22 @@ bool type_context::update_options(options const & opts) {
options o = opts;
unsigned max_depth = get_class_instance_max_depth(o);
bool trans_instances = get_class_trans_instances(o);
bool trace_instances = get_class_trace_instances(o);
if (trace_instances) {
o = o.update_if_undef(get_pp_purify_metavars_name(), false);
o = o.update_if_undef(get_pp_implicit_name(), true);
}
bool r = true;
if (m_ci_max_depth != max_depth ||
m_ci_trans_instances != trans_instances ||
m_ci_trace_instances != trace_instances) {
m_ci_trans_instances != trans_instances) {
r = false;
}
m_ci_max_depth = max_depth;
m_ci_trans_instances = trans_instances;
m_ci_trace_instances = trace_instances;
m_ios.set_options(o);
return r;
}
[[ noreturn ]] static void throw_class_exception(char const * msg, expr const & m) { throw_generic_exception(msg, m); }
io_state_stream type_context::diagnostic() {
return lean::diagnostic(m_env, m_ios);
}
void type_context::trace(unsigned depth, expr const & mvar, expr const & mvar_type, expr const & r) {
lean_assert(m_ci_trace_instances);
auto out = diagnostic();
auto out = tout();
if (!m_ci_displayed_trace_header && m_ci_choices.size() == m_ci_choices_ini_sz + 1) {
out << tclass("class_instances");
if (m_pip) {
if (auto fname = m_pip->get_file_name()) {
out << fname << ":";
@ -1409,10 +1387,7 @@ void type_context::trace(unsigned depth, expr const & mvar, expr const & mvar_ty
out << " class-instance resolution trace" << endl;
m_ci_displayed_trace_header = true;
}
for (unsigned i = 0; i < depth; i++)
out << " ";
if (depth > 0)
out << "[" << depth << "] ";
out << tclass("class_instances") << "(" << depth << ") ";
out << mvar << " : " << instantiate_uvars_mvars(mvar_type) << " := " << r << endl;
}
@ -1446,9 +1421,7 @@ bool type_context::try_instance(ci_stack_entry const & e, expr const & inst, exp
r = mk_app(r, new_arg);
type = instantiate(binding_body(type), new_arg);
}
if (m_ci_trace_instances) {
trace(e.m_depth, mk_app(mvar, locals), mvar_type, r);
}
lean_trace_plain("class_instances", trace(e.m_depth, mk_app(mvar, locals), mvar_type, r););
if (!is_def_eq(mvar_type, type)) {
return false;
}
@ -1504,7 +1477,7 @@ bool type_context::mk_choice_point(expr const & mvar) {
throw_class_exception("maximum class-instance resolution depth has been reached "
"(the limit can be increased by setting option 'class.instance_max_depth') "
"(the class-instance resolution trace can be visualized "
"by setting option 'class.trace_instances')",
"by setting option 'trace.class_instances')",
infer(m_ci_main_mvar));
}
// Remark: we initially tried to reject branches where mvar_type contained unassigned metavariables.
@ -1675,9 +1648,7 @@ optional<expr> type_context::ensure_no_meta(optional<expr> r) {
optional<expr> type_context::mk_class_instance_core(expr const & type) {
if (auto r = check_ci_cache(type)) {
if (m_ci_trace_instances) {
diagnostic() << "cached instance for " << type << "\n" << *r << "\n";
}
lean_trace("class_instances", tout() << "cached instance for " << type << "\n" << *r << "\n";);
return r;
}
init_search(type);
@ -1697,6 +1668,8 @@ void type_context::restore_choices(unsigned old_sz) {
optional<expr> type_context::mk_class_instance(expr const & type) {
m_ci_choices.clear();
ci_choices_scope scope(*this);
lean_trace_init_bool("class_instances", get_pp_purify_metavars_name(), false);
lean_trace_init_bool("class_instances", get_pp_implicit_name(), true);
m_ci_displayed_trace_header = false;
auto r = mk_class_instance_core(type);
if (r)
@ -1962,15 +1935,11 @@ normalizer::normalizer(type_context & ctx, bool eta, bool nested_prop):
void initialize_type_context() {
g_prefix = new name(name::mk_internal_unique_name());
g_class_trace_instances = new name{"class", "trace_instances"};
register_trace_class("class_instances");
g_class_instance_max_depth = new name{"class", "instance_max_depth"};
g_class_trans_instances = new name{"class", "trans_instances"};
register_bool_option(*g_class_trace_instances, LEAN_DEFAULT_CLASS_TRACE_INSTANCES,
"(class) display messages showing the class-instances resolution execution trace");
register_unsigned_option(*g_class_instance_max_depth, LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH,
"(class) max allowed depth in class-instance resolution");
register_bool_option(*g_class_trans_instances, LEAN_DEFAULT_CLASS_TRANS_INSTANCES,
"(class) use automatically derived instances from the transitive closure of "
"the structure instance graph");
@ -1978,7 +1947,6 @@ void initialize_type_context() {
void finalize_type_context() {
delete g_prefix;
delete g_class_trace_instances;
delete g_class_instance_max_depth;
delete g_class_trans_instances;
}

3
src/library/type_context.h
View file

@ -13,7 +13,6 @@ Author: Leonardo de Moura
#include "library/projection.h"
namespace lean {
bool get_class_trace_instances(options const & o);
unsigned get_class_instance_max_depth(options const & o);
bool get_class_trans_instances(options const & o);
@ -119,7 +118,6 @@ class type_context {
struct ext_ctx;
friend struct ext_ctx;
environment m_env;
io_state m_ios;
name_generator m_ngen;
std::unique_ptr<ext_ctx> m_ext_ctx;
tmp_local_generator * m_local_gen;
@ -271,7 +269,6 @@ class type_context {
bool m_ci_trans_instances;
bool m_ci_trace_instances;
io_state_stream diagnostic();
optional<name> constant_is_class(expr const & e);
optional<name> is_full_class(expr type);
lbool is_quick_class(expr const & type, name & result);