From b62816cc25d3fea9c066d82db25976aab84f9a47 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 6 Sep 2013 17:58:45 -0700 Subject: [PATCH] Fix problem with pretty printer. Add another test for elaborator Signed-off-by: Leonardo de Moura --- src/frontends/lean/lean_frontend.cpp | 5 +++++ src/frontends/lean/lean_frontend.h | 5 +++++ src/frontends/lean/lean_pp.cpp | 10 +++++++++- tests/lean/elab4.lean | 12 ++++++++++++ tests/lean/elab4.lean.expected.out | 23 +++++++++++++++++++++++ tests/lean/tst6.lean.expected.out | 3 +-- 6 files changed, 55 insertions(+), 3 deletions(-) create mode 100644 tests/lean/elab4.lean create mode 100644 tests/lean/elab4.lean.expected.out diff --git a/src/frontends/lean/lean_frontend.cpp b/src/frontends/lean/lean_frontend.cpp index 941518ed1..22e44bc5c 100644 --- a/src/frontends/lean/lean_frontend.cpp +++ b/src/frontends/lean/lean_frontend.cpp @@ -297,6 +297,10 @@ struct frontend::imp { } } + bool is_explicit(name const & n) { + return !n.is_atomic() && get_explicit_version(n.get_prefix()) == n; + } + void add_coercion(expr const & f) { expr type = m_env.infer_type(f); expr norm_type = m_env.normalize(type); @@ -412,6 +416,7 @@ void frontend::mark_implicit_arguments(name const & n, std::initializer_listhas_implicit_arguments(n); } std::vector const & frontend::get_implicit_arguments(name const & n) const { return m_imp->get_implicit_arguments(n); } name const & frontend::get_explicit_version(name const & n) const { return m_imp->get_explicit_version(n); } +bool frontend::is_explicit(name const & n) const { return m_imp->is_explicit(n); } void frontend::add_coercion(expr const & f) { m_imp->add_coercion(f); } expr frontend::get_coercion(expr const & given_type, expr const & expected_type, context const & ctx) const { diff --git a/src/frontends/lean/lean_frontend.h b/src/frontends/lean/lean_frontend.h index 741a6eb05..221163964 100644 --- a/src/frontends/lean/lean_frontend.h +++ b/src/frontends/lean/lean_frontend.h @@ -147,6 +147,11 @@ public: arguments. */ name const & get_explicit_version(name const & n) const; + /** + \brief Return true iff \c n is the name of the "explicit" + version of an object with implicit arguments + */ + bool is_explicit(name const & n) const; /*@}*/ /** diff --git a/src/frontends/lean/lean_pp.cpp b/src/frontends/lean/lean_pp.cpp index 450f5334d..a283d8660 100644 --- a/src/frontends/lean/lean_pp.cpp +++ b/src/frontends/lean/lean_pp.cpp @@ -1182,7 +1182,15 @@ class pp_formatter_cell : public formatter_cell { } format pp_definition(object const & obj, options const & opts) { - return pp_compact_definition(obj.keyword(), obj.get_name(), obj.get_type(), obj.get_value(), opts); + if (m_frontend.is_explicit(obj.get_name())) { + // Hide implicit arguments when pretty printing the + // explicit version on an object. + // We do that because otherwise it looks like a recursive definition. + options new_opts = update(opts, g_pp_implicit, false); + return pp_compact_definition(obj.keyword(), obj.get_name(), obj.get_type(), obj.get_value(), new_opts); + } else { + return pp_compact_definition(obj.keyword(), obj.get_name(), obj.get_type(), obj.get_value(), opts); + } } format pp_notation_decl(object const & obj, options const & opts) { diff --git a/tests/lean/elab4.lean b/tests/lean/elab4.lean new file mode 100644 index 000000000..068146433 --- /dev/null +++ b/tests/lean/elab4.lean @@ -0,0 +1,12 @@ +Variable C {A B : Type} (H : A = B) (a : A) : B + +Variable D {A A' : Type} {B : A -> Type} {B' : A' -> Type} (H : (Pi x : A, B x) = (Pi x : A', B' x)) : A = A' + +Variable R {A A' : Type} {B : A -> Type} {B' : A' -> Type} (H : (Pi x : A, B x) = (Pi x : A', B' x)) (a : A) : + (B a) = (B' (C (D H) a)) + +Theorem R2 : Pi (A1 A2 B1 B2 : Type) (H : A1 -> B1 = A2 -> B2) (a : A1), B1 = B2 := + fun A1 A2 B1 B2 H a, R H a + +Set pp::implicit true +Show Environment 7. diff --git a/tests/lean/elab4.lean.expected.out b/tests/lean/elab4.lean.expected.out new file mode 100644 index 000000000..7daf828ee --- /dev/null +++ b/tests/lean/elab4.lean.expected.out @@ -0,0 +1,23 @@ + Set: pp::colors + Set: pp::unicode + Assumed: C + Assumed: D + Assumed: R + Proved: R2 + Set: lean::pp::implicit +Variable C {A B : Type} (H : 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 : (Π x : A, B x) = (Π x : A', B' x)) : 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 : (Π x : A, B x) = (Π x : A', B' x)) (a : A) : + (B a) = (B' (C::explicit A A' (D::explicit A A' B B' 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 : A1 → B1 = A2 → B2) (a : A1) : B1 = B2 := + R::explicit A1 A2 (λ a : A1, B1) (λ _ : A2, B2) H a diff --git a/tests/lean/tst6.lean.expected.out b/tests/lean/tst6.lean.expected.out index 905264392..e63242bbd 100644 --- a/tests/lean/tst6.lean.expected.out +++ b/tests/lean/tst6.lean.expected.out @@ -14,8 +14,7 @@ Theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h 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::explicit a1 a2 b1 b2 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 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