clash-finite (empty) → 1.0.0.0
raw patch · 9 files changed
+1778/−0 lines, 9 filesdep +basedep +clash-finitedep +clash-prelude
Dependencies added: base, clash-finite, clash-prelude, constraints, deepseq, ghc-typelits-extra, ghc-typelits-knownnat, ghc-typelits-natnormalise, singletons, tasty, tasty-hunit, template-haskell
Files
- CHANGELOG.md +6/−0
- LICENSE +21/−0
- clash-finite.cabal +73/−0
- src/Clash/Class/Finite.hs +44/−0
- src/Clash/Class/Finite/Internal.hs +1086/−0
- src/Clash/Class/Finite/Internal/Evidence.hs +87/−0
- src/Clash/Class/Finite/Internal/TH.hs +207/−0
- tests/Clash/Tests/Laws/Finite.hs +246/−0
- tests/Main.hs +8/−0
+ CHANGELOG.md view
@@ -0,0 +1,6 @@+# Revision history for clash-finite++## 1.0.0.0++* Initial Version: the final state of+ https://github.com/clash-lang/clash-compiler/pull/2858
+ LICENSE view
@@ -0,0 +1,21 @@+MIT License++Copyright (c) 2025 Felix Klein++Permission is hereby granted, free of charge, to any person obtaining a copy+of this software and associated documentation files (the "Software"), to deal+in the Software without restriction, including without limitation the rights+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell+copies of the Software, and to permit persons to whom the Software is+furnished to do so, subject to the following conditions:++The above copyright notice and this permission notice shall be included in all+copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE+SOFTWARE.
+ clash-finite.cabal view
@@ -0,0 +1,73 @@+cabal-version: 2.2+name: clash-finite+version: 1.0.0.0+synopsis: A class for types with only finitely many inhabitants+description: Finite is a class for types with only finitely many inhabitants+ and can be considered a more hardware-friendly alternative to+ Bounded and Enum, utilizing Index instead of Int and vectors+ instead of lists.+homepage: https://github.com/kleinreact/clash-finite+license: MIT+license-file: LICENSE+author: Felix Klein+maintainer: felix@qbaylogic.com+copyright: Copyright © 2024-2025, Felix Klein+category: Hardware+build-type: Simple+extra-doc-files: CHANGELOG.md++source-repository head+ type: git+ location: https://github.com/kleinreact/clash-finite++flag test+ description: You can disable tests via `-f-test`.+ default: True+ manual: True++flag large-tuples+ description: Generate Finite class instances for tuples up to+ and including 62 elements+ default: False+ manual: True++library+ default-language: Haskell2010+ hs-source-dirs: src+ ghc-options: -Wall -Wcompat+ if flag(large-tuples)+ CPP-Options: -DLARGE_TUPLES+ build-depends:+ , base >= 4.11 && < 5+ , clash-prelude >= 1.8 && < 1.10+ , constraints >= 0.9 && < 1.0+ , ghc-typelits-extra >= 0.4 && < 0.5+ , ghc-typelits-knownnat >= 0.7.2 && < 0.8+ , ghc-typelits-natnormalise >= 0.7.2 && < 0.8+ , singletons >= 2.0 && < 3.1+ , template-haskell >= 2.12.0.0 && < 2.23+ exposed-modules:+ Clash.Class.Finite+ Clash.Class.Finite.Internal+ Clash.Class.Finite.Internal.Evidence+ Clash.Class.Finite.Internal.TH++test-suite unittests+ default-language: Haskell2010+ hs-source-dirs: tests+ ghc-options: -Wall -Wcompat -threaded+ type: exitcode-stdio-1.0+ main-is: Main.hs+ if !flag(test)+ buildable: False+ else+ build-depends:+ , base >= 4.11 && < 5+ , clash-prelude >= 1.9 && < 1.10+ , clash-finite+ , constraints >= 0.9 && < 1.0+ , deepseq+ , tasty >= 1.2 && < 1.6+ , tasty-hunit+ other-modules:+ Clash.Tests.Laws.Finite
+ src/Clash/Class/Finite.hs view
@@ -0,0 +1,44 @@+{-|+Copyright : (C) 2024-2025, Felix Klein+License : MIT (see the file LICENSE)+Maintainer : Felix Klein <felix@qbaylogic.com>++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 'Clash.Sized.Index.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 @'Clash.Sized.Index.Index' n@+instead.+-}+module Clash.Class.Finite+ ( -- * Finite Class+ Finite(..)+ , GFinite(..)+ -- * Extensions+ , GenericReverse(..)+ , WithUndefined(..)+ -- * Deriving Helpers+ , FiniteDerive(..)+ , BoundedEnumEq(..)+ )+where++import Clash.Class.Finite.Internal
+ src/Clash/Class/Finite/Internal.hs view
@@ -0,0 +1,1086 @@+{-|+Copyright : (C) 2024-2025, Felix Klein+License : MIT (see the file LICENSE)+Maintainer : Felix Klein <felix@qbaylogic.com>+-}++{-# LANGUAGE ConstrainedClassMethods #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE MultiWayIf #-}+{-# LANGUAGE NoStarIsType #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ViewPatterns #-}++{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}+{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}++{-# OPTIONS_HADDOCK hide #-}++module Clash.Class.Finite.Internal+ ( Finite(..)+ , GFinite(..)+ , BoundedEnumEq(..)+ , FiniteDerive(..)+ , GenericReverse(..)+ , WithUndefined(..)+ )+where++import Prelude hiding ((++), (!!), concatMap, foldl, foldr, repeat, reverse)++import Control.Applicative (Alternative(..))+import Control.Arrow (second)+import Data.Bits (Bits(..), FiniteBits(..))+import Data.Coerce (coerce)+import Data.Constraint (Dict(..))+import Data.Functor.Compose (Compose(..))+import Data.Functor.Const (Const(..))+import Data.Functor.Identity (Identity(..))+import Data.Functor.Product (Product)+import Data.Functor.Sum (Sum)+import Data.Int (Int8, Int16, Int32, Int64)+import Data.Kind (Type)+import Data.Maybe (fromJust)+#if MIN_VERSION_base(4,15,0)+import Data.Ord (Down(..))+#endif+import Data.Proxy (Proxy(..))+import Data.Singletons (Apply, TyFun)+import Data.Type.Bool (If)+import Data.Type.Equality ((:~:)(..), (:~~:)(..), type (~~))+import Data.Void (Void)+import Data.Word (Word8, Word16, Word32, Word64)+import GHC.Generics+ (Generic(..), Rep, V1, U1(..), M1(..), K1(..), (:+:)(..), (:*:)(..))+import GHC.TypeNats+ ( Nat, KnownNat+ , type (^), type (<=), type (<=?), type (*), type (+), type (-)+ )+import GHC.TypeLits (KnownSymbol)++import Clash.Class.Num (SaturatingNum(..), SaturationMode(..))+import Clash.Class.Finite.Internal.Evidence+ ( powPositiveIfPositiveBase, powPositiveImpliesPositiveBase+ , mulPositiveImpliesPositiveOperands, zeroLeAdd, powMonotone1+ , powLawsRewrite+#if !MIN_VERSION_base(4,16,0)+ , pow2CLogDual, leqOnePlusMinus+#endif+ )+import Clash.Class.Finite.Internal.TH (deriveFiniteTuples)+import Clash.Class.Resize (Resize(..))+import Clash.Class.BitPack (BitPack(..), bitCoerce)+import Clash.Num.Erroring (Erroring, fromErroring, toErroring)+import Clash.Num.Overflowing (Overflowing, fromOverflowing, toOverflowing)+import Clash.Num.Saturating (Saturating, fromSaturating, toSaturating)+import Clash.Num.Wrapping (Wrapping, fromWrapping, toWrapping)+import Clash.Num.Zeroing (Zeroing, fromZeroing, toZeroing)+import Clash.Promoted.Nat+ ( SNat(..), UNat(..), SNatLE(..)+ , toUNat, fromUNat, natToNum, snatToNum, compareSNat+ )+import Clash.Promoted.Symbol (SSymbol(..))+import Clash.Sized.Index (Index)+import Clash.Sized.Internal.BitVector (BitVector(..), Bit(..), high, low)+import Clash.Sized.Internal.Unsigned (Unsigned(..))+import Clash.Sized.Signed (Signed)+import Clash.Sized.RTree (RTree(..), tdfold, tfold, trepeat)+import Clash.Sized.Vector+ ( Vec(..), (++), (!!), concatMap, bv2v, dfold, foldl, foldr+ , ifoldr, indicesI, iterateI, unfoldrI, repeat, reverse, replace+ )+import Clash.XException (ShowX, NFDataX, errorX)++import qualified Data.List as List (iterate)++{- $setup+>>> :m -Prelude+>>> :set -XDeriveAnyClass+>>> import Clash.Prelude+>>> import Data.Ord+-}++-- * Finite Class++-- | 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 @+--+class KnownNat (ElementCount a) => Finite a where+ -- | The number of elements of the type.+ type ElementCount a :: Nat+ type ElementCount a = GElementCount (Rep a)++ -- | The elements of the type.+ elements :: Vec (ElementCount a) a+ default elements ::+ ( Generic a, GFinite (Rep a)+ , ElementCount a ~ GElementCount (Rep a)+ ) => Vec (ElementCount a) a+ elements = to <$> gElements++ -- | The element at index @0@.+ lowest :: 1 <= ElementCount a => a+ default lowest ::+ (Generic a, GFinite (Rep a), ElementCount a ~ GElementCount (Rep a)) =>+ 1 <= ElementCount a => a+ lowest = to gLowest++ -- | Just the element at index 0. Nothing, if @ElementCount a = 0@.+ lowestMaybe :: Maybe a+ default lowestMaybe ::+ ( Generic a, GFinite (Rep a)+ ) => Maybe a+ lowestMaybe = to <$> gLowestMaybe++ -- | The element at index @(ElementCount a - 1)@.+ highest :: 1 <= ElementCount a => a+ default highest ::+ (Generic a, GFinite (Rep a), ElementCount a ~ GElementCount (Rep a)) =>+ 1 <= ElementCount a => a+ highest = to gHighest++ -- | Just the element at index @(ElementCount a - 1)@. Nothing, if+ -- @ElementCount a = 0@.+ highestMaybe :: Maybe a+ default highestMaybe ::+ ( Generic a, GFinite (Rep a)+ ) => Maybe a+ highestMaybe = to <$> gHighestMaybe++ -- | 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.+ predMaybe :: a -> Maybe a+ default predMaybe ::+ ( Generic a, GFinite (Rep a)+ ) => a -> Maybe a+ predMaybe = fmap to . gPredMaybe . from++ -- | 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.+ succMaybe :: a -> Maybe a+ default succMaybe ::+ ( Generic a, GFinite (Rep a)+ ) => a -> Maybe a+ succMaybe = fmap to . gSuccMaybe . from++ -- | Maps from an index to the associated element.+ ith :: Index (ElementCount a) -> a+ default ith ::+ ( Generic a, GFinite (Rep a)+ , ElementCount a ~ GElementCount (Rep a)+ ) => Index (ElementCount a) -> a+ ith = to . gIth++ -- | Maps an element of the type to it's associated index.+ index :: a -> Index (ElementCount a)+ default index ::+ ( Generic a, GFinite (Rep a)+ , ElementCount a ~ GElementCount (Rep a)+ ) => a -> Index (ElementCount a)+ index = gIndex . from++ -- | Returns the suffix slice of 'elements' starting at the index+ -- provided via the @SNat@ argument.+ elementsFrom ::+ n + 1 <= ElementCount a =>+ SNat n -> Vec (ElementCount a - n) a+ elementsFrom sn@SNat =+ iterateI (fromJust . succMaybe) (ith $ snatToNum sn)++ -- | Returns the infix slice of 'elements' from the index provided+ -- via the first @SNat@ argument to the index provided via the+ -- second one.+ elementsFromTo ::+ (n + 1 <= ElementCount a, n <= m, m + 1 <= ElementCount a) =>+ SNat n -> SNat m -> Vec (m - n + 1) a+ elementsFromTo sn@SNat SNat =+ iterateI (fromJust . succMaybe) (ith $ snatToNum sn)++-- | The 'Generic' interfaces of 'Finite'.+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)++instance GFinite V1 where+ type GElementCount V1 = 0+ gElements = Nil+ gLowest = (\case{} :: Dict (1 <= 0) -> a) Dict+ gLowestMaybe = Nothing+ gHighest = (\case{} :: Dict (1 <= 0) -> a) Dict+ gHighestMaybe = Nothing+ gPredMaybe = const Nothing+ gSuccMaybe = const Nothing+ -- GHC has no knowledge about Index 0 being an uninhabited+ -- type. Hence, we need to throw an error here although there+ -- provably are no values that can ever be passed to gIth.+ gIth a = errorX $ "Index 0 cannot contain any values like " <> show a+ gIndex = \case {}++instance GFinite U1 where+ type GElementCount U1 = 1+ gElements = U1 :> Nil+ gLowest = U1+ gLowestMaybe = Just U1+ gHighest = U1+ gHighestMaybe = Just U1+ gPredMaybe = const Nothing+ gSuccMaybe = const Nothing+ gIth = const U1+ gIndex = const 0++instance Finite a => GFinite (K1 i a) where+ type GElementCount (K1 _ a) = ElementCount a+ gElements = K1 <$> elements+ gLowest = K1 lowest+ gLowestMaybe = K1 <$> lowestMaybe+ gHighest = K1 highest+ gHighestMaybe = K1 <$> highestMaybe+ gPredMaybe = fmap K1 . predMaybe . unK1+ gSuccMaybe = fmap K1 . succMaybe . unK1+ gIth = K1 . ith+ gIndex = index . unK1++instance GFinite a => GFinite (M1 i v a) where+ type GElementCount (M1 _ _ a) = GElementCount a+ gElements = M1 <$> gElements+ gLowest = M1 gLowest+ gLowestMaybe = M1 <$> gLowestMaybe+ gHighest = M1 gHighest+ gHighestMaybe = M1 <$> gHighestMaybe+ gPredMaybe = fmap M1 . gPredMaybe . unM1+ gSuccMaybe = fmap M1 . gSuccMaybe . unM1+ gIth = M1 . gIth+ gIndex = gIndex . unM1++instance (GFinite a, GFinite b) => GFinite (a :*: b) where+ type GElementCount (a :*: b) = GElementCount a * GElementCount b+ gElements = concatMap (\a -> (a :*:) <$> gElements @b) (gElements @a)++ gLowest+ | Dict <- mulPositiveImpliesPositiveOperands @(GElementCount a) @(GElementCount b)+ = gLowest :*: gLowest+ gLowestMaybe = (:*:) <$> gLowestMaybe <*> gLowestMaybe++ gHighest+ | Dict <- mulPositiveImpliesPositiveOperands @(GElementCount a) @(GElementCount b)+ = gHighest :*: gHighest+ gHighestMaybe = (:*:) <$> gHighestMaybe <*> gHighestMaybe++ gPredMaybe (a :*: b) =+ (:*:) a <$> gPredMaybe b+ <|> (:*:) <$> gPredMaybe a <*> gHighestMaybe+ gSuccMaybe (a :*: b) =+ (:*:) a <$> gSuccMaybe b+ <|> (:*:) <$> gSuccMaybe a <*> gLowestMaybe++ gIth x = gIth (resize $ x `div` m) :*: gIth (resize $ x `mod` m)+ where+ m = natToNum @(GElementCount b)++ gIndex (a :*: b) =+ resize (gIndex a) * natToNum @(GElementCount b)+ + resize (gIndex b)++instance (GFinite a, GFinite b) => GFinite (a :+: b) where+ type GElementCount (a :+: b) = GElementCount a + GElementCount b+ gElements = (L1 <$> gElements @a) ++ (R1 <$> gElements @b)++ gLowest = case compareSNat (SNat @1) (SNat @(GElementCount a)) of+ SNatLE -> L1 gLowest+ SNatGT -> case compareSNat (SNat @1) (SNat @(GElementCount b)) of+ SNatLE -> R1 gLowest+ SNatGT -> case zeroLeAdd @(GElementCount a) @1 of+ Dict -> case zeroLeAdd @(GElementCount b) @1 of {}+ gLowestMaybe = L1 <$> gLowestMaybe @a <|> R1 <$> gLowestMaybe @b++ gHighest = case compareSNat (SNat @1) (SNat @(GElementCount b)) of+ SNatLE -> R1 gHighest+ SNatGT -> case compareSNat (SNat @1) (SNat @(GElementCount a)) of+ SNatLE -> L1 gHighest+ SNatGT -> case zeroLeAdd @(GElementCount a) @1 of+ Dict -> case zeroLeAdd @(GElementCount b) @1 of {}+ gHighestMaybe = R1 <$> gHighestMaybe @b <|> L1 <$> gHighestMaybe @a++ gPredMaybe = \case+ L1 x -> L1 <$> gPredMaybe x+ R1 x -> R1 <$> gPredMaybe x <|> L1 <$> gHighestMaybe++ gSuccMaybe = \case+ R1 x -> R1 <$> gSuccMaybe x+ L1 x -> L1 <$> gSuccMaybe x <|> R1 <$> gLowestMaybe++ gIth x+ | e x < n = L1 $ gIth $ truncateB x+ | otherwise = R1 $ gIth $ truncateB $ e x - n+ where+ n = natToNum @(GElementCount a)+ e = extend @Index @(GElementCount (a :+: b))+ @(If (GElementCount (a :+: b) <=? GElementCount a) 1 0)++ gIndex = \case+ L1 x -> extend (gIndex x)+ R1 x -> extend (gIndex x) + natToNum @(GElementCount a)++instance Finite Void+instance Finite ()+instance Finite Bool+instance Finite Ordering+instance Finite (Proxy a)++instance KnownNat n => Finite (SNat n) where+ type ElementCount (SNat n) = 1+ elements = SNat :> Nil+ lowest = SNat+ lowestMaybe = Just SNat+ highest = SNat+ highestMaybe = Just SNat+ predMaybe = const Nothing+ succMaybe = const Nothing+ ith = const SNat+ index = const 0++instance KnownSymbol s => Finite (SSymbol s) where+ type ElementCount (SSymbol s) = 1+ elements = SSymbol :> Nil+ lowest = SSymbol+ lowestMaybe = Just SSymbol+ highest = SSymbol+ highestMaybe = Just SSymbol+ predMaybe = const Nothing+ succMaybe = const Nothing+ ith = const SSymbol+ index = const 0++instance c => Finite (Dict c) where+ type ElementCount (Dict c) = 1+ elements = Dict :> Nil+ lowest = Dict+ lowestMaybe = Just Dict+ highest = Dict+ highestMaybe = Just Dict+ predMaybe = const Nothing+ succMaybe = const Nothing+ ith = const Dict+ index = const 0++deriving via BoundedEnumEq 0x110000 Char instance Finite Char+deriving via BoundedEnumEq (2^BitSize Int) Int instance Finite Int+deriving via BoundedEnumEq (2^8) Int8 instance Finite Int8+deriving via BoundedEnumEq (2^16) Int16 instance Finite Int16+deriving via BoundedEnumEq (2^32) Int32 instance Finite Int32+deriving via BoundedEnumEq (2^64) Int64 instance Finite Int64+deriving via BoundedEnumEq (2^BitSize Word) Word instance Finite Word+deriving via BoundedEnumEq (2^8) Word8 instance Finite Word8+deriving via BoundedEnumEq (2^16) Word16 instance Finite Word16+deriving via BoundedEnumEq (2^32) Word32 instance Finite Word32+deriving via BoundedEnumEq (2^64) Word64 instance Finite Word64++deriving newtype instance Finite a => Finite (Const a b)+deriving newtype instance Finite a => Finite (Identity a)+deriving newtype instance Finite (f (g a)) => Finite (Compose f g a)++instance Finite a => Finite (Maybe a)+instance (Finite a, Finite b ) => Finite (Either a b)+instance (Finite (f a), Finite (g a)) => Finite (Product f g a)+instance (Finite (f a), Finite (g a)) => Finite (Sum f g a)++instance KnownNat n => Finite (Index n) where+ type ElementCount (Index n) = n+ elements = indicesI+ lowest = minBound+ lowestMaybe = case toUNat (SNat @n) of+ UZero -> Nothing+ _ -> Just minBound+ highest = maxBound+ highestMaybe = case toUNat (SNat @n) of+ UZero -> Nothing+ _ -> Just maxBound+ predMaybe = case toUNat (SNat @n) of+ UZero -> const Nothing+ _ -> \n -> if n == minBound then Nothing else Just $ n - 1+ succMaybe = case toUNat (SNat @n)of+ UZero -> const Nothing+ _ -> \n -> if n == maxBound then Nothing else Just $ n + 1+ ith = id+ index = id++instance KnownNat n => Finite (Signed n) where+ type ElementCount (Signed n) = 2^n+ elements = iterateI (+1) minBound+ lowest = minBound+ lowestMaybe = Just minBound+ highest = maxBound+ highestMaybe = Just maxBound+ predMaybe n = if n == minBound then Nothing else Just $ n - 1+ succMaybe n = if n == maxBound then Nothing else Just $ n + 1+ ith = unpack . xor (complement (complement 0 `shiftR` 1)) . pack+ index = unpack . xor (complement (complement 0 `shiftR` 1)) . pack++instance KnownNat n => Finite (Unsigned n) where+ type ElementCount (Unsigned n) = 2^n+ elements = iterateI (+1) minBound+ lowest = minBound+ lowestMaybe = Just minBound+ highest = maxBound+ highestMaybe = Just maxBound+ predMaybe n = if n == minBound then Nothing else Just $ n - 1+ succMaybe n = if n == maxBound then Nothing else Just $ n + 1+ ith = bitCoerce+ index = bitCoerce++instance Finite Bit where+ type ElementCount Bit = 2+ elements = low :> high :> Nil+ lowest = low+ lowestMaybe = Just low+ highest = high+ highestMaybe = Just high+ predMaybe b = if b == low then Nothing else Just low+ succMaybe b = if b == high then Nothing else Just high+ ith = \case { 0 -> low; _ -> high }+ index b = if b == low then 0 else 1++instance KnownNat n => Finite (BitVector n) where+ type ElementCount (BitVector n) = 2^n+ elements = iterateI (+1) 0+ lowest = minBound+ lowestMaybe = Just minBound+ highest = maxBound+ highestMaybe = Just maxBound+ predMaybe bv = if bv == minBound then Nothing else Just $ bv - 1+ succMaybe bv = if bv == maxBound then Nothing else Just $ bv + 1+ ith = pack+ index = unpack++instance (SaturatingNum a, Finite a) => Finite (Erroring a) where+ type ElementCount (Erroring a) = ElementCount a+ elements = toErroring <$> elements+ lowest = toErroring lowest+ lowestMaybe = toErroring <$> lowestMaybe+ highest = toErroring highest+ highestMaybe = toErroring <$> highestMaybe+ predMaybe = fmap toErroring . predMaybe . fromErroring+ succMaybe = fmap toErroring . succMaybe . fromErroring+ ith = toErroring . ith+ index = index . fromErroring++instance Finite a => Finite (Overflowing a) where+ type ElementCount (Overflowing a) = ElementCount a+ elements = toOverflowing <$> elements+ lowest = toOverflowing lowest+ lowestMaybe = toOverflowing <$> lowestMaybe+ highest = toOverflowing highest+ highestMaybe = toOverflowing <$> highestMaybe+ predMaybe = fmap toOverflowing . predMaybe . fromOverflowing+ succMaybe = fmap toOverflowing . succMaybe . fromOverflowing+ ith = toOverflowing . ith+ index = index . fromOverflowing++instance (SaturatingNum a, Finite a) => Finite (Saturating a) where+ type ElementCount (Saturating a) = ElementCount a+ elements = toSaturating <$> elements+ lowest = toSaturating lowest+ lowestMaybe = toSaturating <$> lowestMaybe+ highest = toSaturating highest+ highestMaybe = toSaturating <$> highestMaybe+ predMaybe = fmap toSaturating . predMaybe . fromSaturating+ succMaybe = fmap toSaturating . succMaybe . fromSaturating+ ith = toSaturating . ith+ index = index . fromSaturating++instance (SaturatingNum a, Finite a) => Finite (Wrapping a) where+ type ElementCount (Wrapping a) = ElementCount a+ elements = toWrapping <$> elements+ lowest = toWrapping lowest+ lowestMaybe = toWrapping <$> lowestMaybe+ highest = toWrapping highest+ highestMaybe = toWrapping <$> highestMaybe+ predMaybe = fmap toWrapping . predMaybe . fromWrapping+ succMaybe = fmap toWrapping . succMaybe . fromWrapping+ ith = toWrapping . ith+ index = index . fromWrapping++instance (SaturatingNum a, Finite a) => Finite (Zeroing a) where+ type ElementCount (Zeroing a) = ElementCount a+ elements = toZeroing <$> elements+ lowest = toZeroing lowest+ lowestMaybe = toZeroing <$> lowestMaybe+ highest = toZeroing highest+ highestMaybe = toZeroing <$> highestMaybe+ predMaybe = fmap toZeroing . predMaybe . fromZeroing+ succMaybe = fmap toZeroing . succMaybe . fromZeroing+ ith = toZeroing . ith+ index = index . fromZeroing++data PowV (k :: Nat) (a :: Type) (f :: TyFun Nat Type) :: Type+type instance Apply (PowV k a) n = Vec (k^n) (Vec n a)++instance (KnownNat n, Finite a) => Finite (Vec n a) where+ type ElementCount (Vec n a) = ElementCount a^n++ elements = dfold+ (Proxy @(PowV (ElementCount a) a))+ (\_ _ -> concatMap ((<$> elements) . (:<)))+ (Nil :> Nil)+ (repeat @n ())++ lowest = case toUNat (SNat @n) of+ UZero -> Nil+ _ -> case compareSNat (SNat @1) (SNat @(ElementCount a)) of+ SNatGT -> case zeroLeAdd @(ElementCount a) @1 of+ Dict -> case powPositiveImpliesPositiveBase @(ElementCount a) @n of {}+ SNatLE -> repeat lowest++ lowestMaybe = case toUNat (SNat @n) of+ UZero -> Just Nil+ _ -> repeat <$> lowestMaybe++ highest = case toUNat (SNat @n) of+ UZero -> Nil+ _ -> case compareSNat (SNat @1) (SNat @(ElementCount a)) of+ SNatGT -> case zeroLeAdd @(ElementCount a) @1 of+ Dict -> case powPositiveImpliesPositiveBase @(ElementCount a) @n of {}+ SNatLE -> repeat highest++ highestMaybe = case toUNat (SNat @n) of+ UZero -> Just Nil+ _ -> repeat <$> highestMaybe++ predMaybe v = do+ h <- highestMaybe+ either Just (const Nothing)+ $ ifoldr+ (\i x a -> case predMaybe x of+ Nothing -> replace i h <$> a+ Just y -> a >>= Left . replace i y+ ) (Right v) v++ succMaybe v = do+ l <- lowestMaybe+ either Just (const Nothing)+ $ ifoldr+ (\i x a -> case succMaybe x of+ Nothing -> replace i l <$> a+ Just y -> a >>= Left . replace i y+ ) (Right v) v++ ith = case toUNat (SNat @n) of+ UZero -> const Nil+ USucc UZero -> (:> Nil) . ith+ _ -> (reverse .) . unfoldrI+ $ \i -> ( ith $ resize $ i `mod` natToNum @(ElementCount a)+ , i `div` natToNum @(ElementCount a)+ )++ index = (fst .) . (`foldr` (0, 1))+ $ \a (n, p) ->+ ( p * resize (index a) + n+ , natToNum @(ElementCount a) * p+ )++data PowT (k :: Nat) (a :: Type) (f :: TyFun Nat Type) :: Type+type instance Apply (PowT k a) d = Vec (k^(2^d)) (RTree d a)++instance (KnownNat d, Finite a) => Finite (RTree d a) where+ type ElementCount (RTree d a) = ElementCount a^(2^d)++ elements = tdfold+ (Proxy @(PowT (ElementCount a) a))+ (const $ RLeaf <$> (elements @a))+ (\(_ :: SNat m) l r -> case powLawsRewrite @(ElementCount a) @m of+ Dict -> concatMap ((<$> r) . RBranch) l+ )+ (trepeat @d ())++ lowest = case compareSNat (SNat @1) (SNat @(ElementCount a)) of+ SNatLE -> trepeat lowest+ SNatGT -> case zeroLeAdd @(ElementCount a) @1 of+ Dict -> case powPositiveImpliesPositiveBase @(ElementCount a) @(2^d) of {}++ lowestMaybe = trepeat <$> lowestMaybe++ highest = case compareSNat (SNat @1) (SNat @(ElementCount a)) of+ SNatLE -> trepeat highest+ SNatGT -> case zeroLeAdd @(ElementCount a) @1 of+ Dict -> case powPositiveImpliesPositiveBase @(ElementCount a) @(2^d) of {}++ highestMaybe = trepeat <$> highestMaybe++ predMaybe t = highestMaybe >>= predSuccMaybeT# t predMaybe+ succMaybe t = lowestMaybe >>= predSuccMaybeT# t succMaybe++ ith = case toUNat (SNat @d) of+ UZero -> RLeaf . ith+ USucc (_ :: UNat p) -> \i -> RBranch+ (ith @(RTree p a) $ resize $ i `div` m)+ (ith @(RTree p a) $ resize $ i `mod` m)+ where+ m = natToNum @(ElementCount a^(2^p))++ index =+ fst . tfold+ ((, natToNum @(ElementCount a)) . resize . index)+ (\(nL, pL) (nR, pR) -> (nR + pR * nL, pL * pR))++data IterT (a :: Type) (f :: TyFun Nat Type) :: Type+type instance Apply (IterT a) d = (RTree d a, (Bool, RTree d a))++predSuccMaybeT# :: forall n a. KnownNat n =>+ RTree n a -> (a -> Maybe a) -> a -> Maybe (RTree n a)+predSuccMaybeT# t op o+ | hasSuccMaybe = return t'+ | otherwise = Nothing+ where+ (hasSuccMaybe, t') = snd $ tdfold (Proxy @(IterT a)) fLeaf fBranch t++ fLeaf x = (RLeaf x, ) $ case op x of+ Nothing -> (False, RLeaf o)+ Just y -> (True, RLeaf y)++ fBranch _ (lO, (lF, lM)) (rO, (rF, rM)) =+ (RBranch lO rO, )+ $ if rF then (rF, RBranch lO rM)+ else (lF, RBranch lM rM)++instance (Finite a, Finite b) => Finite (a -> b) where+ type ElementCount (a -> b) = ElementCount b^ElementCount a+ elements = fmap ((. index) . (!!)) $ elements @(Vec (ElementCount a) b)++ lowest = case compareSNat (SNat @1) (SNat @(ElementCount b)) of+ SNatLE -> const lowest+ SNatGT -> case zeroLeAdd @(ElementCount b) @1 of+ Dict -> case powPositiveImpliesPositiveBase+ @(ElementCount b) @(ElementCount a) of {}++ lowestMaybe = const <$> lowestMaybe++ highest = case compareSNat (SNat @1) (SNat @(ElementCount b)) of+ SNatLE -> const highest+ SNatGT -> case zeroLeAdd @(ElementCount b) @1 of+ Dict -> case powPositiveImpliesPositiveBase+ @(ElementCount b) @(ElementCount a) of {}++ highestMaybe = const <$> highestMaybe++ predMaybe f = do+ h <- highestMaybe+ either Just (const Nothing)+ $ foldr (\i -> (=<<) $ \g -> do+ let g' y x = if index x == i then y else g x+ maybe (Right $ g' h) (Left . g') $ predMaybe $ g $ ith i+ ) (Right f) $ indicesI @(ElementCount a)++ succMaybe f = do+ l <- lowestMaybe+ either Just (const Nothing)+ $ foldr (\i -> (=<<) $ \g -> do+ let g' y x = if index x == i then y else g x+ maybe (Right $ g' l) (Left . g') $ succMaybe $ g $ ith i+ ) (Right f) $ indicesI @(ElementCount a)++ ith = ((. index) . (!!)) . ith @(Vec (ElementCount a) b)+ index f = index (f . ith <$> indicesI)++instance a ~ b => Finite (a :~: b) where+ type ElementCount (a :~: b) = 1+ elements = Refl :> Nil+ lowest = Refl+ lowestMaybe = Just Refl+ highest = Refl+ highestMaybe = Just Refl+ predMaybe = const Nothing+ succMaybe = const Nothing+ ith = const Refl+ index = const 0++instance a ~~ b => Finite (a :~~: b) where+ type ElementCount (a :~~: b) = 1+ elements = HRefl :> Nil+ lowest = HRefl+ lowestMaybe = Just HRefl+ highest = HRefl+ highestMaybe = Just HRefl+ predMaybe = const Nothing+ succMaybe = const Nothing+ ith = const HRefl+ index = const 0++#if MIN_VERSION_base(4,15,0)+-- | 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 Finite a => Finite (Down a) where+ type ElementCount (Down a) = ElementCount a+ elements = Down <$> reverse elements+ lowest = Down highest+ lowestMaybe = Down <$> highestMaybe+ highest = Down lowest+ highestMaybe = Down <$> lowestMaybe+ predMaybe = fmap Down . succMaybe . getDown+ succMaybe = fmap Down . predMaybe . getDown+ ith = Down . ith . (maxBound -)+ index = (maxBound -) . index . getDown+#endif++#if MIN_VERSION_base(4,15,0)+-- | 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+-- 'Data.Ord.Down' in any other case introducing equivalent behavior.+--+-- The reason why we introduce an additional newtype to+-- 'Data.Ord.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+-- 'Data.Ord.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+-- @'Data.Ord.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+-- 'Clash.Class.Finite.GenericReverse' instead.+--+-- @+-- deriving via GenericReverse T instance Finite T+-- @+--+#else+-- | 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.+#endif+newtype GenericReverse a = GenericReverse { getGenericReverse :: a }++-- | see 'Clash.Class.Finite.GenericReverse'+instance (Generic a, GFinite (Rep a), KnownNat (GElementCount (Rep a))) =>+ Finite (GenericReverse a)+ where+ type ElementCount (GenericReverse a) = GElementCount (Rep a)+ elements = GenericReverse . to <$> reverse gElements+ lowest = GenericReverse $ to gHighest+ lowestMaybe = GenericReverse . to <$> gHighestMaybe+ highest = GenericReverse $ to gLowest+ highestMaybe = GenericReverse . to <$> gLowestMaybe+ predMaybe = fmap (GenericReverse . to) . gSuccMaybe . from . getGenericReverse+ succMaybe = fmap (GenericReverse . to) . gPredMaybe . from . getGenericReverse+ ith = GenericReverse . to . gIth . (maxBound -)+ index = (maxBound -) . gIndex . from . getGenericReverse++-- | The elements of the 'Clash.Sized.BitVector.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+newtype WithUndefined a = WithUndefined { getWithUndefined :: a }+ deriving newtype ( Bits, BitPack, Bounded, Enum, Eq, FiniteBits+ , Generic, Integral, NFDataX, Num, Ord, Real, Read+ , Show, ShowX+ )++-- | __NB__: not synthesizable (see 'Clash.Class.Finite.WithUndefined')+instance Finite (WithUndefined Bit) where+ type ElementCount (WithUndefined Bit) = 3+ elements = coerce <$> Bit 0 0 :> Bit 0 1 :> Bit 1 0 :> Nil+ lowest = coerce $ Bit 0 0+ lowestMaybe = Just $ coerce $ Bit 0 0+ highest = coerce $ Bit 1 0+ highestMaybe = Just $ coerce $ Bit 1 0+ predMaybe b = fmap coerce $ case coerce b of+ Bit 0 0 -> Nothing+ Bit 0 _ -> Just $ Bit 0 0+ _ -> Just $ Bit 0 1+ succMaybe b = fmap coerce $ case coerce b of+ Bit 0 0 -> Just $ Bit 0 1+ Bit 0 _ -> Just $ Bit 1 0+ _ -> Nothing+ ith = coerce . \case+ 0 -> Bit 0 0+ 1 -> Bit 0 1+ _ -> Bit 1 0+ index b = case coerce b of+ Bit 0 0 -> 0+ Bit 0 _ -> 1+ _ -> 2++-- | __NB__: not synthesizable (see 'Clash.Class.Finite.WithUndefined')+instance KnownNat n => Finite (WithUndefined (BitVector n)) where+ type ElementCount (WithUndefined (BitVector n)) = 3^n++ elements = coerce <$> iterateI bvwuSuccMaybe# (BV 0 0)++ lowest = coerce $ BV 0 0+ lowestMaybe = Just $ coerce $ BV 0 0++ highest = coerce $ BV mb mb+ where+ BV _ mb = maxBound :: BitVector n++ highestMaybe = Just $ coerce $ BV mb mb+ where+ BV _ mb = maxBound :: BitVector n++ predMaybe bv = case coerce bv of+ BV 0 0 -> Nothing+ BV m n -> Just $ coerce $+ if ((m `xor` mb) .&. n) == 0+ then BV (m - 1) ((m - 1) `xor` mb)+ else BV m ((m `xor` mb) .&. (n - 1))+ where+ BV _ mb = maxBound :: BitVector n++ succMaybe (coerce -> bv@(BV m _))+ | m < mb = Just $ coerce $ bvwuSuccMaybe# bv+ | otherwise = Nothing+ where+ BV _ mb = maxBound :: BitVector n++ ith i = coerce $ BV+ (toNat $ complement nMask)+ (toNat $ snd $ foldr stretch (remaining, 0) $ unpack nMask)+ where+ nMask, remaining :: BitVector n+ (nMask, remaining)+ | Dict <- powMonotone1 @2 @3 @n+ , Dict <- powPositiveIfPositiveBase @2 @n+ , Dict <- powPositiveIfPositiveBase @3 @n+#if !MIN_VERSION_base(4,16,0)+ , Dict <- pow2CLogDual @n+ , Dict <- leqOnePlusMinus @(2^n) @(3^n)+#endif+ = second (pack . complement . truncateB @Index @(2^n) @(3^n - 2^n))+ $ fst+ $ foldl+ ( \(((`shiftL` 1) -> m, r), x2) x3 ->+ if r < x2 * x3+ then ((m, r ), x2)+ else ((m `setBit` 0, r - x2 * x3), 2 * x2)+ )+ ((0, negate $ satSucc SatWrap i), 1)+ $ reverse+ $ iterateI @n (3 *) 1++ stretch negMBit (bv, (`shiftR` 1) -> v)+ | negMBit = (shiftR bv 1, ) $ if testBit bv 0 then setMsb v else v+ | otherwise = (bv, v)++ toNat = fromInteger . toInteger+ setMsb = (.|.) (complement $ complement 0 `shiftR` 1)++ index (coerce -> bv@(BV mask _))+ | Dict <- powPositiveIfPositiveBase @3 @n+ = -- compute the mask induced offset+ negate+ ( snd+ $ foldr (\b (p, a) -> (3 * p, if b then p + 2 * a else a)) (1, 0)+ $ bitCoerce @(Unsigned n) @(Vec n Bool)+ $ negate+ $ U mask+ )+ + -- re-align the value bits according to the mask+ foldl+ ( \a (Bit m n) -> if+ | m /= 0 -> a+ | n == 0 -> shiftL a 1+ | otherwise -> shiftL a 1 `setBit` 0+ ) 0 (bv2v bv)++bvwuSuccMaybe# :: forall n. KnownNat n => BitVector n -> BitVector n+bvwuSuccMaybe# (BV m n)+ | n < mb = BV m ((n + 1) .|. m)+ | otherwise = BV (m + 1) (m + 1)+ where+ BV _ mb = maxBound :: BitVector n+{-# INLINE bvwuSuccMaybe# #-}++-- | 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.+newtype BoundedEnumEq (n :: Nat) a = BoundedEnumEq { getBoundedEnumEq :: a }++-- | see 'Clash.Class.Finite.BoundedEnumEq'+instance+ ( Bounded a, Enum a, Eq a, KnownNat n, 1 <= n+ ) => Finite (BoundedEnumEq n a)+ where+ type ElementCount (BoundedEnumEq n a) = n+ elements = BoundedEnumEq <$> iterateI succ minBound+ lowest = BoundedEnumEq minBound+ lowestMaybe = Just $ BoundedEnumEq minBound+ highest = BoundedEnumEq maxBound+ highestMaybe = Just $ BoundedEnumEq maxBound+ predMaybe (getBoundedEnumEq -> x)+ | x == minBound = Nothing+ | otherwise = Just $ BoundedEnumEq $ pred x+ succMaybe (getBoundedEnumEq -> x)+ | x == maxBound = Nothing+ | otherwise = Just $ BoundedEnumEq $ succ x+ ith = BoundedEnumEq . toEnum . (+ fromEnum (minBound @a)) . fromEnum+ index = toEnum . flip (-) (fromEnum (minBound @a))+ . fromEnum . getBoundedEnumEq++-- | A newtype wrapper for implementing deriving strategies of classes+-- whose implementation may follow from 'Finite', e.g., the 'Enum'+-- class.+newtype FiniteDerive a = FiniteDerive { getFiniteDerive :: a }++instance Finite a => Enum (FiniteDerive a) where+ succ = FiniteDerive . fromJust . succMaybe . getFiniteDerive+ pred = FiniteDerive . fromJust . predMaybe . getFiniteDerive+ toEnum = FiniteDerive . ith . toEnum . (`mod` natToNum @(ElementCount a))+ fromEnum = fromEnum . index . getFiniteDerive+ enumFrom x =+ take (natToNum @(ElementCount a) - fromEnum (index $ getFiniteDerive x))+ $ List.iterate succ x+ enumFromTo x y =+ take (fromEnum (index (getFiniteDerive y) - index (getFiniteDerive x)))+ $ List.iterate succ x+ enumFromThen = case toUNat (SNat @(ElementCount a)) of+ UZero -> const $ const []+ USucc um -> \x y -> FiniteDerive . ith <$>+ [ index (getFiniteDerive x)+ , index (getFiniteDerive y)+ .. snatToNum (fromUNat um)+ ]+ enumFromThenTo = case toUNat (SNat @(ElementCount a)) of+ UZero -> const $ const $ const []+ USucc _ -> \x y z -> FiniteDerive . ith <$>+ [ index (getFiniteDerive x)+ , index (getFiniteDerive y)+ .. index (getFiniteDerive z)+ ]++instance (Finite a, 1 <= ElementCount a) => Bounded (FiniteDerive a) where+ minBound = FiniteDerive lowest+ maxBound = FiniteDerive highest++instance (Finite a, Finite b) => Finite (a, b)++-- | __NB__: The documentation only shows instances up to /3/-tuples. By+-- default, instances up to and including /12/-tuples will exist. If the flag+-- @large-tuples@ is set instances up to the GHC imposed limit will exist. The+-- GHC imposed limit is either 62 or 64 depending on the GHC version.+deriveFiniteTuples ''Finite ''ElementCount 'elements 'lowest 'lowestMaybe+ 'highest 'highestMaybe 'predMaybe 'succMaybe 'ith 'index
+ src/Clash/Class/Finite/Internal/Evidence.hs view
@@ -0,0 +1,87 @@+{-|+Copyright : (C) 2024-2025, Felix Klein+License : MIT (see the file LICENSE)+Maintainer : Felix Klein <felix@qbaylogic.com>+-}++{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE NoStarIsType #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}++{-# OPTIONS_HADDOCK hide #-}++module Clash.Class.Finite.Internal.Evidence where++import Data.Constraint (Dict(..))+import GHC.TypeNats+ ( Nat, type (^), type (<=), type (*), type (+)+#if !MIN_VERSION_base(4,16,0)+ , type (-)+#endif+ )+#if !MIN_VERSION_base(4,16,0)+import GHC.TypeLits.Extra (CLog)+#endif+import Unsafe.Coerce (unsafeCoerce)++-- | Evidence that exponentiation can never return a zero result,+-- except the base is zero.+powPositiveIfPositiveBase ::+ forall (n :: Nat) (m :: Nat).+ 1 <= n => Dict (1 <= n^m)+powPositiveIfPositiveBase = unsafeCoerce (Dict :: Dict (0 <= 0))++-- | Evidence that exponentiation not returning a zero result is+-- a proof of the base being greater than zero.+powPositiveImpliesPositiveBase ::+ forall (n :: Nat) (m :: Nat).+ 1 <= n^m => Dict (1 <= n)+powPositiveImpliesPositiveBase = unsafeCoerce (Dict :: Dict (0 <= 0))++-- | Evidence that any multiplicaton resulting in a positive number+-- must have two positive operands.+mulPositiveImpliesPositiveOperands ::+ forall (n :: Nat) (m :: Nat).+ 1 <= n * m => Dict (1 <= n, 1 <= m)+mulPositiveImpliesPositiveOperands =+ unsafeCoerce (Dict :: Dict (0 <= 0, 0 <= 0))++-- | Evidence that zero is the only natural number that is less or+-- equal than zero, also in the scope of addition.+zeroLeAdd ::+ forall (n :: Nat) (m :: Nat).+ n + m <= m => Dict (n ~ 0)+zeroLeAdd = unsafeCoerce (Dict :: Dict (0 ~ 0))++-- | Evidence that exponentiation with a fixed exponent perserves+-- monotonicity.+powMonotone1 ::+ forall (a :: Nat) (b :: Nat) (n :: Nat).+ a <= b => Dict (a^n <= b^n)+powMonotone1 = unsafeCoerce (Dict :: Dict (0 <= 0))++-- | Evidence that we can use the exponentiation laws to rewrite the+-- term as stated below.+powLawsRewrite ::+ forall (a :: Nat) (n :: Nat).+ Dict ((a^(2^(n + 1))) ~ ((a^(2^n)) * (a^(2^n))))+powLawsRewrite = unsafeCoerce (Dict :: Dict (0 ~ 0))++#if !MIN_VERSION_base(4,16,0)+-- | Evidence that exponentiation and clog are dual to each other.+pow2CLogDual ::+ forall (n :: Nat).+ Dict (CLog 2 (2^n) ~ n)+pow2CLogDual = unsafeCoerce (Dict :: Dict (0 ~ 0))++-- | Evidence that substraction and addition of the same nat cancels+-- each other in a greater or equal than one equation.+leqOnePlusMinus ::+ forall (a :: Nat) (b :: Nat).+ (a <= b, 1 <= b) => Dict (1 <= a + (b - a))+leqOnePlusMinus = unsafeCoerce (Dict :: Dict (0 <= 0))+#endif
+ src/Clash/Class/Finite/Internal/TH.hs view
@@ -0,0 +1,207 @@+{-|+Copyright : (C) 2024-2025, Felix Klein+License : MIT (see the file LICENSE)+Maintainer : Felix Klein <felix@qbaylogic.com>+-}++{-# LANGUAGE CPP #-}+{-# LANGUAGE NoStarIsType #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeOperators #-}++{-# OPTIONS_HADDOCK hide #-}++module Clash.Class.Finite.Internal.TH where++import Control.Monad (forM, replicateM)+#if !MIN_VERSION_base(4,20,0)+import Data.List (foldl')+#endif+import GHC.TypeNats (type (*))+import Language.Haskell.TH++#ifndef MAX_TUPLE_SIZE+#ifdef LARGE_TUPLES+#if MIN_VERSION_ghc(9,0,0)+import GHC.Settings.Constants (mAX_TUPLE_SIZE)+#else+import Constants (mAX_TUPLE_SIZE)+#endif+#define MAX_TUPLE_SIZE (fromIntegral mAX_TUPLE_SIZE)+#else+#define MAX_TUPLE_SIZE 12+#endif+#endif++maxTupleSize :: Num a => a+maxTupleSize = MAX_TUPLE_SIZE++-- | Contruct all the tuple instances (starting at size 3) for+-- 'Clash.Class.Finite.Internal.Finite'.+deriveFiniteTuples ::+ -- | Finite+ Name ->+ -- | ElementCount+ Name ->+ -- | elements+ Name ->+ -- | lowest+ Name ->+ -- | lowestMaybe+ Name ->+ -- | highest+ Name ->+ -- | highestMaybe+ Name ->+ -- | predMaybe+ Name ->+ -- | succMaybe+ Name ->+ -- | ith+ Name ->+ -- | index+ Name ->+ DecsQ+deriveFiniteTuples finiteName elementCountName elementsName lowestName+ lowestMaybeName highestName highestMaybeName predMaybeName succMaybeName+ ithName indexName+ = do+ let finite = ConT finiteName+ elementCount = ConT elementCountName+ times = ConT ''(*)++ allNames <- replicateM maxTupleSize $ newName "a"+ t2N <- newName "t2N"+ tN2 <- newName "tN2"+ x <- newName "x"++ forM [3..maxTupleSize] $ \tupleNum -> do+ let names = take tupleNum allNames+ (v,vs) = case map VarT names of+ (z:zs) -> (z,zs)+ _ -> error "maxTupleSize < 3"+ tuple xs = foldl' AppT (TupleT $ length xs) xs+ withConvContext b2N bN2 binds impl = return+ $ Clause binds (NormalB impl)+ $ ( if b2N then+ (:) $ FunD t2N $ return+ $ Clause+ [ TupP [ p, TupP ps ]+ | let (p,ps) = case map VarP names of+ (z:zs) -> (z,zs)+ _ -> error "maxTupleSize < 3"++ ]+ ( NormalB $ mkTupE $ map VarE names )+ []+ else id+ )+ $ ( if bN2 then+ (:) $ FunD tN2 $ return+ $ Clause+ [ TupP $ map VarP names ]+ ( let (e,es) = case map VarE names of+ (z:zs) -> (z,zs)+ _ -> error "maxTupleSize < 3"+ in NormalB (mkTupE [e,mkTupE es])+ )+ []+ else id+ )+ []++ -- Instance declaration+ context =+ [ finite `AppT` v+ , finite `AppT` tuple vs+ ]+ instTy = AppT finite $ tuple (v:vs)++ elementCountType =+ mkTySynInstD elementCountName [tuple (v:vs)]+ $ times `AppT` (elementCount `AppT` v) `AppT`+ (elementCount `AppT` foldl AppT (TupleT $ tupleNum - 1) vs)++ elements = FunD elementsName+ $ withConvContext True False []+ $ AppE (AppE (VarE '(<$>)) (VarE t2N))+ $ VarE elementsName++ lowest = FunD lowestName+ $ withConvContext True False []+ $ AppE (VarE t2N)+ $ VarE lowestName++ lowestMaybe = FunD lowestMaybeName+ $ withConvContext True False []+ $ AppE (AppE (VarE '(<$>)) (VarE t2N))+ $ VarE lowestMaybeName++ highest = FunD highestName+ $ withConvContext True False []+ $ AppE (VarE t2N)+ $ VarE highestName++ highestMaybe = FunD highestMaybeName+ $ withConvContext True False []+ $ AppE (AppE (VarE '(<$>)) (VarE t2N))+ $ VarE highestMaybeName++ predMaybe = FunD predMaybeName+ $ withConvContext True True [ VarP x ]+ $ AppE (AppE (VarE '(<$>)) (VarE t2N))+ $ AppE (VarE predMaybeName)+ $ AppE (VarE tN2)+ $ VarE x++ succMaybe = FunD succMaybeName+ $ withConvContext True True [ VarP x ]+ $ AppE (AppE (VarE '(<$>)) (VarE t2N))+ $ AppE (VarE succMaybeName)+ $ AppE (VarE tN2)+ $ VarE x++ ith = FunD ithName+ $ withConvContext True False [ VarP x ]+ $ AppE (VarE t2N)+ $ AppE (VarE ithName)+ $ VarE x++ index = FunD indexName+ $ withConvContext False True [ VarP x ]+ $ AppE (VarE indexName)+ $ AppE (VarE tN2)+ $ VarE x++ return $ InstanceD Nothing context instTy+ [ elementCountType+ , elements+ , lowest+ , lowestMaybe+ , highest+ , highestMaybe+ , predMaybe+ , succMaybe+ , ith+ , index+ ]+ where+ mkTupE = TupE+#if MIN_VERSION_template_haskell(2,16,0)+ . map Just+#endif+++-- | Compatibility helper to create TySynInstD (stolen from Clash+-- Prelude, as it is not exported by the library)+mkTySynInstD :: Name -> [Type] -> Type -> Dec+mkTySynInstD tyConNm tyArgs rhs =+#if MIN_VERSION_template_haskell(2,15,0)+ TySynInstD (TySynEqn Nothing+ (foldl AppT (ConT tyConNm) tyArgs)+ rhs)+#else+ TySynInstD tyConNm+ (TySynEqn tyArgs+ rhs)+#endif
+ tests/Clash/Tests/Laws/Finite.hs view
@@ -0,0 +1,246 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}++module Clash.Tests.Laws.Finite (tests) where++import Prelude hiding (reverse)++import Control.DeepSeq (NFData)+import Control.Monad (forM_)+import Data.Constraint (Dict(..))+import Data.Functor.Compose (Compose(..))+import Data.Functor.Const (Const(..))+import Data.Functor.Identity (Identity(..))+import Data.Functor.Product (Product)+import Data.Functor.Sum (Sum)+import Data.Int (Int8, Int16)+#if MIN_VERSION_base(4,15,0)+import Data.Ord (Down(..))+#endif+import Data.Proxy (Proxy(..))+import Data.Typeable (Typeable, typeRep)+import Data.Void (Void)+import Data.Word (Word8, Word16)+import Test.Tasty (TestTree, testGroup)+import Test.Tasty.HUnit (Assertion, (@=?), testCase)++import Clash.Class.Finite (Finite(..))+import Clash.Promoted.Nat (SNatLE(..), SNat(..), compareSNat)+import Clash.Sized.BitVector (BitVector, Bit)+import Clash.Sized.Index (Index)+import Clash.Sized.RTree (RTree)+import Clash.Sized.Signed (Signed)+import Clash.Sized.Unsigned (Unsigned)+import Clash.Sized.Vector (Vec, indicesI, iterateI, reverse)++indexOrderLaw ::+ forall a.+ (NFData a, Show a, Finite a) =>+ Proxy a ->+ Assertion+indexOrderLaw Proxy =+ index <$> elements @a @=? indicesI++forwardIterateLaw ::+ forall a.+ (NFData a, Show a, Eq a, Finite a) =>+ Proxy a ->+ Assertion+forwardIterateLaw Proxy =+ iterateI (>>= succMaybe) (lowestMaybe @a) @=? Just <$> elements @a++backwardIterateLaw ::+ forall a.+ (NFData a, Show a, Eq a, Finite a) =>+ Proxy a ->+ Assertion+backwardIterateLaw Proxy =+ iterateI (>>= predMaybe) (highestMaybe @a) @=? Just <$> reverse (elements @a)++indexIsomorphismLaw ::+ forall a.+ (NFData a, Show a, Eq a, Finite a) =>+ Proxy a ->+ Assertion+indexIsomorphismLaw Proxy =+ ith . index <$> elements @a @=? elements @a++minimumPredecessor ::+ forall a.+ (NFData a, Show a, Eq a, Finite a) =>+ Proxy a ->+ Assertion+minimumPredecessor Proxy =+ (lowestMaybe >>= predMaybe @a) @=? Nothing++maximumSuccessor ::+ forall a.+ (NFData a, Show a, Eq a, Finite a) =>+ Proxy a ->+ Assertion+maximumSuccessor Proxy =+ (highestMaybe >>= succMaybe @a) @=? Nothing++extremes ::+ forall a.+ (NFData a, Show a, Eq a, Finite a) =>+ Proxy a ->+ Assertion+extremes Proxy = case compareSNat (SNat @1) (SNat @(ElementCount a)) of+ SNatLE -> do+ lowestMaybe @a @=? Just lowest+ highestMaybe @a @=? Just highest+ SNatGT -> do+ lowestMaybe @a @=? Nothing+ highestMaybe @a @=? Nothing++boundedCompatibility ::+ forall a.+ (NFData a, Show a, Eq a, Finite a) =>+ Maybe (Dict (Bounded a)) ->+ Assertion+boundedCompatibility = \case+ Nothing -> return ()+ Just Dict -> case compareSNat (SNat @1) (SNat @(ElementCount a)) of+ SNatGT -> return ()+ SNatLE -> do+ lowest @a @=? minBound @a+ highest @a @=? maxBound @a++enumCompatibility ::+ forall a.+ (NFData a, Show a, Eq a, Finite a) =>+ Maybe (Dict (Enum a)) ->+ Assertion+enumCompatibility = \case+ Nothing -> return ()+ Just Dict -> forM_ (elements @a) $ \x -> do+ maybe (return ()) (@=? succ x) $ succMaybe x+ maybe (return ()) (@=? pred x) $ predMaybe x++finiteLaws ::+ forall a.+ (NFData a, Show a, Eq a, Finite a) =>+ Maybe (Dict (Bounded a)) ->+ Maybe (Dict (Enum a)) ->+ [TestTree]+finiteLaws mBounded mEnum =+ [ testCase "Index Order" $ indexOrderLaw proxy+ , testCase "Forward Iterate" $ forwardIterateLaw proxy+ , testCase "Backward Iterate" $ backwardIterateLaw proxy+ , testCase "Index Isomorphism" $ indexIsomorphismLaw proxy+ , testCase "Minimum Predecessor" $ minimumPredecessor proxy+ , testCase "Maximum Successor" $ maximumSuccessor proxy+ , testCase "Extremes" $ extremes proxy+ , testCase "Bounded Compatibility" $ boundedCompatibility mBounded+ , testCase "Enum Compatibility" $ enumCompatibility mEnum+ ]+ where+ proxy :: Proxy a+ proxy = Proxy++testFiniteLaws ::+ forall a.+ (NFData a, Show a, Eq a, Finite a, Typeable a) =>+ Maybe (Dict (Bounded a)) ->+ Maybe (Dict (Enum a)) ->+ TestTree+testFiniteLaws mBounded mEnum =+ testGroup (show (typeRep proxy)) $ finiteLaws mBounded mEnum+ where+ proxy :: Proxy a+ proxy = Proxy++tests :: TestTree+tests = testGroup "Finite"+ [ testFiniteLaws noBInst $ noEInst @Void+ , testFiniteLaws hasBInst $ hasEInst @()+ , testFiniteLaws hasBInst $ hasEInst @Bit+ , testFiniteLaws hasBInst $ hasEInst @Bool+ , testFiniteLaws hasBInst $ hasEInst @Ordering++ , testFiniteLaws hasBInst $ hasEInst @Char+ , testFiniteLaws hasBInst $ hasEInst @Int8+ , testFiniteLaws hasBInst $ hasEInst @Int16+ , testFiniteLaws hasBInst $ hasEInst @Word8+ , testFiniteLaws hasBInst $ hasEInst @Word16++ , testFiniteLaws hasBInst $ hasEInst @(BitVector 0)+ , testFiniteLaws hasBInst $ hasEInst @(BitVector 1)+ , testFiniteLaws hasBInst $ hasEInst @(BitVector 8)++ , testFiniteLaws hasBInst $ hasEInst @(Index 0)+ , testFiniteLaws hasBInst $ hasEInst @(Index 1)+ , testFiniteLaws hasBInst $ hasEInst @(Index 128)++ , testFiniteLaws hasBInst $ hasEInst @(Signed 0)+ , testFiniteLaws hasBInst $ hasEInst @(Signed 1)+ , testFiniteLaws hasBInst $ hasEInst @(Signed 8)++ , testFiniteLaws hasBInst $ hasEInst @(Unsigned 0)+ , testFiniteLaws hasBInst $ hasEInst @(Unsigned 1)+ , testFiniteLaws hasBInst $ hasEInst @(Unsigned 8)++ , testFiniteLaws noBInst $ noEInst @(Maybe (Index 0))+ , testFiniteLaws noBInst $ noEInst @(Maybe (Index 1))+ , testFiniteLaws noBInst $ noEInst @(Maybe (Index 27))++ , testFiniteLaws noBInst $ noEInst @(Either Void (Index 0))+ , testFiniteLaws noBInst $ noEInst @(Either Void (Index 1))+ , testFiniteLaws noBInst $ noEInst @(Either Void (Index 27))+ , testFiniteLaws noBInst $ noEInst @(Either Bool (Index 0))+ , testFiniteLaws noBInst $ noEInst @(Either Bool (Index 1))+ , testFiniteLaws noBInst $ noEInst @(Either Bool (Index 27))++ , testFiniteLaws noBInst $ noEInst @(Compose Maybe Maybe Bool)+ , testFiniteLaws hasBInst $ hasEInst @(Const Bool [Int])+#if MIN_VERSION_base(4,15,0)+ , testFiniteLaws hasBInst $ hasEInst @(Down Bool)+#endif+ , testFiniteLaws hasBInst $ hasEInst @(Identity Bool)+ , testFiniteLaws noBInst $ noEInst @(Product Maybe Maybe Bit)+ , testFiniteLaws noBInst $ noEInst @(Sum Maybe Maybe Bit)++ , testFiniteLaws noBInst $ noEInst @(Vec 0 Void)+ , testFiniteLaws noBInst $ noEInst @(Vec 1 Void)+ , testFiniteLaws noBInst $ noEInst @(Vec 16 Void)+ , testFiniteLaws noBInst $ noEInst @(Vec 0 Bool)+ , testFiniteLaws noBInst $ noEInst @(Vec 1 Bool)+ , testFiniteLaws noBInst $ noEInst @(Vec 16 Bool)++ , testFiniteLaws noBInst $ noEInst @(RTree 0 Void)+ , testFiniteLaws noBInst $ noEInst @(RTree 1 Void)+ , testFiniteLaws noBInst $ noEInst @(RTree 4 Void)+ , testFiniteLaws noBInst $ noEInst @(RTree 0 Bool)+ , testFiniteLaws noBInst $ noEInst @(RTree 1 Bool)+ , testFiniteLaws noBInst $ noEInst @(RTree 4 Bool)++ , testFiniteLaws noBInst $ noEInst @(Void, Void)+ , testFiniteLaws noBInst $ noEInst @(Bool, Void)+ , testFiniteLaws noBInst $ noEInst @(Void, Bool)+ , testFiniteLaws noBInst $ noEInst @(Bool, Bool)++ , testFiniteLaws noBInst $ noEInst @(Bool, Bool, Bool)+ , testFiniteLaws noBInst $ noEInst @(Void, Bool, Bool)+ , testFiniteLaws noBInst $ noEInst @(Bool, Void, Bool)+ , testFiniteLaws noBInst $ noEInst @(Bool, Bool, Void)++ , testFiniteLaws noBInst $ noEInst @(Bool, Bool, Bool, Bool)+ ]+ where+ noBInst :: Maybe (Dict (Bounded a))+ noBInst = Nothing++ hasBInst :: Bounded a => Maybe (Dict (Bounded a))+ hasBInst = Just Dict++ noEInst :: Maybe (Dict (Enum a))+ noEInst = Nothing++ hasEInst :: Enum a => Maybe (Dict (Enum a))+ hasEInst = Just Dict
+ tests/Main.hs view
@@ -0,0 +1,8 @@+module Main where++import Test.Tasty (defaultMain)++import Clash.Tests.Laws.Finite++main :: IO ()+main = defaultMain tests