clash-finite-1.0.0.0: A class for types with only finitely many inhabitants
Copyright(C) 2024-2025 Felix Klein
LicenseMIT (see the file LICENSE)
MaintainerFelix Klein <felix@qbaylogic.com>
Safe HaskellSafe-Inferred
LanguageHaskell2010

Clash.Class.Finite

Description

The class of types holding only a finite number of elements. The Finite class offers type level access to the number of elements n and defines a total order on the elements via indexing them from 0 to n-1. Therewith, it gives access to the vector of all inhabitants of the type and allows to iterate over them in order or to map them back and forth between their associated indices.

The class can be considered as a more hardware-friendly alternative to Bounded and Enum, utilizing Index instead of Int and vectors instead of lists.

In comparison, Finite is well suited for types holding finitely many elements, while the Enum class is better suited for types with infinitely many inhabitants. The type of succ, pred :: Enum a => a -> a clearly reflects this design choice, as it assumes that every element has a successor and predecessor, which makes perfect sense for infinite types, but requires finite types to error on certain inputs. Wrapping behavior is forbidden according to the documentation of Enum (assuming that finite types usually have a Bounded instance) such that Enum instances must ship partial functions for most finite types. Likewise, the number of inhabitants does not align with the number of indices offered by Int for most types, which Finite resolves by using Index n instead.

Synopsis

Finite Class

class KnownNat (ElementCount a) => Finite a where Source #

The class of types holding only a finite number of elements.

The class supports generic deriving, i.e., for custom types the class instances can be derived via derive (Generic, Finite) requiring that all inner types of the type declaration have Finite instances as well.

>>> data T = B Bit | D (Index 2) (Signed 1) deriving (Generic, Finite, Show)
>>> natToNum @(ElementCount T)
6
>>> elements @T
B 0 :> B 1 :> D 0 -1 :> D 0 0 :> D 1 -1 :> D 1 0 :> Nil
>>> lowestMaybe @T
Just (B 0)
>>> highestMaybe @T
Just (D 1 0)
>>> succMaybe (B 1)
Just (D 0 -1)
>>> predMaybe (B 0)
Nothing
>>> index (D 0 0)
3
>>> ith @T 5
D 1 0

Any definition must satisfy the following laws (automatically ensured when generic deriving the instance):

Index Order
index <$> elements = indicesI
Forward Iterate
iterateI (>>= succMaybe) (lowestMaybe @a) = Just <$> (elements @a)
Backward Iterate
iterateI (>>= predMaybe) (highestMaybe @a) = Just <$> reverse (elements @a)
Index Isomorphism
ith (index x) = x
Minimum Predecessor
lowestMaybe >>= predMaybe = Nothing
Maximum Successor
highestMaybe >>= succMaybe = Nothing
Extremes
ElementCount a = 0: lowestMaybe @a = Nothing, highestMaybe @a = Nothing
ElementCount a > 0: lowestMaybe @a = Just lowest, highestMaybe @a = Just highest

If a has a Bounded instance, it further must satisfy:

Bounded Compatibility
ElementCount a > 0: lowest @a = minBound, highest @a = maxBound

If a has an Enum instance, it further must satisfy:

Enum Compatibility
succMaybe x = Just y: succ x = y
predMaybe x = Just y: pred x = y

Minimal complete definition

Nothing

Associated Types

type ElementCount a :: Nat Source #

The number of elements of the type.

Methods

elements :: Vec (ElementCount a) a Source #

The elements of the type.

lowest :: 1 <= ElementCount a => a Source #

The element at index 0.

default lowest :: (Generic a, GFinite (Rep a), ElementCount a ~ GElementCount (Rep a)) => 1 <= ElementCount a => a Source #

lowestMaybe :: Maybe a Source #

Just the element at index 0. Nothing, if ElementCount a = 0.

default lowestMaybe :: (Generic a, GFinite (Rep a)) => Maybe a Source #

highest :: 1 <= ElementCount a => a Source #

The element at index (ElementCount a - 1).

default highest :: (Generic a, GFinite (Rep a), ElementCount a ~ GElementCount (Rep a)) => 1 <= ElementCount a => a Source #

highestMaybe :: Maybe a Source #

Just the element at index (ElementCount a - 1). Nothing, if ElementCount a = 0.

default highestMaybe :: (Generic a, GFinite (Rep a)) => Maybe a Source #

predMaybe :: a -> Maybe a Source #

Just the element before the given one according to the associated index order with the lowest one being the only element that has no predecessor.

default predMaybe :: (Generic a, GFinite (Rep a)) => a -> Maybe a Source #

succMaybe :: a -> Maybe a Source #

Just the element after the given one according to the associated index order with the highest one being the only element that has no successor.

default succMaybe :: (Generic a, GFinite (Rep a)) => a -> Maybe a Source #

ith :: Index (ElementCount a) -> a Source #

Maps from an index to the associated element.

default ith :: (Generic a, GFinite (Rep a), ElementCount a ~ GElementCount (Rep a)) => Index (ElementCount a) -> a Source #

index :: a -> Index (ElementCount a) Source #

Maps an element of the type to it's associated index.

default index :: (Generic a, GFinite (Rep a), ElementCount a ~ GElementCount (Rep a)) => a -> Index (ElementCount a) Source #

elementsFrom :: (n + 1) <= ElementCount a => SNat n -> Vec (ElementCount a - n) a Source #

Returns the suffix slice of elements starting at the index provided via the SNat argument.

elementsFromTo :: ((n + 1) <= ElementCount a, n <= m, (m + 1) <= ElementCount a) => SNat n -> SNat m -> Vec ((m - n) + 1) a Source #

Returns the infix slice of elements from the index provided via the first SNat argument to the index provided via the second one.

Instances

Instances details
Finite Void Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount Void :: Nat Source #

Finite Int16 Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount Int16 :: Nat Source #

Finite Int32 Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount Int32 :: Nat Source #

Finite Int64 Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount Int64 :: Nat Source #

Finite Int8 Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount Int8 :: Nat Source #

Finite Word16 Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount Word16 :: Nat Source #

Finite Word32 Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount Word32 :: Nat Source #

Finite Word64 Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount Word64 :: Nat Source #

Finite Word8 Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount Word8 :: Nat Source #

Finite Bit Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount Bit :: Nat Source #

Finite Ordering Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount Ordering :: Nat Source #

Finite () Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount () :: Nat Source #

Methods

elements :: Vec (ElementCount ()) () Source #

lowest :: () Source #

lowestMaybe :: Maybe () Source #

highest :: () Source #

highestMaybe :: Maybe () Source #

