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