-- | Monadic interface for writing /Dynamic Logic/ properties.
--
-- This interface offers a much nicer experience than manipulating the
-- expressions it is implemented on top of, especially as it improves
-- readability. It's still possible to express properties as pure
-- expressions using the `Test.QuickCheck.DynamicLogic.Core` module
-- and it might make sense depending on the context and the kind of
-- properties one wants to express.
module Test.QuickCheck.DynamicLogic (
  DL,
  action,
  anyAction,
  anyActions,
  anyActions_,
  stopping,
  weight,
  getSize,
  getModelStateDL,
  assert,
  assertModel,
  monitorDL,
  forAllQ,
  forAllDL,
  forAllDL_,
  forAllMappedDL,
  forAllMappedDL_,
  forAllUniqueDL,
  withDLTest,
  DL.DynLogic,
  DL.DynLogicModel (..),
  DL.DynLogicTest (..),
  DL.TestStep (..),
  module Test.QuickCheck.DynamicLogic.Quantify,
) where

import Control.Applicative
import Control.Monad
import Data.Typeable
import Test.QuickCheck hiding (getSize)
import Test.QuickCheck.DynamicLogic.Core qualified as DL
import Test.QuickCheck.DynamicLogic.Quantify
import Test.QuickCheck.StateModel

-- | The `DL` monad provides a nicer interface to dynamic logic formulae than the plain API.
--   It's a continuation monad producing a `DL.DynFormula` formula, with a state component threaded
--   through.
newtype DL s a = DL {forall s a. DL s a -> s -> (a -> s -> DynFormula s) -> DynFormula s
unDL :: s -> (a -> s -> DL.DynFormula s) -> DL.DynFormula s}
  deriving (forall a b. a -> DL s b -> DL s a
forall a b. (a -> b) -> DL s a -> DL s b
forall s a b. a -> DL s b -> DL s a
forall s a b. (a -> b) -> DL s a -> DL s b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> DL s b -> DL s a
$c<$ :: forall s a b. a -> DL s b -> DL s a
fmap :: forall a b. (a -> b) -> DL s a -> DL s b
$cfmap :: forall s a b. (a -> b) -> DL s a -> DL s b
Functor)

instance Applicative (DL s) where
  pure :: forall a. a -> DL s a
pure a
x = forall s a.
(s -> (a -> s -> DynFormula s) -> DynFormula s) -> DL s a
DL forall a b. (a -> b) -> a -> b
$ \s
s a -> s -> DynFormula s
k -> a -> s -> DynFormula s
k a
x s
s
  <*> :: forall a b. DL s (a -> b) -> DL s a -> DL s b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Alternative (DL s) where
  empty :: forall a. DL s a
empty = forall s a.
(s -> (a -> s -> DynFormula s) -> DynFormula s) -> DL s a
DL forall a b. (a -> b) -> a -> b
$ \s
_ a -> s -> DynFormula s
_ -> forall s. DynFormula s
DL.ignore
  DL s -> (a -> s -> DynFormula s) -> DynFormula s
h <|> :: forall a. DL s a -> DL s a -> DL s a
<|> DL s -> (a -> s -> DynFormula s) -> DynFormula s
j = forall s a.
(s -> (a -> s -> DynFormula s) -> DynFormula s) -> DL s a
DL forall a b. (a -> b) -> a -> b
$ \s
s a -> s -> DynFormula s
k -> s -> (a -> s -> DynFormula s) -> DynFormula s
h s
s a -> s -> DynFormula s
k forall s. DynFormula s -> DynFormula s -> DynFormula s
DL.||| s -> (a -> s -> DynFormula s) -> DynFormula s
j s
s a -> s -> DynFormula s
k

instance Monad (DL s) where
  return :: forall a. a -> DL s a
return = forall (f :: * -> *) a. Applicative f => a -> f a
pure
  DL s -> (a -> s -> DynFormula s) -> DynFormula s