predMaybe :: () -> Maybe () Source #

succMaybe :: () -> Maybe () Source #

ith :: Index (ElementCount ()) -> () Source #

index :: () -> Index (ElementCount ()) Source #

elementsFrom :: forall (n :: Natural). (n + 1) <= ElementCount () => SNat n -> Vec (ElementCount () - n) () Source #

elementsFromTo :: forall (n :: Natural) (m :: Natural). ((n + 1) <= ElementCount (), n <= m, (m + 1) <= ElementCount ()) => SNat n -> SNat m -> Vec ((m - n) + 1) () Source #

Finite Bool Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount Bool :: Nat Source #

Finite Char Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount Char :: Nat Source #

Finite Int Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount Int :: Nat Source #

Finite Word Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount Word :: Nat Source #

Finite a => Finite (Identity a) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (Identity a) :: Nat Source #

Finite a => Finite (Down a) Source #

Reverses the index order used by the Finite instance of the inner type.

>>> elements @(Maybe Bool)
Nothing :> Just False :> Just True :> Nil
>>> elements @(Down (Maybe Bool))
Down (Just True) :> Down (Just False) :> Down Nothing :> Nil
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (Down a) :: Nat Source #

Methods

elements :: Vec (ElementCount (Down a)) (Down a) Source #

lowest :: Down a Source #

lowestMaybe :: Maybe (Down a) Source #

highest :: Down a Source #

highestMaybe :: Maybe (Down a) Source #

predMaybe :: Down a -> Maybe (Down a) Source #

succMaybe :: Down a -> Maybe (Down a) Source #

ith :: Index (ElementCount (Down a)) -> Down a Source #

index :: Down a -> Index (ElementCount (Down a)) Source #

elementsFrom :: forall (n :: Natural). (n + 1) <= ElementCount (Down a) => SNat n -> Vec (ElementCount (Down a) - n) (Down a) Source #

elementsFromTo :: forall (n :: Natural) (m :: Natural). ((n + 1) <= ElementCount (Down a), n <= m, (m + 1) <= ElementCount (Down a)) => SNat n -> SNat m -> Vec ((m - n) + 1) (Down a) Source #

(Generic a, GFinite (Rep a), KnownNat (GElementCount (Rep a))) => Finite (GenericReverse a) Source #

see GenericReverse

Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (GenericReverse a) :: Nat Source #

Finite (WithUndefined Bit) Source #

NB: not synthesizable (see WithUndefined)

Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (WithUndefined Bit) :: Nat Source #

KnownNat n => Finite (WithUndefined (BitVector n)) Source #

NB: not synthesizable (see WithUndefined)

Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (WithUndefined (BitVector n)) :: Nat Source #

(SaturatingNum a, Finite a) => Finite (Erroring a) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (Erroring a) :: Nat Source #

Finite a => Finite (Overflowing a) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (Overflowing a) :: Nat Source #

(SaturatingNum a, Finite a) => Finite (Saturating a) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (Saturating a) :: Nat Source #

(SaturatingNum a, Finite a) => Finite (Wrapping a) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (Wrapping a) :: Nat Source #

(SaturatingNum a, Finite a) => Finite (Zeroing a) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (Zeroing a) :: Nat Source #

KnownNat n => Finite (SNat n) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (SNat n) :: Nat Source #

Methods

elements :: Vec (ElementCount (SNat n)) (SNat n) Source #

lowest :: SNat n Source #

lowestMaybe :: Maybe (SNat n) Source #

highest :: SNat n Source #

highestMaybe :: Maybe (SNat n) Source #

predMaybe :: SNat n -> Maybe (SNat n) Source #

succMaybe :: SNat n -> Maybe (SNat n) Source #

ith :: Index (ElementCount (SNat n)) -> SNat n Source #

index :: SNat n -> Index (ElementCount (SNat n)) Source #

elementsFrom :: forall (n0 :: Natural). (n0 + 1) <= ElementCount (SNat n) => SNat n0 -> Vec (ElementCount (SNat n) - n0) (SNat n) Source #

elementsFromTo :: forall (n0 :: Natural) (m :: Natural). ((n0 + 1) <= ElementCount (SNat n), n0 <= m, (m + 1) <= ElementCount (SNat n)) => SNat n0 -> SNat m -> Vec ((m - n0) + 1) (SNat n) Source #

KnownSymbol s => Finite (SSymbol s) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (SSymbol s) :: Nat Source #

KnownNat n => Finite (BitVector n) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (BitVector n) :: Nat Source #

KnownNat n => Finite (Index n) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (Index n) :: Nat Source #

Methods

elements :: Vec (ElementCount (Index n)) (Index n) Source #

lowest :: Index n Source #

lowestMaybe :: Maybe (Index n) Source #

highest :: Index n Source #

highestMaybe :: Maybe (Index n) Source #

predMaybe :: Index n -> Maybe (Index n) Source #

succMaybe :: Index n -> Maybe (Index n) Source #

ith :: Index (ElementCount (Index n)) -> Index n Source #

index :: Index n -> Index (ElementCount (Index n)) Source #

elementsFrom :: forall (n0 :: Natural). (n0 + 1) <= ElementCount (Index n) => SNat n0 -> Vec (ElementCount (Index n) - n0) (Index n) Source #

elementsFromTo :: forall (n0 :: Natural) (m :: Natural). ((n0 + 1) <= ElementCount (Index n), n0 <= m, (m + 1) <= ElementCount (Index n)) => SNat n0 -> SNat m -> Vec ((m - n0) + 1) (Index n) Source #

KnownNat n => Finite (Signed n) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (Signed n) :: Nat Source #

KnownNat n => Finite (Unsigned n) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (Unsigned n) :: Nat Source #

c => Finite (Dict c) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (Dict c) :: Nat Source #

Methods

elements :: Vec (ElementCount (Dict c)) (Dict c) Source #

lowest :: Dict c Source #

lowestMaybe :: Maybe (Dict c) Source #

highest :: Dict c Source #

highestMaybe :: Maybe (Dict c) Source #

predMaybe :: Dict c -> Maybe (Dict c) Source #

succMaybe :: Dict c -> Maybe (Dict c) Source #

ith :: Index (ElementCount (Dict c)) -> Dict c Source #

index :: Dict c -> Index (ElementCount (Dict c)) Source #

elementsFrom :: forall (n :: Natural). (n + 1) <= ElementCount (Dict c) => SNat n -> Vec (ElementCount (Dict c) - n) (Dict c) Source #

