feat: add trace! macro

src/frontends/lean/builtin_exprs.cpp

@@ -812,6 +812,15 @@ static expr parse_panic(parser & p, unsigned, expr const *, pos_info const & pos
     return save_pos(r, pos);
 }
 
+static expr parse_trace(parser & p, unsigned, expr const *, pos_info const & pos) {
+    expr k = p.parse_expr(get_max_prec());
+    expr e = p.parse_expr(get_max_prec());
+    expr m = mk_constant(get_lean_message_data_name());
+    e = mk_typed_expr(m, e);
+    expr r = mk_app(mk_constant(get_lean_monad_tracer_trace_name()), k, mk_lambda("_", mk_unit(), e, binder_info()));
+    return save_pos(r, pos);
+}
+
 parse_table init_nud_table() {
     action Expr(mk_expr_action());
     action Skip(mk_skip_action());
@@ -849,6 +858,7 @@ parse_table init_nud_table() {
     r = r.add({transition("parser!", mk_ext_action(parse_lparser))}, x0);
     r = r.add({transition("tparser!", mk_ext_action(parse_tparser))}, x0);
     r = r.add({transition("panic!", mk_ext_action(parse_panic))}, x0);
+    r = r.add({transition("trace!", mk_ext_action(parse_trace))}, x0);
     return r;
 }
 

src/frontends/lean/token_table.cpp

@@ -96,7 +96,7 @@ void init_token_table(token_table & t) {
          {"@@", g_max_prec}, {"@", g_max_prec}, {"@&", g_max_prec},
          {"sorry", g_max_prec}, {"+", g_plus_prec}, {"->", g_arrow_prec}, {"<-", 0},
          {"match", 0}, {"nomatch", 0}, {"^.", g_max_prec+1}, {"::", 67},
-         {"renaming", 0}, {"extends", 0}, {"parser!", g_max_prec}, {"tparser!", g_max_prec}, {"panic!", g_max_prec}, {nullptr, 0}};
+         {"renaming", 0}, {"extends", 0}, {"parser!", g_max_prec}, {"tparser!", g_max_prec}, {"panic!", g_max_prec}, {"trace!", g_max_prec}, {nullptr, 0}};
 
     char const * commands[] =
         {"theorem", "axiom", "variable", "protected", "private", "hide",

src/library/constants.cpp

@@ -56,6 +56,8 @@ name const * g_eq_false_intro = nullptr;
 name const * g_eq_self_iff_true = nullptr;
 name const * g_lean_level = nullptr;
 name const * g_lean_expr = nullptr;
+name const * g_lean_message_data = nullptr;
+name const * g_lean_monad_tracer_trace = nullptr;
 name const * g_false = nullptr;
 name const * g_false_of_true_iff_false = nullptr;
 name const * g_false_of_true_eq_false = nullptr;
@@ -242,6 +244,8 @@ void initialize_constants() {
     g_eq_self_iff_true = new name{"eqSelfIffTrue"};
     g_lean_level = new name{"Lean", "Level"};
     g_lean_expr = new name{"Lean", "Expr"};
+    g_lean_message_data = new name{"Lean", "MessageData"};
+    g_lean_monad_tracer_trace = new name{"Lean", "MonadTracer", "trace"};
     g_false = new name{"False"};
     g_false_of_true_iff_false = new name{"falseOfTrueIffFalse"};
     g_false_of_true_eq_false = new name{"falseOfTrueEqFalse"};
@@ -429,6 +433,8 @@ void finalize_constants() {
     delete g_eq_self_iff_true;
     delete g_lean_level;
     delete g_lean_expr;
+    delete g_lean_message_data;
+    delete g_lean_monad_tracer_trace;
     delete g_false;
     delete g_false_of_true_iff_false;
     delete g_false_of_true_eq_false;
@@ -615,6 +621,8 @@ name const & get_eq_false_intro_name() { return *g_eq_false_intro; }
 name const & get_eq_self_iff_true_name() { return *g_eq_self_iff_true; }
 name const & get_lean_level_name() { return *g_lean_level; }
 name const & get_lean_expr_name() { return *g_lean_expr; }
+name const & get_lean_message_data_name() { return *g_lean_message_data; }
+name const & get_lean_monad_tracer_trace_name() { return *g_lean_monad_tracer_trace; }
 name const & get_false_name() { return *g_false; }
 name const & get_false_of_true_iff_false_name() { return *g_false_of_true_iff_false; }
 name const & get_false_of_true_eq_false_name() { return *g_false_of_true_eq_false; }

src/library/constants.h

@@ -58,6 +58,8 @@ name const & get_eq_false_intro_name();
 name const & get_eq_self_iff_true_name();
 name const & get_lean_level_name();
 name const & get_lean_expr_name();
+name const & get_lean_message_data_name();
+name const & get_lean_monad_tracer_trace_name();
 name const & get_false_name();
 name const & get_false_of_true_iff_false_name();
 name const & get_false_of_true_eq_false_name();

src/library/constants.txt

@@ -51,6 +51,8 @@ eqFalseIntro
 eqSelfIffTrue
 Lean.Level
 Lean.Expr
+Lean.MessageData
+Lean.MonadTracer.trace
 False
 falseOfTrueIffFalse
 falseOfTrueEqFalse

tests/lean/run/trace.lean

@@ -14,14 +14,14 @@ instance : SimpleMonadTracerAdapter M :=
   modifyTraceState := fun f => modify $ fun s => { traceState := f s.traceState, .. s } }
 
 def tst1 : M Unit :=
-do trace `module (fun _ => ("hello" ++ MessageData.nest 9 (Format.line ++ "world" : MessageData)));
-   trace `module.aux (fun _ => ("another message" : MessageData));
+do trace! `module ("hello" ++ MessageData.nest 9 (Format.line ++ "world"));
+   trace! `module.aux "another message";
    pure ()
 
 def tst2 (b : Bool) : M Unit :=
 traceCtx `module $ fun _ => do
   tst1;
-  trace `bughunt (fun _ => ("at test2" : MessageData));
+  trace! `bughunt "at test2";
   when b $ throw "error";
   tst1;
   pure ()