h >>= :: forall a b. DL s a -> (a -> DL s b) -> DL s b
>>= a -> DL s b
j = forall s a.
(s -> (a -> s -> DynFormula s) -> DynFormula s) -> DL s a
DL forall a b. (a -> b) -> a -> b
$ \s
s b -> s -> DynFormula s
k -> s -> (a -> s -> DynFormula s) -> DynFormula s
h s
s forall a b. (a -> b) -> a -> b
$ \a
x s
s1 -> forall s a. DL s a -> s -> (a -> s -> DynFormula s) -> DynFormula s
unDL (a -> DL s b
j a
x) s
s1 b -> s -> DynFormula s
k

instance MonadFail (DL s) where
  fail :: forall a. String -> DL s a
fail = forall s a. String -> DL s a
errorDL

action :: (Typeable a, Eq (Action s a)) => Action s a -> DL s ()
action :: forall a s. (Typeable a, Eq (Action s a)) => Action s a -> DL s ()
action Action s a
cmd = forall s a.
(s -> (a -> s -> DynFormula s) -> DynFormula s) -> DL s a
DL forall a b. (a -> b) -> a -> b
$ \s
_ () -> s -> DynFormula s
k -> forall a s.
(Typeable a, Eq (Action s a)) =>
Action s a -> (s -> DynFormula s) -> DynFormula s
DL.after Action s a
cmd forall a b. (a -> b) -> a -> b
$ () -> s -> DynFormula s
k ()

anyAction :: DL s ()
anyAction :: forall s. DL s ()
anyAction = forall s a.
(s -> (a -> s -> DynFormula s) -> DynFormula s) -> DL s a
DL forall a b. (a -> b) -> a -> b
$ \s
_ () -> s -> DynFormula s
k -> forall s. (s -> DynFormula s) -> DynFormula s
DL.afterAny forall a b. (a -> b) -> a -> b
$ () -> s -> DynFormula s
k ()

anyActions :: Int -> DL s ()
anyActions :: forall s. Int -> DL s ()
anyActions Int
n =
  forall s. DL s ()
