fix: pretty printing multiple universe levels

Fixes #190

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]

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;

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)
 

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