From f43db96e1f477dcd7d66f099bcb5b475edc51c11 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 19 Dec 2013 15:23:43 -0800
Subject: [PATCH] fix(frontends/lean/pp): pretty printer for Type

Add parenthesis around Type when it has a universe.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/pp.cpp          |  6 +--
 tests/lean/conv.lean.expected.out  |  2 +-
 tests/lean/elab1.lean.expected.out | 62 +++++++++++++++---------------
 tests/lean/norm1.lean.expected.out |  2 +-
 tests/lean/tst11.lean.expected.out |  2 +-
 tests/lean/tst15.lean.expected.out | 34 ++++++++--------
 tests/lean/tst4.lean.expected.out  |  3 +-
 7 files changed, 56 insertions(+), 55 deletions(-)

diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 4dd4f03cec..1333481df2 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -197,12 +197,10 @@ class pp_fn {
     */
     bool is_atomic(expr const & e) {
         switch (e.kind()) {
-        case expr_kind::Var: case expr_kind::Constant:
+        case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type:
             return true;
         case expr_kind::Value:
             return !is_choice(e);
-        case expr_kind::Type:
-            return e == Type();
         case expr_kind::MetaVar:
             return !metavar_lctx(e);
         case expr_kind::App:
@@ -257,7 +255,7 @@ class pp_fn {
         if (e == Type()) {
             return mk_result(g_Type_fmt, 1);
         } else {
-            return mk_result(format{g_Type_fmt, space(), ::lean::pp(ty_level(e), m_unicode)}, 1);
+            return mk_result(paren(format{g_Type_fmt, space(), ::lean::pp(ty_level(e), m_unicode)}), 1);
         }
     }
 
diff --git a/tests/lean/conv.lean.expected.out b/tests/lean/conv.lean.expected.out
index 361c1b4413..676b216d5f 100644
--- a/tests/lean/conv.lean.expected.out
+++ b/tests/lean/conv.lean.expected.out
@@ -11,7 +11,7 @@ p f : Bool
 g a : Bool
   Defined: c2
   Assumed: b
-c2::explicit : Π (T : Type), Type 3 → T → Type 3
+c2::explicit : Π (T : Type), (Type 3) → T → (Type 3)
   Assumed: g2
 g2 : c2 (Type 2) b → Bool
   Assumed: a2
diff --git a/tests/lean/elab1.lean.expected.out b/tests/lean/elab1.lean.expected.out
index df60f07996..e25f66c269 100644
--- a/tests/lean/elab1.lean.expected.out
+++ b/tests/lean/elab1.lean.expected.out
@@ -210,7 +210,8 @@ Failed to solve
             Bool
             Bool
     Failed to solve
-     ⊢ (?M::0 ≈ Type) ⊕ (?M::0 ≈ Type 1) ⊕ (?M::0 ≈ Type 2) ⊕ (?M::0 ≈ Type M) ⊕ (?M::0 ≈ Type U)
+     ⊢
+    (?M::0 ≈ Type) ⊕ (?M::0 ≈ (Type 1)) ⊕ (?M::0 ≈ (Type 2)) ⊕ (?M::0 ≈ (Type M)) ⊕ (?M::0 ≈ (Type U))
         Destruct/Decompose
          ⊢ Type ≺ ?M::0
             (line: 24: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
@@ -220,9 +221,9 @@ Failed to solve
                 Bool
                 Bool
         Failed to solve
-         ⊢ Type 1 ≺ Type
+         ⊢ (Type 1) ≺ Type
             Substitution
-             ⊢ Type 1 ≺ ?M::1
+             ⊢ (Type 1) ≺ ?M::1
                 Propagate type, ?M::0 : ?M::1
                     Assignment
                      ⊢ ?M::0 ≈ Type
@@ -231,51 +232,52 @@ Failed to solve
                  ⊢ ?M::1 ≈ Type
                     Assumption 0
         Failed to solve
-         ⊢ Type 2 ≺ Type
+         ⊢ (Type 2) ≺ Type
             Substitution
-             ⊢ Type 2 ≺ ?M::1
+             ⊢ (Type 2) ≺ ?M::1
                 Propagate type, ?M::0 : ?M::1
                     Assignment
-                     ⊢ ?M::0 ≈ Type 1
+                     ⊢ ?M::0 ≈ (Type 1)
                         Assumption 2
                 Assignment
                  ⊢ ?M::1 ≈ Type
                     Assumption 0
         Failed to solve
-         ⊢ Type 3 ≺ Type
+         ⊢ (Type 3) ≺ Type
             Substitution
-             ⊢ Type 3 ≺ ?M::1
+             ⊢ (Type 3) ≺ ?M::1
                 Propagate type, ?M::0 : ?M::1
                     Assignment
-                     ⊢ ?M::0 ≈ Type 2
+                     ⊢ ?M::0 ≈ (Type 2)
                         Assumption 3
                 Assignment
                  ⊢ ?M::1 ≈ Type
                     Assumption 0
         Failed to solve
-         ⊢ Type M+1 ≺ Type
+         ⊢ (Type M+1) ≺ Type
             Substitution
-             ⊢ Type M+1 ≺ ?M::1
+             ⊢ (Type M+1) ≺ ?M::1
                 Propagate type, ?M::0 : ?M::1
                     Assignment
-                     ⊢ ?M::0 ≈ Type M
+                     ⊢ ?M::0 ≈ (Type M)
                         Assumption 4
                 Assignment
                  ⊢ ?M::1 ≈ Type
                     Assumption 0
         Failed to solve
-         ⊢ Type U+1 ≺ Type
+         ⊢ (Type U+1) ≺ Type
             Substitution
-             ⊢ Type U+1 ≺ ?M::1
+             ⊢ (Type U+1) ≺ ?M::1
                 Propagate type, ?M::0 : ?M::1
                     Assignment
-                     ⊢ ?M::0 ≈ Type U
+                     ⊢ ?M::0 ≈ (Type U)
                         Assumption 5
                 Assignment
                  ⊢ ?M::1 ≈ Type
                     Assumption 0
     Failed to solve
-     ⊢ (?M::0 ≈ Type) ⊕ (?M::0 ≈ Type 1) ⊕ (?M::0 ≈ Type 2) ⊕ (?M::0 ≈ Type M) ⊕ (?M::0 ≈ Type U)
+     ⊢
+    (?M::0 ≈ Type) ⊕ (?M::0 ≈ (Type 1)) ⊕ (?M::0 ≈ (Type 2)) ⊕ (?M::0 ≈ (Type M)) ⊕ (?M::0 ≈ (Type U))
         Destruct/Decompose
          ⊢ Type ≺ ?M::0
             (line: 24: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
@@ -285,9 +287,9 @@ Failed to solve
                 Bool
                 Bool
         Failed to solve
-         ⊢ Type 1 ≺ Bool
+         ⊢ (Type 1) ≺ Bool
             Substitution
-             ⊢ Type 1 ≺ ?M::1
+             ⊢ (Type 1) ≺ ?M::1
                 Propagate type, ?M::0 : ?M::1
                     Assignment
                      ⊢ ?M::0 ≈ Type
@@ -296,45 +298,45 @@ Failed to solve
                  ⊢ ?M::1 ≈ Bool
                     Assumption 6
         Failed to solve
-         ⊢ Type 2 ≺ Bool
+         ⊢ (Type 2) ≺ Bool
             Substitution
-             ⊢ Type 2 ≺ ?M::1
+             ⊢ (Type 2) ≺ ?M::1
                 Propagate type, ?M::0 : ?M::1
                     Assignment
-                     ⊢ ?M::0 ≈ Type 1
+                     ⊢ ?M::0 ≈ (Type 1)
                         Assumption 8
                 Assignment
                  ⊢ ?M::1 ≈ Bool
                     Assumption 6
         Failed to solve
-         ⊢ Type 3 ≺ Bool
+         ⊢ (Type 3) ≺ Bool
             Substitution
-             ⊢ Type 3 ≺ ?M::1
+             ⊢ (Type 3) ≺ ?M::1
                 Propagate type, ?M::0 : ?M::1
                     Assignment
-                     ⊢ ?M::0 ≈ Type 2
+                     ⊢ ?M::0 ≈ (Type 2)
                         Assumption 9
                 Assignment
                  ⊢ ?M::1 ≈ Bool
                     Assumption 6
         Failed to solve
-         ⊢ Type M+1 ≺ Bool
+         ⊢ (Type M+1) ≺ Bool
             Substitution
-             ⊢ Type M+1 ≺ ?M::1
+             ⊢ (Type M+1) ≺ ?M::1
                 Propagate type, ?M::0 : ?M::1
                     Assignment
-                     ⊢ ?M::0 ≈ Type M
+                     ⊢ ?M::0 ≈ (Type M)
                         Assumption 10
                 Assignment
                  ⊢ ?M::1 ≈ Bool
                     Assumption 6
         Failed to solve
-         ⊢ Type U+1 ≺ Bool
+         ⊢ (Type U+1) ≺ Bool
             Substitution
-             ⊢ Type U+1 ≺ ?M::1
+             ⊢ (Type U+1) ≺ ?M::1
                 Propagate type, ?M::0 : ?M::1
                     Assignment
-                     ⊢ ?M::0 ≈ Type U
+                     ⊢ ?M::0 ≈ (Type U)
                         Assumption 11
                 Assignment
                  ⊢ ?M::1 ≈ Bool
diff --git a/tests/lean/norm1.lean.expected.out b/tests/lean/norm1.lean.expected.out
index 526460a0ef..84cf91d823 100644
--- a/tests/lean/norm1.lean.expected.out
+++ b/tests/lean/norm1.lean.expected.out
@@ -8,7 +8,7 @@
 λ (f : N → N) (y : N), g (f a)
 λ (a : N) (f : N → N) (g : (N → N) → N → N) (h : N → N → N) (z : N), h (g (λ x : N, f (f x)) (f a)) (f a)
 λ (a b : N) (g : Bool → N) (y : Bool), g (a == b)
-λ (a : Type) (b : a → Type) (g : Type U → Bool) (y : Type U), g (Π x : a, b x)
+λ (a : Type) (b : a → Type) (g : (Type U) → Bool) (y : (Type U)), g (Π x : a, b x)
 λ (f : N → N) (y z : N), g (f a)
 λ (f g : N → N) (y z : N), g (f a)
 λ (f : N → N) (y z : N), P (f a) y z
diff --git a/tests/lean/tst11.lean.expected.out b/tests/lean/tst11.lean.expected.out
index 72b9edd86d..65bfede331 100644
--- a/tests/lean/tst11.lean.expected.out
+++ b/tests/lean/tst11.lean.expected.out
@@ -6,7 +6,7 @@
 ⊤
   Assumed: a
 a ⊕ a ⊕ a
-Subst::explicit : Π (A : Type U) (a b : A) (P : A → Bool), P a → a == b → P b
+Subst::explicit : Π (A : (Type U)) (a b : A) (P : A → Bool), P a → a == b → P b
   Proved: EM2
 EM2 : Π a : Bool, a ∨ ¬ a
 EM2 a : a ∨ ¬ a
diff --git a/tests/lean/tst15.lean.expected.out b/tests/lean/tst15.lean.expected.out
index e027340390..c61fd88efe 100644
--- a/tests/lean/tst15.lean.expected.out
+++ b/tests/lean/tst15.lean.expected.out
@@ -1,22 +1,22 @@
   Set: pp::colors
   Set: pp::unicode
   Assumed: x
-x : Type U+3 ⊔ M+2 ⊔ 3
+x : (Type U+3 ⊔ M+2 ⊔ 3)
   Assumed: f
-f : Type U+10 → Type
+f : (Type U+10) → Type
 f x : Type
-Type 4 : Type 5
-x : Type U+3 ⊔ M+2 ⊔ 3
-Type U ⊔ M : Type U+1 ⊔ M+1
-Type U+3
-Type U+3 : Type U+4
-Type U ⊔ M : Type U+1 ⊔ M+1
-Type U ⊔ M ⊔ 3 : Type U+1 ⊔ M+1 ⊔ 4
-Type U+1 ⊔ M ⊔ 3
-Type U+1 ⊔ M ⊔ 3 : Type U+2 ⊔ M+1 ⊔ 4
-Type U → Type 5
-Type U → Type 5 : Type U+1 ⊔ 6
-Type M ⊔ 3 → Type U+5 : Type M+1 ⊔ 4 ⊔ U+6
-Type M ⊔ 3 → Type U → Type 5
-Type M ⊔ 3 → Type U → Type 5 : Type M+1 ⊔ 6 ⊔ U+1
-Type U
+(Type 4) : (Type 5)
+x : (Type U+3 ⊔ M+2 ⊔ 3)
+(Type U ⊔ M) : (Type U+1 ⊔ M+1)
+(Type U+3)
+(Type U+3) : (Type U+4)
+(Type U ⊔ M) : (Type U+1 ⊔ M+1)
+(Type U ⊔ M ⊔ 3) : (Type U+1 ⊔ M+1 ⊔ 4)
+(Type U+1 ⊔ M ⊔ 3)
+(Type U+1 ⊔ M ⊔ 3) : (Type U+2 ⊔ M+1 ⊔ 4)
+(Type U) → (Type 5)
+(Type U) → (Type 5) : (Type U+1 ⊔ 6)
+(Type M ⊔ 3) → (Type U+5) : (Type M+1 ⊔ 4 ⊔ U+6)
+(Type M ⊔ 3) → (Type U) → (Type 5)
+(Type M ⊔ 3) → (Type U) → (Type 5) : (Type M+1 ⊔ 6 ⊔ U+1)
+(Type U)
diff --git a/tests/lean/tst4.lean.expected.out b/tests/lean/tst4.lean.expected.out
index 4d9ba45f98..73eb7c872c 100644
--- a/tests/lean/tst4.lean.expected.out
+++ b/tests/lean/tst4.lean.expected.out
@@ -10,7 +10,8 @@ f::explicit ((N → N) → N → N) (λ x : N → N, x) (λ y : N → N, y)
   Assumed: EqNice
 EqNice::explicit N n1 n2
 f::explicit N n1 n2 : N
-Congr::explicit : Π (A : Type U) (B : A → Type U) (f g : Π x : A, B x) (a b : A), f == g → a == b → f a == g b
+Congr::explicit :
+    Π (A : (Type U)) (B : A → (Type U)) (f g : Π x : A, B x) (a b : A), f == g → a == b → f a == g b
 f::explicit N n1 n2
   Assumed: a
   Assumed: b