From 591fb91f34c89d49dc0e3c1fd78f5086461a45a2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 13 Jun 2015 11:32:59 -0700 Subject: [PATCH] fix(frontends/lean/builtin_cmds): fixes #671 --- src/frontends/lean/builtin_cmds.cpp | 13 ++++++++----- tests/lean/584a.lean.expected.out | 2 +- tests/lean/608.hlean.expected.out | 4 ++-- tests/lean/671.lean | 1 + tests/lean/671.lean.expected.out | 2 ++ tests/lean/nested1.lean.expected.out | 8 ++++---- tests/lean/nested2.lean.expected.out | 14 +++++++------- 7 files changed, 25 insertions(+), 19 deletions(-) create mode 100644 tests/lean/671.lean create mode 100644 tests/lean/671.lean.expected.out diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 00f47d97f..b9ca8457b 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -174,7 +174,7 @@ static void print_definition(parser const & p, name const & n, pos_info const & io_state_stream new_out = out.update_options(opts); if (d.is_axiom()) throw parser_error(sstream() << "invalid 'print definition', theorem '" << n - << "' is not available (suggestion: use command 'wait " << n << "')", pos); + << "' is not available (suggestion: use command 'reveal " << n << "')", pos); if (!d.is_definition()) throw parser_error(sstream() << "invalid 'print definition', '" << n << "' is not a definition", pos); new_out << d.get_value() << endl; @@ -265,13 +265,16 @@ static void print_recursor_info(parser & p) { } } -bool print_constant(parser & p, char const * kind, declaration const & d) { +bool print_constant(parser & p, char const * kind, declaration const & d, bool is_def = false) { io_state_stream out = p.regular_stream(); if (is_protected(p.env(), d.get_name())) out << "protected "; out << kind << " " << d.get_name(); print_attributes(p, d.get_name()); - out << " : " << d.get_type() << "\n"; + out << " : " << d.get_type(); + if (is_def) + out << " :="; + out << "\n"; return true; } @@ -287,7 +290,7 @@ bool print_polymorphic(parser & p) { for (name const & c : cs) { declaration const & d = env.get(c); if (d.is_theorem()) { - print_constant(p, "theorem", d); + print_constant(p, "theorem", d, true); print_definition(p, c, pos); } else if (d.is_axiom() || d.is_constant_assumption()) { if (inductive::is_inductive_decl(env, c)) { @@ -306,7 +309,7 @@ bool print_polymorphic(parser & p) { print_constant(p, "constant", d); } } else if (d.is_definition()) { - print_constant(p, "definition", d); + print_constant(p, "definition", d, true); print_definition(p, c, pos); } } diff --git a/tests/lean/584a.lean.expected.out b/tests/lean/584a.lean.expected.out index 2fa0ac087..0884db45d 100644 --- a/tests/lean/584a.lean.expected.out +++ b/tests/lean/584a.lean.expected.out @@ -1,5 +1,5 @@ foo : Π (A : Type) [H : inhabited A], A → A foo' : Π {A : Type} [H : inhabited A] {x : A}, A foo ℕ 10 : ℕ -definition test : ∀ {A : Type} [H : inhabited A], @foo' num num.is_inhabited 10 = 10 +definition test : ∀ {A : Type} [H : inhabited A], @foo' num num.is_inhabited 10 = 10 := λ (A : Type) (H : inhabited A), @rfl num (@foo' num num.is_inhabited 10) diff --git a/tests/lean/608.hlean.expected.out b/tests/lean/608.hlean.expected.out index e3bebab09..2d0901e72 100644 --- a/tests/lean/608.hlean.expected.out +++ b/tests/lean/608.hlean.expected.out @@ -1,6 +1,6 @@ -definition category.id [reducible] : Π {ob : Type} [C : precategory ob] {a : ob}, hom a a +definition category.id [reducible] : Π {ob : Type} [C : precategory ob] {a : ob}, hom a a := ID -definition function.id [reducible] : Π {A : Type}, A → A +definition function.id [reducible] : Π {A : Type}, A → A := λ (A : Type) (a : A), a ----------- definition category.id [reducible] : Π {ob : Type} [C : precategory ob] {a : ob}, hom a a diff --git a/tests/lean/671.lean b/tests/lean/671.lean new file mode 100644 index 000000000..255e1c22f --- /dev/null +++ b/tests/lean/671.lean @@ -0,0 +1 @@ +print nat.add diff --git a/tests/lean/671.lean.expected.out b/tests/lean/671.lean.expected.out new file mode 100644 index 000000000..869b128ec --- /dev/null +++ b/tests/lean/671.lean.expected.out @@ -0,0 +1,2 @@ +definition nat.add : nat → nat → nat := +λ (a b : nat), nat.rec_on b a (λ (b₁ : nat), nat.succ) diff --git a/tests/lean/nested1.lean.expected.out b/tests/lean/nested1.lean.expected.out index 732b9debf..d2c80028c 100644 --- a/tests/lean/nested1.lean.expected.out +++ b/tests/lean/nested1.lean.expected.out @@ -1,8 +1,8 @@ -definition test.foo.prf [irreducible] : ∀ (x : ℕ), 0 < succ (succ x) +definition test.foo.prf [irreducible] : ∀ (x : ℕ), 0 < succ (succ x) := λ (x : ℕ), lt.step (zero_lt_succ x) -definition test.bla : ℕ → ℕ +definition test.bla : ℕ → ℕ := λ (a : ℕ), foo (succ (succ a)) (foo.prf a) -definition test.bla : ℕ → ℕ +definition test.bla : ℕ → ℕ := λ (a : ℕ), test.foo (succ (succ a)) (test.foo.prf a) -definition test.foo.prf : ∀ (x : ℕ), 0 < succ (succ x) +definition test.foo.prf : ∀ (x : ℕ), 0 < succ (succ x) := λ (x : ℕ), lt.step (zero_lt_succ x) diff --git a/tests/lean/nested2.lean.expected.out b/tests/lean/nested2.lean.expected.out index 42b513514..464debfc1 100644 --- a/tests/lean/nested2.lean.expected.out +++ b/tests/lean/nested2.lean.expected.out @@ -1,15 +1,15 @@ -definition bla : ℕ → ℕ +definition bla : ℕ → ℕ := λ (a : ℕ), foo (succ (succ a)) (bla_2 a) -definition bla_1 : ∀ (x : ℕ), 0 < succ x +definition bla_1 : ∀ (x : ℕ), 0 < succ x := λ (x : ℕ), zero_lt_succ x -definition bla_2 : ∀ (x : ℕ), 0 < succ (succ x) +definition bla_2 : ∀ (x : ℕ), 0 < succ (succ x) := λ (x : ℕ), lt.step (bla_1 x) -definition test_1 [irreducible] : ∀ (x : ℕ), 0 < succ x +definition test_1 [irreducible] : ∀ (x : ℕ), 0 < succ x := λ (x : ℕ), zero_lt_succ x -definition test_2 [reducible] : ∀ (x : ℕ), 0 < succ (succ x) +definition test_2 [reducible] : ∀ (x : ℕ), 0 < succ (succ x) := λ (x : ℕ), lt.step (test_1 x) definition tst_1 : ∀ (x : Type.{l_1}) (x_1 : x) (x_2 : list.{l_1} x), - x_1 :: x_2 = nil.{l_1} → list.no_confusion_type.{0 l_1} false (x_1 :: x_2) nil.{l_1} + x_1 :: x_2 = nil.{l_1} → list.no_confusion_type.{0 l_1} false (x_1 :: x_2) nil.{l_1} := λ (x : Type.{l_1}) (x_1 : x) (x_2 : list.{l_1} x), list.no_confusion.{0 l_1} -definition tst : Π {A : Type.{l_1}}, A → list.{l_1} A → bool +definition tst : Π {A : Type.{l_1}}, A → list.{l_1} A → bool := λ (A : Type.{l_1}) (a : A) (l : list.{l_1} A), voo.{(max 1 l_1)} (a :: l) nil.{l_1} (tst_1.{l_1} A a l)