module Test.Falsify.Internal.Generator.Shrinking (
    -- * Shrinking
    shrinkFrom
    -- * With full history
  , ShrinkExplanation(..)
  , ShrinkHistory(..)
  , IsValidShrink(..)
  , limitShrinkSteps
  , shrinkHistory
  , shrinkOutcome
  ) where

import Data.Bifunctor
import Data.Either
import Data.List.NonEmpty (NonEmpty((:|)))

import Test.Falsify.Internal.Generator.Definition
import Test.Falsify.Internal.SampleTree (SampleTree(..))

{-------------------------------------------------------------------------------
  Explanation
-------------------------------------------------------------------------------}

-- | Shrink explanation
--
-- @p@ is the type of \"positive\" elements that satisfied the predicate (i.e.,
-- valid shrinks), and @n@ is the type of \"negative\" which didn't.
data ShrinkExplanation p n = ShrinkExplanation {
      -- | The value we started, before shrinking
      forall p n. ShrinkExplanation p n -> p
initial :: p

      -- | The full shrink history
    , forall p n. ShrinkExplanation p n -> ShrinkHistory p n
history :: ShrinkHistory p n
    }
  deriving (Int -> ShrinkExplanation p n -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall p n.
(Show p, Show n) =>
Int -> ShrinkExplanation p n -> ShowS
forall p n. (Show p, Show n) => [ShrinkExplanation p n] -> ShowS
forall p n. (Show p, Show n) => ShrinkExplanation p n -> String
showList :: [ShrinkExplanation p n] -> ShowS
$cshowList :: forall p n. (Show p, Show n) => [ShrinkExplanation p n] -> ShowS
show :: ShrinkExplanation p n -> String
$cshow :: forall p n. (Show p, Show n) => ShrinkExplanation p n -> String
showsPrec :: Int -> ShrinkExplanation p n -> ShowS
$cshowsPrec :: forall p n.
(Show p, Show n) =>
Int -> ShrinkExplanation p n -> ShowS
Show)

-- | Shrink explanation
data ShrinkHistory p n =
    -- | We successfully executed a single shrink step
    ShrunkTo p (ShrinkHistory p n)

    -- | We could no shrink any further
    --
    -- We also record all rejected next steps. This is occasionally useful when
    -- trying to figure out why a value didn't shrink any further (what did it
    -- try to shrink to?)
  | ShrinkingDone [n]

    -- | We stopped shrinking early
    --
    -- This is used when the number of shrink steps is limited.
  | ShrinkingStopped
  deriving (Int -> ShrinkHistory p n -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall p n. (Show p, Show n) => Int -> ShrinkHistory p n -> ShowS
forall p n. (Show p, Show n) => [ShrinkHistory p n] -> ShowS
forall p n. (Show p, Show n) => ShrinkHistory p n -> String
showList :: [ShrinkHistory p n] -> ShowS
$cshowList :: forall p n. (Show p, Show n) => [ShrinkHistory p n] -> ShowS
show :: ShrinkHistory p n -> String
$cshow :: forall p n. (Show p, Show n) => ShrinkHistory p n -> String
showsPrec :: Int -> ShrinkHistory p n -> ShowS
$cshowsPrec :: forall p n. (Show p, Show n) => Int -> ShrinkHistory p n -> ShowS
Show)

limitShrinkSteps :: Maybe Word -> ShrinkExplanation p n -> ShrinkExplanation p n
limitShrinkSteps :: forall p n.
Maybe Word -> ShrinkExplanation p n -> ShrinkExplanation p n
limitShrinkSteps Maybe Word
Nothing      = forall a. a -> a
id
limitShrinkSteps (Just Word
limit) = \case
    ShrinkExplanation{p
initial :: p
initial :: forall p n. ShrinkExplanation p n -> p
initial, ShrinkHistory p n
history :: ShrinkHistory p n
history :: forall p n. ShrinkExplanation p n -> ShrinkHistory p n
history} ->
      ShrinkExplanation{
          p
initial :: p
initial :: p
initial
        , history :: ShrinkHistory p n
history = forall p n. Word -> ShrinkHistory p n -> ShrinkHistory p n
go Word
limit ShrinkHistory p n
history
        }
  where
    go :: Word -> ShrinkHistory p n -> ShrinkHistory p n
    go :: forall p n. Word -> ShrinkHistory p n -> ShrinkHistory p n
go Word
0 (ShrunkTo p
_ ShrinkHistory p n
_)      = forall p n. ShrinkHistory p n
ShrinkingStopped
    go Word
