From ad3f771b1d8c85dfc6c715266b35348c522feff1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 19 Dec 2013 13:12:39 -0800 Subject: [PATCH] feat(frontends/lean): hide 'explicit' version of objects with implicit arguments Signed-off-by: Leonardo de Moura --- src/frontends/lean/parser.cpp | 32 +++++++++++++++++++----------- src/library/io_state.cpp | 6 ++++++ src/library/io_state.h | 1 + tests/lean/elab4.lean.expected.out | 13 +++--------- tests/lean/elab5.lean.expected.out | 13 +++--------- tests/lean/tst1.lean.expected.out | 9 ++++----- tests/lean/tst6.lean.expected.out | 4 ++-- 7 files changed, 39 insertions(+), 39 deletions(-) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 0eaab79ad..55f177a73 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1789,6 +1789,11 @@ class parser::imp { regular(m_io_state) << r << endl; } + /** \brief Return true iff \c obj is an object that should be ignored by the Show command */ + bool is_hidden_object(object const & obj) const { + return obj.is_definition() && is_explicit(m_env, obj.get_name()); + } + /** \brief Parse 'Show' expr 'Show' Environment [num] @@ -1800,20 +1805,23 @@ class parser::imp { name opt_id = curr_name(); next(); if (opt_id == g_env_kwd) { + unsigned i; if (curr_is_nat()) { - unsigned i = parse_unsigned("invalid argument, value does not fit in a machine integer"); - auto end = m_env->end_objects(); - auto beg = m_env->begin_objects(); - auto it = end; - while (it != beg && i != 0) { - --i; - --it; - } - for (; it != end; ++it) { - regular(m_io_state) << *it << endl; - } + i = parse_unsigned("invalid argument, value does not fit in a machine integer"); } else { - regular(m_io_state) << m_env << endl; + i = std::numeric_limits::max(); + } + auto end = m_env->end_objects(); + auto beg = m_env->begin_objects(); + auto it = end; + while (it != beg && i != 0) { + --it; + if (!is_hidden_object(*it)) + --i; + } + for (; it != end; ++it) { + if (!is_hidden_object(*it)) + regular(m_io_state) << *it << endl; } } else if (opt_id == g_options_kwd) { regular(m_io_state) << pp(m_io_state.get_options()) << endl; diff --git a/src/library/io_state.cpp b/src/library/io_state.cpp index 5ea1f8cd3..89123361c 100644 --- a/src/library/io_state.cpp +++ b/src/library/io_state.cpp @@ -59,6 +59,12 @@ io_state_stream const & operator<<(io_state_stream const & out, object const & o return out; } +io_state_stream const & operator<<(io_state_stream const & out, environment const & env) { + options const & opts = out.get_options(); + out.get_stream() << mk_pair(out.get_formatter()(env, opts), opts); + return out; +} + io_state_stream const & operator<<(io_state_stream const & out, kernel_exception const & ex) { options const & opts = out.get_options(); out.get_stream() << mk_pair(ex.pp(out.get_formatter(), opts), opts); diff --git a/src/library/io_state.h b/src/library/io_state.h index 21e174820..56f75fa4c 100644 --- a/src/library/io_state.h +++ b/src/library/io_state.h @@ -84,6 +84,7 @@ class kernel_exception; io_state_stream const & operator<<(io_state_stream const & out, endl_class); io_state_stream const & operator<<(io_state_stream const & out, expr const & e); io_state_stream const & operator<<(io_state_stream const & out, object const & obj); +io_state_stream const & operator<<(io_state_stream const & out, environment const & env); io_state_stream const & operator<<(io_state_stream const & out, kernel_exception const & ex); template io_state_stream const & operator<<(io_state_stream const & out, T const & t) { out.get_stream() << t; diff --git a/tests/lean/elab4.lean.expected.out b/tests/lean/elab4.lean.expected.out index 8f83cfcad..360fa2342 100644 --- a/tests/lean/elab4.lean.expected.out +++ b/tests/lean/elab4.lean.expected.out @@ -5,24 +5,17 @@ Assumed: R Proved: R2 Set: lean::pp::implicit +Coercion int_to_real +Coercion nat_to_real +Definition SubstP : Π (A : Type U) (a b : A) (P : A → Bool), P a → a == b → P b := Subst::explicit Variable C {A B : Type} (H : eq::explicit Type A B) (a : A) : B -Definition C::explicit (A B : Type) (H : A = B) (a : A) : B := C H a Variable D {A A' : Type} {B : A → Type} {B' : A' → Type} (H : eq::explicit Type (Π x : A, B x) (Π x : A', B' x)) : eq::explicit Type A A' -Definition D::explicit (A A' : Type) (B : A → Type) (B' : A' → Type) (H : (Π x : A, B x) = (Π x : A', B' x)) : A = - A' := - D H Variable R {A A' : Type} {B : A → Type} {B' : A' → Type} (H : eq::explicit Type (Π x : A, B x) (Π x : A', B' x)) (a : A) : eq::explicit Type (B a) (B' (C::explicit A A' (D::explicit A A' (λ x : A, B x) (λ x : A', B' x) H) a)) -Definition R::explicit (A A' : Type) - (B : A → Type) - (B' : A' → Type) - (H : (Π x : A, B x) = (Π x : A', B' x)) - (a : A) : B a = B' (C (D H) a) := - R H a Theorem R2 (A1 A2 B1 B2 : Type) (H : eq::explicit Type (A1 → B1) (A2 → B2)) (a : A1) : eq::explicit Type B1 B2 := R::explicit A1 A2 (λ x : A1, B1) (λ x : A2, B2) H a diff --git a/tests/lean/elab5.lean.expected.out b/tests/lean/elab5.lean.expected.out index 8f83cfcad..360fa2342 100644 --- a/tests/lean/elab5.lean.expected.out +++ b/tests/lean/elab5.lean.expected.out @@ -5,24 +5,17 @@ Assumed: R Proved: R2 Set: lean::pp::implicit +Coercion int_to_real +Coercion nat_to_real +Definition SubstP : Π (A : Type U) (a b : A) (P : A → Bool), P a → a == b → P b := Subst::explicit Variable C {A B : Type} (H : eq::explicit Type A B) (a : A) : B -Definition C::explicit (A B : Type) (H : A = B) (a : A) : B := C H a Variable D {A A' : Type} {B : A → Type} {B' : A' → Type} (H : eq::explicit Type (Π x : A, B x) (Π x : A', B' x)) : eq::explicit Type A A' -Definition D::explicit (A A' : Type) (B : A → Type) (B' : A' → Type) (H : (Π x : A, B x) = (Π x : A', B' x)) : A = - A' := - D H Variable R {A A' : Type} {B : A → Type} {B' : A' → Type} (H : eq::explicit Type (Π x : A, B x) (Π x : A', B' x)) (a : A) : eq::explicit Type (B a) (B' (C::explicit A A' (D::explicit A A' (λ x : A, B x) (λ x : A', B' x) H) a)) -Definition R::explicit (A A' : Type) - (B : A → Type) - (B' : A' → Type) - (H : (Π x : A, B x) = (Π x : A', B' x)) - (a : A) : B a = B' (C (D H) a) := - R H a Theorem R2 (A1 A2 B1 B2 : Type) (H : eq::explicit Type (A1 → B1) (A2 → B2)) (a : A1) : eq::explicit Type B1 B2 := R::explicit A1 A2 (λ x : A1, B1) (λ x : A2, B2) H a diff --git a/tests/lean/tst1.lean.expected.out b/tests/lean/tst1.lean.expected.out index 65ee19a39..fe96efd45 100644 --- a/tests/lean/tst1.lean.expected.out +++ b/tests/lean/tst1.lean.expected.out @@ -12,19 +12,18 @@ Defined: update Defined: select Defined: map +Variable one : N +Variable two : N +Variable three : N +Infix 50 < : lt Axiom two_lt_three : two < three Definition vector (A : Type) (n : N) : Type := Π (i : N), i < n → A Definition const {A : Type} (n : N) (d : A) : vector A n := λ (i : N) (H : i < n), d -Definition const::explicit (A : Type) (n : N) (d : A) : vector A n := const n d Definition update {A : Type} {n : N} (v : vector A n) (i : N) (d : A) : vector A n := λ (j : N) (H : j < n), if (j = i) d (v j H) -Definition update::explicit (A : Type) (n : N) (v : vector A n) (i : N) (d : A) : vector A n := update v i d Definition select {A : Type} {n : N} (v : vector A n) (i : N) (H : i < n) : A := v i H -Definition select::explicit (A : Type) (n : N) (v : vector A n) (i : N) (H : i < n) : A := select v i H Definition map {A B C : Type} {n : N} (f : A → B → C) (v1 : vector A n) (v2 : vector B n) : vector C n := λ (i : N) (H : i < n), f (v1 i H) (v2 i H) -Definition map::explicit (A B C : Type) (n : N) (f : A → B → C) (v1 : vector A n) (v2 : vector B n) : vector C n := - map f v1 v2 select (update (const three ⊥) two ⊤) two two_lt_three : Bool if (two == two) ⊤ ⊥ update (const three ⊥) two ⊤ : vector Bool three diff --git a/tests/lean/tst6.lean.expected.out b/tests/lean/tst6.lean.expected.out index 54b8a63a4..a740b7192 100644 --- a/tests/lean/tst6.lean.expected.out +++ b/tests/lean/tst6.lean.expected.out @@ -4,6 +4,7 @@ Assumed: h Proved: CongrH Set: lean::pp::implicit +Variable h : N → N → N Theorem CongrH {a1 a2 b1 b2 : N} (H1 : eq::explicit N a1 b1) (H2 : eq::explicit N a2 b2) : eq::explicit N (h a1 a2) @@ -17,10 +18,9 @@ Theorem CongrH {a1 a2 b1 b2 : N} (H1 : eq::explicit N a1 b1) (H2 : eq::explicit b2 (Congr::explicit N (λ x : N, N → N) h h a1 b1 (Refl::explicit (N → N → N) h) H1) H2 -Theorem CongrH::explicit (a1 a2 b1 b2 : N) (H1 : a1 = b1) (H2 : a2 = b2) : h a1 a2 = h b1 b2 := CongrH H1 H2 Set: lean::pp::implicit +Variable h : N → N → N Theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : h a1 a2 = h b1 b2 := Congr (Congr (Refl h) H1) H2 -Theorem CongrH::explicit (a1 a2 b1 b2 : N) (H1 : a1 = b1) (H2 : a2 = b2) : h a1 a2 = h b1 b2 := CongrH H1 H2 Proved: Example1 Set: lean::pp::implicit Theorem Example1 (a b c d : N)