elementsFromTo :: forall (n :: Natural) (m :: Natural). ((n + 1) <= ElementCount (Dict c), n <= m, (m + 1) <= ElementCount (Dict c)) => SNat n -> SNat m -> Vec ((m - n) + 1) (Dict c) Source #

Finite a => Finite (Maybe a) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (Maybe a) :: Nat Source #

Methods

elements :: Vec (ElementCount (Maybe a)) (Maybe a) Source #

lowest :: Maybe a Source #

lowestMaybe :: Maybe (Maybe a) Source #

highest :: Maybe a Source #

highestMaybe :: Maybe (Maybe a) Source #

predMaybe :: Maybe a -> Maybe (Maybe a) Source #

succMaybe :: Maybe a -> Maybe (Maybe a) Source #

ith :: Index (ElementCount (Maybe a)) -> Maybe a Source #

index :: Maybe a -> Index (ElementCount (Maybe a)) Source #

elementsFrom :: forall (n :: Natural). (n + 1) <= ElementCount (Maybe a) => SNat n -> Vec (ElementCount (Maybe a) - n) (Maybe a) Source #

elementsFromTo :: forall (n :: Natural) (m :: Natural). ((n + 1) <= ElementCount (Maybe a), n <= m, (m + 1) <= ElementCount (Maybe a)) => SNat n -> SNat m -> Vec ((m - n) + 1) (Maybe a) Source #

(Finite a, Finite b) => Finite (Either a b) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (Either a b) :: Nat Source #

Methods

elements :: Vec (ElementCount (Either a b)) (Either a b) Source #

lowest :: Either a b Source #

lowestMaybe :: Maybe (Either a b) Source #

highest :: Either a b Source #

highestMaybe :: Maybe (Either a b) Source #

predMaybe :: Either a b -> Maybe (Either a b) Source #

succMaybe :: Either a b -> Maybe (Either a b) Source #

ith :: Index (ElementCount (Either a b)) -> Either a b Source #

index :: Either a b -> Index (ElementCount (Either a b)) Source #

elementsFrom :: forall (n :: Natural). (n + 1) <= ElementCount (Either a b) => SNat n -> Vec (ElementCount (Either a b) - n) (Either a b) Source #

elementsFromTo :: forall (n :: Natural) (m :: Natural). ((n + 1) <= ElementCount (Either a b), n <= m, (m + 1) <= ElementCount (Either a b)) => SNat n -> SNat m -> Vec ((m - n) + 1) (Either a b) Source #

Finite (Proxy a) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (Proxy a) :: Nat Source #

Methods

elements :: Vec (ElementCount (Proxy a)) (Proxy a) Source #

lowest :: Proxy a Source #

lowestMaybe :: Maybe (Proxy a) Source #

highest :: Proxy a Source #

highestMaybe :: Maybe (Proxy a) Source #

predMaybe :: Proxy a -> Maybe (Proxy a) Source #

succMaybe :: Proxy a -> Maybe (Proxy a) Source #

ith :: Index (ElementCount (Proxy a)) -> Proxy a Source #

index :: Proxy a -> Index (ElementCount (Proxy a)) Source #

elementsFrom :: forall (n :: Natural). (n + 1) <= ElementCount (Proxy a) => SNat n -> Vec (ElementCount (Proxy a) - n) (Proxy a) Source #

elementsFromTo :: forall (n :: Natural) (m :: Natural). ((n + 1) <= ElementCount (Proxy a), n <= m, (m + 1) <= ElementCount (Proxy a)) => SNat n -> SNat m -> Vec ((m - n) + 1) (Proxy a) Source #

(Bounded a, Enum a, Eq a, KnownNat n, 1 <= n) => Finite (BoundedEnumEq n a) Source #

see BoundedEnumEq

Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (BoundedEnumEq n a) :: Nat Source #

(KnownNat d, Finite a) => Finite (RTree d a) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (RTree d a) :: Nat Source #

Methods

elements :: Vec (ElementCount (RTree d a)) (RTree d a) Source #

lowest :: RTree d a Source #

lowestMaybe :: Maybe (RTree d a) Source #

highest :: RTree d a Source #

highestMaybe :: Maybe (RTree d a) Source #

predMaybe :: RTree d a -> Maybe (RTree d a) Source #

succMaybe :: RTree d a -> Maybe (RTree d a) Source #

ith :: Index (ElementCount (RTree d a)) -> RTree d a Source #

index :: RTree d a -> Index (ElementCount (RTree d a)) Source #

elementsFrom :: forall (n :: Natural). (n + 1) <= ElementCount (RTree d a) => SNat n -> Vec (ElementCount (RTree d a) - n) (RTree d a) Source #

elementsFromTo :: forall (n :: Natural) (m :: Natural). ((n + 1) <= ElementCount (RTree d a), n <= m, (m + 1) <= ElementCount (RTree d a)) => SNat n -> SNat m -> Vec ((m - n) + 1) (RTree d a) Source #

(KnownNat n, Finite a) => Finite (Vec n a) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (Vec n a) :: Nat Source #

Methods

elements :: Vec (ElementCount (Vec n a)) (Vec n a) Source #

lowest :: Vec n a Source #

lowestMaybe :: Maybe (Vec n a) Source #

highest :: Vec n a Source #

highestMaybe :: Maybe (Vec n a) Source #

predMaybe :: Vec n a -> Maybe (Vec n a) Source #

succMaybe :: Vec n a -> Maybe (Vec n a) Source #

ith :: Index (ElementCount (Vec n a)) -> Vec n a Source #

index :: Vec n a -> Index (ElementCount (Vec n a)) Source #

elementsFrom :: forall (n0 :: Natural). (n0 + 1) <= ElementCount (Vec n a) => SNat n0 -> Vec (ElementCount (Vec n a) - n0) (Vec n a) Source #

elementsFromTo :: forall (n0 :: Natural) (m :: Natural). ((n0 + 1) <= ElementCount (Vec n a), n0 <= m, (m + 1) <= ElementCount (Vec n a)) => SNat n0 -> SNat m -> Vec ((m - n0) + 1) (Vec n a) Source #

(Finite a, Finite b) => Finite (a, b) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (a, b) :: Nat Source #

Methods

elements :: Vec (ElementCount (a, b)) (a, b) Source #

lowest :: (a, b) Source #

lowestMaybe :: Maybe (a, b) Source #

highest :: (a, b) Source #

highestMaybe :: Maybe (a, b) Source #

predMaybe :: (a, b) -> Maybe (a, b) Source #

succMaybe :: (a, b) -> Maybe (a, b) Source #

ith :: Index (ElementCount (a, b)) -> (a, b) Source #

index :: (a, b) -> Index (ElementCount (a, b)) Source #

