From 9367e94900215281b2f9b8039400ee5866bee0ea Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Sat, 15 Jul 2017 22:21:22 +0100 Subject: [PATCH] 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 | 48 ++++++++--------------- src/frontends/lean/pp.h | 2 - tests/lean/anc1.lean.expected.out | 2 +- tests/lean/defeq_simp2.lean.expected.out | 8 ++-- tests/lean/pp_char_bug.lean.expected.out | 4 +- tests/lean/pp_no_proofs.lean.expected.out | 6 +-- tests/lean/task.lean.expected.out | 3 +- tests/lean/uni_bug1.lean.expected.out | 2 +- 8 files changed, 28 insertions(+), 47 deletions(-) diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 46aa34f776..0acb23c3fe 100644 --- a/src/frontends/lean/pp.cpp +++ b/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 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 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 sep; // NOLINT diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h index be3a288057..c19167ebbc 100644 --- a/src/frontends/lean/pp.h +++ b/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 is_proof(expr const & f); bool is_prop(expr const & e); bool has_implicit_args(expr const & f); optional 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); diff --git a/tests/lean/anc1.lean.expected.out b/tests/lean/anc1.lean.expected.out index 396e79cb0f..c60e55475a 100644 --- a/tests/lean/anc1.lean.expected.out +++ b/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 : diff --git a/tests/lean/defeq_simp2.lean.expected.out b/tests/lean/defeq_simp2.lean.expected.out index 1ecd61cafd..842a4afaf9 100644 --- a/tests/lean/defeq_simp2.lean.expected.out +++ b/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 _ diff --git a/tests/lean/pp_char_bug.lean.expected.out b/tests/lean/pp_char_bug.lean.expected.out index 41bbba914f..ec28ef3587 100644 --- a/tests/lean/pp_char_bug.lean.expected.out +++ b/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" diff --git a/tests/lean/pp_no_proofs.lean.expected.out b/tests/lean/pp_no_proofs.lean.expected.out index b38300d0d0..3860e17fe1 100644 --- a/tests/lean/pp_no_proofs.lean.expected.out +++ b/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)))))) diff --git a/tests/lean/task.lean.expected.out b/tests/lean/task.lean.expected.out index 38eec2394e..7259a266b2 100644 --- a/tests/lean/task.lean.expected.out +++ b/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) diff --git a/tests/lean/uni_bug1.lean.expected.out b/tests/lean/uni_bug1.lean.expected.out index 064adc9284..b4ea4f6ab8 100644 --- a/tests/lean/uni_bug1.lean.expected.out +++ b/tests/lean/uni_bug1.lean.expected.out @@ -1 +1 @@ -f 1 0 (Rtrue ((1, 0).fst) 0) : ℕ +f 1 0 _ : ℕ