wweeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeee

StateAPI.hs

{-# LANGUAGE RankNTypes #-}
module StateAPI where

import           Control.Lens           (Lens', cons, lens, (%~))
import           Control.Monad.IO.Class (MonadIO)

import           Data.Function          ((&))
import           Data.Typeable          (Typeable)

import           Hedgehog

data CmdBuilder g m model inp out = CmdBuilder
  (MonadGen g => model Symbolic -> Maybe (g (inp Symbolic)))
  (inp Concrete -> m out)
  [Callback inp out model]

cmdgen :: (MonadGen g, MonadTest m) => Lens' (CmdBuilder g m model inp out) (model Symbolic -> Maybe (g (inp Symbolic)))
cmdgen = lens (\(CmdBuilder g _ _) -> g) (\(CmdBuilder _ e cbs) g -> CmdBuilder g e cbs)

cmdexec :: (MonadGen g, MonadTest m) => Lens' (CmdBuilder g m model inp out) (inp Concrete -> m out)
cmdexec = lens (\(CmdBuilder _ e _) -> e) (\(CmdBuilder g _ cbs) e -> CmdBuilder g e cbs)

callbacks :: (MonadGen g, MonadTest m) => Lens' (CmdBuilder g m model inp out) [Callback inp out model]
callbacks = lens (\(CmdBuilder _ _ cbs) -> cbs) (\(CmdBuilder g e _) cbs -> CmdBuilder g e cbs)

emptyCmd
  :: ( MonadGen g
     , MonadTest m
     )
  => (model Symbolic -> Maybe (g (inp Symbolic)))
  -> (inp Concrete -> m out)
  -> CmdBuilder g m model inp out
emptyCmd g e = CmdBuilder g e []

require
  :: ( MonadGen g
     , MonadTest m
     )
  => CmdBuilder g m model inp out
  -> (model Symbolic -> inp Symbolic -> Bool)
  -> CmdBuilder g m model inp out
require cmd cb = cmd & callbacks %~ cons (Require cb)

ensure
  :: ( MonadGen g
     , MonadTest m
     )
  => CmdBuilder g m model inp out
  -> (model Concrete -> model Concrete -> inp Concrete -> out -> Test ())
  -> CmdBuilder g m model inp out
ensure cmd cb = cmd & callbacks %~ cons (Ensure cb)

update
  :: ( MonadGen g
     , MonadTest m
     )
  => CmdBuilder g m model inp out
  -> (forall v. Ord1 v => model v -> inp v -> Var out v -> model v)
  -> CmdBuilder g m model inp out
update cmd cb = cmd & callbacks %~ cons (Update cb)

flipdate
  :: ( MonadGen g
     , MonadTest m
     )
  => (forall v. Ord1 v => model v -> inp v -> Var out v -> model v)
  -> CmdBuilder g m model inp out
  -> CmdBuilder g m model inp out
flipdate cb cmd = cmd & callbacks %~ cons (Update cb)

build
  :: ( MonadGen g
     , MonadTest m
     , HTraversable inp
     , Show (inp Symbolic)
     , Typeable out
     )
  => CmdBuilder g m model inp out
  -> Command g m model
build (CmdBuilder g e cbs) = Command g e cbs

buildCmd
  :: ( HTraversable inp
     , Show (inp Symbolic)
     , Typeable out
     , MonadGen g
     , MonadTest m
     )
  => (model Symbolic -> Maybe (g (inp Symbolic)))
  -> (inp Concrete -> m out)
  -> (CmdBuilder g m model inp out -> CmdBuilder g m model inp out)
  -> Command g m model
buildCmd g e f = build $ f (emptyCmd g e) 

alwaysGen :: MonadGen g => a Symbolic -> m Symbolic -> Maybe (g (a Symbolic))
alwaysGen = const . pure . pure

overwrite :: Ord1 v => model v -> model v -> inp v -> Var out v -> model v
overwrite newM _ _ _ = newM

enOut :: (out -> Test ()) -> model Concrete -> model Concrete -> inp Concrete -> out -> Test ()
enOut t _ _ _ = t 

enInOut :: (inp Concrete -> out -> Test ()) -> model Concrete -> model Concrete -> inp Concrete -> out -> Test ()
enInOut t _ _ = t

execIO :: (MonadTest m, MonadIO m) => (a -> IO b) -> a -> m b
execIO f = evalIO . f

execIO_ :: (MonadTest m, MonadIO m) => IO a -> b -> m a
execIO_ f = const $ evalIO f