stopping
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (forall s. Double -> DL s ()
weight (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall s. DL s ()
anyAction forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall s. Int -> DL s ()
anyActions Int
n)

-- average number of actions same as average length of a list
anyActions_ :: DL s ()
anyActions_ :: forall s. DL s ()
anyActions_ = do
  Int
n <- forall s. DL s Int
getSize
  forall s. Int -> DL s ()
anyActions (Int
n forall a. Integral a => a -> a -> a
`div` Int
2 forall a. Num a => a -> a -> a
+ Int
1)

stopping :: DL s ()
stopping :: forall s. DL s ()
stopping = forall s a.
(s -> (a -> s -> DynFormula s) -> DynFormula s) -> DL s a
DL forall a b. (a -> b) -> a -> b
$ \s
s () -> s -> DynFormula s
k -> forall s. DynFormula s -> DynFormula s
DL.toStop (() -> s -> DynFormula s
k () s
s)

weight :: Double -> DL s ()
weight :: forall s. Double -> DL s ()
weight Double
w = forall s a.
(s -> (a -> s -> DynFormula s) -> DynFormula s) -> DL s a
DL forall a b. (a -> b) -> a -> b
$ \s
s () -> s -> DynFormula s
k -> forall s. Double -> DynFormula s -> DynFormula s
DL.weight Double
w (() -> s -> DynFormula s
k () s
s)

getSize :: DL s Int
getSize :: forall s. DL s Int
getSize = forall s a.
(s -> (a -> s -> DynFormula s) -> DynFormula s) -> DL s a
DL forall a b. (a -> b) -> a -> b
$ \s
s Int -> s -> DynFormula s
k -> forall s. (Int -> DynFormula s) -> DynFormula s
DL.withSize forall a b. (a -> b) -> a -> b
$ \Int
n -> Int -> s -> DynFormula s
k Int
n s
s

getModelStateDL :: DL s s
getModelStateDL :: forall s. DL s s
getModelStateDL = forall s a.
(s -> (a -> s -> DynFormula s) -> DynFormula s) -> DL s a
DL forall a b. (a -> b) -> a -> b
$ \s
s s -> s -> DynFormula s
k -> s -> s -> DynFormula s
k s
s s
s

errorDL :: String -> DL s a
errorDL :: forall s a. String -> DL s a
errorDL String
name = forall s a.
(s -> (a -> s -> DynFormula s) -> DynFormula s) -> DL s a
DL forall a b. (a -> b) -> a -> b
$ \s
_ a -> s -> DynFormula s
_ -> forall s. String -> DynFormula s
DL.errorDL String
name

-- | Fail if the boolean is @False@.
--
--   Equivalent to
--
-- @
-- assert msg b = unless b (fail msg)
-- @
assert :: String -> Bool -> DL s ()
assert :: forall s. String -> Bool -> DL s ()
assert String
name Bool
b = if Bool
b then forall (m :: * -> *) a. Monad m => a -> m a
return () else forall s a. String -> DL s a
errorDL String
name

assertModel :: String -> (s -> Bool) -> DL s ()
assertModel :: forall s. String -> (s -> Bool) -> DL s ()
assertModel String
name s -> Bool
p = forall s. String -> Bool -> DL s ()
assert String
name forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> Bool
p forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall s. DL s s
getModelStateDL

monitorDL :: (Property -> Property) -> DL s ()
monitorDL :: forall s. (Property -> Property) -> DL s ()
monitorDL Property -> Property
f = forall s a.
(s -> (a -> s -> DynFormula s) -> DynFormula s) -> DL s a
DL forall a b. (a -> b) -> a -> b
$ \s
s () -> s -> DynFormula s
k -> forall s. (Property -> Property) -> DynFormula s -> DynFormula s
DL.monitorDL Property -> Property
f (() -> s -> DynFormula s
k () s
s)

-- | Generate a random value using the given `Quantification` (or list/tuple of quantifications).
--   Generated values will only shrink to smaller values that could also have been generated.
forAllQ :: Quantifiable q => q -> DL s (Quantifies q)
forAllQ :: forall q s. Quantifiable q => q -> DL s (Quantifies q)
forAllQ q
q = forall s a.
(s -> (a -> s -> DynFormula s) -> DynFormula s) -> DL s a
DL forall a b. (a -> b) -> a -> b
$ \s
s Quantifies q -> s -> DynFormula s
k -> forall q s.
Quantifiable q =>
q -> (Quantifies q -> DynFormula s) -> DynFormula s
DL.forAllQ q
q forall a b. (a -> b) -> a -> b
$ \Quantifies q
x -> Quantifies q -> s -> DynFormula s
k Quantifies q
x s
s

runDL :: s -> DL s () -> DL.DynFormula s
runDL :: forall s. s -> DL s () -> DynFormula s
runDL s
s DL s ()
dl = forall s a. DL s a -> s -> (a -> s -> DynFormula s) -> DynFormula s
unDL DL s ()
dl s
s forall a b. (a -> b) -> a -> b
$ \()
_ s
_ -> forall s. DynFormula s
DL.passTest

forAllUniqueDL ::
  (DL.DynLogicModel s, Testable a) =>
  Int ->
  s ->
  DL s () ->
  (Actions s -> a) ->
  Property
forAllUniqueDL :: forall s a.
(DynLogicModel s, Testable a) =>
Int -> s -> DL s () -> (Actions s -> a) -> Property
forAllUniqueDL Int
nextVar s
initState DL s ()
d = forall s a.
(DynLogicModel s, Testable a) =>
Int -> s -> DynFormula s -> (Actions s -> a) -> Property
DL.forAllUniqueScripts Int
nextVar s
initState (forall s. s -> DL s () -> DynFormula s
runDL s
initState DL s ()
d)

forAllDL ::
  (DL.DynLogicModel s, Testable a) =>
  DL s () ->
  (Actions s -> a) ->
  Property
forAllDL :: forall s a.
(DynLogicModel s, Testable a) =>
DL s () -> (Actions s -> a) -> Property
forAllDL DL s ()
d = forall s a.
(DynLogicModel s, Testable a) =>
DynFormula s -> (Actions s -> a) -> Property
DL.forAllScripts (forall s. s -> DL s () -> DynFormula s
runDL forall state. StateModel state => state
initialState DL s ()
d)

forAllDL_ ::
  (DL.DynLogicModel s, Testable a) =>
  DL s () ->
  (Actions s -> a) ->
  Property
forAllDL_ :: forall s a.
(DynLogicModel s, Testable a) =>
DL s () -> (Actions s -> a) -> Property
forAllDL_ DL s ()
d = forall s a.
(DynLogicModel s, Testable a) =>
DynFormula s -> (Actions s -> a) -> Property
DL.forAllScripts_ (forall s. s -> DL s () -> DynFormula s
runDL forall state. StateModel state => state
initialState DL s ()
d)

forAllMappedDL ::
  (DL.DynLogicModel s, Testable a, Show rep) =>
  (rep -> DL.DynLogicTest s) ->
  (DL.DynLogicTest s -> rep) ->
  (Actions s -> srep) ->
  DL s () ->
  (srep -> a) ->
  Property
forAllMappedDL :: forall s a rep srep.
(DynLogicModel s, Testable a, Show rep) =>
(rep -> DynLogicTest s)
-> (DynLogicTest s -> rep)
-> (Actions s -> srep)
-> DL s ()
-> (srep -> a)
-> Property
forAllMappedDL rep -> DynLogicTest s
to DynLogicTest s -> rep
from Actions s -> srep
fromScript DL s ()
d srep -> a
prop =
  forall s a rep.
(DynLogicModel s, Testable a, Show rep) =>
(rep -> DynLogicTest s)
-> (DynLogicTest s -> rep)
-> DynFormula s
-> (Actions s -> a)
-> Property
DL.forAllMappedScripts rep -> DynLogicTest s
to DynLogicTest s -> rep
from (forall s. s -> DL s () -> DynFormula s
runDL forall state. StateModel state => state
initialState DL s ()
d) (srep -> a
prop forall b c a. (b -> c) -> (a -> b) -> a -> c
. Actions s -> srep
fromScript)

forAllMappedDL_ ::
  (DL.DynLogicModel s, Testable a, Show rep) =>
  (rep -> DL.DynLogicTest s) ->
  (DL.DynLogicTest s -> rep) ->
  (Actions s -> srep) ->
  DL s () ->
  (srep -> a) ->
  Property
forAllMappedDL_ :: forall s a rep srep.
(DynLogicModel s, Testable a, Show rep) =>
(rep -> DynLogicTest s)
-> (DynLogicTest s -> rep)
-> (Actions s -> srep)
-> DL s ()
-> (srep -> a)
-> Property
forAllMappedDL_ rep -> DynLogicTest s
to DynLogicTest s -> rep
from Actions s -> srep
fromScript DL s ()
d srep -> a
prop =
  forall s a rep.
(DynLogicModel s, Testable a, Show rep) =>
(rep -> DynLogicTest s)
-> (DynLogicTest s -> rep)
-> DynFormula s
-> (Actions s -> a)
-> Property
DL.forAllMappedScripts_ rep -> DynLogicTest s
to DynLogicTest s -> rep
from (forall s. s -> DL s () -> DynFormula s
runDL forall state. StateModel state => state
initialState DL s ()
d) (srep -> a
prop forall b c a. (b -> c) -> (a -> b) -> a -> c
. Actions s -> srep
fromScript)

withDLTest :: (DL.DynLogicModel s, Testable a) => DL s () -> (Actions s -> a) -> DL.DynLogicTest s -> Property
withDLTest :: forall s a.
(DynLogicModel s, Testable a) =>
DL s () -> (Actions s -> a) -> DynLogicTest s -> Property
withDLTest DL s ()
d = forall s a.
(DynLogicModel s, Testable a) =>
DynFormula s -> (Actions s -> a) -> DynLogicTest s -> Property
DL.withDLScriptPrefix (forall s. s -> DL s () -> DynFormula s
runDL forall state. StateModel state => state
initialState DL s ()
d)