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

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

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

import qualified Test.Falsify.Context as Context

{-------------------------------------------------------------------------------
  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
[ShrinkExplanation p n] -> ShowS
ShrinkExplanation p n -> String
(Int -> ShrinkExplanation p n -> ShowS)
-> (ShrinkExplanation p n -> String)
-> ([ShrinkExplanation p n] -> ShowS)
-> Show (ShrinkExplanation p n)
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
$cshowsPrec :: forall p n.
(Show p, Show n) =>
Int -> ShrinkExplanation p n -> ShowS
showsPrec :: Int -> ShrinkExplanation p n -> ShowS
$cshow :: forall p n. (Show p, Show n) => ShrinkExplanation p n -> String
show :: ShrinkExplanation p n -> String
$cshowList :: forall p n. (Show p, Show n) => [ShrinkExplanation p n] -> ShowS
showList :: [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 record
    --
    -- * All rejected next steps
    -- * The outcome of the repeated 'Context.Final' step
    --
    -- Recording the rejected next steps 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] p

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

-- | 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 p -> [p] -> NonEmpty p
forall a. a -> [a] -> NonEmpty a
:| ShrinkHistory p n -> [p]
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 p -> [p] -> [p]
forall a. a -> [a] -> [a]
: ShrinkHistory p n -> [p]
forall p n. ShrinkHistory p n -> [p]
go ShrinkHistory p n
xs
    go (ShrinkingDone [n]
_ns p
p) = [p
p]
    go (ShrinkingStopped  p
p) = [p
p]

-- | 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 (e.g. 'Context.maxShrinks')
-- * @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{ShrinkHistory p n
history :: forall p n. ShrinkExplanation p n -> ShrinkHistory p n
history :: ShrinkHistory p n
history} ->
    ShrinkHistory p n -> (p, Maybe [n])
go ShrinkHistory p n
history
  where
    go :: ShrinkHistory p n -> (p, Maybe [n])
    go :: ShrinkHistory p n -> (p, Maybe [n])
go (ShrunkTo p
_p ShrinkHistory p n
h)      = ShrinkHistory p n -> (p, Maybe [n])
go ShrinkHistory p n
h
    go (ShrinkingDone [n]
ns p
p) = (p
p, [n] -> Maybe [n]
forall a. a -> Maybe a
Just [n]
ns)
    go (ShrinkingStopped p
p) = (p
p, Maybe [n]
forall a. Maybe a
Nothing)

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

instance Functor (ShrinkExplanation p) where
  fmap :: forall a b.
(a -> b) -> ShrinkExplanation p a -> ShrinkExplanation p b
fmap = (a -> b) -> ShrinkExplanation p a -> ShrinkExplanation p b
forall b c a.
(b -> c) -> ShrinkExplanation a b -> ShrinkExplanation a c
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 = (a -> b) -> ShrinkHistory p a -> ShrinkHistory p b
forall b c a. (b -> c) -> ShrinkHistory a b -> ShrinkHistory a c
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 :: forall p n. ShrinkExplanation p n -> p
initial :: a
initial, ShrinkHistory a c
history :: forall p n. ShrinkExplanation p n -> ShrinkHistory p n
history :: ShrinkHistory a c
history} = ShrinkExplanation{
        initial :: b
initial = a -> b
f a
initial
      , history :: ShrinkHistory b d
history = (a -> b) -> (c -> d) -> ShrinkHistory a c -> ShrinkHistory b d
forall a b c d.
(a -> b) -> (c -> d) -> ShrinkHistory a c -> ShrinkHistory b d
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
p ShrinkHistory a c
h -> b -> ShrinkHistory b d -> ShrinkHistory b d
forall p n. p -> ShrinkHistory p n -> ShrinkHistory p n
ShrunkTo                 (a -> b
f a
p) ((a -> b) -> (c -> d) -> ShrinkHistory a c -> ShrinkHistory b d
forall a b c d.
(a -> b) -> (c -> d) -> ShrinkHistory a c -> ShrinkHistory b d
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
h)
      ShrinkingDone [c]
ns a
p   -> [d] -> b -> ShrinkHistory b d
forall p n. [n] -> p -> ShrinkHistory p n
ShrinkingDone ((c -> d) -> [c] -> [d]
forall a b. (a -> b) -> [a] -> [b]
map c -> d
g [c]
ns) (a -> b
f a
p)
      ShrinkingStopped a
p   -> b -> ShrinkHistory b d
forall p n. p -> ShrinkHistory p n
ShrinkingStopped         (a -> b
f a
p)

{-------------------------------------------------------------------------------
  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
[IsValidShrink p n] -> ShowS
IsValidShrink p n -> String
(Int -> IsValidShrink p n -> ShowS)
-> (IsValidShrink p n -> String)
-> ([IsValidShrink p n] -> ShowS)
-> Show (IsValidShrink p n)
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
$cshowsPrec :: forall p n. (Show p, Show n) => Int -> IsValidShrink p n -> ShowS
showsPrec :: Int -> IsValidShrink p n -> ShowS
$cshow :: forall p n. (Show p, Show n) => IsValidShrink p n -> String
show :: IsValidShrink p n -> String
$cshowList :: forall p n. (Show p, Show n) => [IsValidShrink p n] -> ShowS
showList :: [IsValidShrink p n] -> ShowS
Show)

isValidShrink :: IsValidShrink p n -> Either n p
isValidShrink :: forall p n. IsValidShrink p n -> Either n p
isValidShrink (ValidShrink p
p)   = p -> Either n p
forall a b. b -> Either a b
Right p
p
isValidShrink (InvalidShrink n
n) = n -> Either n p
forall a b. a -> Either a b
Left n
n

-- | 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.
shrinkFrom :: forall p n.
     Context.Static
     -- ^ Static context
     --
     -- Passed as-is to the property as part of the t'Context'.
     -- Used to extract shrinking parameters.
  -> Context.Iteration
     -- ^ Iteration context
     --
     -- Passsed as-is to the property as part of the t'Context'.
     -- Not used otherwise.
  -> (Context -> Gen (IsValidShrink p n))
     -- ^ The property we're shrinking
  -> SampleTree
     -- ^ The sample tree we started with
  -> (p, [SampleTree])
     -- ^ The initial result of the generator
  -> ShrinkExplanation p n
shrinkFrom :: forall p n.
Static
-> Iteration
-> (Context -> Gen (IsValidShrink p n))
-> SampleTree
-> (p, [SampleTree])
-> ShrinkExplanation p n
shrinkFrom Static
static Iteration
iteration Context -> Gen (IsValidShrink p n)
prop = \SampleTree
st (p
p, [SampleTree]
shrunk) ->
    p -> ShrinkHistory p n -> ShrinkExplanation p n
forall p n. p -> ShrinkHistory p n -> ShrinkExplanation p n
ShrinkExplanation p
p (ShrinkHistory p n -> ShrinkExplanation p n)
-> ShrinkHistory p n -> ShrinkExplanation p n
forall a b. (a -> b) -> a -> b
$ Word -> SampleTree -> [SampleTree] -> ShrinkHistory p n
go Word
0 SampleTree
st [SampleTree]
shrunk
  where
    go :: Word -> SampleTree -> [SampleTree] -> ShrinkHistory p n
    go :: Word -> SampleTree -> [SampleTree] -> ShrinkHistory p n
go Word
i = \SampleTree
st [SampleTree]
shrunk ->
        -- NOTE: 'partitionEithers' is lazy enough:
        --
        -- > head . fst $ partitionEithers [Left True, undefined] == True
        let candidates :: [(SampleTree, p, [SampleTree])]
            rejected   :: [n]
            ([(SampleTree, p, [SampleTree])]
candidates, [n]
rejected) = [Either (SampleTree, p, [SampleTree]) n]
-> ([(SampleTree, p, [SampleTree])], [n])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ([Either (SampleTree, p, [SampleTree]) n]
 -> ([(SampleTree, p, [SampleTree])], [n]))
-> [Either (SampleTree, p, [SampleTree]) n]
-> ([(SampleTree, p, [SampleTree])], [n])
forall a b. (a -> b) -> a -> b
$ (SampleTree -> Either (SampleTree, p, [SampleTree]) n)
-> [SampleTree] -> [Either (SampleTree, p, [SampleTree]) n]
forall a b. (a -> b) -> [a] -> [b]
map SampleTree -> Either (SampleTree, p, [SampleTree]) n
consider [SampleTree]
shrunk

         in case [(SampleTree, p, [SampleTree])]
candidates of
              [] ->
                [n] -> p -> ShrinkHistory p n
forall p n. [n] -> p -> ShrinkHistory p n
ShrinkingDone [n]
rejected (p -> ShrinkHistory p n) -> p -> ShrinkHistory p n
forall a b. (a -> b) -> a -> b
$ Word -> SampleTree -> p
runFinal Word
i SampleTree
st
              (SampleTree
st', p
p, [SampleTree]
shrunk'):[(SampleTree, p, [SampleTree])]
_ | Bool
canContinue ->
                p -> ShrinkHistory p n -> ShrinkHistory p n
forall p n. p -> ShrinkHistory p n -> ShrinkHistory p n
ShrunkTo p
p (ShrinkHistory p n -> ShrinkHistory p n)
-> ShrinkHistory p n -> ShrinkHistory p n
forall a b. (a -> b) -> a -> b
$ Word -> SampleTree -> [SampleTree] -> ShrinkHistory p n
go (Word -> Word
forall a. Enum a => a -> a
succ Word
i) SampleTree
st' [SampleTree]
shrunk'
              [(SampleTree, p, [SampleTree])]
_otherwise ->
                p -> ShrinkHistory p n
forall p n. p -> ShrinkHistory p n
ShrinkingStopped (p -> ShrinkHistory p n) -> p -> ShrinkHistory p n
forall a b. (a -> b) -> a -> b
$ Word -> SampleTree -> p
runFinal Word
i SampleTree
st
      where
        ctx :: Context
        ctx :: Context
ctx = Static -> Iteration -> Execution -> Context
Context Static
static Iteration
iteration (Execution -> Context) -> Execution -> Context
forall a b. (a -> b) -> a -> b
$ Word -> Execution
Context.Shrinking Word
i

        canContinue :: Bool
        canContinue :: Bool
canContinue =
             Bool -> (Word -> Bool) -> Maybe Word -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
               Bool
True
               (\Word
limit -> Word
i Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
< Word
limit)
               (Static -> Maybe Word
Context.maxShrinks Static
static)

        consider :: SampleTree -> Either (SampleTree, p, [SampleTree]) n
        consider :: SampleTree -> Either (SampleTree, p, [SampleTree]) n
consider SampleTree
st =
            case IsValidShrink p n
isValid of
              ValidShrink p
p   -> (SampleTree, p, [SampleTree])
-> Either (SampleTree, p, [SampleTree]) n
forall a b. a -> Either a b
Left (SampleTree
st, p
p, [SampleTree]
shrunk')
              InvalidShrink n
n -> n -> Either (SampleTree, p, [SampleTree]) n
forall a b. b -> Either a b
Right n
n
          where
            isValid :: IsValidShrink p n
            shrunk' :: [SampleTree]
            (IsValidShrink p n
isValid, [SampleTree]
shrunk') = Gen (IsValidShrink p n)
-> SampleTree -> (IsValidShrink p n, [SampleTree])
forall a. Gen a -> SampleTree -> (a, [SampleTree])
runGen (Context -> Gen (IsValidShrink p n)
prop Context
ctx) SampleTree
st

    -- Run the property one final time
    --
    -- Precondition: must be run on a sample tree for which we know the
    -- property fails.
    runFinal :: Word -> SampleTree -> p
    runFinal :: Word -> SampleTree -> p
runFinal Word
i SampleTree
st =
        case (IsValidShrink p n, [SampleTree]) -> IsValidShrink p n
forall a b. (a, b) -> a
fst ((IsValidShrink p n, [SampleTree]) -> IsValidShrink p n)
-> (IsValidShrink p n, [SampleTree]) -> IsValidShrink p n
forall a b. (a -> b) -> a -> b
$ Gen (IsValidShrink p n)
-> SampleTree -> (IsValidShrink p n, [SampleTree])
forall a. Gen a -> SampleTree -> (a, [SampleTree])
runGen (Context -> Gen (IsValidShrink p n)
prop Context
ctx) SampleTree
st of
          ValidShrink   p
p -> p
p
          InvalidShrink n
_ -> String -> p
forall a. HasCallStack => String -> a
error String
"runFinal: precondition violated"
      where
        ctx :: Context
        ctx :: Context
ctx = Static -> Iteration -> Execution -> Context
Context Static
static Iteration
iteration (Execution -> Context) -> Execution -> Context
forall a b. (a -> b) -> a -> b
$ Word -> Execution
Context.Final Word
i