content: {-# LANGUAGE DerivingStrategies #-}
  {-# LANGUAGE GeneralizedNewtypeDeriving #-}
  {-# LANGUAGE NegativeLiterals #-}
  {-# LANGUAGE PatternSynonyms #-}
  {-# LANGUAGE TypeApplications #-}
  
  module Test.Proto.Interval (testTree) where
  
  import Data.Foldable (for_)
  
  import Proto3.Suite.DotProto.Internal (joinIntervals, normalizeIntervals)
  
  import Hedgehog (Gen, forAll, property, (===))
  import Hedgehog qualified
  import Hedgehog.Gen qualified as Gen
  import Hedgehog.Range qualified as Range
  
  import Test.Tasty (TestTree, testGroup)
  import Test.Tasty.Hedgehog (testProperty)
  
  --------------------------------------------------------------------------------
  
  -- | Check if the given value is some given bounds (inclusive).
  isIn :: (Ord a) => a -> (a, a) -> Bool
  isIn x (a, b) = a <= x && x <= b
  
  -- | Check if the given value is any of the given bounds (inclusive).
  isInAnyOf :: (Ord a) => a -> [(a, a)] -> Bool
  isInAnyOf = any . isIn
  
  -- | Generates an arbitrary interval.  May generate
  -- empty intervals, though at about 10% probability.
  genInterval :: (Bounded a, Integral a) => Gen (a, a)
  genInterval = Gen.frequency [(4, alwaysNonempty), (1, halfEmpty)]
    where
      alwaysNonempty = do
        x <- Gen.integral Range.constantBounded
        y <- Gen.integral Range.constantBounded
        pure (min x y, max x y)
  
      halfEmpty = do
        x <- Gen.integral Range.constantBounded
        y <- Gen.integral Range.constantBounded
        pure (x, y)
  
  -- | A value in the range [-8 .. 7].  We intentionally limit this type to
  -- just a few values in order to increase the chance of overlapping intervals
  -- in some tests, while still retaining enough distinct values to allow many
  -- different relationships between intervals.  We also want to check for
  -- arithmetic overflow in the code under test by throwing an exception,
  -- which should cause the test to fail.
  newtype Nybble = UnsafeNybble Int
    deriving newtype (Eq, Ord, Real, Show)
  
  {-# COMPLETE Nybble #-}
  
  pattern Nybble :: Int -> Nybble
  pattern Nybble x <- UnsafeNybble x
    where
      Nybble x
        | -8 <= x && x <= 7 = UnsafeNybble x
        | otherwise = error $ "Nybble out of bounds: " ++ show x
  
  instance Bounded Nybble
    where
      minBound = Nybble -8
      maxBound = Nybble 7
  
  -- | Manual implementation to ensure an exception is thrown for out-of-bounds values.
  instance Enum Nybble
    where
      toEnum x = Nybble x
      fromEnum (Nybble x) = x
  
  -- | Manual implementation to ensure an exception is thrown for arithmetic overflow.
  instance Num Nybble
    where
      Nybble x + Nybble y = Nybble (x + y)
      Nybble x - Nybble y = Nybble (x - y)
      Nybble x * Nybble y = Nybble (x * y)
      negate (Nybble x) = Nybble (negate x)
      abs (Nybble x) = Nybble (abs x)
      signum (Nybble x) = Nybble (signum x)
      fromInteger x = Nybble (fromInteger x)
  
  -- | Manual implementation to ensure an exception is thrown for arithmetic overflow.
  instance Integral Nybble
    where
      quotRem (Nybble n) (Nybble d) = let (q, r) = quotRem n d in (Nybble q, Nybble r)
      toInteger (Nybble x) = toInteger x
  
  --------------------------------------------------------------------------------
  
  testTree :: TestTree
  testTree =
    testGroup
      "Test.Proto.Interval"
      [ testJoinIntervals
      , testNormalizeIntervals
      ]
  
  -- This test verifies the documented behavior of 'joinIntervals'.
  testJoinIntervals :: TestTree
  testJoinIntervals = testProperty "joinIntervals" $ property do
    (a, b) <- forAll $ genInterval @Nybble
    (c, d) <- forAll $ genInterval @Nybble
    case joinIntervals (a, b) (c, d) of
      Nothing -> do
        -- The code under test says that one cannot merge the two intervals into
        -- a single interval.  For that to be true, both intervals must be nonempty/valid:
        Hedgehog.assert (a <= b)
        Hedgehog.assert (c <= d)
        -- And in addition, the least interval containing both of the given intervals
        -- must /not/ be their union.  Namely, it must include some extra element:
        let extra x = not (x `isIn` (a, b) || x `isIn` (c, d))
        Hedgehog.assert (any extra [min a c .. max b d])
        -- That suffices to verify that the intervals cannot be combined, but because
        -- the code under test currently considers similar issues, we note that there
        -- must be at least one value strictly between the two given intervals;
        -- otherwise we could merge them because there would be nothing between them:
        let between x = (b < x && x < c) || (d < x && x < a)
        Hedgehog.assert (any between [minBound .. maxBound])
      Just combined -> do
        -- The code under test claims that 'combined' equals the union of the given
        -- intervals.  We check that conclusion by testing every possible element:
        Hedgehog.annotateShow combined
        for_ [minBound .. maxBound] \x -> do
          x `isIn` combined === (x `isIn` (a, b) || x `isIn` (c, d))
  
  -- This test verifies the documented behavior of 'normalizeIntervals'.
  -- (Note the correspondence between the various documented properties
  -- and the specific checks included here.)
  --
  -- This test also checks an additional property: that 'normalizeIntervals'
  -- never increases the sum of the sizes of the listed intervals, where by
  -- "size" we mean the count of elements within the interval.  That is, we
  -- are only eliminating redundancy in the
  testNormalizeIntervals :: TestTree
  testNormalizeIntervals = testProperty "normalizeIntervals" $ property do
    messy <- forAll $ Gen.list (Range.linear 0 20) $ genInterval @Nybble
  
    let clean :: [(Nybble, Nybble)]
        clean = normalizeIntervals messy
    Hedgehog.annotateShow clean
  
    -- The result must not contain any empty intervals.
    for_ clean \(a, b) ->
      Hedgehog.assert (a <= b)
  
    -- The union of the result must be the same as the union of the input.
    for_ [minBound .. maxBound] \x -> do
      (x, isInAnyOf x clean) === (x, isInAnyOf x messy)
  
    -- Check that the listed intervals do not overlap, and moreover,
    -- cannot be merged because there are no values between them.
    --
    -- Note that here we rely upon the accuracy of 'joinIntervals',
    -- which is checked in isolation by the test 'testJoinIntervals'.
    for_ (zip [1 ..] clean) \(d, i1) ->
      for_ (drop d clean) \i2 -> do
        (i1, i2, joinIntervals i1 i2) === (i1, i2, Nothing)
  
    -- The code under test should have ensured that for any two consecutive intervals,
    -- there is at least one value strictly inbetween those two intervals.  This check
    -- should subsume the previous one, but we run both checks just to be sure.
    --
    -- The nonempty gaps between intervals prevent further merging, making 'clean'
    -- at least locally minimal.  But a simple exhaustive search would be extremely
    -- expensive, and hence we rely upon the mathematical argument in the comments for
    -- 'normalizeIntervals' to completely rule out the possibility of shorter lists.
    for_ (zip clean (drop 1 clean)) \((_, b), (c, _)) ->
      Hedgehog.assert (b < c && succ b < c)  -- The first check is to sure that 'succ' is safe.
  
    -- Verify interval merging by checking that the size of the merged intervals is
    -- bounded below the sum of the sizes of each individual interval that was merged.
    let intervalSize :: (Nybble, Nybble) -> Integer
        intervalSize (a, b) = if a <= b then toInteger b + 1 - toInteger a else 0
        overallSize :: [(Nybble, Nybble)] -> Integer
        overallSize = sum . map intervalSize
    Hedgehog.annotateShow (overallSize clean, overallSize messy)
    Hedgehog.assert (overallSize clean <= overallSize messy)
  