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