IOSpec 0.1.1 → 0.2

raw patch · 18 files changed

+1253/−660 lines, 18 filesdep +Streamdep ~QuickCheckPVP ok

version bump matches the API change (PVP)

Dependencies added: Stream

Dependency ranges changed: QuickCheck

API changes (from Hackage documentation)

Files

• IOSpec.cabal +46/−14
• README +5/−1
• examples/Channels.hs +19/−9
• examples/Echo.hs +25/−11
• examples/Queues.hs +43/−26
• examples/Refs.hs +23/−0
• examples/Sudoku.hs +316/−0
• src/Data/Stream.hs +0/−178
• src/Test/IOSpec.hs +14/−3
• src/Test/IOSpec/Concurrent.hs +0/−282
• src/Test/IOSpec/Fork.hs +34/−0
• src/Test/IOSpec/IORef.hs +43/−92
• src/Test/IOSpec/MVar.hs +71/−0
• src/Test/IOSpec/STM.hs +132/−0
• src/Test/IOSpec/Surrogate.hs +31/−0
• src/Test/IOSpec/Teletype.hs +50/−44
• src/Test/IOSpec/Types.hs +64/−0
• src/Test/IOSpec/VirtualMachine.hs +337/−0

@@ -1,32 +1,64 @@ Name:		        IOSpec-Version:        	0.1.1+Version:        	0.2 License:        	BSD3 License-file:		LICENSE Author:			Wouter Swierstra Maintainer:     	Wouter Swierstra <wss@cs.nott.ac.uk> Homepage:       	http://www.cs.nott.ac.uk/~wss/repos/IOSpec Synopsis:       	A pure specification of the IO monad.-Description:		At the moment this package consists of four -			modules:+Description:		This package consists of several modules, that give a+			pure specification of functions in the IO monad: 			.-                           * "Test.IOSpec.Teletype": a specification of getChar and putChar.+                           * "Test.IOSpec.Fork": a pure specification of+			      'forkIO'. 			.-			   * "Test.IOSpec.IORef": a specification of most functions on IORefs.+			   * "Test.IOSpec.IORef": a pure specification of most+			      functions that create and manipulate on 'IORefs'. 			.-			   * "Test.IOSpec.Concurrent": specification of forkIO and MVars.+			   * "Test.IOSpec.MVar": a pure specification of most+			      functions that create and manipulate and 'MVars'. 			.-			   * "Data.Stream": a library for manipulating infinite lists.+			   * "Test.IOSpec.STM": a pure specification of+			      'atomically' and the 'STM' monad. 			.-			There are several well-documented examples included with the source distribution.+			   * "Test.IOSpec.Teletype": a pure specification of+			      'getChar', 'putChar', and several related+			      Prelude functions.+			.+			Besides these modules containing the specifications,+			there are a few other important modules:+			.+			   * "Test.IOSpec.Types": defines the 'IOSpec' type and+			     several amenities.+			.+			   * "Test.IOSpec.VirtualMachine": defines a virtual+			     machine on which to execute pure specifications.+			.+			   * "Test.IOSpec.Surrogate": a drop-in replacement for+			     the other modules. Import this and recompile your+			     code once you've finished testing and debugging.+			.+			There are several well-documented examples included +			with the source distribution. Category:       	Testing-Build-Depends:  	base, mtl, QuickCheck +Build-Type:		Simple+Build-Depends:  	base, mtl, QuickCheck < 2.0, Stream+Extensions:		MultiParamTypeClasses+Ghc-options:		-Wall -fglasgow-exts Hs-source-dirs:		src Extra-source-files:	README+			, examples/Channels.hs 			, examples/Echo.hs 			, examples/Queues.hs-			, examples/Channels.hs-Exposed-modules:	Data.Stream-			, Test.IOSpec-			, Test.IOSpec.Teletype+			, examples/Refs.hs+			, examples/Sudoku.hs+Exposed-modules:	Test.IOSpec+			, Test.IOSpec.Fork 			, Test.IOSpec.IORef-			, Test.IOSpec.Concurrent+			, Test.IOSpec.MVar+			, Test.IOSpec.STM+			, Test.IOSpec.Surrogate+			, Test.IOSpec.Teletype+			, Test.IOSpec.Types+			, Test.IOSpec.VirtualMachine+

@@ -1,4 +1,4 @@-IOSpec version 0.1+IOSpec version 0.2   Author: Wouter Swierstra <wss@cs.nott.ac.uk>  IOSpec provides a library containing pure, executable specifications@@ -21,11 +21,15 @@ To build the Haddock API execute the following command:     $ runhaskell Setup.lhs haddock +This will require Haddock 2.0+ Check out the examples directory for the following examples:      * Echo.hs - illustrates how to test the echo function.     * Queues.hs - an implementation of queues using IORefs.     * Channels.hs - an implementation of channels using MVars.+    * Sudoku.hs - a parallel Sudoku solver that uses STM and MVars+         based on Graham Hutton's version of Richard Bird's "Solving Sudoku".  Every example contains quite some comments, explaining how to use the library.

@@ -3,7 +3,7 @@ import Control.Monad import Data.Maybe (fromJust, isJust) import Data.List (sort)-import Test.IOSpec.Concurrent+import Test.IOSpec hiding (Data,putStrLn) import Data.Dynamic  -- An implementation of channels using MVars. Simon Peyton Jones's@@ -14,6 +14,8 @@  type Channel = (MVar (MVar Data), MVar (MVar Data)) +type IOConc a = IOSpec (MVarS :+: ForkS) a+ newChan :: IOConc Channel newChan = do read <- newEmptyMVar 	     write <- newEmptyMVar@@ -23,14 +25,14 @@ 	     return (read,write)  putChan :: Channel -> Int -> IOConc ()-putChan (_,write) val = +putChan (_,write) val =   do newHole <- newEmptyMVar      oldHole <- takeMVar write      putMVar write newHole      putMVar oldHole (Cell val newHole)  getChan :: Channel -> IOConc Int-getChan (read,write) = +getChan (read,write) =   do headVar <- takeMVar read      Cell val newHead <- takeMVar headVar      putMVar read newHead@@ -56,17 +58,24 @@   ch <- newChan   result <- newEmptyMVar   putMVar result []-  forM ints (\i -> forkIO (writer ch i)) +  forM ints (\i -> forkIO (writer ch i))   replicateM (length ints) (forkIO (reader ch result))-  wait result ints +  wait result ints  wait :: MVar [Int] -> [Int] -> IOConc [Int] wait var xs  = do   res <- takeMVar var-  if length res == length xs +  if length res == length xs     then return res     else putMVar var res >> wait var xs ++-- When do we consider two Effects equal? In this case, we want the+-- same final result, and no other visible effects.+(===) :: Eq a => Effect a -> Effect a -> Bool+Done x === Done y = x == y+_ === _ = False+ -- To actually run concurrent programs, we must choose the scheduler -- with which to run. At the moment, IOSpec provides a simple -- round-robin scheduler; alternatively we can write our own@@ -76,9 +85,10 @@ -- Using QuickCheck to generate a random stream, we can use the -- streamSched to implement a random scheduler -- thereby testing as -- many interleavings as possible.-chanProp ints stream =-  sort (fromJust (runIOConc (chanTest ints) (streamSched stream))) -  ==  sort ints+chanProp :: [Int] -> Scheduler -> Bool+chanProp ints sched =+  fmap sort (evalIOSpec (chanTest ints) sched)+  ===  Done (sort ints)  main = do putStrLn "Testing channels..."           quickCheck chanProp

@@ -3,42 +3,56 @@ -- definitions in the prelude and work with the pure specification.  import Prelude hiding (getChar, putChar)+import qualified Prelude (putStrLn) import qualified Data.Stream as Stream-import Test.IOSpec.Teletype+import Test.IOSpec hiding (putStrLn) import Test.QuickCheck+import Data.Char (ord)  -- The echo function, as we have always known it-echo :: IOTeletype ()+echo :: IOSpec Teletype () echo = getChar >>= putChar >> echo  -- It should echo any character entered at the teletype.  This is -- the behaviour we would expect echo to have.  The Output data type -- is defined in Test.IOSpec.Teletype and represents the observable -- behaviour of a teletype interaction.-copy :: Stream.Stream Char -> Output ()-copy (Stream.Cons x xs) = Print x (copy xs)+copy :: Effect ()+copy = ReadChar (\x -> Print x copy)  -- An auxiliary function that takes the first n elements printed to -- the teletype.-takeOutput :: Int -> Output () -> String+takeOutput :: Int -> Effect () -> String takeOutput 0 _ = "" takeOutput (n + 1) (Print c xs) = c : takeOutput n xs+takeOutput _ _ = error "Echo.takeOutput" +-- withInput runs an Effect, passing the argument stream of+-- characters as the characters entered to stdin. Any effects left+-- over will be either Print statements, or a final Done result.+withInput :: Stream.Stream Char -> Effect a -> Effect a+withInput stdin (Done x)     = Done x+withInput stdin (Print c e)  = Print c (withInput stdin e)+withInput stdin (ReadChar f) = withInput (Stream.tail stdin)+                                 (f (Stream.head stdin))+ -- We can use QuickCheck to test if our echo function meets the -- desired specification: that is that for every input the user -- enters, every finite prefix of runTT echo input and copy input is -- the same. echoProp :: Int -> Stream.Stream Char -> Property-echoProp n input = -  n > 0 ==>  -    takeOutput n (runTT echo input) -    == takeOutput n (copy input)+echoProp n input =+  n > 0 ==>+    takeOutput n (withInput input (evalIOSpec echo singleThreaded))+    == takeOutput n (withInput input copy)  instance Arbitrary Char where   arbitrary = choose ('a','z')+  coarbitrary = variant . ord -main = do putStrLn "Testing echo..."-          quickCheck echoProp+main = do+  Prelude.putStrLn "Testing echo..."+  quickCheck echoProp  -- Once we are satisfied with our definition of echo, we can change -- our imports. Rather than importing Test.IOSpec.Teletype, we

