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

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

src/frontends/lean/builtin_exprs.cpp

@@ -264,8 +264,8 @@ static expr parse_have_core(parser & p, pos_info const & pos, optional<expr> con
     }
     // remark: mk_contextual_info(false) informs the elaborator that prop should not occur inside metavariables.
     body = abstract(body, l);
-    expr r = p.save_pos(mk_lambda(id, prop, body, bi), pos);
-    return p.save_pos(mk_have_annotation(p.mk_app(r, proof, pos)), pos);
+    expr r = p.save_pos(mk_have_annotation(p.save_pos(mk_lambda(id, prop, body, bi), pos)), pos);
+    return p.mk_app(r, proof, pos);
 }
 
 static expr parse_have(parser & p, unsigned, expr const *, pos_info const & pos) {

src/frontends/lean/pp.cpp

@@ -32,6 +32,9 @@ 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_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(":="));
 
 name pretty_fn::mk_metavar_name(name const & m) {
@@ -298,9 +301,8 @@ 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_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)); }
 
 auto pretty_fn::pp_let(expr e) -> result {
     buffer<expr_pair> decls;
@@ -332,6 +334,27 @@ auto pretty_fn::pp_let(expr e) -> result {
     return mk_result(r, 0);
 }
 
+auto pretty_fn::pp_have(expr const & e) -> result {
+    expr proof   = app_arg(e);
+    expr binding = get_annotation_arg(app_fn(e));
+    auto p       = binding_body_fresh(binding, true);
+    expr local   = p.second;
+    expr body    = p.first;
+    name const & n = local_pp_name(local);
+    format type_fmt  = pp_child(mlocal_type(local), 0).first;
+    format proof_fmt = pp_child(proof, 0).first;
+    format body_fmt  = pp_child(body, 0).first;
+    format r = format{g_have_fmt, space(), format(n), space()};
+    if (binding_info(binding).is_contextual())
+        r += compose(g_fact_fmt, space());
+    r += format{colon(), nest(m_indent, format{line(), type_fmt, comma(), space(), g_from_fmt})};
+    r = group(r);
+    r += nest(m_indent, compose(line(), compose(proof_fmt, comma())));
+    r = group(r);
+    r += compose(line(), body_fmt);
+    return mk_result(r, 0);
+}
+
 auto pretty_fn::pp_macro(expr const & e) -> result {
     // TODO(Leo): have macro annotations
     // fix macro<->pp interface
@@ -348,10 +371,9 @@ auto pretty_fn::pp(expr const & e) -> result {
     flet<unsigned> let_d(m_depth, m_depth+1);
     m_num_steps++;
 
-    if (is_placeholder(e))
-        return mk_result(g_placeholder_fmt);
-    if (is_let(e))
-        return pp_let(e);
+    if (is_placeholder(e)) return mk_result(g_placeholder_fmt);
+    if (is_let(e)) return pp_let(e);
+    if (is_have(e)) return pp_have(e);
 
     switch (e.kind()) {
     case expr_kind::Var:       return pp_var(e);

src/frontends/lean/pp.h

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

tests/lean/crash.lean.expected.out

@@ -1,5 +1,6 @@
 crash.lean:8:12: error: type mismatch at application
-  (λ (H' : not P), _) H
+  have H' : not P, from H,
+  _
 expected type:
   not P
 given type:

tests/lean/have1.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 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⁻¹,
+      have e5 : b = c, from e4 ⬝ e2,
+      have e6 : a = a, from H1 ⬝ H2 ⬝ H2⁻¹ ⬝ H1⁻¹ ⬝ H1 ⬝ H2 ⬝ H2⁻¹ ⬝ H1⁻¹,
+      e3 ⬝ e2

tests/lean/have1.lean.expected.out

@@ -0,0 +1,9 @@
+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,
+have e5 : eq b c, from trans e4 e2,
+have e6 : eq a a, from
+  trans H1 (trans H2 (trans (symm H2) (trans (symm H1) (trans H1 (trans H2 (trans (symm H2) (symm H1))))))),
+trans e3 e2 :
+  eq c c