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