From f88561ae68aeda96e8d310b587efd00d57357400 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 22 Oct 2019 16:08:37 -0700 Subject: [PATCH] feat: add `trace!` macro --- src/frontends/lean/builtin_exprs.cpp | 10 ++++++++++ src/frontends/lean/token_table.cpp | 2 +- src/library/constants.cpp | 8 ++++++++ src/library/constants.h | 2 ++ src/library/constants.txt | 2 ++ tests/lean/run/trace.lean | 6 +++--- 6 files changed, 26 insertions(+), 4 deletions(-) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index d965eaa119..b24afc9b84 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/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; } diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index d333b9228e..671b24ca51 100644 --- a/src/frontends/lean/token_table.cpp +++ b/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", diff --git a/src/library/constants.cpp b/src/library/constants.cpp index d04635c624..41f4043db6 100644 --- a/src/library/constants.cpp +++ b/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; } diff --git a/src/library/constants.h b/src/library/constants.h index 8f741db256..c2b9f162c9 100644 --- a/src/library/constants.h +++ b/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(); diff --git a/src/library/constants.txt b/src/library/constants.txt index 7140527c08..2bf2e3ab47 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -51,6 +51,8 @@ eqFalseIntro eqSelfIffTrue Lean.Level Lean.Expr +Lean.MessageData +Lean.MonadTracer.trace False falseOfTrueIffFalse falseOfTrueEqFalse diff --git a/tests/lean/run/trace.lean b/tests/lean/run/trace.lean index dabd3480fa..aea4f23f17 100644 --- a/tests/lean/run/trace.lean +++ b/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 ()