{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Test.Control.State.Transition.Trace.Generator.QuickCheck (
  HasTrace (BaseEnv, envGen, sigGen, shrinkSignal, interpretSTS),
  traceFrom,
  traceFromInitState,
  trace,
  shrinkTrace,

  -- * Trace generator properties
  forAllTrace,
  forAllTraceFromInitState,
  onlyValidSignalsAreGenerated,
  onlyValidSignalsAreGeneratedFromInitState,

  -- * Trace classification
  traceLengthsAreClassified,
  classifyTraceLength,
  classifySize,

  -- * Internal
  mkIntervals,
)
where

import Control.State.Transition (Environment, IRC (IRC), STS, Signal, State, TRC (TRC))
import qualified Control.State.Transition.Extended as STS
import Data.Functor.Identity (Identity (..))
import Data.Kind (Type)
import Data.List.NonEmpty (NonEmpty)
import Data.Maybe (fromMaybe)
import Data.Word (Word64)
import GHC.Stack
import Test.Control.State.Transition.Trace (Trace)
import qualified Test.Control.State.Transition.Trace as Trace
import qualified Test.QuickCheck as QuickCheck

-- | State transition systems for which traces can be generated, given a trace
-- generation environment.
--
-- The trace generation environment allows to pass relevant data to the trace
-- generation algorithm.
class STS sts => HasTrace sts traceGenEnv where
  type BaseEnv sts :: Type
  type BaseEnv s = ()

  -- | Interpret the action from the base monad into a pure value, given some
  -- initial environment. This obviously places some contraints on the nature of
  -- the base monad for a trace to be completed.
  interpretSTS :: forall a. HasCallStack => (BaseEnv sts -> STS.BaseM sts a -> a)
  default interpretSTS :: STS.BaseM sts ~ Identity => forall a. BaseEnv sts -> STS.BaseM sts a -> a
  interpretSTS BaseEnv sts
_ (Identity a
x) = a
x

  envGen :: HasCallStack => traceGenEnv -> QuickCheck.Gen (Environment sts)

  sigGen ::
    HasCallStack =>
    traceGenEnv ->
    Environment sts ->
    State sts ->
    QuickCheck.Gen (Signal sts)

  shrinkSignal :: HasCallStack => Signal sts -> [Signal sts]

-- | Generate a random trace starting in the given environment and initial state.
traceFrom ::
  forall sts traceGenEnv.
  HasTrace sts traceGenEnv =>
  BaseEnv sts ->
  -- | Maximum trace length.
  Word64 ->
  traceGenEnv ->
  Environment sts ->
  State sts ->
  QuickCheck.Gen (Trace sts)
traceFrom :: forall sts traceGenEnv.
HasTrace sts traceGenEnv =>
BaseEnv sts
-> Word64
-> traceGenEnv
-> Environment sts
-> State sts
-> Gen (Trace sts)
traceFrom BaseEnv sts
traceEnv Word64
maxTraceLength traceGenEnv
traceGenEnv Environment sts
env State sts
st0 = do
  Word64
chosenTraceLength <- forall a. Random a => (a, a) -> Gen a
QuickCheck.choose (Word64
0, Word64
maxTraceLength)
  forall s.
Environment s -> State s -> [(State s, Signal s)] -> Trace s
Trace.mkTrace Environment sts
env State sts
st0 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Word64
-> State sts
-> [(State sts, Signal sts)]
-> Gen [(State sts, Signal sts)]
loop Word64
chosenTraceLength State sts
st0 []
  where
    loop ::
      Word64 ->
      State sts ->
      [(State sts, Signal sts)] ->
      QuickCheck.Gen [(State sts, Signal sts)]
    loop :: Word64
-> State sts
-> [(State sts, Signal sts)]
-> Gen [(State sts, Signal sts)]
loop Word64
0 State sts
_ ![(State sts, Signal sts)]
acc = forall (f :: * -> *) a. Applicative f => a -> f a
pure [(State sts, Signal sts)]
acc
    loop Word64
d !State sts
sti ![(State sts, Signal sts)]
stSigs = do
      Signal sts
sig <- forall sts traceGenEnv.
(HasTrace sts traceGenEnv, HasCallStack) =>
traceGenEnv -> Environment sts -> State sts -> Gen (Signal sts)
sigGen @sts @traceGenEnv traceGenEnv
traceGenEnv Environment sts
env State sts
sti
      case forall sts traceGenEnv a.
(HasTrace sts traceGenEnv, HasCallStack) =>
BaseEnv sts -> BaseM sts a -> a
interpretSTS @sts @traceGenEnv BaseEnv sts
traceEnv (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
Trace.applySTSTest @sts (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment sts
env, State sts
sti, Signal sts
sig))) of
        Left NonEmpty (PredicateFailure sts)
