feat(frontends/lean/pp): pretty print 'show' expressions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/builtin_exprs.cpp

@@ -25,7 +25,6 @@ static name g_comma(","), g_fact("[fact]"), g_inline("[inline]"), g_from("from")
 static name g_then("then"), g_have("have"), g_by("by"), g_qed("qed");
 static name g_take("take"), g_assume("assume"), g_show("show"), g_fun("fun");
 
-
 static expr parse_Type(parser & p, unsigned, expr const *, pos_info const & pos) {
     if (p.curr_is_token(g_llevel_curly)) {
         p.next();
@@ -394,6 +393,7 @@ parse_table init_led_table() {
     return r;
 }
 }
+bool is_show_aux_name(name const & n) { return n == notation::H_show; }
 
 parse_table get_builtin_nud_table() {
     static optional<parse_table> r;

src/frontends/lean/builtin_exprs.h

@@ -9,4 +9,5 @@ Author: Leonardo de Moura
 namespace lean {
 parse_table get_builtin_nud_table();
 parse_table get_builtin_led_table();
+bool is_show_aux_name(name const & n);
 }

src/frontends/lean/pp.cpp

@@ -17,6 +17,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/pp.h"
 #include "frontends/lean/pp_options.h"
 #include "frontends/lean/token_table.h"
+#include "frontends/lean/builtin_exprs.h"
 
 namespace lean {
 static format g_ellipsis_n_fmt  = highlight(format("\u2026"));
@@ -32,10 +33,11 @@ static format g_arrow_n_fmt     = highlight_keyword(format("\u2192"));
 static format g_arrow_fmt       = highlight_keyword(format("->"));
 static format g_let_fmt         = highlight_keyword(format("let"));
 static format g_in_fmt          = highlight_keyword(format("in"));
+static format g_assign_fmt      = highlight_keyword(format(":="));
 static format g_have_fmt        = highlight_keyword(format("have"));
 static format g_from_fmt        = highlight_keyword(format("from"));
 static format g_fact_fmt        = highlight_keyword(format("[fact]"));
-static format g_assign_fmt      = highlight_keyword(format(":="));
+static format g_show_fmt        = highlight_keyword(format("show"));
 
 name pretty_fn::mk_metavar_name(name const & m) {
     if (auto it = m_purify_meta_table.find(m))
@@ -303,6 +305,12 @@ auto pretty_fn::pp_pi(expr const & e) -> result {
 
 static bool is_let(expr const & e) { return is_app(e) && is_let_annotation(app_fn(e)); }
 static bool is_have(expr const & e) { return is_app(e) && is_have_annotation(app_fn(e)); }
+static bool is_show(expr const & e) {
+    if (!is_let(e))
+        return false;
+    expr b = get_annotation_arg(app_fn(e));
+    return is_show_aux_name(binding_name(b)) && is_var(binding_body(b), 0);
+}
 
 auto pretty_fn::pp_let(expr e) -> result {
     buffer<expr_pair> decls;
@@ -355,6 +363,17 @@ auto pretty_fn::pp_have(expr const & e) -> result {
     return mk_result(r, 0);
 }
 
+auto pretty_fn::pp_show(expr const & e) -> result {
+    expr proof       = app_arg(e);
+    expr binding     = get_annotation_arg(app_fn(e));
+    format type_fmt  = pp_child(binding_domain(binding), 0).first;
+    format proof_fmt = pp_child(proof, 0).first;
+    format r = format{g_show_fmt, space(), nest(5, type_fmt), comma(), space(), g_from_fmt};
+    r = group(r);
+    r += nest(m_indent, compose(line(), proof_fmt));
+    return mk_result(group(r), 0);
+}
+
 auto pretty_fn::pp_macro(expr const & e) -> result {
     // TODO(Leo): have macro annotations
     // fix macro<->pp interface
@@ -372,7 +391,8 @@ auto pretty_fn::pp(expr const & e) -> result {
     m_num_steps++;
 
     if (is_placeholder(e)) return mk_result(g_placeholder_fmt);
-    if (is_let(e)) return pp_let(e);
+    if (is_show(e)) return pp_show(e);
+    if (is_let(e))  return pp_let(e);
     if (is_have(e)) return pp_have(e);
 
     switch (e.kind()) {

src/frontends/lean/pp.h

@@ -67,6 +67,7 @@ private:
     result pp_pi(expr const & e);
     result pp_let(expr e);
     result pp_have(expr const & e);
+    result pp_show(expr const & e);
     result pp_macro(expr const & e);
 
 public:

tests/lean/show1.lean

@@ -0,0 +1,14 @@
+import logic bool tactic
+using bool eq_proofs tactic
+
+variables a b c : bool
+axiom H1 : a = b
+axiom H2 : b = c
+
+check show a = c, from H1 ⬝ H2
+print "------------"
+check have e1 [fact] : a = b, from H1,
+      have e2 : a = c, by apply trans; apply e1; apply H2,
+      have e3 : c = a, from e2⁻¹,
+      have e4 [fact] : b = a, from e1⁻¹,
+      show b = c, from e1⁻¹ ⬝ e2

tests/lean/show1.lean.expected.out

@@ -0,0 +1,8 @@
+show eq a c, from trans H1 H2 : eq a c
+------------
+have e1 [fact] : eq a b, from H1,
+have e2 : eq a c, from trans e1 H2,
+have e3 : eq c a, from symm e2,
+have e4 [fact] : eq b a, from symm e1,
+show eq b c, from trans (symm e1) e2 :
+  eq b c