| Copyright | (C) 2024-2025 Felix Klein |
|---|---|
| License | MIT (see the file LICENSE) |
| Maintainer | Felix Klein <felix@qbaylogic.com> |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
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 -> aEnum (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
Synopsis
- class KnownNat (ElementCount a) => Finite a where
- type ElementCount a :: Nat
- elements :: Vec (ElementCount a) a
- lowest :: 1 <= ElementCount a => a
- lowestMaybe :: Maybe a
- highest :: 1 <= ElementCount a => a
- highestMaybe :: Maybe a
- predMaybe :: a -> Maybe a
- succMaybe :: a -> Maybe a
- ith :: Index (ElementCount a) -> a
- index :: a -> Index (ElementCount a)
- elementsFrom :: (n + 1) <= ElementCount a => SNat n -> Vec (ElementCount a - n) a
- elementsFromTo :: ((n + 1) <= ElementCount a, n <= m, (m + 1) <= ElementCount a) => SNat n -> SNat m -> Vec ((m - n) + 1) a
- class KnownNat (GElementCount rep) => GFinite rep where
- type GElementCount rep :: Nat
- gElements :: Vec (GElementCount rep) (rep a)
- gLowest :: 1 <= GElementCount rep => rep a
- gLowestMaybe :: Maybe (rep a)
- gHighest :: 1 <= GElementCount rep => rep a
- gHighestMaybe :: Maybe (rep a)
- gPredMaybe :: rep a -> Maybe (rep a)
- gSuccMaybe :: rep a -> Maybe (rep a)
- gIth :: Index (GElementCount rep) -> rep a
- gIndex :: rep a -> Index (GElementCount rep)
- newtype GenericReverse a = GenericReverse {
- getGenericReverse :: a
- newtype WithUndefined a = WithUndefined {
- getWithUndefined :: a
- newtype FiniteDerive a = FiniteDerive {
- getFiniteDerive :: a
- newtype BoundedEnumEq (n :: Nat) a = BoundedEnumEq {
- getBoundedEnumEq :: a
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 @TB 0 :> B 1 :> D 0 -1 :> D 0 0 :> D 1 -1 :> D 1 0 :> Nil>>>lowestMaybe @TJust (B 0)>>>highestMaybe @TJust (D 1 0)>>>succMaybe (B 1)Just (D 0 -1)>>>predMaybe (B 0)Nothing>>>index (D 0 0)3>>>ith @T 5D 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 =NothingElementCount a > 0: lowestMaybe @a =Justlowest, highestMaybe @a =Justhighest
If a has a Bounded instance, it further must satisfy:
If a has an Enum instance, it further must satisfy:
Minimal complete definition
Nothing
Associated Types
type ElementCount a :: Nat Source #
The number of elements of the type.
type ElementCount a = GElementCount (Rep a)
Methods
elements :: Vec (ElementCount a) a Source #
The elements of the type.
default elements :: (Generic a, GFinite (Rep a), ElementCount a ~ GElementCount (Rep a)) => Vec (ElementCount a) a Source #
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.
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.
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.
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.
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
class KnownNat (GElementCount rep) => GFinite rep where Source #
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
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 nFinite 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
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
| |
Instances
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
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
| |
Instances
| (Finite a, 1 <= ElementCount a) => Bounded (FiniteDerive a) Source # | |
Defined in Clash.Class.Finite.Internal | |
| Finite a => Enum (FiniteDerive a) Source # | |
Defined in Clash.Class.Finite.Internal Methods succ :: FiniteDerive a -> FiniteDerive a # pred :: FiniteDerive a -> FiniteDerive a # toEnum :: Int -> FiniteDerive a # fromEnum :: FiniteDerive a -> Int # enumFrom :: FiniteDerive a -> [FiniteDerive a] # enumFromThen :: FiniteDerive a -> FiniteDerive a -> [FiniteDerive a] # enumFromTo :: FiniteDerive a -> FiniteDerive a -> [FiniteDerive a] # enumFromThenTo :: FiniteDerive a -> FiniteDerive a -> FiniteDerive a -> [FiniteDerive a] # | |
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
| |