-- | 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.Internal` 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,
  getVarContextDL,
  forAllVar,
  assert,
  assertModel,
  monitorDL,
  forAllQ,
  forAllDL,
  forAllMappedDL,
  forAllUniqueDL,
  DL.DynLogicModel (..),
  module Test.QuickCheck.DynamicLogic.Quantify,
) where

import Control.Applicative
import Control.Monad
import Data.Typeable
import Test.QuickCheck hiding (getSize)
import Test.QuickCheck.DynamicLogic.Internal 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 (with
--   variable context) threaded through.
newtype DL s a = DL {forall s a.
DL s a
-> Annotated s
-> (a -> Annotated s -> DynFormula s)
-> DynFormula s
unDL :: Annotated s -> (a -> Annotated 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.
(Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
DL forall a b. (a -> b) -> a -> b
$ \Annotated s
s a -> Annotated s -> DynFormula s
k -> a -> Annotated s -> DynFormula s
k a
x Annotated 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.
(Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
DL forall a b. (a -> b) -> a -> b
$ \Annotated s
_ a -> Annotated s -> DynFormula s
_ -> forall s. DynFormula s
DL.ignore
  DL Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s
h <|> :: forall a. DL s a -> DL s a -> DL s a
<|> DL Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s
j = forall s a.
(Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
DL forall a b. (a -> b) -> a -> b
$ \Annotated s
s a -> Annotated s -> DynFormula s
k -> Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s
h Annotated s
s a -> Annotated s -> DynFormula s
k forall s. DynFormula s -> DynFormula s -> DynFormula s
DL.||| Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s
j Annotated s
s a -> Annotated 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 Annotated s -> (a -> Annotated 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.
(Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
DL forall a b. (a -> b) -> a -> b
$ \Annotated s
s b -> Annotated s -> DynFormula s
k -> Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s
h Annotated s
s forall a b. (a -> b) -> a -> b
$ \a
x Annotated s
s1 -> forall s a.
DL s a
-> Annotated s
-> (a -> Annotated s -> DynFormula s)
-> DynFormula s
unDL (a -> DL s b
j a
x) Annotated s
s1 b -> Annotated 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), Show (Action s a)) => Action s a -> DL s (Var a)
action :: forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action Action s a
cmd = forall s a.
(Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
DL forall a b. (a -> b) -> a -> b
$ \Annotated s
_ Var a -> Annotated s -> DynFormula s
k -> forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a
-> (Var a -> Annotated s -> DynFormula s) -> DynFormula s
DL.after Action s a
cmd Var a -> Annotated s -> DynFormula s
k

anyAction :: DL s ()
anyAction :: forall s. DL s ()
anyAction = forall s a.
(Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
DL forall a b. (a -> b) -> a -> b
$ \Annotated s
_ () -> Annotated s -> DynFormula s
k -> forall s. (Annotated s -> DynFormula s) -> DynFormula s
DL.afterAny forall a b. (a -> b) -> a -> b
$ () -> Annotated 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.
(Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
DL forall a b. (a -> b) -> a -> b
$ \Annotated s
s () -> Annotated s -> DynFormula s
k -> forall s. DynFormula s -> DynFormula s
DL.toStop (() -> Annotated s -> DynFormula s
k () Annotated s
s)

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

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

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

getVarContextDL :: DL s VarContext
getVarContextDL :: forall s. DL s VarContext
getVarContextDL = forall s a.
(Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
DL forall a b. (a -> b) -> a -> b
$ \Annotated s
s VarContext -> Annotated s -> DynFormula s
k -> VarContext -> Annotated s -> DynFormula s
k (forall state. Annotated state -> VarContext
vars Annotated s
s) Annotated s
s

forAllVar :: forall a s. Typeable a => DL s (Var a)
forAllVar :: forall a s. Typeable a => DL s (Var a)
forAllVar = do
  [Var a]
xs <- forall a. Typeable a => VarContext -> [Var a]
ctxAtType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s. DL s VarContext
getVarContextDL
  forall q s. Quantifiable q => q -> DL s (Quantifies q)
forAllQ forall a b. (a -> b) -> a -> b
$ forall a. Eq a => [a] -> Quantification a
elementsQ [Var a]
xs

errorDL :: String -> DL s a
errorDL :: forall s a. String -> DL s a
errorDL String
name = forall s a.
(Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
DL forall a b. (a -> b) -> a -> b
$ \Annotated s
_ a -> Annotated 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.
(Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
DL forall a b. (a -> b) -> a -> b
$ \Annotated s
s () -> Annotated s -> DynFormula s
k -> forall s. (Property -> Property) -> DynFormula s -> DynFormula s
DL.monitorDL Property -> Property
f (() -> Annotated s -> DynFormula s
k () Annotated 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.
(Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
DL forall a b. (a -> b) -> a -> b
$ \Annotated s
s Quantifies q -> Annotated 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 -> Annotated s -> DynFormula s
k Quantifies q
x Annotated s
s

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

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

forAllMappedDL ::
  (DL.DynLogicModel s, Testable a) =>
  (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) =>
(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) =>
(rep -> DynLogicTest s)
-> (DynLogicTest s -> rep)
-> DynFormula s
-> (Actions s -> a)
-> Property
DL.forAllMappedScripts rep -> DynLogicTest s
to DynLogicTest s -> rep
from (forall s. Annotated s -> DL s () -> DynFormula s
runDL forall state. StateModel state => Annotated state
initialAnnotatedState DL s ()
d) (srep -> a
prop forall b c a. (b -> c) -> (a -> b) -> a -> c
. Actions s -> srep
fromScript)