From c3b5ce07859bb1dfce3ca1eb7e37eec4e66ca10a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 7 Dec 2015 12:39:51 -0800 Subject: [PATCH] feat(frontends/lean/builtin_cmds): show metavariable arguments when pretty printing patterns --- src/frontends/lean/builtin_cmds.cpp | 5 ++++- tests/lean/pattern_pp.lean | 11 +++++++++++ tests/lean/pattern_pp.lean.expected.out | 5 +++++ 3 files changed, 20 insertions(+), 1 deletion(-) create mode 100644 tests/lean/pattern_pp.lean create mode 100644 tests/lean/pattern_pp.lean.expected.out diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index f359191aa..47117c730 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -240,7 +240,10 @@ static void print_patterns(parser & p, name const & n) { blast::scope_debug scope(p.env(), p.ios()); auto hi = blast::mk_hi_lemma(n, LEAN_FORWARD_LEMMA_DEFAULT_PRIORITY); if (hi.m_multi_patterns) { - io_state_stream out = p.regular_stream(); + io_state_stream _out = p.regular_stream(); + options opts = _out.get_options(); + opts = opts.update_if_undef(get_pp_metavar_args_name(), true); + io_state_stream out = _out.update_options(opts); out << "(multi-)patterns:\n"; if (!is_nil(hi.m_mvars)) { expr m = head(hi.m_mvars); diff --git a/tests/lean/pattern_pp.lean b/tests/lean/pattern_pp.lean new file mode 100644 index 000000000..7a4a52116 --- /dev/null +++ b/tests/lean/pattern_pp.lean @@ -0,0 +1,11 @@ +definition Sum : nat → (nat → nat) → nat := sorry +definition Sum_weird [forward] (f g h : nat → nat) (n : nat) : (Sum n (λ x, f (g (h x)))) = 1 := sorry +print Sum_weird + +/- +definition Sum_weird [forward] : ∀ (f g h : nat → nat) (n : nat), eq (Sum n (λ (x : nat), f (g (h x)))) 1 := +λ (f g h : nat → nat) (n : nat), sorry +(multi-)patterns: +?M_1 : nat → nat, ?M_2 : nat → nat, ?M_3 : nat → nat, ?M_4 : nat +{Sum ?M_4 (λ (x : nat), ?M_1)} +-/ diff --git a/tests/lean/pattern_pp.lean.expected.out b/tests/lean/pattern_pp.lean.expected.out new file mode 100644 index 000000000..9297527d7 --- /dev/null +++ b/tests/lean/pattern_pp.lean.expected.out @@ -0,0 +1,5 @@ +definition Sum_weird [forward] : ∀ (f g h : ℕ → ℕ) (n : ℕ), Sum n (λ (x : ℕ), f (g (h x))) = 1 := +λ (f g h : ℕ → ℕ) (n : ℕ), sorry +(multi-)patterns: +?M_1 : ℕ → ℕ, ?M_2 : ℕ → ℕ, ?M_3 : ℕ → ℕ, ?M_4 : ℕ +{Sum ?M_4 (λ (x : ℕ), ?M_1 (?M_2 (?M_3 x)))}