From 6b1469264de4c8486a8998dcdc26da967ba57bd1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 8 Dec 2015 11:58:03 -0800 Subject: [PATCH] feat(library/trace): add new tracing infrastructure --- src/frontends/lean/parser.cpp | 2 + src/library/CMakeLists.txt | 2 +- src/library/init_module.cpp | 3 + src/library/io_state_stream.cpp | 27 +++++++ src/library/io_state_stream.h | 2 + src/library/trace.cpp | 129 ++++++++++++++++++++++++++++++++ src/library/trace.h | 63 ++++++++++++++++ src/library/unifier.cpp | 8 +- src/util/sexpr/options.cpp | 6 ++ src/util/sexpr/options.h | 2 + 10 files changed, 240 insertions(+), 4 deletions(-) create mode 100644 src/library/trace.cpp create mode 100644 src/library/trace.h diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 0bc1aaf37..1b1c5e3cd 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -20,6 +20,7 @@ Author: Leonardo de Moura #include "kernel/abstract.h" #include "kernel/instantiate.h" #include "kernel/error_msgs.h" +#include "library/trace.h" #include "library/parser_nested_exception.h" #include "library/aliases.h" #include "library/constants.h" @@ -1949,6 +1950,7 @@ void parser::parse_command() { } else { next(); m_local_decls_size_at_beg_cmd = m_local_decls.size(); + scope_trace_env scope(m_env, m_ios); m_env = it->get_fn()(*this); } } else { diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 5412495f5..18a42bc86 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -18,4 +18,4 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp aux_recursors.cpp norm_num.cpp decl_stats.cpp meng_paulson.cpp norm_num.cpp class_instance_resolution.cpp type_context.cpp tmp_type_context.cpp fun_info_manager.cpp congr_lemma_manager.cpp - abstract_expr_manager.cpp light_lt_manager.cpp) + abstract_expr_manager.cpp light_lt_manager.cpp trace.cpp) diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index 68aa6bf23..a6de6a786 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "library/trace.h" #include "library/constants.h" #include "library/unifier.h" #include "library/kernel_serializer.h" @@ -49,6 +50,7 @@ Author: Leonardo de Moura namespace lean { void initialize_library_module() { + initialize_trace(); initialize_constants(); initialize_fingerprint(); initialize_print(); @@ -136,5 +138,6 @@ void finalize_library_module() { finalize_print(); finalize_fingerprint(); finalize_constants(); + finalize_trace(); } } diff --git a/src/library/io_state_stream.cpp b/src/library/io_state_stream.cpp index fbbd29c3e..a9b08757b 100644 --- a/src/library/io_state_stream.cpp +++ b/src/library/io_state_stream.cpp @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "kernel/constraint.h" +#include "kernel/level.h" #include "library/io_state_stream.h" namespace lean { @@ -23,6 +25,31 @@ io_state_stream const & operator<<(io_state_stream const & out, expr const & e) return out; } +io_state_stream const & operator<<(io_state_stream const & out, level const & l) { + out.get_stream() << l; + return out; +} + +io_state_stream const & operator<<(io_state_stream const & out, constraint const & c) { + switch (c.kind()) { + case constraint_kind::Eq: + out << cnstr_lhs_expr(c) << " =?= " << cnstr_rhs_expr(c); + break; + case constraint_kind::LevelEq: + out << cnstr_lhs_level(c) << " =?= " << cnstr_rhs_level(c); + break; + case constraint_kind::Choice: + out << "choice "; + if (cnstr_on_demand(c)) + out << "[on-demand]"; + else if (cnstr_delay_factor(c) != 0) + out << "[delayed:" << cnstr_delay_factor(c) << "] "; + out << cnstr_expr(c); + break; + } + return out; +} + io_state_stream const & operator<<(io_state_stream const & out, ext_exception const & ex) { options const & opts = out.get_options(); out.get_stream() << mk_pair(ex.pp(out.get_formatter()), opts); diff --git a/src/library/io_state_stream.h b/src/library/io_state_stream.h index 60c5700fd..5bf08b99d 100644 --- a/src/library/io_state_stream.h +++ b/src/library/io_state_stream.h @@ -41,6 +41,8 @@ class ext_exception; io_state_stream const & operator<<(io_state_stream const & out, endl_class); io_state_stream const & operator<<(io_state_stream const & out, expr const & e); +io_state_stream const & operator<<(io_state_stream const & out, level const & l); +io_state_stream const & operator<<(io_state_stream const & out, constraint const & c); io_state_stream const & operator<<(io_state_stream const & out, ext_exception const & ex); io_state_stream const & operator<<(io_state_stream const & out, format const & f); template io_state_stream const & display(io_state_stream const & out, T const & t) { diff --git a/src/library/trace.cpp b/src/library/trace.cpp new file mode 100644 index 000000000..e4b04b8a1 --- /dev/null +++ b/src/library/trace.cpp @@ -0,0 +1,129 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include "util/sexpr/option_declarations.h" +#include "kernel/environment.h" +#include "library/io_state.h" +#include "library/trace.h" + +namespace lean { +static name_set * g_trace_classes = nullptr; +static name_map * g_trace_aliases = nullptr; +MK_THREAD_LOCAL_GET_DEF(std::vector, get_enabled_trace_classes); +MK_THREAD_LOCAL_GET_DEF(environment, get_dummy_env); +LEAN_THREAD_PTR(environment, g_env); +LEAN_THREAD_PTR(io_state, g_ios); +LEAN_THREAD_VALUE(unsigned, g_depth, 0); + +void register_trace_class(name const & n) { + register_option(name("trace") + n, BoolOption, "false", "(trace) enable/disable tracing for the given module and submodules"); + g_trace_classes->insert(n); +} + +void register_trace_class_alias(name const & n, name const & alias) { + name_set new_s; + if (auto s = g_trace_aliases->find(n)) + new_s = *s; + new_s.insert(alias); + g_trace_aliases->insert(n, new_s); +} + +bool is_trace_enabled() { + return !get_enabled_trace_classes().empty(); +} + +void enable_trace_class(name const & c) { + std::vector & cs = get_enabled_trace_classes(); + if (std::find(cs.begin(), cs.end(), c) == cs.end()) + cs.push_back(c); +} + +bool is_trace_class_enabled_core(name const & n) { + for (name const & p : get_enabled_trace_classes()) { + if (is_prefix_of(p, n)) + return true; + } + return false; +} + +bool is_trace_class_enabled(name const & n) { + if (!is_trace_enabled()) + return false; + if (is_trace_class_enabled_core(n)) + return true; + if (auto s = g_trace_aliases->find(n)) { + bool found = false; + s->for_each([&](name const & alias) { + if (!found && is_trace_class_enabled_core(alias)) + found = true; + }); + if (found) + return true; + } + return false; +} + +scope_trace_env::scope_trace_env(environment const & env, io_state const & ios) { + m_sz = get_enabled_trace_classes().size(); + m_old_env = g_env; + m_old_ios = g_ios; + g_env = const_cast(&env); + g_ios = const_cast(&ios); + name trace("trace"); + ios.get_options().for_each([&](name const & n) { + if (is_prefix_of(trace, n)) { + name cls = n.replace_prefix(trace, name()); + enable_trace_class(cls); + } + }); +} + +scope_trace_env::~scope_trace_env() { + g_env = const_cast(m_old_env); + g_ios = const_cast(m_old_ios); + get_enabled_trace_classes().resize(m_sz); +} + +void scope_trace_inc_depth::activate() { + lean_assert(!m_active); + m_active = true; + g_depth++; +} + +scope_trace_inc_depth::~scope_trace_inc_depth() { + if (m_active) + g_depth--; +} + +io_state_stream tout() { + if (g_env) { + return diagnostic(*g_env, *g_ios); + } else { + return diagnostic(get_dummy_env(), get_dummy_ios()); + } +} + +io_state_stream const & operator<<(io_state_stream const & ios, tdepth const &) { + ios << g_depth << ". "; + return ios; +} + +io_state_stream const & operator<<(io_state_stream const & ios, tclass const & c) { + ios << "[" << c.m_cls << "] "; + return ios; +} + +void initialize_trace() { + g_trace_classes = new name_set(); + g_trace_aliases = new name_map(); +} + +void finalize_trace() { + delete g_trace_classes; + delete g_trace_aliases; +} +} diff --git a/src/library/trace.h b/src/library/trace.h new file mode 100644 index 000000000..b03756e1a --- /dev/null +++ b/src/library/trace.h @@ -0,0 +1,63 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "library/io_state_stream.h" + +namespace lean { +void register_trace_class(name const & n); +void register_trace_class_alias(name const & n, name const & alias); +bool is_trace_enabled(); +bool is_trace_class_enabled(name const & n); + +class scope_trace_env { + unsigned m_sz; + environment const * m_old_env; + io_state const * m_old_ios; +public: + scope_trace_env(environment const & env, io_state const & ios); + ~scope_trace_env(); +}; + +class scope_trace_inc_depth { + bool m_active{false}; +public: + ~scope_trace_inc_depth(); + void activate(); +}; + +#define lean_trace_inc_depth(CName) \ +scope_trace_inc_depth trace_inc_depth_helper; \ +if (is_trace_enabled() && is_trace_class_enabled(name(CName))) \ + trace_inc_depth_helper.activate(); + +struct tdepth {}; +struct tclass { name m_cls; tclass(name const & c):m_cls(c) {} }; + +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) (is_trace_enabled() && is_trace_class_enabled(name(CName))) + +#define lean_trace_core(CName, CODE) { \ +if (lean_is_trace_class_enabled(CName)) { \ + CODE \ +}} + +#define lean_trace(CName, CODE) { \ +if (lean_is_trace_enabled(CName)) { \ + tout() << tclass(name(CName)); CODE \ +}} + +#define lean_dtrace(CName, CODE) { \ +if (lean_is_trace_enabled(CName)) { \ + tout() << tdepth() << tclass(name(CName)); CODE \ +}} + +void initialize_trace(); +void finalize_trace(); +} diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index bbc94d5db..1efd40a08 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -22,6 +22,7 @@ Author: Leonardo de Moura #include "kernel/type_checker.h" #include "kernel/kernel_exception.h" #include "kernel/error_msgs.h" +#include "library/trace.h" #include "library/normalize.h" #include "library/occurs.h" #include "library/locals.h" @@ -570,7 +571,7 @@ struct unifier_fn { try { auto dcs = m_tc->is_def_eq(t1, t2, j); if (!dcs.first) { - // std::cout << "conflict: " << t1 << " =?= " << t2 << "\n"; + lean_trace("unifier", tout() << "conflict: " << t1 << " =?= " << t2 << "\n";); set_conflict(j); return false; } else { @@ -1215,7 +1216,7 @@ struct unifier_fn { if (in_conflict()) return false; check_full(); - // std::cout << "process: " << c << "\n"; + lean_trace("unifier", tout() << "process: " << c << "\n";); switch (c.kind()) { case constraint_kind::Choice: return preprocess_choice_constraint(c); @@ -2664,7 +2665,7 @@ struct unifier_fn { postpone(c); return true; } - // std::cout << "process_next: " << c << "\n"; + lean_trace("unifier", tout() << "process_next: " << c << "\n";); m_cnstrs.erase_min(); if (is_choice_cnstr(c)) { return process_choice_constraint(c); @@ -2978,6 +2979,7 @@ void open_unifier(lua_State * L) { } void initialize_unifier() { + register_trace_class(name{"unifier"}); g_unifier_max_steps = new name{"unifier", "max_steps"}; g_unifier_normalizer_max_steps = new name{"unifier", "normalizer_max_steps"}; g_unifier_computation = new name{"unifier", "computation"}; diff --git a/src/util/sexpr/options.cpp b/src/util/sexpr/options.cpp index 91dd0b227..0caa053d3 100644 --- a/src/util/sexpr/options.cpp +++ b/src/util/sexpr/options.cpp @@ -200,6 +200,12 @@ format pp(options const & o) { return group(nest(1, open + r + close)); } +void options::for_each(std::function const & fn) const { + ::lean::for_each(m_value, [&](sexpr const & p) { + fn(to_name(head(p))); + }); +} + std::ostream & operator<<(std::ostream & out, options const & o) { bool unicode = get_pp_unicode(o); out << (unicode ? g_left_angle_bracket : "("); diff --git a/src/util/sexpr/options.h b/src/util/sexpr/options.h index b95550db0..984c7d54f 100644 --- a/src/util/sexpr/options.h +++ b/src/util/sexpr/options.h @@ -49,6 +49,8 @@ public: char const * get_string(char const * n, char const * default_value = nullptr) const; sexpr get_sexpr(char const * n, sexpr const & default_value = sexpr()) const; + void for_each(std::function const & fn) const; + options update(name const & n, sexpr const & v) const; template options update(name const & n, T v) const { return update(n, sexpr(v)); } options update(name const & n, unsigned v) const { return update(n, sexpr(static_cast(v))); }