n (ShrunkTo p
x ShrinkHistory p n
xs)     = forall p n. p -> ShrinkHistory p n -> ShrinkHistory p n
ShrunkTo p
x (forall p n. Word -> ShrinkHistory p n -> ShrinkHistory p n
go (forall a. Enum a => a -> a
pred Word
n) ShrinkHistory p n
xs)
    go Word
_ (ShrinkingDone [n]
rej) = forall p n. [n] -> ShrinkHistory p n
ShrinkingDone [n]
rej
    go Word
_ ShrinkHistory p n
ShrinkingStopped    = forall p n. ShrinkHistory p n
ShrinkingStopped

-- | Simplify the shrink explanation to keep only the shrink history
shrinkHistory :: ShrinkExplanation p n -> NonEmpty p
shrinkHistory :: forall p n. ShrinkExplanation p n -> NonEmpty p
shrinkHistory = \(ShrinkExplanation p
unshrunk ShrinkHistory p n
shrunk) ->
    p
unshrunk forall a. a -> [a] -> NonEmpty a
:| forall p n. ShrinkHistory p n -> [p]
go ShrinkHistory p n
shrunk
  where
    go :: ShrinkHistory p n -> [p]
    go :: forall p n. ShrinkHistory p n -> [p]
go (ShrunkTo p
x ShrinkHistory p n
xs)   = p
x forall a. a -> [a] -> [a]
: forall p n. ShrinkHistory p n -> [p]
go ShrinkHistory p n
xs
    go (ShrinkingDone [n]
_) = []
    go ShrinkHistory p n
ShrinkingStopped  = []

-- | The final shrunk value, as well as all rejected /next/ shrunk steps
--
-- The list of rejected next steps is
--
-- * @Nothing@ if shrinking was terminated early ('limitShrinkSteps')
-- * @Just []@ if the final value truly is minimal (typically, it is only
--   minimal wrt to a particular properly, but not the minimal value that a
--   generator can produce).
shrinkOutcome :: forall p n. ShrinkExplanation p n -> (p, Maybe [n])
shrinkOutcome :: forall p n. ShrinkExplanation p n -> (p, Maybe [n])
shrinkOutcome = \ShrinkExplanation{p
initial :: p
initial :: forall p n. ShrinkExplanation p n -> p
initial, ShrinkHistory p n
history :: ShrinkHistory p n
history :: forall p n. ShrinkExplanation p n -> ShrinkHistory p n
history} ->
    p -> ShrinkHistory p n -> (p, Maybe [n])
go p
initial ShrinkHistory p n
history
  where
    go :: p -> ShrinkHistory p n -> (p, Maybe [n])
    go :: p -> ShrinkHistory p n -> (p, Maybe [n])
go p
_ (ShrunkTo p
p ShrinkHistory p n
h)     = p -> ShrinkHistory p n -> (p, Maybe [n])
go p
p ShrinkHistory p n
h
    go p
p (ShrinkingDone [n]
ns) = (p
p, forall a. a -> Maybe a
Just [n]
ns)
    go p
p  ShrinkHistory p n
ShrinkingStopped  = (p
p, forall a. Maybe a
Nothing)

{-------------------------------------------------------------------------------
  Mapping
-------------------------------------------------------------------------------}

instance Functor (ShrinkExplanation p) where
  fmap :: forall a b.
(a -> b) -> ShrinkExplanation p a -> ShrinkExplanation p b
fmap = forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second

instance Functor (ShrinkHistory p) where
  fmap :: forall a b. (a -> b) -> ShrinkHistory p a -> ShrinkHistory p b
fmap = forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second

instance Bifunctor ShrinkExplanation where
  bimap :: forall a b c d.
(a -> b)
-> (c -> d) -> ShrinkExplanation a c -> ShrinkExplanation b d
bimap a -> b
f c -> d
g ShrinkExplanation{a
initial :: a
initial :: forall p n. ShrinkExplanation p n -> p
initial, ShrinkHistory a c
history :: ShrinkHistory a c
history :: forall p n. ShrinkExplanation p n -> ShrinkHistory p n
history} = ShrinkExplanation{
        initial :: b
initial = a -> b
f a
initial
      , history :: ShrinkHistory b d
history = forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap a -> b
f c -> d
g ShrinkHistory a c
history
      }

instance Bifunctor ShrinkHistory where
  bimap :: forall a b c d.
(a -> b) -> (c -> d) -> ShrinkHistory a c -> ShrinkHistory b d
bimap a -> b
f c -> d
g = \case
      ShrunkTo a
