content: {-|
  Copyright   : (C) 2021-2022, QBayLogic B.V.
  License     : BSD2 (see the file LICENSE)
  Maintainer  : QBayLogic B.V. <devops@qbaylogic.com>
  
  Random generation of vectors.
  -}
  
  {-# OPTIONS_GHC -fplugin=GHC.TypeLits.KnownNat.Solver #-}
  
  {-# LANGUAGE CPP #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE MagicHash #-}
  
  module Clash.Hedgehog.Sized.Vector
    ( genVec
    , genNonEmptyVec
    , SomeVec(..)
    , genSomeVec
    ) where
  
  import Prelude hiding (repeat)
  
  #if !MIN_VERSION_base(4,16,0)
  import GHC.Natural (Natural)
  #endif
  import GHC.TypeNats
  #if MIN_VERSION_base(4,18,0)
    hiding (SNat)
  #endif
  import Hedgehog (MonadGen, Range)
  import qualified Hedgehog.Gen as Gen
  
  import Clash.Promoted.Nat
  import Clash.Sized.Vector
  
  -- | Generate a potentially empty vector, where each element is produced
  -- using the supplied generator. For a non-empty vector, see 'genNonEmptyVec'.
  --
  genVec :: forall n a m. (MonadGen m, KnownNat n) => m a -> m (Vec n a)
  genVec genElem = traverse# id (repeat genElem)
  
  -- | Generate a non-empty vector, where each element is produced using the
  -- supplied generator. For a potentially empty vector, see 'genVec'.
  --
  genNonEmptyVec :: forall n a m. (MonadGen m, KnownNat n, 1 <= n) => m a -> m (Vec n a)
  genNonEmptyVec = genVec
  
  data SomeVec atLeast a where
    SomeVec :: SNat n -> Vec (atLeast + n) a -> SomeVec atLeast a
  
  instance (KnownNat atLeast, Show a) => Show (SomeVec atLeast a) where
    show (SomeVec SNat xs) = show xs
  
  genSomeVec
    :: forall atLeast a m
     . (MonadGen m, KnownNat atLeast)
    => Range Natural
    -> m a
    -> m (SomeVec atLeast a)
  genSomeVec rangeElems genElem = do
    numExtra <- Gen.integral rangeElems
  
    case someNatVal numExtra of
      SomeNat proxy -> SomeVec (snatProxy proxy) <$> genVec genElem
  