From eae32b08a6939d42d6d71b7af5dc0a642ec16772 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 25 Sep 2020 20:06:18 +0200
Subject: [PATCH] fix: pretty printing multiple universe levels

Fixes #190
---
 src/Init/LeanInit.lean                   | 7 +++++--
 src/Lean/Delaborator.lean                | 4 ++--
 tests/lean/PPRoundtrip.lean              | 1 +
 tests/lean/PPRoundtrip.lean.expected.out | 1 +
 4 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/src/Init/LeanInit.lean b/src/Init/LeanInit.lean
index 58a06f5e62..655ca39587 100644
--- a/src/Init/LeanInit.lean
+++ b/src/Init/LeanInit.lean
@@ -540,13 +540,16 @@ Syntax.ident {} (toString val).toSubstring val []
 @[inline] def mkNullNode (args : Array Syntax := #[]) : Syntax :=
 Syntax.node nullKind args
 
-def mkSepStx (a : Array Syntax) (sep : Syntax) : Syntax :=
-mkNullNode $ a.iterate #[] $ fun i a r =>
+def mkSepArray (a : Array Syntax) (sep : Syntax) : Array Syntax :=
+a.iterate #[] $ fun i a r =>
   if i.val > 0 then
     (r.push sep).push a
   else
     r.push a
 
+def mkSepStx (a : Array Syntax) (sep : Syntax) : Syntax :=
+mkNullNode $ mkSepArray a sep
+
 def mkOptionalNode (arg : Option Syntax) : Syntax :=
 match arg with
 | some arg => Syntax.node nullKind #[arg]
diff --git a/src/Lean/Delaborator.lean b/src/Lean/Delaborator.lean
index a6237d243e..d1ac3bfaa1 100644
--- a/src/Lean/Delaborator.lean
+++ b/src/Lean/Delaborator.lean
@@ -320,7 +320,7 @@ ppUnivs ← getPPOption getPPUniverses;
 if ls.isEmpty || !ppUnivs then
   pure $ mkIdent c
 else
-  `($(mkIdent c).{$(ls.toArray.map quote)*})
+  `($(mkIdent c).{$(mkSepArray (ls.toArray.map quote) (mkAtom ","))*})
 
 inductive ParamKind
 | explicit
@@ -563,7 +563,7 @@ let fieldNames := getStructureFields env s.induct;
   ];
   pure (idx + 1, fields.push field)
 };
-let fields := (mkSepStx fields (mkAtom ",")).getArgs;
+let fields := mkSepArray fields (mkAtom ",");
 condM (getPPOption getPPStructureInstanceType)
   (do
     ty ← inferType e;
diff --git a/tests/lean/PPRoundtrip.lean b/tests/lean/PPRoundtrip.lean
index bc23693191..e0f91648a7 100644
--- a/tests/lean/PPRoundtrip.lean
+++ b/tests/lean/PPRoundtrip.lean
@@ -50,6 +50,7 @@ section
   set_option pp.universes true
   #eval check `(List Nat)
   #eval check `(id Nat)
+  #eval check `(Sum Nat Nat)
 end
 #eval check `(id (id Nat)) (Std.RBMap.empty.insert 4 $ KVMap.empty.insert `pp.explicit true)
 
diff --git a/tests/lean/PPRoundtrip.lean.expected.out b/tests/lean/PPRoundtrip.lean.expected.out
index 24fe7aeda7..b7049ea38d 100644
--- a/tests/lean/PPRoundtrip.lean.expected.out
+++ b/tests/lean/PPRoundtrip.lean.expected.out
@@ -12,6 +12,7 @@ List Nat
 @id Type Nat
 List.{0} Nat
 id.{2} Nat
+Sum.{0, 0} Nat Nat
 id (@id Type Nat)
 fun (a : Nat) => a
 fun (a b : Nat) => a