elementsFrom :: forall (n :: Natural). (n + 1) <= ElementCount (a, b) => SNat n -> Vec (ElementCount (a, b) - n) (a, b) Source #

elementsFromTo :: forall (n :: Natural) (m :: Natural). ((n + 1) <= ElementCount (a, b), n <= m, (m + 1) <= ElementCount (a, b)) => SNat n -> SNat m -> Vec ((m - n) + 1) (a, b) Source #

(Finite a, Finite b) => Finite (a -> b) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (a -> b) :: Nat Source #

Methods

elements :: Vec (ElementCount (a -> b)) (a -> b) Source #

lowest :: a -> b Source #

lowestMaybe :: Maybe (a -> b) Source #

highest :: a -> b Source #

highestMaybe :: Maybe (a -> b) Source #

predMaybe :: (a -> b) -> Maybe (a -> b) Source #

succMaybe :: (a -> b) -> Maybe (a -> b) Source #

ith :: Index (ElementCount (a -> b)) -> a -> b Source #

index :: (a -> b) -> Index (ElementCount (a -> b)) Source #

elementsFrom :: forall (n :: Natural). (n + 1) <= ElementCount (a -> b) => SNat n -> Vec (ElementCount (a -> b) - n) (a -> b) Source #

elementsFromTo :: forall (n :: Natural) (m :: Natural). ((n + 1) <= ElementCount (a -> b), n <= m, (m + 1) <= ElementCount (a -> b)) => SNat n -> SNat m -> Vec ((m - n) + 1) (a -> b) Source #

Finite a => Finite (Const a b) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (Const a b) :: Nat Source #

Methods

elements :: Vec (ElementCount (Const a b)) (Const a b) Source #

lowest :: Const a b Source #

lowestMaybe :: Maybe (Const a b) Source #

highest :: Const a b Source #

highestMaybe :: Maybe (Const a b) Source #

predMaybe :: Const a b -> Maybe (Const a b) Source #

succMaybe :: Const a b -> Maybe (Const a b) Source #

ith :: Index (ElementCount (Const a b)) -> Const a b Source #

index :: Const a b -> Index (ElementCount (Const a b)) Source #

elementsFrom :: forall (n :: Natural). (n + 1) <= ElementCount (Const a b) => SNat n -> Vec (ElementCount (Const a b) - n) (Const a b) Source #

elementsFromTo :: forall (n :: Natural) (m :: Natural). ((n + 1) <= ElementCount (Const a b), n <= m, (m + 1) <= ElementCount (Const a b)) => SNat n -> SNat m -> Vec ((m - n) + 1) (Const a b) Source #

a ~ b => Finite (a :~: b) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (a :~: b) :: Nat Source #

Methods

elements :: Vec (ElementCount (a :~: b)) (a :~: b) Source #

lowest :: a :~: b Source #

lowestMaybe :: Maybe (a :~: b) Source #

highest :: a :~: b Source #

highestMaybe :: Maybe (a :~: b) Source #

predMaybe :: (a :~: b) -> Maybe (a :~: b) Source #

succMaybe :: (a :~: b) -> Maybe (a :~: b) Source #

ith :: Index (ElementCount (a :~: b)) -> a :~: b Source #

index :: (a :~: b) -> Index (ElementCount (a :~: b)) Source #

elementsFrom :: forall (n :: Natural). (n + 1) <= ElementCount (a :~: b) => SNat n -> Vec (ElementCount (a :~: b) - n) (a :~: b) Source #

elementsFromTo :: forall (n :: Natural) (m :: Natural). ((n + 1) <= ElementCount (a :~: b), n <= m, (m + 1) <= ElementCount (a :~: b)) => SNat n -> SNat m -> Vec ((m - n) + 1) (a :~: b) Source #

(Finite a1, Finite (a2, a3)) => Finite (a1, a2, a3) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (a1, a2, a3) :: Nat Source #

Methods

elements :: Vec (ElementCount (a1, a2, a3)) (a1, a2, a3) Source #

lowest :: (a1, a2, a3) Source #

lowestMaybe :: Maybe (a1, a2, a3) Source #

highest :: (a1, a2, a3) Source #

highestMaybe :: Maybe (a1, a2, a3) Source #

predMaybe :: (a1, a2, a3) -> Maybe (a1, a2, a3) Source #

succMaybe :: (a1, a2, a3) -> Maybe (a1, a2, a3) Source #

ith :: Index (ElementCount (a1, a2, a3)) -> (a1, a2, a3) Source #

index :: (a1, a2, a3) -> Index (ElementCount (a1, a2, a3)) Source #

elementsFrom :: forall (n :: Natural). (n + 1) <= ElementCount (a1, a2, a3) => SNat n -> Vec (ElementCount (a1, a2, a3) - n) (a1, a2, a3) Source #

elementsFromTo :: forall (n :: Natural) (m :: Natural). ((n + 1) <= ElementCount (a1, a2, a3), n <= m, (m + 1) <= ElementCount (a1, a2, a3)) => SNat n -> SNat m -> Vec ((m - n) + 1) (a1, a2, a3) Source #

(Finite (f a), Finite (g a)) => Finite (Product f g a) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (Product f g a) :: Nat Source #

Methods

elements :: Vec (ElementCount (Product f g a)) (Product f g a) Source #

lowest :: Product f g a Source #

lowestMaybe :: Maybe (Product f g a) Source #

highest :: Product f g a Source #

highestMaybe :: Maybe (Product f g a) Source #

predMaybe :: Product f g a -> Maybe (Product f g a) Source #

succMaybe :: Product f g a -> Maybe (Product f g a) Source #

ith :: Index (ElementCount (Product f g a)) -> Product f g a Source #

index :: Product f g a -> Index (ElementCount (Product f g a)) Source #

elementsFrom :: forall (n :: Natural). (n + 1) <= ElementCount (Product f g a) => SNat n -> Vec (ElementCount (Product f g a) - n) (Product f g a) Source #

elementsFromTo :: forall (n :: Natural) (m :: Natural). ((n + 1) <= ElementCount (Product f g a), n <= m, (m + 1) <= ElementCount (Product f g a)) => SNat n -> SNat m -> Vec ((m - n) + 1) (Product f g a) Source #

(Finite (f a), Finite (g a)) => Finite (Sum f g a) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (Sum f g a) :: Nat Source #

Methods

elements :: Vec (ElementCount (Sum f g a)) (Sum f g a) Source #

lowest :: Sum f g a Source #

lowestMaybe :: Maybe (Sum f g a) Source #

highest :: Sum f g a Source #

