{-# LANGUAGE FlexibleContexts #-}

-- | 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 {DL s a -> s -> (a -> s -> DynFormula s) -> DynFormula s
unDL :: s -> (a -> s -> DL.DynFormula s) -> DL.DynFormula s}
  deriving (a -> DL s b -> DL s a
(a -> b) -> DL s a -> DL s b
(forall a b. (a -> b) -> DL s a -> DL s b)
-> (forall a b. a -> DL s b -> DL s a) -> Functor (DL s)
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
<$ :: a -> DL s b -> DL s a
$c<$ :: forall s a b. a -> DL s b -> DL s a
fmap :: (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 :: a -> DL s a
pure a
x = (s -> (a -> s -> DynFormula s) -> DynFormula s) -> DL s a
forall s a.
(s -> (a -> s -> DynFormula s) -> DynFormula s) -> DL s a
DL ((s -> (a -> s -> DynFormula s) -> DynFormula s) -> DL s a)
-> (s -> (a -> s -> DynFormula s) -> DynFormula s) -> DL s a
forall a b. (a -> b) -> a -> b
$ \s
s a -> s -> DynFormula s
k -> a -> s -> DynFormula s
k a
x s
s
  <*> :: DL s (a -> b) -> DL s a -> DL s 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 :: DL s a
empty = (s -> (a -> s -> DynFormula s) -> DynFormula s) -> DL s a
forall s a.
(s -> (a -> s -> DynFormula s) -> DynFormula s) -> DL s a
DL ((s -> (a -> s -> DynFormula s) -> DynFormula s) -> DL s a)
-> (s -> (a -> s -> DynFormula s) -> DynFormula s) -> DL s a
forall a b. (a -> b) -> a -> b
$ \s
_ a -> s -> DynFormula s
_ -> DynFormula s
forall s. DynFormula s
DL.ignore
  DL s -> (a -> s -> DynFormula s) -> DynFormula s
h <|> :: DL s a -> DL s a -> DL s a
<|> DL s -> (a -> s -> DynFormula s) -> DynFormula s
j = (s -> (a -> s -> DynFormula s) -> DynFormula s) -> DL s a
forall s a.
(s -> (a -> s -> DynFormula s) -> DynFormula s) -> DL s a
DL ((s -> (a -> s -> DynFormula s) -> DynFormula s) -> DL s a)
-> (s -> (a -> s -> DynFormula s) -> DynFormula s) -> DL s a
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 DynFormula s -> DynFormula s -> DynFormula s
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 :: a -> DL s a
return = a -> DL s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  DL s -> (a -> s -> DynFormula s) -> DynFormula s
h >>= :: DL s a -> (a -> DL s b) -> DL s b
>>= a -> DL s b
j = (s -> (b -> s -> DynFormula s) -> DynFormula s) -> DL s b
forall s a.
(s -> (a -> s -> DynFormula s) -> DynFormula s) -> DL s a
DL ((s -> (b -> s -> DynFormula s) -> DynFormula s) -> DL s b)
-> (s -> (b -> s -> DynFormula s) -> DynFormula s) -> DL s b
forall a b. (a -> b) -> a -> b
$ \s
s b -> s -> DynFormula s
k -> s -> (a -> s -> DynFormula s) -> DynFormula s
h s
s ((a -> s -> DynFormula s) -> DynFormula s)
-> (a -> s -> DynFormula s) -> DynFormula s
forall a b. (a -> b) -> a -> b
$ \a
x s
s1 -> DL s b -> s -> (b -> s -> DynFormula s) -> DynFormula s
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 :: String -> DL s a
fail = String -> DL s a
forall s a. String -> DL s a
errorDL

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

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

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

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

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

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

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

getModelStateDL :: DL s s
getModelStateDL :: DL s s
getModelStateDL = (s -> (s -> s -> DynFormula s) -> DynFormula s) -> DL s s
forall s a.
(s -> (a -> s -> DynFormula s) -> DynFormula s) -> DL s a
DL ((s -> (s -> s -> DynFormula s) -> DynFormula s) -> DL s s)
-> (s -> (s -> s -> DynFormula s) -> DynFormula s) -> DL s s
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 :: String -> DL s a
errorDL String
name = (s -> (a -> s -> DynFormula s) -> DynFormula s) -> DL s a
forall s a.
(s -> (a -> s -> DynFormula s) -> DynFormula s) -> DL s a
DL ((s -> (a -> s -> DynFormula s) -> DynFormula s) -> DL s a)
-> (s -> (a -> s -> DynFormula s) -> DynFormula s) -> DL s a
forall a b. (a -> b) -> a -> b
$ \s
_ a -> s -> DynFormula s
_ -> String -> 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 :: String -> Bool -> DL s ()
assert String
name Bool
b = if Bool
b then () -> DL s ()
forall (m :: * -> *) a. Monad m => a -> m a
return () else String -> DL s ()
forall s a. String -> DL s a
errorDL String
name

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

monitorDL :: (Property -> Property) -> DL s ()
monitorDL :: (Property -> Property) -> DL s ()
monitorDL Property -> Property
f = (s -> (() -> s -> DynFormula s) -> DynFormula s) -> DL s ()
forall s a.
(s -> (a -> s -> DynFormula s) -> DynFormula s) -> DL s a
DL ((s -> (() -> s -> DynFormula s) -> DynFormula s) -> DL s ())
-> (s -> (() -> s -> DynFormula s) -> DynFormula s) -> DL s ()
forall a b. (a -> b) -> a -> b
$ \s
s () -> s -> DynFormula s
k -> (Property -> Property) -> DynFormula s -> DynFormula s
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 :: q -> DL s (Quantifies q)
forAllQ q
q = (s -> (Quantifies q -> s -> DynFormula s) -> DynFormula s)
-> DL s (Quantifies q)
forall s a.
(s -> (a -> s -> DynFormula s) -> DynFormula s) -> DL s a
DL ((s -> (Quantifies q -> s -> DynFormula s) -> DynFormula s)
 -> DL s (Quantifies q))
-> (s -> (Quantifies q -> s -> DynFormula s) -> DynFormula s)
-> DL s (Quantifies q)
forall a b. (a -> b) -> a -> b
$ \s
s Quantifies q -> s -> DynFormula s
k -> q -> (Quantifies q -> DynFormula s) -> DynFormula s
forall q s.
Quantifiable q =>
q -> (Quantifies q -> DynFormula s) -> DynFormula s
DL.forAllQ q
q ((Quantifies q -> DynFormula s) -> DynFormula s)
-> (Quantifies q -> DynFormula s) -> DynFormula s
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 :: s -> DL s () -> DynFormula s
runDL s
s DL s ()
dl = DL s () -> s -> (() -> s -> DynFormula s) -> DynFormula s
forall s a. DL s a -> s -> (a -> s -> DynFormula s) -> DynFormula s
unDL DL s ()
dl s
s ((() -> s -> DynFormula s) -> DynFormula s)
-> (() -> s -> DynFormula s) -> DynFormula s
forall a b. (a -> b) -> a -> b
$ \()
_ s
_ -> DynFormula s
forall s. DynFormula s
DL.passTest

forAllUniqueDL ::
  (DL.DynLogicModel s, Testable a) =>
  Int ->
  s ->
  DL s () ->
  (Actions s -> a) ->
  Property
forAllUniqueDL :: Int -> s -> DL s () -> (Actions s -> a) -> Property
forAllUniqueDL Int
nextVar s
initState DL s ()
d = Int -> s -> DynFormula s -> (Actions s -> a) -> Property
forall s a.
(DynLogicModel s, Testable a) =>
Int -> s -> DynFormula s -> (Actions s -> a) -> Property
DL.forAllUniqueScripts Int
nextVar s
initState (s -> DL s () -> DynFormula s
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 :: DL s () -> (Actions s -> a) -> Property
forAllDL DL s ()
d = DynFormula s -> (Actions s -> a) -> Property
forall s a.
(DynLogicModel s, Testable a) =>
DynFormula s -> (Actions s -> a) -> Property
DL.forAllScripts (s -> DL s () -> DynFormula s
forall s. s -> DL s () -> DynFormula s
runDL s
forall state. StateModel state => state
initialState DL s ()
d)

forAllDL_ ::
  (DL.DynLogicModel s, Testable a) =>
  DL s () ->
  (Actions s -> a) ->
  Property
forAllDL_ :: DL s () -> (Actions s -> a) -> Property
forAllDL_ DL s ()
d = DynFormula s -> (Actions s -> a) -> Property
forall s a.
(DynLogicModel s, Testable a) =>
DynFormula s -> (Actions s -> a) -> Property
DL.forAllScripts_ (s -> DL s () -> DynFormula s
forall s. s -> DL s () -> DynFormula s
runDL s
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 :: (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 =
  (rep -> DynLogicTest s)
-> (DynLogicTest s -> rep)
-> DynFormula s
-> (Actions s -> a)
-> Property
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 (s -> DL s () -> DynFormula s
forall s. s -> DL s () -> DynFormula s
runDL s
forall state. StateModel state => state
initialState DL s ()
d) (srep -> a
prop (srep -> a) -> (Actions s -> srep) -> Actions s -> a
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_ :: (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 =
  (rep -> DynLogicTest s)
-> (DynLogicTest s -> rep)
-> DynFormula s
-> (Actions s -> a)
-> Property
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 (s -> DL s () -> DynFormula s
forall s. s -> DL s () -> DynFormula s
runDL s
forall state. StateModel state => state
initialState DL s ()
d) (srep -> a
prop (srep -> a) -> (Actions s -> srep) -> Actions s -> a
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 :: DL s () -> (Actions s -> a) -> DynLogicTest s -> Property
withDLTest DL s ()
d = DynFormula s -> (Actions s -> a) -> DynLogicTest s -> Property
forall s a.
(DynLogicModel s, Testable a) =>
DynFormula s -> (Actions s -> a) -> DynLogicTest s -> Property
DL.withDLScriptPrefix (s -> DL s () -> DynFormula s
forall s. s -> DL s () -> DynFormula s
runDL s
forall state. StateModel state => state
initialState DL s ()
d)