From 58ab526d44a7026fee68e3daa263068668502a5f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 8 Dec 2015 14:34:20 -0800 Subject: [PATCH] feat(library/type_context): use new tracing infrastructure in new type class resolution procedure --- src/library/class_instance_resolution.cpp | 4 ++ src/library/trace.cpp | 14 +++--- src/library/trace.h | 35 ++++++++++----- src/library/type_context.cpp | 54 +++++------------------ src/library/type_context.h | 3 -- 5 files changed, 46 insertions(+), 64 deletions(-) diff --git a/src/library/class_instance_resolution.cpp b/src/library/class_instance_resolution.cpp index 4b00a294b..15db6a3c2 100644 --- a/src/library/class_instance_resolution.cpp +++ b/src/library/class_instance_resolution.cpp @@ -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; diff --git a/src/library/trace.cpp b/src/library/trace.cpp index cdf67f73a..44c6d43f5 100644 --- a/src/library/trace.cpp +++ b/src/library/trace.cpp @@ -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(m_old_ios); + if (m_tmp_ios) { + g_ios = const_cast(m_old_ios); + } } io_state_stream tout() { diff --git a/src/library/trace.h b/src/library/trace.h index 5f8b77fc1..bfb4e8e2b 100644 --- a/src/library/trace.h +++ b/src/library/trace.h @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once +#include #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 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 \ diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 216774b7d..80b940e7e 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -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 type_context::ensure_no_meta(optional r) { optional 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 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; } diff --git a/src/library/type_context.h b/src/library/type_context.h index d3dfe0217..3f823d84d 100644 --- a/src/library/type_context.h +++ b/src/library/type_context.h @@ -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 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 constant_is_class(expr const & e); optional is_full_class(expr type); lbool is_quick_class(expr const & type, name & result);