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