feat(library/tactic/goal): when listing context/goal variables, collect vars of same type in one line

closes #391

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();
+    unsigned i = 0;
-    for (auto it = tmp.begin(); it != end; ++it) {
+    while (i < tmp.size()) {
-        if (first) first = false; else r += compose(comma(), line());
+        if (i > 0)
-        expr l     = *it;
+            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);

tests/lean/beginend_bug.lean.expected.out

@@ -1,16 +1,12 @@
 beginend_bug.lean:7:2: error: tactic failed
 A : Type,
-a : A,
+a b c : A,
-b : A,
-c : A,
 Hab : a = b,
 Hbc : b = c
 ⊢ a = ?M_1
 
 A : Type,
-a : A,
+a b c : A,
-b : A,
-c : A,
 Hab : a = b,
 Hbc : b = c
 ⊢ ?M_1 = c

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 :=
+_

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

tests/lean/gen_bug.lean.expected.out

@@ -1,6 +1,5 @@
 gen_bug.lean:9:2: error: tactic failed
-A : Type,
+A B : Type,
-B : Type,
 a : A,
 b : B,
 H : @heq A a B b

tests/lean/goals1.lean.expected.out

@@ -1,8 +1,6 @@
 goals1.lean:9:0: error: unsolved subgoals
 A : Type,
-a : A,
+a b c : A,
-b : A,
-c : A,
 Hab : eq a b,
 Hbc : eq b c
 ⊢ eq b c

tests/lean/interactive/proof_state_info.input.expected.out

@@ -2,9 +2,7 @@
 -- ENDWAIT
 -- BEGININFO
 -- PROOF_STATE|7|2
-a : Prop,
+a b c : Prop,
-b : Prop,
-c : Prop,
 Ha : a,
 Hb : b
 ⊢ a ∧ b

tests/lean/interactive/proof_state_info2.input.expected.out

@@ -2,9 +2,7 @@
 -- ENDWAIT
 -- BEGININFO
 -- PROOF_STATE|5|17
-a : Prop,
+a b c : Prop,
-b : Prop,
-c : Prop,
 Ha : a,
 Hb : b
 ⊢ a ∧ b
@@ -12,16 +10,12 @@ Hb : b
 -- ENDINFO
 -- BEGININFO
 -- PROOF_STATE|6|17
-a : Prop,
+a b c : Prop,
-b : Prop,
-c : Prop,
 Ha : a,
 Hb : b
 ⊢ a
 --
-a : Prop,
+a b c : Prop,
-b : Prop,
-c : Prop,
 Ha : a,
 Hb : b
 ⊢ b
@@ -29,9 +23,7 @@ Hb : b
 -- ENDINFO
 -- BEGININFO
 -- PROOF_STATE|7|10
-a : Prop,
+a b c : Prop,
-b : Prop,
-c : Prop,
 Ha : a,
 Hb : b
 ⊢ 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,
+a b c : A,
-b : A,
-c : A,
 h₁ : a = b,
 h₂ : b = c
 ⊢ b = c