content: {-# LANGUAGE DerivingStrategies #-}
  
  module Part03.QueueTest (module Part03.QueueTest) where
  
  import Control.Monad
  import Test.QuickCheck
  import Test.QuickCheck.Monadic
  
  import Part03.Queue
  
  ------------------------------------------------------------------------
  
  -- The model of our queue will use a simple immutable linked list rather than
  -- the complicated mutable array.
  
  data Model a = Model
    { mCapacity :: Int
    , mQueue    :: [a]
    }
    deriving stock Show
  
  newModel :: Int -> Model a
  newModel cap = Model cap []
  
  data Command a
    = Size
    | Clear
    | IsEmpty
    | Enqueue a
    | Dequeue
    deriving stock Show
  
  prettyCommand :: Command a -> String
  prettyCommand Size       = "Size"
  prettyCommand Clear      = "Clear"
  prettyCommand IsEmpty    = "IsEmpty"
  prettyCommand Enqueue {} = "Enqueue"
  prettyCommand Dequeue    = "Dequeue"
  
  data Response a
    = Int Int
    | Unit ()
    | Maybe (Maybe a)
    | Bool Bool
    deriving stock (Show, Eq)
  
  -- Enqueuing merely appends to the back of the list.
  
  fakeEnqueue :: a -> Model a -> (Model a, Bool)
  fakeEnqueue x m
    | length (mQueue m) >= mCapacity m = (m, False)
    | otherwise = (m { mQueue = mQueue m ++ [x]}, True)
  
  -- While dequeuing merely returns the head of the list.
  
  fakeDequeue :: Model a -> (Model a, Maybe a)
  fakeDequeue m = case mQueue m of
    []       -> (m, Nothing)
    (x : xs) -> (m { mQueue = xs }, Just x)
  
  step :: Command a -> Model a -> (Model a, Response a)
  step Size        m = (m, Int (length (mQueue m)))
  step Clear       m = (m { mQueue = [] }, Unit ())
  step IsEmpty     m = (m, Bool (null (mQueue m)))
  step (Enqueue x) m = Bool  <$> fakeEnqueue x m
  step Dequeue     m = Maybe <$> fakeDequeue m
  
  exec :: Command a -> Queue a -> IO (Response a)
  exec Size             q = Int   <$> size q
  exec Clear            q = Unit  <$> clear q
  exec IsEmpty          q = Bool  <$> isEmpty q
  exec (Enqueue x)      q = Bool  <$> enqueue q x
  exec Dequeue          q = Maybe <$> dequeue q
  
  genCommand :: Arbitrary a => Int -> Int -> Gen (Command a)
  genCommand _cap _sz = frequency
    [ (3, pure Size)
    , (0, pure Clear) -- NOTE: If this happens too often, it causing enqueue to
                      -- rarely write to a full queue.
    , (2, pure IsEmpty)
    , (5, Enqueue <$> arbitrary)
    , (2, pure Dequeue)
    ]
  
  genCommands :: Arbitrary a => Int -> Int -> Gen [Command a]
  genCommands cap sz0 = sized (go sz0)
    where
      go _sz 0 = return []
      go sz  n = do
        cmd <- genCommand cap sz
        let sz' = case cmd of
                    Size       -> sz
                    Clear      -> 0
                    IsEmpty    -> sz
                    Enqueue {} -> sz + 1
                    Dequeue    -> sz - 1
        cmds <- go sz' (n - 1)
        return (cmd : cmds)
  
  newtype Capacity = Capacity Int
    deriving stock Show
  
  instance Arbitrary Capacity where
    arbitrary = Capacity <$> choose (0, 5)
  
  -- The tests that ensure that the model is faithful to the real queue
  -- implementation also doubles as contract tests once we turn or model into a
  -- fake.
  
  prop_contractTests :: Capacity -> Property
  prop_contractTests (Capacity cap) =
    forAllShrink (genCommands cap 0) (shrinkList (const [])) $ \cmds -> monadicIO $ do
      let m = newModel cap
      q <- run (newQueue cap)
      monitor (tabulate "Commands" (map prettyCommand cmds))
      (result, hist) <- go cmds m q []
      mapM_ (monitor . classify') (zip cmds hist)
      return result
      where
        go :: [Command Int] -> Model Int -> Queue Int -> [Response Int] -> PropertyM IO (Bool, [Response Int])
        go []          _m _q hist = return (True, reverse hist)
        go (cmd : cmds) m  q hist = do
          let (m', resp) = step cmd m
          resp' <- run (exec cmd q)
          unless (resp == resp') $
            monitor (counterexample (show resp ++ " /= " ++ show resp'))
          go cmds m' q (resp : hist)
  
        classify' :: (Command a, Response a) -> Property -> Property
        classify' (Enqueue {},     Bool b) = classify b "enqueue successful"
        classify' (_, _)                   = id
  