_predicateFailures ->
          Word64
-> State sts
-> [(State sts, Signal sts)]
-> Gen [(State sts, Signal sts)]
loop (Word64
d forall a. Num a => a -> a -> a
- Word64
1) State sts
sti [(State sts, Signal sts)]
stSigs
        Right State sts
sti' ->
          Word64
-> State sts
-> [(State sts, Signal sts)]
-> Gen [(State sts, Signal sts)]
loop (Word64
d forall a. Num a => a -> a -> a
- Word64
1) State sts
sti' ((State sts
sti', Signal sts
sig) forall a. a -> [a] -> [a]
: [(State sts, Signal sts)]
stSigs)

-- | Generate a random trace.
trace ::
  forall sts traceGenEnv.
  ( HasTrace sts traceGenEnv
  , Show (Environment sts)
  ) =>
  BaseEnv sts ->
  -- | Maximum trace length.
  Word64 ->
  traceGenEnv ->
  QuickCheck.Gen (Trace sts)
trace :: forall sts traceGenEnv.
(HasTrace sts traceGenEnv, Show (Environment sts)) =>
BaseEnv sts -> Word64 -> traceGenEnv -> Gen (Trace sts)
trace BaseEnv sts
traceEnv Word64
maxTraceLength traceGenEnv
traceGenEnv =
  forall sts traceGenEnv.
