From 317b3c1543efb48903b777191e49918d00d31aa0 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Thu, 2 Sep 2021 16:39:03 -0700 Subject: [PATCH 1/5] Switch prettyprinter layout engine from `layoutSmart` to `layoutPretty`. This avoids an exponential slowdown that occurs with `layoutSmart` in combination with nested lists or lists of tuples. Fixes #1274. --- src/Cryptol/Utils/PP.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Cryptol/Utils/PP.hs b/src/Cryptol/Utils/PP.hs index 1e91a04ca..115535bcc 100644 --- a/src/Cryptol/Utils/PP.hs +++ b/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 From 58723d074b078bb09d0344e4ae8c2b3f127b9642 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Thu, 2 Sep 2021 16:44:44 -0700 Subject: [PATCH 2/5] Change linebreak heuristic for `commaSepFill` in the prettyprinter. The combinator is altered so that if a list item cannot be laid out on a single line, then we insert a linebreak before it so that it starts on its own line. Fixes #1275. --- src/Cryptol/Utils/PP.hs | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/Cryptol/Utils/PP.hs b/src/Cryptol/Utils/PP.hs index 115535bcc..7c14a3075 100644 --- a/src/Cryptol/Utils/PP.hs +++ b/src/Cryptol/Utils/PP.hs @@ -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))) From f25536aab362d8878117b0e20ce0cba16b225eb7 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Thu, 2 Sep 2021 17:34:12 -0700 Subject: [PATCH 3/5] Update expected test output related to #1275 fix. --- tests/issues/issue226.icry.stdout | 4 ++-- tests/issues/issue268.icry.stdout | 12 ++++++------ tests/issues/issue407.icry.stdout | 7 ++++--- tests/issues/padding.icry.stdout | 4 ++-- 4 files changed, 14 insertions(+), 13 deletions(-) diff --git a/tests/issues/issue226.icry.stdout b/tests/issues/issue226.icry.stdout index 5d1c5e2a1..94139b152 100644 --- a/tests/issues/issue226.icry.stdout +++ b/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} diff --git a/tests/issues/issue268.icry.stdout b/tests/issues/issue268.icry.stdout index 0b5cd9257..038b29cea 100644 --- a/tests/issues/issue268.icry.stdout +++ b/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)] diff --git a/tests/issues/issue407.icry.stdout b/tests/issues/issue407.icry.stdout index 9c7cff2ea..ed1d25234 100644 --- a/tests/issues/issue407.icry.stdout +++ b/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. diff --git a/tests/issues/padding.icry.stdout b/tests/issues/padding.icry.stdout index 3344bd385..4deb95178 100644 --- a/tests/issues/padding.icry.stdout +++ b/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], ...] From b9f97e77904dc6cc9a132178120491557145a149 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Thu, 2 Sep 2021 20:30:55 -0700 Subject: [PATCH 4/5] Update expected output for check-docs. --- docs/ProgrammingCryptol/crashCourse/CrashCourse.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex b/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex index bd45787aa..a2c8d4a5b 100644 --- a/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex +++ b/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: From 17260deff230c10e623e97ff1dfec8c7921da2fc Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Thu, 2 Sep 2021 21:39:08 -0700 Subject: [PATCH 5/5] Update more expected test output. --- tests/regression/rec-update.icry.stdout | 8 ++++---- tests/regression/sort.icry.stdout | 8 ++++---- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/tests/regression/rec-update.icry.stdout b/tests/regression/rec-update.icry.stdout index d54c60586..6da94fc66 100644 --- a/tests/regression/rec-update.icry.stdout +++ b/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}] diff --git a/tests/regression/sort.icry.stdout b/tests/regression/sort.icry.stdout index 6e4ef73a9..ae5fb5ab2 100644 --- a/tests/regression/sort.icry.stdout +++ b/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),