Add failing test for large vcat
[packages/pretty.git] / tests / Test.hs
1 -----------------------------------------------------------------------------
2 -- Module : HughesPJQuickCheck
3 -- Copyright : (c) 2008 Benedikt Huber
4 -- License : BSD-style
5 --
6 -- QuickChecks for HughesPJ pretty printer.
7 --
8 -- 1) Testing laws (blackbox)
9 -- - CDoc (combinator datatype)
10 -- 2) Testing invariants (whitebox)
11 -- 3) Testing bug fixes (whitebox)
12 --
13 -----------------------------------------------------------------------------
14 import PrettyTestVersion
15 import TestGenerators
16 import TestStructures
17 import TestLargePretty
18
19 import UnitPP1
20 import UnitT3911
21
22 import Control.Exception
23 import Control.Monad
24 import Data.Char (isSpace)
25 import Data.List (intersperse)
26 import Debug.Trace
27
28 import Test.QuickCheck
29
30 main :: IO ()
31 main = do
32 large_doc
33 check_laws
34 check_invariants
35 check_improvements
36 check_non_prims -- hpc full coverage
37 check_rendering
38 check_list_def
39 testPP1
40 testT3911
41
42 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
43 -- Utility functions
44 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
45
46 -- tweaked to perform many small tests
47 myConfig :: Int -> Int -> Args
48 myConfig d n = stdArgs { maxSize = d, maxDiscardRatio = n*5 }
49
50 maxTests :: Int
51 maxTests = 1000
52
53 myTest :: (Testable a) => String -> a -> IO ()
54 myTest = myTest' 15 maxTests
55
56 myTest' :: (Testable a) => Int -> Int -> String -> a -> IO ()
57 myTest' d n msg t = do
58 putStrLn (" * " ++ msg)
59 r <- quickCheckWithResult (myConfig d n) t
60 case r of
61 (Failure {}) -> error "Failed testing!"
62 _ -> return ()
63
64 myAssert :: String -> Bool -> IO ()
65 myAssert msg b = putStrLn $ (if b then "Ok, passed " else "Failed test:\n ") ++ msg
66
67 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
68 -- Ordinary tests
69 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
70
71 large_doc :: IO ()
72 large_doc = do
73 putStrLn "Testing large doc..."
74 evaluate largeDocRender
75 return ()
76
77 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
78 -- Quickcheck tests
79 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
80
81 -- Equalities on Documents
82 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
83
84 -- compare text details
85 tdEq :: TextDetails -> TextDetails -> Bool
86 tdEq td1 td2 = (tdToStr td1) == (tdToStr td2)
87
88 -- algebraic equality on reduced docs
89 docEq :: RDoc -> RDoc -> Bool
90 docEq rd1 rd2 = case (rd1, rd2) of
91 (Empty, Empty) -> True
92 (NoDoc, NoDoc) -> True
93 (NilAbove ds1, NilAbove ds2) -> docEq ds1 ds2
94 (TextBeside td1 l1 ds1, TextBeside td2 l2 ds2) | td1 `tdEq` td2 -> docEq ds1 ds2
95 (Nest k1 d1, Nest k2 d2) | k1 == k2 -> docEq d1 d2
96 (Union d11 d12, Union d21 d22) -> docEq d11 d21 && docEq d12 d22
97 (d1,d2) -> False
98
99 -- algebraic equality, with text reduction
100 deq :: Doc -> Doc -> Bool
101 deq d1 d2 = docEq (reduceDoc' d1) (reduceDoc' d2) where
102 reduceDoc' = mergeTexts . reduceDoc
103 deqs :: [Doc] -> [Doc] -> Bool
104 deqs ds1 ds2 =
105 case zipE ds1 ds2 of
106 Nothing -> False
107 (Just zds) -> all (uncurry deq) zds
108
109
110 zipLayouts :: Doc -> Doc -> Maybe [(Doc,Doc)]
111 zipLayouts d1 d2 = zipE (reducedDocs d1) (reducedDocs d2)
112 where reducedDocs = map mergeTexts . flattenDoc
113
114 zipE :: [Doc] -> [Doc] -> Maybe [(Doc, Doc)]
115 zipE l1 l2 | length l1 == length l2 = Just $ zip l1 l2
116 | otherwise = Nothing
117
118 -- algebraic equality for layouts (without permutations)
119 lseq :: Doc -> Doc -> Bool
120 lseq d1 d2 = maybe False id . fmap (all (uncurry docEq)) $ zipLayouts d1 d2
121
122 -- abstract render equality for layouts
123 -- should only be performed if the number of layouts is reasonably small
124 rdeq :: Doc -> Doc -> Bool
125 rdeq d1 d2 = maybe False id . fmap (all (uncurry layoutEq)) $ zipLayouts d1 d2
126 where layoutEq d1 d2 = (abstractLayout d1) == (abstractLayout d2)
127
128 layoutsCountBounded :: Int -> [Doc] -> Bool
129 layoutsCountBounded k docs = isBoundedBy k (concatMap flattenDoc docs)
130 where
131 isBoundedBy k [] = True
132 isBoundedBy 0 (x:xs) = False
133 isBoundedBy k (x:xs) = isBoundedBy (k-1) xs
134
135 layoutCountBounded :: Int -> Doc -> Bool
136 layoutCountBounded k doc = layoutsCountBounded k [doc]
137
138 maxLayouts :: Int
139 maxLayouts = 64
140
141 infix 4 `deq`
142 infix 4 `lseq`
143 infix 4 `rdeq`
144
145 debugRender :: Int -> Doc -> IO ()
146 debugRender k = putStr . visibleSpaces . renderStyle (Style PageMode k 1)
147 visibleSpaces = unlines . map (map visibleSpace) . lines
148
149 visibleSpace :: Char -> Char
150 visibleSpace ' ' = '.'
151 visibleSpace '.' = error "dot in visibleSpace (avoid confusion, please)"
152 visibleSpace c = c
153
154
155 -- (1) QuickCheck Properties: Laws
156 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
157
158 {-
159 Monoid laws for <>,<+>,$$,$+$
160 ~~~~~~~~~~~~~
161 <a,b 1> (x * y) * z = x * (y * z)
162 <a,b 2> empty * x = x
163 <a,b 3> x * empty = x
164 -}
165 prop_1 op x y z = classify (any isEmpty [x,y,z]) "empty x, y or z" $
166 ((x `op` y) `op` z) `deq` (x `op` (y `op` z))
167 prop_2 op x = classify (isEmpty x) "empty" $ (empty `op` x) `deq` x
168 prop_3 op x = classify (isEmpty x) "empty" $ x `deq` (empty `op` x)
169
170 check_monoid = do
171 putStrLn " = Monoid Laws ="
172 mapM_ (myTest' 5 maxTests "Associativity") [ liftDoc3 (prop_1 op) | op <- allops ]
173 mapM_ (myTest "Left neutral") [ prop_2 op . buildDoc | op <- allops ]
174 mapM_ (myTest "Right neutral") [ prop_3 op . buildDoc | op <- allops ]
175 where
176 allops = [ (<>), (<+>) ,($$) , ($+$) ]
177
178 {-
179 Laws for text
180 ~~~~~~~~~~~~~
181 <t1> text s <> text t = text (s++t)
182 <t2> text "" <> x = x, if x non-empty [only true if x does not start with nest, because of <n6> ]
183 -}
184 prop_t1 s t = text' s <> text' t `deq` text (unText s ++ unText t)
185 prop_t2 x = not (isEmpty x) ==> text "" <> x `deq` x
186 prop_t2_a x = not (isEmpty x) && not (isNest x) ==> text "" <> x `deq` x
187
188 isNest :: Doc -> Bool
189 isNest d = case reduceDoc d of
190 (Nest _ _) -> True
191 (Union d1 d2) -> isNest d1 || isNest d2
192 _ -> False
193
194 check_t = do
195 putStrLn " = Text laws ="
196 myTest "t1" prop_t1
197 myTest "t2_a (precondition: x does not start with nest)" (prop_t2_a . buildDoc)
198 myTest "t_2 (Known to fail)" (expectFailure . prop_t2 . buildDoc)
199
200 {-
201 Laws for nest
202 ~~~~~~~~~~~~~
203 <n1> nest 0 x = x
204 <n2> nest k (nest k' x) = nest (k+k') x
205 <n3> nest k (x <> y) = nest k z <> nest k y
206 <n4> nest k (x $$ y) = nest k x $$ nest k y
207 <n5> nest k empty = empty
208 <n6> x <> nest k y = x <> y, if x non-empty
209 -}
210 prop_n1 x = nest 0 x `deq` x
211 prop_n2 k k' x = nest k (nest k' x) `deq` nest (k+k') x
212 prop_n3 k k' x = nest k (nest k' x) `deq` nest (k+k') x
213 prop_n4 k x y = nest k (x $$ y) `deq` nest k x $$ nest k y
214 prop_n5 k = nest k empty `deq` empty
215 prop_n6 x k y = not (isEmpty x) ==>
216 x <> nest k y `deq` x <> y
217 check_n = do
218 putStrLn "Nest laws"
219 myTest "n1" (prop_n1 . buildDoc)
220 myTest "n2" (\k k' -> prop_n2 k k' . buildDoc)
221 myTest "n3" (\k k' -> prop_n3 k k' . buildDoc)
222 myTest "n4" (\k -> liftDoc2 (prop_n4 k))
223 myTest "n5" prop_n5
224 myTest "n6" (\k -> liftDoc2 (\x -> prop_n6 x k))
225
226 {-
227 <m1> (text s <> x) $$ y = text s <> ((text "" <> x)) $$
228 nest (-length s) y)
229
230 <m2> (x $$ y) <> z = x $$ (y <> z)
231 if y non-empty
232 -}
233 prop_m1 s x y = (text' s <> x) $$ y `deq` text' s <> ((text "" <> x) $$
234 nest (-length (unText s)) y)
235 prop_m2 x y z = not (isEmpty y) ==>
236 (x $$ y) <> z `deq` x $$ (y <> z)
237 check_m = do
238 putStrLn "Misc laws"
239 myTest "m1" (\s -> liftDoc2 (prop_m1 s))
240 myTest' 10 maxTests "m2" (liftDoc3 prop_m2)
241
242
243 {-
244 Laws for list versions
245 ~~~~~~~~~~~~~~~~~~~~~~
246 <l1> sep (ps++[empty]++qs) = sep (ps ++ qs)
247 ...ditto hsep, hcat, vcat, fill...
248 [ Fails for fill ! ]
249 <l2> nest k (sep ps) = sep (map (nest k) ps)
250 ...ditto hsep, hcat, vcat, fill...
251 -}
252 prop_l1 sp ps qs =
253 sp (ps++[empty]++qs) `rdeq` sp (ps ++ qs)
254 prop_l2 sp k ps = nest k (sep ps) `deq` sep (map (nest k) ps)
255
256
257 prop_l1' sp cps cqs =
258 let [ps,qs] = map buildDocList [cps,cqs] in
259 layoutCountBounded maxLayouts (sp (ps++qs)) ==> prop_l1 sp ps qs
260 prop_l2' sp k ps = prop_l2 sp k (buildDocList ps)
261 check_l = do
262 allCats $ myTest "l1" . prop_l1'
263 allCats $ myTest "l2" . prop_l2'
264 where
265 allCats = flip mapM_ [ sep, hsep, cat, hcat, vcat, fsep, fcat ]
266 prop_l1_fail_1 = [ text "a" ]
267 prop_l1_fail_2 = [ text "a" $$ text "b" ]
268
269 {-
270 Laws for oneLiner
271 ~~~~~~~~~~~~~~~~~
272 <o1> oneLiner (nest k p) = nest k (oneLiner p)
273 <o2> oneLiner (x <> y) = oneLiner x <> oneLiner y
274
275 [One liner only takes reduced arguments]
276 -}
277 oneLinerR = oneLiner . reduceDoc
278 prop_o1 k p = oneLinerR (nest k p) `deq` nest k (oneLinerR p)
279 prop_o2 x y = oneLinerR (x <> y) `deq` oneLinerR x <> oneLinerR y
280
281 check_o = do
282 putStrLn "oneliner laws"
283 myTest "o1 (RDoc arg)" (\k p -> prop_o1 k (buildDoc p))
284 myTest "o2 (RDoc arg)" (liftDoc2 prop_o2)
285
286 {-
287 Definitions of list versions
288 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
289 <ldef1> vcat = foldr ($$) empty
290 <ldef2> hcat = foldr (<>) empty
291 <ldef3> hsep = foldr (<+>) empty
292 -}
293 prop_hcat :: [Doc] -> Bool
294 prop_hcat ds = hcat ds `deq` (foldr (<>) empty) ds
295
296 prop_hsep :: [Doc] -> Bool
297 prop_hsep ds = hsep ds `deq` (foldr (<+>) empty) ds
298
299 prop_vcat :: [Doc] -> Bool
300 prop_vcat ds = vcat ds `deq` (foldr ($$) empty) ds
301
302 {-
303 Update (pretty-1.1.0):
304 *failing* definition of sep: oneLiner (hsep ps) `union` vcat ps
305 <ldef4> ?
306 -}
307 prop_sep :: [Doc] -> Bool
308 prop_sep ds = sep ds `rdeq` (sepDef ds)
309
310 sepDef :: [Doc] -> Doc
311 sepDef docs = let ds = filter (not . isEmpty) docs in
312 case ds of
313 [] -> empty
314 [d] -> d
315 ds -> reduceDoc (oneLiner (reduceDoc $ hsep ds)
316 `Union`
317 (reduceDoc $ foldr ($+$) empty ds))
318
319 check_list_def = do
320 myTest "hcat def" (prop_hcat . buildDocList)
321 myTest "hsep def" (prop_hsep . buildDocList)
322 myTest "vcat def" (prop_vcat . buildDocList)
323 -- XXX: Not sure if this is meant to fail (I added the expectFailure [DT])
324 myTest "sep def" (expectFailure . prop_sep . buildDocList)
325
326 {-
327 Definition of fill (fcat/fsep)
328 -- Specification:
329 -- fill [] = empty
330 -- fill [p] = p
331 -- fill (p1:p2:ps) = oneLiner p1 <#> nest (length p1)
332 -- (fill (oneLiner p2 : ps))
333 -- `union`
334 -- p1 $$ fill ps
335 -- Revised Specification:
336 -- fill g docs = fillIndent 0 docs
337 --
338 -- fillIndent k [] = []
339 -- fillIndent k [p] = p
340 -- fillIndent k (p1:p2:ps) =
341 -- oneLiner p1 <g> fillIndent (k + length p1 + g ? 1 : 0) (remove_nests (oneLiner p2) : ps)
342 -- `Union`
343 -- (p1 $*$ nest (-k) (fillIndent 0 ps))
344 --
345 -- $*$ is defined for layouts (not Docs) as
346 -- layout1 $*$ layout2 | isOneLiner layout1 = layout1 $+$ layout2
347 -- | otherwise = layout1 $$ layout2
348 --
349 -- Old implementation ambiguities/problems:
350 -- ========================================
351 -- Preserving nesting:
352 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
353 -- fcat [cat[ text "b", text "a"], nest 2 ( text "" $$ text "a")]
354 -- ==> fcat [ text "b" $$ text "a", nest 2 (text "" $$ text "a")] // cat: union right
355 -- ==> (text "b" $$ text "a" $$ nest 2 (text "" $$ text "a")) // fcat: union right with overlap
356 -- ==> (text "ab" $$ nest 2 (text "" $$ text "a"))
357 -- ==> "b\na\n..a"
358 -- Bug #1337:
359 -- ~~~~~~~~~~
360 -- > fcat [ nest 1 $ text "a", nest 2 $ text "b", text "c"]
361 -- ==> [second alternative] roughly (a <#> b $#$ c)
362 -- " ab"
363 -- "c "
364 -- expected: (nest 1; text "a"; text "b"; nest -3; "c")
365 -- actual : (nest 1; text "a"; text "b"; nest -5; "c")
366 -- === (nest 1; text a) <> (fill (-2) (p2:ps))
367 -- ==> (nest 2 (text "b") $+$ text "c")
368 -- ==> (nest 2 (text "b") `nilabove` nest (-3) (text "c"))
369 -- ==> (nest 1; text a; text b; nest -5 c)
370
371 -}
372 prop_fcat_vcat :: [Doc] -> Bool
373 prop_fcat_vcat ds = last (flattenDoc $ fcat ds) `deq` last (flattenDoc $ vcat ds)
374
375 prop_fcat :: [Doc] -> Bool
376 prop_fcat ds = fcat ds `rdeq` fillDef False (filter (not . isEmpty) ds)
377
378 prop_fsep :: [Doc] -> Bool
379 prop_fsep ds = fsep ds `rdeq` fillDef True (filter (not . isEmpty) ds)
380
381 prop_fcat_old :: [Doc] -> Bool
382 prop_fcat_old ds = fillOld2 False ds `rdeq` fillDef False (filter (not . isEmpty) ds)
383
384 prop_fcat_old_old :: [Doc] -> Bool
385 prop_fcat_old_old ds = fillOld2 False ds `rdeq` fillDefOld False (filter (not . isEmpty) ds)
386
387 prop_restrict_sz :: (Testable a) => Int -> ([Doc] -> a) -> ([Doc] -> Property)
388 prop_restrict_sz k p ds = layoutCountBounded k (fsep ds) ==> p ds
389
390 prop_restrict_ol :: (Testable a) => ([Doc] -> a) -> ([Doc] -> Property)
391 prop_restrict_ol p ds = (all isOneLiner . map normalize $ ds) ==> p ds
392
393 prop_restrict_no_nest_start :: (Testable a) => ([Doc] -> a) -> ([Doc] -> Property)
394 prop_restrict_no_nest_start p ds = (all (not .isNest) ds) ==> p ds
395
396 fillDef :: Bool -> [Doc] -> Doc
397 fillDef g = normalize . fill' 0 . filter (not.isEmpty) . map reduceDoc
398 where
399 fill' _ [] = Empty
400 fill' _ [x] = x
401 fill' k (p1:p2:ps) =
402 reduceDoc (oneLiner p1 `append` (fill' (k + firstLineLength p1 + (if g then 1 else 0)) $ (oneLiner' p2) : ps))
403 `union`
404 reduceDoc (p1 $*$ (nest (-k) (fillDef g (p2:ps))))
405
406 union = Union
407
408 append = if g then (<+>) else (<>)
409
410 oneLiner' (Nest k d) = oneLiner' d
411 oneLiner' d = oneLiner d
412
413 ($*$) :: RDoc -> RDoc -> RDoc
414 ($*$) p ps = case flattenDoc p of
415 [] -> NoDoc
416 ls -> foldr1 Union (map combine ls)
417 where
418 combine p | isOneLiner p = p $+$ ps
419 | otherwise = p $$ ps
420
421 fillDefOld :: Bool -> [Doc] -> Doc
422 fillDefOld g = normalize . fill' . filter (not.isEmpty) . map normalize where
423 fill' [] = Empty
424 fill' [p1] = p1
425 fill' (p1:p2:ps) = (normalize (oneLiner p1 `append` nest (firstLineLength p1)
426 (fill' (oneLiner p2 : ps))))
427 `union`
428 (p1 $$ fill' (p2:ps))
429 append = if g then (<+>) else (<>)
430 union = Union
431
432 check_fill_prop :: Testable a => String -> ([Doc] -> a) -> IO ()
433 check_fill_prop msg p = myTest msg (prop_restrict_sz maxLayouts p . buildDocList)
434
435 check_fill_def_fail :: IO ()
436 check_fill_def_fail = do
437 check_fill_prop "fcat defOld vs fcatOld (ol)" (prop_restrict_ol prop_fcat_old_old)
438 check_fill_prop "fcat defOld vs fcatOld" prop_fcat_old_old
439
440 check_fill_prop "fcat def (ol) vs fcatOld" (prop_restrict_ol prop_fcat_old)
441 check_fill_prop "fcat def vs fcatOld" prop_fcat_old
442
443 check_fill_def_ok :: IO ()
444 check_fill_def_ok = do
445 check_fill_prop "fcat def (not nest start) vs fcatOld" (prop_restrict_no_nest_start prop_fcat_old)
446
447 check_fill_prop "fcat def (not nest start) vs fcat" (prop_restrict_no_nest_start prop_fcat)
448 -- XXX: These all fail now with the change of pretty to GHC behaviour.
449 check_fill_prop "fcat def (ol) vs fcat" (expectFailure . prop_restrict_ol prop_fcat)
450 check_fill_prop "fcat def vs fcat" (expectFailure . prop_fcat)
451 check_fill_prop "fsep def vs fsep" (expectFailure . prop_fsep)
452
453
454 check_fill_def_laws :: IO ()
455 check_fill_def_laws = do
456 check_fill_prop "lastLayout (fcat ps) == vcat ps" prop_fcat_vcat
457
458 check_fill_def :: IO ()
459 check_fill_def = check_fill_def_fail >> check_fill_def_ok
460 {-
461 text "ac"; nilabove; nest -1; text "a"; empty
462 text "ac"; nilabove; nest -2; text "a"; empty
463 -}
464
465 {-
466 Zero width text (Neil)
467
468 Here it would be convenient to generate functions (or replace empty / text bz z-w-t)
469 -}
470 -- TODO
471 {-
472 All laws: monoid, text, nest, misc, list versions, oneLiner, list def
473 -}
474 check_laws :: IO ()
475 check_laws = do
476 check_fill_def_ok
477 check_monoid
478 check_t
479 check_n
480 check_m
481 check_l
482 check_o
483 check_list_def
484
485 -- (2) QuickCheck Properties: Invariants (whitebox)
486 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
487
488 -- strategies: synthesize with stop condition
489 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
490 stop :: a -> (a, Bool)
491 stop a = (a,False)
492
493 recurse :: a -> (a, Bool)
494 recurse a = (a,True)
495 -- strategy: generic synthesize with stop condition
496 -- terms are combined top-down, left-right (latin text order)
497 genericProp :: (a -> a -> a) -> (Doc -> (a,Bool)) -> Doc -> a
498 genericProp c q doc =
499 case q doc of
500 (v,False) -> v
501 (v,True) -> foldl c v (subs doc)
502 where
503 rec = genericProp c q
504 subs d = case d of
505 Empty -> []
506 NilAbove d -> [rec d]
507 TextBeside _ _ d -> [rec d]
508 Nest _ d -> [rec d]
509 Union d1 d2 -> [rec d1, rec d2]
510 NoDoc -> []
511 Beside d1 _ d2 -> subs (reduceDoc d)
512 Above d1 _ d2 -> subs (reduceDoc d)
513
514
515 {-
516 * The argument of NilAbove is never Empty. Therefore
517 a NilAbove occupies at least two lines.
518 -}
519 prop_inv1 :: Doc -> Bool
520 prop_inv1 d = genericProp (&&) nilAboveNotEmpty d where
521 nilAboveNotEmpty (NilAbove Empty) = stop False
522 nilAboveNotEmpty _ = recurse True
523
524 {-
525 * The argument of @TextBeside@ is never @Nest@.
526 -}
527 prop_inv2 :: Doc -> Bool
528 prop_inv2 = genericProp (&&) textBesideNotNest where
529 textBesideNotNest (TextBeside _ _ (Nest _ _)) = stop False
530 textBesideNotNest _ = recurse True
531 {-
532 * The layouts of the two arguments of @Union@ both flatten to the same
533 string
534 -}
535 prop_inv3 :: Doc -> Bool
536 prop_inv3 = genericProp (&&) unionsFlattenSame where
537 unionsFlattenSame (Union d1 d2) = stop (pairwiseEqual (extractTexts d1 ++ extractTexts d2))
538 unionsFlattenSame _ = recurse True
539 pairwiseEqual (x:y:zs) = x==y && pairwiseEqual (y:zs)
540 pairwiseEqual _ = True
541
542
543 {-
544 * The arguments of @Union@ are either @TextBeside@, or @NilAbove@.
545 -}
546 prop_inv4 :: Doc -> Bool
547 prop_inv4 = genericProp (&&) unionArgs where
548 unionArgs (Union d1 d2) | goodUnionArg d1 && goodUnionArg d2 = recurse True
549 | otherwise = stop False
550 unionArgs _ = recurse True
551 goodUnionArg (TextBeside _ _ _) = True
552 goodUnionArg (NilAbove _) = True
553 goodUnionArg _ = False
554
555 {-
556 * A @NoDoc@ may only appear on the first line of the left argument of
557 an union. Therefore, the right argument of an union can never be equivalent
558 to the empty set.
559 -}
560 prop_inv5 :: Doc -> Bool
561 prop_inv5 = genericProp (&&) unionArgs . reduceDoc where
562 unionArgs NoDoc = stop False
563 unionArgs (Union d1 d2) = stop $ genericProp (&&) noDocIsFirstLine d1 && nonEmptySet (reduceDoc d2)
564 unionArgs _ = (True,True) -- recurse
565 noDocIsFirstLine (NilAbove d) = stop $ genericProp (&&) unionArgs d
566 noDocIsFirstLine _ = recurse True
567
568 {-
569 * An empty document is always represented by @Empty@. It can't be
570 hidden inside a @Nest@, or a @Union@ of two @Empty@s.
571 -}
572 prop_inv6 :: Doc -> Bool
573 prop_inv6 d | not (prop_inv1 d) || not (prop_inv2 d) = False
574 | not (isEmptyDoc d) = True
575 | otherwise = case d of Empty -> True ; _ -> False
576
577 isEmptyDoc :: Doc -> Bool
578 isEmptyDoc d = case emptyReduction d of Empty -> True; _ -> False
579
580 {-
581 * Consistency
582 If all arguments of one of the list versions are empty documents, the list is an empty document
583 -}
584 prop_inv6a :: ([Doc] -> Doc) -> Property
585 prop_inv6a sep = forAll emptyDocListGen $
586 \ds -> isEmptyRepr (sep $ buildDocList ds)
587 where
588 isEmptyRepr Empty = True
589 isEmptyRepr _ = False
590
591 {-
592 * The first line of every layout in the left argument of @Union@ is
593 longer than the first line of any layout in the right argument.
594 (1) ensures that the left argument has a first line. In view of
595 (3), this invariant means that the right argument must have at
596 least two lines.
597 -}
598 counterexample_inv7 = cat [ text " ", nest 2 ( text "a") ]
599
600 prop_inv7 :: Doc -> Bool
601 prop_inv7 = genericProp (&&) firstLonger where
602 firstLonger (Union d1 d2) = (firstLineLength d1 >= firstLineLength d2, True)
603 firstLonger _ = (True, True)
604
605 {-
606 * If we take as precondition: the arguments of cat,sep,fill do not start with Nest, invariant 7 holds
607 -}
608 prop_inv7_pre :: CDoc -> Bool
609 prop_inv7_pre cdoc = nestStart True cdoc where
610 nestStart nestOk doc =
611 case doc of
612 CList sep ds -> all (nestStart False) ds
613 CBeside _ d1 d2 -> nestStart nestOk d1 && nestStart (not . isEmpty $ buildDoc d1) d2
614 CAbove _ d1 d2 -> nestStart nestOk d1 && nestStart (not . isEmpty $ buildDoc d1) d2
615 CNest _ d | not nestOk -> False
616 | otherwise -> nestStart True d
617 _empty_or_text -> True
618
619 {-
620 inv7_pre ==> inv7
621 -}
622 prop_inv7_a :: CDoc -> Property
623 prop_inv7_a cdoc = prop_inv7_pre cdoc ==> prop_inv7 (buildDoc cdoc)
624
625 check_invariants :: IO ()
626 check_invariants = do
627 myTest "Invariant 1" (prop_inv1 . buildDoc)
628 myTest "Invariant 2" (prop_inv2 . buildDoc)
629 myTest "Invariant 3" (prop_inv3 . buildDoc)
630 myTest "Invariant 4" (prop_inv4 . buildDoc)
631 myTest "Invariant 5+" (prop_inv5 . buildDoc)
632 myTest "Invariant 6" (prop_inv6 . buildDoc)
633 mapM_ (\sp -> myTest "Invariant 6a" $ prop_inv6a sp) [ cat, sep, fcat, fsep, vcat, hcat, hsep ]
634 -- XXX: Not sure if this is meant to fail (I added the expectFailure [DT])
635 myTest "Invariant 7 (fails in HughesPJ:20080621)" (expectFailure . prop_inv7 . buildDoc)
636
637 -- `negative indent'
638 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
639
640 {-
641 In the documentation we have:
642
643 (spaces n) generates a list of n spaces
644 It should never be called with 'n' < 0, but that can happen for reasons I don't understand
645
646 This is easy to explain:
647 Suppose we have layout1 <> layout2
648 length of last line layout1 is k1
649 indentation of first line of layout2 is k2
650 indentation of some other line of layout2 is k2'
651 Now layout1 <> nest k2 (line1 $$ nest k2' lineK)
652 ==> layout1 <> (line1 $$ nest k2' lineK)
653 When k1 - k2' < 0, we need to layout lineK with negative indentation
654
655 Here is a quick check property to ducment this.
656 -}
657 prop_negative_indent :: CDoc -> Property
658 prop_negative_indent cdoc = noNegNest cdoc ==> noNegSpaces (buildDoc cdoc)
659 noNegNest = genericCProp (&&) notIsNegNest where
660 notIsNegNest (CNest k _) | k < 0 = stop False
661 notIsNegNest _ = recurse True
662 noNegSpaces = go 0 . reduceDoc where
663 go k Empty = True
664 go k (NilAbove d) = go k d
665 go k (TextBeside _ s d) | k < 0 = False
666 go k (TextBeside _ s d) = go (k+s) d
667 go k (Nest k' d) = go (k+k') d
668 go k (Union d1 d2) = (if nonEmptySet d1 then (&&) (go k d1) else id) (go k d2)
669 go k NoDoc = True
670
671 counterexample_fail9 :: Doc
672 counterexample_fail9 = text "a" <> ( nest 2 ( text "b") $$ text "c")
673 -- reduces to textb "a" ; textb "b" ; nilabove ; nest -3 ; textb "c" ; empty
674
675 {-
676 This cannot be fixed with violating the "intuitive property of layouts", described by John Hughes:
677 "Composing layouts should preserve the layouts themselves (i.e. translation)"
678
679 Consider the following example:
680 It is the user's fault to use <+> in t2.
681 -}
682
683 tstmt = (nest 6 $ text "/* double indented comment */") $+$
684 (nest 3 $ text "/* indented comment */") $+$
685 text "skip;"
686
687 t1 = text "while(true)" $+$ (nest 2) tstmt
688 {-
689 while(true)
690 /* double indented comment */
691 /* indented comment */
692 skip;
693 -}
694 t2 = text "while(true)" $+$ (nest 2 $ text "//" <+> tstmt)
695 {-
696 while(true)
697 // /* double indented comment */
698 /* indented comment */
699 skip;
700 -}
701
702 -- (3) Touching non-prims
703 -- ~~~~~~~~~~~~~~~~~~~~~~
704
705 check_non_prims :: IO ()
706 check_non_prims = do
707 myTest "Non primitive: show = renderStyle style" $ \cd -> let d = buildDoc cd in
708 show ((zeroWidthText "a") <> d) /= renderStyle style d
709 myAssert "symbols" $
710 (semi <> comma <> colon <> equals <> lparen <> rparen <> lbrack <> rbrack <> lbrace <> rbrace)
711 `deq`
712 (text ";,:=()[]{}")
713 myAssert "quoting" $
714 (quotes . doubleQuotes . parens . brackets .braces $ (text "a" $$ text "b"))
715 `deq`
716 (text "'\"([{" <> (text "a" $$ text "b") <> text "}])\"'")
717 myAssert "numbers" $
718 fsep [int 42, integer 42, float 42, double 42, rational 42]
719 `rdeq`
720 (fsep . map text)
721 [show (42 :: Int), show (42 :: Integer), show (42 :: Float), show (42 :: Double), show (42 :: Rational)]
722 myTest "Definition of <+>" $ \cd1 cd2 ->
723 let (d1,d2) = (buildDoc cd1, buildDoc cd2) in
724 layoutsCountBounded maxLayouts [d1,d2] ==>
725 not (isEmpty d1) && not (isEmpty d2) ==>
726 d1 <+> d2 `rdeq` d1 <> space <> d2
727
728 myTest "hang" $ liftDoc2 (\d1 d2 -> hang d1 2 d2 `deq` sep [d1, nest 2 d2])
729
730 let pLift f cp cds = f (buildDoc cp) (buildDocList cds)
731 myTest "punctuate" $ pLift (\p ds -> (punctuate p ds) `deqs` (punctuateDef p ds))
732
733 check_rendering = do
734 myTest' 20 10000 "one - line rendering" $ \cd ->
735 let d = buildDoc cd in
736 (renderStyle (Style OneLineMode undefined undefined) d) == oneLineRender d
737 myTest' 20 10000 "left-mode rendering" $ \cd ->
738 let d = buildDoc cd in
739 extractText (renderStyle (Style LeftMode undefined undefined) d) == extractText (oneLineRender d)
740 myTest' 20 10000 "page mode rendering" $ \cd ->
741 let d = buildDoc cd in
742 extractText (renderStyle (Style PageMode 6 1.7) d) == extractText (oneLineRender d)
743 myTest' 20 10000 "zigzag mode rendering" $ \cd ->
744 let d = buildDoc cd in
745 extractTextZZ (renderStyle (Style ZigZagMode 6 1.7) d) == extractText (oneLineRender d)
746
747 extractText :: String -> String
748 extractText = filter (not . isSpace)
749
750 extractTextZZ :: String -> String
751 extractTextZZ = filter (\c -> not (isSpace c) && c /= '/' && c /= '\\')
752
753 punctuateDef :: Doc -> [Doc] -> [Doc]
754 punctuateDef p [] = []
755 punctuateDef p ps =
756 let (dsInit,dLast) = (init ps, last ps) in
757 map (\d -> d <> p) dsInit ++ [dLast]
758
759 -- (4) QuickChecking improvments and bug fixes
760 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
761
762 {-
763 putStrLn $ render' $ fill True [ text "c", text "c",empty, text "c", text "b"]
764 c c c
765 b
766 putStrLn $ render' $ fillOld True [ text "c", text "c",empty, text "c", text "b"]
767 c c c
768 b
769 -}
770 prop_fill_empty_reduce :: [Doc] -> Bool
771 prop_fill_empty_reduce ds = fill True ds `deq` fillOld True (filter (not.isEmpty.reduceDoc) ds)
772
773 check_improvements :: IO ()
774 check_improvements = do
775 myTest "fill = fillOld . filter (not.isEmpty) [if no argument starts with nest]"
776 (prop_fill_empty_reduce . filter (not .isNest) . buildDocList)
777
778 -- old implementation of fill
779 fillOld :: Bool -> [Doc] -> RDoc
780 fillOld _ [] = empty
781 fillOld g (p:ps) = fill1 g (reduceDoc p) 0 ps where
782 fill1 :: Bool -> RDoc -> Int -> [Doc] -> Doc
783 fill1 _ _ k _ | k `seq` False = undefined
784 fill1 _ NoDoc _ _ = NoDoc
785 fill1 g (p `Union` q) k ys = fill1 g p k ys
786 `union_`
787 (aboveNest q False k (fillOld g ys))
788
789 fill1 g Empty k ys = mkNest k (fillOld g ys)
790 fill1 g (Nest n p) k ys = nest_ n (fill1 g p (k - n) ys)
791
792 fill1 g (NilAbove p) k ys = nilAbove_ (aboveNest p False k (fillOld g ys))
793 fill1 g (TextBeside s sl p) k ys = textBeside_ s sl (fillNB g p (k - sl) ys)
794 fill1 _ (Above {}) _ _ = error "fill1 Above"
795 fill1 _ (Beside {}) _ _ = error "fill1 Beside"
796 -- fillNB gap textBesideArgument space_left docs
797 fillNB :: Bool -> Doc -> Int -> [Doc] -> Doc
798 fillNB _ _ k _ | k `seq` False = undefined
799 fillNB g (Nest _ p) k ys = fillNB g p k ys
800 fillNB _ Empty _ [] = Empty
801 fillNB g Empty k (y:ys) = nilBeside g (fill1 g (oneLiner (reduceDoc y)) k1 ys)
802 `mkUnion`
803 nilAboveNest False k (fillOld g (y:ys))
804 where
805 k1 | g = k - 1
806 | otherwise = k
807 fillNB g p k ys = fill1 g p k ys
808
809
810 -- Specification:
811 -- fill [] = empty
812 -- fill [p] = p
813 -- fill (p1:p2:ps) = oneLiner p1 <#> nest (length p1)
814 -- (fill (oneLiner p2 : ps))
815 -- `union`
816 -- p1 $$ fill ps
817 fillOld2 :: Bool -> [Doc] -> RDoc
818 fillOld2 _ [] = empty
819 fillOld2 g (p:ps) = fill1 g (reduceDoc p) 0 ps where
820 fill1 :: Bool -> RDoc -> Int -> [Doc] -> Doc
821 fill1 _ _ k _ | k `seq` False = undefined
822 fill1 _ NoDoc _ _ = NoDoc
823 fill1 g (p `Union` q) k ys = fill1 g p k ys
824 `union_`
825 (aboveNest q False k (fill g ys))
826
827 fill1 g Empty k ys = mkNest k (fill g ys)
828 fill1 g (Nest n p) k ys = nest_ n (fill1 g p (k - n) ys)
829
830 fill1 g (NilAbove p) k ys = nilAbove_ (aboveNest p False k (fill g ys))
831 fill1 g (TextBeside s sl p) k ys = textBeside_ s sl (fillNB g p (k - sl) ys)
832 fill1 _ (Above {}) _ _ = error "fill1 Above"
833 fill1 _ (Beside {}) _ _ = error "fill1 Beside"
834
835 fillNB :: Bool -> Doc -> Int -> [Doc] -> Doc
836 fillNB _ _ k _ | k `seq` False = undefined
837 fillNB g (Nest _ p) k ys = fillNB g p k ys
838 fillNB _ Empty _ [] = Empty
839 fillNB g Empty k (Empty:ys) = fillNB g Empty k ys
840 fillNB g Empty k (y:ys) = fillNBE g k y ys
841 fillNB g p k ys = fill1 g p k ys
842
843 fillNBE g k y ys = nilBeside g (fill1 g (oneLiner (reduceDoc y)) k1 ys)
844 `mkUnion`
845 nilAboveNest True k (fill g (y:ys))
846 where
847 k1 | g = k - 1
848 | otherwise = k
849
850 -- (5) Pretty printing RDocs and RDOC properties
851 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
852 prettyDoc :: Doc -> Doc
853 prettyDoc d =
854 case reduceDoc d of
855 Empty -> text "empty"
856 NilAbove d -> (text "nilabove") <> semi <+> (prettyDoc d)
857 TextBeside s sl d -> (text ("text \""++tdToStr s ++ "\"" ++ show sl)) <> semi <+> (prettyDoc d)
858 Nest k d -> text "nest" <+> integer (fromIntegral k) <> semi <+> prettyDoc d
859 Union d1 d2 -> sep [text "union", parens (prettyDoc d1), parens (prettyDoc d2)]
860 NoDoc -> text "nodoc"
861
862 -- TODO: map strategy for Docs to avoid code duplication
863 -- Debug: Doc -> [Layout]
864 flattenDoc :: Doc -> [RDoc]
865 flattenDoc d = flatten (reduceDoc d) where
866 flatten NoDoc = []
867 flatten Empty = return Empty
868 flatten (NilAbove d) = map NilAbove (flatten d)
869 flatten (TextBeside s sl d) = map (TextBeside s sl) (flatten d)
870 flatten (Nest k d) = map (Nest k) (flatten d)
871 flatten (Union d1 d2) = flattenDoc d1 ++ flattenDoc d2
872 flatten (Beside d1 b d2) = error $ "flattenDoc Beside"
873 flatten (Above d1 b d2) = error $ "flattenDoc Above"
874
875 normalize :: Doc -> RDoc
876 normalize d = norm d where
877 norm NoDoc = NoDoc
878 norm Empty = Empty
879 norm (NilAbove d) = NilAbove (norm d)
880 norm (TextBeside s sl (Nest k d)) = norm (TextBeside s sl d)
881 norm (TextBeside s sl d) = (TextBeside s sl) (norm d)
882 norm (Nest k (Nest k' d)) = norm $ Nest (k+k') d
883 norm (Nest 0 d) = norm d
884 norm (Nest k d) = (Nest k) (norm d)
885 -- * The arguments of @Union@ are either @TextBeside@, or @NilAbove@.
886 norm (Union d1 d2) = normUnion (norm d1) (norm d2)
887 norm d@(Beside d1 b d2) = norm (reduceDoc d)
888 norm d@(Above d1 b d2) = norm (reduceDoc d)
889 normUnion d0@(Nest k d) (Union d1 d2) = norm (Union d0 (normUnion d1 d2))
890 normUnion (Union d1 d2) d3@(Nest k d) = norm (Union (normUnion d1 d2) d3)
891 normUnion (Nest k d1) (Nest k' d2) | k == k' = Nest k $ Union (norm d1) (norm d2)
892 | otherwise = error "normalize: Union Nest length mismatch ?"
893 normUnion (Nest _ _) d2 = error$ "normUnion Nest "++topLevelCTor d2
894 normUnion d1 (Nest _ _) = error$ "normUnion Nset "++topLevelCTor d1
895 normUnion p1 p2 = Union p1 p2
896
897 topLevelCTor :: Doc -> String
898 topLevelCTor d = tlc d where
899 tlc NoDoc = "NoDoc"
900 tlc Empty = "Empty"
901 tlc (NilAbove d) = "NilAbove"
902 tlc (TextBeside s sl d) = "TextBeside"
903 tlc (Nest k d) = "Nest"
904 tlc (Union d1 d2) = "Union"
905 tlc (Above _ _ _) = "Above"
906 tlc (Beside _ _ _) = "Beside"
907
908 -- normalize TextBeside (and consequently apply some laws for simplification)
909 mergeTexts :: RDoc -> RDoc
910 mergeTexts = merge where
911 merge NoDoc = NoDoc
912 merge Empty = Empty
913 merge (NilAbove d) = NilAbove (merge d)
914 merge (TextBeside t1 l1 (TextBeside t2 l2 doc)) = (merge.normalize) (TextBeside (mergeText t1 t2) (l1 +l2) doc)
915 merge (TextBeside s sl d) = TextBeside s sl (merge d)
916 merge (Nest k d) = Nest k (merge d)
917 merge (Union d1 d2) = Union (merge d1) (merge d2)
918 mergeText t1 t2 = Str $ tdToStr t1 ++ tdToStr t2
919
920 isOneLiner :: RDoc -> Bool
921 isOneLiner = genericProp (&&) iol where
922 iol (NilAbove _) = stop False
923 iol (Union _ _) = stop False
924 iol NoDoc = stop False
925 iol _ = recurse True
926
927 hasOneLiner :: RDoc -> Bool
928 hasOneLiner = genericProp (&&) iol where
929 iol (NilAbove _) = stop False
930 iol (Union d1 _) = stop $ hasOneLiner d1
931 iol NoDoc = stop False
932 iol _ = recurse True
933
934 -- use elementwise concatenation as generic combinator
935 extractTexts :: Doc -> [String]
936 extractTexts = map normWS . genericProp combine go where
937 combine xs ys = [ a ++ b | a <- xs, b <- ys ]
938 go (TextBeside s _ _ ) = recurse [tdToStr s]
939 go (Union d1 d2) = stop $ extractTexts d1 ++ extractTexts d2
940 go NoDoc = stop []
941 go _ = recurse [""]
942 -- modulo whitespace
943 normWS txt = filter (not . isWS) txt where
944 isWS ws | ws == ' ' || ws == '\n' || ws == '\t' = True
945 | otherwise = False
946
947 emptyReduction :: Doc -> Doc
948 emptyReduction doc =
949 case doc of
950 Empty -> Empty
951 NilAbove d -> case emptyReduction d of Empty -> Empty ; d' -> NilAbove d'
952 TextBeside s sl d -> TextBeside s sl (emptyReduction d)
953 Nest k d -> case emptyReduction d of Empty -> Empty; d -> Nest k d
954 Union d1 d2 -> case emptyReduction d2 of Empty -> Empty; _ -> Union d1 d2 -- if d2 is empty, both have to be
955 NoDoc -> NoDoc
956 Beside d1 _ d2 -> emptyReduction (reduceDoc doc)
957 Above d1 _ d2 -> emptyReduction (reduceDoc doc)
958
959 firstLineLength :: Doc -> Int
960 firstLineLength = genericProp (+) fll . reduceDoc where
961 fll (NilAbove d) = stop 0
962 fll (TextBeside _ l d) = recurse l
963 fll (Nest k d) = recurse k
964 fll (Union d1 d2) = stop (firstLineLength d1) -- inductively assuming inv7
965 fll (Above _ _ _) = error "Above"
966 fll (Beside _ _ _) = error "Beside"
967 fll _ = (0,True)
968
969 abstractLayout :: Doc -> [(Int,String)]
970 abstractLayout d = cal 0 Nothing (reduceDoc d) where
971 -- current column -> this line -> doc -> [(indent,line)]
972 cal :: Int -> (Maybe (Int,String)) -> Doc -> [(Int,String)]
973 cal k cur Empty = [ addTextEOL k (Str "") cur ]
974 cal k cur (NilAbove d) = (addTextEOL k (Str "") cur) : cal k Nothing d
975 cal k cur (TextBeside s sl d) = cal (k+sl) (addText k s cur) d
976 cal k cur (Nest n d) = cal (k+n) cur d
977 cal _ _ (Union d1 d2) = error "abstractLayout: Union"
978 cal _ _ NoDoc = error "NoDoc"
979 cal _ _ (Above _ _ _) = error "Above"
980 cal _ _ (Beside _ _ _) = error "Beside"
981 addTextEOL k str Nothing = (k,tdToStr str)
982 addTextEOL _ str (Just (k,pre)) = (k,pre++ tdToStr str)
983 addText k str = Just . addTextEOL k str
984
985 docifyLayout :: [(Int,String)] -> Doc
986 docifyLayout = vcat . map (\(k,t) -> nest k (text t))
987
988 oneLineRender :: Doc -> String
989 oneLineRender = olr . abstractLayout . last . flattenDoc where
990 olr = concat . intersperse " " . map snd
991
992 -- because of invariant 4, we do not have to expand to layouts here
993 -- but it is easier, so for now we use abstractLayout
994 firstLineIsLeftMost :: Doc -> Bool
995 firstLineIsLeftMost = all (firstIsLeftMost . abstractLayout) . flattenDoc where
996 firstIsLeftMost ((k,_):xs@(_:_)) = all ( (>= k) . fst) xs
997 firstIsLeftMost _ = True
998
999 noNegativeIndent :: Doc -> Bool
1000 noNegativeIndent = all (noNegIndent . abstractLayout) . flattenDoc where
1001 noNegIndent = all ( (>= 0) . fst)
1002