highestMaybe :: Maybe (Sum f g a) Source #

predMaybe :: Sum f g a -> Maybe (Sum f g a) Source #

succMaybe :: Sum f g a -> Maybe (Sum f g a) Source #

ith :: Index (ElementCount (Sum f g a)) -> Sum f g a Source #

index :: Sum f g a -> Index (ElementCount (Sum f g a)) Source #

elementsFrom :: forall (n :: Natural). (n + 1) <= ElementCount (Sum f g a) => SNat n -> Vec (ElementCount (Sum f g a) - n) (Sum f g a) Source #

elementsFromTo :: forall (n :: Natural) (m :: Natural). ((n + 1) <= ElementCount (Sum f g a), n <= m, (m + 1) <= ElementCount (Sum f g a)) => SNat n -> SNat m -> Vec ((m - n) + 1) (Sum f g a) Source #

a ~~ b => Finite (a :~~: b) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (a :~~: b) :: Nat Source #

Methods

elements :: Vec (ElementCount (a :~~: b)) (a :~~: b) Source #

lowest :: a :~~: b Source #

lowestMaybe :: Maybe (a :~~: b) Source #

highest :: a :~~: b Source #

highestMaybe :: Maybe (a :~~: b) Source #

predMaybe :: (a :~~: b) -> Maybe (a :~~: b) Source #

succMaybe :: (a :~~: b) -> Maybe (a :~~: b) Source #

ith :: Index (ElementCount (a :~~: b)) -> a :~~: b Source #

index :: (a :~~: b) -> Index (ElementCount (a :~~: b)) Source #

elementsFrom :: forall (n :: Natural). (n + 1) <= ElementCount (a :~~: b) => SNat n -> Vec (ElementCount (a :~~: b) - n) (a :~~: b) Source #

elementsFromTo :: forall (n :: Natural) (m :: Natural). ((n + 1) <= ElementCount (a :~~: b), n <= m, (m + 1) <= ElementCount (a :~~: b)) => SNat n -> SNat m -> Vec ((m - n) + 1) (a :~~: b) Source #

(Finite a1, Finite (a2, a3, a4)) => Finite (a1, a2, a3, a4) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (a1, a2, a3, a4) :: Nat Source #

Methods

elements :: Vec (ElementCount (a1, a2, a3, a4)) (a1, a2, a3, a4) Source #

lowest :: (a1, a2, a3, a4) Source #

lowestMaybe :: Maybe (a1, a2, a3, a4) Source #

highest :: (a1, a2, a3, a4) Source #

highestMaybe :: Maybe (a1, a2, a3, a4) Source #

predMaybe :: (a1, a2, a3, a4) -> Maybe (a1, a2, a3, a4) Source #

succMaybe :: (a1, a2, a3, a4) -> Maybe (a1, a2, a3, a4) Source #

ith :: Index (ElementCount (a1, a2, a3, a4)) -> (a1, a2, a3, a4) Source #

index :: (a1, a2, a3, a4) -> Index (ElementCount (a1, a2, a3, a4)) Source #

elementsFrom :: forall (n :: Natural). (n + 1) <= ElementCount (a1, a2, a3, a4) => SNat n -> Vec (ElementCount (a1, a2, a3, a4) - n) (a1, a2, a3, a4) Source #

elementsFromTo :: forall (n :: Natural) (m :: Natural). ((n + 1) <= ElementCount (a1, a2, a3, a4), n <= m, (m + 1) <= ElementCount (a1, a2, a3, a4)) => SNat n -> SNat m -> Vec ((m - n) + 1) (a1, a2, a3, a4) Source #

Finite (f (g a)) => Finite (Compose f g a) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (Compose f g a) :: Nat Source #

Methods

elements :: Vec (ElementCount (Compose f g a)) (Compose f g a) Source #

lowest :: Compose f g a Source #

lowestMaybe :: Maybe (Compose f g a) Source #

highest :: Compose f g a Source #

highestMaybe :: Maybe (Compose f g a) Source #

predMaybe :: Compose f g a -> Maybe (Compose f g a) Source #

succMaybe :: Compose f g a -> Maybe (Compose f g a) Source #

ith :: Index (ElementCount (Compose f g a)) -> Compose f g a Source #

index :: Compose f g a -> Index (ElementCount (Compose f g a)) Source #

elementsFrom :: forall (n :: Natural). (n + 1) <= ElementCount (Compose f g a) => SNat n -> Vec (ElementCount (Compose f g a) - n) (Compose f g a) Source #

elementsFromTo :: forall (n :: Natural) (m :: Natural). ((n + 1) <= ElementCount (Compose f g a), n <= m, (m + 1) <= ElementCount (Compose f g a)) => SNat n -> SNat m -> Vec ((m - n) + 1) (Compose f g a) Source #

(Finite a1, Finite (a2, a3, a4, a5)) => Finite (a1, a2, a3, a4, a5) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (a1, a2, a3, a4, a5) :: Nat Source #

Methods

elements :: Vec (ElementCount (a1, a2, a3, a4, a5)) (a1, a2, a3, a4, a5) Source #

lowest :: (a1, a2, a3, a4, a5) Source #

lowestMaybe :: Maybe (a1, a2, a3, a4, a5) Source #

highest :: (a1, a2, a3, a4, a5) Source #

highestMaybe :: Maybe (a1, a2, a3, a4, a5) Source #

predMaybe :: (a1, a2, a3, a4, a5) -> Maybe (a1, a2, a3, a4, a5) Source #

succMaybe :: (a1, a2, a3, a4, a5) -> Maybe (a1, a2, a3, a4, a5) Source #

ith :: Index (ElementCount (a1, a2, a3, a4, a5)) -> (a1, a2, a3, a4, a5) Source #

index :: (a1, a2, a3, a4, a5) -> Index (ElementCount (a1, a2, a3, a4, a5)) Source #

elementsFrom :: forall (n :: Natural). (n + 1) <= ElementCount (a1, a2, a3, a4, a5) => SNat n -> Vec (ElementCount (a1, a2, a3, a4, a5) - n) (a1, a2, a3, a4, a5) Source #

elementsFromTo :: forall (n :: Natural) (m :: Natural). ((n + 1) <= ElementCount (a1, a2, a3, a4, a5), n <= m, (m + 1) <= ElementCount (a1, a2, a3, a4, a5)) => SNat n -> SNat m -> Vec ((m - n) + 1) (a1, a2, a3, a4, a5) Source #

(Finite a1, Finite (a2, a3, a4, a5, a6)) => Finite (a1, a2, a3, a4, a5, a6) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (a1, a2, a3, a4, a5, a6) :: Nat Source #

