feat(library/trace): add new tracing infrastructure

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 {

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)

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

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

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<typename T> io_state_stream const & display(io_state_stream const & out, T const & t) {

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 <vector>
+#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<name_set>  * g_trace_aliases = nullptr;
+MK_THREAD_LOCAL_GET_DEF(std::vector<name>, 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<name> & 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<environment*>(&env);
+    g_ios     = const_cast<io_state*>(&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<environment*>(m_old_env);
+    g_ios = const_cast<io_state*>(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<name_set>();
+}
+
+void finalize_trace() {
+    delete g_trace_classes;
+    delete g_trace_aliases;
+}
+}

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();
+}

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"};

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<void(name const &)> 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 : "(");

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<void(name const &)> const & fn) const;
+
     options update(name const & n, sexpr const & v) const;
     template<typename T> 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<int>(v))); }