fix(frontends/lean/pp): hide proof terms in non-proofs by default

This is mainly to reduce clutter.  Proof term printing can still be
forced using the `pp.proofs` option.

src/frontends/lean/pp.cpp

@@ -1608,30 +1608,6 @@ static bool is_pp_atomic(expr const & e) {
     }
 }
 
-/* Returns the theorem type if `e` is a proof and `m_proofs` is set to false. */
-optional<expr> pretty_fn::is_proof(expr const & e) {
-    if (m_proofs)
-        return none_expr(); // showing proof terms
-    if (!closed(e))
-        // the Lean type checker assumes expressions are closed.
-        return none_expr();
-    try {
-        expr t = m_ctx.infer(e);
-        if (is_prop(t))
-            return some_expr(head_beta_reduce(t));
-        else
-            return none_expr();
-    } catch (exception &) {
-        return none_expr();
-    }
-}
-
-auto pretty_fn::pp_proof_type(expr const & t) -> result {
-    format li = m_unicode ? format("⌞") : format("[proof ");
-    format ri = m_unicode ? format("⌟") : format("]");
-    return result(group(nest(1, li + pp(t).fmt() + ri)));
-}
-
 static bool is_subtype(expr const & e) {
     return
         is_constant(get_app_fn(e), get_subtype_name()) &&
@@ -1771,9 +1747,11 @@ auto pretty_fn::pp(expr const & e, bool ignore_hide) -> result {
         if (auto r = to_string(e))      return pp_string_literal(*r);
         if (auto r = to_char(m_ctx, e)) return pp_char_literal(*r);
     }
-    if (auto t = is_proof(e)) {
-        return pp_proof_type(*t);
-    }
+    try {
+        if (!m_proofs && !is_constant(e) && !is_mlocal(e) && closed(e) && is_prop(m_ctx.infer(e))) {
+            return result(format("_"));
+        }
+    } catch (exception) {}
 
     if (auto r = pp_notation(e))
         return *r;
@@ -1896,12 +1874,18 @@ std::pair<bool, token_table const *> pretty_fn::needs_space_sep(token_table cons
 }
 
 format pretty_fn::operator()(expr const & e) {
+    auto purified = purify(m_beta ? pp_beta_reduce_fn()(e) : e);
+
+    if (!m_options.contains(get_pp_proofs_name()) && !get_pp_all(m_options)) {
+        try {
+            m_proofs = !closed(purified) || is_prop(m_ctx.infer(purified));
+        } catch (exception) {
+            m_proofs = true;
+        }
+    }
+
     m_depth = 0; m_num_steps = 0;
-    result r;
-    if (m_beta)
-        r = pp_child(purify(pp_beta_reduce_fn()(e)), 0);
-    else
-        r = pp_child(purify(e), 0);
+    result r = pp_child(purified, 0);
 
     // insert spaces so that lexing the result round-trips
     std::function<bool(sexpr const &, sexpr const &)> sep; // NOLINT

src/frontends/lean/pp.h

@@ -89,7 +89,6 @@ private:
     expr purify(expr const & e);
     bool is_implicit(expr const & f);
     bool is_default_arg_app(expr const & e);
-    optional<expr> is_proof(expr const & f);
     bool is_prop(expr const & e);
     bool has_implicit_args(expr const & f);
     optional<name> is_aliased(name const & n) const;
@@ -146,7 +145,6 @@ private:
     result pp_let(expr e);
     result pp_num(mpz const & n);
     result pp_prod(expr const & e);
-    result pp_proof_type(expr const & t);
     void set_options_core(options const & o);
 
     expr infer_type(expr const & e);

tests/lean/anc1.lean.expected.out

@@ -1,7 +1,7 @@
 (1, 2) : ℕ × ℕ
 and.intro trivial trivial : true ∧ true
 anc1.lean:5:0: warning: declaration '[anonymous]' uses sorry
-⟨1, sorry⟩ : Σ' (x : ℕ), x > 0
+⟨1, _⟩ : Σ' (x : ℕ), x > 0
 show true, from true.intro : true
 Exists.intro 1 (id_locked (λ (a : 1 = 0), nat.no_confusion a)) : ∃ (x : ℕ), 1 ≠ 0
 λ (A B C : Prop) (Ha : A) (Hb : B) (Hc : C), show B ∧ A, from and.intro Hb Ha :

tests/lean/defeq_simp2.lean.expected.out

@@ -1,4 +1,4 @@
-f a (foo1 a) = f a (foo2 a)
-f a (foo1 a) = f a (foo2 a)
-f a (foo1 a) = f a (foo2 a)
-(λ (x : ℕ), f x (foo1 x)) = λ (x : ℕ), f x (foo2 x)
+f a _ = f a _
+f a _ = f a _
+f a _ = f a _
+(λ (x : ℕ), f x _) = λ (x : ℕ), f x _

tests/lean/pp_char_bug.lean.expected.out

@@ -1,5 +1,5 @@
-⟨2, of_as_true trivial⟩ : fin 5
-⟨1, of_as_true trivial⟩ : fin 3
+⟨2, _⟩ : fin 5
+⟨1, _⟩ : fin 3
 'a' : char
 to_string 'a' : string
 "a"

tests/lean/pp_no_proofs.lean.expected.out

@@ -1,4 +1,4 @@
-f (Ps (Ps (Ps (Ps (Ps (Ps P0))))))
-f ⌞P 6⌟
-@f 6 ⌞@P ⌞true⌟ 6⌟
+f _
+f _
+@f 6 _
 @f 6 (@Ps 5 (@Ps 4 (@Ps 3 (@Ps 2 (@Ps 1 (@Ps 0 P0))))))

tests/lean/task.lean.expected.out

@@ -1,4 +1,3 @@
 trace message from a different task
 def foo : Π {α : Type u} {n : ℕ}, vector α (0 + n) → vector α n :=
-λ {α : Type u} {n : ℕ},
-  ite (n = 0) (λ (v : vector α (0 + n)), cast (foo._aux_1 v) v) (λ (v : vector α (0 + n)), cast (foo._aux_2 v) v)
+λ {α : Type u} {n : ℕ}, ite (n = 0) (λ (v : vector α (0 + n)), cast _ v) (λ (v : vector α (0 + n)), cast _ v)

tests/lean/uni_bug1.lean.expected.out

@@ -1 +1 @@
-f 1 0 (Rtrue ((1, 0).fst) 0) : ℕ
+f 1 0 _ : ℕ