Methods

elements :: Vec (ElementCount (a1, a2, a3, a4, a5, a6)) (a1, a2, a3, a4, a5, a6) Source #

lowest :: (a1, a2, a3, a4, a5, a6) Source #

lowestMaybe :: Maybe (a1, a2, a3, a4, a5, a6) Source #

highest :: (a1, a2, a3, a4, a5, a6) Source #

highestMaybe :: Maybe (a1, a2, a3, a4, a5, a6) Source #

predMaybe :: (a1, a2, a3, a4, a5, a6) -> Maybe (a1, a2, a3, a4, a5, a6) Source #

succMaybe :: (a1, a2, a3, a4, a5, a6) -> Maybe (a1, a2, a3, a4, a5, a6) Source #

ith :: Index (ElementCount (a1, a2, a3, a4, a5, a6)) -> (a1, a2, a3, a4, a5, a6) Source #

index :: (a1, a2, a3, a4, a5, a6) -> Index (ElementCount (a1, a2, a3, a4, a5, a6)) Source #

elementsFrom :: forall (n :: Natural). (n + 1) <= ElementCount (a1, a2, a3, a4, a5, a6) => SNat n -> Vec (ElementCount (a1, a2, a3, a4, a5, a6) - n) (a1, a2, a3, a4, a5, a6) Source #

elementsFromTo :: forall (n :: Natural) (m :: Natural). ((n + 1) <= ElementCount (a1, a2, a3, a4, a5, a6), n <= m, (m + 1) <= ElementCount (a1, a2, a3, a4, a5, a6)) => SNat n -> SNat m -> Vec ((m - n) + 1) (a1, a2, a3, a4, a5, a6) Source #

(Finite a1, Finite (a2, a3, a4, a5, a6, a7)) => Finite (a1, a2, a3, a4, a5, a6, a7) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (a1, a2, a3, a4, a5, a6, a7) :: Nat Source #

Methods

elements :: Vec (ElementCount (a1, a2, a3, a4, a5, a6, a7)) (a1, a2, a3, a4, a5, a6, a7) Source #

lowest :: (a1, a2, a3, a4, a5, a6, a7) Source #

lowestMaybe :: Maybe (a1, a2, a3, a4, a5, a6, a7) Source #

highest :: (a1, a2, a3, a4, a5, a6, a7) Source #

highestMaybe :: Maybe (a1, a2, a3, a4, a5, a6, a7) Source #

predMaybe :: (a1, a2, a3, a4, a5, a6, a7) -> Maybe (a1, a2, a3, a4, a5, a6, a7) Source #

succMaybe :: (a1, a2, a3, a4, a5, a6, a7) -> Maybe (a1, a2, a3, a4, a5, a6, a7) Source #

ith :: Index (ElementCount (a1, a2, a3, a4, a5, a6, a7)) -> (a1, a2, a3, a4, a5, a6, a7) Source #

index :: (a1, a2, a3, a4, a5, a6, a7) -> Index (ElementCount (a1, a2, a3, a4, a5, a6, a7)) Source #

elementsFrom :: forall (n :: Natural). (n + 1) <= ElementCount (a1, a2, a3, a4, a5, a6, a7) => SNat n -> Vec (ElementCount (a1, a2, a3, a4, a5, a6, a7) - n) (a1, a2, a3, a4, a5, a6, a7) Source #

elementsFromTo :: forall (n :: Natural) (m :: Natural). ((n + 1) <= ElementCount (a1, a2, a3, a4, a5, a6, a7), n <= m, (m + 1) <= ElementCount (a1, a2, a3, a4, a5, a6, a7)) => SNat n -> SNat m -> Vec ((m - n) + 1) (a1, a2, a3, a4, a5, a6, a7) Source #

(Finite a1, Finite (a2, a3, a4, a5, a6, a7, a8)) => Finite (a1, a2, a3, a4, a5, a6, a7, a8) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (a1, a2, a3, a4, a5, a6, a7, a8) :: Nat Source #

Methods

elements :: Vec (ElementCount (a1, a2, a3, a4, a5, a6, a7, a8)) (a1, a2, a3, a4, a5, a6, a7, a8) Source #

lowest :: (a1, a2, a3, a4, a5, a6, a7, a8) Source #

lowestMaybe :: Maybe (a1, a2, a3, a4, a5, a6, a7, a8) Source #

highest :: (a1, a2, a3, a4, a5, a6, a7, a8) Source #

highestMaybe :: Maybe (a1, a2, a3, a4, a5, a6, a7, a8) Source #

predMaybe :: (a1, a2, a3, a4, a5, a6, a7, a8) -> Maybe (a1, a2, a3, a4, a5, a6, a7, a8) Source #

succMaybe :: (a1, a2, a3, a4, a5, a6, a7, a8) -> Maybe (a1, a2, a3, a4, a5, a6, a7, a8) Source #

ith :: Index (ElementCount (a1, a2, a3, a4, a5, a6, a7, a8)) -> (a1, a2, a3, a4, a5, a6, a7, a8) Source #

index :: (a1, a2, a3, a4, a5, a6, a7, a8) -> Index (ElementCount (a1, a2, a3, a4, a5, a6, a7, a8)) Source #

elementsFrom :: forall (n :: Natural). (n + 1) <= ElementCount (a1, a2, a3, a4, a5, a6, a7, a8) => SNat n -> Vec (ElementCount (a1, a2, a3, a4, a5, a6, a7, a8) - n) (a1, a2, a3, a4, a5, a6, a7, a8) Source #

elementsFromTo :: forall (n :: Natural) (m :: Natural). ((n + 1) <= ElementCount (a1, a2, a3, a4, a5, a6, a7, a8), n <= m, (m + 1) <= ElementCount (a1, a2, a3, a4, a5, a6, a7, a8)) => SNat n -> SNat m -> Vec ((m - n) + 1) (a1, a2, a3, a4, a5, a6, a7, a8) Source #

(Finite a1, Finite (a2, a3, a4, a5, a6, a7, a8, a9)) => Finite (a1, a2, a3, a4, a5, a6, a7, a8, a9) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (a1, a2, a3, a4, a5, a6, a7, a8, a9) :: Nat Source #

Methods

elements :: Vec (ElementCount (a1, a2, a3, a4, a5, a6, a7, a8, a9)) (a1, a2, a3, a4, a5, a6, a7, a8, a9) Source #

lowest :: (a1, a2, a3, a4, a5, a6, a7, a8, a9) Source #

lowestMaybe :: Maybe (a1, a2, a3, a4, a5, a6, a7, a8, a9) Source #

