-----------------------------------------------------------------------------
-- Module : HughesPJQuickCheck
-- Copyright : (c) 2008 Benedikt Huber
-- License : BSD-style
--
-- QuickChecks for HughesPJ pretty printer.
--
-- 1) Testing laws (blackbox)
-- - CDoc (combinator datatype)
-- 2) Testing invariants (whitebox)
-- 3) Testing bug fixes (whitebox)
--
-----------------------------------------------------------------------------
import PrettyTestVersion
import TestGenerators
import TestStructures
import UnitLargeDoc
import UnitPP1
import UnitT3911
import UnitT32
import Control.Monad
import Data.Char (isSpace)
import Data.List (intersperse)
import Debug.Trace
import Test.QuickCheck
main :: IO ()
main = do
-- quickcheck tests
check_laws
check_invariants
check_improvements
check_non_prims -- hpc full coverage
check_rendering
check_list_def
-- unit tests
testPP1
testT3911
testT32
testLargeDoc
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- Utility functions
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- tweaked to perform many small tests
myConfig :: Int -> Int -> Args
myConfig d n = stdArgs { maxSize = d, maxDiscardRatio = n*5 }
maxTests :: Int
maxTests = 1000
myTest :: (Testable a) => String -> a -> IO ()
myTest = myTest' 15 maxTests
myTest' :: (Testable a) => Int -> Int -> String -> a -> IO ()
myTest' d n msg t = do
putStrLn (" * " ++ msg)
r <- quickCheckWithResult (myConfig d n) t
case r of
(Failure {}) -> error "Failed testing!"
_ -> return ()
myAssert :: String -> Bool -> IO ()
myAssert msg b = putStrLn $ (if b then "Ok, passed " else "Failed test:\n ") ++ msg
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- Quickcheck tests
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- Equalities on Documents
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- compare text details
tdEq :: TextDetails -> TextDetails -> Bool
tdEq td1 td2 = (tdToStr td1) == (tdToStr td2)
-- algebraic equality on reduced docs
docEq :: RDoc () -> RDoc () -> Bool
docEq rd1 rd2 = case (rd1, rd2) of
(Empty, Empty) -> True
(NoDoc, NoDoc) -> True
(NilAbove ds1, NilAbove ds2) -> docEq ds1 ds2
(TextBeside td1 ds1, TextBeside td2 ds2) | annotToTd td1 `tdEq` annotToTd td2 -> docEq ds1 ds2
(Nest k1 d1, Nest k2 d2) | k1 == k2 -> docEq d1 d2
(Union d11 d12, Union d21 d22) -> docEq d11 d21 && docEq d12 d22
(d1,d2) -> False
-- algebraic equality, with text reduction
deq :: Doc () -> Doc () -> Bool
deq d1 d2 = docEq (reduceDoc' d1) (reduceDoc' d2) where
reduceDoc' = mergeTexts . reduceDoc
deqs :: [Doc ()] -> [Doc ()] -> Bool
deqs ds1 ds2 =
case zipE ds1 ds2 of
Nothing -> False
(Just zds) -> all (uncurry deq) zds
zipLayouts :: Doc () -> Doc () -> Maybe [(Doc (),Doc ())]
zipLayouts d1 d2 = zipE (reducedDocs d1) (reducedDocs d2)
where reducedDocs = map mergeTexts . flattenDoc
zipE :: [Doc ()] -> [Doc ()] -> Maybe [(Doc (), Doc ())]
zipE l1 l2 | length l1 == length l2 = Just $ zip l1 l2
| otherwise = Nothing
-- algebraic equality for layouts (without permutations)
lseq :: Doc () -> Doc () -> Bool
lseq d1 d2 = maybe False id . fmap (all (uncurry docEq)) $ zipLayouts d1 d2
-- abstract render equality for layouts
-- should only be performed if the number of layouts is reasonably small
rdeq :: Doc () -> Doc () -> Bool
rdeq d1 d2 = maybe False id . fmap (all (uncurry layoutEq)) $ zipLayouts d1 d2
where layoutEq d1 d2 = (abstractLayout d1) == (abstractLayout d2)
layoutsCountBounded :: Int -> [Doc ()] -> Bool
layoutsCountBounded k docs = isBoundedBy k (concatMap flattenDoc docs)
where
isBoundedBy k [] = True
isBoundedBy 0 (x:xs) = False
isBoundedBy k (x:xs) = isBoundedBy (k-1) xs
layoutCountBounded :: Int -> Doc () -> Bool
layoutCountBounded k doc = layoutsCountBounded k [doc]
maxLayouts :: Int
maxLayouts = 64
infix 4 `deq`
infix 4 `lseq`
infix 4 `rdeq`
debugRender :: Int -> Doc () -> IO ()
debugRender k = putStr . visibleSpaces . renderStyle (Style PageMode k 1)
visibleSpaces = unlines . map (map visibleSpace) . lines
visibleSpace :: Char -> Char
visibleSpace ' ' = '.'
visibleSpace '.' = error "dot in visibleSpace (avoid confusion, please)"
visibleSpace c = c
-- (1) QuickCheck Properties: Laws
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
{-
Monoid laws for <>,<+>,$$,$+$
~~~~~~~~~~~~~
(x * y) * z = x * (y * z)
empty * x = x
x * empty = x
-}
prop_1 op x y z = classify (any isEmpty [x,y,z]) "empty x, y or z" $
((x `op` y) `op` z) `deq` (x `op` (y `op` z))
prop_2 op x = classify (isEmpty x) "empty" $ (empty `op` x) `deq` x
prop_3 op x = classify (isEmpty x) "empty" $ x `deq` (empty `op` x)
check_monoid = do
putStrLn " = Monoid Laws ="
mapM_ (myTest' 5 maxTests "Associativity") [ liftDoc3 (prop_1 op) | op <- allops ]
mapM_ (myTest "Left neutral") [ prop_2 op . buildDoc | op <- allops ]
mapM_ (myTest "Right neutral") [ prop_3 op . buildDoc | op <- allops ]
where
allops = [ (<>), (<+>) ,($$) , ($+$) ]
{-
Laws for text
~~~~~~~~~~~~~
text s <> text t = text (s++t)
text "" <> x = x, if x non-empty [only true if x does not start with nest, because of ]
-}
prop_t1 s t = text' s <> text' t `deq` text (unText s ++ unText t)
prop_t2 x = not (isEmpty x) ==> text "" <> x `deq` x
prop_t2_a x = not (isEmpty x) && not (isNest x) ==> text "" <> x `deq` x
isNest :: Doc () -> Bool
isNest d = case reduceDoc d of
(Nest _ _) -> True
(Union d1 d2) -> isNest d1 || isNest d2
_ -> False
check_t = do
putStrLn " = Text laws ="
myTest "t1" prop_t1
myTest "t2_a (precondition: x does not start with nest)" (prop_t2_a . buildDoc)
myTest "t_2 (Known to fail)" (expectFailure . prop_t2 . buildDoc)
{-
Laws for nest
~~~~~~~~~~~~~
nest 0 x = x
nest k (nest k' x) = nest (k+k') x
nest k (x <> y) = nest k z <> nest k y
nest k (x $$ y) = nest k x $$ nest k y
nest k empty = empty
x <> nest k y = x <> y, if x non-empty
-}
prop_n1 x = nest 0 x `deq` x
prop_n2 k k' x = nest k (nest k' x) `deq` nest (k+k') x
prop_n3 k k' x = nest k (nest k' x) `deq` nest (k+k') x
prop_n4 k x y = nest k (x $$ y) `deq` nest k x $$ nest k y
prop_n5 k = nest k empty `deq` empty
prop_n6 x k y = not (isEmpty x) ==>
x <> nest k y `deq` x <> y
check_n = do
putStrLn "Nest laws"
myTest "n1" (prop_n1 . buildDoc)
myTest "n2" (\k k' -> prop_n2 k k' . buildDoc)
myTest "n3" (\k k' -> prop_n3 k k' . buildDoc)
myTest "n4" (\k -> liftDoc2 (prop_n4 k))
myTest "n5" prop_n5
myTest "n6" (\k -> liftDoc2 (\x -> prop_n6 x k))
{-
(text s <> x) $$ y = text s <> ((text "" <> x)) $$
nest (-length s) y)
(x $$ y) <> z = x $$ (y <> z)
if y non-empty
-}
prop_m1 s x y = (text' s <> x) $$ y `deq` text' s <> ((text "" <> x) $$
nest (-length (unText s)) y)
prop_m2 x y z = not (isEmpty y) ==>
(x $$ y) <> z `deq` x $$ (y <> z)
check_m = do
putStrLn "Misc laws"
myTest "m1" (\s -> liftDoc2 (prop_m1 s))
myTest' 10 maxTests "m2" (liftDoc3 prop_m2)
{-
Laws for list versions
~~~~~~~~~~~~~~~~~~~~~~
sep (ps++[empty]++qs) = sep (ps ++ qs)
...ditto hsep, hcat, vcat, fill...
[ Fails for fill ! ]
nest k (sep ps) = sep (map (nest k) ps)
...ditto hsep, hcat, vcat, fill...
-}
prop_l1 sp ps qs =
sp (ps++[empty]++qs) `rdeq` sp (ps ++ qs)
prop_l2 sp k ps = nest k (sep ps) `deq` sep (map (nest k) ps)
prop_l1' sp cps cqs =
let [ps,qs] = map buildDocList [cps,cqs] in
layoutCountBounded maxLayouts (sp (ps++qs)) ==> prop_l1 sp ps qs
prop_l2' sp k ps = prop_l2 sp k (buildDocList ps)
check_l = do
allCats $ myTest "l1" . prop_l1'
allCats $ myTest "l2" . prop_l2'
where
allCats = flip mapM_ [ sep, hsep, cat, hcat, vcat, fsep, fcat ]
prop_l1_fail_1 = [ text "a" ]
prop_l1_fail_2 = [ text "a" $$ text "b" ]
{-
Laws for oneLiner
~~~~~~~~~~~~~~~~~
oneLiner (nest k p) = nest k (oneLiner p)
oneLiner (x <> y) = oneLiner x <> oneLiner y
[One liner only takes reduced arguments]
-}
oneLinerR = oneLiner . reduceDoc
prop_o1 k p = oneLinerR (nest k p) `deq` nest k (oneLinerR p)
prop_o2 x y = oneLinerR (x <> y) `deq` oneLinerR x <> oneLinerR y
check_o = do
putStrLn "oneliner laws"
myTest "o1 (RDoc arg)" (\k p -> prop_o1 k (buildDoc p))
myTest "o2 (RDoc arg)" (liftDoc2 prop_o2)
{-
Definitions of list versions
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
vcat = foldr ($$) empty
hcat = foldr (<>) empty
hsep = foldr (<+>) empty
-}
prop_hcat :: [Doc ()] -> Bool
prop_hcat ds = hcat ds `deq` (foldr (<>) empty) ds
prop_hsep :: [Doc ()] -> Bool
prop_hsep ds = hsep ds `deq` (foldr (<+>) empty) ds
prop_vcat :: [Doc ()] -> Bool
prop_vcat ds = vcat ds `deq` (foldr ($$) empty) ds
{-
Update (pretty-1.1.0):
*failing* definition of sep: oneLiner (hsep ps) `union` vcat ps
?
-}
prop_sep :: [Doc ()] -> Bool
prop_sep ds = sep ds `rdeq` (sepDef ds)
sepDef :: [Doc ()] -> Doc ()
sepDef docs = let ds = filter (not . isEmpty) docs in
case ds of
[] -> empty
[d] -> d
ds -> reduceDoc (oneLiner (reduceDoc $ hsep ds)
`Union`
(reduceDoc $ foldr ($+$) empty ds))
check_list_def = do
myTest "hcat def" (prop_hcat . buildDocList)
myTest "hsep def" (prop_hsep . buildDocList)
myTest "vcat def" (prop_vcat . buildDocList)
-- XXX: Not sure if this is meant to fail (I added the expectFailure [DT])
myTest "sep def" (expectFailure . prop_sep . buildDocList)
{-
Definition of fill (fcat/fsep)
-- Specification:
-- fill [] = empty
-- fill [p] = p
-- fill (p1:p2:ps) = oneLiner p1 <#> nest (length p1)
-- (fill (oneLiner p2 : ps))
-- `union`
-- p1 $$ fill ps
-- Revised Specification:
-- fill g docs = fillIndent 0 docs
--
-- fillIndent k [] = []
-- fillIndent k [p] = p
-- fillIndent k (p1:p2:ps) =
-- oneLiner p1 fillIndent (k + length p1 + g ? 1 : 0) (remove_nests (oneLiner p2) : ps)
-- `Union`
-- (p1 $*$ nest (-k) (fillIndent 0 ps))
--
-- $*$ is defined for layouts (not Docs) as
-- layout1 $*$ layout2 | isOneLiner layout1 = layout1 $+$ layout2
-- | otherwise = layout1 $$ layout2
--
-- Old implementation ambiguities/problems:
-- ========================================
-- Preserving nesting:
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- fcat [cat[ text "b", text "a"], nest 2 ( text "" $$ text "a")]
-- ==> fcat [ text "b" $$ text "a", nest 2 (text "" $$ text "a")] // cat: union right
-- ==> (text "b" $$ text "a" $$ nest 2 (text "" $$ text "a")) // fcat: union right with overlap
-- ==> (text "ab" $$ nest 2 (text "" $$ text "a"))
-- ==> "b\na\n..a"
-- Bug #1337:
-- ~~~~~~~~~~
-- > fcat [ nest 1 $ text "a", nest 2 $ text "b", text "c"]
-- ==> [second alternative] roughly (a <#> b $#$ c)
-- " ab"
-- "c "
-- expected: (nest 1; text "a"; text "b"; nest -3; "c")
-- actual : (nest 1; text "a"; text "b"; nest -5; "c")
-- === (nest 1; text a) <> (fill (-2) (p2:ps))
-- ==> (nest 2 (text "b") $+$ text "c")
-- ==> (nest 2 (text "b") `nilabove` nest (-3) (text "c"))
-- ==> (nest 1; text a; text b; nest -5 c)
-}
prop_fcat_vcat :: [Doc ()] -> Bool
prop_fcat_vcat ds = last (flattenDoc $ fcat ds) `deq` last (flattenDoc $ vcat ds)
prop_fcat :: [Doc ()] -> Bool
prop_fcat ds = fcat ds `rdeq` fillDef False (filter (not . isEmpty) ds)
prop_fsep :: [Doc ()] -> Bool
prop_fsep ds = fsep ds `rdeq` fillDef True (filter (not . isEmpty) ds)
prop_fcat_old :: [Doc ()] -> Bool
prop_fcat_old ds = fillOld2 False ds `rdeq` fillDef False (filter (not . isEmpty) ds)
prop_fcat_old_old :: [Doc ()] -> Bool
prop_fcat_old_old ds = fillOld2 False ds `rdeq` fillDefOld False (filter (not . isEmpty) ds)
prop_restrict_sz :: (Testable a) => Int -> ([Doc ()] -> a) -> ([Doc ()] -> Property)
prop_restrict_sz k p ds = layoutCountBounded k (fsep ds) ==> p ds
prop_restrict_ol :: (Testable a) => ([Doc ()] -> a) -> ([Doc ()] -> Property)
prop_restrict_ol p ds = (all isOneLiner . map normalize $ ds) ==> p ds
prop_restrict_no_nest_start :: (Testable a) => ([Doc ()] -> a) -> ([Doc ()] -> Property)
prop_restrict_no_nest_start p ds = (all (not .isNest) ds) ==> p ds
fillDef :: Bool -> [Doc ()] -> Doc ()
fillDef g = normalize . fill' 0 . filter (not.isEmpty) . map reduceDoc
where
fill' _ [] = Empty
fill' _ [x] = x
fill' k (p1:p2:ps) =
reduceDoc (oneLiner p1 `append` (fill' (k + firstLineLength p1 + (if g then 1 else 0)) $ (oneLiner' p2) : ps))
`union`
reduceDoc (p1 $*$ (nest (-k) (fillDef g (p2:ps))))
union = Union
append = if g then (<+>) else (<>)
oneLiner' (Nest k d) = oneLiner' d
oneLiner' d = oneLiner d
($*$) :: RDoc () -> RDoc () -> RDoc ()
($*$) p ps = case flattenDoc p of
[] -> NoDoc
ls -> foldr1 Union (map combine ls)
where
combine p | isOneLiner p = p $+$ ps
| otherwise = p $$ ps
fillDefOld :: Bool -> [Doc ()] -> Doc ()
fillDefOld g = normalize . fill' . filter (not.isEmpty) . map normalize where
fill' [] = Empty
fill' [p1] = p1
fill' (p1:p2:ps) = (normalize (oneLiner p1 `append` nest (firstLineLength p1)
(fill' (oneLiner p2 : ps))))
`union`
(p1 $$ fill' (p2:ps))
append = if g then (<+>) else (<>)
union = Union
check_fill_prop :: Testable a => String -> ([Doc ()] -> a) -> IO ()
check_fill_prop msg p = myTest msg (prop_restrict_sz maxLayouts p . buildDocList)
check_fill_def_fail :: IO ()
check_fill_def_fail = do
check_fill_prop "fcat defOld vs fcatOld (ol)" (prop_restrict_ol prop_fcat_old_old)
check_fill_prop "fcat defOld vs fcatOld" prop_fcat_old_old
check_fill_prop "fcat def (ol) vs fcatOld" (prop_restrict_ol prop_fcat_old)
check_fill_prop "fcat def vs fcatOld" prop_fcat_old
check_fill_def_ok :: IO ()
check_fill_def_ok = do
check_fill_prop "fcat def (not nest start) vs fcatOld" (prop_restrict_no_nest_start prop_fcat_old)
check_fill_prop "fcat def (not nest start) vs fcat" (prop_restrict_no_nest_start prop_fcat)
-- XXX: These all fail now with the change of pretty to GHC behaviour.
check_fill_prop "fcat def (ol) vs fcat" (expectFailure . prop_restrict_ol prop_fcat)
check_fill_prop "fcat def vs fcat" (expectFailure . prop_fcat)
check_fill_prop "fsep def vs fsep" (expectFailure . prop_fsep)
check_fill_def_laws :: IO ()
check_fill_def_laws = do
check_fill_prop "lastLayout (fcat ps) == vcat ps" prop_fcat_vcat
check_fill_def :: IO ()
check_fill_def = check_fill_def_fail >> check_fill_def_ok
{-
text "ac"; nilabove; nest -1; text "a"; empty
text "ac"; nilabove; nest -2; text "a"; empty
-}
{-
Zero width text (Neil)
Here it would be convenient to generate functions (or replace empty / text bz z-w-t)
-}
-- TODO
{-
All laws: monoid, text, nest, misc, list versions, oneLiner, list def
-}
check_laws :: IO ()
check_laws = do
check_fill_def_ok
check_monoid
check_t
check_n
check_m
check_l
check_o
check_list_def
-- (2) QuickCheck Properties: Invariants (whitebox)
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- strategies: synthesize with stop condition
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
stop :: a -> (a, Bool)
stop a = (a,False)
recurse :: a -> (a, Bool)
recurse a = (a,True)
-- strategy: generic synthesize with stop condition
-- terms are combined top-down, left-right (latin text order)
genericProp :: (a -> a -> a) -> (Doc () -> (a,Bool)) -> Doc () -> a
genericProp c q doc =
case q doc of
(v,False) -> v
(v,True) -> foldl c v (subs doc)
where
rec = genericProp c q
subs d = case d of
Empty -> []
NilAbove d -> [rec d]
TextBeside _ d -> [rec d]
Nest _ d -> [rec d]
Union d1 d2 -> [rec d1, rec d2]
NoDoc -> []
Beside d1 _ d2 -> subs (reduceDoc d)
Above d1 _ d2 -> subs (reduceDoc d)
{-
* The argument of NilAbove is never Empty. Therefore
a NilAbove occupies at least two lines.
-}
prop_inv1 :: Doc () -> Bool
prop_inv1 d = genericProp (&&) nilAboveNotEmpty d where
nilAboveNotEmpty (NilAbove Empty) = stop False
nilAboveNotEmpty _ = recurse True
{-
* The argument of @TextBeside@ is never @Nest@.
-}
prop_inv2 :: Doc () -> Bool
prop_inv2 = genericProp (&&) textBesideNotNest where
textBesideNotNest (TextBeside _ (Nest _ _)) = stop False
textBesideNotNest _ = recurse True
{-
* The layouts of the two arguments of @Union@ both flatten to the same
string
-}
prop_inv3 :: Doc () -> Bool
prop_inv3 = genericProp (&&) unionsFlattenSame where
unionsFlattenSame (Union d1 d2) = stop (pairwiseEqual (extractTexts d1 ++ extractTexts d2))
unionsFlattenSame _ = recurse True
pairwiseEqual (x:y:zs) = x==y && pairwiseEqual (y:zs)
pairwiseEqual _ = True
{-
* The arguments of @Union@ are either @TextBeside@, or @NilAbove@.
-}
prop_inv4 :: Doc () -> Bool
prop_inv4 = genericProp (&&) unionArgs where
unionArgs (Union d1 d2) | goodUnionArg d1 && goodUnionArg d2 = recurse True
| otherwise = stop False
unionArgs _ = recurse True
goodUnionArg (TextBeside _ _) = True
goodUnionArg (NilAbove _) = True
goodUnionArg _ = False
{-
* A @NoDoc@ may only appear on the first line of the left argument of
an union. Therefore, the right argument of an union can never be equivalent
to the empty set.
-}
prop_inv5 :: Doc () -> Bool
prop_inv5 = genericProp (&&) unionArgs . reduceDoc where
unionArgs NoDoc = stop False
unionArgs (Union d1 d2) = stop $ genericProp (&&) noDocIsFirstLine d1 && nonEmptySet (reduceDoc d2)
unionArgs _ = (True,True) -- recurse
noDocIsFirstLine (NilAbove d) = stop $ genericProp (&&) unionArgs d
noDocIsFirstLine _ = recurse True
{-
* An empty document is always represented by @Empty@. It can't be
hidden inside a @Nest@, or a @Union@ of two @Empty@s.
-}
prop_inv6 :: Doc () -> Bool
prop_inv6 d | not (prop_inv1 d) || not (prop_inv2 d) = False
| not (isEmptyDoc d) = True
| otherwise = case d of Empty -> True ; _ -> False
isEmptyDoc :: Doc () -> Bool
isEmptyDoc d = case emptyReduction d of Empty -> True; _ -> False
{-
* Consistency
If all arguments of one of the list versions are empty documents, the list is an empty document
-}
prop_inv6a :: ([Doc ()] -> Doc ()) -> Property
prop_inv6a sep = forAll emptyDocListGen $
\ds -> isEmptyRepr (sep $ buildDocList ds)
where
isEmptyRepr Empty = True
isEmptyRepr _ = False
{-
* The first line of every layout in the left argument of @Union@ is
longer than the first line of any layout in the right argument.
(1) ensures that the left argument has a first line. In view of
(3), this invariant means that the right argument must have at
least two lines.
-}
counterexample_inv7 = cat [ text " ", nest 2 ( text "a") ]
prop_inv7 :: Doc () -> Bool
prop_inv7 = genericProp (&&) firstLonger where
firstLonger (Union d1 d2) = (firstLineLength d1 >= firstLineLength d2, True)
firstLonger _ = (True, True)
{-
* If we take as precondition: the arguments of cat,sep,fill do not start with Nest, invariant 7 holds
-}
prop_inv7_pre :: CDoc -> Bool
prop_inv7_pre cdoc = nestStart True cdoc where
nestStart nestOk doc =
case doc of
CList sep ds -> all (nestStart False) ds
CBeside _ d1 d2 -> nestStart nestOk d1 && nestStart (not . isEmpty $ buildDoc d1) d2
CAbove _ d1 d2 -> nestStart nestOk d1 && nestStart (not . isEmpty $ buildDoc d1) d2
CNest _ d | not nestOk -> False
| otherwise -> nestStart True d
_empty_or_text -> True
{-
inv7_pre ==> inv7
-}
prop_inv7_a :: CDoc -> Property
prop_inv7_a cdoc = prop_inv7_pre cdoc ==> prop_inv7 (buildDoc cdoc)
check_invariants :: IO ()
check_invariants = do
myTest "Invariant 1" (prop_inv1 . buildDoc)
myTest "Invariant 2" (prop_inv2 . buildDoc)
myTest "Invariant 3" (prop_inv3 . buildDoc)
myTest "Invariant 4" (prop_inv4 . buildDoc)
myTest "Invariant 5+" (prop_inv5 . buildDoc)
myTest "Invariant 6" (prop_inv6 . buildDoc)
mapM_ (\sp -> myTest "Invariant 6a" $ prop_inv6a sp) [ cat, sep, fcat, fsep, vcat, hcat, hsep ]
-- XXX: Not sure if this is meant to fail (I added the expectFailure [DT])
myTest "Invariant 7 (fails in HughesPJ:20080621)" (expectFailure . prop_inv7 . buildDoc)
-- `negative indent'
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
{-
In the documentation we have:
(spaces n) generates a list of n spaces
It should never be called with 'n' < 0, but that can happen for reasons I don't understand
This is easy to explain:
Suppose we have layout1 <> layout2
length of last line layout1 is k1
indentation of first line of layout2 is k2
indentation of some other line of layout2 is k2'
Now layout1 <> nest k2 (line1 $$ nest k2' lineK)
==> layout1 <> (line1 $$ nest k2' lineK)
When k1 - k2' < 0, we need to layout lineK with negative indentation
Here is a quick check property to ducment this.
-}
prop_negative_indent :: CDoc -> Property
prop_negative_indent cdoc = noNegNest cdoc ==> noNegSpaces (buildDoc cdoc)
noNegNest = genericCProp (&&) notIsNegNest where
notIsNegNest (CNest k _) | k < 0 = stop False
notIsNegNest _ = recurse True
noNegSpaces = go 0 . reduceDoc where
go k Empty = True
go k (NilAbove d) = go k d
go k (TextBeside _ d) | k < 0 = False
go k (TextBeside s d) = go (k+annotSize s) d
go k (Nest k' d) = go (k+k') d
go k (Union d1 d2) = (if nonEmptySet d1 then (&&) (go k d1) else id) (go k d2)
go k NoDoc = True
counterexample_fail9 :: Doc ()
counterexample_fail9 = text "a" <> ( nest 2 ( text "b") $$ text "c")
-- reduces to textb "a" ; textb "b" ; nilabove ; nest -3 ; textb "c" ; empty
{-
This cannot be fixed with violating the "intuitive property of layouts", described by John Hughes:
"Composing layouts should preserve the layouts themselves (i.e. translation)"
Consider the following example:
It is the user's fault to use <+> in t2.
-}
tstmt = (nest 6 $ text "/* double indented comment */") $+$
(nest 3 $ text "/* indented comment */") $+$
text "skip;"
t1 = text "while(true)" $+$ (nest 2) tstmt
{-
while(true)
/* double indented comment */
/* indented comment */
skip;
-}
t2 = text "while(true)" $+$ (nest 2 $ text "//" <+> tstmt)
{-
while(true)
// /* double indented comment */
/* indented comment */
skip;
-}
-- (3) Touching non-prims
-- ~~~~~~~~~~~~~~~~~~~~~~
check_non_prims :: IO ()
check_non_prims = do
myTest "Non primitive: show = renderStyle style" $ \cd -> let d = buildDoc cd in
show ((zeroWidthText "a") <> d) /= renderStyle style d
myAssert "symbols" $
(semi <> comma <> colon <> equals <> lparen <> rparen <> lbrack <> rbrack <> lbrace <> rbrace)
`deq`
(text ";,:=()[]{}")
myAssert "quoting" $
(quotes . doubleQuotes . parens . brackets .braces $ (text "a" $$ text "b"))
`deq`
(text "'\"([{" <> (text "a" $$ text "b") <> text "}])\"'")
myAssert "numbers" $
fsep [int 42, integer 42, float 42, double 42, rational 42]
`rdeq`
(fsep . map text)
[show (42 :: Int), show (42 :: Integer), show (42 :: Float), show (42 :: Double), show (42 :: Rational)]
myTest "Definition of <+>" $ \cd1 cd2 ->
let (d1,d2) = (buildDoc cd1, buildDoc cd2) in
layoutsCountBounded maxLayouts [d1,d2] ==>
not (isEmpty d1) && not (isEmpty d2) ==>
d1 <+> d2 `rdeq` d1 <> space <> d2
myTest "hang" $ liftDoc2 (\d1 d2 -> hang d1 2 d2 `deq` sep [d1, nest 2 d2])
let pLift f cp cds = f (buildDoc cp) (buildDocList cds)
myTest "punctuate" $ pLift (\p ds -> (punctuate p ds) `deqs` (punctuateDef p ds))
check_rendering = do
myTest' 20 10000 "one - line rendering" $ \cd ->
let d = buildDoc cd in
(renderStyle (Style OneLineMode undefined undefined) d) == oneLineRender d
myTest' 20 10000 "left-mode rendering" $ \cd ->
let d = buildDoc cd in
extractText (renderStyle (Style LeftMode undefined undefined) d) == extractText (oneLineRender d)
myTest' 20 10000 "page mode rendering" $ \cd ->
let d = buildDoc cd in
extractText (renderStyle (Style PageMode 6 1.7) d) == extractText (oneLineRender d)
myTest' 20 10000 "zigzag mode rendering" $ \cd ->
let d = buildDoc cd in
extractTextZZ (renderStyle (Style ZigZagMode 6 1.7) d) == extractText (oneLineRender d)
extractText :: String -> String
extractText = filter (not . isSpace)
extractTextZZ :: String -> String
extractTextZZ = filter (\c -> not (isSpace c) && c /= '/' && c /= '\\')
punctuateDef :: Doc () -> [Doc ()] -> [Doc ()]
punctuateDef p [] = []
punctuateDef p ps =
let (dsInit,dLast) = (init ps, last ps) in
map (\d -> d <> p) dsInit ++ [dLast]
-- (4) QuickChecking improvments and bug fixes
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
{-
putStrLn $ render' $ fill True [ text "c", text "c",empty, text "c", text "b"]
c c c
b
putStrLn $ render' $ fillOld True [ text "c", text "c",empty, text "c", text "b"]
c c c
b
-}
prop_fill_empty_reduce :: [Doc ()] -> Bool
prop_fill_empty_reduce ds = fill True ds `deq` fillOld True (filter (not.isEmpty.reduceDoc) ds)
check_improvements :: IO ()
check_improvements = do
myTest "fill = fillOld . filter (not.isEmpty) [if no argument starts with nest]"
(prop_fill_empty_reduce . filter (not .isNest) . buildDocList)
-- old implementation of fill
fillOld :: Bool -> [Doc ()] -> RDoc ()
fillOld _ [] = empty
fillOld g (p:ps) = fill1 g (reduceDoc p) 0 ps where
fill1 :: Bool -> RDoc () -> Int -> [Doc ()] -> Doc ()
fill1 _ _ k _ | k `seq` False = undefined
fill1 _ NoDoc _ _ = NoDoc
fill1 g (p `Union` q) k ys = fill1 g p k ys
`union_`
(aboveNest q False k (fillOld g ys))
fill1 g Empty k ys = mkNest k (fillOld g ys)
fill1 g (Nest n p) k ys = nest_ n (fill1 g p (k - n) ys)
fill1 g (NilAbove p) k ys = nilAbove_ (aboveNest p False k (fillOld g ys))
fill1 g (TextBeside s p) k ys = textBeside_ s (fillNB g p (k - annotSize s) ys)
fill1 _ (Above {}) _ _ = error "fill1 Above"
fill1 _ (Beside {}) _ _ = error "fill1 Beside"
-- fillNB gap textBesideArgument space_left docs
fillNB :: Bool -> Doc () -> Int -> [Doc ()] -> Doc ()
fillNB _ _ k _ | k `seq` False = undefined
fillNB g (Nest _ p) k ys = fillNB g p k ys
fillNB _ Empty _ [] = Empty
fillNB g Empty k (y:ys) = nilBeside g (fill1 g (oneLiner (reduceDoc y)) k1 ys)
`mkUnion`
nilAboveNest False k (fillOld g (y:ys))
where
k1 | g = k - 1
| otherwise = k
fillNB g p k ys = fill1 g p k ys
-- Specification:
-- fill [] = empty
-- fill [p] = p
-- fill (p1:p2:ps) = oneLiner p1 <#> nest (length p1)
-- (fill (oneLiner p2 : ps))
-- `union`
-- p1 $$ fill ps
fillOld2 :: Bool -> [Doc ()] -> RDoc ()
fillOld2 _ [] = empty
fillOld2 g (p:ps) = fill1 g (reduceDoc p) 0 ps where
fill1 :: Bool -> RDoc () -> Int -> [Doc ()] -> Doc ()
fill1 _ _ k _ | k `seq` False = undefined
fill1 _ NoDoc _ _ = NoDoc
fill1 g (p `Union` q) k ys = fill1 g p k ys
`union_`
(aboveNest q False k (fill g ys))
fill1 g Empty k ys = mkNest k (fill g ys)
fill1 g (Nest n p) k ys = nest_ n (fill1 g p (k - n) ys)
fill1 g (NilAbove p) k ys = nilAbove_ (aboveNest p False k (fill g ys))
fill1 g (TextBeside s p) k ys = textBeside_ s (fillNB g p (k - annotSize s) ys)
fill1 _ (Above {}) _ _ = error "fill1 Above"
fill1 _ (Beside {}) _ _ = error "fill1 Beside"
fillNB :: Bool -> Doc () -> Int -> [Doc ()] -> Doc ()
fillNB _ _ k _ | k `seq` False = undefined
fillNB g (Nest _ p) k ys = fillNB g p k ys
fillNB _ Empty _ [] = Empty
fillNB g Empty k (Empty:ys) = fillNB g Empty k ys
fillNB g Empty k (y:ys) = fillNBE g k y ys
fillNB g p k ys = fill1 g p k ys
fillNBE g k y ys = nilBeside g (fill1 g (oneLiner (reduceDoc y)) k1 ys)
`mkUnion`
nilAboveNest True k (fill g (y:ys))
where
k1 | g = k - 1
| otherwise = k
-- (5) Pretty printing RDocs and RDOC properties
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
prettyDoc :: Doc () -> Doc ()
prettyDoc d =
case reduceDoc d of
Empty -> text "empty"
NilAbove d -> (text "nilabove") <> semi <+> (prettyDoc d)
TextBeside s d -> (text ("text \""++tdToStr (annotToTd s) ++ "\"" ++ show (annotSize s))) <> semi <+> (prettyDoc d)
Nest k d -> text "nest" <+> integer (fromIntegral k) <> semi <+> prettyDoc d
Union d1 d2 -> sep [text "union", parens (prettyDoc d1), parens (prettyDoc d2)]
NoDoc -> text "nodoc"
-- TODO: map strategy for Docs to avoid code duplication
-- Debug: Doc -> [Layout]
flattenDoc :: Doc () -> [RDoc ()]
flattenDoc d = flatten (reduceDoc d) where
flatten NoDoc = []
flatten Empty = return Empty
flatten (NilAbove d) = map NilAbove (flatten d)
flatten (TextBeside s d) = map (TextBeside s) (flatten d)
flatten (Nest k d) = map (Nest k) (flatten d)
flatten (Union d1 d2) = flattenDoc d1 ++ flattenDoc d2
flatten (Beside d1 b d2) = error $ "flattenDoc Beside"
flatten (Above d1 b d2) = error $ "flattenDoc Above"
normalize :: Doc () -> RDoc ()
normalize d = norm d where
norm NoDoc = NoDoc
norm Empty = Empty
norm (NilAbove d) = NilAbove (norm d)
norm (TextBeside s (Nest k d)) = norm (TextBeside s d)
norm (TextBeside s d) = (TextBeside s) (norm d)
norm (Nest k (Nest k' d)) = norm $ Nest (k+k') d
norm (Nest 0 d) = norm d
norm (Nest k d) = (Nest k) (norm d)
-- * The arguments of @Union@ are either @TextBeside@, or @NilAbove@.
norm (Union d1 d2) = normUnion (norm d1) (norm d2)
norm d@(Beside d1 b d2) = norm (reduceDoc d)
norm d@(Above d1 b d2) = norm (reduceDoc d)
normUnion d0@(Nest k d) (Union d1 d2) = norm (Union d0 (normUnion d1 d2))
normUnion (Union d1 d2) d3@(Nest k d) = norm (Union (normUnion d1 d2) d3)
normUnion (Nest k d1) (Nest k' d2) | k == k' = Nest k $ Union (norm d1) (norm d2)
| otherwise = error "normalize: Union Nest length mismatch ?"
normUnion (Nest _ _) d2 = error$ "normUnion Nest "++topLevelCTor d2
normUnion d1 (Nest _ _) = error$ "normUnion Nset "++topLevelCTor d1
normUnion p1 p2 = Union p1 p2
topLevelCTor :: Doc () -> String
topLevelCTor d = tlc d where
tlc NoDoc = "NoDoc"
tlc Empty = "Empty"
tlc (NilAbove d) = "NilAbove"
tlc (TextBeside s d) = "TextBeside"
tlc (Nest k d) = "Nest"
tlc (Union d1 d2) = "Union"
tlc (Above _ _ _) = "Above"
tlc (Beside _ _ _) = "Beside"
-- normalize TextBeside (and consequently apply some laws for simplification)
mergeTexts :: RDoc () -> RDoc ()
mergeTexts = merge where
merge NoDoc = NoDoc
merge Empty = Empty
merge (NilAbove d) = NilAbove (merge d)
merge (TextBeside t1 (TextBeside t2 doc)) = (merge.normalize) (TextBeside (mergeText t1 t2) doc)
merge (TextBeside s d) = TextBeside s (merge d)
merge (Nest k d) = Nest k (merge d)
merge (Union d1 d2) = Union (merge d1) (merge d2)
mergeText t1 t2 =
NoAnnot (Str $ tdToStr (annotToTd t1) ++ tdToStr (annotToTd t2))
(annotSize t1 + annotSize t2)
isOneLiner :: RDoc () -> Bool
isOneLiner = genericProp (&&) iol where
iol (NilAbove _) = stop False
iol (Union _ _) = stop False
iol NoDoc = stop False
iol _ = recurse True
hasOneLiner :: RDoc () -> Bool
hasOneLiner = genericProp (&&) iol where
iol (NilAbove _) = stop False
iol (Union d1 _) = stop $ hasOneLiner d1
iol NoDoc = stop False
iol _ = recurse True
-- use elementwise concatenation as generic combinator
extractTexts :: Doc () -> [String]
extractTexts = map normWS . genericProp combine go where
combine xs ys = [ a ++ b | a <- xs, b <- ys ]
go (TextBeside s _ ) = recurse [tdToStr (annotToTd s)]
go (Union d1 d2) = stop $ extractTexts d1 ++ extractTexts d2
go NoDoc = stop []
go _ = recurse [""]
-- modulo whitespace
normWS txt = filter (not . isWS) txt where
isWS ws | ws == ' ' || ws == '\n' || ws == '\t' = True
| otherwise = False
emptyReduction :: Doc () -> Doc ()
emptyReduction doc =
case doc of
Empty -> Empty
NilAbove d -> case emptyReduction d of Empty -> Empty ; d' -> NilAbove d'
TextBeside s d -> TextBeside s (emptyReduction d)
Nest k d -> case emptyReduction d of Empty -> Empty; d -> Nest k d
Union d1 d2 -> case emptyReduction d2 of Empty -> Empty; _ -> Union d1 d2 -- if d2 is empty, both have to be
NoDoc -> NoDoc
Beside d1 _ d2 -> emptyReduction (reduceDoc doc)
Above d1 _ d2 -> emptyReduction (reduceDoc doc)
firstLineLength :: Doc () -> Int
firstLineLength = genericProp (+) fll . reduceDoc where
fll (NilAbove d) = stop 0
fll (TextBeside s d) = recurse (annotSize s)
fll (Nest k d) = recurse k
fll (Union d1 d2) = stop (firstLineLength d1) -- inductively assuming inv7
fll (Above _ _ _) = error "Above"
fll (Beside _ _ _) = error "Beside"
fll _ = (0,True)
abstractLayout :: Doc () -> [(Int,String)]
abstractLayout d = cal 0 Nothing (reduceDoc d) where
-- current column -> this line -> doc -> [(indent,line)]
cal :: Int -> (Maybe (Int,String)) -> Doc () -> [(Int,String)]
cal k cur Empty = [ addTextEOL k (Str "") cur ]
cal k cur (NilAbove d) = (addTextEOL k (Str "") cur) : cal k Nothing d
cal k cur (TextBeside s d) = cal (k + annotSize s) (addText k s cur) d
cal k cur (Nest n d) = cal (k+n) cur d
cal _ _ (Union d1 d2) = error "abstractLayout: Union"
cal _ _ NoDoc = error "NoDoc"
cal _ _ (Above _ _ _) = error "Above"
cal _ _ (Beside _ _ _) = error "Beside"
addTextEOL k str Nothing = (k,tdToStr str)
addTextEOL _ str (Just (k,pre)) = (k,pre++ tdToStr str)
addText k str = Just . addTextEOL k (annotToTd str)
docifyLayout :: [(Int,String)] -> Doc ()
docifyLayout = vcat . map (\(k,t) -> nest k (text t))
oneLineRender :: Doc () -> String
oneLineRender = olr . abstractLayout . last . flattenDoc where
olr = concat . intersperse " " . map snd
-- because of invariant 4, we do not have to expand to layouts here
-- but it is easier, so for now we use abstractLayout
firstLineIsLeftMost :: Doc () -> Bool
firstLineIsLeftMost = all (firstIsLeftMost . abstractLayout) . flattenDoc where
firstIsLeftMost ((k,_):xs@(_:_)) = all ( (>= k) . fst) xs
firstIsLeftMost _ = True
noNegativeIndent :: Doc () -> Bool
noNegativeIndent = all (noNegIndent . abstractLayout) . flattenDoc where
noNegIndent = all ( (>= 0) . fst)