truncated ShrinkHistory a c
history ->
        forall p n. p -> ShrinkHistory p n -> ShrinkHistory p n
ShrunkTo (a -> b
f a
truncated) (forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap a -> b
f c -> d
g ShrinkHistory a c
history)
      ShrinkingDone [c]
rejected ->
        forall p n. [n] -> ShrinkHistory p n
ShrinkingDone (forall a b. (a -> b) -> [a] -> [b]
map c -> d
g [c]
rejected)
      ShrinkHistory a c
ShrinkingStopped ->
        forall p n. ShrinkHistory p n
ShrinkingStopped

{-------------------------------------------------------------------------------
  Shrinking
-------------------------------------------------------------------------------}

-- | Does a given shrunk value represent a valid shrink step?
data IsValidShrink p n =
    ValidShrink p
  | InvalidShrink n
  deriving stock (Int -> IsValidShrink p n -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall p n. (Show p, Show n) => Int -> IsValidShrink p n -> ShowS
forall p n. (Show p, Show n) => [IsValidShrink p n] -> ShowS
forall p n. (Show p, Show n) => IsValidShrink p n -> String
showList :: [IsValidShrink p n] -> ShowS
$cshowList :: forall p n. (Show p, Show n) => [IsValidShrink p n] -> ShowS
show :: IsValidShrink p n -> String
$cshow :: forall p n. (Show p, Show n) => IsValidShrink p n -> String
showsPrec :: Int -> IsValidShrink p n -> ShowS
$cshowsPrec :: forall p n. (Show p, Show n) => Int -> IsValidShrink p n -> ShowS
Show)

-- | Find smallest value that the generator can produce and still satisfies
-- the predicate.
--
-- Returns the full shrink history.
--
-- To avoid boolean blindness, we use different types for values that satisfy
-- the property and values that do not.
--
-- This is lazy in the shrink history; see 'limitShrinkSteps' to limit the
-- number of shrinking steps.
shrinkFrom :: forall a p n.
     (a -> IsValidShrink p n)
  -> Gen a
  -> (p, [SampleTree]) -- ^ Initial result of the generator
  -> ShrinkExplanation p n
shrinkFrom :: forall a p n.
(a -> IsValidShrink p n)
-> Gen a -> (p, [SampleTree]) -> ShrinkExplanation p n
shrinkFrom a -> IsValidShrink p n
prop Gen a
gen = \(p
p, [SampleTree]
shrunk) ->
    forall p n. p -> ShrinkHistory p n -> ShrinkExplanation p n
ShrinkExplanation p
p forall a b. (a -> b) -> a -> b
$ [SampleTree] -> ShrinkHistory p n
go [SampleTree]
shrunk
  where
    go :: [SampleTree] -> ShrinkHistory p n
    go :: [SampleTree] -> ShrinkHistory p n
go [SampleTree]
shrunk =
        -- Shrinking is a greedy algorithm: we go with the first candidate that
        -- works, and discard the others.
        --
        -- NOTE: 'partitionEithers' is lazy enough:
        --
        -- > head . fst $ partitionEithers [Left True, undefined] == True
        case forall a b. [Either a b] -> ([a], [b])
partitionEithers [Either (p, [SampleTree]) n]
candidates of
          ([], [n]
rejected)      -> forall p n. [n] -> ShrinkHistory p n
ShrinkingDone [n]
rejected
          ((p
p, [SampleTree]
shrunk'):[(p, [SampleTree])]
_, [n]
_) -> forall p n. p -> ShrinkHistory p n -> ShrinkHistory p n
ShrunkTo p
p forall a b. (a -> b) -> a -> b
$ [SampleTree] -> ShrinkHistory p n
go [SampleTree]
shrunk'
      where
        candidates :: [Either (p, [SampleTree]) n]
        candidates :: [Either (p, [SampleTree]) n]
candidates = forall a b. (a -> b) -> [a] -> [b]
map (a, [SampleTree]) -> Either (p, [SampleTree]) n
consider forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. Gen a -> SampleTree -> (a, [SampleTree])
runGen Gen a
gen) [SampleTree]
shrunk

    consider :: (a, [SampleTree]) -> Either (p, [SampleTree]) n
    consider :: (a, [SampleTree]) -> Either (p, [SampleTree]) n
consider (a
a, [SampleTree]
shrunk) =
        case a -> IsValidShrink p n
prop a
a of
          ValidShrink p
p   -> forall a b. a -> Either a b
Left (p
p, [SampleTree]
shrunk)
          InvalidShrink n
n -> forall a b. b -> Either a b
Right n
n