Prototype.hs

{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DeriveFunctor         #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE TemplateHaskell       #-}

module Prototype where

import           Control.Monad
import           Control.Monad.Free
import           Control.Monad.Free.TH
import           Control.Monad.State
import           Control.Monad.Writer
import           Test.QuickCheck
import           Test.QuickCheck.Gen.Unsafe
import           Test.QuickCheck.Monadic
import           Test.QuickCheck.Property

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

data StackF x
  = Push Int x
  | Pop (Int -> x)
  deriving Functor

makeFree ''StackF

type Stack = Free StackF

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

data TraceStep
  = Pushed
  | Popped Int
  deriving (Eq, Show)

type Trace = [TraceStep]

showT :: Show a => Stack a -> Trace -> String
showT (Pure x)           []              = "return " ++ show x
showT (Free (Push x ih)) (Pushed   : ts) =
  "push " ++ show x ++  "; " ++ showT ih    ts
showT (Free (Pop k))     (Popped i : ts) =
  "pop [" ++ show i ++ "]; " ++ showT (k i) ts

showT _ [] = "..."
showT _ _  = error "Impossible."

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

runS :: Stack a -> ((a, Trace), [Int])
runS = flip runState [] . runWriterT . iterM alg

type OurMonad m = (MonadState [Int] m, MonadWriter Trace m)

alg :: OurMonad m => StackF (m a) -> m a
alg (Push x ih) = do
  modify (x:)
  tell [Pushed]
  ih
alg (Pop k)     = do
  s <- get
  -- Break the implementation.
  -- put (tail s)
  let x = head s
  tell [Popped x]
  k x

ex0 :: Bool
ex0 = runS (push 1 >> push 2 >> pop) == ((2, [Pushed, Pushed, Popped 2]), [1])

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

type Model = [Int]

initModel :: Model
initModel = []

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

push_pre :: Model -> Bool
push_pre = const True

push_next :: Model -> Int -> () -> Model
push_next m x () = x : m

push_post :: Model -> Int -> () -> Bool
push_post m x () = x == head (push_next m x ())


pop_pre :: Model -> Bool
pop_pre = not . null

pop_next :: Model -> () -> Int -> Model
pop_next m () _ = tail m

pop_post :: Model -> () -> Int -> Bool
pop_post m () r = r == head m && tail m == pop_next m () r

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

gen1 :: Model -> Gen (Stack Model)
gen1 m = frequency
  [ (if push_pre m then 1 else 0, genPush)
  , (if pop_pre  m then 1 else 0, genPop )
  ]
  where
  genPush :: Gen (Stack Model)
  genPush = do
    x <- arbitrary
    return $ fmap (push_next m x) $ push x

  genPop :: Gen (Stack Model)
  genPop = return $ fmap (pop_next m ()) $ pop

gen :: Gen (Stack ())
gen = sized $ \n -> go n initModel
  where
  go :: Int -> Model -> Gen (Stack ())
  go 0 _ = return $ return ()
  go i m = do
    cmd1 <- gen1 m
    fmap join $ promote $ fmap (go (i - 1)) cmd1

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

data StackNTrace = Stack () :- Trace

instance Show StackNTrace where
  show (s :- t) = showT s t

instance Arbitrary StackNTrace where
  arbitrary = undefined
  shrink (s :- t) = shrinkT s t []

shrinkT :: Stack () -> Trace -> Model -> [StackNTrace]
shrinkT (Pure _)          _                   _ = []
shrinkT (Free (Push x s))    (Pushed : ts')   m =
  [ return () :- [] ]
  ++ (if preCondsStillHold m s ts'
     then [ s :- correctTrace m s ts' ]
     else [])
  ++ [ (Free (Push x s')) :- (Pushed : ts'')
     | s' :- ts'' <- shrinkT s ts' (push_next m x ())
     ]
shrinkT (Free (Pop k))       (Popped i : ts') m =
  [ return () :- [] ]
  ++ (if preCondsStillHold m (k i) ts'
      then [ k i :- correctTrace m (k i) ts' ]
      else [])
  ++ [ Free (Pop (const s')) :- (Popped i : ts'')
     | s' :- ts'' <- shrinkT (k i) ts' (pop_next m () i)
     ]                                                   -- Hmm? const s'...
shrinkT _ [] _ = []
shrinkT _ _ _  = error "Impossible."

preCondsStillHold :: Model -> Stack () -> Trace -> Bool
preCondsStillHold _ (Pure _)          _               = True
preCondsStillHold m (Free (Push x s)) (Pushed : ts)   =
  push_pre m && preCondsStillHold (push_next m x ()) s ts
preCondsStillHold m (Free (Pop k))    (Popped i : ts) =
  pop_pre m  && preCondsStillHold (pop_next m () i) (k i) ts
preCondsStillHold _ _                 []              = True
preCondsStillHold _ _                 _               = error "Impossible."

correctTrace :: Model -> Stack () -> Trace -> Trace
correctTrace _ (Pure _)          []              = []
correctTrace m (Free (Push x s)) (Pushed : ts)   =
  Pushed : correctTrace (push_next m x ()) s ts
correctTrace m (Free (Pop k))    (Popped i : ts) =
  Popped (head m) : correctTrace (pop_next m () i) (k i) ts   -- head here isn't generic...
correctTrace _ _                 _               = error "Impossible."

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

forallStack :: (Stack () -> PropertyM Stack ()) -> Property
forallStack p = MkProperty $ do
  stack <- scale (+ 100) gen
  unProperty $ MkProperty (fmap (MkProp . joinRose . fmap unProp) (props stack))
  where
  props :: Stack () -> Gen (Rose Prop)
  props stack = do
    (prop, trace) <- proper stack
    prop' <- unProperty prop
    roses <- mapM (\(s' :- _) -> props s') $ shrinkT stack trace initModel
    return $ MkRose prop' roses

  proper :: Stack () -> Gen (Property, Trace)
  proper stack = fmap helper $ monadic' $ p stack
    where
    helper :: Stack Property -> (Property, Trace)
    helper s = let ((prop, trace), _) = runS s
               in (counterexample (showT stack trace) prop, trace)

prop_safety :: Property
prop_safety = forallStack (go initModel)
  where
  go :: Model -> Stack () -> PropertyM Stack ()
  go _ (Pure ())          = return ()
  go m (Free (Push x ih)) = do
    r <- run $ push x
    assert $ push_post m x r
    go (push_next m x r) ih
  go m (Free (Pop k))     = do
    r <- run pop
    assert $ pop_post m () r
    go (pop_next m () r) $ k r

test :: IO ()
test = verboseCheck prop_safety

Sample output:

Assertion failed (after 1 test and 91 shrinks):    
push 81; push -44; pop [-44]; pop [-44]; ...

Assertion failed (after 1 test and 96 shrinks):    
push -28; push -91; pop [-91]; pop [-91]; return ()

Assertion failed (after 1 test and 88 shrinks):    
push 5; push -24; pop [-24]; pop [-24]; ...