From 1fbfe59a9aecb679d0ce78bf551a3b9071156abe Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 13 Jan 2015 11:10:28 -0800
Subject: [PATCH] feat(library/tactic/goal): when listing context/goal
 variables, collect vars of same type in one line

closes #391
---
 src/library/tactic/goal.cpp                   | 23 ++++++++++++++-----
 tests/lean/beginend_bug.lean.expected.out     |  8 ++-----
 tests/lean/ctx.lean                           |  3 +++
 tests/lean/ctx.lean.expected.out              | 10 ++++++++
 tests/lean/gen_bug.lean.expected.out          |  3 +--
 tests/lean/goals1.lean.expected.out           |  4 +---
 .../proof_state_info.input.expected.out       |  4 +---
 .../proof_state_info2.input.expected.out      | 16 ++++---------
 tests/lean/pstate.lean.expected.out           |  4 +---
 9 files changed, 40 insertions(+), 35 deletions(-)
 create mode 100644 tests/lean/ctx.lean
 create mode 100644 tests/lean/ctx.lean.expected.out

diff --git a/src/library/tactic/goal.cpp b/src/library/tactic/goal.cpp
index da0a71ac3..60ad06a04 100644
--- a/src/library/tactic/goal.cpp
+++ b/src/library/tactic/goal.cpp
@@ -48,14 +48,25 @@ format goal::pp(formatter const & fmt, substitution const & s) const {
     expr conclusion  = m_type;
     buffer<expr> tmp;
     get_app_args(m_meta, tmp);
-    bool first = true;
     format r;
-    auto end = tmp.end();
-    for (auto it = tmp.begin(); it != end; ++it) {
-        if (first) first = false; else r += compose(comma(), line());
-        expr l     = *it;
+    unsigned i = 0;
+    while (i < tmp.size()) {
+        if (i > 0)
+            r += compose(comma(), line());
+        expr l     = tmp[i];
+        format ids = fmt(l);
         expr t     = tmp_subst.instantiate(mlocal_type(l));
-        r += group(fmt(l) + space() + colon() + nest(indent, line() + fmt(t)));
+        lean_assert(tmp.size() > 0);
+        while (i < tmp.size() - 1) {
+            expr l2 = tmp[i+1];
+            expr t2 = tmp_subst.instantiate(mlocal_type(l2));
+            if (t2 != t)
+                break;
+            ids += space() + fmt(l2);
+            i++;
+        }
+        r += group(ids + space() + colon() + nest(indent, line() + fmt(t)));
+        i++;
     }
     if (compact)
         r = group(r);
diff --git a/tests/lean/beginend_bug.lean.expected.out b/tests/lean/beginend_bug.lean.expected.out
index 7d649bd32..665fc426a 100644
--- a/tests/lean/beginend_bug.lean.expected.out
+++ b/tests/lean/beginend_bug.lean.expected.out
@@ -1,16 +1,12 @@
 beginend_bug.lean:7:2: error: tactic failed
 A : Type,
-a : A,
-b : A,
-c : A,
+a b c : A,
 Hab : a = b,
 Hbc : b = c
 ⊢ a = ?M_1
 
 A : Type,
-a : A,
-b : A,
-c : A,
+a b c : A,
 Hab : a = b,
 Hbc : b = c
 ⊢ ?M_1 = c
diff --git a/tests/lean/ctx.lean b/tests/lean/ctx.lean
new file mode 100644
index 000000000..803df0215
--- /dev/null
+++ b/tests/lean/ctx.lean
@@ -0,0 +1,3 @@
+open prod
+definition foo {A B : Type} (a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 : nat) (b1 b2 b3 : bool) (h : A = B) (p1 p2 : A × B) : nat :=
+_
diff --git a/tests/lean/ctx.lean.expected.out b/tests/lean/ctx.lean.expected.out
new file mode 100644
index 000000000..76c785599
--- /dev/null
+++ b/tests/lean/ctx.lean.expected.out
@@ -0,0 +1,10 @@
+ctx.lean:3:0: error: don't know how to synthesize placeholder
+A B : Type,
+a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 : nat,
+b1 b2 b3 : bool,
+h : A = B,
+p1 p2 : A × B
+⊢ nat
+ctx.lean:3:0: error: failed to add declaration 'foo' to environment, value has metavariables
+  λ (A B : Type) (a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 : nat) (b1 b2 b3 : bool) (h : A = B) (p1 p2 : A × B),
+    ?M_1
diff --git a/tests/lean/gen_bug.lean.expected.out b/tests/lean/gen_bug.lean.expected.out
index e07e4f52c..fac193206 100644
--- a/tests/lean/gen_bug.lean.expected.out
+++ b/tests/lean/gen_bug.lean.expected.out
@@ -1,6 +1,5 @@
 gen_bug.lean:9:2: error: tactic failed
-A : Type,
-B : Type,
+A B : Type,
 a : A,
 b : B,
 H : @heq A a B b
diff --git a/tests/lean/goals1.lean.expected.out b/tests/lean/goals1.lean.expected.out
index b27b5f931..9b2ff3931 100644
--- a/tests/lean/goals1.lean.expected.out
+++ b/tests/lean/goals1.lean.expected.out
@@ -1,8 +1,6 @@
 goals1.lean:9:0: error: unsolved subgoals
 A : Type,
-a : A,
-b : A,
-c : A,
+a b c : A,
 Hab : eq a b,
 Hbc : eq b c
 ⊢ eq b c
diff --git a/tests/lean/interactive/proof_state_info.input.expected.out b/tests/lean/interactive/proof_state_info.input.expected.out
index 8353f9885..982ce8a9a 100644
--- a/tests/lean/interactive/proof_state_info.input.expected.out
+++ b/tests/lean/interactive/proof_state_info.input.expected.out
@@ -2,9 +2,7 @@
 -- ENDWAIT
 -- BEGININFO
 -- PROOF_STATE|7|2
-a : Prop,
-b : Prop,
-c : Prop,
+a b c : Prop,
 Ha : a,
 Hb : b
 ⊢ a ∧ b
diff --git a/tests/lean/interactive/proof_state_info2.input.expected.out b/tests/lean/interactive/proof_state_info2.input.expected.out
index c9865cc11..2debaaae8 100644
--- a/tests/lean/interactive/proof_state_info2.input.expected.out
+++ b/tests/lean/interactive/proof_state_info2.input.expected.out
@@ -2,9 +2,7 @@
 -- ENDWAIT
 -- BEGININFO
 -- PROOF_STATE|5|17
-a : Prop,
-b : Prop,
-c : Prop,
+a b c : Prop,
 Ha : a,
 Hb : b
 ⊢ a ∧ b
@@ -12,16 +10,12 @@ Hb : b
 -- ENDINFO
 -- BEGININFO
 -- PROOF_STATE|6|17
-a : Prop,
-b : Prop,
-c : Prop,
+a b c : Prop,
 Ha : a,
 Hb : b
 ⊢ a
 --
-a : Prop,
-b : Prop,
-c : Prop,
+a b c : Prop,
 Ha : a,
 Hb : b
 ⊢ b
@@ -29,9 +23,7 @@ Hb : b
 -- ENDINFO
 -- BEGININFO
 -- PROOF_STATE|7|10
-a : Prop,
-b : Prop,
-c : Prop,
+a b c : Prop,
 Ha : a,
 Hb : b
 ⊢ b
diff --git a/tests/lean/pstate.lean.expected.out b/tests/lean/pstate.lean.expected.out
index 396348f39..b902706f7 100644
--- a/tests/lean/pstate.lean.expected.out
+++ b/tests/lean/pstate.lean.expected.out
@@ -1,8 +1,6 @@
 pstate.lean:4:26: error: don't know how to synthesize placeholder
 A : Type,
-a : A,
-b : A,
-c : A,
+a b c : A,
 h₁ : a = b,
 h₂ : b = c
 ⊢ b = c