highest :: (a1, a2, a3, a4, a5, a6, a7, a8, a9) Source #

highestMaybe :: Maybe (a1, a2, a3, a4, a5, a6, a7, a8, a9) Source #

predMaybe :: (a1, a2, a3, a4, a5, a6, a7, a8, a9) -> Maybe (a1, a2, a3, a4, a5, a6, a7, a8, a9) Source #

succMaybe :: (a1, a2, a3, a4, a5, a6, a7, a8, a9) -> Maybe (a1, a2, a3, a4, a5, a6, a7, a8, a9) Source #

ith :: Index (ElementCount (a1, a2, a3, a4, a5, a6, a7, a8, a9)) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9) Source #

index :: (a1, a2, a3, a4, a5, a6, a7, a8, a9) -> Index (ElementCount (a1, a2, a3, a4, a5, a6, a7, a8, a9)) Source #

elementsFrom :: forall (n :: Natural). (n + 1) <= ElementCount (a1, a2, a3, a4, a5, a6, a7, a8, a9) => SNat n -> Vec (ElementCount (a1, a2, a3, a4, a5, a6, a7, a8, a9) - n) (a1, a2, a3, a4, a5, a6, a7, a8, a9) Source #

elementsFromTo :: forall (n :: Natural) (m :: Natural). ((n + 1) <= ElementCount (a1, a2, a3, a4, a5, a6, a7, a8, a9), n <= m, (m + 1) <= ElementCount (a1, a2, a3, a4, a5, a6, a7, a8, a9)) => SNat n -> SNat m -> Vec ((m - n) + 1) (a1, a2, a3, a4, a5, a6, a7, a8, a9) Source #

(Finite a1, Finite (a2, a3, a4, a5, a6, a7, a8, a9, a10)) => Finite (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) :: Nat Source #

Methods

elements :: Vec (ElementCount (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10)) (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) Source #

lowest :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) Source #

lowestMaybe :: Maybe (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) Source #

highest :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) Source #

highestMaybe :: Maybe (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) Source #

predMaybe :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) -> Maybe (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) Source #

succMaybe :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) -> Maybe (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) Source #

ith :: Index (ElementCount (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10)) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) Source #

index :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) -> Index (ElementCount (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10)) Source #

elementsFrom :: forall (n :: Natural). (n + 1) <= ElementCount (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) => SNat n -> Vec (ElementCount (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) - n) (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) Source #

elementsFromTo :: forall (n :: Natural) (m :: Natural). ((n + 1) <= ElementCount (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10), n <= m, (m + 1) <= ElementCount (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10)) => SNat n -> SNat m -> Vec ((m - n) + 1) (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) Source #

(Finite a1, Finite (a2, a3, a4, a5, a6, a7, a8, a9, a10, a11)) => Finite (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) :: Nat Source #

Methods

elements :: Vec (ElementCount (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11)) (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) Source #

lowest :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) Source #

lowestMaybe :: Maybe (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) Source #

highest :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) Source #

highestMaybe :: Maybe (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) Source #

predMaybe :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) -> Maybe (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) Source #

succMaybe :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) -> Maybe (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) Source #

ith :: Index (ElementCount (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11)) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) Source #

index :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) -> Index (ElementCount (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11)) Source #

elementsFrom :: forall (n :: Natural). (n + 1) <= ElementCount (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) => SNat n -> Vec (ElementCount (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) - n) (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) Source #

elementsFromTo :: forall (n :: Natural) (m :: Natural). ((n + 1) <= ElementCount (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11), n <= m, (m + 1) <= ElementCount (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11)) => SNat n -> SNat m -> Vec ((m - n) + 1) (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) Source #

(Finite a1, Finite (a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12)) => Finite (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) :: Nat Source #

Methods

elements :: Vec (ElementCount (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12)) (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) Source #

lowest :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) Source #

lowestMaybe :: Maybe (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) Source #

highest :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) Source #

highestMaybe :: Maybe (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) Source #

predMaybe :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) -> Maybe (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) Source #

succMaybe :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) -> Maybe (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) Source #

ith :: Index (ElementCount (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12)) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) Source #

index :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) -> Index (ElementCount (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12)) Source #

elementsFrom :: forall (n :: Natural). (n + 1) <= ElementCount (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) => SNat n -> Vec (ElementCount (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) - n) (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) Source #

elementsFromTo :: forall (n :: Natural) (m :: Natural). ((n + 1) <= ElementCount (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12), n <= m, (m + 1) <= ElementCount (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12)) => SNat n -> SNat m -> Vec ((m - n) + 1) (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) Source #

class KnownNat (GElementCount rep) => GFinite rep where Source #

The Generic interfaces of Finite.

Associated Types

type GElementCount rep :: Nat Source #

Methods

gElements :: Vec (GElementCount rep) (rep a) Source #

gLowest :: 1 <= GElementCount rep => rep a Source #

gLowestMaybe :: Maybe (rep a) Source #

gHighest :: 1 <= GElementCount rep => rep a Source #

gHighestMaybe :: Maybe (rep a) Source #

gPredMaybe :: rep a -> Maybe (rep a) Source #

gSuccMaybe :: rep a -> Maybe (rep a) Source #

gIth :: Index (GElementCount rep) -> rep a Source #

gIndex :: rep a -> Index (GElementCount rep) Source #

Instances

Instances details
GFinite (U1 :: Type -> Type) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type GElementCount U1 :: Nat Source #

GFinite (V1 :: Type -> Type) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type GElementCount V1 :: Nat Source #

(GFinite a, GFinite b) => GFinite (a :*: b) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type GElementCount (a :*: b) :: Nat Source #

Methods

gElements :: Vec (GElementCount (a :*: b)) ((a :*: b) a0) Source #

gLowest :: 1 <= GElementCount (a :*: b) => (a :*: b) a0 Source #

gLowestMaybe :: Maybe ((a :*: b) a0) Source #

gHighest :: 1 <= GElementCount (a :*: b) => (a :*: b) a0 Source #

gHighestMaybe :: Maybe ((a :*: b) a0) Source #

gPredMaybe :: (a :*: b) a0 -> Maybe ((a :*: b) a0) Source #

gSuccMaybe :: (a :*: b) a0 -> Maybe ((a :*: b) a0) Source #

gIth :: Index (GElementCount (a :*: b)) -> (a :*: b) a0 Source #

gIndex :: (a :*: b) a0 -> Index (GElementCount (a :*: b)) Source #

(GFinite a, GFinite b) => GFinite (a :+: b) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type GElementCount (a :+: b) :: Nat Source #

Methods

