{-# OPTIONS_GHC -fplugin=GHC.TypeLits.KnownNat.Solver #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE GADTs #-}
module Clash.Hedgehog.Sized.Unsigned
( genUnsigned
, SomeUnsigned(..)
, genSomeUnsigned
) where
#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 qualified Hedgehog.Range as Range
import Clash.Promoted.Nat
import Clash.Sized.Internal.Unsigned
genUnsigned :: (MonadGen m, KnownNat n) => Range (Unsigned n) -> m (Unsigned n)
genUnsigned :: Range (Unsigned n) -> m (Unsigned n)
genUnsigned Range (Unsigned n)
range =
[(Int, m (Unsigned n))] -> m (Unsigned n)
forall (m :: Type -> Type) a. MonadGen m => [(Int, m a)] -> m a
Gen.frequency
[ (Int
70, Range (Unsigned n) -> m (Unsigned n)
forall (m :: Type -> Type) a.
(MonadGen m, Integral a) =>
Range a -> m a
Gen.integral Range (Unsigned n)
range)
, (Int
30, Unsigned n -> m (Unsigned n)
forall (m :: Type -> Type) a. MonadGen m => a -> m a
Gen.constant (Size -> Range (Unsigned n) -> Unsigned n
forall a. Ord a => Size -> Range a -> a
Range.upperBound Size
99 Range (Unsigned n)
range))
]
data SomeUnsigned atLeast where
SomeUnsigned :: SNat n -> Unsigned (atLeast + n) -> SomeUnsigned atLeast
instance KnownNat atLeast => Show (SomeUnsigned atLeast) where
show :: SomeUnsigned atLeast -> String
show (SomeUnsigned SNat n
SNat Unsigned (atLeast + n)
x) = Unsigned (atLeast + n) -> String
forall a. Show a => a -> String
show Unsigned (atLeast + n)
x
genSomeUnsigned
:: (MonadGen m, KnownNat atLeast)
=> Range Natural
-> m (SomeUnsigned atLeast)
genSomeUnsigned :: Range Natural -> m (SomeUnsigned atLeast)
genSomeUnsigned Range Natural
rangeUnsigned = do
Natural
numExtra <- Range Natural -> m Natural
forall (m :: Type -> Type) a.
(MonadGen m, Integral a) =>
Range a -> m a
Gen.integral Range Natural
rangeUnsigned
case Natural -> SomeNat
someNatVal Natural
numExtra of
SomeNat Proxy n
proxy -> SNat n -> Unsigned (atLeast + n) -> SomeUnsigned atLeast
forall (n :: Nat) (atLeast :: Nat).
SNat n -> Unsigned (atLeast + n) -> SomeUnsigned atLeast
SomeUnsigned (Proxy n -> SNat n
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> SNat n
snatProxy Proxy n
proxy) (Unsigned (atLeast + n) -> SomeUnsigned atLeast)
-> m (Unsigned (atLeast + n)) -> m (SomeUnsigned atLeast)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Range (Unsigned (atLeast + n)) -> m (Unsigned (atLeast + n))
forall (m :: Type -> Type) (n :: Nat).
(MonadGen m, KnownNat n) =>
Range (Unsigned n) -> m (Unsigned n)
genUnsigned Range (Unsigned (atLeast + n))
forall a. (Bounded a, Integral a) => Range a
Range.linearBounded