{-|
Copyright   : (C) 2021-2024, QBayLogic B.V.
License     : BSD2 (see the file LICENSE)
Maintainer  : QBayLogic B.V. <devops@qbaylogic.com>

Random generation of BitVector.
-}

{-# OPTIONS_GHC -fplugin=GHC.TypeLits.KnownNat.Solver #-}

{-# LANGUAGE CPP #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE RankNTypes #-}

module Clash.Hedgehog.Sized.BitVector
  ( genDefinedBit
  , genBit
  , genDefinedBitVector
  , genBitVector
  , SomeBitVector(..)
  , genSomeBitVector
  ) where

import GHC.TypeNats
  hiding (SNat)
import Hedgehog (MonadGen, Range)
import Hedgehog.Internal.Range (constantBounded, constant)
import qualified Hedgehog.Gen as Gen

import Clash.Class.BitPack (pack)
import Clash.Promoted.Nat
import Clash.Sized.Internal.BitVector
import Clash.XException (errorX)

import Clash.Hedgehog.Sized.Unsigned

-- | Generate a bit which is guaranteed to be defined.
-- This will either have the value 'low' or 'high'.
--
genDefinedBit :: (MonadGen m) => m Bit
genDefinedBit :: forall (m :: Type -> Type). MonadGen m => m Bit
genDefinedBit = [Bit] -> m Bit
forall (f :: Type -> Type) (m :: Type -> Type) a.
(Foldable f, MonadGen m) =>
f a -> m a
Gen.element [Bit
low, Bit
high]

-- | Generate a bit which is not guaranteed to be defined.
-- This will either have the value 'low' or 'high', or throw an @XException@.
--
genBit :: (MonadGen m) => m Bit
genBit :: forall (m :: Type -> Type). MonadGen m => m Bit
genBit = [Bit] -> m Bit
forall (f :: Type -> Type) (m :: Type -> Type) a.
(Foldable f, MonadGen m) =>
f a -> m a
Gen.element [Bit
low, Bit
high, String -> Bit
forall a. HasCallStack => String -> a
errorX String
"X"]

-- | Generate a bit vector where all bits are defined.
--
genDefinedBitVector :: forall n m. (MonadGen m, KnownNat n) => m (BitVector n)
genDefinedBitVector :: forall (n :: Nat) (m :: Type -> Type).
(MonadGen m, KnownNat n) =>
m (BitVector n)
genDefinedBitVector = Unsigned n -> BitVector n
Unsigned n -> BitVector (BitSize (Unsigned n))
forall a. BitPack a => a -> BitVector (BitSize a)
pack (Unsigned n -> BitVector n) -> m (Unsigned n) -> m (BitVector n)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Range (Unsigned n) -> m (Unsigned n)
forall (n :: Nat) (m :: Type -> Type).
(MonadGen m, KnownNat n) =>
Range (Unsigned n) -> m (Unsigned n)
genUnsigned Range (Unsigned n)
forall a. (Bounded a, Num a) => Range a
constantBounded

-- | Generate a bit vector where some bits may be undefined.
--
genBitVector :: forall n m. (MonadGen m, KnownNat n) => m (BitVector n)
genBitVector :: forall (n :: Nat) (m :: Type -> Type).
(MonadGen m, KnownNat n) =>
m (BitVector n)
genBitVector =
  [(Int, m (BitVector n))] -> m (BitVector n)
forall (m :: Type -> Type) a. MonadGen m => [(Int, m a)] -> m a
Gen.frequency
    [ (Int
70, Nat -> Nat -> BitVector n
forall (n :: Nat). Nat -> Nat -> BitVector n
BV (Nat -> Nat -> BitVector n) -> m Nat -> m (Nat -> BitVector n)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> m Nat
genNatural m (Nat -> BitVector n) -> m Nat -> m (BitVector n)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> m Nat
genNatural)
    , (Int
10, BitVector n -> m (BitVector n)
forall (m :: Type -> Type) a. MonadGen m => a -> m a
Gen.constant BitVector n
forall a. Bounded a => a
minBound)
    , (Int
10, BitVector n -> m (BitVector n)
forall (m :: Type -> Type) a. MonadGen m => a -> m a
Gen.constant BitVector n
forall a. Bounded a => a
maxBound)
    , (Int
10, BitVector n -> m (BitVector n)
forall (m :: Type -> Type) a. MonadGen m => a -> m a
Gen.constant BitVector n
forall (n :: Nat). KnownNat n => BitVector n
undefined#)
    ]
 where
  genNatural :: m Nat
genNatural = Range Nat -> m Nat
forall (m :: Type -> Type) a.
(MonadGen m, Integral a) =>
Range a -> m a
Gen.integral (Range Nat -> m Nat) -> Range Nat -> m Nat
forall a b. (a -> b) -> a -> b
$ Nat -> Nat -> Range Nat
forall a. a -> a -> Range a
constant Nat
0 (Nat
2Nat -> Nat -> Nat
forall a b. (Num a, Integral b) => a -> b -> a
^forall (n :: Nat). KnownNat n => Nat
natToNatural @n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1)

data SomeBitVector atLeast where
  SomeBitVector :: SNat n -> BitVector (atLeast + n) -> SomeBitVector atLeast

instance KnownNat atLeast => Show (SomeBitVector atLeast) where
  show :: SomeBitVector atLeast -> String
show (SomeBitVector SNat n
SNat BitVector (atLeast + n)
bv) = BitVector (atLeast + n) -> String
forall a. Show a => a -> String
show BitVector (atLeast + n)
bv

genSomeBitVector
  :: forall atLeast m
   . (MonadGen m, KnownNat atLeast)
  => Range Natural
  -> (forall n. KnownNat n => m (BitVector n))
  -> m (SomeBitVector atLeast)
genSomeBitVector :: forall (atLeast :: Nat) (m :: Type -> Type).
(MonadGen m, KnownNat atLeast) =>
Range Nat
-> (forall (n :: Nat). KnownNat n => m (BitVector n))
-> m (SomeBitVector atLeast)
genSomeBitVector Range Nat
rangeBv forall (n :: Nat). KnownNat n => m (BitVector n)
genBv = do
  Nat
numExtra <- Range Nat -> m Nat
forall (m :: Type -> Type) a.
(MonadGen m, Integral a) =>
Range a -> m a
Gen.integral Range Nat
rangeBv

  case Nat -> SomeNat
someNatVal Nat
numExtra of
    SomeNat Proxy n
proxy -> SNat n -> BitVector (atLeast + n) -> SomeBitVector atLeast
forall (n :: Nat) (atLeast :: Nat).
SNat n -> BitVector (atLeast + n) -> SomeBitVector atLeast
SomeBitVector (Proxy n -> SNat n
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> SNat n
snatProxy Proxy n
proxy) (BitVector (atLeast + n) -> SomeBitVector atLeast)
-> m (BitVector (atLeast + n)) -> m (SomeBitVector atLeast)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> m (BitVector (atLeast + n))
forall (n :: Nat). KnownNat n => m (BitVector n)
genBv