gElements :: Vec (GElementCount (a :+: b)) ((a :+: b) a0) Source #

gLowest :: 1 <= GElementCount (a :+: b) => (a :+: b) a0 Source #

gLowestMaybe :: Maybe ((a :+: b) a0) Source #

gHighest :: 1 <= GElementCount (a :+: b) => (a :+: b) a0 Source #

gHighestMaybe :: Maybe ((a :+: b) a0) Source #

gPredMaybe :: (a :+: b) a0 -> Maybe ((a :+: b) a0) Source #

gSuccMaybe :: (a :+: b) a0 -> Maybe ((a :+: b) a0) Source #

gIth :: Index (GElementCount (a :+: b)) -> (a :+: b) a0 Source #

gIndex :: (a :+: b) a0 -> Index (GElementCount (a :+: b)) Source #

Finite a => GFinite (K1 i a :: Type -> Type) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type GElementCount (K1 i a) :: Nat Source #

Methods

gElements :: Vec (GElementCount (K1 i a)) (K1 i a a0) Source #

gLowest :: 1 <= GElementCount (K1 i a) => K1 i a a0 Source #

gLowestMaybe :: Maybe (K1 i a a0) Source #

gHighest :: 1 <= GElementCount (K1 i a) => K1 i a a0 Source #

gHighestMaybe :: Maybe (K1 i a a0) Source #

gPredMaybe :: K1 i a a0 -> Maybe (K1 i a a0) Source #

gSuccMaybe :: K1 i a a0 -> Maybe (K1 i a a0) Source #

gIth :: Index (GElementCount (K1 i a)) -> K1 i a a0 Source #

gIndex :: K1 i a a0 -> Index (GElementCount (K1 i a)) Source #

GFinite a => GFinite (M1 i v a) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type GElementCount (M1 i v a) :: Nat Source #

Methods

gElements :: Vec (GElementCount (M1 i v a)) (M1 i v a a0) Source #

gLowest :: 1 <= GElementCount (M1 i v a) => M1 i v a a0 Source #

gLowestMaybe :: Maybe (M1 i v a a0) Source #

gHighest :: 1 <= GElementCount (M1 i v a) => M1 i v a a0 Source #

gHighestMaybe :: Maybe (M1 i v a a0) Source #

gPredMaybe :: M1 i v a a0 -> Maybe (M1 i v a a0) Source #

gSuccMaybe :: M1 i v a a0 -> Maybe (M1 i v a a0) Source #

gIth :: Index (GElementCount (M1 i v a)) -> M1 i v a a0 Source #

gIndex :: M1 i v a a0 -> Index (GElementCount (M1 i v a)) Source #

Extensions

newtype GenericReverse a Source #

A newtype wrapper that reverses the index order, which normally would be used by the Finite instance of the inner type via Generic deriving. The newtype is only intended be used with the DerivingVia strategy and custom data types, while you should use Down in any other case introducing equivalent behavior.

The reason why we introduce an additional newtype to Down here results from how generics play together with via deriving strategies. For example, if you like to have an Signed n with a reversed index order, then you can introduce a newtype for that and derive the Finite instance via Down, e.g.,

newtype DownSigned n = DownSigned (Signed n) deriving newtype (Generic)
deriving via Down (Signed n) instance KnownNat n => Finite (DownSigned)

However, if you create your own new data type T, then it might be desirable to use a reversed order right for that type T and not Down T. However, the following does not work

data T = A (DownSigned 3) | B Bool deriving (Generic)
deriving via Down T instance Finite T

as in this case the deriving strategy already requires an Finite instance for T. The issue is resolved by using GenericReverse instead.

deriving via GenericReverse T instance Finite T

Constructors

GenericReverse 

Fields

newtype WithUndefined a Source #

The elements of the Bit and BitVector types may have undefined bits, which are not in scope when using their default Finite class instances. The default instances only consider the synthesizable fragment of the types, while for simulation or testing purposes, it may be useful to have access to the range of undefined inhabitants as well.

The Finite instances of WithUndefined Bit and WithUndefined (BitVector n) also add the elements containing undefined bits, but are not synthesizable as a consequence. They make use of a special index order, that first enumerates all well-defined values, i.e., those that have no undefined bits, and then continues with the non-well-defined ones.

>>> elements @(BitVector 2)
0b00 :> 0b01 :> 0b10 :> 0b11 :> Nil
>>> elements @(WithUndefined (BitVector 2))
0b00 :> 0b01 :> 0b10 :> 0b11 :> 0b0. :> 0b1. :> 0b.0 :> 0b.1 :> 0b.. :> Nil

Constructors

WithUndefined 

Fields

Instances

Instances details
Bits a => Bits (WithUndefined a) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

FiniteBits a => FiniteBits (WithUndefined a) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Bounded a => Bounded (WithUndefined a) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Enum a => Enum (WithUndefined a) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Generic a => Generic (WithUndefined a) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type Rep (WithUndefined a) :: Type -> Type #

Num a => Num (WithUndefined a) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Read a => Read (WithUndefined a) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Integral a => Integral (WithUndefined a) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Real a => Real (WithUndefined a) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Show a => Show (WithUndefined a) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Finite (WithUndefined Bit) Source #

NB: not synthesizable (see WithUndefined)

Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (WithUndefined Bit) :: Nat Source #

KnownNat n => Finite (WithUndefined (BitVector n)) Source #

NB: not synthesizable (see WithUndefined)

Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type ElementCount (WithUndefined (BitVector n)) :: Nat Source #

BitPack a => BitPack (WithUndefined a) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Associated Types

type BitSize (WithUndefined a) :: Nat #

NFDataX a => NFDataX (WithUndefined a) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

ShowX a => ShowX (WithUndefined a) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Eq a => Eq (WithUndefined a) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Ord a => Ord (WithUndefined a) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

type Rep (WithUndefined a) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

type Rep (WithUndefined a) = Rep a
type ElementCount (WithUndefined Bit) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

type ElementCount (WithUndefined (BitVector n)) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

type BitSize (WithUndefined a) Source # 
Instance details

Defined in Clash.Class.Finite.Internal

Deriving Helpers

newtype FiniteDerive a Source #

A newtype wrapper for implementing deriving strategies of classes whose implementation may follow from Finite, e.g., the Enum class.

Constructors

FiniteDerive 

Fields

newtype BoundedEnumEq (n :: Nat) a Source #

A newtype wrapper for deriving Finite instances from existing instances of Bounded, Enum, and Eq, where Eq is only utilized for efficiency reasons although it is not strictly necessary.

Constructors

BoundedEnumEq 

Fields