1-- Check that the terminal output works correctly.
2{-# LANGUAGE TemplateHaskell, DeriveGeneric #-}
3import Test.QuickCheck
4import Test.QuickCheck.Text
5import System.Process
6import System.IO
7import Control.Exception
8import GHC.Generics
9import Control.DeepSeq
10
11data Command =
12    PutPart String
13  | PutLine String
14  | PutTemp String
15  deriving (Eq, Ord, Show, Generic)
16
17instance Arbitrary Command where
18  arbitrary =
19    oneof [
20      PutPart <$> line,
21      PutLine <$> line,
22      PutTemp <$> line]
23    where
24      line = filter (/= '\n') <$> arbitrary
25  shrink = genericShrink
26
27exec :: Terminal -> Command -> IO ()
28exec tm (PutPart xs) = putPart tm xs
29exec tm (PutLine xs) = putLine tm xs
30exec tm (PutTemp xs) = putTemp tm xs
31
32eval :: [Command] -> String
33eval = concatMap eval1
34  where
35    eval1 (PutPart xs) = xs
36    eval1 (PutLine xs) = xs ++ "\n"
37    -- PutTemp only has an effect on stderr
38    eval1 (PutTemp xs) = ""
39
40-- Evaluate the result of printing a given string, taking backspace
41-- characters into account.
42format :: String -> String
43format xs = format1 [] [] xs
44  where
45    -- Arguments: text before the cursor (in reverse order),
46    -- text after the cursor, text to print
47    format1 xs ys [] = line xs ys
48    -- \n emits a new line
49    format1 xs ys ('\n':zs) = line xs ys ++ "\n" ++ format1 [] [] zs
50    -- \b moves the cursor to the left
51    format1 (x:xs) ys ('\b':zs) = format1 xs (x:xs) zs
52    -- beginning of line: \b ignored
53    format1 [] ys ('\b':zs) = format1 [] ys zs
54    -- Normal printing puts the character before the cursor,
55    -- and overwrites the next character after the cursor
56    format1 xs ys (z:zs) = format1 (z:xs) (drop 1 ys) zs
57
58    line xs ys = reverse xs ++ ys
59
60-- Check that the terminal satisfies the following properties:
61-- * The text written to stdout matches what's returned by terminalOutput
62-- * The output agrees with the model implementation 'eval'
63-- * Anything written to stderr (presumably by putTemp) is erased
64prop_terminal :: [Command] -> Property
65prop_terminal cmds =
66  withMaxSuccess 1000 $ ioProperty $
67  withPipe $ \stdout_read stdout_write ->
68  withPipe $ \stderr_read stderr_write -> do
69    out <- withHandleTerminal stdout_write (Just stderr_write) $ \tm -> do
70      mapM_ (exec tm) (cmds ++ [PutPart ""])
71      terminalOutput tm
72    stdout <- stdout_read
73    stderr <- stderr_read
74    return $ conjoin [
75        counterexample "output == terminalOutput" $ stdout === out,
76        counterexample "output == model" $ out === eval cmds,
77        counterexample "putTemp erased" $ all (== ' ') (format stderr) ]
78  where
79    withPipe :: (IO String -> Handle -> IO a) -> IO a
80    withPipe action = do
81      (readh, writeh) <- createPipe
82      hSetEncoding readh utf8
83      hSetEncoding writeh utf8
84      let
85        read = do
86          hClose writeh
87          contents <- hGetContents readh
88          return $!! contents
89      action read writeh `finally` do
90        hClose readh
91        hClose writeh
92
93return []
94main = do True <- $quickCheckAll; return ()
95