From e16dbac0dbd57a4e0e52f4dfaa473fc1c3fe5ab2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 28 Jun 2016 11:45:56 +0100
Subject: [PATCH] feat(frontends/lean): add declare_trace command

It allows users to define their own tracing classes.
---
 src/emacs/lean-syntax.el            |  3 +--
 src/frontends/lean/builtin_cmds.cpp | 20 ++++++++++++++++++++
 src/frontends/lean/token_table.cpp  |  2 +-
 tests/lean/trace2.lean              | 20 ++++++++++++++++++++
 tests/lean/trace2.lean.expected.out |  3 +++
 5 files changed, 45 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/trace2.lean
 create mode 100644 tests/lean/trace2.lean.expected.out

diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index af1a0c031b..cf2f21fbf9 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -13,9 +13,8 @@
     "hypothesis" "lemma" "corollary" "variable" "variables" "premise" "premises" "theory"
     "print" "theorem" "proposition" "example" "abbreviation" "abstract"
     "open" "as" "export" "override" "axiom" "axioms" "inductive" "with" "structure" "record" "universe" "universes"
-    "alias" "help" "precedence" "reserve"
+    "alias" "help" "precedence" "reserve" "declare_trace"
     "match" "infix" "infixl" "infixr" "notation" "postfix" "prefix"
-    "tactic_infix" "tactic_infixl" "tactic_infixr" "tactic_notation" "tactic_postfix" "tactic_prefix"
     "eval" "vm_eval" "check" "end" "reveal" "this" "suppose"
     "using" "namespace" "section" "fields" "find_decl"
     "attribute" "local" "set_option" "extends" "include" "omit" "classes"
diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 7b7f2ba3ab..0fd2cbc896 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -691,6 +691,22 @@ static environment elab_cmd(parser & p) {
     return p.env();
 }
 
+static std::string * g_declare_trace_key = nullptr;
+
+environment declare_trace_cmd(parser & p) {
+    name cls = p.check_id_next("invalid declare_trace command, identifier expected");
+    register_trace_class(cls);
+    return module::add(p.env(), *g_declare_trace_key, [=](environment const &, serializer & s) { s << cls; });
+}
+
+static void declare_trace_reader(deserializer & d, shared_environment &,
+                                 std::function<void(asynch_update_fn const &)> &,
+                                 std::function<void(delayed_update_fn const &)> &) {
+    name cls;
+    d >> cls;
+    register_trace_class(cls);
+}
+
 void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("open",              "create aliases for declarations, and use objects defined in other namespaces",
                         open_cmd));
@@ -712,6 +728,7 @@ void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("help",              "brief description of available commands and options", help_cmd));
     add_cmd(r, cmd_info("init_quotient",     "initialize quotient type computational rules", init_quotient_cmd));
     add_cmd(r, cmd_info("init_hits",         "initialize builtin HITs", init_hits_cmd));
+    add_cmd(r, cmd_info("declare_trace",     "declare a new trace class (for debugging Lean tactics)", declare_trace_cmd));
     add_cmd(r, cmd_info("#erase_cache",      "erase cached definition (for debugging purposes)", erase_cache_cmd));
     add_cmd(r, cmd_info("#normalizer",       "(for debugging purposes)", normalizer_cmd));
     add_cmd(r, cmd_info("#unify",            "(for debugging purposes)", unify_cmd));
@@ -735,9 +752,12 @@ cmd_table get_builtin_cmds() {
 void initialize_builtin_cmds() {
     g_cmds = new cmd_table();
     init_cmd_table(*g_cmds);
+    g_declare_trace_key = new std::string("decl_trace");
+    register_module_object_reader(*g_declare_trace_key, declare_trace_reader);
 }
 
 void finalize_builtin_cmds() {
     delete g_cmds;
+    delete g_declare_trace_key;
 }
 }
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 550539cf08..6ed7adf165 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -118,7 +118,7 @@ void init_token_table(token_table & t) {
          "exit", "set_option", "open", "export", "override", "tactic_hint",
          "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class",
          "multiple_instances", "find_decl", "attribute", "persistent", "inline",
-         "include", "omit", "migrate", "init_quotient", "init_hits", "#erase_cache",
+         "include", "omit", "migrate", "init_quotient", "init_hits", "declare_trace", "#erase_cache",
          "#compile", "#simplify", "#normalizer", "#unify", "#elab", "#compile", nullptr};
 
     pair<char const *, char const *> aliases[] =
diff --git a/tests/lean/trace2.lean b/tests/lean/trace2.lean
new file mode 100644
index 0000000000..1610fbfc88
--- /dev/null
+++ b/tests/lean/trace2.lean
@@ -0,0 +1,20 @@
+open tactic
+
+declare_trace foo.bla
+
+example : true :=
+by do
+  when_tracing ("foo" <.> "bla") $ do {
+    trace "hello",
+    trace "world" },
+  constructor
+
+set_option trace.foo.bla true
+print "------------"
+
+example : true :=
+by do
+  when_tracing ("foo" <.> "bla") $ do {
+    trace "hello",
+    trace "world" },
+  constructor
diff --git a/tests/lean/trace2.lean.expected.out b/tests/lean/trace2.lean.expected.out
new file mode 100644
index 0000000000..65b0c43b02
--- /dev/null
+++ b/tests/lean/trace2.lean.expected.out
@@ -0,0 +1,3 @@
+------------
+hello
+world