@@ -1,15 +1,17 @@ {-# OPTIONS_GHC -fglasgow-exts #-} import Test.QuickCheck-import Test.IOSpec.IORef+import Test.IOSpec hiding (putStrLn)+import Prelude hiding (putStrLn)+import qualified Prelude (putStrLn) import Data.Dynamic import Control.Monad  -- We begin by giving an implementation of queues using our pure -- specification of IORefs. -type Queue = (IORef Data, IORef Data)+type Queue = (IORef Cell, IORef Cell) -data Data  = Cell Int (IORef Data) | NULL deriving Typeable+data Cell = Cell Int (IORef Cell) | NULL deriving Typeable  -- There is one important point here. To use the IORefs in IOSpec, -- we need to make sure that any data we store in an IORef is an@@ -19,23 +21,23 @@ -- The implementation of Queues is fairly standard. We use a linked -- list, with special pointers to the head and tail of the queue. -emptyQueue :: IOState Queue-emptyQueue  = do  -  front <- newIORef NULL +emptyQueue :: IOSpec IORefS Queue+emptyQueue  = do+  front <- newIORef NULL   back <- newIORef NULL   return (front,back) -enqueue :: Queue -> Int -> IOState ()-enqueue (front,back) x = +enqueue :: Queue -> Int -> IOSpec IORefS ()+enqueue (front,back) x =   do  newBack <- newIORef NULL       let cell = Cell x newBack       c <- readIORef back-      writeIORef back cell +      writeIORef back cell       case c of         NULL -> writeIORef front cell         Cell y t -> writeIORef t cell -dequeue :: Queue -> IOState (Maybe Int)+dequeue :: Queue -> IOSpec IORefS (Maybe Int) dequeue (front,back) = do   c <- readIORef front   case c of@@ -47,7 +49,7 @@  -- Besides basic queue operations, we also implement queue reversal. -reverseQueue :: Queue -> IOState ()+reverseQueue :: Queue -> IOSpec IORefS () reverseQueue (front,back) = do   f <- readIORef front   case f of@@ -59,19 +61,19 @@       writeIORef front b       writeIORef back f -flipPointers :: Data -> Data -> IOState ()+flipPointers :: Cell -> Cell -> IOSpec IORefS () flipPointers prev NULL = return () flipPointers prev (Cell x next) = do       nextCell <- readIORef next       writeIORef next prev       flipPointers (Cell x next) nextCell-    + -- A pair of functions that convert lists to queues and vice versa. -queueToList :: Queue -> IOState [Int]+queueToList :: Queue -> IOSpec IORefS [Int] queueToList = unfoldM dequeue -listToQueue :: [Int] -> IOState Queue+listToQueue :: [Int] -> IOSpec IORefS Queue listToQueue xs = do q <- emptyQueue                     sequence_ (map (enqueue q) xs)                     return q@@ -83,31 +85,46 @@     Nothing -> return []     Just x -> liftM (x:) (unfoldM f a) --- Now we can state a few properties of queues.+-- When do we consider two Effects equal? In this case, we want the+-- same final result, and no other visible effects.+(===) :: Eq a => Effect a -> Effect a -> Bool+Done x === Done y = x == y+_ === _ = False +-- Now we can state a few properties of queues. inversesProp :: [Int] -> Bool-inversesProp xs = xs == runIOState (listToQueue xs >>= queueToList)+inversesProp xs =+  (return xs) === evalIOSpec (listToQueue xs >>= queueToList) singleThreaded -revRevProp xs = runIOState revRevProg == xs+revRevProp xs = evalIOSpec revRevProg singleThreaded === return xs   where   revRevProg = do q <- listToQueue xs                   reverseQueue q                   reverseQueue q                   queueToList q -revProp xs = runIOState revProg == reverse xs+revProp xs = evalIOSpec revProg singleThreaded === return (reverse xs)   where   revProg = do q <- listToQueue xs                reverseQueue q                queueToList q -queueProp1 x = runIOState queueProg1 == Just x+fifoProp :: [Int] -> Bool+fifoProp xs = evalIOSpec enqDeq singleThreaded === return xs   where+  enqDeq :: IOSpec IORefS [Int]+  enqDeq = do+    q <- emptyQueue+    forM_ xs (enqueue q)+    unfoldM dequeue q++queueProp1 x = evalIOSpec queueProg1 singleThreaded === Done (Just x)+  where   queueProg1 = do q <- emptyQueue                   enqueue q x                   dequeue q -queueProp2 x y = runIOState queueProg2 == Just y+queueProp2 x y = evalIOSpec queueProg2 singleThreaded === Done (Just y)   where   queueProg2 = do q <- emptyQueue                   enqueue q x@@ -115,15 +132,15 @@                   dequeue q                   dequeue q -main = do putStrLn "Testing first queue property..."+main = do Prelude.putStrLn "Testing first queue property..."           quickCheck queueProp1-          putStrLn "Testing second queue property..."+          Prelude.putStrLn "Testing second queue property..."           quickCheck queueProp2-          putStrLn "Testing queueToList and listToQueue.."+          Prelude.putStrLn "Testing queueToList and listToQueue.."           quickCheck inversesProp-          putStrLn "Testing that reverseQueue is its own inverse..."+          Prelude.putStrLn "Testing that reverseQueue is its own inverse..."           quickCheck revRevProp-          putStrLn "Testing reverseQueue matches the spec..."+          Prelude.putStrLn "Testing reverseQueue matches the spec..."           quickCheck revProp -- Once we are satisfied with our implementation, we can import the -- "real" Data.IORef instead of Test.IOSpec.IORef.

@@ -0,0 +1,23 @@+import Test.IOSpec+import Test.QuickCheck++readOnce :: Int -> IOSpec IORefS Int+readOnce x = do ref <- newIORef x+                readIORef ref++readTwice :: Int -> IOSpec IORefS Int+readTwice x = do ref <- newIORef x+                 readIORef ref+                 readIORef ref++readIORefProp :: Int -> Bool+readIORefProp x =+  let once  = evalIOSpec (readOnce x) singleThreaded+      twice = evalIOSpec (readTwice x) singleThreaded+  in once == twice++main = quickCheck readIORefProp++instance Eq a => Eq (Effect a) where+  (Done x) == (Done y) = x == y+  _ == _ = error "Incomparable effects."

@@ -0,0 +1,316 @@+{-# OPTIONS_GHC -fglasgow-exts #-}++-- Based on Graham Hutton's version of Richard Bird's Sudoku solver.+module Main where++import Data.List+import Control.Monad++-- Import these modules to test+import Test.IOSpec hiding (putStrLn)+import Test.QuickCheck++-- Drop the test modules and import these when you want to release+-- import Control.Concurrent+-- import Control.Concurrent.STM++type Grid             = Matrix Value+type Matrix a         = [Row a]+type Row a            = [TVar a]+type Value            = Char++data Sudoku = Sudoku [[Value]] deriving (Eq,Show)++type Concurrency = STMS :+: ForkS :+: MVarS++-- Some pure amenities++-- The size of the board+boxsize :: Int+boxsize =  3++-- The possible values of a cell+values :: [Value]+values =  ['1'..'9']++-- A dummy value representing the empty cell+empty :: Value -> Bool+empty =  (== '.')++-- When is a cell filled in or not+single     :: [a] -> Bool+single [_] = True+single _   = False++-- Some functions that return a list of nine rows, columns, or+-- boxes of a grid.+chop      :: Int -> [a] -> [[a]]+chop n [] =  []+chop n xs =  take n xs : chop n (drop n xs)++rows :: [[a]] -> [[a]]+rows =  id++cols :: [[a]] -> [[a]]+cols =  transpose++boxes :: [[a]] -> [[a]]+boxes =  unpack . map cols . pack+  where+    pack   = split . map split+    split  = chop boxsize+    unpack = map concat . concat++-- When does a list have no duplicates+nodups        :: Eq a => [a] -> Bool+nodups []     =  True+nodups (x:xs) =  not (elem x xs) && nodups xs++-- collapse takes a Grid where every cell contains a list of+-- possibilities, to a list of Grids where every cell contains a+-- single value.+collapse :: [[[a]]] -> [[[a]]]+collapse =  cp . map cp++-- cartesian product of a list of lists+cp          :: [[a]] -> [[a]]+cp []       =  [[]]+cp (xs:xss) =  [y:ys | y <- xs, ys <- cp xss]++-- The choices function reads in a Sudoku grid, replacing each+-- unknown entry by a TVar containing ['1' .. '9'] and each fixed+-- entry x by a TVar containing [x].+type Choices          =  [Value]++choices               :: [[Value]] -> STM (Matrix Choices)+choices vs            =  mapM (mapM choice) vs++choice :: Value -> STM (TVar [Value])+choice v = do+  newTVar $+    if empty v+    then values+    else return v++-- find all the digits that have been filled in+findSingles :: Row Choices -> STM [Value]+findSingles [] = return []+findSingles (xs:xss) = do+  v <- readTVar xs+  ss <- findSingles xss+  if single v then return (v ++ ss)+              else return ss++-- cross off all the digits that have been filled in+reduce :: Row Choices -> STM ()+reduce row = do+  singles <- findSingles row+  mapM_ (removeSingles singles) row++removeSingles :: Choices -> TVar Choices -> STM ()+removeSingles singles var = do+  v <- readTVar var+  writeTVar var (v `minus` singles)++-- the prune function prunes the search space, e.g. removing '9'+-- from the cells in a row/column/box if there is already a cell+-- with a '9' in said row/column/box. Using STM makes the+-- concurrency here quite neat - we can prune the rows, columns, and+-- boxes at the same time.+prune :: Matrix Choices -> IOSpec Concurrency ()+prune ms = do+  rowsDone <- newEmptyMVar+  colsDone <- newEmptyMVar+  boxesDone <- newEmptyMVar+  forkIO (pruneBy rowsDone rows ms)+  forkIO (pruneBy colsDone cols ms)+  forkIO (pruneBy boxesDone boxes ms)+  takeMVar rowsDone+  takeMVar colsDone+  takeMVar boxesDone++pruneBy :: MVar () -> (Matrix Choices -> Matrix Choices)+  -> Matrix Choices -> IOSpec Concurrency ()+pruneBy mvar f m = do+  atomically $ mapM_ reduce (f m)+  putMVar mvar ()++-- When is a matrix completely filled in?+complete              :: Matrix Choices -> STM Bool+complete m            =  liftM (all (all single)) (mapM (mapM readTVar) m)++-- When are we 'stuck', i.e. when there is a cell with no possible+-- choices left.+void                  :: Matrix Choices -> STM Bool+void m                =  liftM (any (any null)) (mapM (mapM readTVar) m)++minus                 :: Choices -> Choices -> Choices+xs `minus` ys         =  if single xs then xs else xs \\ ys++-- A board is consistent if there are no duplicates in every row,+-- column, and box.+isInconsistent    :: Matrix Choices -> STM Bool+isInconsistent cm = do+  rowC <- liftM (all consistent) (mapM (mapM readTVar) (rows cm))+  colC <- liftM (all consistent) (mapM (mapM readTVar) (cols cm))+  boxC <- liftM (all consistent) (mapM (mapM readTVar) (boxes cm))+  return (not (rowC && colC && boxC))++consistent            :: [[Value]] -> Bool+consistent            =  nodups . concat . filter single++-- A board is blocked if it is void or inconsistent+blocked               :: Matrix Choices -> STM Bool+blocked m             =  liftM2 (||) (void m) (isInconsistent m)++-- The search function checks+--+-- * if the board is blocked, we cannot make any progress in this+-- thread+--+-- * if the board is complete, we are done and fill in the MVar+-- waiting for the result.+--+-- * otherwise, expand the cell with the smallest number of+-- remaining choices to make a list of boards, corresponding to the+-- possible ways to fill in that cell. We then fork off a thread to+-- try and find a solution for every board in that list.+search :: MVar [[Value]] -> Matrix Choices -> IOSpec Concurrency ()+search mvar m = do+  isBlocked <- atomically $ blocked m+  isComplete <- atomically $ complete m+  if isBlocked+    then return ()+    else+      if isComplete+      then do+        result <- atomically $ liftM collapse (mapM (mapM readTVar) m)+        putMVar mvar (head result)+      else do+        ms <- expand m+        mapM_ (\m -> forkIO (prune m >> search mvar m)) ms++expand :: Matrix Choices -> IOSpec Concurrency ([Matrix Choices])+expand matrix = do+  ms <- atomically $ mapM (mapM readTVar) matrix+  let mms = expand' ms+  atomically $ mapM (mapM (mapM newTVar)) mms++expand'                :: [[Choices]] -> [[[Choices]]]+expand' m              =+   [rows1 ++ [row1 ++ [c] : row2] ++ rows2 | c <- cs]+   where+      (rows1,row:rows2) = break (any p) m+      (row1,cs:row2)    = break p row+      p xs              = length xs == minLength+      minLength         = minimum (filter (> 1) (concatMap (map length) m))+++-- The solve function makes an empty MVar, reads in the board,+-- prunes it, and searches for solutions. Once a solution is found,+-- it will be written to the MVar and returned.+solve :: Sudoku -> IOSpec Concurrency Sudoku+solve (Sudoku grid) = do+  solution <- newEmptyMVar+  matrix <- atomically $ choices grid+  prune matrix+  search solution matrix+  sol <- takeMVar solution+  return (Sudoku sol)+++-- Examples+easy :: Sudoku+easy = Sudoku+        ["2....1.38",+         "........5",+         ".7...6...",+         ".......13",+         ".981..257",+         "31....8..",+         "9..8...2.",+         ".5..69784",+         "4..25...."]++gentle :: Sudoku+gentle = Sudoku+           [".1.42...5",+           "..2.71.39",+           ".......4.",+           "2.71....6",+           "....4....",+           "6....74.3",+           ".7.......",+           "12.73.5..",+           "3...82.7."]++diabolical :: Sudoku+diabolical = Sudoku+               [".9.7..86.",+               ".31..5.2.",+               "8.6......",+               "..7.5...6",+               "...3.7...",+               "5...1.7..",+               "......1.9",+               ".2.6..35.",+               ".54..8.7."]++solution :: [[Value]]+solution = ["295743861",+            "431865927",+            "876192543",+            "387459216",+            "612387495",+            "549216738",+            "763524189",+            "928671354",+            "154938672"]++-- Given a sudoku puzzle, solve it and check that your solution is ok.+unsolved :: Sudoku -> Int+unsolved (Sudoku xs) = length $ filter (== '.') (concat xs)++correctProp sudoku sched =+  let+    (Done computed) = evalIOSpec (solve sudoku) sched+  in collect (unsolved sudoku) (isSolution computed)++-- Determines when a sudoku has been filled in properly.+isSolution :: Sudoku -> Bool+isSolution (Sudoku grid) =+  isOk (boxes grid) && isOk (cols grid) && isOk (rows grid)+  where+    isOk xss = all (== values) (map sort xss)++-- To generate a random sudoku puzzle, we delete a number of cells+-- from a solved grid.+instance Arbitrary Sudoku where+  arbitrary  = do+    xs <- arbitrary+    return (Sudoku $ blankOut xs (concat solution))+  coarbitrary = error "No instance coarbitrary for Sudoku grids"++blankOut :: [Int] -> [Value] -> [[Value]]+blankOut [] grid     = chop (boxsize * boxsize) grid+blankOut (x:xs) grid =+  let+    y = x `mod` 81+  in blankOut xs (replace y '.' grid)++replace :: Eq a => Int -> a -> [a] -> [a]+replace n x xs = take n xs ++ [x] ++ drop (n+1) xs++main = do+  putStrLn "Running QuickCheck tests..."+  -- A few unit tests+  putStrLn "Solving easy..."+  quickCheck (correctProp easy)+  putStrLn "Solving gentle..."+  quickCheck (correctProp gentle)+  putStrLn "Solving diabolical..."+  quickCheck (correctProp diabolical)+--   -- QuickCheck the solver+  putStrLn "Solving random tests..."+  quickCheck correctProp+

@@ -1,178 +0,0 @@--- | Streams are infinite lists. Most operations on streams are--- completely analogous to the definition in Data.List.--module Data.Stream-   (-     Stream(..) -   , head -   , tail-   , intersperse -   , iterate-   , repeat-   , cycle-   , unfold -   , take-   , drop-   , splitAt-   , takeWhile-   , dropWhile-   , span-   , break-   , isPrefixOf-   , filter-   , partition-   , (!!)-   , zip-   , zipWith-   , unzip-   , words-   , unwords-   , lines-   , unlines-   , listToStream-   , streamToList-   )-   where--import Prelude hiding (head, tail, iterate, take, drop, takeWhile,-  dropWhile, repeat, cycle, filter, (!!), zip, unzip,-  zipWith,words,unwords,lines,unlines, break, span, splitAt)--import Control.Applicative-import Data.Char (isSpace)-import Test.QuickCheck--data Stream a = Cons a (Stream a) deriving (Show, Eq)--instance Functor Stream where-  fmap f (Cons x xs) = Cons (f x) (fmap f xs)--instance Applicative Stream where-  pure = repeat-  (<*>) = zipWith ($)--instance Arbitrary a => Arbitrary (Stream a) where-  arbitrary = do  x <- arbitrary-                  xs <- arbitrary-                  return (Cons x xs)-  coarbitrary = coarbitrary . streamToList--head :: Stream a -> a-head (Cons x _ ) = x--tail :: Stream a -> Stream a-tail (Cons _ xs) = xs--intersperse :: a -> Stream a -> Stream a-intersperse y (Cons x xs) = Cons x (Cons y (intersperse y xs))--unfold :: (c -> (a,c)) -> c -> Stream a-unfold f c = -  let (x,d) = f c -  in Cons x (unfold f d)-          -iterate :: (a -> a) -> a -> Stream a-iterate f x = Cons x (iterate f (f x))--take :: Int -> Stream a  -> [a]-take n (Cons x xs)-  | n == 0    = []-  | n > 0     =  x : (take (n - 1) xs)-  | otherwise = error "Stream.take: negative argument."--drop n xs-  | n == 0    = xs-  | n > 0     = drop (n - 1) (tail xs)-  | otherwise = error "Stream.drop: negative argument."--takeWhile :: (a -> Bool) -> Stream a -> [a]-takeWhile p (Cons x xs)-  | p x       = x : takeWhile p xs-  | otherwise = []--dropWhile :: (a -> Bool) -> Stream a -> Stream a-dropWhile p (Cons x xs)-  | p x       = dropWhile p xs-  | otherwise = Cons x xs--repeat :: a -> Stream a-repeat x = Cons x (repeat x)--cycle :: [a] -> Stream a-cycle xs = foldr Cons (cycle xs) xs--filter :: (a -> Bool) -> Stream a -> Stream a-filter p (Cons x xs)-  | p x       = Cons x (filter p xs)-  | otherwise = filter p xs--(!!) :: Int -> Stream a -> a-(!!) n (Cons x xs)-  | n == 0    = x-  | n > 0     = (!!) (n - 1) xs-  | otherwise = error "Stream.!! negative argument"--zip :: Stream a -> Stream b -> Stream (a,b)-zip (Cons x xs) (Cons y ys) = Cons (x,y) (zip xs ys)--unzip :: Stream (a,b) -> (Stream a, Stream b)-unzip (Cons (x,y) xys) = (Cons x (fst (unzip xys)),-                                Cons y (snd (unzip xys)))     --zipWith :: (a -> b -> c) -> Stream a -> Stream b -> Stream c-zipWith f (Cons x xs) (Cons y ys) = Cons (f x y) (zipWith f xs ys)--span :: (a -> Bool) -> Stream a -> ([a], Stream a)-span p (Cons x xs)-  | p x       = let (trues, falses) = span p xs-                in (x : trues, falses)-  | otherwise = ([], Cons x xs)--break :: (a -> Bool) -> Stream a -> ([a], Stream a)-break p = span (not . p)--words :: Stream Char -> Stream String-words xs = let (w, ys) = break isSpace xs-                 in Cons w (words ys)--unwords :: Stream String -> Stream Char-unwords (Cons x xs) = foldr Cons (Cons ' ' (unwords xs)) x--lines :: Stream Char -> Stream String-lines xs = let (l, ys) = break (== '\n') xs-                 in Cons l (lines (tail ys))--unlines :: Stream String -> Stream Char-unlines (Cons x xs) = foldr Cons (Cons '\n' (unlines xs)) x--isPrefixOf :: Eq a => [a] -> Stream a -> Bool-isPrefixOf [] _ = True-isPrefixOf (y:ys) (Cons x xs)-  | y == x    = isPrefixOf ys xs-  | otherwise = False--partition :: (a -> Bool) -> Stream a -> (Stream a, Stream a)-partition p (Cons x xs) = -  let (trues,falses) = partition p xs-  in if p x then (Cons x trues, falses)-            else (trues, Cons x falses)--inits :: Stream a -> Stream ([a])-inits (Cons x xs) = Cons [] (fmap (x:) (inits xs))--tails :: Stream a -> Stream (Stream a)-tails xs = Cons xs (tails (tail xs))--splitAt :: Int -> Stream a -> ([a], Stream a)-splitAt n xs-  | n == 0    = ([],xs)-  | n > 0     = let (prefix,rest) = splitAt (n-1) (tail xs)-                in (head xs : prefix, rest)-  | otherwise = error "Stream.splitAt negative argument."--streamToList :: Stream a -> [a]-streamToList (Cons x xs) = x : streamToList xs--listToStream (x:xs) = Cons xs (listToStream xs)-listToStream []     = error "Stream.listToStream applied to finite list"-

@@ -1,10 +1,21 @@ module Test.IOSpec   (-    module Test.IOSpec.IORef-  , module Test.IOSpec.Concurrent+-- * The specifications+    module Test.IOSpec.Fork+  , module Test.IOSpec.MVar+  , module Test.IOSpec.IORef+  , module Test.IOSpec.STM   , module Test.IOSpec.Teletype+-- * The basic types+  , module Test.IOSpec.Types+-- * The virtual machine+  , module Test.IOSpec.VirtualMachine   ) where -import Test.IOSpec.Concurrent+import Test.IOSpec.Fork+import Test.IOSpec.MVar import Test.IOSpec.IORef+import Test.IOSpec.STM import Test.IOSpec.Teletype+import Test.IOSpec.Types+import Test.IOSpec.VirtualMachine

@@ -1,282 +0,0 @@-{-#  OPTIONS -fglasgow-exts -fno-warn-missing-fields  #-}--- | A pure specification of basic concurrency operations.--module Test.IOSpec.Concurrent-   (-   -- * The IOConc monad-     IOConc-   , runIOConc-   -- * Supported functions-   , ThreadId-   , MVar-   , newEmptyMVar-   , takeMVar-   , putMVar-   , forkIO-   -- * Schedulers-   , Scheduler(..)-   , streamSched-   , roundRobin-   )-   where --import Data.Dynamic-import Data.Maybe (fromJust)-import Data.List (nub)-import Control.Monad.State-import qualified Data.Stream as Stream---- The IOConc data type and its instances-newtype ThreadId  = ThreadId Int deriving (Eq, Show)-type Data         = Dynamic-type Loc          = Int--data IOConc a = -     NewEmptyMVar (Loc -> IOConc a) -  |  TakeMVar Loc (Data -> IOConc a) -  |  PutMVar Loc Data (IOConc a)-  |  forall b . Fork  (IOConc b) (ThreadId -> IOConc  a)-  |  Return a --instance Functor IOConc where -  fmap f (Return x) = Return (f x)-  fmap f (NewEmptyMVar io) = NewEmptyMVar (\l -> fmap f (io l))-  fmap f (TakeMVar l io) = TakeMVar l (\d -> fmap f (io d))-  fmap f (PutMVar l d io) = PutMVar l d (fmap f io)-  fmap f (Fork l io)      = Fork l (\tid -> fmap f (io tid))--instance Monad IOConc where-  return = Return-  (Return x) >>= g       = g x-  (NewEmptyMVar f) >>= g = NewEmptyMVar (\l -> f l >>= g)-  (TakeMVar l f) >>= g   = TakeMVar l (\d -> f d >>= g)-  PutMVar c d f >>= g    = PutMVar c d (f >>= g)-  Fork p1 p2 >>= g       = Fork p1 (\tid -> p2 tid >>= g)---- | An 'MVar' is a shared, mutable variable.-newtype MVar a = MVar Loc deriving Typeable---- | The 'newEmptyMVar' function creates a new 'MVar' that is initially empty.-newEmptyMVar        :: IOConc (MVar a)-newEmptyMVar        = NewEmptyMVar (Return . MVar)- --- | The 'takeMVar' function removes the value stored in an--- 'MVar'. If the 'MVar' is empty, the thread is blocked.-takeMVar            :: Typeable a => MVar a -> IOConc a-takeMVar (MVar l)   = TakeMVar l (Return . unsafeFromDynamic)---- | The 'putMVar' function fills an 'MVar' with a new value. If the--- 'MVar' is not empty, the thread is blocked.-putMVar             :: Typeable a => MVar a -> a -> IOConc ()-putMVar (MVar l) d  = PutMVar l (toDyn d) (Return ())---- | The 'forkIO' function forks off a new thread.-forkIO              :: IOConc a -> IOConc ThreadId -forkIO p            = Fork p Return---- The scheduler and store---- | A scheduler consists of a function that, given the number of--- threads, returns the 'ThreadId' of the next scheduled thread,--- together with a new scheduler.-newtype Scheduler = -  Scheduler (Int -> (ThreadId, Scheduler))--data ThreadStatus = -     forall b . Running (IOConc b) -  |  Finished--type Heap = Loc -> Maybe Data--data Store   = Store    {  fresh :: Loc-                        ,  heap :: Heap-                        ,  nextTid :: ThreadId-                        ,  soup :: ThreadId -> ThreadStatus-                        ,  scheduler :: Scheduler-                        ,  blockedThreads :: [ThreadId]-                        }--initStore :: Scheduler -> Store-initStore s   = Store  {   fresh    = 0 -                        ,  nextTid   = ThreadId 1-                        ,  scheduler = s-                        ,  blockedThreads = []-                        }---- | The 'runIOConc' function runs a concurrent computation with a given scheduler.--- If a deadlock occurs, Nothing is returned.--runIOConc :: IOConc a -> Scheduler -> Maybe a-runIOConc io s = evalState (interleave io) (initStore s)---- A single step--data Status a = Stop a | Step (IOConc a) | Blocked --step ::  IOConc a -> State Store (Status a)-step (Return a) = return (Stop a)-step (NewEmptyMVar f)-  = do  loc <- alloc-        modifyHeap (update loc Nothing)-        return (Step (f loc))-step (TakeMVar l f)  -  = do  var <- lookupHeap l-        case var of-          Nothing   ->  return Blocked-          (Just d)  ->  do  emptyMVar l-                            return (Step (f d))-step (PutMVar l d p)   -  = do  var <- lookupHeap l-        case var of-          Nothing   ->  do  fillMVar l d-                            return (Step p)-          (Just d)  ->  return Blocked-step (Fork l r)        -  = do  tid <- freshThreadId-        extendSoup l tid-        return (Step (r tid))--emptyMVar :: Loc -> State Store ()-emptyMVar l = modifyHeap (update l Nothing)--fillMVar :: Loc -> Data -> State Store ()-fillMVar l d = modifyHeap (update l (Just d))--extendSoup :: IOConc a -> ThreadId -> State Store () -extendSoup p tid = modifySoup (update tid (Running p))---- Interleaving steps--data Process a = -     Main (IOConc a)-  |  forall b . Aux (IOConc b)--interleave :: IOConc a -> State Store (Maybe a)-interleave main  -  = do  (tid,t) <- schedule main-        case t of-          Main p -> -            do  x <- step p-                case x of-                  Stop r   ->  return (Just r)-                  Step p   ->  do resetBlockedThreads-                                  interleave p-                  Blocked  ->  do isDeadlock <- detectDeadlock-                                  if isDeadlock -                                    then return Nothing-                                    else interleave main-          Aux p -> -            do  x <- step p-                case x of-                  Stop _   ->   do  resetBlockedThreads-                                    finishThread tid-                                    interleave main-                  Step q   ->   do  resetBlockedThreads-                                    extendSoup q tid-                                    interleave main-                  Blocked  ->   do  recordBlockedThread tid-                                    interleave main--schedule :: IOConc a -> State Store (ThreadId, Process a)-schedule main = do  (ThreadId tid) <- getNextThreadId-                    if tid == 0 -                      then return (ThreadId 0, Main main)-                      else do-                        tsoup <- gets soup-                        case tsoup (ThreadId tid) of-                          Finished ->  schedule main-                          Running p -> return (ThreadId tid, Aux p)-                          --getNextThreadId :: State Store ThreadId-getNextThreadId = do  Scheduler sch <- gets scheduler-                      (ThreadId n) <- gets nextTid-                      let (tid,s) = sch n-                      modifyScheduler (const s)-                      return tid----- | Given a stream of integers, 'streamSched' builds a--- scheduler. This is especially useful if you use QuickCheck and--- generate a random stream; the resulting random scheduler will--- hopefully cover a large number of interleavings.--streamSched :: Stream.Stream Int -> Scheduler-streamSched xs = -  Scheduler (\k -> (ThreadId (Stream.head xs `mod` k), streamSched (Stream.tail xs)))----- | A simple round-robin scheduler.-roundRobin :: Scheduler-roundRobin = streamSched (Stream.unfold (\k -> (k, k+1)) 0)---- Utilities--freshThreadId :: State Store ThreadId-freshThreadId = do tid <- gets nextTid-                   modifyTid (\(ThreadId k) -> ThreadId (k + 1))-                   return tid--alloc :: State Store Loc -alloc = do  loc <- gets fresh-            modifyFresh ((+) 1)-            return loc--lookupHeap :: Loc -> State Store (Maybe Data)-lookupHeap l = do  h <- gets heap-                   return (h l)--extendHeap :: Loc -> Data -> State Store ()-extendHeap l d  = modifyHeap (update l (Just d))--finishThread :: ThreadId -> State Store ()-finishThread tid = modifySoup (update tid Finished)--resetBlockedThreads :: State Store ()-resetBlockedThreads = modifyBlockedThreads (const [])--recordBlockedThread :: ThreadId -> State Store ()-recordBlockedThread tid = do -  tids <- gets blockedThreads-  if tid `elem` tids -    then return ()-    else modifyBlockedThreads (tid :)--detectDeadlock :: State Store Bool-detectDeadlock = do blockedThreads <- liftM length (gets blockedThreads)                   -                    (ThreadId nrThreads) <- gets nextTid-                    threadSoup <- gets soup-                    let allThreadIds = [ThreadId x | x <- [1 .. (nrThreads - 1)]]-                    let finishedThreads = length $ filter isFinished (map threadSoup allThreadIds)-                    return (blockedThreads + finishedThreads == nrThreads - 1)--isFinished :: ThreadStatus -> Bool-isFinished Finished = True-isFinished _        = False-                       --update :: Eq a => a -> b -> (a -> b) -> (a -> b)-update l d h k-  | l == k       = d-  | otherwise    = h k--unsafeFromDynamic :: Typeable a => Dynamic -> a-unsafeFromDynamic = fromJust . fromDynamic--modifyHeap f            = do s <- get-                             put (s {heap = f (heap s)})--modifyScheduler f       = do s <- get-                             put (s {scheduler = f (scheduler s)})--modifyFresh f           = do s <- get-                             put (s {fresh = f (fresh s)})--modifyTid f             = do s <- get-                             put (s {nextTid = f (nextTid s)})- -modifySoup f            = do s <- get-                             put (s {soup = f (soup s)})--modifyBlockedThreads f     = do s <- get-                                put (s {blockedThreads = f (blockedThreads s)})

@@ -0,0 +1,34 @@+-- | A pure specification of 'forkIO'.+module Test.IOSpec.Fork+   (+     ForkS+   , forkIO+   )+   where++import Test.IOSpec.VirtualMachine+import Test.IOSpec.Types++-- The 'ForkS' data type and its instances.+--+-- | An expression of type @IOSpec ForkS a@ corresponds to an 'IO'+-- computation that uses 'forkIO' and returns a value of+-- type 'a'.+--+-- By itself, 'ForkS' is not terribly useful. You will probably want+-- to use @IOSpec (ForkS :+: MVarS)@ or @IOSpec (ForkS :+: STMS)@.+data ForkS a =+  forall f b . Executable f => Fork (IOSpec f b) (ThreadId -> a)++instance Functor ForkS where+  fmap f (Fork l io)      = Fork l (f . io)++-- | The 'forkIO' function forks off a new thread.+forkIO :: (Executable f, ForkS :<: g) => IOSpec f a -> IOSpec g ThreadId+forkIO p =  inject (Fork p return)++instance Executable ForkS where+  step (Fork t p) = do+    tid <- freshThreadId+    updateSoup tid t+    return (Step (p tid))

@@ -1,116 +1,67 @@--{-#  OPTIONS -fglasgow-exts -fno-warn-missing-fields  #-}---- | A pure specification of mutable variables. -module Test.IOSpec.IORef +-- | A pure specification of mutable variables.+module Test.IOSpec.IORef    (-    -- * The IOState monad-     IOState-   , runIOState-    -- * Manipulation of IORefs+    -- * The 'IORefS' spec+     IORefS+    -- * Manipulation and creation of IORefs    , IORef    , newIORef    , readIORef    , writeIORef    , modifyIORef-   ) +   )    where -import Control.Monad.State  import Data.Dynamic import Data.Maybe (fromJust)+import Test.IOSpec.Types+import Test.IOSpec.VirtualMachine -type Data           = Dynamic-type Loc            = Int --- | The IOState monad--data IOState a  = -     NewIORef Data (Loc -> IOState a) -  |  ReadIORef Loc (Data -> IOState a)-  |  WriteIORef Loc Data (IOState  a) -  |  Return a --instance Functor IOState where-  fmap f (NewIORef d io)     = NewIORef d (\l -> fmap f (io l))-  fmap f (ReadIORef l io)    = ReadIORef l (\d -> fmap f (io d))-  fmap f (WriteIORef l d io) = WriteIORef l d (fmap f io)-  fmap f (Return x)     = Return (f x)+-- The 'IORefS' spec.+-- | An expression of type @IOSpec IORefS a@ corresponds to an @IO@+-- computation that uses mutable references and returns a value of+-- type @a@.+data IORefS a  =+     NewIORef Data (Loc -> a)+  |  ReadIORef Loc (Data -> a)+  |  WriteIORef Loc Data a -instance Monad IOState where-  return                    = Return-  (Return a) >>= g          = g a-  (NewIORef d f) >>= g      = NewIORef d (\l -> f l >>= g)-  (ReadIORef l f) >>= g     = ReadIORef l (\d -> f d >>= g)-  (WriteIORef l d s) >>= g  = WriteIORef l d (s >>= g)+instance Functor IORefS where+  fmap f (NewIORef d io)     = NewIORef d (f . io)+  fmap f (ReadIORef l io)    = ReadIORef l (f . io)+  fmap f (WriteIORef l d io) = WriteIORef l d (f io) --- | A mutable variable in the IOState monad+-- | A mutable variable storing a value of type a. Note that the+-- types stored by an 'IORef' are assumed to be @Typeable@. newtype IORef a = IORef Loc  -- | The 'newIORef' function creates a new mutable variable.-newIORef :: Typeable a => a -> IOState (IORef a)-newIORef d = NewIORef (toDyn d) (Return . IORef)+newIORef :: (Typeable a, IORefS :<: f) => a -> IOSpec f (IORef a)+newIORef d = inject $ NewIORef (toDyn d) (return . IORef)  -- | The 'readIORef' function reads the value stored in a mutable variable.-readIORef :: Typeable a => IORef a -> IOState a-readIORef (IORef l) = ReadIORef l (Return . unsafeFromDynamic)+readIORef :: (Typeable a, IORefS :<:f ) => IORef a -> IOSpec f a+readIORef (IORef l) = inject $ ReadIORef l (return .  fromJust . fromDynamic) --- | The 'writeIORef' function overwrites the value stored in an IORef.-writeIORef :: Typeable a => IORef a -> a -> IOState ()-writeIORef (IORef l) d = WriteIORef l (toDyn d) (Return ())+-- | The 'writeIORef' function overwrites the value stored in a+-- mutable variable.+writeIORef :: (Typeable a, IORefS :<: f) => IORef a -> a -> IOSpec f ()+writeIORef (IORef l) d = inject $ WriteIORef l (toDyn d) (return ()) --- | The 'modifyIORef' function applies a function to the value stored in --- and IORef.-modifyIORef :: Typeable a => IORef a -> (a -> a) -> IOState ()+-- | The 'modifyIORef' function applies a function to the value stored in+-- and 'IORef'.+modifyIORef :: (Typeable a, IORefS :<: f)+  => IORef a -> (a -> a) -> IOSpec f () modifyIORef ref f = readIORef ref >>= \x -> writeIORef ref (f x) -unsafeFromDynamic :: Typeable a => Dynamic -> a-unsafeFromDynamic = fromJust . fromDynamic--data Store = Store {fresh :: Loc, heap :: Heap}-type Heap = Loc -> Data --emptyStore :: Store-emptyStore = Store {fresh = 0}---- | The 'runIOState' function executes a computation in the `IOState' monad.-runIOState :: IOState a -> a-runIOState io = evalState (step io) emptyStore--step :: IOState a -> State Store a-step (Return a) = return a-step (NewIORef d g)      -  = do  loc <- alloc-        extendHeap loc d-        step (g loc) -step (ReadIORef l g)     -  = do  d <- lookupHeap l-        step (g d)-step (WriteIORef l d p)-  = do  extendHeap l d-        step p--alloc :: State Store Loc -alloc = do  loc <- gets fresh-            modifyFresh ((+) 1)-            return loc--lookupHeap :: Loc -> State Store Data-lookupHeap l = do  h <- gets heap-                   return (h l)--extendHeap :: Loc -> Data -> State Store ()-extendHeap l d  = modifyHeap (update l d)--modifyHeap :: (Heap -> Heap) -> State Store ()-modifyHeap f = do  s <- get-                   put (s {heap = f (heap s)})--modifyFresh :: (Loc -> Loc) -> State Store ()-modifyFresh f = do  s <- get-                    put (s {fresh = f (fresh s)})+-- | The 'Executable' instance for the `IORefS' monad.+instance Executable IORefS where+  step (NewIORef d t)     = do loc <- alloc+                               updateHeap loc d+                               return (Step (t loc))+  step (ReadIORef l t)    = do Just d <- lookupHeap l+                               return (Step (t d))+  step (WriteIORef l d t) = do updateHeap l d+                               return (Step t) -update :: Loc -> Data -> Heap -> Heap-update l d h k-  | l == k       = d-  | otherwise    = h k

@@ -0,0 +1,71 @@+-- | A pure specification of basic operations on MVars.++module Test.IOSpec.MVar+   (+   -- * The 'MVarS' spec+     MVarS+   -- * Supported functions+   , MVar+   , newEmptyMVar+   , takeMVar+   , putMVar+   )+   where++import Data.Dynamic+import Data.Maybe (fromJust)+import Test.IOSpec.Types+import Test.IOSpec.VirtualMachine++-- The 'MVarS' data type and its instances.+--+-- | An expression of type @IOSpec MVarS a@ corresponds to an @IO@+-- computation that uses shared, mutable variables and returns a+-- value of type @a@.+--+-- By itself, 'MVarS' is not terribly useful. You will probably want+-- to use @IOSpec (ForkS :+: MVarS)@.++data MVarS a =+     NewEmptyMVar (Loc -> a)+  |  TakeMVar Loc (Data -> a)+  |  PutMVar Loc Data a++instance Functor MVarS where+  fmap f (NewEmptyMVar io) = NewEmptyMVar (f . io)+  fmap f (TakeMVar l io) = TakeMVar l (f . io)+  fmap f (PutMVar l d io) = PutMVar l d (f io)++-- | An 'MVar' is a shared, mutable variable.+newtype MVar a = MVar Loc deriving Typeable++-- | The 'newEmptyMVar' function creates a new 'MVar' that is initially empty.+newEmptyMVar        :: (Typeable a, MVarS :<: f) => IOSpec f (MVar a)+newEmptyMVar        = inject $ NewEmptyMVar (return . MVar)++-- | The 'takeMVar' function removes the value stored in an+-- 'MVar'. If the 'MVar' is empty, the thread is blocked.+takeMVar            :: (Typeable a, MVarS :<: f) => MVar a -> IOSpec f a+takeMVar (MVar l)   = inject $ TakeMVar l (return . fromJust . fromDynamic)++-- | The 'putMVar' function fills an 'MVar' with a new value. If the+-- 'MVar' is not empty, the thread is blocked.+putMVar             :: (Typeable a, MVarS :<: f) => MVar a -> a -> IOSpec f ()+putMVar (MVar l) d  = inject $ PutMVar l (toDyn d) (return ())++instance Executable MVarS where+  step (NewEmptyMVar t) = do loc <- alloc+                             emptyLoc loc+                             return (Step (t loc))+  step (TakeMVar loc t) = do var <- lookupHeap loc+                             case var of+                               Nothing -> return Block+                               Just x -> do+                                 emptyLoc loc+                                 return (Step (t x))+  step (PutMVar loc d t) = do var <- lookupHeap loc+                              case var of+                                Nothing -> do+                                  updateHeap loc d+                                  return (Step t)+                                Just _ -> return Block

@@ -0,0 +1,132 @@+module Test.IOSpec.STM+   (+   -- * The specification of STM+     STMS+   -- * Atomically+   , atomically+   -- * The STM monad+   , STM+   , TVar+   , newTVar+   , readTVar+   , writeTVar+   , retry+   , orElse+   , check+   )+   where++import Test.IOSpec.VirtualMachine+import Test.IOSpec.Types+import Data.Dynamic+import Data.Maybe (fromJust)+import Control.Monad.State++-- The 'STMS' data type and its instances.+--+-- | An expression of type @IOSpec 'STMS' a@ corresponds to an 'IO'+-- computation that may use 'atomically' and returns a value of type+-- @a@.+--+-- By itself, 'STMS' is not terribly useful. You will probably want+-- to use @IOSpec (ForkS :+: STMS)@.+data STMS a =+  forall b . Atomically (STM b) (b -> a)++instance Functor STMS where+  fmap f (Atomically s io) = Atomically s (f . io)++-- | The 'atomically' function atomically executes an 'STM' action.+atomically     :: (STMS :<: f) => STM a -> IOSpec f a+atomically stm = inject $ Atomically stm (return)++instance Executable STMS where+  step (Atomically stm b) =+    do state <- get+       case runStateT (executeSTM stm) state of+         Done (Nothing,_)         -> return Block+         Done (Just x,finalState) -> put finalState >> return (Step (b x))+         _                        -> internalError "Unsafe usage of STM"++-- The 'STM' data type and its instances.+data STM a =+    STMReturn a+  | NewTVar Data (Loc -> STM a)+  | ReadTVar Loc (Data -> STM a)+  | WriteTVar Loc Data (STM a)+  | Retry+  | OrElse (STM a) (STM a)++instance Functor STM where+  fmap f (STMReturn x)      = STMReturn (f x)+  fmap f (NewTVar d io)     = NewTVar d (fmap f . io)+  fmap f (ReadTVar l io)    = ReadTVar l (fmap f . io)+  fmap f (WriteTVar l d io) = WriteTVar l d (fmap f io)+  fmap _ Retry              = Retry+  fmap f (OrElse io1 io2)   = OrElse (fmap f io1) (fmap f io2)++instance Monad STM where+    return                = STMReturn+    STMReturn a >>= f     = f a+    NewTVar d g >>= f     = NewTVar d (\l -> g l >>= f)+    ReadTVar l g >>= f    = ReadTVar l (\d -> g d >>= f)+    WriteTVar l d p >>= f = WriteTVar l d (p >>= f)+    Retry >>= _           = Retry+    OrElse p q >>= f      = OrElse (p >>= f) (q >>= f)++-- | A 'TVar' is a shared, mutable variable used by STM.+newtype TVar a = TVar Loc++-- | The 'newTVar' function creates a new transactional variable.+newTVar   :: Typeable a => a -> STM (TVar a)+newTVar d = NewTVar (toDyn d) (STMReturn . TVar)++-- | The 'readTVar' function reads the value stored in a+-- transactional variable.+readTVar          :: Typeable a => TVar a -> STM a+readTVar (TVar l) = ReadTVar l (STMReturn . fromJust . fromDynamic)++-- | The 'writeTVar' function overwrites the value stored in a+-- transactional variable.+writeTVar            :: Typeable a => TVar a -> a -> STM ()+writeTVar (TVar l) d = WriteTVar l (toDyn d) (STMReturn ())++-- | The 'retry' function abandons a transaction and retries at some+-- later time.+retry :: STM a+retry = Retry++-- | The 'check' function checks if its boolean argument holds. If+-- the boolean is true, it returns (); otherwise it calls 'retry'.+check       :: Bool -> STM ()+check True  = return ()+check False = retry++-- | The 'orElse' function takes two 'STM' actions @stm1@ and @stm2@ and+-- performs @stm1@. If @stm1@ calls 'retry' it performs @stm2@. If @stm1@+-- succeeds, on the other hand, @stm2@ is not executed.+orElse     :: STM a -> STM a -> STM a+orElse p q = OrElse p q++executeSTM :: STM a -> VM (Maybe a)+executeSTM (STMReturn x)      = return (return x)+executeSTM (NewTVar d io)     = do+  loc <- alloc+  updateHeap loc d+  executeSTM (io loc)+executeSTM (ReadTVar l io)    = do+  (Just d) <- lookupHeap l+  executeSTM (io d)+executeSTM (WriteTVar l d io) = do+  updateHeap l d+  executeSTM io+executeSTM Retry              = return Nothing+executeSTM (OrElse p q)       = do+  state <- get+  case runStateT (executeSTM p) state of+    Done (Nothing,_) -> executeSTM q+    Done (Just x,s)  -> put s >> return (Just x)+    _                -> internalError "Unsafe usage of STM"++internalError :: String -> a+internalError msg = error ("IOSpec.STM: " ++ msg)

@@ -0,0 +1,31 @@+-- | This module contains a few type signatures to help replace pure+-- specifications by their effectful counterparts.+module Test.IOSpec.Surrogate+  (+  -- * The IOSpec type+    IOSpec+  -- * The specifications+  , ForkS+  , MVarS+  , IORefS+  , STMS+  , Teletype+  , (:+:)+  )+  where++-- | The @IOSpec f a@ is merely type synonym for @IO a@. Once you've+-- tested a module, you can use these definitions to avoid having to+-- change your type signatures.+--+-- Note that because this definition of 'IOSpec' ignores its @f@+-- argument, each of 'ForkS', 'MVarS', etc., is simply an empty data+-- type.+type IOSpec f a  = IO a++data ForkS+data MVarS+data IORefS+data STMS+data Teletype+data (f :+: g)

@@ -1,60 +1,66 @@--- | A pure implementation of getChar and putChar.-+-- | A pure specification of getChar and putChar. module Test.IOSpec.Teletype    (    -- * The IOTeletype monad-     IOTeletype-   , Output(..)-   , runTT+     Teletype    -- * Pure getChar and putChar    , getChar    , putChar-   ) +   , putStr+   , putStrLn+   , getLine+   )    where -import qualified Data.Stream as Stream-import Prelude hiding (getChar, putChar)---- | The IOTeletype monad-data IOTeletype a = -     GetChar (Char -> IOTeletype a)-  |  PutChar Char (IOTeletype a)-  |  ReturnTeletype a--instance Functor IOTeletype where-  fmap f (GetChar tt)       = GetChar (\x -> fmap f (tt x))-  fmap f (PutChar c tt)     = PutChar c (fmap f tt)-  fmap f (ReturnTeletype x) = ReturnTeletype (f x)+import Prelude hiding (getChar, putChar, putStr, putStrLn, getLine)+import Control.Monad (forM_)+import Test.IOSpec.Types+import Test.IOSpec.VirtualMachine -instance Monad IOTeletype where-  return = ReturnTeletype-  (ReturnTeletype a)  >>= g     = g a-  (GetChar f)         >>= g     = GetChar (\c -> f c >>= g)-  (PutChar c a)       >>= g     = PutChar c (a >>= g)+-- The 'Teletype' specification.+--+-- | An expression of type 'IOSpec' 'Teletype' @a@ corresponds to an @IO@+-- computation that may print to or read from stdout and stdin+-- respectively.+--+-- There is a minor caveat here. I assume that stdin and stdout are+-- not buffered. This is not the standard behaviour in many Haskell+-- compilers.+data Teletype a =+     GetChar (Char -> a)+  |  PutChar Char a +instance Functor Teletype where+  fmap f (GetChar tt)       = GetChar (f . tt)+  fmap f (PutChar c tt)     = PutChar c (f tt) --- | Once you have constructed something of type 'IOTeletype' you--- can run the interaction. If you pass in a stream of characters--- entered at the teletype, it will produce a value of type 'Output'-runTT :: IOTeletype a -> Stream.Stream Char -> Output a-runTT (ReturnTeletype a) cs  = Finish a-runTT (GetChar f) cs         = runTT (f (Stream.head cs)) (Stream.tail cs)-runTT (PutChar c p) cs       = Print c (runTT p cs)+-- | The 'getChar' function can be used to read a character from the+-- teletype.+getChar    :: (:<:) Teletype f => IOSpec f Char+getChar    = inject (GetChar return) --- | The result of running a teletype interation is a (potentially--- infinite) list of characters, that are printed to the screen. The--- interaction can also end, and return a final value, using the--- 'Finish' constructor.-data Output a = -     Print Char (Output a) -  |  Finish a+-- | The 'getChar' function can be used to print a character to the+-- teletype.+putChar    ::  (Teletype :<: f) => Char -> IOSpec f ()+putChar c  =   inject (PutChar c (return ())) +instance Executable Teletype where+  step (GetChar f)   = do+    c <- readChar+    return (Step (f c))+  step (PutChar c a) = do+    printChar c+    return (Step a) --- | The getChar function can be used to read input from the teletype.-getChar    ::  IOTeletype Char -getChar    =   GetChar ReturnTeletype+putStr :: (Teletype :<: f) => String -> IOSpec f ()+putStr str = forM_ str putChar --- | The getChar function can be used to print to the teletype.-putChar    ::  Char -> IOTeletype () -putChar c  =   PutChar c (ReturnTeletype ())+putStrLn :: (Teletype :<: f) => String -> IOSpec f ()+putStrLn str = putStr str >> putChar '\n' +getLine :: (Teletype :<: f) => IOSpec f String+getLine = do+  c <- getChar+  if c == '\n'+    then return []+    else getLine >>= \line -> return (c : line)

@@ -0,0 +1,64 @@+{-# OPTIONS_GHC -fallow-overlapping-instances#-}+-- | This module contains the basic data types underlying the+-- 'IOSpec' library. Most of the types and classes in this module+-- are described in+-- <http://www.cs.nott.ac.uk/~wss/Publications/DataTypesALaCarte.pdf>.+module Test.IOSpec.Types+  (+  -- * The 'IOSpec' type.+    IOSpec(..)+  , foldIOSpec+  -- * Coproducts of functors+  , (:+:)(..)+  -- * Injections from one functor to another+  , (:<:)+  , inject+  ) where++-- | A value of type 'IOSpec' @f@ @a@ is either a pure value of type @a@+-- or some effect, determined by @f@. Crucially, 'IOSpec' @f@ is a+-- monad, provided @f@ is a functor.+data IOSpec f a =+    Pure a+  | Impure (f (IOSpec f a))++instance (Functor f) => Functor (IOSpec f) where+  fmap f (Pure x)   = Pure (f x)+  fmap f (Impure t) = Impure (fmap (fmap f) t)++instance (Functor f) => Monad (IOSpec f) where+  return           = Pure+  (Pure x) >>= f   = f x+  (Impure t) >>= f = Impure (fmap (>>= f) t)++-- | The fold over 'IOSpec' values.+foldIOSpec :: Functor f => (a -> b) -> (f b -> b) -> IOSpec f a -> b+foldIOSpec pure _ (Pure x)        = pure x+foldIOSpec pure impure (Impure t) = impure (fmap (foldIOSpec pure impure) t)++-- | The coproduct of functors+data (f :+: g) x = Inl (f x) | Inr (g x)++infixr 5 :+:++instance (Functor f, Functor g) => Functor (f :+: g) where+  fmap f (Inl x) = Inl (fmap f x)+  fmap f (Inr y) = Inr (fmap f y)++-- | The (:<:) class++class (Functor sub, Functor sup) => sub :<: sup where+  inj :: sub a -> sup a++instance Functor f => (:<:) f f where+  inj = id++instance (Functor f, Functor g) => (:<:) f (f :+: g) where+  inj = Inl++instance ((:<:) f g, Functor f, Functor g, Functor h)+  => (:<:) f (h :+: g) where+    inj = Inr . inj++inject :: (g :<: f) => g (IOSpec f a) -> IOSpec f a+inject = Impure . inj

@@ -0,0 +1,337 @@+-- | The virtual machine on which the specifications execute.+module Test.IOSpec.VirtualMachine+  (+  -- * The Virtual Machine+   VM+  , Data+  , Loc+  , Scheduler+  , Store+  , ThreadId+  , initialStore+  -- * Primitive operations on the VM+  , alloc+  , emptyLoc+  , freshThreadId+  , finishThread+  , lookupHeap+  , mainTid+  , printChar+  , readChar+  , updateHeap+  , updateSoup+  -- * The observable effects on the VM+  , Effect (..)+  -- * Sample schedulers+  -- $schedulerDoc+  , roundRobin+  , singleThreaded+  -- * Executing code on the VM+  , Executable(..)+  , Step(..)+  , runIOSpec+  , evalIOSpec+  , execIOSpec+  )+  where++import Control.Monad.State+import Data.Dynamic+import Data.List+import qualified Data.Stream as Stream+import Test.IOSpec.Types+import Test.QuickCheck++type Data         = Dynamic+type Loc          = Int+type Heap         = Loc -> Maybe Data++newtype ThreadId  = ThreadId Int deriving (Eq, Show)++instance Arbitrary ThreadId where+  arbitrary                = liftM ThreadId arbitrary+  coarbitrary (ThreadId k) = coarbitrary k++newtype Scheduler =+  Scheduler (Int -> (Int, Scheduler))++instance Arbitrary Scheduler where+  arbitrary   = liftM streamSched arbitrary+  coarbitrary = internalError+    "Test.IOSpec: no definition of coarbitrary for Schedulers."++instance Show Scheduler where+  show _ = "Test.IOSpec.Scheduler"+++data ThreadStatus =+     forall f b . Executable f => Running (IOSpec f b)+  |  Finished++type ThreadSoup = ThreadId -> ThreadStatus++data Store =+  Store { fresh :: Loc+        ,  heap :: Heap+        ,  nextTid :: ThreadId+        ,  blockedThreads :: [ThreadId]+        ,  finishedThreads :: [ThreadId]+        ,  scheduler :: Scheduler+        ,  threadSoup :: ThreadSoup+        }++initialStore :: Scheduler -> Store+initialStore sch =+  Store { fresh = 0+        , heap = internalError "Access of unallocated memory "+        , nextTid = ThreadId 1+        , blockedThreads = []+        , finishedThreads = []+        , scheduler = sch+        , threadSoup = internalError "Unknown thread scheduled"+        }++-- Auxiliary functions+modifyFresh :: (Loc -> Loc) -> VM ()+modifyFresh f           = do s <- get+                             put (s {fresh = f (fresh s)})++modifyHeap :: (Heap -> Heap) -> VM ()+modifyHeap f            = do s <- get+                             put (s {heap = f (heap s)})++modifyNextTid :: (ThreadId -> ThreadId) -> VM ()+modifyNextTid f         = do s <- get+                             put (s {nextTid = f (nextTid s)})++modifyBlockedThreads :: ([ThreadId] -> [ThreadId]) -> VM ()+modifyBlockedThreads f  = do s <- get+                             put (s {blockedThreads = f (blockedThreads s)})++modifyFinishedThreads :: ([ThreadId] -> [ThreadId]) -> VM ()+modifyFinishedThreads f  = do s <- get+                              put (s {finishedThreads = f (finishedThreads s)})++modifyScheduler :: (Scheduler -> Scheduler) -> VM ()+modifyScheduler f       = do s <- get+                             put (s {scheduler = f (scheduler s)})++modifyThreadSoup :: (ThreadSoup -> ThreadSoup) -> VM ()+modifyThreadSoup f = do s <- get+                        put (s {threadSoup = f (threadSoup s)})+++-- | The 'VM' monad is essentially a state monad, modifying the+-- store. Besides returning pure values, various primitive effects+-- may occur, such as printing characters or failing with an error+-- message.+type VM a = StateT Store Effect a++-- | The 'alloc' function allocate a fresh location on the heap.+alloc :: VM Loc+alloc = do  loc <- gets fresh+            modifyFresh ((+) 1)+            return loc++-- | The 'emptyLoc' function removes the data stored at a given+-- location. This corresponds, for instance, to emptying an @MVar@.+emptyLoc :: Loc -> VM ()+emptyLoc l = modifyHeap (update l Nothing)++-- | The 'freshThreadId' function returns a previously unallocated 'ThreadId'.+freshThreadId :: VM ThreadId+freshThreadId = do+  t <- gets nextTid+  modifyNextTid (\(ThreadId n) -> ThreadId (n+1))+  return t++-- | The 'finishThread' function kills the thread with the specified+-- 'ThreadId'.+finishThread :: ThreadId -> VM ()+finishThread tid = do+  modifyFinishedThreads (tid:)+  modifyThreadSoup (update tid Finished)++-- | The 'blockThread' method is used to record when a thread cannot+-- make progress.+blockThread :: ThreadId -> VM ()+blockThread tid = modifyBlockedThreads (tid:)++-- | When progress is made, the 'resetBlockedThreads' function+-- | ensures that any thread can be scheduled.+resetBlockedThreads :: VM ()+resetBlockedThreads = modifyBlockedThreads (const [])++-- | The 'lookupHeap' function returns the data stored at a given+-- heap location, if there is any.+lookupHeap :: Loc -> VM (Maybe Data)+lookupHeap l = do  h <- gets heap+                   return (h l)++-- | The 'mainTid' constant is the 'ThreadId' of the main process.+mainTid :: ThreadId+mainTid = ThreadId 0++-- | The 'readChar' and 'printChar' functions are the primitive+-- counterparts of 'getChar' and 'putChar' in the 'VM' monad.+readChar :: VM Char+readChar = StateT (\s -> (ReadChar (\c -> (Done (c,s)))))++printChar :: Char -> VM ()+printChar c = StateT (\s -> (Print c (Done ((),s))))++-- | The 'updateHeap' function overwrites a given location with+-- new data.+updateHeap :: Loc -> Data -> VM ()+updateHeap l d  = modifyHeap (update l (Just d))++-- | The 'updateSoup' function updates the process associated with a+-- given 'ThreadId'.+updateSoup :: Executable f => ThreadId -> IOSpec f a -> VM ()+updateSoup tid p = modifyThreadSoup (update tid (Running p))++update :: Eq a => a -> b -> (a -> b) -> (a -> b)+update l d h k+  | l == k       = d+  | otherwise    = h k++-- | The 'Effect' type contains all the primitive effects that are+-- observable on the virtual machine.+data Effect a =+    Done a+  | ReadChar (Char -> Effect a)+  | Print Char (Effect a)+  | Fail String++instance Functor Effect where+  fmap f (Done x) = Done (f x)+  fmap f (ReadChar t) = ReadChar (\c -> fmap f (t c))+  fmap f (Print c t) = Print c (fmap f t)+  fmap _ (Fail msg) = Fail msg++instance Monad Effect where+  return = Done+  (Done x) >>= f = f x+  (ReadChar t) >>= f = ReadChar (\c -> t c >>= f)+  (Print c t) >>= f = Print c (t >>= f)+  (Fail msg) >>= _ = Fail msg++-- $schedulerDoc+--+-- There are two example scheduling algorithms 'roundRobin' and+-- 'singleThreaded'. Note that 'Scheduler' is also an instance of+-- @Arbitrary@. Using QuickCheck to generate random schedulers is a+-- great way to maximise the number of interleavings that your tests+-- cover.++-- | The 'roundRobin' scheduler provides a simple round-robin scheduler.+roundRobin :: Scheduler+roundRobin = streamSched (Stream.unfold (\k -> (k, k+1)) 0)++-- | The 'singleThreaded' scheduler will never schedule forked+-- threads, always scheduling the main thread. Only use this+-- scheduler if your code is not concurrent.+singleThreaded :: Scheduler+singleThreaded = streamSched (Stream.repeat 0)++streamSched :: Stream.Stream Int -> Scheduler+streamSched (Stream.Cons x xs) =+  Scheduler (\k -> (x `mod` k, streamSched xs))+++-- | The 'Executable' type class captures all the different types of+-- operations that can be executed in the 'VM' monad.+class Functor f => Executable f where+  step :: f a -> VM (Step a)++data Step a = Step a | Block++instance (Executable f, Executable g) => Executable (f :+: g) where+  step (Inl x) = step x+  step (Inr y) = step y++-- The 'execVM' function essentially schedules a thread and allows+-- it to perform a single step. If the main thread is finished, it+-- returns the final result of the comptuation.+execVM :: Executable f => IOSpec f a -> VM a+execVM main = do+  (tid,t) <- schedule main+  case t of+    (Main (Pure x)) -> resetBlockedThreads >> return x+    (Main (Impure p)) -> do x <- step p+                            case x of+                              Step y -> resetBlockedThreads >> execVM y+                              Block -> blockThread mainTid >> execVM main+    (Aux (Pure _)) -> do finishThread tid+                         execVM main+    (Aux (Impure p)) -> do x <- step p+                           case x of+                             Step y -> resetBlockedThreads >>+                                       updateSoup tid y >>+                                       execVM main+                             Block -> blockThread tid >>+                                      execVM main+-- A Process is the result of a call to the scheduler.+data Process a =+     forall f . Executable f => Main (IOSpec f a)+  |  forall f b . Executable f => Aux (IOSpec f b)++-- Gets the ThreadId of the next thread to schedule.+getNextThreadId :: VM ThreadId+getNextThreadId = do+  Scheduler sch <- gets scheduler+  (ThreadId total) <- gets nextTid+  let allTids = [ThreadId i | i <- [0 .. total - 1]]+  blockedTids <- gets blockedThreads+  finishedTids <- gets finishedThreads+  let activeThreads = allTids \\ (blockedTids `union` finishedTids)+  let (i,s) = sch (length activeThreads)+  modifyScheduler (const s)+  return (activeThreads !! i)++-- The 'schedule' function tries to schedule an active thread,+-- returning the scheduled thread's ThreadId and the process+-- associated with that id.+schedule :: Executable f => IOSpec f a -> VM (ThreadId, Process a)+schedule main = do  tid <- getNextThreadId+                    if tid == mainTid+                      then return (mainTid, Main main)+                      else do+                        tsoup <- gets threadSoup+                        case tsoup tid of+                          Finished ->  internalError+                            "Scheduled finished thread."+                          Running p -> return (tid, Aux p)++-- | The 'runIOSpec' function is the heart of this library.  Given+-- the scheduling algorithm you want to use, it will run a value of+-- type 'IOSpec' @f@ @a@, returning the sequence of observable effects+-- together with the final store.+runIOSpec :: Executable f => IOSpec f a -> Scheduler -> Effect (a, Store)+runIOSpec io sched = runStateT+                       (execVM io)+                       (initialStore sched)++-- | The 'execIOSpec' returns the final 'Store' after executing a+-- computation.+--+-- /Beware/: this function assumes that your computation will+-- succeed, without any other visible 'Effect'. If your computation+-- reads a character from the teletype, for instance, it will return+-- an error.+execIOSpec :: Executable f => IOSpec f a -> Scheduler -> Store+execIOSpec io sched =+  case runIOSpec io sched of+    Done (_,s) -> s+    _ -> error $ "Failed application of Test.IOSpec.execIOSpec.\n" +++                 "Probable cause: your function uses functions such as " +++                 "putChar and getChar. Check the preconditions for calling " +++                 "this function in the IOSpec documentation."++-- | The 'evalIOSpec' function returns the effects a computation+-- yields, but discards the final state of the virtual machine.+evalIOSpec :: Executable f => IOSpec f a -> Scheduler -> Effect a+evalIOSpec io sched = fmap fst (runIOSpec io sched)++internalError :: String -> a+internalError msg = error ("IOSpec.VirtualMachine: " ++ msg)