(HasTrace sts traceGenEnv, Show (Environment sts), HasCallStack) =>
BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
     (IRC sts
      -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
-> Gen (Trace sts)
traceFromInitState BaseEnv sts
traceEnv Word64
maxTraceLength traceGenEnv
traceGenEnv forall a. Maybe a
Nothing

-- | Generate a random trace given a generator for initial state.
--
-- Takes an optional generator for initial state, or defaults to 'applySTS'
-- if no initial state is required by the STS.
traceFromInitState ::
  forall sts traceGenEnv.
  ( HasTrace sts traceGenEnv
  , Show (Environment sts)
  , HasCallStack
  ) =>
  BaseEnv sts ->
  -- | Maximum trace length.
  Word64 ->
  traceGenEnv ->
  -- | Optional generator of STS initial state
  Maybe (IRC sts -> QuickCheck.Gen (Either (NonEmpty (STS.PredicateFailure sts)) (State sts))) ->
  QuickCheck.Gen (Trace sts)
traceFromInitState :: forall sts traceGenEnv.
(HasTrace sts traceGenEnv, Show (Environment sts), HasCallStack) =>
BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
     (IRC sts
      -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
-> Gen (Trace sts)
traceFromInitState BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv Maybe
  (IRC sts
   -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
genSt0 = do
  Environment sts
env <- forall sts traceGenEnv.
(HasTrace sts traceGenEnv, HasCallStack) =>
traceGenEnv -> Gen (Environment sts)
envGen @sts @traceGenEnv traceGenEnv
traceGenEnv
  Either (NonEmpty (PredicateFailure sts)) (State sts)
res <-
    forall a. a -> Maybe a -> a
fromMaybe
      ( forall (f :: * -> *) a. Applicative f => a -> f a
pure
          forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sts traceGenEnv a.
(HasTrace sts traceGenEnv, HasCallStack) =>
BaseEnv sts -> BaseM sts a -> a
interpretSTS @sts @traceGenEnv BaseEnv sts
baseEnv
          forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
Trace.applySTSTest
      )
      Maybe
  (IRC sts
   -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
genSt0
      forall a b. (a -> b) -> a -> b
$ forall sts. Environment sts -> IRC sts
IRC Environment sts
env

  case Either (NonEmpty (PredicateFailure sts)) (State sts)
res of
    Left NonEmpty (PredicateFailure sts)
pf ->
      forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$
        [Char]
"Failed to apply the initial rule to the generated environment.\n"
          forall a. [a] -> [a] -> [a]
++ [Char]
"Generated environment: "
          forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Environment sts
env
          forall a. [a] -> [a] -> [a]
++ [Char]
"Failure: "
          forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show NonEmpty (PredicateFailure sts)
pf
    Right State sts
st0 -> forall sts traceGenEnv.
HasTrace sts traceGenEnv =>
BaseEnv sts
-> Word64
-> traceGenEnv
-> Environment sts
-> State sts
-> Gen (Trace sts)
traceFrom BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv Environment sts
env State sts
st0

-- | Check a property on the 'sts' traces.
--
-- Takes an optional generator for initial state of the STS.
forAllTraceFromInitState ::
  forall sts traceGenEnv prop.
  ( HasTrace sts traceGenEnv
  , QuickCheck.Testable prop
  , Show (Environment sts)
  ) =>
  BaseEnv sts ->
  -- | Maximum trace length.
  Word64 ->
  traceGenEnv ->
  -- | Optional generator of STS initial state
  Maybe (IRC sts -> QuickCheck.Gen (Either (NonEmpty (STS.PredicateFailure sts)) (State sts))) ->
  (Trace sts -> prop) ->
  QuickCheck.Property
forAllTraceFromInitState :: forall sts traceGenEnv prop.
(HasTrace sts traceGenEnv, Testable prop,
 Show (Environment sts)) =>
BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
     (IRC sts
      -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
-> (Trace sts -> prop)
-> Property
forAllTraceFromInitState BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv Maybe
  (IRC sts
   -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
genSt0 Trace sts -> prop
prop =
  forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
QuickCheck.forAllShrinkBlind
    (forall sts traceGenEnv.
(HasTrace sts traceGenEnv, Show (Environment sts), HasCallStack) =>
BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
     (IRC sts
      -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
-> Gen (Trace sts)
traceFromInitState @sts @traceGenEnv BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv Maybe
  (IRC sts
   -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
genSt0)
    (forall sts traceGenEnv.
HasTrace sts traceGenEnv =>
BaseEnv sts -> Trace sts -> [Trace sts]
shrinkTrace @sts @traceGenEnv BaseEnv sts
baseEnv)
    Trace sts -> prop
prop

-- | Check a property on the 'sts' traces.
forAllTrace ::
  forall sts traceGenEnv prop.
  ( HasTrace sts traceGenEnv
  , QuickCheck.Testable prop
  , Show (Environment sts)
  ) =>
  BaseEnv sts ->
  -- | Maximum trace length.
  Word64 ->
  traceGenEnv ->
  (Trace sts -> prop) ->
  QuickCheck.Property
forAllTrace :: forall sts traceGenEnv prop.
(HasTrace sts traceGenEnv, Testable prop,
 Show (Environment sts)) =>
BaseEnv sts
-> Word64 -> traceGenEnv -> (Trace sts -> prop) -> Property
forAllTrace BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv =
  forall sts traceGenEnv prop.
(HasTrace sts traceGenEnv, Testable prop,
 Show (Environment sts)) =>
BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
     (IRC sts
      -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
-> (Trace sts -> prop)
-> Property
forAllTraceFromInitState BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv forall a. Maybe a
Nothing

-- | Shrink a trace by shrinking the list of signals and reconstructing traces from these
-- shrunk lists of signals.
--
-- When shrinking a trace that is failing some property (often stated in terms of a signal in the trace)
-- then the most recent signal is likely crucial to the failure of the property and must be preserved
-- in the shrunk traces.
shrinkTrace ::
  forall sts traceGenEnv.
  HasTrace sts traceGenEnv =>
  BaseEnv sts ->
  Trace sts ->
  [Trace sts]
shrinkTrace :: forall sts traceGenEnv.
HasTrace sts traceGenEnv =>
BaseEnv sts -> Trace sts -> [Trace sts]
shrinkTrace BaseEnv sts
baseEnv Trace sts
tr =
  forall sts traceGenEnv a.
(HasTrace sts traceGenEnv, HasCallStack) =>
BaseEnv sts -> BaseM sts a -> a
interpretSTS @sts @traceGenEnv BaseEnv sts
baseEnv forall a b. (a -> b) -> a -> b
$
    forall s (m :: * -> *).
(STS s, m ~ BaseM s) =>
Environment s -> State s -> [Signal s] -> m (Trace s)
Trace.closure Environment sts
env State sts
st0 forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
`traverse` forall {a}. [a] -> [[a]]
shrinkSignals [Signal sts]
signals
  where
    env :: Environment sts
env = forall s. Trace s -> Environment s
Trace._traceEnv Trace sts
tr
    st0 :: State sts
st0 = forall s. Trace s -> State s
Trace._traceInitState Trace sts
tr
    signals :: [Signal sts]
signals = forall s. TraceOrder -> Trace s -> [Signal s]
Trace.traceSignals TraceOrder
Trace.NewestFirst Trace sts
tr

    -- Shrink a list of signals such that we preserve the most recent signal in the shrunk lists.
    -- This shrinker
    --   - recursively omits all but the most recent signal
    --   - builds up lists of signals starting with the most recent signal and
    --     building up to a list excluding the first (oldest) signal
    --   - explicitly shrinks in order from small to larger lists of signals
    --     (i.e. ordered by most to least aggressive shrinking)
    shrinkSignals :: [a] -> [[a]]
shrinkSignals (a
sn : a
_last : []) =
      [[a
sn]]
    shrinkSignals (a
sn : a
sm : [a]
sigs) =
      [[a
sn]] -- a trace with only the most recent signal
        forall a. [a] -> [a] -> [a]
++ ((a
sn forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a] -> [[a]]
shrinkSignals (a
sm forall a. a -> [a] -> [a]
: [a]
sigs)) -- shrink the tail
        forall a. [a] -> [a] -> [a]
++ [a
sn forall a. a -> [a] -> [a]
: [a]
sigs] -- discard the second most recent signal

    -- shrink to [] if there is one or no signals
    shrinkSignals [a]
_ = []

-- | Property that asserts that only valid signals are generated.
onlyValidSignalsAreGenerated ::
  forall sts traceGenEnv.
  ( HasTrace sts traceGenEnv
  , Show (Environment sts)
  , Show (Signal sts)
  ) =>
  BaseEnv sts ->
  -- | Maximum trace length.
  Word64 ->
  traceGenEnv ->
  QuickCheck.Property
onlyValidSignalsAreGenerated :: forall sts traceGenEnv.
(HasTrace sts traceGenEnv, Show (Environment sts),
 Show (Signal sts)) =>
BaseEnv sts -> Word64 -> traceGenEnv -> Property
onlyValidSignalsAreGenerated BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv =
  forall sts traceGenEnv.
(HasTrace sts traceGenEnv, Show (Environment sts),
 Show (Signal sts)) =>
BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
     (IRC sts
      -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
-> Property
onlyValidSignalsAreGeneratedFromInitState @sts BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv forall a. Maybe a
Nothing

-- | Property that asserts that only valid signals are generated.
--
-- Takes an optional generator for initial state of the STS.
onlyValidSignalsAreGeneratedFromInitState ::
  forall sts traceGenEnv.
  ( HasTrace sts traceGenEnv
  , Show (Environment sts)
  , Show (Signal sts)
  ) =>
  BaseEnv sts ->
  -- | Maximum trace length.
  Word64 ->
  traceGenEnv ->
  -- | Optional generator of STS initial state
  Maybe (IRC sts -> QuickCheck.Gen (Either (NonEmpty (STS.PredicateFailure sts)) (State sts))) ->
  QuickCheck.Property
onlyValidSignalsAreGeneratedFromInitState :: forall sts traceGenEnv.
(HasTrace sts traceGenEnv, Show (Environment sts),
 Show (Signal sts)) =>
BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
     (IRC sts
      -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
-> Property
onlyValidSignalsAreGeneratedFromInitState BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv Maybe
  (IRC sts
   -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
genSt0 =
  forall sts traceGenEnv prop.
(HasTrace sts traceGenEnv, Testable prop,
 Show (Environment sts)) =>
BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
     (IRC sts
      -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
-> (Trace sts -> prop)
-> Property
forAllTraceFromInitState BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv Maybe
  (IRC sts
   -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
genSt0 Trace sts -> Property
validSignalsAreGenerated
  where
    validSignalsAreGenerated ::
      Trace sts ->
      QuickCheck.Property
    validSignalsAreGenerated :: Trace sts -> Property
validSignalsAreGenerated Trace sts
someTrace =
      forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
QuickCheck.forAllShrink
        (forall sts traceGenEnv.
(HasTrace sts traceGenEnv, HasCallStack) =>
traceGenEnv -> Environment sts -> State sts -> Gen (Signal sts)
sigGen @sts @traceGenEnv traceGenEnv
traceGenEnv Environment sts
env State sts
lastState)
        (forall sts traceGenEnv.
(HasTrace sts traceGenEnv, HasCallStack) =>
Signal sts -> [Signal sts]
shrinkSignal @sts @traceGenEnv)
        Signal sts -> Property
signalIsValid
      where
        signalIsValid :: Signal sts -> Property
signalIsValid Signal sts
signal =
          case forall sts traceGenEnv a.
(HasTrace sts traceGenEnv, HasCallStack) =>
BaseEnv sts -> BaseM sts a -> a
interpretSTS @sts @traceGenEnv BaseEnv sts
baseEnv (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
Trace.applySTSTest @sts (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment sts
env, State sts
lastState, Signal sts
signal))) of
            Left NonEmpty (PredicateFailure sts)
pf -> forall prop. Testable prop => [Char] -> prop -> Property
QuickCheck.counterexample (forall a. Show a => a -> [Char]
show (Signal sts
signal, NonEmpty (PredicateFailure sts)
pf)) Bool
False
            Right State sts
_ -> forall prop. Testable prop => prop -> Property
QuickCheck.property Bool
True
        env :: Environment sts
env = forall s. Trace s -> Environment s
Trace._traceEnv Trace sts
someTrace
        lastState :: State sts
lastState = forall s. Trace s -> State s
Trace.lastState Trace sts
someTrace

--------------------------------------------------------------------------------
-- Trace classification
--------------------------------------------------------------------------------

-- | Property that simply classifies the lengths of the generated traces.
traceLengthsAreClassified ::
  forall sts traceGenEnv.
  ( HasTrace sts traceGenEnv
  , Show (Environment sts)
  ) =>
  BaseEnv sts ->
  -- | Maximum trace length that the signal generator of 's' can generate.
  Word64 ->
  -- | Lengths of the intervals in which the lengths range should be split.
  Word64 ->
  -- | Trace generation environment
  traceGenEnv ->
  QuickCheck.Property
traceLengthsAreClassified :: forall sts traceGenEnv.
(HasTrace sts traceGenEnv, Show (Environment sts)) =>
BaseEnv sts -> Word64 -> Word64 -> traceGenEnv -> Property
traceLengthsAreClassified BaseEnv sts
baseEnv Word64
maxTraceLength Word64
intervalSize traceGenEnv
traceGenEnv =
  forall sts traceGenEnv prop.
(HasTrace sts traceGenEnv, Testable prop,
 Show (Environment sts)) =>
BaseEnv sts
-> Word64 -> traceGenEnv -> (Trace sts -> prop) -> Property
forAllTrace @sts
    BaseEnv sts
baseEnv
    Word64
maxTraceLength
    traceGenEnv
traceGenEnv
    (forall s. Word64 -> Word64 -> Trace s -> Property
classifyTraceLength Word64
maxTraceLength Word64
intervalSize)

-- | Classify the trace length as either:
--
-- - being empty
-- - being a singleton
-- - having the given maximum size
-- - belonging to one of the intervals between 2 and the maximum size - 1. The
--   number of intervals are determined by the @step@ parameter.
classifyTraceLength ::
  -- | Maximum size of the traces
  Word64 ->
  -- | Steps used to divide the interval
  Word64 ->
  Trace s ->
  QuickCheck.Property
classifyTraceLength :: forall s. Word64 -> Word64 -> Trace s -> Property
classifyTraceLength Word64
maxTraceLength Word64
step Trace s
tr =
  forall n a.
(Show n, Integral n) =>
[Char] -> a -> (a -> n) -> n -> n -> Property
classifySize [Char]
"trace length:" Trace s
tr (forall a b. (Integral a, Num b) => a -> b
fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s. Trace s -> Int
Trace.traceLength) Word64
maxTraceLength Word64
step

-- | Classify the value size as either:
--
-- - being empty
-- - being a singleton
-- - having the given maximum size
-- - belonging to one of the intervals between 2 and the maximum size - 1. The
--   number of intervals are determined by the @step@ parameter.
classifySize ::
  (Show n, Integral n) =>
  -- | Prefix to be added to the label intervals
  String ->
  -- | Value to classify
  a ->
  -- | Size function
  (a -> n) ->
  -- | Maximum value size
  n ->
  -- | Steps used to divide the size interval
  n ->
  QuickCheck.Property
classifySize :: forall n a.
(Show n, Integral n) =>
[Char] -> a -> (a -> n) -> n -> n -> Property
classifySize [Char]
prefixLabel a
value a -> n
sizeF n
upBound n
step =
  forall prop. Testable prop => Bool -> [Char] -> prop -> Property
QuickCheck.classify (a -> n
sizeF a
value forall a. Eq a => a -> a -> Bool
== n
0) ([Char] -> [Char]
mkLabel [Char]
"empty") forall a b. (a -> b) -> a -> b
$
    forall prop. Testable prop => Bool -> [Char] -> prop -> Property
QuickCheck.classify (a -> n
sizeF a
value forall a. Eq a => a -> a -> Bool
== n
1) ([Char] -> [Char]
mkLabel [Char]
"singleton") forall a b. (a -> b) -> a -> b
$
      forall prop. Testable prop => Bool -> [Char] -> prop -> Property
QuickCheck.classify (a -> n
sizeF a
value forall a. Eq a => a -> a -> Bool
== n
upBound) [Char]
upBoundLabel forall a b. (a -> b) -> a -> b
$
        forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (n, n) -> Property -> Property
classifySizeInterval (forall prop. Testable prop => prop -> Property
QuickCheck.property Bool
True) (forall n. Integral n => n -> n -> n -> [(n, n)]
mkIntervals n
2 (n
upBound forall a. Num a => a -> a -> a
- n
1) n
step)
  where
    upBoundLabel :: [Char]
upBoundLabel = [Char] -> [Char]
mkLabel forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> [Char]
show n
upBound
    mkLabel :: [Char] -> [Char]
mkLabel = (([Char]
prefixLabel forall a. [a] -> [a] -> [a]
++ [Char]
" ") forall a. [a] -> [a] -> [a]
++)
    classifySizeInterval :: (n, n) -> Property -> Property
classifySizeInterval (n
low, n
high) Property
prop =
      forall prop. Testable prop => Bool -> [Char] -> prop -> Property
QuickCheck.classify (n
low forall a. Ord a => a -> a -> Bool
<= a -> n
sizeF a
value Bool -> Bool -> Bool
&& a -> n
sizeF a
value forall a. Ord a => a -> a -> Bool
< n
high) [Char]
desc Property
prop
      where
        desc :: [Char]
desc = [Char]
"[" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show n
low forall a. [a] -> [a] -> [a]
++ [Char]
", " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show n
high forall a. [a] -> [a] -> [a]
++ [Char]
")"

-- | Given a lower bound @low@,  an upper bound @high@ and a step size @step@
-- (both of which must be positive), divide the interval @[0, ub]@ into
-- sub-intervals of @step@ size.
--
-- If any of these values is negative the empty list will be returned.
--
-- Examples:
--
-- >>> mkIntervals 0 0 0 :: [(Int, Int)]
-- []
--
-- >>> mkIntervals 0 10 2 :: [(Int, Int)]
-- [(0,2),(2,4),(4,6),(6,8),(8,10)]
--
-- >>> mkIntervals 1 10 2 :: [(Int, Int)]
-- [(1,3),(3,5),(5,7),(7,9),(9,10)]
--
--
-- >>> mkIntervals 3 10 3 :: [(Int, Int)]
-- [(3,6),(6,9),(9,10)]
--
-- >>> mkIntervals 5 2 3 :: [(Int, Int)]
-- []
--
-- >>> mkIntervals (-1) 10 3 :: [(Int, Int)]
-- []
--
-- >>> mkIntervals 1 (-10) 3 :: [(Int, Int)]
-- []
--
-- >>> mkIntervals 1 1000 (-100) :: [(Int, Int)]
-- []
mkIntervals ::
  Integral n =>
  -- | Interval lower bound
  n ->
  -- | Interval upper bound
  n ->
  -- | Step size, used to divide the interval in sub-intervals of the same
  -- length.
  n ->
  [(n, n)]
mkIntervals :: forall n. Integral n => n -> n -> n -> [(n, n)]
mkIntervals n
low n
high n
step
  | n
0 forall a. Ord a => a -> a -> Bool
<= n
low Bool -> Bool -> Bool
&& n
low forall a. Ord a => a -> a -> Bool
<= n
high Bool -> Bool -> Bool
&& n
0 forall a. Ord a => a -> a -> Bool
< n
step =
      [(n
low forall a. Num a => a -> a -> a
+ n
i forall a. Num a => a -> a -> a
* n
step, n
high forall a. Ord a => a -> a -> a
`min` (n
low forall a. Num a => a -> a -> a
+ (n
i forall a. Num a => a -> a -> a
+ n
1) forall a. Num a => a -> a -> a
* n
step)) | n
i <- [n
0 .. n
n forall a. Num a => a -> a -> a
- n
1]]
  | Bool
otherwise = []
  where
    highNorm :: n
highNorm = n
high forall a. Num a => a -> a -> a
- n
low
    n :: n
n = n
highNorm forall a. Integral a => a -> a -> a
`div` n
step forall a. Num a => a -> a -> a
+ n
1 forall a. Ord a => a -> a -> a
`min` (n
highNorm forall a. Integral a => a -> a -> a
`mod` n
step)