Prettyprinter fixes

docs/ProgrammingCryptol/crashCourse/CrashCourse.tex

@@ -722,8 +722,8 @@ \subsection{Comprehensions}\indComp
 \end{replinVerb}
   produces:
 \begin{reploutVerb}
-  [[(1, 1), (1, 2), (1, 3)], [(2, 1), (2, 2), (2, 3)], [(3, 1), (3,
-     2), (3, 3)]]
+  [[(1, 1), (1, 2), (1, 3)], [(2, 1), (2, 2), (2, 3)],
+   [(3, 1), (3, 2), (3, 3)]]
 \end{reploutVerb}
 The outer comprehension is a comprehension (and hence is nested). In
 particular the expression is:

src/Cryptol/Utils/PP.hs

@@ -132,7 +132,7 @@ runDoc :: NameDisp -> Doc -> PP.Doc Void
 runDoc names (Doc f) = f names
 
 instance Show Doc where
-  show d = PP.renderString (PP.layoutSmart opts (runDoc mempty d))
+  show d = PP.renderString (PP.layoutPretty opts (runDoc mempty d))
     where opts = PP.defaultLayoutOptions{ PP.layoutPageWidth = PP.AvailablePerLine 100 0.666 }
 
 instance IsString Doc where
@@ -298,8 +298,14 @@ quotes  = liftPP1 PP.squotes
 commaSep :: [Doc] -> Doc
 commaSep xs = Doc (\e -> PP.sep (PP.punctuate PP.comma [ d e | Doc d <- xs ]))
 
+-- | Print a comma-separated list. Lay out each item on a single line
+-- if it will fit. If an item requires multiple lines, then start it
+-- on its own line.
 commaSepFill :: [Doc] -> Doc
-commaSepFill xs = Doc (\e -> PP.fillSep (PP.punctuate PP.comma [ d e | Doc d <- xs ]))
+commaSepFill xs = Doc (\e -> fillSep (PP.punctuate PP.comma [ d e | Doc d <- xs ]))
+  where
+    fillSep [] = mempty
+    fillSep (d0 : ds) = foldl (\a d -> a <> PP.group (PP.line <> d)) d0 ds
 
 ppList :: [Doc] -> Doc
 ppList xs = group (nest 1 (brackets (commaSepFill xs)))

tests/issues/issue226.icry.stdout

@@ -133,8 +133,8 @@ Symbols
     fromThenTo :
       {first, next, last, a, len}
         (fin first, fin next, fin last, Literal first a, Literal next a,
-         Literal last a, first != next, lengthFromThenTo first next last ==
-         len) =>
+         Literal last a, first != next,
+         lengthFromThenTo first next last == len) =>
         [len]a
     fromTo :
       {first, last, a}

tests/issues/issue268.icry.stdout

@@ -1,9 +1,9 @@
 Loading module Cryptol
 Loading module Cryptol
 Loading module Main
-[(0x00, 0x00), (0x00, 0x00), (0x00, 0x00), (0x00, 0x00), (0x00,
-  0x00), (0x00, 0x00), (0x00, 0x00), (0x00, 0x00), (0x00, 0x00),
- (0x00, 0x00)]
-[(0x00, 0x00), (0x00, 0x00), (0x00, 0x00), (0x00, 0x00), (0x00,
-  0x00), (0x00, 0x00), (0x00, 0x00), (0x00, 0x00), (0x00, 0x00),
- (0x00, 0x00)]
+[(0x00, 0x00), (0x00, 0x00), (0x00, 0x00), (0x00, 0x00),
+ (0x00, 0x00), (0x00, 0x00), (0x00, 0x00), (0x00, 0x00),
+ (0x00, 0x00), (0x00, 0x00)]
+[(0x00, 0x00), (0x00, 0x00), (0x00, 0x00), (0x00, 0x00),
+ (0x00, 0x00), (0x00, 0x00), (0x00, 0x00), (0x00, 0x00),
+ (0x00, 0x00), (0x00, 0x00)]

tests/issues/issue407.icry.stdout

@@ -1,7 +1,8 @@
 Loading module Cryptol
-[[False, False, False, False, False, ...], [False, False, False,
-  False, True, ...], [False, False, True, True, False, ...], [False,
-  True, False, True, False, ...]]
+[[False, False, False, False, False, ...],
+ [False, False, False, False, True, ...],
+ [False, False, True, True, False, ...],
+ [False, True, False, True, False, ...]]
 Counterexample
 (\(x : [4]) -> (transpose [x ...]) @ 0 @ 0 == False) 0x8 = False
 Q.E.D.

tests/issues/padding.icry.stdout

@@ -2,5 +2,5 @@ Loading module Cryptol
 Showing a specific instance of polymorphic result:
   * Using 'Integer' for type argument 'a' of 'Cryptol::fromTo'
   * Using 'inf' for type argument 'parts' of 'Cryptol::groupBy'
-[[1, 2, 3, 4, 5], [6, 7, 8, 9, 10], [11, 12, 13, 14, 15], [16, 17,
-  18, 19, 20], [21, 22, 23, 24, 0], ...]
+[[1, 2, 3, 4, 5], [6, 7, 8, 9, 10], [11, 12, 13, 14, 15],
+ [16, 17, 18, 19, 20], [21, 22, 23, 24, 0], ...]

tests/regression/rec-update.icry.stdout

@@ -1,7 +1,7 @@
 Loading module Cryptol
 Loading module Cryptol
 Loading module Main
-[{x = 0x02, y = True}, {x = 0x03, y = True}, {x = 0x04,
-  y = False}, {x = 0x05, y = False}]
-[{x = 0x07, y = True}, {x = 0x08, y = True}, {x = 0x09,
-  y = False}, {x = 0x0a, y = False}]
+[{x = 0x02, y = True}, {x = 0x03, y = True},
+ {x = 0x04, y = False}, {x = 0x05, y = False}]
+[{x = 0x07, y = True}, {x = 0x08, y = True},
+ {x = 0x09, y = False}, {x = 0x0a, y = False}]

tests/regression/sort.icry.stdout

@@ -4,10 +4,10 @@ Loading module Cryptol
  (18, 8), (12, 9), (8, 10), (6, 11), (6, 12), (8, 13), (12, 14),
  (18, 15), (3, 16), (13, 17), (2, 18), (16, 19), (9, 20), (4, 21),
  (1, 22)]
-[(0, 0), (1, 1), (1, 22), (2, 5), (2, 18), (3, 7), (3, 16), (4,
-  2), (4, 21), (6, 11), (6, 12), (8, 10), (8, 13), (9, 3), (9, 20),
- (12, 9), (12, 14), (13, 6), (13, 17), (16, 4), (16, 19), (18, 8),
- (18, 15)]
+[(0, 0), (1, 1), (1, 22), (2, 5), (2, 18), (3, 7), (3, 16),
+ (4, 2), (4, 21), (6, 11), (6, 12), (8, 10), (8, 13), (9, 3),
+ (9, 20), (12, 9), (12, 14), (13, 6), (13, 17), (16, 4), (16, 19),
+ (18, 8), (18, 15)]
 [(1, 22), (4, 21), (9, 20), (16, 19), (2, 18), (13, 17), (3, 16),
  (18, 15), (12, 14), (8, 13), (6, 12), (6, 11), (8, 10), (12, 9),
  (18, 8), (3, 7), (13, 6), (2, 5), (16, 4), (9, 3), (4, 2), (1, 1),