content: {-# LANGUAGE CPP #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeApplications #-}
  {-# LANGUAGE TypeOperators #-}
  
  
  module Test.FinMap (finMapTests) where
  
  import           Control.Monad (foldM)
  import           Data.Foldable.WithIndex (itoList)
  import           Data.Functor.WithIndex (FunctorWithIndex(imap))
  import           Data.Foldable.WithIndex (FoldableWithIndex(ifoldMap))
  import           Data.Proxy (Proxy(Proxy))
  import           Data.Type.Equality ((:~:)(Refl))
  
  import           Data.Parameterized.Fin (Fin)
  import qualified Data.Parameterized.Fin as Fin
  import           Data.Parameterized.NatRepr (LeqProof, NatRepr, type (<=), type (+))
  import qualified Data.Parameterized.NatRepr as NatRepr
  
  import           Hedgehog
  import qualified Hedgehog.Gen as HG
  import           Hedgehog.Range (linear)
  import           Test.Tasty
  import           Test.Tasty.Hedgehog
  
  #if __GLASGOW_HASKELL__ >= 806
  import           Test.Tasty.HUnit (assertBool, testCase)
  import qualified Hedgehog.Classes as HC
  #endif
  
  import qualified Data.Parameterized.FinMap.Safe as S
  import qualified Data.Parameterized.FinMap.Unsafe as U
  import qualified Data.Parameterized.Vector as Vec
  
  import           Test.Fin (genFin)
  import           Test.Vector (SomeVector(..), genSomeVector, genVectorOfLength, genOrdering, orderingEndomorphisms, orderingToStringFuns)
  
  data SomeSafeFinMap a = forall n. SomeSafeFinMap (NatRepr n) (S.FinMap n a)
  data SomeUnsafeFinMap a = forall n. SomeUnsafeFinMap (NatRepr n) (U.FinMap n a)
  
  instance Show a => Show (SomeSafeFinMap a) where
    show (SomeSafeFinMap _ v) = show v
  instance Show a => Show (SomeUnsafeFinMap a) where
    show (SomeUnsafeFinMap _ v) = show v
  
  genSafeFinMap :: (Monad m) => NatRepr n -> GenT m a -> GenT m (S.FinMap (n + 1) a)
  genSafeFinMap n genElem = S.fromVector <$> genVectorOfLength n (HG.maybe genElem)
  
  genUnsafeFinMap :: (Monad m) => NatRepr n -> GenT m a -> GenT m (U.FinMap (n + 1) a)
  genUnsafeFinMap n genElem = U.fromVector <$> genVectorOfLength n (HG.maybe genElem)
  
  genSomeSafeFinMap :: (Monad m) => GenT m a -> GenT m (SomeSafeFinMap a)
  genSomeSafeFinMap genElem =
    do SomeVector v <- genSomeVector (HG.maybe genElem)
       return (SomeSafeFinMap (Vec.length v) (S.fromVector v))
  
  genSomeUnsafeFinMap :: (Monad m) => GenT m a -> GenT m (SomeUnsafeFinMap a)
  genSomeUnsafeFinMap genElem =
    do SomeVector v <- genSomeVector (HG.maybe genElem)
       return (SomeUnsafeFinMap (Vec.length v) (U.fromVector v))
  
  prop_incMax_size_safe :: Property
  prop_incMax_size_safe = property $
    do SomeSafeFinMap _ fm <- forAll $ genSomeSafeFinMap genOrdering
       Fin.finToNat (S.size (S.incMax fm)) === Fin.finToNat (S.size fm)
  
  prop_incMax_size_unsafe :: Property
  prop_incMax_size_unsafe = property $
    do SomeUnsafeFinMap _ fm <- forAll $ genSomeUnsafeFinMap genOrdering
       Fin.finToNat (U.size (U.incMax fm)) === Fin.finToNat (U.size fm)
  
  prop_imap_const_safe :: Property
  prop_imap_const_safe = property $
    do f <- forAll (HG.element orderingEndomorphisms)
       SomeSafeFinMap _ fm <- forAll (genSomeSafeFinMap genOrdering)
       imap (const f) fm === fmap f fm
  
  prop_imap_const_unsafe :: Property
  prop_imap_const_unsafe = property $
    do f <- forAll (HG.element orderingEndomorphisms)
       SomeUnsafeFinMap _ fm <- forAll (genSomeUnsafeFinMap genOrdering)
       imap (const f) fm === fmap f fm
  
  prop_ifoldMap_const_safe :: Property
  prop_ifoldMap_const_safe = property $
    do f <- forAll (HG.element orderingToStringFuns)
       SomeSafeFinMap _ fm <- forAll (genSomeSafeFinMap genOrdering)
       ifoldMap (const f) fm === foldMap f fm
  
  prop_ifoldMap_const_unsafe :: Property
  prop_ifoldMap_const_unsafe = property $
    do f <- forAll (HG.element orderingToStringFuns)
       SomeUnsafeFinMap _ fm <- forAll (genSomeUnsafeFinMap genOrdering)
       ifoldMap (const f) fm === foldMap f fm
  
  cancelPlusOne ::
    forall f g i n.
    f i ->
    g n ->
    LeqProof (i + 1) (n + 1) ->
    LeqProof i n
  cancelPlusOne i n NatRepr.LeqProof =
    case NatRepr.plusMinusCancel n (NatRepr.knownNat :: NatRepr 1) of
      Refl ->
        case NatRepr.plusMinusCancel i (NatRepr.knownNat :: NatRepr 1) of
          Refl ->
            case NatRepr.leqSub2
                    (NatRepr.LeqProof :: LeqProof (i + 1) (n + 1))
                    (NatRepr.LeqProof :: LeqProof 1 1) of
              NatRepr.LeqProof -> NatRepr.LeqProof
  
  withIndexSafe ::
    SomeSafeFinMap a ->
    (forall n. Fin n -> S.FinMap n a -> PropertyT IO ()) ->
    PropertyT IO ()
  withIndexSafe (SomeSafeFinMap n fm) k =
    case NatRepr.isZeroOrGT1 n of
      Left Refl -> k Fin.minFin (S.incMax fm)
      Right NatRepr.LeqProof ->
        do idx <- forAll (genFin n)
           k idx fm
  
  withIndexUnsafe ::
    SomeUnsafeFinMap a ->
    (forall n. Fin n -> U.FinMap n a -> PropertyT IO ()) ->
    PropertyT IO ()
  withIndexUnsafe (SomeUnsafeFinMap n fm) k =
    case NatRepr.isZeroOrGT1 n of
      Left Refl -> k Fin.minFin (U.incMax fm)
      Right NatRepr.LeqProof ->
        do idx <- forAll (genFin n)
           k idx fm
  
  withSizeUnsafe ::
    U.FinMap n a ->
    (forall i. (i + 1 <= n + 1, i <= n) => NatRepr i -> r) ->
    r
  withSizeUnsafe fm k =
    case U.size fm of
      (sz :: Fin (n + 1)) ->
        Fin.viewFin
          (\(i :: NatRepr i) ->
            case cancelPlusOne i (Proxy :: Proxy n) NatRepr.LeqProof of
              NatRepr.LeqProof -> k i)
          sz
  
  prop_insert_size_safe :: Property
  prop_insert_size_safe = property $
    do sfm <- forAll $ genSomeSafeFinMap genOrdering
       withIndexSafe sfm $ \idx fm -> do
        o <- forAll genOrdering
        let size = Fin.finToNat (S.size fm)
        let newSize = Fin.finToNat (S.size (S.insert (Fin.embed idx) o fm))
        assert (size == newSize || size + 1 == newSize)
  
  prop_insert_size_unsafe :: Property
  prop_insert_size_unsafe = property $
    do sfm <- forAll $ genSomeUnsafeFinMap genOrdering
       withIndexUnsafe sfm $ \idx fm -> do
        o <- forAll genOrdering
        let size = Fin.finToNat (U.size fm)
        let newSize = Fin.finToNat (U.size (U.insert (Fin.embed idx) o fm))
        assert (size == newSize || size + 1 == newSize)
  
  prop_insert_delete_safe :: Property
  prop_insert_delete_safe = property $
    do sfm <- forAll $ genSomeSafeFinMap genOrdering
       withIndexSafe sfm $ \idx fm -> do
        o <- forAll genOrdering
        S.delete idx (S.insert idx o fm) === S.delete idx fm
  
  prop_insert_delete_unsafe :: Property
  prop_insert_delete_unsafe = property $
    do sfm <- forAll $ genSomeUnsafeFinMap genOrdering
       withIndexUnsafe sfm $ \idx fm -> do
        o <- forAll genOrdering
        U.delete idx (U.insert idx o fm) === U.delete idx fm
  
  prop_delete_insert_safe :: Property
  prop_delete_insert_safe = property $
    do sfm <- forAll $ genSomeSafeFinMap genOrdering
       withIndexSafe sfm $ \idx fm -> do
        o <- forAll genOrdering
        S.insert idx o (S.delete idx fm) === S.insert idx o fm
  
  prop_delete_insert_unsafe :: Property
  prop_delete_insert_unsafe = property $
    do sfm <- forAll $ genSomeUnsafeFinMap genOrdering
       withIndexUnsafe sfm $ \idx fm -> do
        o <- forAll genOrdering
        U.insert idx o (U.delete idx fm) === U.insert idx o fm
  
  prop_empty_insert_safe :: Property
  prop_empty_insert_safe = property $
    do withIndexSafe (SomeSafeFinMap (NatRepr.knownNat @0) S.empty) $ \idx fm -> do
        o <- forAll genOrdering
        fm /== S.insert idx o fm
  
  prop_empty_insert_unsafe :: Property
  prop_empty_insert_unsafe = property $
    do withIndexUnsafe (SomeUnsafeFinMap (NatRepr.knownNat @0) U.empty) $ \idx fm -> do
        o <- forAll genOrdering
        fm /== U.insert idx o fm
  
  prop_insert_insert_safe :: Property
  prop_insert_insert_safe = property $
    do sfm <- forAll $ genSomeSafeFinMap genOrdering
       withIndexSafe sfm $ \idx fm -> do
        o <- forAll genOrdering
        S.insert idx o (S.insert idx o fm) === S.insert idx o fm
  
  prop_insert_insert_unsafe :: Property
  prop_insert_insert_unsafe = property $
    do sfm <- forAll $ genSomeUnsafeFinMap genOrdering
       withIndexUnsafe sfm $ \idx fm -> do
        o <- forAll genOrdering
        U.insert idx o (U.insert idx o fm) === U.insert idx o fm
  
  prop_delete_delete_safe :: Property
  prop_delete_delete_safe = property $
    do sfm <- forAll $ genSomeSafeFinMap genOrdering
       withIndexSafe sfm $ \idx fm -> do
        S.delete idx (S.delete idx fm) === S.delete idx fm
  
  prop_delete_delete_unsafe :: Property
  prop_delete_delete_unsafe = property $
    do sfm <- forAll $ genSomeUnsafeFinMap genOrdering
       withIndexUnsafe sfm $ \idx fm -> do
        U.delete idx (U.delete idx fm) === U.delete idx fm
  
  -- | Type used for comparative API tests
  data MatchedMaps a =
    forall n.
    MatchedMaps
      { _unsafe :: U.FinMap n a
      , _safe :: S.FinMap n a
      }
  
  operations ::
    Show a =>
    Gen a ->
    -- | For testing 'fmap'.
    [a -> a] ->
    [MatchedMaps a -> PropertyT IO (MatchedMaps a)]
  operations genValue valEndomorphisms =
    [ \(MatchedMaps u s) ->
        withSizeUnsafe u $ \sz -> do
          case NatRepr.isZeroOrGT1 sz of
            Left Refl ->
              do v <- forAll genValue
                 return $
                   MatchedMaps
                     (U.insert Fin.minFin v (U.incMax u))
                     (S.insert Fin.minFin v (S.incMax s))
            Right NatRepr.LeqProof ->
              do idx <- Fin.embed <$> forAll (genFin sz)
                 v <- forAll genValue
                 return (MatchedMaps (U.insert idx v u) (S.insert idx v s))
    , \(MatchedMaps u s) ->
        withSizeUnsafe u $ \sz -> do
          case NatRepr.isZeroOrGT1 sz of
            Left Refl -> return (MatchedMaps u s)
            Right NatRepr.LeqProof ->
              do idx <- Fin.embed <$> forAll (genFin sz)
                 return (MatchedMaps (U.delete idx u) (S.delete idx s))
    , \(MatchedMaps u s) ->
          return (MatchedMaps (U.incMax u) (S.incMax s))
    , \(MatchedMaps u s) ->
        do f <- forAll (HG.element (id:valEndomorphisms))
           return (MatchedMaps (fmap f u) (fmap f s))
    , \(MatchedMaps u s) ->
        do f <- forAll (HG.element (id:valEndomorphisms))
           return (MatchedMaps (imap (const f) u) (imap (const f) s))
    , \(MatchedMaps _ _) ->
        do v <- forAll genValue
           return (MatchedMaps (U.singleton v) (S.singleton v))
    , \(MatchedMaps _ _) ->
        return (MatchedMaps (U.empty @0) S.empty)
    , \(MatchedMaps _ _) ->
        return (MatchedMaps (U.empty @8) S.empty)
    ]
  
  -- | Possibly the most important and far-reaching test: The unsafe API should
  -- yield the same results as the safe API, after some randomized sequence of
  -- operations.
  prop_safe_unsafe :: Property
  prop_safe_unsafe = property $
    do numOps <- forAll (HG.integral (linear 0 (99 :: Int)))
       let empty = MatchedMaps (U.empty @0) S.empty
       MatchedMaps u s <-
         doTimes (chooseAndApply orderingOps) numOps empty
       itoList u === itoList s
    where
      orderingOps = operations genOrdering orderingEndomorphisms
  
      chooseAndApply :: [a -> PropertyT IO b] -> a -> PropertyT IO b
      chooseAndApply funs arg =
        do f <- forAll (HG.element funs)
           f arg
  
      doTimes f n m = foldM (\accum () -> f accum) m (replicate n ())
  
  
  finMapTests :: IO TestTree
  finMapTests = testGroup "FinMap" <$> return
    [ testPropertyNamed "incSize-decSize-safe" "prop_incMax_size_safe" prop_incMax_size_safe
    , testPropertyNamed "incSize-decSize-unsafe" "prop_incMax_size_unsafe" prop_incMax_size_unsafe
    , testPropertyNamed "insert-size-safe" "prop_insert_size_safe" prop_insert_size_safe
    , testPropertyNamed "insert-size-unsafe" "prop_insert_size_unsafe" prop_insert_size_unsafe
    , testPropertyNamed "insert-delete-safe" "prop_insert_delete_safe" prop_insert_delete_safe
    , testPropertyNamed "insert-delete-unsafe" "prop_insert_delete_unsafe" prop_insert_delete_unsafe
    , testPropertyNamed "delete-insert-safe" "prop_delete_insert_safe" prop_delete_insert_safe
    , testPropertyNamed "delete-insert-unsafe" "prop_delete_insert_unsafe" prop_delete_insert_unsafe
    , testPropertyNamed "empty-insert-safe" "prop_empty_insert_safe" prop_empty_insert_safe
    , testPropertyNamed "empty-insert-unsafe" "prop_empty_insert_unsafe" prop_empty_insert_unsafe
    , testPropertyNamed "insert-insert-safe" "prop_insert_insert_safe" prop_insert_insert_safe
    , testPropertyNamed "insert-insert-unsafe" "prop_insert_insert_unsafe" prop_insert_insert_unsafe
    , testPropertyNamed "delete-delete-safe" "prop_delete_delete_safe" prop_delete_delete_safe
    , testPropertyNamed "delete-delete-unsafe" "prop_delete_delete_unsafe" prop_delete_delete_unsafe
    , testPropertyNamed "imap-const-safe" "prop_imap_const_safe" prop_imap_const_safe
    , testPropertyNamed "imap-const-unsafe" "prop_imap_const_unsafe" prop_imap_const_unsafe
    , testPropertyNamed "ifoldMap-const-safe" "prop_ifoldMap_const_safe" prop_ifoldMap_const_safe
    , testPropertyNamed "ifoldMap-const-unsafe" "prop_ifoldMap_const_unsafe" prop_ifoldMap_const_unsafe
    , testPropertyNamed "safe-unsafe" "prop_safe_unsafe" prop_safe_unsafe
  
  #if __GLASGOW_HASKELL__ >= 806
    , testCase "Eq-Safe-FinMap-laws-1" $
        assertBool "Eq-Safe-FinMap-laws-1" =<<
          HC.lawsCheck (HC.eqLaws (genSafeFinMap (NatRepr.knownNat @1) genOrdering))
    , testCase "Eq-Unsafe-FinMap-laws-1" $
        assertBool "Eq-Unsafe-FinMap-laws-1" =<<
          HC.lawsCheck (HC.eqLaws (genUnsafeFinMap (NatRepr.knownNat @1) genOrdering))
    , testCase "Eq-Safe-FinMap-laws-10" $
        assertBool "Eq-Safe-FinMap-laws-10" =<<
          HC.lawsCheck (HC.eqLaws (genSafeFinMap (NatRepr.knownNat @10) genOrdering))
    , testCase "Eq-Unsafe-FinMap-laws-10" $
        assertBool "Eq-Unsafe-FinMap-laws-10" =<<
          HC.lawsCheck (HC.eqLaws (genUnsafeFinMap (NatRepr.knownNat @10) genOrdering))
    , testCase "Semigroup-Safe-FinMap-laws-1" $
        assertBool "Semigroup-Safe-FinMap-laws-1" =<<
          HC.lawsCheck (HC.semigroupLaws (genSafeFinMap (NatRepr.knownNat @1) genOrdering))
    , testCase "Semigroup-Unsafe-FinMap-laws-1" $
        assertBool "Semigroup-Unsafe-FinMap-laws-1" =<<
          HC.lawsCheck (HC.semigroupLaws (genUnsafeFinMap (NatRepr.knownNat @1) genOrdering))
    , testCase "Semigroup-Safe-FinMap-laws-10" $
        assertBool "Semigroup-Safe-FinMap-laws-10" =<<
          HC.lawsCheck (HC.semigroupLaws (genSafeFinMap (NatRepr.knownNat @10) genOrdering))
    , testCase "Semigroup-Unsafe-FinMap-laws-10" $
        assertBool "Semigroup-Unsafe-FinMap-laws-10" =<<
          HC.lawsCheck (HC.semigroupLaws (genUnsafeFinMap (NatRepr.knownNat @10) genOrdering))
    , testCase "Monoid-Safe-FinMap-laws-1" $
        assertBool "Monoid-Safe-FinMap-laws-1" =<<
          HC.lawsCheck (HC.monoidLaws (genSafeFinMap (NatRepr.knownNat @1) genOrdering))
    , testCase "Monoid-Unsafe-FinMap-laws-1" $
        assertBool "Monoid-Unsafe-FinMap-laws-1" =<<
          HC.lawsCheck (HC.monoidLaws (genUnsafeFinMap (NatRepr.knownNat @1) genOrdering))
    , testCase "Monoid-Safe-FinMap-laws-10" $
        assertBool "Monoid-Safe-FinMap-laws-10" =<<
          HC.lawsCheck (HC.monoidLaws (genSafeFinMap (NatRepr.knownNat @10) genOrdering))
    , testCase "Monoid-Unsafe-FinMap-laws-10" $
        assertBool "Monoid-Unsafe-FinMap-laws-10" =<<
          HC.lawsCheck (HC.monoidLaws (genUnsafeFinMap (NatRepr.knownNat @10) genOrdering))
    , testCase "Foldable-Safe-FinMap-laws-1" $
        assertBool "Foldable-Safe-FinMap-laws-1" =<<
          HC.lawsCheck (HC.foldableLaws (genSafeFinMap (NatRepr.knownNat @1)))
    , testCase "Foldable-Unsafe-FinMap-laws-1" $
        assertBool "Foldable-Unsafe-FinMap-laws-1" =<<
          HC.lawsCheck (HC.foldableLaws (genUnsafeFinMap (NatRepr.knownNat @1)))
    , testCase "Foldable-Safe-FinMap-laws-10" $
        assertBool "Foldable-Safe-FinMap-laws-10" =<<
          HC.lawsCheck (HC.foldableLaws (genSafeFinMap (NatRepr.knownNat @10)))
    , testCase "Foldable-Unsafe-FinMap-laws-10" $
        assertBool "Foldable-Unsafe-FinMap-laws-10" =<<
          HC.lawsCheck (HC.foldableLaws (genUnsafeFinMap (NatRepr.knownNat @10)))
    , testCase "Traversable-Safe-FinMap-laws-1" $
        assertBool "Traversable-Safe-FinMap-laws-1" =<<
          HC.lawsCheck (HC.traversableLaws (genSafeFinMap (NatRepr.knownNat @1)))
    , testCase "Traversable-Unsafe-FinMap-laws-1" $
        assertBool "Traversable-Unsafe-FinMap-laws-1" =<<
          HC.lawsCheck (HC.traversableLaws (genUnsafeFinMap (NatRepr.knownNat @1)))
    , testCase "Traversable-Safe-FinMap-laws-10" $
        assertBool "Traversable-Safe-FinMap-laws-10" =<<
          HC.lawsCheck (HC.traversableLaws (genSafeFinMap (NatRepr.knownNat @10)))
    , testCase "Traversable-Unsafe-FinMap-laws-10" $
        assertBool "Traversable-Unsafe-FinMap-laws-10" =<<
          HC.lawsCheck (HC.traversableLaws (genUnsafeFinMap (NatRepr.knownNat @10)))
  #endif
    ]
  