diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -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 diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/clash-finite.cabal b/clash-finite.cabal new file mode 100644 --- /dev/null +++ b/clash-finite.cabal @@ -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 diff --git a/src/Clash/Class/Finite.hs b/src/Clash/Class/Finite.hs new file mode 100644 --- /dev/null +++ b/src/Clash/Class/Finite.hs @@ -0,0 +1,44 @@ +{-| +Copyright : (C) 2024-2025, Felix Klein +License : MIT (see the file LICENSE) +Maintainer : Felix Klein + +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 diff --git a/src/Clash/Class/Finite/Internal.hs b/src/Clash/Class/Finite/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Clash/Class/Finite/Internal.hs @@ -0,0 +1,1086 @@ +{-| +Copyright : (C) 2024-2025, Felix Klein +License : MIT (see the file LICENSE) +Maintainer : Felix Klein +-} + +{-# 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 diff --git a/src/Clash/Class/Finite/Internal/Evidence.hs b/src/Clash/Class/Finite/Internal/Evidence.hs new file mode 100644 --- /dev/null +++ b/src/Clash/Class/Finite/Internal/Evidence.hs @@ -0,0 +1,87 @@ +{-| +Copyright : (C) 2024-2025, Felix Klein +License : MIT (see the file LICENSE) +Maintainer : Felix Klein +-} + +{-# 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 diff --git a/src/Clash/Class/Finite/Internal/TH.hs b/src/Clash/Class/Finite/Internal/TH.hs new file mode 100644 --- /dev/null +++ b/src/Clash/Class/Finite/Internal/TH.hs @@ -0,0 +1,207 @@ +{-| +Copyright : (C) 2024-2025, Felix Klein +License : MIT (see the file LICENSE) +Maintainer : Felix Klein +-} + +{-# 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 diff --git a/tests/Clash/Tests/Laws/Finite.hs b/tests/Clash/Tests/Laws/Finite.hs new file mode 100644 --- /dev/null +++ b/tests/Clash/Tests/Laws/Finite.hs @@ -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 diff --git a/tests/Main.hs b/tests/Main.hs new file mode 100644 --- /dev/null +++ b/tests/Main.hs @@ -0,0 +1,8 @@ +module Main where + +import Test.Tasty (defaultMain) + +import Clash.Tests.Laws.Finite + +main :: IO () +main = defaultMain tests