{-# LANGUAGE DataKinds          #-}
{-# LANGUAGE DeriveAnyClass     #-}
{-# LANGUAGE DeriveGeneric      #-}
{-# LANGUAGE FlexibleInstances  #-}
{-# LANGUAGE GADTs              #-}
{-# LANGUAGE KindSignatures     #-}
{-# LANGUAGE LambdaCase         #-}
{-# LANGUAGE NamedFieldPuns     #-}
{-# LANGUAGE PolyKinds          #-}
{-# LANGUAGE RankNTypes         #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell    #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  CircularBuffer
-- Copyright   :  (C) 2017, Xia Li-yao
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Xia Li-yao
-- Stability   :  provisional
-- Portability :  non-portable (GHC extensions)
--
-- This module contains a specification of a circular buffer. Adapted
-- from John Hughes' /Experiences with QuickCheck: Testing the hard
-- stuff and staying sane/.
--
------------------------------------------------------------------------

module CircularBuffer
  ( unpropNoSizeCheck
  , unpropFullIsEmpty
  , unpropBadRem
  , unpropStillBadRem
  , prop_circularBuffer
  )
  where

import           Control.Applicative
                   (liftA2)
import           Control.Monad
                   (guard)
import           Data.Function
                   (on)
import           Data.Functor.Classes
                   (Eq1)
import           Data.IORef
                   (IORef, newIORef, readIORef, writeIORef)
import           Data.Kind
                   (Type)
import           Data.Maybe
                   (isJust)
import           Data.TreeDiff
                   (ToExpr)
import           Data.Vector.Unboxed.Mutable
                   (IOVector)
import qualified Data.Vector.Unboxed.Mutable   as V
import           GHC.Generics
                   (Generic, Generic1)
import           Prelude                       hiding
                   (elem)
import qualified Prelude                       as P
import           Test.QuickCheck
                   (Gen, Positive(..), Property, arbitrary, elements,
                   frequency, shrink, (===))
import           Test.QuickCheck.Monadic
                   (monadicIO)

import           Test.StateMachine
import qualified Test.StateMachine.Types.Rank2 as Rank2

------------------------------------------------------------------------

-- | Sets of bugs in the implementation and specification.
type Bugs = [Bug]

-- | Possible bugs.
--
-- See 'unpropNoSizeCheck', 'unpropFullIsEmpty', 'unpropBadRem',
-- and 'unpropStillBadRem'.
data Bug = NoSizeCheck | FullIsEmpty | BadRem | StillBadRem
  deriving (Eq, Enum)

-- | Switch to disable or enable testing of the 'lenBuffer' function.
data Version = NoLen | YesLen
  deriving Eq

------------------------------------------------------------------------

-- | An efficient mutable circular buffer.
data Buffer = Buffer
  { top :: IORef Int     -- ^ Index to the top: where to 'Put' the next element
  , bot :: IORef Int     -- ^ Index to the bottom: where to 'Get' the next element
  , arr :: IOVector Int  -- ^ Array of elements of fixed capacity
  }

-- | Different buffers are assumed to have disjoint memories,
-- so we can use 'V.overlaps' to check equality.
instance Eq Buffer where
  (==) =
    ((==) `on` top) `also`
    ((==) `on` bot) `also`
    (V.overlaps `on` arr)
    where
      also = (liftA2 . liftA2) (&&)

-- | See 'New'.
newBuffer :: Bugs -> Int -> IO Buffer
newBuffer bugs n = Buffer
  <$> newIORef 0
  <*> newIORef 0
  <*> V.new (if FullIsEmpty `P.elem` bugs then n else n + 1)

-- | See 'Put'.
putBuffer :: Int -> Buffer -> IO ()
putBuffer x Buffer{top, arr} = do
  i <- readIORef top
  V.write arr i x
  writeIORef top $! (i + 1) `mod` V.length arr

-- | See 'Get'.
getBuffer :: Buffer -> IO Int
getBuffer Buffer{bot, arr} = do
  j <- readIORef bot
  y <- V.read arr j
  writeIORef bot $! (j + 1) `mod` V.length arr
  return y

-- | See 'Len'.
lenBuffer :: Bugs -> Buffer -> IO Int
lenBuffer bugs Buffer{top, bot, arr} = do
  i <- readIORef top
  j <- readIORef bot
  return $
    if BadRem `P.elem` bugs then
      (i - j) `rem` V.length arr
    else if StillBadRem `P.elem` bugs then
      abs ((i - j) `rem` V.length arr)
    else
      (i - j) `mod` V.length arr

------------------------------------------------------------------------

-- | Buffer actions.
data Action (r :: Type -> Type)
    -- | Create a new buffer of bounded capacity.
  = New Int

    -- | Put an element at the top of the buffer.
  | Put Int (Reference (Opaque Buffer) r)

    -- | Get an element out of the bottom of the buffer.
  | Get (Reference (Opaque Buffer) r)

    -- | Get the number of elements in the buffer.
  | Len (Reference (Opaque Buffer) r)
  deriving (Show, Generic1, Rank2.Functor, Rank2.Foldable, Rank2.Traversable, CommandNames)

data Response (r :: Type -> Type)
  = NewR (Reference (Opaque Buffer) r)
  | PutR
  | GetR Int
  | LenR Int
  deriving (Show, Generic1, Rank2.Foldable)

------------------------------------------------------------------------

-- | A simple, persistent, inefficient buffer.
--
-- The top of the buffer is the head of the list, the bottom is the last
-- element.
data SpecBuffer = SpecBuffer
  { specSize     :: Int    -- ^ Maximum number of elements
  , specContents :: [Int]  -- ^ Contents of the buffer
  }
  deriving (Generic, Show, ToExpr)

emptySpecBuffer :: Int -> SpecBuffer
emptySpecBuffer n = SpecBuffer n []

insertSpecBuffer :: Int -> SpecBuffer -> SpecBuffer
insertSpecBuffer x (SpecBuffer n xs) = SpecBuffer n (x : xs)

removeSpecBuffer :: SpecBuffer -> (Int, SpecBuffer)
removeSpecBuffer (SpecBuffer n xs) = (last xs, SpecBuffer n (init xs))

------------------------------------------------------------------------

-- | The model is a map from buffer references to their values.
newtype Model r = Model [(Reference (Opaque Buffer) r, SpecBuffer)]
  deriving (Generic, Show)

deriving instance ToExpr (Model Concrete)

-- | Initially, there are no references to buffers.
initModel :: Model v
initModel = Model []

precondition :: Bugs -> Model Symbolic -> Action Symbolic -> Logic
precondition _    _         (New n) = n .> 0
precondition bugs (Model m) (Put _ buffer) | NoSizeCheck `P.elem` bugs =
  buffer `elem` map fst m
precondition _    (Model m) (Put _ buffer) = Boolean $ isJust $ do
  specBuffer <- lookup buffer m
  guard $ length (specContents specBuffer) < specSize specBuffer
precondition _    (Model m) (Get buffer) = Boolean $ isJust $ do
  specBuffer <- lookup buffer m
  guard $ not (null (specContents specBuffer))
precondition _    (Model m) (Len buffer) = buffer `elem` map fst m

transition :: Eq1 r => Model r -> Action r -> Response r -> Model r
transition (Model m) (New n)        (NewR ref) =
  Model ((ref, emptySpecBuffer n) : m)
transition (Model m) (Put x buffer) _          =
  case lookup buffer m of
    Just old -> Model (update buffer (insertSpecBuffer x old) m)
    Nothing  -> error "transition: put"
transition (Model m) (Get buffer) _ =
  case lookup buffer m of
    Just old ->
      let (_, new) = removeSpecBuffer old in
      Model (update buffer new m)
    Nothing  -> error "transition: get"
transition m    _ _ = m

update :: Eq a => a -> b -> [(a, b)] -> [(a, b)]
update ref i m = (ref, i) : filter ((/= ref) . fst) m

postcondition :: Model Concrete -> Action Concrete -> Response Concrete -> Logic
postcondition _         (New _)      _        = Top
postcondition _         (Put _ _)    _        = Top
postcondition (Model m) (Get buffer) (GetR y) = case lookup buffer m of
  Nothing         -> Bot
  Just specBuffer ->
    let (y', _) = removeSpecBuffer specBuffer
    in y .== y'
postcondition (Model m) (Len buffer) (LenR k) = case lookup buffer m of
  Nothing         -> Bot
  Just specBuffer -> k .== length (specContents specBuffer)
postcondition _         _            _        = error "postcondition"

------------------------------------------------------------------------

genNew :: Gen (Action Symbolic)
genNew = do
  Positive n <- arbitrary
  return (New n)

generator :: Version -> Model Symbolic -> Maybe (Gen (Action Symbolic))
generator _       (Model m) | null m = Just $ genNew
generator version (Model m)          = Just $ frequency $
  [ (1, genNew)
  , (4, Put <$> arbitrary <*> (fst <$> elements m))
  , (4, Get <$> (fst <$> elements m))
  ] ++
  [ (4, Len <$> (fst <$> elements m)) | version == YesLen ]

shrinker :: Model Symbolic -> Action Symbolic -> [Action Symbolic]
shrinker _ (New n)        = [ New n'        | n' <- shrink n ]
shrinker _ (Put x buffer) = [ Put x' buffer | x' <- shrink x ]
shrinker _ _              = []

------------------------------------------------------------------------

semantics :: Bugs -> Action Concrete -> IO (Response Concrete)
semantics bugs (New n)        = NewR . reference . Opaque <$> newBuffer bugs n
semantics _    (Put x buffer) = PutR <$  putBuffer x (opaque buffer)
semantics _    (Get buffer)   = GetR <$> getBuffer (opaque buffer)
semantics bugs (Len buffer)   = LenR <$> lenBuffer bugs (opaque buffer)

mock :: Model Symbolic -> Action Symbolic -> GenSym (Response Symbolic)
mock _         (New _)      = NewR <$> genSym
mock _         (Put _ _)    = pure PutR
mock (Model m) (Get buffer) = case lookup buffer m of
  Nothing   -> error "mock: get"
  Just spec -> case specContents spec of
    []      -> error "mock: get 2"
    (i : _) -> pure (GetR i)
mock (Model m) (Len buffer) = case lookup buffer m of
  Nothing   -> error "mock: len"
  Just spec -> pure (LenR (specSize spec))

------------------------------------------------------------------------

sm :: Version -> Bugs -> StateMachine Model Action IO Response
sm version bugs = StateMachine
  initModel transition (precondition bugs) postcondition
  Nothing (generator version) Nothing shrinker (semantics bugs) mock

-- | Property parameterized by spec version and bugs.
prepropcircularBuffer :: Version -> Bugs -> Property
prepropcircularBuffer version bugs =
  forAllCommands sm' Nothing $ \cmds -> monadicIO $ do
    (hist, _, res) <- runCommands sm' cmds
    prettyCommands sm' hist $
      checkCommandNames cmds (res === Ok)
  where
    sm' = sm version bugs

-- Adapted from John Hughes'
-- /Experiences with QuickCheck: Testing the hard stuff and staying sane/,

-- | The first bug. 'NoSizeCheck'
--
-- Putting more elements than the capacity of the buffer (set when it is
-- constructed using 'New') causes a buffer overflow: new elements overwrite
-- older ones that haven't been removed yet.
-- A minimal counterexample that reveals the bug is simply:
--
-- > buffer <- newBuffer 1
-- > putBuffer 0 buffer
-- > putBuffer 1 buffer
-- > getBuffer buffer
-- >
-- > -- Expected: 0
-- > -- Actual:   1
--
-- The mistake is in the specification: it models an unbounded buffer.
-- For a bounded buffer, that sequence of calls makes no sense.
-- The fix is to add a precondition to forbid 'Put' when the buffer is full.

unpropNoSizeCheck :: Property
unpropNoSizeCheck = prepropcircularBuffer NoLen  [NoSizeCheck ..]

-- | The second bug. 'FullIsEmpty'
--
-- The top and bottom pointers wrap around when they reach the end of the
-- array. We have that @top == bottom@ whenever the buffer is either empty or
-- full.
-- In other words, a full buffer is undistinguishable from an empty one.
-- A minimal counterexample:
--
-- > buffer <- newBuffer 1
-- > putBuffer 0 buffer
-- > lenBuffer buffer
-- >
-- > -- Expected: 1
-- > -- Actual:   0
--
-- In this implementation, the length of a buffer is given by the remainder of
-- a division by its capacity. When the capacity is one, that remainder is
-- always 0.
-- The fix is to allocate one more cell when we allocate a 'New' buffer.
--
-- In a way, the bug is still there. But to observe it, one has to
-- 'Put' one more element than the buffer capacity. Since this violates the
-- specification, it's the user's fault!

unpropFullIsEmpty :: Property
unpropFullIsEmpty = prepropcircularBuffer YesLen [FullIsEmpty ..]

-- | The third bug. 'BadRem'
--
-- The length of a buffer uses 'rem', which is the remainder of a
-- division truncated towards zero (the standard division in many languages,
-- such as C, but not Haskell). When the dividend @(top - bottom)@ is negative,
-- the remainder is non-positive.
-- A minimal counterexample:
--
-- > buffer <- newBuffer 1
-- > putBuffer 0 buffer
-- > getBuffer buffer
-- > putBuffer 0 buffer
-- > lenBuffer buffer
-- >
-- > -- Expected:  1
-- > -- Actual:   -1
--
-- The fix is to ensure the remainder is non-negative...

unpropBadRem :: Property
unpropBadRem = prepropcircularBuffer YesLen [BadRem ..]

-- | The fourth bug. 'StillBadRem'
--
-- ... One way to obtain a non-negative remainder is to make the dividend
-- non-negative. /Clearly/ we should divide by the absolute value instead.
-- QuickCheck provides a minimal counterexample to that "obvious" fix:
--
-- > buffer <- newBuffer 2
-- > putBuffer 0 buffer
-- > getBuffer buffer
-- > putBuffer 0 buffer
-- > putBuffer 0 buffer
-- > lenBuffer len
-- >
-- > -- Expected: 2
-- > -- Actual:   1
--
-- As an aside, for the first time, the buffer /needs/ to be of capacity two.
-- That non-fix fixed buffers of capacity one!
--
-- The actual fix is to use 'mod',
-- which performs division rounding towards -∞.

unpropStillBadRem :: Property
unpropStillBadRem = prepropcircularBuffer YesLen [StillBadRem]

-- | And now tests pass.

prop_circularBuffer :: Property
prop_circularBuffer = prepropcircularBuffer YesLen []