{-|
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 = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Rep a Any -> a)
-> Vec (GElementCount (Rep a)) (Rep a Any)
-> Vec (GElementCount (Rep a)) a
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vec (GElementCount (Rep a)) (Rep a Any)
forall a. Vec (GElementCount (Rep a)) (Rep a a)
forall (rep :: Type -> Type) a.
GFinite rep =>
Vec (GElementCount rep) (rep a)
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 = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to Rep a Any
forall a. (1 <= GElementCount (Rep a)) => Rep a a
forall (rep :: Type -> Type) a.
(GFinite rep, 1 <= GElementCount rep) =>
rep a
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 = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Rep a Any -> a) -> Maybe (Rep a Any) -> Maybe a
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Rep a Any)
forall a. Maybe (Rep a a)
forall (rep :: Type -> Type) a. GFinite rep => Maybe (rep a)
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 = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to Rep a Any
forall a. (1 <= GElementCount (Rep a)) => Rep a a
forall (rep :: Type -> Type) a.
(GFinite rep, 1 <= GElementCount rep) =>
rep a
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 = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Rep a Any -> a) -> Maybe (Rep a Any) -> Maybe a
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Rep a Any)
forall a. Maybe (Rep a a)
forall (rep :: Type -> Type) a. GFinite rep => Maybe (rep a)
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 = (Rep a Any -> a) -> Maybe (Rep a Any) -> Maybe a
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Maybe (Rep a Any) -> Maybe a)
-> (a -> Maybe (Rep a Any)) -> a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep a Any -> Maybe (Rep a Any)
forall a. Rep a a -> Maybe (Rep a a)
forall (rep :: Type -> Type) a.
GFinite rep =>
rep a -> Maybe (rep a)
gPredMaybe (Rep a Any -> Maybe (Rep a Any))
-> (a -> Rep a Any) -> a -> Maybe (Rep a Any)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
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 = (Rep a Any -> a) -> Maybe (Rep a Any) -> Maybe a
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Maybe (Rep a Any) -> Maybe a)
-> (a -> Maybe (Rep a Any)) -> a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep a Any -> Maybe (Rep a Any)
forall a. Rep a a -> Maybe (Rep a a)
forall (rep :: Type -> Type) a.
GFinite rep =>
rep a -> Maybe (rep a)
gSuccMaybe (Rep a Any -> Maybe (Rep a Any))
-> (a -> Rep a Any) -> a -> Maybe (Rep a Any)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
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 = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Rep a Any -> a)
-> (Index (GElementCount (Rep a)) -> Rep a Any)
-> Index (GElementCount (Rep a))
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (GElementCount (Rep a)) -> Rep a Any
forall a. Index (GElementCount (Rep a)) -> Rep a a
forall (rep :: Type -> Type) a.
GFinite rep =>
Index (GElementCount rep) -> rep a
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 = Rep a Any -> Index (GElementCount (Rep a))
forall a. Rep a a -> Index (GElementCount (Rep a))
forall (rep :: Type -> Type) a.
GFinite rep =>
rep a -> Index (GElementCount rep)
gIndex (Rep a Any -> Index (GElementCount (Rep a)))
-> (a -> Rep a Any) -> a -> Index (GElementCount (Rep a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
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 n
sn@SNat n
SNat =
    (a -> a) -> a -> Vec (ElementCount a - n) a
forall (n :: Nat) a. KnownNat n => (a -> a) -> a -> Vec n a
iterateI (Maybe a -> a
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe a -> a) -> (a -> Maybe a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. Finite a => a -> Maybe a
succMaybe) (Index (ElementCount a) -> a
forall a. Finite a => Index (ElementCount a) -> a
ith (Index (ElementCount a) -> a) -> Index (ElementCount a) -> a
forall a b. (a -> b) -> a -> b
$ SNat n -> Index (ElementCount a)
forall a (n :: Nat). Num a => SNat n -> a
snatToNum SNat n
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 n
sn@SNat n
SNat SNat m
SNat =
    (a -> a) -> a -> Vec ((m - n) + 1) a
forall (n :: Nat) a. KnownNat n => (a -> a) -> a -> Vec n a
iterateI (Maybe a -> a
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe a -> a) -> (a -> Maybe a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. Finite a => a -> Maybe a
succMaybe) (Index (ElementCount a) -> a
forall a. Finite a => Index (ElementCount a) -> a
ith (Index (ElementCount a) -> a) -> Index (ElementCount a) -> a
forall a b. (a -> b) -> a -> b
$ SNat n -> Index (ElementCount a)
forall a (n :: Nat). Num a => SNat n -> a
snatToNum SNat n
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 :: forall a. Vec (GElementCount V1) (V1 a)
gElements     = Vec 0 (V1 a)
Vec (GElementCount V1) (V1 a)
forall b. Vec 0 b
Nil
  gLowest :: forall a. (1 <= GElementCount V1) => V1 a
gLowest       = (\case{} :: Dict (1 <= 0) -> a) Dict (TypeError ...)
Dict (1 <= 0)
forall (a :: Constraint). a => Dict a
Dict
  gLowestMaybe :: forall a. Maybe (V1 a)
gLowestMaybe  = Maybe (V1 a)
forall a. Maybe a
Nothing
  gHighest :: forall a. (1 <= GElementCount V1) => V1 a
gHighest      = (\case{} :: Dict (1 <= 0) -> a) Dict (TypeError ...)
Dict (1 <= 0)
forall (a :: Constraint). a => Dict a
Dict
  gHighestMaybe :: forall a. Maybe (V1 a)
gHighestMaybe = Maybe (V1 a)
forall a. Maybe a
Nothing
  gPredMaybe :: forall a. V1 a -> Maybe (V1 a)
gPredMaybe    = Maybe (V1 a) -> V1 a -> Maybe (V1 a)
forall a b. a -> b -> a
const Maybe (V1 a)
forall a. Maybe a
Nothing
  gSuccMaybe :: forall a. V1 a -> Maybe (V1 a)
gSuccMaybe    = Maybe (V1 a) -> V1 a -> Maybe (V1 a)
forall a b. a -> b -> a
const Maybe (V1 a)
forall a. Maybe a
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 :: forall a. Index (GElementCount V1) -> V1 a
gIth Index (GElementCount V1)
a        = String -> V1 a
forall a. HasCallStack => String -> a
errorX (String -> V1 a) -> String -> V1 a
forall a b. (a -> b) -> a -> b
$ String
"Index 0 cannot contain any values like " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Index 0 -> String
forall a. Show a => a -> String
show Index 0
Index (GElementCount V1)
a
  gIndex :: forall a. V1 a -> Index (GElementCount V1)
gIndex        = \case {}

instance GFinite U1 where
  type GElementCount U1 = 1
  gElements :: forall a. Vec (GElementCount U1) (U1 a)
gElements     = U1 a
forall k (p :: k). U1 p
U1 U1 a -> Vec 0 (U1 a) -> Vec (0 + 1) (U1 a)
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
:> Vec 0 (U1 a)
forall b. Vec 0 b
Nil
  gLowest :: forall a. (1 <= GElementCount U1) => U1 a
gLowest       = U1 a
forall k (p :: k). U1 p
U1
  gLowestMaybe :: forall a. Maybe (U1 a)
gLowestMaybe  = U1 a -> Maybe (U1 a)
forall a. a -> Maybe a
Just U1 a
forall k (p :: k). U1 p
U1
  gHighest :: forall a. (1 <= GElementCount U1) => U1 a
gHighest      = U1 a
forall k (p :: k). U1 p
U1
  gHighestMaybe :: forall a. Maybe (U1 a)
gHighestMaybe = U1 a -> Maybe (U1 a)
forall a. a -> Maybe a
Just U1 a
forall k (p :: k). U1 p
U1
  gPredMaybe :: forall a. U1 a -> Maybe (U1 a)
gPredMaybe    = Maybe (U1 a) -> U1 a -> Maybe (U1 a)
forall a b. a -> b -> a
const Maybe (U1 a)
forall a. Maybe a
Nothing
  gSuccMaybe :: forall a. U1 a -> Maybe (U1 a)
gSuccMaybe    = Maybe (U1 a) -> U1 a -> Maybe (U1 a)
forall a b. a -> b -> a
const Maybe (U1 a)
forall a. Maybe a
Nothing
  gIth :: forall a. Index (GElementCount U1) -> U1 a
gIth          = U1 a -> Index 1 -> U1 a
forall a b. a -> b -> a
const U1 a
forall k (p :: k). U1 p
U1
  gIndex :: forall a. U1 a -> Index (GElementCount U1)
gIndex        = Index 1 -> U1 a -> Index 1
forall a b. a -> b -> a
const Index 1
0

instance Finite a => GFinite (K1 i a) where
  type GElementCount (K1 _ a)  = ElementCount a
  gElements :: forall a. Vec (GElementCount (K1 i a)) (K1 i a a)
gElements     = a -> K1 i a a
forall k i c (p :: k). c -> K1 i c p
K1 (a -> K1 i a a)
-> Vec (ElementCount a) a -> Vec (ElementCount a) (K1 i a a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vec (ElementCount a) a
forall a. Finite a => Vec (ElementCount a) a
elements
  gLowest :: forall a. (1 <= GElementCount (K1 i a)) => K1 i a a
gLowest       = a -> K1 i a a
forall k i c (p :: k). c -> K1 i c p
K1 a
forall a. (Finite a, 1 <= ElementCount a) => a
lowest
  gLowestMaybe :: forall a. Maybe (K1 i a a)
gLowestMaybe  = a -> K1 i a a
forall k i c (p :: k). c -> K1 i c p
K1 (a -> K1 i a a) -> Maybe a -> Maybe (K1 i a a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe a
forall a. Finite a => Maybe a
lowestMaybe
  gHighest :: forall a. (1 <= GElementCount (K1 i a)) => K1 i a a
gHighest      = a -> K1 i a a
forall k i c (p :: k). c -> K1 i c p
K1 a
forall a. (Finite a, 1 <= ElementCount a) => a
highest
  gHighestMaybe :: forall a. Maybe (K1 i a a)
gHighestMaybe = a -> K1 i a a
forall k i c (p :: k). c -> K1 i c p
K1 (a -> K1 i a a) -> Maybe a -> Maybe (K1 i a a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe a
forall a. Finite a => Maybe a
highestMaybe
  gPredMaybe :: forall a. K1 i a a -> Maybe (K1 i a a)
gPredMaybe    = (a -> K1 i a a) -> Maybe a -> Maybe (K1 i a a)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> K1 i a a
forall k i c (p :: k). c -> K1 i c p
K1 (Maybe a -> Maybe (K1 i a a))
-> (K1 i a a -> Maybe a) -> K1 i a a -> Maybe (K1 i a a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. Finite a => a -> Maybe a
predMaybe (a -> Maybe a) -> (K1 i a a -> a) -> K1 i a a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K1 i a a -> a
forall k i c (p :: k). K1 i c p -> c
unK1
  gSuccMaybe :: forall a. K1 i a a -> Maybe (K1 i a a)
gSuccMaybe    = (a -> K1 i a a) -> Maybe a -> Maybe (K1 i a a)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> K1 i a a
forall k i c (p :: k). c -> K1 i c p
K1 (Maybe a -> Maybe (K1 i a a))
-> (K1 i a a -> Maybe a) -> K1 i a a -> Maybe (K1 i a a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. Finite a => a -> Maybe a
succMaybe (a -> Maybe a) -> (K1 i a a -> a) -> K1 i a a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K1 i a a -> a
forall k i c (p :: k). K1 i c p -> c
unK1
  gIth :: forall a. Index (GElementCount (K1 i a)) -> K1 i a a
gIth          = a -> K1 i a a
forall k i c (p :: k). c -> K1 i c p
K1 (a -> K1 i a a)
-> (Index (ElementCount a) -> a)
-> Index (ElementCount a)
-> K1 i a a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (ElementCount a) -> a
forall a. Finite a => Index (ElementCount a) -> a
ith
  gIndex :: forall a. K1 i a a -> Index (GElementCount (K1 i a))
gIndex        = a -> Index (ElementCount a)
forall a. Finite a => a -> Index (ElementCount a)
index (a -> Index (ElementCount a))
-> (K1 i a a -> a) -> K1 i a a -> Index (ElementCount a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K1 i a a -> a
forall k i c (p :: k). K1 i c p -> c
unK1

instance GFinite a => GFinite (M1 i v a) where
  type GElementCount (M1 _ _ a) = GElementCount a
  gElements :: forall a. Vec (GElementCount (M1 i v a)) (M1 i v a a)
gElements     = a a -> M1 i v a a
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 (a a -> M1 i v a a)
-> Vec (GElementCount a) (a a)
-> Vec (GElementCount a) (M1 i v a a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vec (GElementCount a) (a a)
forall a. Vec (GElementCount a) (a a)
forall (rep :: Type -> Type) a.
GFinite rep =>
Vec (GElementCount rep) (rep a)
gElements
  gLowest :: forall a. (1 <= GElementCount (M1 i v a)) => M1 i v a a
gLowest       = a a -> M1 i v a a
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 a a
forall a. (1 <= GElementCount a) => a a
forall (rep :: Type -> Type) a.
(GFinite rep, 1 <= GElementCount rep) =>
rep a
gLowest
  gLowestMaybe :: forall a. Maybe (M1 i v a a)
gLowestMaybe  = a a -> M1 i v a a
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 (a a -> M1 i v a a) -> Maybe (a a) -> Maybe (M1 i v a a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (a a)
forall a. Maybe (a a)
forall (rep :: Type -> Type) a. GFinite rep => Maybe (rep a)
gLowestMaybe
  gHighest :: forall a. (1 <= GElementCount (M1 i v a)) => M1 i v a a
gHighest      = a a -> M1 i v a a
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 a a
forall a. (1 <= GElementCount a) => a a
forall (rep :: Type -> Type) a.
(GFinite rep, 1 <= GElementCount rep) =>
rep a
gHighest
  gHighestMaybe :: forall a. Maybe (M1 i v a a)
gHighestMaybe = a a -> M1 i v a a
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 (a a -> M1 i v a a) -> Maybe (a a) -> Maybe (M1 i v a a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (a a)
forall a. Maybe (a a)
forall (rep :: Type -> Type) a. GFinite rep => Maybe (rep a)
gHighestMaybe
  gPredMaybe :: forall a. M1 i v a a -> Maybe (M1 i v a a)
gPredMaybe    = (a a -> M1 i v a a) -> Maybe (a a) -> Maybe (M1 i v a a)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a a -> M1 i v a a
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 (Maybe (a a) -> Maybe (M1 i v a a))
-> (M1 i v a a -> Maybe (a a)) -> M1 i v a a -> Maybe (M1 i v a a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a a -> Maybe (a a)
forall a. a a -> Maybe (a a)
forall (rep :: Type -> Type) a.
GFinite rep =>
rep a -> Maybe (rep a)
gPredMaybe (a a -> Maybe (a a))
-> (M1 i v a a -> a a) -> M1 i v a a -> Maybe (a a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 i v a a -> a a
forall k i (c :: Meta) (f :: k -> Type) (p :: k). M1 i c f p -> f p
unM1
  gSuccMaybe :: forall a. M1 i v a a -> Maybe (M1 i v a a)
gSuccMaybe    = (a a -> M1 i v a a) -> Maybe (a a) -> Maybe (M1 i v a a)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a a -> M1 i v a a
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 (Maybe (a a) -> Maybe (M1 i v a a))
-> (M1 i v a a -> Maybe (a a)) -> M1 i v a a -> Maybe (M1 i v a a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a a -> Maybe (a a)
forall a. a a -> Maybe (a a)
forall (rep :: Type -> Type) a.
GFinite rep =>
rep a -> Maybe (rep a)
gSuccMaybe (a a -> Maybe (a a))
-> (M1 i v a a -> a a) -> M1 i v a a -> Maybe (a a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 i v a a -> a a
forall k i (c :: Meta) (f :: k -> Type) (p :: k). M1 i c f p -> f p
unM1
  gIth :: forall a. Index (GElementCount (M1 i v a)) -> M1 i v a a
gIth          = a a -> M1 i v a a
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 (a a -> M1 i v a a)
-> (Index (GElementCount a) -> a a)
-> Index (GElementCount a)
-> M1 i v a a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (GElementCount a) -> a a
forall a. Index (GElementCount a) -> a a
forall (rep :: Type -> Type) a.
GFinite rep =>
Index (GElementCount rep) -> rep a
gIth
  gIndex :: forall a. M1 i v a a -> Index (GElementCount (M1 i v a))
gIndex        = a a -> Index (GElementCount a)
forall a. a a -> Index (GElementCount a)
forall (rep :: Type -> Type) a.
GFinite rep =>
rep a -> Index (GElementCount rep)
gIndex (a a -> Index (GElementCount a))
-> (M1 i v a a -> a a) -> M1 i v a a -> Index (GElementCount a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 i v a a -> a a
forall k i (c :: Meta) (f :: k -> Type) (p :: k). M1 i c f p -> f p
unM1

instance (GFinite a, GFinite b) => GFinite (a :*: b) where
  type GElementCount (a :*: b) = GElementCount a * GElementCount b
  gElements :: forall a. Vec (GElementCount (a :*: b)) ((:*:) a b a)
gElements = (a a -> Vec (GElementCount b) ((:*:) a b a))
-> Vec (GElementCount a) (a a)
-> Vec (GElementCount a * GElementCount b) ((:*:) a b a)
forall a (m :: Nat) b (n :: Nat).
(a -> Vec m b) -> Vec n a -> Vec (n * m) b
concatMap (\a a
a -> (a a
a a a -> b a -> (:*:) a b a
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*:) (b a -> (:*:) a b a)
-> Vec (GElementCount b) (b a)
-> Vec (GElementCount b) ((:*:) a b a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (rep :: Type -> Type) a.
GFinite rep =>
Vec (GElementCount rep) (rep a)
gElements @b) (forall (rep :: Type -> Type) a.
GFinite rep =>
Vec (GElementCount rep) (rep a)
gElements @a)

  gLowest :: forall a. (1 <= GElementCount (a :*: b)) => (:*:) a b a
gLowest
    | Dict (1 <= GElementCount a, 1 <= GElementCount b)
Dict <- forall (n :: Nat) (m :: Nat).
(1 <= (n * m)) =>
Dict (1 <= n, 1 <= m)
mulPositiveImpliesPositiveOperands @(GElementCount a) @(GElementCount b)
    = a a
forall a. (1 <= GElementCount a) => a a
forall (rep :: Type -> Type) a.
(GFinite rep, 1 <= GElementCount rep) =>
rep a
gLowest a a -> b a -> (:*:) a b a
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: b a
forall a. (1 <= GElementCount b) => b a
forall (rep :: Type -> Type) a.
(GFinite rep, 1 <= GElementCount rep) =>
rep a
gLowest
  gLowestMaybe :: forall a. Maybe ((:*:) a b a)
gLowestMaybe = a a -> b a -> (:*:) a b a
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
(:*:) (a a -> b a -> (:*:) a b a)
-> Maybe (a a) -> Maybe (b a -> (:*:) a b a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (a a)
forall a. Maybe (a a)
forall (rep :: Type -> Type) a. GFinite rep => Maybe (rep a)
gLowestMaybe  Maybe (b a -> (:*:) a b a) -> Maybe (b a) -> Maybe ((:*:) a b a)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Maybe (b a)
forall a. Maybe (b a)
forall (rep :: Type -> Type) a. GFinite rep => Maybe (rep a)
gLowestMaybe

  gHighest :: forall a. (1 <= GElementCount (a :*: b)) => (:*:) a b a
gHighest
    | Dict (1 <= GElementCount a, 1 <= GElementCount b)
Dict <- forall (n :: Nat) (m :: Nat).
(1 <= (n * m)) =>
Dict (1 <= n, 1 <= m)
mulPositiveImpliesPositiveOperands @(GElementCount a) @(GElementCount b)
    = a a
forall a. (1 <= GElementCount a) => a a
forall (rep :: Type -> Type) a.
(GFinite rep, 1 <= GElementCount rep) =>
rep a
gHighest a a -> b a -> (:*:) a b a
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: b a
forall a. (1 <= GElementCount b) => b a
forall (rep :: Type -> Type) a.
(GFinite rep, 1 <= GElementCount rep) =>
rep a
gHighest
  gHighestMaybe :: forall a. Maybe ((:*:) a b a)
gHighestMaybe = a a -> b a -> (:*:) a b a
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
(:*:) (a a -> b a -> (:*:) a b a)
-> Maybe (a a) -> Maybe (b a -> (:*:) a b a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (a a)
forall a. Maybe (a a)
forall (rep :: Type -> Type) a. GFinite rep => Maybe (rep a)
gHighestMaybe Maybe (b a -> (:*:) a b a) -> Maybe (b a) -> Maybe ((:*:) a b a)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Maybe (b a)
forall a. Maybe (b a)
forall (rep :: Type -> Type) a. GFinite rep => Maybe (rep a)
gHighestMaybe

  gPredMaybe :: forall a. (:*:) a b a -> Maybe ((:*:) a b a)
gPredMaybe (a a
a :*: b a
b) =
        a a -> b a -> (:*:) a b a
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
(:*:)             a a
a (b a -> (:*:) a b a) -> Maybe (b a) -> Maybe ((:*:) a b a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> b a -> Maybe (b a)
forall a. b a -> Maybe (b a)
forall (rep :: Type -> Type) a.
GFinite rep =>
rep a -> Maybe (rep a)
gPredMaybe b a
b
    Maybe ((:*:) a b a) -> Maybe ((:*:) a b a) -> Maybe ((:*:) a b a)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> a a -> b a -> (:*:) a b a
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
(:*:) (a a -> b a -> (:*:) a b a)
-> Maybe (a a) -> Maybe (b a -> (:*:) a b a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> a a -> Maybe (a a)
forall a. a a -> Maybe (a a)
forall (rep :: Type -> Type) a.
GFinite rep =>
rep a -> Maybe (rep a)
gPredMaybe a a
a Maybe (b a -> (:*:) a b a) -> Maybe (b a) -> Maybe ((:*:) a b a)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Maybe (b a)
forall a. Maybe (b a)
forall (rep :: Type -> Type) a. GFinite rep => Maybe (rep a)
gHighestMaybe
  gSuccMaybe :: forall a. (:*:) a b a -> Maybe ((:*:) a b a)
gSuccMaybe (a a
a :*: b a
b) =
        a a -> b a -> (:*:) a b a
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
(:*:)            a a
a (b a -> (:*:) a b a) -> Maybe (b a) -> Maybe ((:*:) a b a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> b a -> Maybe (b a)
forall a. b a -> Maybe (b a)
forall (rep :: Type -> Type) a.
GFinite rep =>
rep a -> Maybe (rep a)
gSuccMaybe b a
b
    Maybe ((:*:) a b a) -> Maybe ((:*:) a b a) -> Maybe ((:*:) a b a)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> a a -> b a -> (:*:) a b a
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
(:*:) (a a -> b a -> (:*:) a b a)
-> Maybe (a a) -> Maybe (b a -> (:*:) a b a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> a a -> Maybe (a a)
forall a. a a -> Maybe (a a)
forall (rep :: Type -> Type) a.
GFinite rep =>
rep a -> Maybe (rep a)
gSuccMaybe a a
a Maybe (b a -> (:*:) a b a) -> Maybe (b a) -> Maybe ((:*:) a b a)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Maybe (b a)
forall a. Maybe (b a)
forall (rep :: Type -> Type) a. GFinite rep => Maybe (rep a)
gLowestMaybe

  gIth :: forall a. Index (GElementCount (a :*: b)) -> (:*:) a b a
gIth Index (GElementCount (a :*: b))
x = Index (GElementCount a) -> a a
forall a. Index (GElementCount a) -> a a
forall (rep :: Type -> Type) a.
GFinite rep =>
Index (GElementCount rep) -> rep a
gIth (Index (GElementCount a * GElementCount b)
-> Index (GElementCount a)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b) =>
Index a -> Index b
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f b
resize (Index (GElementCount a * GElementCount b)
 -> Index (GElementCount a))
-> Index (GElementCount a * GElementCount b)
-> Index (GElementCount a)
forall a b. (a -> b) -> a -> b
$ Index (GElementCount a * GElementCount b)
Index (GElementCount (a :*: b))
x Index (GElementCount a * GElementCount b)
-> Index (GElementCount a * GElementCount b)
-> Index (GElementCount a * GElementCount b)
forall a. Integral a => a -> a -> a
`div` Index (GElementCount a * GElementCount b)
m) a a -> b a -> (:*:) a b a
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Index (GElementCount b) -> b a
forall a. Index (GElementCount b) -> b a
forall (rep :: Type -> Type) a.
GFinite rep =>
Index (GElementCount rep) -> rep a
gIth (Index (GElementCount a * GElementCount b)
-> Index (GElementCount b)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b) =>
Index a -> Index b
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f b
resize (Index (GElementCount a * GElementCount b)
 -> Index (GElementCount b))
-> Index (GElementCount a * GElementCount b)
-> Index (GElementCount b)
forall a b. (a -> b) -> a -> b
$ Index (GElementCount a * GElementCount b)
Index (GElementCount (a :*: b))
x Index (GElementCount a * GElementCount b)
-> Index (GElementCount a * GElementCount b)
-> Index (GElementCount a * GElementCount b)
forall a. Integral a => a -> a -> a
`mod` Index (GElementCount a * GElementCount b)
m)
   where
    m :: Index (GElementCount a * GElementCount b)
m = forall (n :: Nat) a. (Num a, KnownNat n) => a
natToNum @(GElementCount b)

  gIndex :: forall a. (:*:) a b a -> Index (GElementCount (a :*: b))
gIndex (a a
a :*: b a
b) =
      Index (GElementCount a)
-> Index (GElementCount a * GElementCount b)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b) =>
Index a -> Index b
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f b
resize (a a -> Index (GElementCount a)
forall a. a a -> Index (GElementCount a)
forall (rep :: Type -> Type) a.
GFinite rep =>
rep a -> Index (GElementCount rep)
gIndex a a
a) Index (GElementCount a * GElementCount b)
-> Index (GElementCount a * GElementCount b)
-> Index (GElementCount a * GElementCount b)
forall a. Num a => a -> a -> a
* forall (n :: Nat) a. (Num a, KnownNat n) => a
natToNum @(GElementCount b)
    Index (GElementCount a * GElementCount b)
-> Index (GElementCount a * GElementCount b)
-> Index (GElementCount a * GElementCount b)
forall a. Num a => a -> a -> a
+ Index (GElementCount b)
-> Index (GElementCount a * GElementCount b)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b) =>
Index a -> Index b
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f b
resize (b a -> Index (GElementCount b)
forall a. b a -> Index (GElementCount b)
forall (rep :: Type -> Type) a.
GFinite rep =>
rep a -> Index (GElementCount rep)
gIndex b a
b)

instance (GFinite a, GFinite b) => GFinite (a :+: b) where
  type GElementCount (a :+: b) = GElementCount a + GElementCount b
  gElements :: forall a. Vec (GElementCount (a :+: b)) ((:+:) a b a)
gElements = (a a -> (:+:) a b a
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 (a a -> (:+:) a b a)
-> Vec (GElementCount a) (a a)
-> Vec (GElementCount a) ((:+:) a b a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (rep :: Type -> Type) a.
GFinite rep =>
Vec (GElementCount rep) (rep a)
gElements @a) Vec (GElementCount a) ((:+:) a b a)
-> Vec (GElementCount b) ((:+:) a b a)
-> Vec (GElementCount a + GElementCount b) ((:+:) a b a)
forall (n :: Nat) a (m :: Nat). Vec n a -> Vec m a -> Vec (n + m) a
++ (b a -> (:+:) a b a
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 (b a -> (:+:) a b a)
-> Vec (GElementCount b) (b a)
-> Vec (GElementCount b) ((:+:) a b a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (rep :: Type -> Type) a.
GFinite rep =>
Vec (GElementCount rep) (rep a)
gElements @b)

  gLowest :: forall a. (1 <= GElementCount (a :+: b)) => (:+:) a b a
gLowest = case SNat 1 -> SNat (GElementCount a) -> SNatLE 1 (GElementCount a)
forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> SNatLE a b
compareSNat (forall (n :: Nat). KnownNat n => SNat n
SNat @1) (forall (n :: Nat). KnownNat n => SNat n
SNat @(GElementCount a)) of
    SNatLE 1 (GElementCount a)
SNatLE -> a a -> (:+:) a b a
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 a a
forall a. (1 <= GElementCount a) => a a
forall (rep :: Type -> Type) a.
(GFinite rep, 1 <= GElementCount rep) =>
rep a
gLowest
    SNatLE 1 (GElementCount a)
SNatGT -> case SNat 1 -> SNat (GElementCount b) -> SNatLE 1 (GElementCount b)
forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> SNatLE a b
compareSNat (forall (n :: Nat). KnownNat n => SNat n
SNat @1) (forall (n :: Nat). KnownNat n => SNat n
SNat @(GElementCount b)) of
      SNatLE 1 (GElementCount b)
SNatLE -> b a -> (:+:) a b a
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 b a
forall a. (1 <= GElementCount b) => b a
forall (rep :: Type -> Type) a.
(GFinite rep, 1 <= GElementCount rep) =>
rep a
gLowest
      SNatLE 1 (GElementCount b)
SNatGT -> case forall (n :: Nat) (m :: Nat). ((n + m) <= m) => Dict (n ~ 0)
zeroLeAdd @(GElementCount a) @1 of
        Dict (GElementCount a ~ 0)
Dict -> case forall (n :: Nat) (m :: Nat). ((n + m) <= m) => Dict (n ~ 0)
zeroLeAdd @(GElementCount b) @1 of {}
  gLowestMaybe :: forall a. Maybe ((:+:) a b a)
gLowestMaybe = a a -> (:+:) a b a
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 (a a -> (:+:) a b a) -> Maybe (a a) -> Maybe ((:+:) a b a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (rep :: Type -> Type) a. GFinite rep => Maybe (rep a)
gLowestMaybe  @a Maybe ((:+:) a b a) -> Maybe ((:+:) a b a) -> Maybe ((:+:) a b a)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> b a -> (:+:) a b a
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 (b a -> (:+:) a b a) -> Maybe (b a) -> Maybe ((:+:) a b a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (rep :: Type -> Type) a. GFinite rep => Maybe (rep a)
gLowestMaybe  @b

  gHighest :: forall a. (1 <= GElementCount (a :+: b)) => (:+:) a b a
gHighest = case SNat 1 -> SNat (GElementCount b) -> SNatLE 1 (GElementCount b)
forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> SNatLE a b
compareSNat (forall (n :: Nat). KnownNat n => SNat n
SNat @1) (forall (n :: Nat). KnownNat n => SNat n
SNat @(GElementCount b)) of
    SNatLE 1 (GElementCount b)
SNatLE -> b a -> (:+:) a b a
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 b a
forall a. (1 <= GElementCount b) => b a
forall (rep :: Type -> Type) a.
(GFinite rep, 1 <= GElementCount rep) =>
rep a
gHighest
    SNatLE 1 (GElementCount b)
SNatGT -> case SNat 1 -> SNat (GElementCount a) -> SNatLE 1 (GElementCount a)
forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> SNatLE a b
compareSNat (forall (n :: Nat). KnownNat n => SNat n
SNat @1) (forall (n :: Nat). KnownNat n => SNat n
SNat @(GElementCount a)) of
      SNatLE 1 (GElementCount a)
SNatLE -> a a -> (:+:) a b a
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 a a
forall a. (1 <= GElementCount a) => a a
forall (rep :: Type -> Type) a.
(GFinite rep, 1 <= GElementCount rep) =>
rep a
gHighest
      SNatLE 1 (GElementCount a)
SNatGT -> case forall (n :: Nat) (m :: Nat). ((n + m) <= m) => Dict (n ~ 0)
zeroLeAdd @(GElementCount a) @1 of
        Dict (GElementCount a ~ 0)
Dict -> case forall (n :: Nat) (m :: Nat). ((n + m) <= m) => Dict (n ~ 0)
zeroLeAdd @(GElementCount b) @1 of {}
  gHighestMaybe :: forall a. Maybe ((:+:) a b a)
gHighestMaybe = b a -> (:+:) a b a
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 (b a -> (:+:) a b a) -> Maybe (b a) -> Maybe ((:+:) a b a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (rep :: Type -> Type) a. GFinite rep => Maybe (rep a)
gHighestMaybe @b Maybe ((:+:) a b a) -> Maybe ((:+:) a b a) -> Maybe ((:+:) a b a)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> a a -> (:+:) a b a
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 (a a -> (:+:) a b a) -> Maybe (a a) -> Maybe ((:+:) a b a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (rep :: Type -> Type) a. GFinite rep => Maybe (rep a)
gHighestMaybe @a

  gPredMaybe :: forall a. (:+:) a b a -> Maybe ((:+:) a b a)
gPredMaybe = \case
    L1 a a
x -> a a -> (:+:) a b a
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 (a a -> (:+:) a b a) -> Maybe (a a) -> Maybe ((:+:) a b a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> a a -> Maybe (a a)
forall a. a a -> Maybe (a a)
forall (rep :: Type -> Type) a.
GFinite rep =>
rep a -> Maybe (rep a)
gPredMaybe a a
x
    R1 b a
x -> b a -> (:+:) a b a
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 (b a -> (:+:) a b a) -> Maybe (b a) -> Maybe ((:+:) a b a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> b a -> Maybe (b a)
forall a. b a -> Maybe (b a)
forall (rep :: Type -> Type) a.
GFinite rep =>
rep a -> Maybe (rep a)
gPredMaybe b a
x Maybe ((:+:) a b a) -> Maybe ((:+:) a b a) -> Maybe ((:+:) a b a)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> a a -> (:+:) a b a
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 (a a -> (:+:) a b a) -> Maybe (a a) -> Maybe ((:+:) a b a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (a a)
forall a. Maybe (a a)
forall (rep :: Type -> Type) a. GFinite rep => Maybe (rep a)
gHighestMaybe

  gSuccMaybe :: forall a. (:+:) a b a -> Maybe ((:+:) a b a)
gSuccMaybe = \case
    R1 b a
x -> b a -> (:+:) a b a
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 (b a -> (:+:) a b a) -> Maybe (b a) -> Maybe ((:+:) a b a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> b a -> Maybe (b a)
forall a. b a -> Maybe (b a)
forall (rep :: Type -> Type) a.
GFinite rep =>
rep a -> Maybe (rep a)
gSuccMaybe b a
x
    L1 a a
x -> a a -> (:+:) a b a
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 (a a -> (:+:) a b a) -> Maybe (a a) -> Maybe ((:+:) a b a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> a a -> Maybe (a a)
forall a. a a -> Maybe (a a)
forall (rep :: Type -> Type) a.
GFinite rep =>
rep a -> Maybe (rep a)
gSuccMaybe a a
x Maybe ((:+:) a b a) -> Maybe ((:+:) a b a) -> Maybe ((:+:) a b a)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> b a -> (:+:) a b a
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 (b a -> (:+:) a b a) -> Maybe (b a) -> Maybe ((:+:) a b a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (b a)
forall a. Maybe (b a)
forall (rep :: Type -> Type) a. GFinite rep => Maybe (rep a)
gLowestMaybe

  gIth :: forall a. Index (GElementCount (a :+: b)) -> (:+:) a b a
gIth Index (GElementCount (a :+: b))
x
    | Index (GElementCount (a :+: b))
-> Index
     (If (GElementCount (a :+: b) <=? GElementCount a) 1 0
      + GElementCount (a :+: b))
e Index (GElementCount (a :+: b))
x Index
  (If
     (OrdCond
        (CmpNat (GElementCount a + GElementCount b) (GElementCount a))
        'True
        'True
        'False)
     1
     0
   + (GElementCount a + GElementCount b))
-> Index
     (If
        (OrdCond
           (CmpNat (GElementCount a + GElementCount b) (GElementCount a))
           'True
           'True
           'False)
        1
        0
      + (GElementCount a + GElementCount b))
-> Bool
forall a. Ord a => a -> a -> Bool
< Index
  (If
     (OrdCond
        (CmpNat (GElementCount a + GElementCount b) (GElementCount a))
        'True
        'True
        'False)
     1
     0
   + (GElementCount a + GElementCount b))
n   = a a -> (:+:) a b a
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 (a a -> (:+:) a b a) -> a a -> (:+:) a b a
forall a b. (a -> b) -> a -> b
$ Index (GElementCount a) -> a a
forall a. Index (GElementCount a) -> a a
forall (rep :: Type -> Type) a.
GFinite rep =>
Index (GElementCount rep) -> rep a
gIth (Index (GElementCount a) -> a a) -> Index (GElementCount a) -> a a
forall a b. (a -> b) -> a -> b
$ Index (GElementCount a + GElementCount b)
-> Index (GElementCount a)
forall (a :: Nat) (b :: Nat).
KnownNat a =>
Index (a + b) -> Index a
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a) =>
f (a + b) -> f a
truncateB Index (GElementCount a + GElementCount b)
Index (GElementCount (a :+: b))
x
    | Bool
otherwise = b a -> (:+:) a b a
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 (b a -> (:+:) a b a) -> b a -> (:+:) a b a
forall a b. (a -> b) -> a -> b
$ Index (GElementCount b) -> b a
forall a. Index (GElementCount b) -> b a
forall (rep :: Type -> Type) a.
GFinite rep =>
Index (GElementCount rep) -> rep a
gIth (Index (GElementCount b) -> b a) -> Index (GElementCount b) -> b a
forall a b. (a -> b) -> a -> b
$ Index
  (GElementCount b
   + (If
        (OrdCond
           (CmpNat (GElementCount a + GElementCount b) (GElementCount a))
           'True
           'True
           'False)
        1
        0
      + GElementCount a))
-> Index (GElementCount b)
forall (a :: Nat) (b :: Nat).
KnownNat a =>
Index (a + b) -> Index a
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a) =>
f (a + b) -> f a
truncateB (Index
   (GElementCount b
    + (If
         (OrdCond
            (CmpNat (GElementCount a + GElementCount b) (GElementCount a))
            'True
            'True
            'False)
         1
         0
       + GElementCount a))
 -> Index (GElementCount b))
-> Index
     (GElementCount b
      + (If
           (OrdCond
              (CmpNat (GElementCount a + GElementCount b) (GElementCount a))
              'True
              'True
              'False)
           1
           0
         + GElementCount a))
-> Index (GElementCount b)
forall a b. (a -> b) -> a -> b
$ Index (GElementCount (a :+: b))
-> Index
     (If (GElementCount (a :+: b) <=? GElementCount a) 1 0
      + GElementCount (a :+: b))
e Index (GElementCount (a :+: b))
x Index
  (If
     (OrdCond
        (CmpNat (GElementCount a + GElementCount b) (GElementCount a))
        'True
        'True
        'False)
     1
     0
   + (GElementCount a + GElementCount b))
-> Index
     (If
        (OrdCond
           (CmpNat (GElementCount a + GElementCount b) (GElementCount a))
           'True
           'True
           'False)
        1
        0
      + (GElementCount a + GElementCount b))
-> Index
     (If
        (OrdCond
           (CmpNat (GElementCount a + GElementCount b) (GElementCount a))
           'True
           'True
           'False)
        1
        0
      + (GElementCount a + GElementCount b))
forall a. Num a => a -> a -> a
- Index
  (If
     (OrdCond
        (CmpNat (GElementCount a + GElementCount b) (GElementCount a))
        'True
        'True
        'False)
     1
     0
   + (GElementCount a + GElementCount b))
n
   where
    n :: Index
  (If
     (OrdCond
        (CmpNat (GElementCount a + GElementCount b) (GElementCount a))
        'True
        'True
        'False)
     1
     0
   + (GElementCount a + GElementCount b))
n = forall (n :: Nat) a. (Num a, KnownNat n) => a
natToNum @(GElementCount a)
    e :: Index (GElementCount (a :+: b))
-> Index
     (If (GElementCount (a :+: b) <=? GElementCount a) 1 0
      + GElementCount (a :+: b))
e = forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f (b + a)
extend @Index @(GElementCount (a :+: b))
      @(If (GElementCount (a :+: b) <=? GElementCount a) 1 0)

  gIndex :: forall a. (:+:) a b a -> Index (GElementCount (a :+: b))
gIndex = \case
    L1 a a
x -> Index (GElementCount a)
-> Index (GElementCount b + GElementCount a)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b) =>
Index a -> Index (b + a)
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f (b + a)
extend (a a -> Index (GElementCount a)
forall a. a a -> Index (GElementCount a)
forall (rep :: Type -> Type) a.
GFinite rep =>
rep a -> Index (GElementCount rep)
gIndex a a
x)
    R1 b a
x -> Index (GElementCount b)
-> Index (GElementCount a + GElementCount b)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b) =>
Index a -> Index (b + a)
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f (b + a)
extend (b a -> Index (GElementCount b)
forall a. b a -> Index (GElementCount b)
forall (rep :: Type -> Type) a.
GFinite rep =>
rep a -> Index (GElementCount rep)
gIndex b a
x) Index (GElementCount a + GElementCount b)
-> Index (GElementCount a + GElementCount b)
-> Index (GElementCount a + GElementCount b)
forall a. Num a => a -> a -> a
+ forall (n :: Nat) a. (Num a, KnownNat n) => a
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 :: Vec (ElementCount (SNat n)) (SNat n)
elements     = SNat n
forall (n :: Nat). KnownNat n => SNat n
SNat SNat n -> Vec 0 (SNat n) -> Vec (0 + 1) (SNat n)
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
:> Vec 0 (SNat n)
forall b. Vec 0 b
Nil
  lowest :: (1 <= ElementCount (SNat n)) => SNat n
lowest       = SNat n
forall (n :: Nat). KnownNat n => SNat n
SNat
  lowestMaybe :: Maybe (SNat n)
lowestMaybe  = SNat n -> Maybe (SNat n)
forall a. a -> Maybe a
Just SNat n
forall (n :: Nat). KnownNat n => SNat n
SNat
  highest :: (1 <= ElementCount (SNat n)) => SNat n
highest      = SNat n
forall (n :: Nat). KnownNat n => SNat n
SNat
  highestMaybe :: Maybe (SNat n)
highestMaybe = SNat n -> Maybe (SNat n)
forall a. a -> Maybe a
Just SNat n
forall (n :: Nat). KnownNat n => SNat n
SNat
  predMaybe :: SNat n -> Maybe (SNat n)
predMaybe    = Maybe (SNat n) -> SNat n -> Maybe (SNat n)
forall a b. a -> b -> a
const Maybe (SNat n)
forall a. Maybe a
Nothing
  succMaybe :: SNat n -> Maybe (SNat n)
succMaybe    = Maybe (SNat n) -> SNat n -> Maybe (SNat n)
forall a b. a -> b -> a
const Maybe (SNat n)
forall a. Maybe a
Nothing
  ith :: Index (ElementCount (SNat n)) -> SNat n
ith          = SNat n -> Index 1 -> SNat n
forall a b. a -> b -> a
const SNat n
forall (n :: Nat). KnownNat n => SNat n
SNat
  index :: SNat n -> Index (ElementCount (SNat n))
index        = Index 1 -> SNat n -> Index 1
forall a b. a -> b -> a
const Index 1
0

instance KnownSymbol s => Finite (SSymbol s) where
  type ElementCount (SSymbol s) = 1
  elements :: Vec (ElementCount (SSymbol s)) (SSymbol s)
elements     = SSymbol s
forall (s :: Symbol). KnownSymbol s => SSymbol s
SSymbol SSymbol s -> Vec 0 (SSymbol s) -> Vec (0 + 1) (SSymbol s)
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
:> Vec 0 (SSymbol s)
forall b. Vec 0 b
Nil
  lowest :: (1 <= ElementCount (SSymbol s)) => SSymbol s
lowest       = SSymbol s
forall (s :: Symbol). KnownSymbol s => SSymbol s
SSymbol
  lowestMaybe :: Maybe (SSymbol s)
lowestMaybe  = SSymbol s -> Maybe (SSymbol s)
forall a. a -> Maybe a
Just SSymbol s
forall (s :: Symbol). KnownSymbol s => SSymbol s
SSymbol
  highest :: (1 <= ElementCount (SSymbol s)) => SSymbol s
highest      = SSymbol s
forall (s :: Symbol). KnownSymbol s => SSymbol s
SSymbol
  highestMaybe :: Maybe (SSymbol s)
highestMaybe = SSymbol s -> Maybe (SSymbol s)
forall a. a -> Maybe a
Just SSymbol s
forall (s :: Symbol). KnownSymbol s => SSymbol s
SSymbol
  predMaybe :: SSymbol s -> Maybe (SSymbol s)
predMaybe    = Maybe (SSymbol s) -> SSymbol s -> Maybe (SSymbol s)
forall a b. a -> b -> a
const Maybe (SSymbol s)
forall a. Maybe a
Nothing
  succMaybe :: SSymbol s -> Maybe (SSymbol s)
succMaybe    = Maybe (SSymbol s) -> SSymbol s -> Maybe (SSymbol s)
forall a b. a -> b -> a
const Maybe (SSymbol s)
forall a. Maybe a
Nothing
  ith :: Index (ElementCount (SSymbol s)) -> SSymbol s
ith          = SSymbol s -> Index 1 -> SSymbol s
forall a b. a -> b -> a
const SSymbol s
forall (s :: Symbol). KnownSymbol s => SSymbol s
SSymbol
  index :: SSymbol s -> Index (ElementCount (SSymbol s))
index        = Index 1 -> SSymbol s -> Index 1
forall a b. a -> b -> a
const Index 1
0

instance c => Finite (Dict c) where
  type ElementCount (Dict c) = 1
  elements :: Vec (ElementCount (Dict c)) (Dict c)
elements     = Dict c
forall (a :: Constraint). a => Dict a
Dict Dict c -> Vec 0 (Dict c) -> Vec (0 + 1) (Dict c)
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
:> Vec 0 (Dict c)
forall b. Vec 0 b
Nil
  lowest :: (1 <= ElementCount (Dict c)) => Dict c
lowest       = Dict c
forall (a :: Constraint). a => Dict a
Dict
  lowestMaybe :: Maybe (Dict c)
lowestMaybe  = Dict c -> Maybe (Dict c)
forall a. a -> Maybe a
Just Dict c
forall (a :: Constraint). a => Dict a
Dict
  highest :: (1 <= ElementCount (Dict c)) => Dict c
highest      = Dict c
forall (a :: Constraint). a => Dict a
Dict
  highestMaybe :: Maybe (Dict c)
highestMaybe = Dict c -> Maybe (Dict c)
forall a. a -> Maybe a
Just Dict c
forall (a :: Constraint). a => Dict a
Dict
  predMaybe :: Dict c -> Maybe (Dict c)
predMaybe    = Maybe (Dict c) -> Dict c -> Maybe (Dict c)
forall a b. a -> b -> a
const Maybe (Dict c)
forall a. Maybe a
Nothing
  succMaybe :: Dict c -> Maybe (Dict c)
succMaybe    = Maybe (Dict c) -> Dict c -> Maybe (Dict c)
forall a b. a -> b -> a
const Maybe (Dict c)
forall a. Maybe a
Nothing
  ith :: Index (ElementCount (Dict c)) -> Dict c
ith          = Dict c -> Index 1 -> Dict c
forall a b. a -> b -> a
const Dict c
forall (a :: Constraint). a => Dict a
Dict
  index :: Dict c -> Index (ElementCount (Dict c))
index        = Index 1 -> Dict c -> Index 1
forall a b. a -> b -> a
const Index 1
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 :: Vec (ElementCount (Index n)) (Index n)
elements     = Vec n (Index n)
Vec (ElementCount (Index n)) (Index n)
forall (n :: Nat). KnownNat n => Vec n (Index n)
indicesI
  lowest :: (1 <= ElementCount (Index n)) => Index n
lowest       = Index n
forall a. Bounded a => a
minBound
  lowestMaybe :: Maybe (Index n)
lowestMaybe  = case SNat n -> UNat n
forall (n :: Nat). SNat n -> UNat n
toUNat (forall (n :: Nat). KnownNat n => SNat n
SNat @n) of
    UNat n
UZero -> Maybe (Index n)
forall a. Maybe a
Nothing
    UNat n
_     -> Index n -> Maybe (Index n)
forall a. a -> Maybe a
Just Index n
forall a. Bounded a => a
minBound
  highest :: (1 <= ElementCount (Index n)) => Index n
highest      = Index n
forall a. Bounded a => a
maxBound
  highestMaybe :: Maybe (Index n)
highestMaybe = case SNat n -> UNat n
forall (n :: Nat). SNat n -> UNat n
toUNat (forall (n :: Nat). KnownNat n => SNat n
SNat @n) of
    UNat n
UZero -> Maybe (Index n)
forall a. Maybe a
Nothing
    UNat n
_     -> Index n -> Maybe (Index n)
forall a. a -> Maybe a
Just Index n
forall a. Bounded a => a
maxBound
  predMaybe :: Index n -> Maybe (Index n)
predMaybe    = case SNat n -> UNat n
forall (n :: Nat). SNat n -> UNat n
toUNat (forall (n :: Nat). KnownNat n => SNat n
SNat @n) of
    UNat n
UZero -> Maybe (Index n) -> Index n -> Maybe (Index n)
forall a b. a -> b -> a
const Maybe (Index n)
forall a. Maybe a
Nothing
    UNat n
_     -> \Index n
n -> if Index n
n Index n -> Index n -> Bool
forall a. Eq a => a -> a -> Bool
== Index n
forall a. Bounded a => a
minBound then Maybe (Index n)
forall a. Maybe a
Nothing else Index n -> Maybe (Index n)
forall a. a -> Maybe a
Just (Index n -> Maybe (Index n)) -> Index n -> Maybe (Index n)
forall a b. (a -> b) -> a -> b
$ Index n
n Index n -> Index n -> Index n
forall a. Num a => a -> a -> a
- Index n
1
  succMaybe :: Index n -> Maybe (Index n)
succMaybe    = case SNat n -> UNat n
forall (n :: Nat). SNat n -> UNat n
toUNat (forall (n :: Nat). KnownNat n => SNat n
SNat @n)of
    UNat n
UZero -> Maybe (Index n) -> Index n -> Maybe (Index n)
forall a b. a -> b -> a
const Maybe (Index n)
forall a. Maybe a
Nothing
    UNat n
_     -> \Index n
n -> if Index n
n Index n -> Index n -> Bool
forall a. Eq a => a -> a -> Bool
== Index n
forall a. Bounded a => a
maxBound then Maybe (Index n)
forall a. Maybe a
Nothing else Index n -> Maybe (Index n)
forall a. a -> Maybe a
Just (Index n -> Maybe (Index n)) -> Index n -> Maybe (Index n)
forall a b. (a -> b) -> a -> b
$ Index n
n Index n -> Index n -> Index n
forall a. Num a => a -> a -> a
+ Index n
1
  ith :: Index (ElementCount (Index n)) -> Index n
ith          = Index n -> Index n
Index (ElementCount (Index n)) -> Index n
forall a. a -> a
id
  index :: Index n -> Index (ElementCount (Index n))
index        = Index n -> Index n
Index n -> Index (ElementCount (Index n))
forall a. a -> a
id

instance KnownNat n => Finite (Signed n) where
  type ElementCount (Signed n) = 2^n
  elements :: Vec (ElementCount (Signed n)) (Signed n)
elements     = (Signed n -> Signed n) -> Signed n -> Vec (2 ^ n) (Signed n)
forall (n :: Nat) a. KnownNat n => (a -> a) -> a -> Vec n a
iterateI (Signed n -> Signed n -> Signed n
forall a. Num a => a -> a -> a
+Signed n
1) Signed n
forall a. Bounded a => a
minBound
  lowest :: (1 <= ElementCount (Signed n)) => Signed n
lowest       = Signed n
forall a. Bounded a => a
minBound
  lowestMaybe :: Maybe (Signed n)
lowestMaybe  = Signed n -> Maybe (Signed n)
forall a. a -> Maybe a
Just Signed n
forall a. Bounded a => a
minBound
  highest :: (1 <= ElementCount (Signed n)) => Signed n
highest      = Signed n
forall a. Bounded a => a
maxBound
  highestMaybe :: Maybe (Signed n)
highestMaybe = Signed n -> Maybe (Signed n)
forall a. a -> Maybe a
Just Signed n
forall a. Bounded a => a
maxBound
  predMaybe :: Signed n -> Maybe (Signed n)
predMaybe Signed n
n  = if Signed n
n Signed n -> Signed n -> Bool
forall a. Eq a => a -> a -> Bool
== Signed n
forall a. Bounded a => a
minBound then Maybe (Signed n)
forall a. Maybe a
Nothing else Signed n -> Maybe (Signed n)
forall a. a -> Maybe a
Just (Signed n -> Maybe (Signed n)) -> Signed n -> Maybe (Signed n)
forall a b. (a -> b) -> a -> b
$ Signed n
n Signed n -> Signed n -> Signed n
forall a. Num a => a -> a -> a
- Signed n
1
  succMaybe :: Signed n -> Maybe (Signed n)
succMaybe Signed n
n  = if Signed n
n Signed n -> Signed n -> Bool
forall a. Eq a => a -> a -> Bool
== Signed n
forall a. Bounded a => a
maxBound then Maybe (Signed n)
forall a. Maybe a
Nothing else Signed n -> Maybe (Signed n)
forall a. a -> Maybe a
Just (Signed n -> Maybe (Signed n)) -> Signed n -> Maybe (Signed n)
forall a b. (a -> b) -> a -> b
$ Signed n
n Signed n -> Signed n -> Signed n
forall a. Num a => a -> a -> a
+ Signed n
1
  ith :: Index (ElementCount (Signed n)) -> Signed n
ith          = BitVector n -> Signed n
BitVector (BitSize (Signed n)) -> Signed n
forall a. BitPack a => BitVector (BitSize a) -> a
unpack (BitVector n -> Signed n)
-> (Index (2 ^ n) -> BitVector n) -> Index (2 ^ n) -> Signed n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BitVector n -> BitVector n -> BitVector n
forall a. Bits a => a -> a -> a
xor (BitVector n -> BitVector n
forall a. Bits a => a -> a
complement (BitVector n -> BitVector n
forall a. Bits a => a -> a
complement BitVector n
0 BitVector n -> Int -> BitVector n
forall a. Bits a => a -> Int -> a
`shiftR` Int
1)) (BitVector n -> BitVector n)
-> (Index (2 ^ n) -> BitVector n) -> Index (2 ^ n) -> BitVector n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (2 ^ n) -> BitVector n
Index (2 ^ n) -> BitVector (BitSize (Index (2 ^ n)))
forall a. BitPack a => a -> BitVector (BitSize a)
pack
  index :: Signed n -> Index (ElementCount (Signed n))
index        = BitVector (BitSize (Index (2 ^ n))) -> Index (2 ^ n)
BitVector (CLog 2 (2 ^ n)) -> Index (2 ^ n)
forall a. BitPack a => BitVector (BitSize a) -> a
unpack (BitVector (CLog 2 (2 ^ n)) -> Index (2 ^ n))
-> (Signed n -> BitVector (CLog 2 (2 ^ n)))
-> Signed n
-> Index (2 ^ n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BitVector (CLog 2 (2 ^ n))
-> BitVector (CLog 2 (2 ^ n)) -> BitVector (CLog 2 (2 ^ n))
forall a. Bits a => a -> a -> a
xor (BitVector (CLog 2 (2 ^ n)) -> BitVector (CLog 2 (2 ^ n))
forall a. Bits a => a -> a
complement (BitVector (CLog 2 (2 ^ n)) -> BitVector (CLog 2 (2 ^ n))
forall a. Bits a => a -> a
complement BitVector (CLog 2 (2 ^ n))
0 BitVector (CLog 2 (2 ^ n)) -> Int -> BitVector (CLog 2 (2 ^ n))
forall a. Bits a => a -> Int -> a
`shiftR` Int
1)) (BitVector (CLog 2 (2 ^ n)) -> BitVector (CLog 2 (2 ^ n)))
-> (Signed n -> BitVector (CLog 2 (2 ^ n)))
-> Signed n
-> BitVector (CLog 2 (2 ^ n))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Signed n -> BitVector (BitSize (Signed n))
Signed n -> BitVector (CLog 2 (2 ^ n))
forall a. BitPack a => a -> BitVector (BitSize a)
pack

instance KnownNat n => Finite (Unsigned n) where
  type ElementCount (Unsigned n) = 2^n
  elements :: Vec (ElementCount (Unsigned n)) (Unsigned n)
elements     = (Unsigned n -> Unsigned n)
-> Unsigned n -> Vec (2 ^ n) (Unsigned n)
forall (n :: Nat) a. KnownNat n => (a -> a) -> a -> Vec n a
iterateI (Unsigned n -> Unsigned n -> Unsigned n
forall a. Num a => a -> a -> a
+Unsigned n
1) Unsigned n
forall a. Bounded a => a
minBound
  lowest :: (1 <= ElementCount (Unsigned n)) => Unsigned n
lowest       = Unsigned n
forall a. Bounded a => a
minBound
  lowestMaybe :: Maybe (Unsigned n)
lowestMaybe  = Unsigned n -> Maybe (Unsigned n)
forall a. a -> Maybe a
Just Unsigned n
forall a. Bounded a => a
minBound
  highest :: (1 <= ElementCount (Unsigned n)) => Unsigned n
highest      = Unsigned n
forall a. Bounded a => a
maxBound
  highestMaybe :: Maybe (Unsigned n)
highestMaybe = Unsigned n -> Maybe (Unsigned n)
forall a. a -> Maybe a
Just Unsigned n
forall a. Bounded a => a
maxBound
  predMaybe :: Unsigned n -> Maybe (Unsigned n)
predMaybe Unsigned n
n  = if Unsigned n
n Unsigned n -> Unsigned n -> Bool
forall a. Eq a => a -> a -> Bool
== Unsigned n
forall a. Bounded a => a
minBound then Maybe (Unsigned n)
forall a. Maybe a
Nothing else Unsigned n -> Maybe (Unsigned n)
forall a. a -> Maybe a
Just (Unsigned n -> Maybe (Unsigned n))
-> Unsigned n -> Maybe (Unsigned n)
forall a b. (a -> b) -> a -> b
$ Unsigned n
n Unsigned n -> Unsigned n -> Unsigned n
forall a. Num a => a -> a -> a
- Unsigned n
1
  succMaybe :: Unsigned n -> Maybe (Unsigned n)
succMaybe Unsigned n
n  = if Unsigned n
n Unsigned n -> Unsigned n -> Bool
forall a. Eq a => a -> a -> Bool
== Unsigned n
forall a. Bounded a => a
maxBound then Maybe (Unsigned n)
forall a. Maybe a
Nothing else Unsigned n -> Maybe (Unsigned n)
forall a. a -> Maybe a
Just (Unsigned n -> Maybe (Unsigned n))
-> Unsigned n -> Maybe (Unsigned n)
forall a b. (a -> b) -> a -> b
$ Unsigned n
n Unsigned n -> Unsigned n -> Unsigned n
forall a. Num a => a -> a -> a
+ Unsigned n
1
  ith :: Index (ElementCount (Unsigned n)) -> Unsigned n
ith          = Index (2 ^ n) -> Unsigned n
Index (ElementCount (Unsigned n)) -> Unsigned n
forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce
  index :: Unsigned n -> Index (ElementCount (Unsigned n))
index        = Unsigned n -> Index (2 ^ n)
Unsigned n -> Index (ElementCount (Unsigned n))
forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce

instance Finite Bit where
  type ElementCount Bit = 2
  elements :: Vec (ElementCount Bit) Bit
elements     = Bit
low Bit -> Vec 1 Bit -> Vec (1 + 1) Bit
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
:> Bit
high Bit -> Vec 0 Bit -> Vec (0 + 1) Bit
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
:> Vec 0 Bit
forall b. Vec 0 b
Nil
  lowest :: (1 <= ElementCount Bit) => Bit
lowest       = Bit
low
  lowestMaybe :: Maybe Bit
lowestMaybe  = Bit -> Maybe Bit
forall a. a -> Maybe a
Just Bit
low
  highest :: (1 <= ElementCount Bit) => Bit
highest      = Bit
high
  highestMaybe :: Maybe Bit
highestMaybe = Bit -> Maybe Bit
forall a. a -> Maybe a
Just Bit
high
  predMaybe :: Bit -> Maybe Bit
predMaybe Bit
b  = if Bit
b Bit -> Bit -> Bool
forall a. Eq a => a -> a -> Bool
== Bit
low then Maybe Bit
forall a. Maybe a
Nothing else Bit -> Maybe Bit
forall a. a -> Maybe a
Just Bit
low
  succMaybe :: Bit -> Maybe Bit
succMaybe Bit
b  = if Bit
b Bit -> Bit -> Bool
forall a. Eq a => a -> a -> Bool
== Bit
high then Maybe Bit
forall a. Maybe a
Nothing else Bit -> Maybe Bit
forall a. a -> Maybe a
Just Bit
high
  ith :: Index (ElementCount Bit) -> Bit
ith          = \case { Index (ElementCount Bit)
0 -> Bit
low; Index (ElementCount Bit)
_ -> Bit
high }
  index :: Bit -> Index (ElementCount Bit)
index Bit
b      = if Bit
b Bit -> Bit -> Bool
forall a. Eq a => a -> a -> Bool
== Bit
low then Index 2
Index (ElementCount Bit)
0 else Index 2
Index (ElementCount Bit)
1

instance KnownNat n => Finite (BitVector n) where
  type ElementCount (BitVector n) = 2^n
  elements :: Vec (ElementCount (BitVector n)) (BitVector n)
elements     = (BitVector n -> BitVector n)
-> BitVector n -> Vec (2 ^ n) (BitVector n)
forall (n :: Nat) a. KnownNat n => (a -> a) -> a -> Vec n a
iterateI (BitVector n -> BitVector n -> BitVector n
forall a. Num a => a -> a -> a
+BitVector n
1) BitVector n
0
  lowest :: (1 <= ElementCount (BitVector n)) => BitVector n
lowest       = BitVector n
forall a. Bounded a => a
minBound
  lowestMaybe :: Maybe (BitVector n)
lowestMaybe  = BitVector n -> Maybe (BitVector n)
forall a. a -> Maybe a
Just BitVector n
forall a. Bounded a => a
minBound
  highest :: (1 <= ElementCount (BitVector n)) => BitVector n
highest      = BitVector n
forall a. Bounded a => a
maxBound
  highestMaybe :: Maybe (BitVector n)
highestMaybe = BitVector n -> Maybe (BitVector n)
forall a. a -> Maybe a
Just BitVector n
forall a. Bounded a => a
maxBound
  predMaybe :: BitVector n -> Maybe (BitVector n)
predMaybe BitVector n
bv = if BitVector n
bv BitVector n -> BitVector n -> Bool
forall a. Eq a => a -> a -> Bool
== BitVector n
forall a. Bounded a => a
minBound then Maybe (BitVector n)
forall a. Maybe a
Nothing else BitVector n -> Maybe (BitVector n)
forall a. a -> Maybe a
Just (BitVector n -> Maybe (BitVector n))
-> BitVector n -> Maybe (BitVector n)
forall a b. (a -> b) -> a -> b
$ BitVector n
bv BitVector n -> BitVector n -> BitVector n
forall a. Num a => a -> a -> a
- BitVector n
1
  succMaybe :: BitVector n -> Maybe (BitVector n)
succMaybe BitVector n
bv = if BitVector n
bv BitVector n -> BitVector n -> Bool
forall a. Eq a => a -> a -> Bool
== BitVector n
forall a. Bounded a => a
maxBound then Maybe (BitVector n)
forall a. Maybe a
Nothing else BitVector n -> Maybe (BitVector n)
forall a. a -> Maybe a
Just (BitVector n -> Maybe (BitVector n))
-> BitVector n -> Maybe (BitVector n)
forall a b. (a -> b) -> a -> b
$ BitVector n
bv BitVector n -> BitVector n -> BitVector n
forall a. Num a => a -> a -> a
+ BitVector n
1
  ith :: Index (ElementCount (BitVector n)) -> BitVector n
ith          = Index (2 ^ n) -> BitVector (BitSize (Index (2 ^ n)))
Index (ElementCount (BitVector n)) -> BitVector n
forall a. BitPack a => a -> BitVector (BitSize a)
pack
  index :: BitVector n -> Index (ElementCount (BitVector n))
index        = BitVector n -> Index (ElementCount (BitVector n))
BitVector (BitSize (Index (2 ^ n))) -> Index (2 ^ n)
forall a. BitPack a => BitVector (BitSize a) -> a
unpack

instance (SaturatingNum a, Finite a) => Finite (Erroring a) where
  type ElementCount (Erroring a) = ElementCount a
  elements :: Vec (ElementCount (Erroring a)) (Erroring a)
elements     = a -> Erroring a
forall a. SaturatingNum a => a -> Erroring a
toErroring (a -> Erroring a)
-> Vec (ElementCount a) a -> Vec (ElementCount a) (Erroring a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vec (ElementCount a) a
forall a. Finite a => Vec (ElementCount a) a
elements
  lowest :: (1 <= ElementCount (Erroring a)) => Erroring a
lowest       = a -> Erroring a
forall a. SaturatingNum a => a -> Erroring a
toErroring a
forall a. (Finite a, 1 <= ElementCount a) => a
lowest
  lowestMaybe :: Maybe (Erroring a)
lowestMaybe  = a -> Erroring a
forall a. SaturatingNum a => a -> Erroring a
toErroring (a -> Erroring a) -> Maybe a -> Maybe (Erroring a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe a
forall a. Finite a => Maybe a
lowestMaybe
  highest :: (1 <= ElementCount (Erroring a)) => Erroring a
highest      = a -> Erroring a
forall a. SaturatingNum a => a -> Erroring a
toErroring a
forall a. (Finite a, 1 <= ElementCount a) => a
highest
  highestMaybe :: Maybe (Erroring a)
highestMaybe = a -> Erroring a
forall a. SaturatingNum a => a -> Erroring a
toErroring (a -> Erroring a) -> Maybe a -> Maybe (Erroring a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe a
forall a. Finite a => Maybe a
highestMaybe
  predMaybe :: Erroring a -> Maybe (Erroring a)
predMaybe    = (a -> Erroring a) -> Maybe a -> Maybe (Erroring a)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Erroring a
forall a. SaturatingNum a => a -> Erroring a
toErroring (Maybe a -> Maybe (Erroring a))
-> (Erroring a -> Maybe a) -> Erroring a -> Maybe (Erroring a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. Finite a => a -> Maybe a
predMaybe (a -> Maybe a) -> (Erroring a -> a) -> Erroring a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Erroring a -> a
forall a. Erroring a -> a
fromErroring
  succMaybe :: Erroring a -> Maybe (Erroring a)
succMaybe    = (a -> Erroring a) -> Maybe a -> Maybe (Erroring a)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Erroring a
forall a. SaturatingNum a => a -> Erroring a
toErroring (Maybe a -> Maybe (Erroring a))
-> (Erroring a -> Maybe a) -> Erroring a -> Maybe (Erroring a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. Finite a => a -> Maybe a
succMaybe (a -> Maybe a) -> (Erroring a -> a) -> Erroring a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Erroring a -> a
forall a. Erroring a -> a
fromErroring
  ith :: Index (ElementCount (Erroring a)) -> Erroring a
ith          = a -> Erroring a
forall a. SaturatingNum a => a -> Erroring a
toErroring (a -> Erroring a)
-> (Index (ElementCount a) -> a)
-> Index (ElementCount a)
-> Erroring a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (ElementCount a) -> a
forall a. Finite a => Index (ElementCount a) -> a
ith
  index :: Erroring a -> Index (ElementCount (Erroring a))
index        = a -> Index (ElementCount a)
forall a. Finite a => a -> Index (ElementCount a)
index (a -> Index (ElementCount a))
-> (Erroring a -> a) -> Erroring a -> Index (ElementCount a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Erroring a -> a
forall a. Erroring a -> a
fromErroring

instance Finite a => Finite (Overflowing a) where
  type ElementCount (Overflowing a) = ElementCount a
  elements :: Vec (ElementCount (Overflowing a)) (Overflowing a)
elements     = a -> Overflowing a
forall a. a -> Overflowing a
toOverflowing (a -> Overflowing a)
-> Vec (ElementCount a) a -> Vec (ElementCount a) (Overflowing a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vec (ElementCount a) a
forall a. Finite a => Vec (ElementCount a) a
elements
  lowest :: (1 <= ElementCount (Overflowing a)) => Overflowing a
lowest       = a -> Overflowing a
forall a. a -> Overflowing a
toOverflowing a
forall a. (Finite a, 1 <= ElementCount a) => a
lowest
  lowestMaybe :: Maybe (Overflowing a)
lowestMaybe  = a -> Overflowing a
forall a. a -> Overflowing a
toOverflowing (a -> Overflowing a) -> Maybe a -> Maybe (Overflowing a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe a
forall a. Finite a => Maybe a
lowestMaybe
  highest :: (1 <= ElementCount (Overflowing a)) => Overflowing a
highest      = a -> Overflowing a
forall a. a -> Overflowing a
toOverflowing a
forall a. (Finite a, 1 <= ElementCount a) => a
highest
  highestMaybe :: Maybe (Overflowing a)
highestMaybe = a -> Overflowing a
forall a. a -> Overflowing a
toOverflowing (a -> Overflowing a) -> Maybe a -> Maybe (Overflowing a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe a
forall a. Finite a => Maybe a
highestMaybe
  predMaybe :: Overflowing a -> Maybe (Overflowing a)
predMaybe    = (a -> Overflowing a) -> Maybe a -> Maybe (Overflowing a)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Overflowing a
forall a. a -> Overflowing a
toOverflowing (Maybe a -> Maybe (Overflowing a))
-> (Overflowing a -> Maybe a)
-> Overflowing a
-> Maybe (Overflowing a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. Finite a => a -> Maybe a
predMaybe (a -> Maybe a) -> (Overflowing a -> a) -> Overflowing a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Overflowing a -> a
forall a. Overflowing a -> a
fromOverflowing
  succMaybe :: Overflowing a -> Maybe (Overflowing a)
succMaybe    = (a -> Overflowing a) -> Maybe a -> Maybe (Overflowing a)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Overflowing a
forall a. a -> Overflowing a
toOverflowing (Maybe a -> Maybe (Overflowing a))
-> (Overflowing a -> Maybe a)
-> Overflowing a
-> Maybe (Overflowing a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. Finite a => a -> Maybe a
succMaybe (a -> Maybe a) -> (Overflowing a -> a) -> Overflowing a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Overflowing a -> a
forall a. Overflowing a -> a
fromOverflowing
  ith :: Index (ElementCount (Overflowing a)) -> Overflowing a
ith          = a -> Overflowing a
forall a. a -> Overflowing a
toOverflowing (a -> Overflowing a)
-> (Index (ElementCount a) -> a)
-> Index (ElementCount a)
-> Overflowing a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (ElementCount a) -> a
forall a. Finite a => Index (ElementCount a) -> a
ith
  index :: Overflowing a -> Index (ElementCount (Overflowing a))
index        = a -> Index (ElementCount a)
forall a. Finite a => a -> Index (ElementCount a)
index (a -> Index (ElementCount a))
-> (Overflowing a -> a) -> Overflowing a -> Index (ElementCount a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Overflowing a -> a
forall a. Overflowing a -> a
fromOverflowing

instance (SaturatingNum a, Finite a) => Finite (Saturating a) where
  type ElementCount (Saturating a) = ElementCount a
  elements :: Vec (ElementCount (Saturating a)) (Saturating a)
elements     = a -> Saturating a
forall a. SaturatingNum a => a -> Saturating a
toSaturating (a -> Saturating a)
-> Vec (ElementCount a) a -> Vec (ElementCount a) (Saturating a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vec (ElementCount a) a
forall a. Finite a => Vec (ElementCount a) a
elements
  lowest :: (1 <= ElementCount (Saturating a)) => Saturating a
lowest       = a -> Saturating a
forall a. SaturatingNum a => a -> Saturating a
toSaturating a
forall a. (Finite a, 1 <= ElementCount a) => a
lowest
  lowestMaybe :: Maybe (Saturating a)
lowestMaybe  = a -> Saturating a
forall a. SaturatingNum a => a -> Saturating a
toSaturating (a -> Saturating a) -> Maybe a -> Maybe (Saturating a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe a
forall a. Finite a => Maybe a
lowestMaybe
  highest :: (1 <= ElementCount (Saturating a)) => Saturating a
highest      = a -> Saturating a
forall a. SaturatingNum a => a -> Saturating a
toSaturating a
forall a. (Finite a, 1 <= ElementCount a) => a
highest
  highestMaybe :: Maybe (Saturating a)
highestMaybe = a -> Saturating a
forall a. SaturatingNum a => a -> Saturating a
toSaturating (a -> Saturating a) -> Maybe a -> Maybe (Saturating a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe a
forall a. Finite a => Maybe a
highestMaybe
  predMaybe :: Saturating a -> Maybe (Saturating a)
predMaybe    = (a -> Saturating a) -> Maybe a -> Maybe (Saturating a)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Saturating a
forall a. SaturatingNum a => a -> Saturating a
toSaturating (Maybe a -> Maybe (Saturating a))
-> (Saturating a -> Maybe a)
-> Saturating a
-> Maybe (Saturating a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. Finite a => a -> Maybe a
predMaybe (a -> Maybe a) -> (Saturating a -> a) -> Saturating a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Saturating a -> a
forall a. Saturating a -> a
fromSaturating
  succMaybe :: Saturating a -> Maybe (Saturating a)
succMaybe    = (a -> Saturating a) -> Maybe a -> Maybe (Saturating a)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Saturating a
forall a. SaturatingNum a => a -> Saturating a
toSaturating (Maybe a -> Maybe (Saturating a))
-> (Saturating a -> Maybe a)
-> Saturating a
-> Maybe (Saturating a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. Finite a => a -> Maybe a
succMaybe (a -> Maybe a) -> (Saturating a -> a) -> Saturating a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Saturating a -> a
forall a. Saturating a -> a
fromSaturating
  ith :: Index (ElementCount (Saturating a)) -> Saturating a
ith          = a -> Saturating a
forall a. SaturatingNum a => a -> Saturating a
toSaturating (a -> Saturating a)
-> (Index (ElementCount a) -> a)
-> Index (ElementCount a)
-> Saturating a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (ElementCount a) -> a
forall a. Finite a => Index (ElementCount a) -> a
ith
  index :: Saturating a -> Index (ElementCount (Saturating a))
index        = a -> Index (ElementCount a)
forall a. Finite a => a -> Index (ElementCount a)
index (a -> Index (ElementCount a))
-> (Saturating a -> a) -> Saturating a -> Index (ElementCount a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Saturating a -> a
forall a. Saturating a -> a
fromSaturating

instance (SaturatingNum a, Finite a) => Finite (Wrapping a) where
  type ElementCount (Wrapping a) = ElementCount a
  elements :: Vec (ElementCount (Wrapping a)) (Wrapping a)
elements     = a -> Wrapping a
forall a. SaturatingNum a => a -> Wrapping a
toWrapping (a -> Wrapping a)
-> Vec (ElementCount a) a -> Vec (ElementCount a) (Wrapping a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vec (ElementCount a) a
forall a. Finite a => Vec (ElementCount a) a
elements
  lowest :: (1 <= ElementCount (Wrapping a)) => Wrapping a
lowest       = a -> Wrapping a
forall a. SaturatingNum a => a -> Wrapping a
toWrapping a
forall a. (Finite a, 1 <= ElementCount a) => a
lowest
  lowestMaybe :: Maybe (Wrapping a)
lowestMaybe  = a -> Wrapping a
forall a. SaturatingNum a => a -> Wrapping a
toWrapping (a -> Wrapping a) -> Maybe a -> Maybe (Wrapping a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe a
forall a. Finite a => Maybe a
lowestMaybe
  highest :: (1 <= ElementCount (Wrapping a)) => Wrapping a
highest      = a -> Wrapping a
forall a. SaturatingNum a => a -> Wrapping a
toWrapping a
forall a. (Finite a, 1 <= ElementCount a) => a
highest
  highestMaybe :: Maybe (Wrapping a)
highestMaybe = a -> Wrapping a
forall a. SaturatingNum a => a -> Wrapping a
toWrapping (a -> Wrapping a) -> Maybe a -> Maybe (Wrapping a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe a
forall a. Finite a => Maybe a
highestMaybe
  predMaybe :: Wrapping a -> Maybe (Wrapping a)
predMaybe    = (a -> Wrapping a) -> Maybe a -> Maybe (Wrapping a)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Wrapping a
forall a. SaturatingNum a => a -> Wrapping a
toWrapping (Maybe a -> Maybe (Wrapping a))
-> (Wrapping a -> Maybe a) -> Wrapping a -> Maybe (Wrapping a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. Finite a => a -> Maybe a
predMaybe (a -> Maybe a) -> (Wrapping a -> a) -> Wrapping a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrapping a -> a
forall a. Wrapping a -> a
fromWrapping
  succMaybe :: Wrapping a -> Maybe (Wrapping a)
succMaybe    = (a -> Wrapping a) -> Maybe a -> Maybe (Wrapping a)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Wrapping a
forall a. SaturatingNum a => a -> Wrapping a
toWrapping (Maybe a -> Maybe (Wrapping a))
-> (Wrapping a -> Maybe a) -> Wrapping a -> Maybe (Wrapping a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. Finite a => a -> Maybe a
succMaybe (a -> Maybe a) -> (Wrapping a -> a) -> Wrapping a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrapping a -> a
forall a. Wrapping a -> a
fromWrapping
  ith :: Index (ElementCount (Wrapping a)) -> Wrapping a
ith          = a -> Wrapping a
forall a. SaturatingNum a => a -> Wrapping a
toWrapping (a -> Wrapping a)
-> (Index (ElementCount a) -> a)
-> Index (ElementCount a)
-> Wrapping a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (ElementCount a) -> a
forall a. Finite a => Index (ElementCount a) -> a
ith
  index :: Wrapping a -> Index (ElementCount (Wrapping a))
index        = a -> Index (ElementCount a)
forall a. Finite a => a -> Index (ElementCount a)
index (a -> Index (ElementCount a))
-> (Wrapping a -> a) -> Wrapping a -> Index (ElementCount a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrapping a -> a
forall a. Wrapping a -> a
fromWrapping

instance (SaturatingNum a, Finite a) => Finite (Zeroing a) where
  type ElementCount (Zeroing a) = ElementCount a
  elements :: Vec (ElementCount (Zeroing a)) (Zeroing a)
elements     = a -> Zeroing a
forall a. SaturatingNum a => a -> Zeroing a
toZeroing (a -> Zeroing a)
-> Vec (ElementCount a) a -> Vec (ElementCount a) (Zeroing a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vec (ElementCount a) a
forall a. Finite a => Vec (ElementCount a) a
elements
  lowest :: (1 <= ElementCount (Zeroing a)) => Zeroing a
lowest       = a -> Zeroing a
forall a. SaturatingNum a => a -> Zeroing a
toZeroing a
forall a. (Finite a, 1 <= ElementCount a) => a
lowest
  lowestMaybe :: Maybe (Zeroing a)
lowestMaybe  = a -> Zeroing a
forall a. SaturatingNum a => a -> Zeroing a
toZeroing (a -> Zeroing a) -> Maybe a -> Maybe (Zeroing a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe a
forall a. Finite a => Maybe a
lowestMaybe
  highest :: (1 <= ElementCount (Zeroing a)) => Zeroing a
highest      = a -> Zeroing a
forall a. SaturatingNum a => a -> Zeroing a
toZeroing a
forall a. (Finite a, 1 <= ElementCount a) => a
highest
  highestMaybe :: Maybe (Zeroing a)
highestMaybe = a -> Zeroing a
forall a. SaturatingNum a => a -> Zeroing a
toZeroing (a -> Zeroing a) -> Maybe a -> Maybe (Zeroing a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe a
forall a. Finite a => Maybe a
highestMaybe
  predMaybe :: Zeroing a -> Maybe (Zeroing a)
predMaybe    = (a -> Zeroing a) -> Maybe a -> Maybe (Zeroing a)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Zeroing a
forall a. SaturatingNum a => a -> Zeroing a
toZeroing (Maybe a -> Maybe (Zeroing a))
-> (Zeroing a -> Maybe a) -> Zeroing a -> Maybe (Zeroing a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. Finite a => a -> Maybe a
predMaybe (a -> Maybe a) -> (Zeroing a -> a) -> Zeroing a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Zeroing a -> a
forall a. Zeroing a -> a
fromZeroing
  succMaybe :: Zeroing a -> Maybe (Zeroing a)
succMaybe    = (a -> Zeroing a) -> Maybe a -> Maybe (Zeroing a)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Zeroing a
forall a. SaturatingNum a => a -> Zeroing a
toZeroing (Maybe a -> Maybe (Zeroing a))
-> (Zeroing a -> Maybe a) -> Zeroing a -> Maybe (Zeroing a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. Finite a => a -> Maybe a
succMaybe (a -> Maybe a) -> (Zeroing a -> a) -> Zeroing a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Zeroing a -> a
forall a. Zeroing a -> a
fromZeroing
  ith :: Index (ElementCount (Zeroing a)) -> Zeroing a
ith          = a -> Zeroing a
forall a. SaturatingNum a => a -> Zeroing a
toZeroing (a -> Zeroing a)
-> (Index (ElementCount a) -> a)
-> Index (ElementCount a)
-> Zeroing a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (ElementCount a) -> a
forall a. Finite a => Index (ElementCount a) -> a
ith
  index :: Zeroing a -> Index (ElementCount (Zeroing a))
index        = a -> Index (ElementCount a)
forall a. Finite a => a -> Index (ElementCount a)
index (a -> Index (ElementCount a))
-> (Zeroing a -> a) -> Zeroing a -> Index (ElementCount a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Zeroing a -> a
forall a. Zeroing a -> a
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 :: Vec (ElementCount (Vec n a)) (Vec n a)
elements = Proxy (PowV (ElementCount a) a)
-> (forall (l :: Nat).
    SNat l
    -> ()
    -> (PowV (ElementCount a) a @@ l)
    -> PowV (ElementCount a) a @@ (l + 1))
-> (PowV (ElementCount a) a @@ 0)
-> Vec n ()
-> PowV (ElementCount a) a @@ n
forall (p :: TyFun Nat Type -> Type) (k :: Nat) a.
KnownNat k =>
Proxy p
-> (forall (l :: Nat). SNat l -> a -> (p @@ l) -> p @@ (l + 1))
-> (p @@ 0)
-> Vec k a
-> p @@ k
dfold
    (forall {k} (t :: k). Proxy t
forall (t :: TyFun Nat Type -> Type). Proxy t
Proxy @(PowV (ElementCount a) a))
    (\SNat l
_ ()
_ -> (Vec l a -> Vec (ElementCount a) (Vec (l + 1) a))
-> Vec (ElementCount a ^ l) (Vec l a)
-> Vec ((ElementCount a ^ l) * ElementCount a) (Vec (l + 1) a)
forall a (m :: Nat) b (n :: Nat).
(a -> Vec m b) -> Vec n a -> Vec (n * m) b
concatMap (((a -> Vec (l + 1) a)
-> Vec (ElementCount a) a -> Vec (ElementCount a) (Vec (l + 1) a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vec (ElementCount a) a
forall a. Finite a => Vec (ElementCount a) a
elements) ((a -> Vec (l + 1) a) -> Vec (ElementCount a) (Vec (l + 1) a))
-> (Vec l a -> a -> Vec (l + 1) a)
-> Vec l a
-> Vec (ElementCount a) (Vec (l + 1) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vec l a -> a -> Vec (l + 1) a
forall (n :: Nat) a. Vec n a -> a -> Vec (n + 1) a
(:<)))
    (Vec 0 a
forall b. Vec 0 b
Nil Vec 0 a -> Vec 0 (Vec 0 a) -> Vec (0 + 1) (Vec 0 a)
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
:> Vec 0 (Vec 0 a)
forall b. Vec 0 b
Nil)
    (forall (n :: Nat) a. KnownNat n => a -> Vec n a
repeat @n ())

  lowest :: (1 <= ElementCount (Vec n a)) => Vec n a
lowest = case SNat n -> UNat n
forall (n :: Nat). SNat n -> UNat n
toUNat (forall (n :: Nat). KnownNat n => SNat n
SNat @n) of
    UNat n
UZero -> Vec n a
Vec 0 a
forall b. Vec 0 b
Nil
    UNat n
_ -> case SNat 1 -> SNat (ElementCount a) -> SNatLE 1 (ElementCount a)
forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> SNatLE a b
compareSNat (forall (n :: Nat). KnownNat n => SNat n
SNat @1) (forall (n :: Nat). KnownNat n => SNat n
SNat @(ElementCount a)) of
      SNatLE 1 (ElementCount a)
SNatGT -> case forall (n :: Nat) (m :: Nat). ((n + m) <= m) => Dict (n ~ 0)
zeroLeAdd @(ElementCount a) @1 of
        Dict (ElementCount a ~ 0)
Dict -> case forall (n :: Nat) (m :: Nat). (1 <= (n ^ m)) => Dict (1 <= n)
powPositiveImpliesPositiveBase @(ElementCount a) @n of {}
      SNatLE 1 (ElementCount a)
SNatLE -> a -> Vec n a
forall (n :: Nat) a. KnownNat n => a -> Vec n a
repeat a
forall a. (Finite a, 1 <= ElementCount a) => a
lowest

  lowestMaybe :: Maybe (Vec n a)
lowestMaybe = case SNat n -> UNat n
forall (n :: Nat). SNat n -> UNat n
toUNat (forall (n :: Nat). KnownNat n => SNat n
SNat @n) of
    UNat n
UZero -> Vec n a -> Maybe (Vec n a)
forall a. a -> Maybe a
Just Vec n a
Vec 0 a
forall b. Vec 0 b
Nil
    UNat n
_     -> a -> Vec n a
forall (n :: Nat) a. KnownNat n => a -> Vec n a
repeat (a -> Vec n a) -> Maybe a -> Maybe (Vec n a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe a
forall a. Finite a => Maybe a
lowestMaybe

  highest :: (1 <= ElementCount (Vec n a)) => Vec n a
highest = case SNat n -> UNat n
forall (n :: Nat). SNat n -> UNat n
toUNat (forall (n :: Nat). KnownNat n => SNat n
SNat @n) of
    UNat n
UZero -> Vec n a
Vec 0 a
forall b. Vec 0 b
Nil
    UNat n
_     -> case SNat 1 -> SNat (ElementCount a) -> SNatLE 1 (ElementCount a)
forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> SNatLE a b
compareSNat (forall (n :: Nat). KnownNat n => SNat n
SNat @1) (forall (n :: Nat). KnownNat n => SNat n
SNat @(ElementCount a)) of
      SNatLE 1 (ElementCount a)
SNatGT -> case forall (n :: Nat) (m :: Nat). ((n + m) <= m) => Dict (n ~ 0)
zeroLeAdd @(ElementCount a) @1 of
        Dict (ElementCount a ~ 0)
Dict -> case forall (n :: Nat) (m :: Nat). (1 <= (n ^ m)) => Dict (1 <= n)
powPositiveImpliesPositiveBase @(ElementCount a) @n of {}
      SNatLE 1 (ElementCount a)
SNatLE -> a -> Vec n a
forall (n :: Nat) a. KnownNat n => a -> Vec n a
repeat a
forall a. (Finite a, 1 <= ElementCount a) => a
highest

  highestMaybe :: Maybe (Vec n a)
highestMaybe = case SNat n -> UNat n
forall (n :: Nat). SNat n -> UNat n
toUNat (forall (n :: Nat). KnownNat n => SNat n
SNat @n) of
    UNat n
UZero -> Vec n a -> Maybe (Vec n a)
forall a. a -> Maybe a
Just Vec n a
Vec 0 a
forall b. Vec 0 b
Nil
    UNat n
_     -> a -> Vec n a
forall (n :: Nat) a. KnownNat n => a -> Vec n a
repeat (a -> Vec n a) -> Maybe a -> Maybe (Vec n a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe a
forall a. Finite a => Maybe a
highestMaybe

  predMaybe :: Vec n a -> Maybe (Vec n a)
predMaybe Vec n a
v = do
    a
h <- Maybe a
forall a. Finite a => Maybe a
highestMaybe
    (Vec n a -> Maybe (Vec n a))
-> (Vec n a -> Maybe (Vec n a))
-> Either (Vec n a) (Vec n a)
-> Maybe (Vec n a)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Vec n a -> Maybe (Vec n a)
forall a. a -> Maybe a
Just (Maybe (Vec n a) -> Vec n a -> Maybe (Vec n a)
forall a b. a -> b -> a
const Maybe (Vec n a)
forall a. Maybe a
Nothing)
      (Either (Vec n a) (Vec n a) -> Maybe (Vec n a))
-> Either (Vec n a) (Vec n a) -> Maybe (Vec n a)
forall a b. (a -> b) -> a -> b
$ (Index n
 -> a -> Either (Vec n a) (Vec n a) -> Either (Vec n a) (Vec n a))
-> Either (Vec n a) (Vec n a)
-> Vec n a
-> Either (Vec n a) (Vec n a)
forall (n :: Nat) a b.
KnownNat n =>
(Index n -> a -> b -> b) -> b -> Vec n a -> b
ifoldr
          (\Index n
i a
x Either (Vec n a) (Vec n a)
a -> case a -> Maybe a
forall a. Finite a => a -> Maybe a
predMaybe a
x of
              Maybe a
Nothing -> Index n -> a -> Vec n a -> Vec n a
forall (n :: Nat) i a.
(KnownNat n, Enum i) =>
i -> a -> Vec n a -> Vec n a
replace Index n
i a
h (Vec n a -> Vec n a)
-> Either (Vec n a) (Vec n a) -> Either (Vec n a) (Vec n a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Either (Vec n a) (Vec n a)
a
              Just a
y  -> Either (Vec n a) (Vec n a)
a Either (Vec n a) (Vec n a)
-> (Vec n a -> Either (Vec n a) (Vec n a))
-> Either (Vec n a) (Vec n a)
forall a b.
Either (Vec n a) a
-> (a -> Either (Vec n a) b) -> Either (Vec n a) b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= Vec n a -> Either (Vec n a) (Vec n a)
forall a b. a -> Either a b
Left (Vec n a -> Either (Vec n a) (Vec n a))
-> (Vec n a -> Vec n a) -> Vec n a -> Either (Vec n a) (Vec n a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index n -> a -> Vec n a -> Vec n a
forall (n :: Nat) i a.
(KnownNat n, Enum i) =>
i -> a -> Vec n a -> Vec n a
replace Index n
i a
y
          ) (Vec n a -> Either (Vec n a) (Vec n a)
forall a b. b -> Either a b
Right Vec n a
v) Vec n a
v

  succMaybe :: Vec n a -> Maybe (Vec n a)
succMaybe Vec n a
v = do
    a
l <- Maybe a
forall a. Finite a => Maybe a
lowestMaybe
    (Vec n a -> Maybe (Vec n a))
-> (Vec n a -> Maybe (Vec n a))
-> Either (Vec n a) (Vec n a)
-> Maybe (Vec n a)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Vec n a -> Maybe (Vec n a)
forall a. a -> Maybe a
Just (Maybe (Vec n a) -> Vec n a -> Maybe (Vec n a)
forall a b. a -> b -> a
const Maybe (Vec n a)
forall a. Maybe a
Nothing)
      (Either (Vec n a) (Vec n a) -> Maybe (Vec n a))
-> Either (Vec n a) (Vec n a) -> Maybe (Vec n a)
forall a b. (a -> b) -> a -> b
$ (Index n
 -> a -> Either (Vec n a) (Vec n a) -> Either (Vec n a) (Vec n a))
-> Either (Vec n a) (Vec n a)
-> Vec n a
-> Either (Vec n a) (Vec n a)
forall (n :: Nat) a b.
KnownNat n =>
(Index n -> a -> b -> b) -> b -> Vec n a -> b
ifoldr
          (\Index n
i a
x Either (Vec n a) (Vec n a)
a -> case a -> Maybe a
forall a. Finite a => a -> Maybe a
succMaybe a
x of
              Maybe a
Nothing -> Index n -> a -> Vec n a -> Vec n a
forall (n :: Nat) i a.
(KnownNat n, Enum i) =>
i -> a -> Vec n a -> Vec n a
replace Index n
i a
l (Vec n a -> Vec n a)
-> Either (Vec n a) (Vec n a) -> Either (Vec n a) (Vec n a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Either (Vec n a) (Vec n a)
a
              Just a
y  -> Either (Vec n a) (Vec n a)
a Either (Vec n a) (Vec n a)
-> (Vec n a -> Either (Vec n a) (Vec n a))
-> Either (Vec n a) (Vec n a)
forall a b.
Either (Vec n a) a
-> (a -> Either (Vec n a) b) -> Either (Vec n a) b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= Vec n a -> Either (Vec n a) (Vec n a)
forall a b. a -> Either a b
Left (Vec n a -> Either (Vec n a) (Vec n a))
-> (Vec n a -> Vec n a) -> Vec n a -> Either (Vec n a) (Vec n a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index n -> a -> Vec n a -> Vec n a
forall (n :: Nat) i a.
(KnownNat n, Enum i) =>
i -> a -> Vec n a -> Vec n a
replace Index n
i a
y
          ) (Vec n a -> Either (Vec n a) (Vec n a)
forall a b. b -> Either a b
Right Vec n a
v) Vec n a
v

  ith :: Index (ElementCount (Vec n a)) -> Vec n a
ith = case SNat n -> UNat n
forall (n :: Nat). SNat n -> UNat n
toUNat (forall (n :: Nat). KnownNat n => SNat n
SNat @n) of
    UNat n
UZero -> Vec n a -> Index 1 -> Vec n a
forall a b. a -> b -> a
const Vec n a
Vec 0 a
forall b. Vec 0 b
Nil
    USucc UNat n
UZero -> (a -> Vec 0 a -> Vec (0 + 1) a
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
:> Vec 0 a
forall b. Vec 0 b
Nil) (a -> Vec n a)
-> (Index (ElementCount a) -> a)
-> Index (ElementCount a)
-> Vec n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (ElementCount a) -> a
forall a. Finite a => Index (ElementCount a) -> a
ith
    UNat n
_ -> (Vec n a -> Vec n a
forall (n :: Nat) a. Vec n a -> Vec n a
reverse (Vec n a -> Vec n a)
-> (Index (ElementCount (Vec n a)) -> Vec n a)
-> Index (ElementCount (Vec n a))
-> Vec n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((Index (ElementCount a ^ n) -> Vec n a)
 -> Index (ElementCount (Vec n a)) -> Vec n a)
-> ((Index (ElementCount a ^ n) -> (a, Index (ElementCount a ^ n)))
    -> Index (ElementCount a ^ n) -> Vec n a)
-> (Index (ElementCount a ^ n) -> (a, Index (ElementCount a ^ n)))
-> Index (ElementCount (Vec n a))
-> Vec n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Index (ElementCount a ^ n) -> (a, Index (ElementCount a ^ n)))
-> Index (ElementCount a ^ n) -> Vec n a
forall (n :: Nat) s a. KnownNat n => (s -> (a, s)) -> s -> Vec n a
unfoldrI
      ((Index (ElementCount a ^ n) -> (a, Index (ElementCount a ^ n)))
 -> Index (ElementCount (Vec n a)) -> Vec n a)
-> (Index (ElementCount a ^ n) -> (a, Index (ElementCount a ^ n)))
-> Index (ElementCount (Vec n a))
-> Vec n a
forall a b. (a -> b) -> a -> b
$ \Index (ElementCount a ^ n)
i -> ( Index (ElementCount a) -> a
forall a. Finite a => Index (ElementCount a) -> a
ith (Index (ElementCount a) -> a) -> Index (ElementCount a) -> a
forall a b. (a -> b) -> a -> b
$ Index (ElementCount a ^ n) -> Index (ElementCount a)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b) =>
Index a -> Index b
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f b
resize (Index (ElementCount a ^ n) -> Index (ElementCount a))
-> Index (ElementCount a ^ n) -> Index (ElementCount a)
forall a b. (a -> b) -> a -> b
$ Index (ElementCount a ^ n)
i Index (ElementCount a ^ n)
-> Index (ElementCount a ^ n) -> Index (ElementCount a ^ n)
forall a. Integral a => a -> a -> a
`mod` forall (n :: Nat) a. (Num a, KnownNat n) => a
natToNum @(ElementCount a)
              , Index (ElementCount a ^ n)
i Index (ElementCount a ^ n)
-> Index (ElementCount a ^ n) -> Index (ElementCount a ^ n)
forall a. Integral a => a -> a -> a
`div` forall (n :: Nat) a. (Num a, KnownNat n) => a
natToNum @(ElementCount a)
              )

  index :: Vec n a -> Index (ElementCount (Vec n a))
index = ((Index (ElementCount a ^ n), Index (ElementCount a ^ n))
-> Index (ElementCount a ^ n)
(Index (ElementCount a ^ n), Index (ElementCount a ^ n))
-> Index (ElementCount (Vec n a))
forall a b. (a, b) -> a
fst ((Index (ElementCount a ^ n), Index (ElementCount a ^ n))
 -> Index (ElementCount (Vec n a)))
-> (Vec n a
    -> (Index (ElementCount a ^ n), Index (ElementCount a ^ n)))
-> Vec n a
-> Index (ElementCount (Vec n a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((Vec n a
  -> (Index (ElementCount a ^ n), Index (ElementCount a ^ n)))
 -> Vec n a -> Index (ElementCount (Vec n a)))
-> ((a
     -> (Index (ElementCount a ^ n), Index (ElementCount a ^ n))
     -> (Index (ElementCount a ^ n), Index (ElementCount a ^ n)))
    -> Vec n a
    -> (Index (ElementCount a ^ n), Index (ElementCount a ^ n)))
-> (a
    -> (Index (ElementCount a ^ n), Index (ElementCount a ^ n))
    -> (Index (ElementCount a ^ n), Index (ElementCount a ^ n)))
-> Vec n a
-> Index (ElementCount (Vec n a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a
 -> (Index (ElementCount a ^ n), Index (ElementCount a ^ n))
 -> (Index (ElementCount a ^ n), Index (ElementCount a ^ n)))
-> (Index (ElementCount a ^ n), Index (ElementCount a ^ n))
-> Vec n a
-> (Index (ElementCount a ^ n), Index (ElementCount a ^ n))
forall a b (n :: Nat). (a -> b -> b) -> b -> Vec n a -> b
`foldr` (Index (ElementCount a ^ n)
0, Index (ElementCount a ^ n)
1))
    ((a
  -> (Index (ElementCount a ^ n), Index (ElementCount a ^ n))
  -> (Index (ElementCount a ^ n), Index (ElementCount a ^ n)))
 -> Vec n a -> Index (ElementCount (Vec n a)))
-> (a
    -> (Index (ElementCount a ^ n), Index (ElementCount a ^ n))
    -> (Index (ElementCount a ^ n), Index (ElementCount a ^ n)))
-> Vec n a
-> Index (ElementCount (Vec n a))
forall a b. (a -> b) -> a -> b
$ \a
a (Index (ElementCount a ^ n)
n, Index (ElementCount a ^ n)
p) ->
        ( Index (ElementCount a ^ n)
p Index (ElementCount a ^ n)
-> Index (ElementCount a ^ n) -> Index (ElementCount a ^ n)
forall a. Num a => a -> a -> a
* Index (ElementCount a) -> Index (ElementCount a ^ n)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b) =>
Index a -> Index b
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f b
resize (a -> Index (ElementCount a)
forall a. Finite a => a -> Index (ElementCount a)
index a
a) Index (ElementCount a ^ n)
-> Index (ElementCount a ^ n) -> Index (ElementCount a ^ n)
forall a. Num a => a -> a -> a
+ Index (ElementCount a ^ n)
n
        , forall (n :: Nat) a. (Num a, KnownNat n) => a
natToNum @(ElementCount a) Index (ElementCount a ^ n)
-> Index (ElementCount a ^ n) -> Index (ElementCount a ^ n)
forall a. Num a => a -> a -> a
* Index (ElementCount a ^ n)
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 :: Vec (ElementCount (RTree d a)) (RTree d a)
elements = Proxy (PowT (ElementCount a) a)
-> (() -> PowT (ElementCount a) a @@ 0)
-> (forall (l :: Nat).
    SNat l
    -> (PowT (ElementCount a) a @@ l)
    -> (PowT (ElementCount a) a @@ l)
    -> PowT (ElementCount a) a @@ (l + 1))
-> RTree d ()
-> PowT (ElementCount a) a @@ d
forall (p :: TyFun Nat Type -> Type) (k :: Nat) a.
KnownNat k =>
Proxy p
-> (a -> p @@ 0)
-> (forall (l :: Nat).
    SNat l -> (p @@ l) -> (p @@ l) -> p @@ (l + 1))
-> RTree k a
-> p @@ k
tdfold
    (forall {k} (t :: k). Proxy t
forall (t :: TyFun Nat Type -> Type). Proxy t
Proxy @(PowT (ElementCount a) a))
    ((PowT (ElementCount a) a @@ 0)
-> () -> PowT (ElementCount a) a @@ 0
forall a b. a -> b -> a
const ((PowT (ElementCount a) a @@ 0)
 -> () -> PowT (ElementCount a) a @@ 0)
-> (PowT (ElementCount a) a @@ 0)
-> ()
-> PowT (ElementCount a) a @@ 0
forall a b. (a -> b) -> a -> b
$ a -> RTree 0 a
forall b. b -> RTree 0 b
RLeaf (a -> RTree 0 a)
-> Vec (ElementCount a) a -> Vec (ElementCount a) (RTree 0 a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. Finite a => Vec (ElementCount a) a
elements @a))
    (\(SNat l
_ :: SNat m) PowT (ElementCount a) a @@ l
l PowT (ElementCount a) a @@ l
r -> case forall (a :: Nat) (n :: Nat).
Dict ((a ^ (2 ^ (n + 1))) ~ ((a ^ (2 ^ n)) * (a ^ (2 ^ n))))
powLawsRewrite @(ElementCount a) @m of
       Dict
  ((ElementCount a ^ (2 ^ (l + 1)))
   ~ ((ElementCount a ^ (2 ^ l)) * (ElementCount a ^ (2 ^ l))))
Dict -> (RTree l a -> Vec (ElementCount a ^ (2 ^ l)) (RTree (l + 1) a))
-> Vec (ElementCount a ^ (2 ^ l)) (RTree l a)
-> Vec
     ((ElementCount a ^ (2 ^ l)) * (ElementCount a ^ (2 ^ l)))
     (RTree (l + 1) a)
forall a (m :: Nat) b (n :: Nat).
(a -> Vec m b) -> Vec n a -> Vec (n * m) b
concatMap (((RTree l a -> RTree (l + 1) a)
-> Vec (ElementCount a ^ (2 ^ l)) (RTree l a)
-> Vec (ElementCount a ^ (2 ^ l)) (RTree (l + 1) a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vec (ElementCount a ^ (2 ^ l)) (RTree l a)
PowT (ElementCount a) a @@ l
r) ((RTree l a -> RTree (l + 1) a)
 -> Vec (ElementCount a ^ (2 ^ l)) (RTree (l + 1) a))
-> (RTree l a -> RTree l a -> RTree (l + 1) a)
-> RTree l a
-> Vec (ElementCount a ^ (2 ^ l)) (RTree (l + 1) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTree l a -> RTree l a -> RTree (l + 1) a
forall (d :: Nat) b. RTree d b -> RTree d b -> RTree (d + 1) b
RBranch) Vec (ElementCount a ^ (2 ^ l)) (RTree l a)
PowT (ElementCount a) a @@ l
l
    )
    (forall (d :: Nat) a. KnownNat d => a -> RTree d a
trepeat @d ())

  lowest :: (1 <= ElementCount (RTree d a)) => RTree d a
lowest = case SNat 1 -> SNat (ElementCount a) -> SNatLE 1 (ElementCount a)
forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> SNatLE a b
compareSNat (forall (n :: Nat). KnownNat n => SNat n
SNat @1) (forall (n :: Nat). KnownNat n => SNat n
SNat @(ElementCount a)) of
    SNatLE 1 (ElementCount a)
SNatLE -> a -> RTree d a
forall (d :: Nat) a. KnownNat d => a -> RTree d a
trepeat a
forall a. (Finite a, 1 <= ElementCount a) => a
lowest
    SNatLE 1 (ElementCount a)
SNatGT -> case forall (n :: Nat) (m :: Nat). ((n + m) <= m) => Dict (n ~ 0)
zeroLeAdd @(ElementCount a) @1 of
      Dict (ElementCount a ~ 0)
Dict -> case forall (n :: Nat) (m :: Nat). (1 <= (n ^ m)) => Dict (1 <= n)
powPositiveImpliesPositiveBase @(ElementCount a) @(2^d) of {}

  lowestMaybe :: Maybe (RTree d a)
lowestMaybe = a -> RTree d a
forall (d :: Nat) a. KnownNat d => a -> RTree d a
trepeat (a -> RTree d a) -> Maybe a -> Maybe (RTree d a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe a
forall a. Finite a => Maybe a
lowestMaybe

  highest :: (1 <= ElementCount (RTree d a)) => RTree d a
highest = case SNat 1 -> SNat (ElementCount a) -> SNatLE 1 (ElementCount a)
forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> SNatLE a b
compareSNat (forall (n :: Nat). KnownNat n => SNat n
SNat @1) (forall (n :: Nat). KnownNat n => SNat n
SNat @(ElementCount a)) of
    SNatLE 1 (ElementCount a)
SNatLE -> a -> RTree d a
forall (d :: Nat) a. KnownNat d => a -> RTree d a
trepeat a
forall a. (Finite a, 1 <= ElementCount a) => a
highest
    SNatLE 1 (ElementCount a)
SNatGT -> case forall (n :: Nat) (m :: Nat). ((n + m) <= m) => Dict (n ~ 0)
zeroLeAdd @(ElementCount a) @1 of
      Dict (ElementCount a ~ 0)
Dict -> case forall (n :: Nat) (m :: Nat). (1 <= (n ^ m)) => Dict (1 <= n)
powPositiveImpliesPositiveBase @(ElementCount a) @(2^d) of {}

  highestMaybe :: Maybe (RTree d a)
highestMaybe = a -> RTree d a
forall (d :: Nat) a. KnownNat d => a -> RTree d a
trepeat (a -> RTree d a) -> Maybe a -> Maybe (RTree d a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe a
forall a. Finite a => Maybe a
highestMaybe

  predMaybe :: RTree d a -> Maybe (RTree d a)
predMaybe RTree d a
t = Maybe a
forall a. Finite a => Maybe a
highestMaybe Maybe a -> (a -> Maybe (RTree d a)) -> Maybe (RTree d a)
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= RTree d a -> (a -> Maybe a) -> a -> Maybe (RTree d a)
forall (n :: Nat) a.
KnownNat n =>
RTree n a -> (a -> Maybe a) -> a -> Maybe (RTree n a)
predSuccMaybeT# RTree d a
t a -> Maybe a
forall a. Finite a => a -> Maybe a
predMaybe
  succMaybe :: RTree d a -> Maybe (RTree d a)
succMaybe RTree d a
t = Maybe a
forall a. Finite a => Maybe a
lowestMaybe  Maybe a -> (a -> Maybe (RTree d a)) -> Maybe (RTree d a)
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= RTree d a -> (a -> Maybe a) -> a -> Maybe (RTree d a)
forall (n :: Nat) a.
KnownNat n =>
RTree n a -> (a -> Maybe a) -> a -> Maybe (RTree n a)
predSuccMaybeT# RTree d a
t a -> Maybe a
forall a. Finite a => a -> Maybe a
succMaybe

  ith :: Index (ElementCount (RTree d a)) -> RTree d a
ith = case SNat d -> UNat d
forall (n :: Nat). SNat n -> UNat n
toUNat (forall (n :: Nat). KnownNat n => SNat n
SNat @d) of
    UNat d
UZero -> a -> RTree d a
a -> RTree 0 a
forall b. b -> RTree 0 b
RLeaf (a -> RTree d a)
-> (Index (ElementCount a) -> a)
-> Index (ElementCount a)
-> RTree d a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (ElementCount a) -> a
forall a. Finite a => Index (ElementCount a) -> a
ith
    USucc (UNat n
_ :: UNat p) -> \Index (ElementCount (RTree d a))
i -> RTree n a -> RTree n a -> RTree (n + 1) a
forall (d :: Nat) b. RTree d b -> RTree d b -> RTree (d + 1) b
RBranch
      (forall a. Finite a => Index (ElementCount a) -> a
ith @(RTree p a) (Index (ElementCount (RTree n a)) -> RTree n a)
-> Index (ElementCount (RTree n a)) -> RTree n a
forall a b. (a -> b) -> a -> b
$ Index (ElementCount a ^ (2 ^ d))
-> Index (ElementCount (RTree n a))
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b) =>
Index a -> Index b
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f b
resize (Index (ElementCount a ^ (2 ^ d))
 -> Index (ElementCount (RTree n a)))
-> Index (ElementCount a ^ (2 ^ d))
-> Index (ElementCount (RTree n a))
forall a b. (a -> b) -> a -> b
$ Index (ElementCount a ^ (2 ^ d))
Index (ElementCount (RTree d a))
i Index (ElementCount a ^ (2 ^ d))
-> Index (ElementCount a ^ (2 ^ d))
-> Index (ElementCount a ^ (2 ^ d))
forall a. Integral a => a -> a -> a
`div` Index (ElementCount a ^ (2 ^ d))
m)
      (forall a. Finite a => Index (ElementCount a) -> a
ith @(RTree p a) (Index (ElementCount (RTree n a)) -> RTree n a)
-> Index (ElementCount (RTree n a)) -> RTree n a
forall a b. (a -> b) -> a -> b
$ Index (ElementCount a ^ (2 ^ d))
-> Index (ElementCount (RTree n a))
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b) =>
Index a -> Index b
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f b
resize (Index (ElementCount a ^ (2 ^ d))
 -> Index (ElementCount (RTree n a)))
-> Index (ElementCount a ^ (2 ^ d))
-> Index (ElementCount (RTree n a))
forall a b. (a -> b) -> a -> b
$ Index (ElementCount a ^ (2 ^ d))
Index (ElementCount (RTree d a))
i Index (ElementCount a ^ (2 ^ d))
-> Index (ElementCount a ^ (2 ^ d))
-> Index (ElementCount a ^ (2 ^ d))
forall a. Integral a => a -> a -> a
`mod` Index (ElementCount a ^ (2 ^ d))
m)
     where
      m :: Index (ElementCount a ^ (2 ^ d))
m = forall (n :: Nat) a. (Num a, KnownNat n) => a
natToNum @(ElementCount a^(2^p))

  index :: RTree d a -> Index (ElementCount (RTree d a))
index =
    (Index (ElementCount a ^ (2 ^ d)),
 Index (ElementCount a ^ (2 ^ d)))
-> Index (ElementCount a ^ (2 ^ d))
forall a b. (a, b) -> a
fst ((Index (ElementCount a ^ (2 ^ d)),
  Index (ElementCount a ^ (2 ^ d)))
 -> Index (ElementCount a ^ (2 ^ d)))
-> (RTree d a
    -> (Index (ElementCount a ^ (2 ^ d)),
        Index (ElementCount a ^ (2 ^ d))))
-> RTree d a
-> Index (ElementCount a ^ (2 ^ d))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a
 -> (Index (ElementCount a ^ (2 ^ d)),
     Index (ElementCount a ^ (2 ^ d))))
-> ((Index (ElementCount a ^ (2 ^ d)),
     Index (ElementCount a ^ (2 ^ d)))
    -> (Index (ElementCount a ^ (2 ^ d)),
        Index (ElementCount a ^ (2 ^ d)))
    -> (Index (ElementCount a ^ (2 ^ d)),
        Index (ElementCount a ^ (2 ^ d))))
-> RTree d a
-> (Index (ElementCount a ^ (2 ^ d)),
    Index (ElementCount a ^ (2 ^ d)))
forall (d :: Nat) a b.
KnownNat d =>
(a -> b) -> (b -> b -> b) -> RTree d a -> b
tfold
      ((, forall (n :: Nat) a. (Num a, KnownNat n) => a
natToNum @(ElementCount a)) (Index (ElementCount a ^ (2 ^ d))
 -> (Index (ElementCount a ^ (2 ^ d)),
     Index (ElementCount a ^ (2 ^ d))))
-> (a -> Index (ElementCount a ^ (2 ^ d)))
-> a
-> (Index (ElementCount a ^ (2 ^ d)),
    Index (ElementCount a ^ (2 ^ d)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (ElementCount a) -> Index (ElementCount a ^ (2 ^ d))
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b) =>
Index a -> Index b
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f b
resize (Index (ElementCount a) -> Index (ElementCount a ^ (2 ^ d)))
-> (a -> Index (ElementCount a))
-> a
-> Index (ElementCount a ^ (2 ^ d))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Index (ElementCount a)
forall a. Finite a => a -> Index (ElementCount a)
index)
      (\(Index (ElementCount a ^ (2 ^ d))
nL, Index (ElementCount a ^ (2 ^ d))
pL) (Index (ElementCount a ^ (2 ^ d))
nR, Index (ElementCount a ^ (2 ^ d))
pR) -> (Index (ElementCount a ^ (2 ^ d))
nR Index (ElementCount a ^ (2 ^ d))
-> Index (ElementCount a ^ (2 ^ d))
-> Index (ElementCount a ^ (2 ^ d))
forall a. Num a => a -> a -> a
+ Index (ElementCount a ^ (2 ^ d))
pR Index (ElementCount a ^ (2 ^ d))
-> Index (ElementCount a ^ (2 ^ d))
-> Index (ElementCount a ^ (2 ^ d))
forall a. Num a => a -> a -> a
* Index (ElementCount a ^ (2 ^ d))
nL, Index (ElementCount a ^ (2 ^ d))
pL Index (ElementCount a ^ (2 ^ d))
-> Index (ElementCount a ^ (2 ^ d))
-> Index (ElementCount a ^ (2 ^ d))
forall a. Num a => a -> a -> a
* Index (ElementCount a ^ (2 ^ d))
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# :: forall (n :: Nat) a.
KnownNat n =>
RTree n a -> (a -> Maybe a) -> a -> Maybe (RTree n a)
predSuccMaybeT# RTree n a
t a -> Maybe a
op a
o
  | Bool
hasSuccMaybe = RTree n a -> Maybe (RTree n a)
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return RTree n a
t'
  | Bool
otherwise = Maybe (RTree n a)
forall a. Maybe a
Nothing
 where
  (Bool
hasSuccMaybe, RTree n a
t') = (RTree n a, (Bool, RTree n a)) -> (Bool, RTree n a)
forall a b. (a, b) -> b
snd ((RTree n a, (Bool, RTree n a)) -> (Bool, RTree n a))
-> (RTree n a, (Bool, RTree n a)) -> (Bool, RTree n a)
forall a b. (a -> b) -> a -> b
$ Proxy (IterT a)
-> (a -> IterT a @@ 0)
-> (forall (l :: Nat).
    SNat l -> (IterT a @@ l) -> (IterT a @@ l) -> IterT a @@ (l + 1))
-> RTree n a
-> IterT a @@ n
forall (p :: TyFun Nat Type -> Type) (k :: Nat) a.
KnownNat k =>
Proxy p
-> (a -> p @@ 0)
-> (forall (l :: Nat).
    SNat l -> (p @@ l) -> (p @@ l) -> p @@ (l + 1))
-> RTree k a
-> p @@ k
tdfold (forall {k} (t :: k). Proxy t
forall (t :: TyFun Nat Type -> Type). Proxy t
Proxy @(IterT a)) a -> (RTree 0 a, (Bool, RTree 0 a))
a -> IterT a @@ 0
fLeaf SNat l
-> (RTree l a, (Bool, RTree l a))
-> (RTree l a, (Bool, RTree l a))
-> (RTree (l + 1) a, (Bool, RTree (l + 1) a))
SNat l
-> Apply (IterT a) l
-> Apply (IterT a) l
-> Apply (IterT a) (l + 1)
forall (l :: Nat).
SNat l -> (IterT a @@ l) -> (IterT a @@ l) -> IterT a @@ (l + 1)
forall {p} {d :: Nat} {b}.
p
-> (RTree d b, (Bool, RTree d b))
-> (RTree d b, (Bool, RTree d b))
-> (RTree (d + 1) b, (Bool, RTree (d + 1) b))
fBranch RTree n a
t

  fLeaf :: a -> (RTree 0 a, (Bool, RTree 0 a))
fLeaf a
x = (a -> RTree 0 a
forall b. b -> RTree 0 b
RLeaf a
x, ) ((Bool, RTree 0 a) -> (RTree 0 a, (Bool, RTree 0 a)))
-> (Bool, RTree 0 a) -> (RTree 0 a, (Bool, RTree 0 a))
forall a b. (a -> b) -> a -> b
$ case a -> Maybe a
op a
x of
    Maybe a
Nothing -> (Bool
False, a -> RTree 0 a
forall b. b -> RTree 0 b
RLeaf a
o)
    Just a
y  -> (Bool
True,  a -> RTree 0 a
forall b. b -> RTree 0 b
RLeaf a
y)

  fBranch :: p
-> (RTree d b, (Bool, RTree d b))
-> (RTree d b, (Bool, RTree d b))
-> (RTree (d + 1) b, (Bool, RTree (d + 1) b))
fBranch p
_ (RTree d b
lO, (Bool
lF, RTree d b
lM)) (RTree d b
rO, (Bool
rF, RTree d b
rM)) =
    (RTree d b -> RTree d b -> RTree (d + 1) b
forall (d :: Nat) b. RTree d b -> RTree d b -> RTree (d + 1) b
RBranch RTree d b
lO RTree d b
rO, )
      ((Bool, RTree (d + 1) b)
 -> (RTree (d + 1) b, (Bool, RTree (d + 1) b)))
-> (Bool, RTree (d + 1) b)
-> (RTree (d + 1) b, (Bool, RTree (d + 1) b))
forall a b. (a -> b) -> a -> b
$ if Bool
rF then (Bool
rF, RTree d b -> RTree d b -> RTree (d + 1) b
forall (d :: Nat) b. RTree d b -> RTree d b -> RTree (d + 1) b
RBranch RTree d b
lO RTree d b
rM)
              else (Bool
lF, RTree d b -> RTree d b -> RTree (d + 1) b
forall (d :: Nat) b. RTree d b -> RTree d b -> RTree (d + 1) b
RBranch RTree d b
lM RTree d b
rM)

instance (Finite a, Finite b) => Finite (a -> b) where
  type ElementCount (a -> b) = ElementCount b^ElementCount a
  elements :: Vec (ElementCount (a -> b)) (a -> b)
elements = (Vec (ElementCount a) b -> a -> b)
-> Vec
     (ElementCount (Vec (ElementCount a) b)) (Vec (ElementCount a) b)
-> Vec (ElementCount (Vec (ElementCount a) b)) (a -> b)
forall a b.
(a -> b)
-> Vec (ElementCount (Vec (ElementCount a) b)) a
-> Vec (ElementCount (Vec (ElementCount a) b)) b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (((Index (ElementCount a) -> b)
-> (a -> Index (ElementCount a)) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Index (ElementCount a)
forall a. Finite a => a -> Index (ElementCount a)
index) ((Index (ElementCount a) -> b) -> a -> b)
-> (Vec (ElementCount a) b -> Index (ElementCount a) -> b)
-> Vec (ElementCount a) b
-> a
-> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vec (ElementCount a) b -> Index (ElementCount a) -> b
forall (n :: Nat) i a. (KnownNat n, Enum i) => Vec n a -> i -> a
(!!)) (Vec
   (ElementCount (Vec (ElementCount a) b)) (Vec (ElementCount a) b)
 -> Vec (ElementCount (Vec (ElementCount a) b)) (a -> b))
-> Vec
     (ElementCount (Vec (ElementCount a) b)) (Vec (ElementCount a) b)
-> Vec (ElementCount (Vec (ElementCount a) b)) (a -> b)
forall a b. (a -> b) -> a -> b
$ forall a. Finite a => Vec (ElementCount a) a
elements @(Vec (ElementCount a) b)

  lowest :: (1 <= ElementCount (a -> b)) => a -> b
lowest = case SNat 1 -> SNat (ElementCount b) -> SNatLE 1 (ElementCount b)
forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> SNatLE a b
compareSNat (forall (n :: Nat). KnownNat n => SNat n
SNat @1) (forall (n :: Nat). KnownNat n => SNat n
SNat @(ElementCount b)) of
    SNatLE 1 (ElementCount b)
SNatLE -> b -> a -> b
forall a b. a -> b -> a
const b
forall a. (Finite a, 1 <= ElementCount a) => a
lowest
    SNatLE 1 (ElementCount b)
SNatGT -> case forall (n :: Nat) (m :: Nat). ((n + m) <= m) => Dict (n ~ 0)
zeroLeAdd @(ElementCount b) @1 of
      Dict (ElementCount b ~ 0)
Dict -> case forall (n :: Nat) (m :: Nat). (1 <= (n ^ m)) => Dict (1 <= n)
powPositiveImpliesPositiveBase
                     @(ElementCount b) @(ElementCount a) of {}

  lowestMaybe :: Maybe (a -> b)
lowestMaybe  = b -> a -> b
forall a b. a -> b -> a
const (b -> a -> b) -> Maybe b -> Maybe (a -> b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe b
forall a. Finite a => Maybe a
lowestMaybe

  highest :: (1 <= ElementCount (a -> b)) => a -> b
highest = case SNat 1 -> SNat (ElementCount b) -> SNatLE 1 (ElementCount b)
forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> SNatLE a b
compareSNat (forall (n :: Nat). KnownNat n => SNat n
SNat @1) (forall (n :: Nat). KnownNat n => SNat n
SNat @(ElementCount b)) of
    SNatLE 1 (ElementCount b)
SNatLE -> b -> a -> b
forall a b. a -> b -> a
const b
forall a. (Finite a, 1 <= ElementCount a) => a
highest
    SNatLE 1 (ElementCount b)
SNatGT -> case forall (n :: Nat) (m :: Nat). ((n + m) <= m) => Dict (n ~ 0)
zeroLeAdd @(ElementCount b) @1 of
      Dict (ElementCount b ~ 0)
Dict -> case forall (n :: Nat) (m :: Nat). (1 <= (n ^ m)) => Dict (1 <= n)
powPositiveImpliesPositiveBase
                     @(ElementCount b) @(ElementCount a) of {}

  highestMaybe :: Maybe (a -> b)
highestMaybe = b -> a -> b
forall a b. a -> b -> a
const (b -> a -> b) -> Maybe b -> Maybe (a -> b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe b
forall a. Finite a => Maybe a
highestMaybe

  predMaybe :: (a -> b) -> Maybe (a -> b)
predMaybe a -> b
f = do
    b
h <- Maybe b
forall a. Finite a => Maybe a
highestMaybe
    ((a -> b) -> Maybe (a -> b))
-> ((a -> b) -> Maybe (a -> b))
-> Either (a -> b) (a -> b)
-> Maybe (a -> b)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (a -> b) -> Maybe (a -> b)
forall a. a -> Maybe a
Just (Maybe (a -> b) -> (a -> b) -> Maybe (a -> b)
forall a b. a -> b -> a
const Maybe (a -> b)
forall a. Maybe a
Nothing)
      (Either (a -> b) (a -> b) -> Maybe (a -> b))
-> Either (a -> b) (a -> b) -> Maybe (a -> b)
forall a b. (a -> b) -> a -> b
$ (Index (ElementCount a)
 -> Either (a -> b) (a -> b) -> Either (a -> b) (a -> b))
-> Either (a -> b) (a -> b)
-> Vec (ElementCount a) (Index (ElementCount a))
-> Either (a -> b) (a -> b)
forall a b (n :: Nat). (a -> b -> b) -> b -> Vec n a -> b
foldr (\Index (ElementCount a)
i -> ((a -> b) -> Either (a -> b) (a -> b))
-> Either (a -> b) (a -> b) -> Either (a -> b) (a -> b)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
(=<<) (((a -> b) -> Either (a -> b) (a -> b))
 -> Either (a -> b) (a -> b) -> Either (a -> b) (a -> b))
-> ((a -> b) -> Either (a -> b) (a -> b))
-> Either (a -> b) (a -> b)
-> Either (a -> b) (a -> b)
forall a b. (a -> b) -> a -> b
$ \a -> b
g -> do
                 let g' :: b -> a -> b
g' b
y a
x = if a -> Index (ElementCount a)
forall a. Finite a => a -> Index (ElementCount a)
index a
x Index (ElementCount a) -> Index (ElementCount a) -> Bool
forall a. Eq a => a -> a -> Bool
== Index (ElementCount a)
i then b
y else a -> b
g a
x
                 Either (a -> b) (a -> b)
-> (b -> Either (a -> b) (a -> b))
-> Maybe b
-> Either (a -> b) (a -> b)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ((a -> b) -> Either (a -> b) (a -> b)
forall a b. b -> Either a b
Right ((a -> b) -> Either (a -> b) (a -> b))
-> (a -> b) -> Either (a -> b) (a -> b)
forall a b. (a -> b) -> a -> b
$ b -> a -> b
g' b
h) ((a -> b) -> Either (a -> b) (a -> b)
forall a b. a -> Either a b
Left ((a -> b) -> Either (a -> b) (a -> b))
-> (b -> a -> b) -> b -> Either (a -> b) (a -> b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> a -> b
g') (Maybe b -> Either (a -> b) (a -> b))
-> Maybe b -> Either (a -> b) (a -> b)
forall a b. (a -> b) -> a -> b
$ b -> Maybe b
forall a. Finite a => a -> Maybe a
predMaybe (b -> Maybe b) -> b -> Maybe b
forall a b. (a -> b) -> a -> b
$ a -> b
g (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ Index (ElementCount a) -> a
forall a. Finite a => Index (ElementCount a) -> a
ith Index (ElementCount a)
i
              ) ((a -> b) -> Either (a -> b) (a -> b)
forall a b. b -> Either a b
Right a -> b
f) (Vec (ElementCount a) (Index (ElementCount a))
 -> Either (a -> b) (a -> b))
-> Vec (ElementCount a) (Index (ElementCount a))
-> Either (a -> b) (a -> b)
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). KnownNat n => Vec n (Index n)
indicesI @(ElementCount a)

  succMaybe :: (a -> b) -> Maybe (a -> b)
succMaybe a -> b
f = do
    b
l <- Maybe b
forall a. Finite a => Maybe a
lowestMaybe
    ((a -> b) -> Maybe (a -> b))
-> ((a -> b) -> Maybe (a -> b))
-> Either (a -> b) (a -> b)
-> Maybe (a -> b)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (a -> b) -> Maybe (a -> b)
forall a. a -> Maybe a
Just (Maybe (a -> b) -> (a -> b) -> Maybe (a -> b)
forall a b. a -> b -> a
const Maybe (a -> b)
forall a. Maybe a
Nothing)
      (Either (a -> b) (a -> b) -> Maybe (a -> b))
-> Either (a -> b) (a -> b) -> Maybe (a -> b)
forall a b. (a -> b) -> a -> b
$ (Index (ElementCount a)
 -> Either (a -> b) (a -> b) -> Either (a -> b) (a -> b))
-> Either (a -> b) (a -> b)
-> Vec (ElementCount a) (Index (ElementCount a))
-> Either (a -> b) (a -> b)
forall a b (n :: Nat). (a -> b -> b) -> b -> Vec n a -> b
foldr (\Index (ElementCount a)
i -> ((a -> b) -> Either (a -> b) (a -> b))
-> Either (a -> b) (a -> b) -> Either (a -> b) (a -> b)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
(=<<) (((a -> b) -> Either (a -> b) (a -> b))
 -> Either (a -> b) (a -> b) -> Either (a -> b) (a -> b))
-> ((a -> b) -> Either (a -> b) (a -> b))
-> Either (a -> b) (a -> b)
-> Either (a -> b) (a -> b)
forall a b. (a -> b) -> a -> b
$ \a -> b
g -> do
                 let g' :: b -> a -> b
g' b
y a
x = if a -> Index (ElementCount a)
forall a. Finite a => a -> Index (ElementCount a)
index a
x Index (ElementCount a) -> Index (ElementCount a) -> Bool
forall a. Eq a => a -> a -> Bool
== Index (ElementCount a)
i then b
y else a -> b
g a
x
                 Either (a -> b) (a -> b)
-> (b -> Either (a -> b) (a -> b))
-> Maybe b
-> Either (a -> b) (a -> b)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ((a -> b) -> Either (a -> b) (a -> b)
forall a b. b -> Either a b
Right ((a -> b) -> Either (a -> b) (a -> b))
-> (a -> b) -> Either (a -> b) (a -> b)
forall a b. (a -> b) -> a -> b
$ b -> a -> b
g' b
l) ((a -> b) -> Either (a -> b) (a -> b)
forall a b. a -> Either a b
Left ((a -> b) -> Either (a -> b) (a -> b))
-> (b -> a -> b) -> b -> Either (a -> b) (a -> b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> a -> b
g') (Maybe b -> Either (a -> b) (a -> b))
-> Maybe b -> Either (a -> b) (a -> b)
forall a b. (a -> b) -> a -> b
$ b -> Maybe b
forall a. Finite a => a -> Maybe a
succMaybe (b -> Maybe b) -> b -> Maybe b
forall a b. (a -> b) -> a -> b
$ a -> b
g (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ Index (ElementCount a) -> a
forall a. Finite a => Index (ElementCount a) -> a
ith Index (ElementCount a)
i
              ) ((a -> b) -> Either (a -> b) (a -> b)
forall a b. b -> Either a b
Right a -> b
f) (Vec (ElementCount a) (Index (ElementCount a))
 -> Either (a -> b) (a -> b))
-> Vec (ElementCount a) (Index (ElementCount a))
-> Either (a -> b) (a -> b)
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). KnownNat n => Vec n (Index n)
indicesI @(ElementCount a)

  ith :: Index (ElementCount (a -> b)) -> a -> b
ith      = (((Index (ElementCount a) -> b)
-> (a -> Index (ElementCount a)) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Index (ElementCount a)
forall a. Finite a => a -> Index (ElementCount a)
index) ((Index (ElementCount a) -> b) -> a -> b)
-> (Vec (ElementCount a) b -> Index (ElementCount a) -> b)
-> Vec (ElementCount a) b
-> a
-> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vec (ElementCount a) b -> Index (ElementCount a) -> b
forall (n :: Nat) i a. (KnownNat n, Enum i) => Vec n a -> i -> a
(!!)) (Vec (ElementCount a) b -> a -> b)
-> (Index (ElementCount b ^ ElementCount a)
    -> Vec (ElementCount a) b)
-> Index (ElementCount b ^ ElementCount a)
-> a
-> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Finite a => Index (ElementCount a) -> a
ith @(Vec (ElementCount a) b)
  index :: (a -> b) -> Index (ElementCount (a -> b))
index a -> b
f  = Vec (ElementCount a) b
-> Index (ElementCount (Vec (ElementCount a) b))
forall a. Finite a => a -> Index (ElementCount a)
index (a -> b
f (a -> b)
-> (Index (ElementCount a) -> a) -> Index (ElementCount a) -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (ElementCount a) -> a
forall a. Finite a => Index (ElementCount a) -> a
ith (Index (ElementCount a) -> b)
-> Vec (ElementCount a) (Index (ElementCount a))
-> Vec (ElementCount a) b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vec (ElementCount a) (Index (ElementCount a))
forall (n :: Nat). KnownNat n => Vec n (Index n)
indicesI)

instance a ~ b => Finite (a :~: b) where
  type ElementCount (a :~: b) = 1
  elements :: Vec (ElementCount (a :~: b)) (a :~: b)
elements     = a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl (a :~: b) -> Vec 0 (a :~: b) -> Vec (0 + 1) (a :~: b)
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
:> Vec 0 (a :~: b)
forall b. Vec 0 b
Nil
  lowest :: (1 <= ElementCount (a :~: b)) => a :~: b
lowest       = a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  lowestMaybe :: Maybe (a :~: b)
lowestMaybe  = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  highest :: (1 <= ElementCount (a :~: b)) => a :~: b
highest      = a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  highestMaybe :: Maybe (a :~: b)
highestMaybe = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  predMaybe :: (a :~: b) -> Maybe (a :~: b)
predMaybe    = Maybe (a :~: b) -> (a :~: b) -> Maybe (a :~: b)
forall a b. a -> b -> a
const Maybe (a :~: b)
forall a. Maybe a
Nothing
  succMaybe :: (a :~: b) -> Maybe (a :~: b)
succMaybe    = Maybe (a :~: b) -> (a :~: b) -> Maybe (a :~: b)
forall a b. a -> b -> a
const Maybe (a :~: b)
forall a. Maybe a
Nothing
  ith :: Index (ElementCount (a :~: b)) -> a :~: b
ith          = (a :~: b) -> Index 1 -> a :~: b
forall a b. a -> b -> a
const a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  index :: (a :~: b) -> Index (ElementCount (a :~: b))
index        = Index 1 -> (a :~: b) -> Index 1
forall a b. a -> b -> a
const Index 1
0

instance a ~~ b => Finite (a :~~: b) where
  type ElementCount (a :~~: b) = 1
  elements :: Vec (ElementCount (a :~~: b)) (a :~~: b)
elements     = a :~~: a
a :~~: b
forall {k1} (a :: k1). a :~~: a
HRefl (a :~~: b) -> Vec 0 (a :~~: b) -> Vec (0 + 1) (a :~~: b)
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
:> Vec 0 (a :~~: b)
forall b. Vec 0 b
Nil
  lowest :: (1 <= ElementCount (a :~~: b)) => a :~~: b
lowest       = a :~~: a
a :~~: b
forall {k1} (a :: k1). a :~~: a
HRefl
  lowestMaybe :: Maybe (a :~~: b)
lowestMaybe  = (a :~~: b) -> Maybe (a :~~: b)
forall a. a -> Maybe a
Just a :~~: a
a :~~: b
forall {k1} (a :: k1). a :~~: a
HRefl
  highest :: (1 <= ElementCount (a :~~: b)) => a :~~: b
highest      = a :~~: a
a :~~: b
forall {k1} (a :: k1). a :~~: a
HRefl
  highestMaybe :: Maybe (a :~~: b)
highestMaybe = (a :~~: b) -> Maybe (a :~~: b)
forall a. a -> Maybe a
Just a :~~: a
a :~~: b
forall {k1} (a :: k1). a :~~: a
HRefl
  predMaybe :: (a :~~: b) -> Maybe (a :~~: b)
predMaybe    = Maybe (a :~~: b) -> (a :~~: b) -> Maybe (a :~~: b)
forall a b. a -> b -> a
const Maybe (a :~~: b)
forall a. Maybe a
Nothing
  succMaybe :: (a :~~: b) -> Maybe (a :~~: b)
succMaybe    = Maybe (a :~~: b) -> (a :~~: b) -> Maybe (a :~~: b)
forall a b. a -> b -> a
const Maybe (a :~~: b)
forall a. Maybe a
Nothing
  ith :: Index (ElementCount (a :~~: b)) -> a :~~: b
ith          = (a :~~: b) -> Index 1 -> a :~~: b
forall a b. a -> b -> a
const a :~~: a
a :~~: b
forall {k1} (a :: k1). a :~~: a
HRefl
  index :: (a :~~: b) -> Index (ElementCount (a :~~: b))
index        = Index 1 -> (a :~~: b) -> Index 1
forall a b. a -> b -> a
const Index 1
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 :: Vec (ElementCount (Down a)) (Down a)
elements     = a -> Down a
forall a. a -> Down a
Down (a -> Down a)
-> Vec (ElementCount a) a -> Vec (ElementCount a) (Down a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vec (ElementCount a) a -> Vec (ElementCount a) a
forall (n :: Nat) a. Vec n a -> Vec n a
reverse Vec (ElementCount a) a
forall a. Finite a => Vec (ElementCount a) a
elements
  lowest :: (1 <= ElementCount (Down a)) => Down a
lowest       = a -> Down a
forall a. a -> Down a
Down a
forall a. (Finite a, 1 <= ElementCount a) => a
highest
  lowestMaybe :: Maybe (Down a)
lowestMaybe  = a -> Down a
forall a. a -> Down a
Down (a -> Down a) -> Maybe a -> Maybe (Down a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe a
forall a. Finite a => Maybe a
highestMaybe
  highest :: (1 <= ElementCount (Down a)) => Down a
highest      = a -> Down a
forall a. a -> Down a
Down a
forall a. (Finite a, 1 <= ElementCount a) => a
lowest
  highestMaybe :: Maybe (Down a)
highestMaybe = a -> Down a
forall a. a -> Down a
Down (a -> Down a) -> Maybe a -> Maybe (Down a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe a
forall a. Finite a => Maybe a
lowestMaybe
  predMaybe :: Down a -> Maybe (Down a)
predMaybe    = (a -> Down a) -> Maybe a -> Maybe (Down a)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Down a
forall a. a -> Down a
Down (Maybe a -> Maybe (Down a))
-> (Down a -> Maybe a) -> Down a -> Maybe (Down a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. Finite a => a -> Maybe a
succMaybe (a -> Maybe a) -> (Down a -> a) -> Down a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Down a -> a
forall a. Down a -> a
getDown
  succMaybe :: Down a -> Maybe (Down a)
succMaybe    = (a -> Down a) -> Maybe a -> Maybe (Down a)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Down a
forall a. a -> Down a
Down (Maybe a -> Maybe (Down a))
-> (Down a -> Maybe a) -> Down a -> Maybe (Down a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. Finite a => a -> Maybe a
predMaybe (a -> Maybe a) -> (Down a -> a) -> Down a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Down a -> a
forall a. Down a -> a
getDown
  ith :: Index (ElementCount (Down a)) -> Down a
ith          = a -> Down a
forall a. a -> Down a
Down (a -> Down a)
-> (Index (ElementCount a) -> a)
-> Index (ElementCount a)
-> Down a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (ElementCount a) -> a
forall a. Finite a => Index (ElementCount a) -> a
ith (Index (ElementCount a) -> a)
-> (Index (ElementCount a) -> Index (ElementCount a))
-> Index (ElementCount a)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Index (ElementCount a)
forall a. Bounded a => a
maxBound Index (ElementCount a)
-> Index (ElementCount a) -> Index (ElementCount a)
forall a. Num a => a -> a -> a
-)
  index :: Down a -> Index (ElementCount (Down a))
index        = (Index (ElementCount a)
forall a. Bounded a => a
maxBound Index (ElementCount a)
-> Index (ElementCount a) -> Index (ElementCount a)
forall a. Num a => a -> a -> a
-) (Index (ElementCount a) -> Index (ElementCount a))
-> (Down a -> Index (ElementCount a))
-> Down a
-> Index (ElementCount a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Index (ElementCount a)
forall a. Finite a => a -> Index (ElementCount a)
index (a -> Index (ElementCount a))
-> (Down a -> a) -> Down a -> Index (ElementCount a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Down a -> a
forall a. Down a -> a
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 { forall a. GenericReverse a -> a
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 :: Vec (ElementCount (GenericReverse a)) (GenericReverse a)
elements     = a -> GenericReverse a
forall a. a -> GenericReverse a
GenericReverse (a -> GenericReverse a)
-> (Rep a Any -> a) -> Rep a Any -> GenericReverse a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Rep a Any -> GenericReverse a)
-> Vec (GElementCount (Rep a)) (Rep a Any)
-> Vec (GElementCount (Rep a)) (GenericReverse a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vec (GElementCount (Rep a)) (Rep a Any)
-> Vec (GElementCount (Rep a)) (Rep a Any)
forall (n :: Nat) a. Vec n a -> Vec n a
reverse Vec (GElementCount (Rep a)) (Rep a Any)
forall a. Vec (GElementCount (Rep a)) (Rep a a)
forall (rep :: Type -> Type) a.
GFinite rep =>
Vec (GElementCount rep) (rep a)
gElements
  lowest :: (1 <= ElementCount (GenericReverse a)) => GenericReverse a
lowest       = a -> GenericReverse a
forall a. a -> GenericReverse a
GenericReverse (a -> GenericReverse a) -> a -> GenericReverse a
forall a b. (a -> b) -> a -> b
$ Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to Rep a Any
forall a. (1 <= GElementCount (Rep a)) => Rep a a
forall (rep :: Type -> Type) a.
(GFinite rep, 1 <= GElementCount rep) =>
rep a
gHighest
  lowestMaybe :: Maybe (GenericReverse a)
lowestMaybe  = a -> GenericReverse a
forall a. a -> GenericReverse a
GenericReverse (a -> GenericReverse a)
-> (Rep a Any -> a) -> Rep a Any -> GenericReverse a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Rep a Any -> GenericReverse a)
-> Maybe (Rep a Any) -> Maybe (GenericReverse a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Rep a Any)
forall a. Maybe (Rep a a)
forall (rep :: Type -> Type) a. GFinite rep => Maybe (rep a)
gHighestMaybe
  highest :: (1 <= ElementCount (GenericReverse a)) => GenericReverse a
highest       = a -> GenericReverse a
forall a. a -> GenericReverse a
GenericReverse (a -> GenericReverse a) -> a -> GenericReverse a
forall a b. (a -> b) -> a -> b
$ Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to Rep a Any
forall a. (1 <= GElementCount (Rep a)) => Rep a a
forall (rep :: Type -> Type) a.
(GFinite rep, 1 <= GElementCount rep) =>
rep a
gLowest
  highestMaybe :: Maybe (GenericReverse a)
highestMaybe = a -> GenericReverse a
forall a. a -> GenericReverse a
GenericReverse (a -> GenericReverse a)
-> (Rep a Any -> a) -> Rep a Any -> GenericReverse a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Rep a Any -> GenericReverse a)
-> Maybe (Rep a Any) -> Maybe (GenericReverse a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Rep a Any)
forall a. Maybe (Rep a a)
forall (rep :: Type -> Type) a. GFinite rep => Maybe (rep a)
gLowestMaybe
  predMaybe :: GenericReverse a -> Maybe (GenericReverse a)
predMaybe       = (Rep a Any -> GenericReverse a)
-> Maybe (Rep a Any) -> Maybe (GenericReverse a)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (a -> GenericReverse a
forall a. a -> GenericReverse a
GenericReverse (a -> GenericReverse a)
-> (Rep a Any -> a) -> Rep a Any -> GenericReverse a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to) (Maybe (Rep a Any) -> Maybe (GenericReverse a))
-> (GenericReverse a -> Maybe (Rep a Any))
-> GenericReverse a
-> Maybe (GenericReverse a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep a Any -> Maybe (Rep a Any)
forall a. Rep a a -> Maybe (Rep a a)
forall (rep :: Type -> Type) a.
GFinite rep =>
rep a -> Maybe (rep a)
gSuccMaybe (Rep a Any -> Maybe (Rep a Any))
-> (GenericReverse a -> Rep a Any)
-> GenericReverse a
-> Maybe (Rep a Any)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from (a -> Rep a Any)
-> (GenericReverse a -> a) -> GenericReverse a -> Rep a Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenericReverse a -> a
forall a. GenericReverse a -> a
getGenericReverse
  succMaybe :: GenericReverse a -> Maybe (GenericReverse a)
succMaybe        = (Rep a Any -> GenericReverse a)
-> Maybe (Rep a Any) -> Maybe (GenericReverse a)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (a -> GenericReverse a
forall a. a -> GenericReverse a
GenericReverse (a -> GenericReverse a)
-> (Rep a Any -> a) -> Rep a Any -> GenericReverse a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to) (Maybe (Rep a Any) -> Maybe (GenericReverse a))
-> (GenericReverse a -> Maybe (Rep a Any))
-> GenericReverse a
-> Maybe (GenericReverse a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep a Any -> Maybe (Rep a Any)
forall a. Rep a a -> Maybe (Rep a a)
forall (rep :: Type -> Type) a.
GFinite rep =>
rep a -> Maybe (rep a)
gPredMaybe (Rep a Any -> Maybe (Rep a Any))
-> (GenericReverse a -> Rep a Any)
-> GenericReverse a
-> Maybe (Rep a Any)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from (a -> Rep a Any)
-> (GenericReverse a -> a) -> GenericReverse a -> Rep a Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenericReverse a -> a
forall a. GenericReverse a -> a
getGenericReverse
  ith :: Index (ElementCount (GenericReverse a)) -> GenericReverse a
ith          = a -> GenericReverse a
forall a. a -> GenericReverse a
GenericReverse (a -> GenericReverse a)
-> (Index (GElementCount (Rep a)) -> a)
-> Index (GElementCount (Rep a))
-> GenericReverse a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Rep a Any -> a)
-> (Index (GElementCount (Rep a)) -> Rep a Any)
-> Index (GElementCount (Rep a))
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (GElementCount (Rep a)) -> Rep a Any
forall a. Index (GElementCount (Rep a)) -> Rep a a
forall (rep :: Type -> Type) a.
GFinite rep =>
Index (GElementCount rep) -> rep a
gIth (Index (GElementCount (Rep a)) -> Rep a Any)
-> (Index (GElementCount (Rep a)) -> Index (GElementCount (Rep a)))
-> Index (GElementCount (Rep a))
-> Rep a Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Index (GElementCount (Rep a))
forall a. Bounded a => a
maxBound Index (GElementCount (Rep a))
-> Index (GElementCount (Rep a)) -> Index (GElementCount (Rep a))
forall a. Num a => a -> a -> a
-)
  index :: GenericReverse a -> Index (ElementCount (GenericReverse a))
index        = (Index (GElementCount (Rep a))
forall a. Bounded a => a
maxBound Index (GElementCount (Rep a))
-> Index (GElementCount (Rep a)) -> Index (GElementCount (Rep a))
forall a. Num a => a -> a -> a
-) (Index (GElementCount (Rep a)) -> Index (GElementCount (Rep a)))
-> (GenericReverse a -> Index (GElementCount (Rep a)))
-> GenericReverse a
-> Index (GElementCount (Rep a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep a Any -> Index (GElementCount (Rep a))
forall a. Rep a a -> Index (GElementCount (Rep a))
forall (rep :: Type -> Type) a.
GFinite rep =>
rep a -> Index (GElementCount rep)
gIndex (Rep a Any -> Index (GElementCount (Rep a)))
-> (GenericReverse a -> Rep a Any)
-> GenericReverse a
-> Index (GElementCount (Rep a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from (a -> Rep a Any)
-> (GenericReverse a -> a) -> GenericReverse a -> Rep a Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenericReverse a -> a
forall a. GenericReverse a -> a
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 { forall a. WithUndefined a -> a
getWithUndefined :: a }
  deriving newtype ( Eq (WithUndefined a)
WithUndefined a
Eq (WithUndefined a) =>
(WithUndefined a -> WithUndefined a -> WithUndefined a)
-> (WithUndefined a -> WithUndefined a -> WithUndefined a)
-> (WithUndefined a -> WithUndefined a -> WithUndefined a)
-> (WithUndefined a -> WithUndefined a)
-> (WithUndefined a -> Int -> WithUndefined a)
-> (WithUndefined a -> Int -> WithUndefined a)
-> WithUndefined a
-> (Int -> WithUndefined a)
-> (WithUndefined a -> Int -> WithUndefined a)
-> (WithUndefined a -> Int -> WithUndefined a)
-> (WithUndefined a -> Int -> WithUndefined a)
-> (WithUndefined a -> Int -> Bool)
-> (WithUndefined a -> Maybe Int)
-> (WithUndefined a -> Int)
-> (WithUndefined a -> Bool)
-> (WithUndefined a -> Int -> WithUndefined a)
-> (WithUndefined a -> Int -> WithUndefined a)
-> (WithUndefined a -> Int -> WithUndefined a)
-> (WithUndefined a -> Int -> WithUndefined a)
-> (WithUndefined a -> Int -> WithUndefined a)
-> (WithUndefined a -> Int -> WithUndefined a)
-> (WithUndefined a -> Int)
-> Bits (WithUndefined a)
Int -> WithUndefined a
WithUndefined a -> Bool
WithUndefined a -> Int
WithUndefined a -> Maybe Int
WithUndefined a -> WithUndefined a
WithUndefined a -> Int -> Bool
WithUndefined a -> Int -> WithUndefined a
WithUndefined a -> WithUndefined a -> WithUndefined a
forall a.
Eq a =>
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> a
-> (Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> Bool)
-> (a -> Maybe Int)
-> (a -> Int)
-> (a -> Bool)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int)
-> Bits a
forall a. Bits a => Eq (WithUndefined a)
forall a. Bits a => WithUndefined a
forall a. Bits a => Int -> WithUndefined a
forall a. Bits a => WithUndefined a -> Bool
forall a. Bits a => WithUndefined a -> Int
forall a. Bits a => WithUndefined a -> Maybe Int
forall a. Bits a => WithUndefined a -> WithUndefined a
forall a. Bits a => WithUndefined a -> Int -> Bool
forall a. Bits a => WithUndefined a -> Int -> WithUndefined a
forall a.
Bits a =>
WithUndefined a -> WithUndefined a -> WithUndefined a
$c.&. :: forall a.
Bits a =>
WithUndefined a -> WithUndefined a -> WithUndefined a
.&. :: WithUndefined a -> WithUndefined a -> WithUndefined a
$c.|. :: forall a.
Bits a =>
WithUndefined a -> WithUndefined a -> WithUndefined a
.|. :: WithUndefined a -> WithUndefined a -> WithUndefined a
$cxor :: forall a.
Bits a =>
WithUndefined a -> WithUndefined a -> WithUndefined a
xor :: WithUndefined a -> WithUndefined a -> WithUndefined a
$ccomplement :: forall a. Bits a => WithUndefined a -> WithUndefined a
complement :: WithUndefined a -> WithUndefined a
$cshift :: forall a. Bits a => WithUndefined a -> Int -> WithUndefined a
shift :: WithUndefined a -> Int -> WithUndefined a
$crotate :: forall a. Bits a => WithUndefined a -> Int -> WithUndefined a
rotate :: WithUndefined a -> Int -> WithUndefined a
$czeroBits :: forall a. Bits a => WithUndefined a
zeroBits :: WithUndefined a
$cbit :: forall a. Bits a => Int -> WithUndefined a
bit :: Int -> WithUndefined a
$csetBit :: forall a. Bits a => WithUndefined a -> Int -> WithUndefined a
setBit :: WithUndefined a -> Int -> WithUndefined a
$cclearBit :: forall a. Bits a => WithUndefined a -> Int -> WithUndefined a
clearBit :: WithUndefined a -> Int -> WithUndefined a
$ccomplementBit :: forall a. Bits a => WithUndefined a -> Int -> WithUndefined a
complementBit :: WithUndefined a -> Int -> WithUndefined a
$ctestBit :: forall a. Bits a => WithUndefined a -> Int -> Bool
testBit :: WithUndefined a -> Int -> Bool
$cbitSizeMaybe :: forall a. Bits a => WithUndefined a -> Maybe Int
bitSizeMaybe :: WithUndefined a -> Maybe Int
$cbitSize :: forall a. Bits a => WithUndefined a -> Int
bitSize :: WithUndefined a -> Int
$cisSigned :: forall a. Bits a => WithUndefined a -> Bool
isSigned :: WithUndefined a -> Bool
$cshiftL :: forall a. Bits a => WithUndefined a -> Int -> WithUndefined a
shiftL :: WithUndefined a -> Int -> WithUndefined a
$cunsafeShiftL :: forall a. Bits a => WithUndefined a -> Int -> WithUndefined a
unsafeShiftL :: WithUndefined a -> Int -> WithUndefined a
$cshiftR :: forall a. Bits a => WithUndefined a -> Int -> WithUndefined a
shiftR :: WithUndefined a -> Int -> WithUndefined a
$cunsafeShiftR :: forall a. Bits a => WithUndefined a -> Int -> WithUndefined a
unsafeShiftR :: WithUndefined a -> Int -> WithUndefined a
$crotateL :: forall a. Bits a => WithUndefined a -> Int -> WithUndefined a
rotateL :: WithUndefined a -> Int -> WithUndefined a
$crotateR :: forall a. Bits a => WithUndefined a -> Int -> WithUndefined a
rotateR :: WithUndefined a -> Int -> WithUndefined a
$cpopCount :: forall a. Bits a => WithUndefined a -> Int
popCount :: WithUndefined a -> Int
Bits, KnownNat (BitSize (WithUndefined a))
KnownNat (BitSize (WithUndefined a)) =>
(WithUndefined a -> BitVector (BitSize (WithUndefined a)))
-> (BitVector (BitSize (WithUndefined a)) -> WithUndefined a)
-> BitPack (WithUndefined a)
BitVector (BitSize (WithUndefined a)) -> WithUndefined a
WithUndefined a -> BitVector (BitSize (WithUndefined a))
forall a.
KnownNat (BitSize a) =>
(a -> BitVector (BitSize a))
-> (BitVector (BitSize a) -> a) -> BitPack a
forall a. BitPack a => KnownNat (BitSize (WithUndefined a))
forall a.
BitPack a =>
BitVector (BitSize (WithUndefined a)) -> WithUndefined a
forall a.
BitPack a =>
WithUndefined a -> BitVector (BitSize (WithUndefined a))
$cpack :: forall a.
BitPack a =>
WithUndefined a -> BitVector (BitSize (WithUndefined a))
pack :: WithUndefined a -> BitVector (BitSize (WithUndefined a))
$cunpack :: forall a.
BitPack a =>
BitVector (BitSize (WithUndefined a)) -> WithUndefined a
unpack :: BitVector (BitSize (WithUndefined a)) -> WithUndefined a
BitPack, WithUndefined a
WithUndefined a -> WithUndefined a -> Bounded (WithUndefined a)
forall a. a -> a -> Bounded a
forall a. Bounded a => WithUndefined a
$cminBound :: forall a. Bounded a => WithUndefined a
minBound :: WithUndefined a
$cmaxBound :: forall a. Bounded a => WithUndefined a
maxBound :: WithUndefined a
Bounded, Int -> WithUndefined a
WithUndefined a -> Int
WithUndefined a -> [WithUndefined a]
WithUndefined a -> WithUndefined a
WithUndefined a -> WithUndefined a -> [WithUndefined a]
WithUndefined a
-> WithUndefined a -> WithUndefined a -> [WithUndefined a]
(WithUndefined a -> WithUndefined a)
-> (WithUndefined a -> WithUndefined a)
-> (Int -> WithUndefined a)
-> (WithUndefined a -> Int)
-> (WithUndefined a -> [WithUndefined a])
-> (WithUndefined a -> WithUndefined a -> [WithUndefined a])
-> (WithUndefined a -> WithUndefined a -> [WithUndefined a])
-> (WithUndefined a
    -> WithUndefined a -> WithUndefined a -> [WithUndefined a])
-> Enum (WithUndefined a)
forall a. Enum a => Int -> WithUndefined a
forall a. Enum a => WithUndefined a -> Int
forall a. Enum a => WithUndefined a -> [WithUndefined a]
forall a. Enum a => WithUndefined a -> WithUndefined a
forall a.
Enum a =>
WithUndefined a -> WithUndefined a -> [WithUndefined a]
forall a.
Enum a =>
WithUndefined a
-> WithUndefined a -> WithUndefined a -> [WithUndefined a]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: forall a. Enum a => WithUndefined a -> WithUndefined a
succ :: WithUndefined a -> WithUndefined a
$cpred :: forall a. Enum a => WithUndefined a -> WithUndefined a
pred :: WithUndefined a -> WithUndefined a
$ctoEnum :: forall a. Enum a => Int -> WithUndefined a
toEnum :: Int -> WithUndefined a
$cfromEnum :: forall a. Enum a => WithUndefined a -> Int
fromEnum :: WithUndefined a -> Int
$cenumFrom :: forall a. Enum a => WithUndefined a -> [WithUndefined a]
enumFrom :: WithUndefined a -> [WithUndefined a]
$cenumFromThen :: forall a.
Enum a =>
WithUndefined a -> WithUndefined a -> [WithUndefined a]
enumFromThen :: WithUndefined a -> WithUndefined a -> [WithUndefined a]
$cenumFromTo :: forall a.
Enum a =>
WithUndefined a -> WithUndefined a -> [WithUndefined a]
enumFromTo :: WithUndefined a -> WithUndefined a -> [WithUndefined a]
$cenumFromThenTo :: forall a.
Enum a =>
WithUndefined a
-> WithUndefined a -> WithUndefined a -> [WithUndefined a]
enumFromThenTo :: WithUndefined a
-> WithUndefined a -> WithUndefined a -> [WithUndefined a]
Enum, WithUndefined a -> WithUndefined a -> Bool
(WithUndefined a -> WithUndefined a -> Bool)
-> (WithUndefined a -> WithUndefined a -> Bool)
-> Eq (WithUndefined a)
forall a. Eq a => WithUndefined a -> WithUndefined a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => WithUndefined a -> WithUndefined a -> Bool
== :: WithUndefined a -> WithUndefined a -> Bool
$c/= :: forall a. Eq a => WithUndefined a -> WithUndefined a -> Bool
/= :: WithUndefined a -> WithUndefined a -> Bool
Eq, Bits (WithUndefined a)
Bits (WithUndefined a) =>
(WithUndefined a -> Int)
-> (WithUndefined a -> Int)
-> (WithUndefined a -> Int)
-> FiniteBits (WithUndefined a)
WithUndefined a -> Int
forall a. FiniteBits a => Bits (WithUndefined a)
forall a. FiniteBits a => WithUndefined a -> Int
forall b.
Bits b =>
(b -> Int) -> (b -> Int) -> (b -> Int) -> FiniteBits b
$cfiniteBitSize :: forall a. FiniteBits a => WithUndefined a -> Int
finiteBitSize :: WithUndefined a -> Int
$ccountLeadingZeros :: forall a. FiniteBits a => WithUndefined a -> Int
countLeadingZeros :: WithUndefined a -> Int
$ccountTrailingZeros :: forall a. FiniteBits a => WithUndefined a -> Int
countTrailingZeros :: WithUndefined a -> Int
FiniteBits
                   , (forall x. WithUndefined a -> Rep (WithUndefined a) x)
-> (forall x. Rep (WithUndefined a) x -> WithUndefined a)
-> Generic (WithUndefined a)
forall a x. Generic a => Rep (WithUndefined a) x -> WithUndefined a
forall a x. Generic a => WithUndefined a -> Rep (WithUndefined a) x
forall x. Rep (WithUndefined a) x -> WithUndefined a
forall x. WithUndefined a -> Rep (WithUndefined a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall a x. Generic a => WithUndefined a -> Rep (WithUndefined a) x
from :: forall x. WithUndefined a -> Rep (WithUndefined a) x
$cto :: forall a x. Generic a => Rep (WithUndefined a) x -> WithUndefined a
to :: forall x. Rep (WithUndefined a) x -> WithUndefined a
Generic, Enum (WithUndefined a)
Real (WithUndefined a)
(Real (WithUndefined a), Enum (WithUndefined a)) =>
(WithUndefined a -> WithUndefined a -> WithUndefined a)
-> (WithUndefined a -> WithUndefined a -> WithUndefined a)
-> (WithUndefined a -> WithUndefined a -> WithUndefined a)
-> (WithUndefined a -> WithUndefined a -> WithUndefined a)
-> (WithUndefined a
    -> WithUndefined a -> (WithUndefined a, WithUndefined a))
-> (WithUndefined a
    -> WithUndefined a -> (WithUndefined a, WithUndefined a))
-> (WithUndefined a -> Integer)
-> Integral (WithUndefined a)
WithUndefined a -> Integer
WithUndefined a
-> WithUndefined a -> (WithUndefined a, WithUndefined a)
WithUndefined a -> WithUndefined a -> WithUndefined a
forall a. Integral a => Enum (WithUndefined a)
forall a. Integral a => Real (WithUndefined a)
forall a. Integral a => WithUndefined a -> Integer
forall a.
Integral a =>
WithUndefined a
-> WithUndefined a -> (WithUndefined a, WithUndefined a)
forall a.
Integral a =>
WithUndefined a -> WithUndefined a -> WithUndefined a
forall a.
(Real a, Enum a) =>
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> (a, a))
-> (a -> a -> (a, a))
-> (a -> Integer)
-> Integral a
$cquot :: forall a.
Integral a =>
WithUndefined a -> WithUndefined a -> WithUndefined a
quot :: WithUndefined a -> WithUndefined a -> WithUndefined a
$crem :: forall a.
Integral a =>
WithUndefined a -> WithUndefined a -> WithUndefined a
rem :: WithUndefined a -> WithUndefined a -> WithUndefined a
$cdiv :: forall a.
Integral a =>
WithUndefined a -> WithUndefined a -> WithUndefined a
div :: WithUndefined a -> WithUndefined a -> WithUndefined a
$cmod :: forall a.
Integral a =>
WithUndefined a -> WithUndefined a -> WithUndefined a
mod :: WithUndefined a -> WithUndefined a -> WithUndefined a
$cquotRem :: forall a.
Integral a =>
WithUndefined a
-> WithUndefined a -> (WithUndefined a, WithUndefined a)
quotRem :: WithUndefined a
-> WithUndefined a -> (WithUndefined a, WithUndefined a)
$cdivMod :: forall a.
Integral a =>
WithUndefined a
-> WithUndefined a -> (WithUndefined a, WithUndefined a)
divMod :: WithUndefined a
-> WithUndefined a -> (WithUndefined a, WithUndefined a)
$ctoInteger :: forall a. Integral a => WithUndefined a -> Integer
toInteger :: WithUndefined a -> Integer
Integral, HasCallStack => String -> WithUndefined a
WithUndefined a -> Bool
WithUndefined a -> ()
WithUndefined a -> WithUndefined a
(HasCallStack => String -> WithUndefined a)
-> (WithUndefined a -> Bool)
-> (WithUndefined a -> WithUndefined a)
-> (WithUndefined a -> ())
-> NFDataX (WithUndefined a)
forall a. (NFDataX a, HasCallStack) => String -> WithUndefined a
forall a. NFDataX a => WithUndefined a -> Bool
forall a. NFDataX a => WithUndefined a -> ()
forall a. NFDataX a => WithUndefined a -> WithUndefined a
forall a.
(HasCallStack => String -> a)
-> (a -> Bool) -> (a -> a) -> (a -> ()) -> NFDataX a
$cdeepErrorX :: forall a. (NFDataX a, HasCallStack) => String -> WithUndefined a
deepErrorX :: HasCallStack => String -> WithUndefined a
$chasUndefined :: forall a. NFDataX a => WithUndefined a -> Bool
hasUndefined :: WithUndefined a -> Bool
$censureSpine :: forall a. NFDataX a => WithUndefined a -> WithUndefined a
ensureSpine :: WithUndefined a -> WithUndefined a
$crnfX :: forall a. NFDataX a => WithUndefined a -> ()
rnfX :: WithUndefined a -> ()
NFDataX, Integer -> WithUndefined a
WithUndefined a -> WithUndefined a
WithUndefined a -> WithUndefined a -> WithUndefined a
(WithUndefined a -> WithUndefined a -> WithUndefined a)
-> (WithUndefined a -> WithUndefined a -> WithUndefined a)
-> (WithUndefined a -> WithUndefined a -> WithUndefined a)
-> (WithUndefined a -> WithUndefined a)
-> (WithUndefined a -> WithUndefined a)
-> (WithUndefined a -> WithUndefined a)
-> (Integer -> WithUndefined a)
-> Num (WithUndefined a)
forall a. Num a => Integer -> WithUndefined a
forall a. Num a => WithUndefined a -> WithUndefined a
forall a.
Num a =>
WithUndefined a -> WithUndefined a -> WithUndefined a
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
$c+ :: forall a.
Num a =>
WithUndefined a -> WithUndefined a -> WithUndefined a
+ :: WithUndefined a -> WithUndefined a -> WithUndefined a
$c- :: forall a.
Num a =>
WithUndefined a -> WithUndefined a -> WithUndefined a
- :: WithUndefined a -> WithUndefined a -> WithUndefined a
$c* :: forall a.
Num a =>
WithUndefined a -> WithUndefined a -> WithUndefined a
* :: WithUndefined a -> WithUndefined a -> WithUndefined a
$cnegate :: forall a. Num a => WithUndefined a -> WithUndefined a
negate :: WithUndefined a -> WithUndefined a
$cabs :: forall a. Num a => WithUndefined a -> WithUndefined a
abs :: WithUndefined a -> WithUndefined a
$csignum :: forall a. Num a => WithUndefined a -> WithUndefined a
signum :: WithUndefined a -> WithUndefined a
$cfromInteger :: forall a. Num a => Integer -> WithUndefined a
fromInteger :: Integer -> WithUndefined a
Num, Eq (WithUndefined a)
Eq (WithUndefined a) =>
(WithUndefined a -> WithUndefined a -> Ordering)
-> (WithUndefined a -> WithUndefined a -> Bool)
-> (WithUndefined a -> WithUndefined a -> Bool)
-> (WithUndefined a -> WithUndefined a -> Bool)
-> (WithUndefined a -> WithUndefined a -> Bool)
-> (WithUndefined a -> WithUndefined a -> WithUndefined a)
-> (WithUndefined a -> WithUndefined a -> WithUndefined a)
-> Ord (WithUndefined a)
WithUndefined a -> WithUndefined a -> Bool
WithUndefined a -> WithUndefined a -> Ordering
WithUndefined a -> WithUndefined a -> WithUndefined a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (WithUndefined a)
forall a. Ord a => WithUndefined a -> WithUndefined a -> Bool
forall a. Ord a => WithUndefined a -> WithUndefined a -> Ordering
forall a.
Ord a =>
WithUndefined a -> WithUndefined a -> WithUndefined a
$ccompare :: forall a. Ord a => WithUndefined a -> WithUndefined a -> Ordering
compare :: WithUndefined a -> WithUndefined a -> Ordering
$c< :: forall a. Ord a => WithUndefined a -> WithUndefined a -> Bool
< :: WithUndefined a -> WithUndefined a -> Bool
$c<= :: forall a. Ord a => WithUndefined a -> WithUndefined a -> Bool
<= :: WithUndefined a -> WithUndefined a -> Bool
$c> :: forall a. Ord a => WithUndefined a -> WithUndefined a -> Bool
> :: WithUndefined a -> WithUndefined a -> Bool
$c>= :: forall a. Ord a => WithUndefined a -> WithUndefined a -> Bool
>= :: WithUndefined a -> WithUndefined a -> Bool
$cmax :: forall a.
Ord a =>
WithUndefined a -> WithUndefined a -> WithUndefined a
max :: WithUndefined a -> WithUndefined a -> WithUndefined a
$cmin :: forall a.
Ord a =>
WithUndefined a -> WithUndefined a -> WithUndefined a
min :: WithUndefined a -> WithUndefined a -> WithUndefined a
Ord, Num (WithUndefined a)
Ord (WithUndefined a)
(Num (WithUndefined a), Ord (WithUndefined a)) =>
(WithUndefined a -> Rational) -> Real (WithUndefined a)
WithUndefined a -> Rational
forall a. (Num a, Ord a) => (a -> Rational) -> Real a
forall a. Real a => Num (WithUndefined a)
forall a. Real a => Ord (WithUndefined a)
forall a. Real a => WithUndefined a -> Rational
$ctoRational :: forall a. Real a => WithUndefined a -> Rational
toRational :: WithUndefined a -> Rational
Real, ReadPrec [WithUndefined a]
ReadPrec (WithUndefined a)
Int -> ReadS (WithUndefined a)
ReadS [WithUndefined a]
(Int -> ReadS (WithUndefined a))
-> ReadS [WithUndefined a]
-> ReadPrec (WithUndefined a)
-> ReadPrec [WithUndefined a]
-> Read (WithUndefined a)
forall a. Read a => ReadPrec [WithUndefined a]
forall a. Read a => ReadPrec (WithUndefined a)
forall a. Read a => Int -> ReadS (WithUndefined a)
forall a. Read a => ReadS [WithUndefined a]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: forall a. Read a => Int -> ReadS (WithUndefined a)
readsPrec :: Int -> ReadS (WithUndefined a)
$creadList :: forall a. Read a => ReadS [WithUndefined a]
readList :: ReadS [WithUndefined a]
$creadPrec :: forall a. Read a => ReadPrec (WithUndefined a)
readPrec :: ReadPrec (WithUndefined a)
$creadListPrec :: forall a. Read a => ReadPrec [WithUndefined a]
readListPrec :: ReadPrec [WithUndefined a]
Read
                   , Int -> WithUndefined a -> String -> String
[WithUndefined a] -> String -> String
WithUndefined a -> String
(Int -> WithUndefined a -> String -> String)
-> (WithUndefined a -> String)
-> ([WithUndefined a] -> String -> String)
-> Show (WithUndefined a)
forall a. Show a => Int -> WithUndefined a -> String -> String
forall a. Show a => [WithUndefined a] -> String -> String
forall a. Show a => WithUndefined a -> String
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: forall a. Show a => Int -> WithUndefined a -> String -> String
showsPrec :: Int -> WithUndefined a -> String -> String
$cshow :: forall a. Show a => WithUndefined a -> String
show :: WithUndefined a -> String
$cshowList :: forall a. Show a => [WithUndefined a] -> String -> String
showList :: [WithUndefined a] -> String -> String
Show, Int -> WithUndefined a -> String -> String
[WithUndefined a] -> String -> String
WithUndefined a -> String
(Int -> WithUndefined a -> String -> String)
-> (WithUndefined a -> String)
-> ([WithUndefined a] -> String -> String)
-> ShowX (WithUndefined a)
forall a. ShowX a => Int -> WithUndefined a -> String -> String
forall a. ShowX a => [WithUndefined a] -> String -> String
forall a. ShowX a => WithUndefined a -> String
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> ShowX a
$cshowsPrecX :: forall a. ShowX a => Int -> WithUndefined a -> String -> String
showsPrecX :: Int -> WithUndefined a -> String -> String
$cshowX :: forall a. ShowX a => WithUndefined a -> String
showX :: WithUndefined a -> String
$cshowListX :: forall a. ShowX a => [WithUndefined a] -> String -> String
showListX :: [WithUndefined a] -> String -> String
ShowX
                   )

-- | __NB__: not synthesizable (see 'Clash.Class.Finite.WithUndefined')
instance Finite (WithUndefined Bit) where
  type ElementCount (WithUndefined Bit) = 3
  elements :: Vec (ElementCount (WithUndefined Bit)) (WithUndefined Bit)
elements     = Bit -> WithUndefined Bit
forall a b. Coercible a b => a -> b
coerce (Bit -> WithUndefined Bit)
-> Vec 3 Bit -> Vec 3 (WithUndefined Bit)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Word -> Word -> Bit
Bit Word
0 Word
0 Bit -> Vec 2 Bit -> Vec (2 + 1) Bit
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
:> Word -> Word -> Bit
Bit Word
0 Word
1 Bit -> Vec 1 Bit -> Vec (1 + 1) Bit
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
:> Word -> Word -> Bit
Bit Word
1 Word
0 Bit -> Vec 0 Bit -> Vec (0 + 1) Bit
forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
:> Vec 0 Bit
forall b. Vec 0 b
Nil
  lowest :: (1 <= ElementCount (WithUndefined Bit)) => WithUndefined Bit
lowest       = Bit -> WithUndefined Bit
forall a b. Coercible a b => a -> b
coerce (Bit -> WithUndefined Bit) -> Bit -> WithUndefined Bit
forall a b. (a -> b) -> a -> b
$ Word -> Word -> Bit
Bit Word
0 Word
0
  lowestMaybe :: Maybe (WithUndefined Bit)
lowestMaybe  = WithUndefined Bit -> Maybe (WithUndefined Bit)
forall a. a -> Maybe a
Just (WithUndefined Bit -> Maybe (WithUndefined Bit))
-> WithUndefined Bit -> Maybe (WithUndefined Bit)
forall a b. (a -> b) -> a -> b
$ Bit -> WithUndefined Bit
forall a b. Coercible a b => a -> b
coerce (Bit -> WithUndefined Bit) -> Bit -> WithUndefined Bit
forall a b. (a -> b) -> a -> b
$ Word -> Word -> Bit
Bit Word
0 Word
0
  highest :: (1 <= ElementCount (WithUndefined Bit)) => WithUndefined Bit
highest      = Bit -> WithUndefined Bit
forall a b. Coercible a b => a -> b
coerce (Bit -> WithUndefined Bit) -> Bit -> WithUndefined Bit
forall a b. (a -> b) -> a -> b
$ Word -> Word -> Bit
Bit Word
1 Word
0
  highestMaybe :: Maybe (WithUndefined Bit)
highestMaybe = WithUndefined Bit -> Maybe (WithUndefined Bit)
forall a. a -> Maybe a
Just (WithUndefined Bit -> Maybe (WithUndefined Bit))
-> WithUndefined Bit -> Maybe (WithUndefined Bit)
forall a b. (a -> b) -> a -> b
$ Bit -> WithUndefined Bit
forall a b. Coercible a b => a -> b
coerce (Bit -> WithUndefined Bit) -> Bit -> WithUndefined Bit
forall a b. (a -> b) -> a -> b
$ Word -> Word -> Bit
Bit Word
1 Word
0
  predMaybe :: WithUndefined Bit -> Maybe (WithUndefined Bit)
predMaybe WithUndefined Bit
b     = (Bit -> WithUndefined Bit)
-> Maybe Bit -> Maybe (WithUndefined Bit)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Bit -> WithUndefined Bit
forall a b. Coercible a b => a -> b
coerce (Maybe Bit -> Maybe (WithUndefined Bit))
-> Maybe Bit -> Maybe (WithUndefined Bit)
forall a b. (a -> b) -> a -> b
$ case WithUndefined Bit -> Bit
forall a b. Coercible a b => a -> b
coerce WithUndefined Bit
b of
    Bit Word
0 Word
0 -> Maybe Bit
forall a. Maybe a
Nothing
    Bit Word
0 Word
_ -> Bit -> Maybe Bit
forall a. a -> Maybe a
Just (Bit -> Maybe Bit) -> Bit -> Maybe Bit
forall a b. (a -> b) -> a -> b
$ Word -> Word -> Bit
Bit Word
0 Word
0
    Bit
_       -> Bit -> Maybe Bit
forall a. a -> Maybe a
Just (Bit -> Maybe Bit) -> Bit -> Maybe Bit
forall a b. (a -> b) -> a -> b
$ Word -> Word -> Bit
Bit Word
0 Word
1
  succMaybe :: WithUndefined Bit -> Maybe (WithUndefined Bit)
succMaybe WithUndefined Bit
b      = (Bit -> WithUndefined Bit)
-> Maybe Bit -> Maybe (WithUndefined Bit)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Bit -> WithUndefined Bit
forall a b. Coercible a b => a -> b
coerce (Maybe Bit -> Maybe (WithUndefined Bit))
-> Maybe Bit -> Maybe (WithUndefined Bit)
forall a b. (a -> b) -> a -> b
$ case WithUndefined Bit -> Bit
forall a b. Coercible a b => a -> b
coerce WithUndefined Bit
b of
    Bit Word
0 Word
0 -> Bit -> Maybe Bit
forall a. a -> Maybe a
Just (Bit -> Maybe Bit) -> Bit -> Maybe Bit
forall a b. (a -> b) -> a -> b
$ Word -> Word -> Bit
Bit Word
0 Word
1
    Bit Word
0 Word
_ -> Bit -> Maybe Bit
forall a. a -> Maybe a
Just (Bit -> Maybe Bit) -> Bit -> Maybe Bit
forall a b. (a -> b) -> a -> b
$ Word -> Word -> Bit
Bit Word
1 Word
0
    Bit
_       -> Maybe Bit
forall a. Maybe a
Nothing
  ith :: Index (ElementCount (WithUndefined Bit)) -> WithUndefined Bit
ith          = Bit -> WithUndefined Bit
forall a b. Coercible a b => a -> b
coerce (Bit -> WithUndefined Bit)
-> (Index 3 -> Bit) -> Index 3 -> WithUndefined Bit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
    Index 3
0 -> Word -> Word -> Bit
Bit Word
0 Word
0
    Index 3
1 -> Word -> Word -> Bit
Bit Word
0 Word
1
    Index 3
_ -> Word -> Word -> Bit
Bit Word
1 Word
0
  index :: WithUndefined Bit -> Index (ElementCount (WithUndefined Bit))
index WithUndefined Bit
b      = case WithUndefined Bit -> Bit
forall a b. Coercible a b => a -> b
coerce WithUndefined Bit
b of
    Bit Word
0 Word
0 -> Index 3
Index (ElementCount (WithUndefined Bit))
0
    Bit Word
0 Word
_ -> Index 3
Index (ElementCount (WithUndefined Bit))
1
    Bit
_       -> Index 3
Index (ElementCount (WithUndefined Bit))
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 :: Vec
  (ElementCount (WithUndefined (BitVector n)))
  (WithUndefined (BitVector n))
elements = BitVector n -> WithUndefined (BitVector n)
forall a b. Coercible a b => a -> b
coerce (BitVector n -> WithUndefined (BitVector n))
-> Vec (3 ^ n) (BitVector n)
-> Vec (3 ^ n) (WithUndefined (BitVector n))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (BitVector n -> BitVector n)
-> BitVector n -> Vec (3 ^ n) (BitVector n)
forall (n :: Nat) a. KnownNat n => (a -> a) -> a -> Vec n a
iterateI BitVector n -> BitVector n
forall (n :: Nat). KnownNat n => BitVector n -> BitVector n
bvwuSuccMaybe# (Nat -> Nat -> BitVector n
forall (n :: Nat). Nat -> Nat -> BitVector n
BV Nat
0 Nat
0)

  lowest :: (1 <= ElementCount (WithUndefined (BitVector n))) =>
WithUndefined (BitVector n)
lowest = BitVector n -> WithUndefined (BitVector n)
forall a b. Coercible a b => a -> b
coerce (BitVector n -> WithUndefined (BitVector n))
-> BitVector n -> WithUndefined (BitVector n)
forall a b. (a -> b) -> a -> b
$ Nat -> Nat -> BitVector n
forall (n :: Nat). Nat -> Nat -> BitVector n
BV Nat
0 Nat
0
  lowestMaybe :: Maybe (WithUndefined (BitVector n))
lowestMaybe = WithUndefined (BitVector n) -> Maybe (WithUndefined (BitVector n))
forall a. a -> Maybe a
Just (WithUndefined (BitVector n)
 -> Maybe (WithUndefined (BitVector n)))
-> WithUndefined (BitVector n)
-> Maybe (WithUndefined (BitVector n))
forall a b. (a -> b) -> a -> b
$ BitVector n -> WithUndefined (BitVector n)
forall a b. Coercible a b => a -> b
coerce (BitVector n -> WithUndefined (BitVector n))
-> BitVector n -> WithUndefined (BitVector n)
forall a b. (a -> b) -> a -> b
$ Nat -> Nat -> BitVector n
forall (n :: Nat). Nat -> Nat -> BitVector n
BV Nat
0 Nat
0

  highest :: (1 <= ElementCount (WithUndefined (BitVector n))) =>
WithUndefined (BitVector n)
highest = BitVector n -> WithUndefined (BitVector n)
forall a b. Coercible a b => a -> b
coerce (BitVector n -> WithUndefined (BitVector n))
-> BitVector n -> WithUndefined (BitVector n)
forall a b. (a -> b) -> a -> b
$ Nat -> Nat -> BitVector n
forall (n :: Nat). Nat -> Nat -> BitVector n
BV Nat
mb Nat
mb
   where
    BV Nat
_ Nat
mb = BitVector n
forall a. Bounded a => a
maxBound :: BitVector n

  highestMaybe :: Maybe (WithUndefined (BitVector n))
highestMaybe = WithUndefined (BitVector n) -> Maybe (WithUndefined (BitVector n))
forall a. a -> Maybe a
Just (WithUndefined (BitVector n)
 -> Maybe (WithUndefined (BitVector n)))
-> WithUndefined (BitVector n)
-> Maybe (WithUndefined (BitVector n))
forall a b. (a -> b) -> a -> b
$ BitVector n -> WithUndefined (BitVector n)
forall a b. Coercible a b => a -> b
coerce (BitVector n -> WithUndefined (BitVector n))
-> BitVector n -> WithUndefined (BitVector n)
forall a b. (a -> b) -> a -> b
$ Nat -> Nat -> BitVector n
forall (n :: Nat). Nat -> Nat -> BitVector n
BV Nat
mb Nat
mb
   where
    BV Nat
_ Nat
mb = BitVector n
forall a. Bounded a => a
maxBound :: BitVector n

  predMaybe :: WithUndefined (BitVector n) -> Maybe (WithUndefined (BitVector n))
predMaybe WithUndefined (BitVector n)
bv = case WithUndefined (BitVector n) -> BitVector n
forall a b. Coercible a b => a -> b
coerce WithUndefined (BitVector n)
bv of
    BV Nat
0 Nat
0 -> Maybe (WithUndefined (BitVector n))
forall a. Maybe a
Nothing
    BV Nat
m Nat
n -> WithUndefined (BitVector n) -> Maybe (WithUndefined (BitVector n))
forall a. a -> Maybe a
Just (WithUndefined (BitVector n)
 -> Maybe (WithUndefined (BitVector n)))
-> WithUndefined (BitVector n)
-> Maybe (WithUndefined (BitVector n))
forall a b. (a -> b) -> a -> b
$ BitVector n -> WithUndefined (BitVector n)
forall a b. Coercible a b => a -> b
coerce (BitVector n -> WithUndefined (BitVector n))
-> BitVector n -> WithUndefined (BitVector n)
forall a b. (a -> b) -> a -> b
$
      if ((Nat
m Nat -> Nat -> Nat
forall a. Bits a => a -> a -> a
`xor` Nat
mb) Nat -> Nat -> Nat
forall a. Bits a => a -> a -> a
.&. Nat
n) Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
0
      then Nat -> Nat -> BitVector n
forall (n :: Nat). Nat -> Nat -> BitVector n
BV (Nat
m Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1) ((Nat
m Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1) Nat -> Nat -> Nat
forall a. Bits a => a -> a -> a
`xor` Nat
mb)
      else Nat -> Nat -> BitVector n
forall (n :: Nat). Nat -> Nat -> BitVector n
BV Nat
m ((Nat
m Nat -> Nat -> Nat
forall a. Bits a => a -> a -> a
`xor` Nat
mb) Nat -> Nat -> Nat
forall a. Bits a => a -> a -> a
.&. (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1))
   where
    BV Nat
_ Nat
mb = BitVector n
forall a. Bounded a => a
maxBound :: BitVector n

  succMaybe :: WithUndefined (BitVector n) -> Maybe (WithUndefined (BitVector n))
succMaybe (WithUndefined (BitVector n) -> BitVector n
forall a b. Coercible a b => a -> b
coerce -> bv :: BitVector n
bv@(BV Nat
m Nat
_))
    | Nat
m Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
< Nat
mb    = WithUndefined (BitVector n) -> Maybe (WithUndefined (BitVector n))
forall a. a -> Maybe a
Just (WithUndefined (BitVector n)
 -> Maybe (WithUndefined (BitVector n)))
-> WithUndefined (BitVector n)
-> Maybe (WithUndefined (BitVector n))
forall a b. (a -> b) -> a -> b
$ BitVector n -> WithUndefined (BitVector n)
forall a b. Coercible a b => a -> b
coerce (BitVector n -> WithUndefined (BitVector n))
-> BitVector n -> WithUndefined (BitVector n)
forall a b. (a -> b) -> a -> b
$ BitVector n -> BitVector n
forall (n :: Nat). KnownNat n => BitVector n -> BitVector n
bvwuSuccMaybe# BitVector n
bv
    | Bool
otherwise = Maybe (WithUndefined (BitVector n))
forall a. Maybe a
Nothing
   where
    BV Nat
_ Nat
mb = BitVector n
forall a. Bounded a => a
maxBound :: BitVector n

  ith :: Index (ElementCount (WithUndefined (BitVector n)))
-> WithUndefined (BitVector n)
ith Index (ElementCount (WithUndefined (BitVector n)))
i = BitVector n -> WithUndefined (BitVector n)
forall a b. Coercible a b => a -> b
coerce (BitVector n -> WithUndefined (BitVector n))
-> BitVector n -> WithUndefined (BitVector n)
forall a b. (a -> b) -> a -> b
$ Nat -> Nat -> BitVector n
forall (n :: Nat). Nat -> Nat -> BitVector n
BV
    (BitVector n -> Nat
toNat (BitVector n -> Nat) -> BitVector n -> Nat
forall a b. (a -> b) -> a -> b
$ BitVector n -> BitVector n
forall a. Bits a => a -> a
complement BitVector n
nMask)
    (BitVector n -> Nat
toNat (BitVector n -> Nat) -> BitVector n -> Nat
forall a b. (a -> b) -> a -> b
$ (BitVector n, BitVector n) -> BitVector n
forall a b. (a, b) -> b
snd ((BitVector n, BitVector n) -> BitVector n)
-> (BitVector n, BitVector n) -> BitVector n
forall a b. (a -> b) -> a -> b
$ (Bool -> (BitVector n, BitVector n) -> (BitVector n, BitVector n))
-> (BitVector n, BitVector n)
-> Vec n Bool
-> (BitVector n, BitVector n)
forall a b (n :: Nat). (a -> b -> b) -> b -> Vec n a -> b
foldr Bool -> (BitVector n, BitVector n) -> (BitVector n, BitVector n)
stretch (BitVector n
remaining, BitVector n
0) (Vec n Bool -> (BitVector n, BitVector n))
-> Vec n Bool -> (BitVector n, BitVector n)
forall a b. (a -> b) -> a -> b
$ BitVector (BitSize (Vec n Bool)) -> Vec n Bool
forall a. BitPack a => BitVector (BitSize a) -> a
unpack BitVector n
BitVector (BitSize (Vec n Bool))
nMask)
   where
    nMask, remaining :: BitVector n
    (BitVector n
nMask, BitVector n
remaining)
      | Dict ((2 ^ n) <= (3 ^ n))
Dict <- forall (a :: Nat) (b :: Nat) (n :: Nat).
(a <= b) =>
Dict ((a ^ n) <= (b ^ n))
powMonotone1 @2 @3 @n
      , Dict (1 <= (2 ^ n))
Dict <- forall (n :: Nat) (m :: Nat). (1 <= n) => Dict (1 <= (n ^ m))
powPositiveIfPositiveBase @2 @n
      , Dict (1 <= (3 ^ n))
Dict <- forall (n :: Nat) (m :: Nat). (1 <= n) => Dict (1 <= (n ^ m))
powPositiveIfPositiveBase @3 @n
#if !MIN_VERSION_base(4,16,0)
      , Dict <- pow2CLogDual @n
      , Dict <- leqOnePlusMinus @(2^n) @(3^n)
#endif
      = (Index ((2 ^ n) + ((3 ^ n) - (2 ^ n))) -> BitVector n)
-> (BitVector n, Index ((2 ^ n) + ((3 ^ n) - (2 ^ n))))
-> (BitVector n, BitVector n)
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: Type -> Type -> Type) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (Index (2 ^ n) -> BitVector n
Index (2 ^ n) -> BitVector (BitSize (Index (2 ^ n)))
forall a. BitPack a => a -> BitVector (BitSize a)
pack (Index (2 ^ n) -> BitVector n)
-> (Index ((2 ^ n) + ((3 ^ n) - (2 ^ n))) -> Index (2 ^ n))
-> Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
-> BitVector n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (2 ^ n) -> Index (2 ^ n)
forall a. Bits a => a -> a
complement (Index (2 ^ n) -> Index (2 ^ n))
-> (Index ((2 ^ n) + ((3 ^ n) - (2 ^ n))) -> Index (2 ^ n))
-> Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
-> Index (2 ^ n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a) =>
f (a + b) -> f a
truncateB @Index @(2^n) @(3^n - 2^n))
      ((BitVector n, Index ((2 ^ n) + ((3 ^ n) - (2 ^ n))))
 -> (BitVector n, BitVector n))
-> (BitVector n, Index ((2 ^ n) + ((3 ^ n) - (2 ^ n))))
-> (BitVector n, BitVector n)
forall a b. (a -> b) -> a -> b
$ ((BitVector n, Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))),
 Index ((2 ^ n) + ((3 ^ n) - (2 ^ n))))
-> (BitVector n, Index ((2 ^ n) + ((3 ^ n) - (2 ^ n))))
forall a b. (a, b) -> a
fst
      (((BitVector n, Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))),
  Index ((2 ^ n) + ((3 ^ n) - (2 ^ n))))
 -> (BitVector n, Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))))
-> ((BitVector n, Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))),
    Index ((2 ^ n) + ((3 ^ n) - (2 ^ n))))
-> (BitVector n, Index ((2 ^ n) + ((3 ^ n) - (2 ^ n))))
forall a b. (a -> b) -> a -> b
$ (((BitVector n, Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))),
  Index ((2 ^ n) + ((3 ^ n) - (2 ^ n))))
 -> Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
 -> ((BitVector n, Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))),
     Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))))
-> ((BitVector n, Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))),
    Index ((2 ^ n) + ((3 ^ n) - (2 ^ n))))
-> Vec n (Index ((2 ^ n) + ((3 ^ n) - (2 ^ n))))
-> ((BitVector n, Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))),
    Index ((2 ^ n) + ((3 ^ n) - (2 ^ n))))
forall b a (n :: Nat). (b -> a -> b) -> b -> Vec n a -> b
foldl
         ( \(((BitVector n -> Int -> BitVector n
forall a. Bits a => a -> Int -> a
`shiftL` Int
1) -> BitVector n
m, Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
r), Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
x2) Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
x3 ->
             if Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
r Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
-> Index ((2 ^ n) + ((3 ^ n) - (2 ^ n))) -> Bool
forall a. Ord a => a -> a -> Bool
< Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
x2 Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
-> Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
-> Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
forall a. Num a => a -> a -> a
* Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
x3
             then ((BitVector n
m,            Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
r          ),     Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
x2)
             else ((BitVector n
m BitVector n -> Int -> BitVector n
forall a. Bits a => a -> Int -> a
`setBit` Int
0, Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
r Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
-> Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
-> Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
forall a. Num a => a -> a -> a
- Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
x2 Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
-> Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
-> Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
forall a. Num a => a -> a -> a
* Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
x3), Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
2 Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
-> Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
-> Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
forall a. Num a => a -> a -> a
* Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
x2)
         )
         ((BitVector n
0, Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
-> Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
forall a. Num a => a -> a
negate (Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
 -> Index ((2 ^ n) + ((3 ^ n) - (2 ^ n))))
-> Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
-> Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
forall a b. (a -> b) -> a -> b
$ SaturationMode
-> Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
-> Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
forall a. SaturatingNum a => SaturationMode -> a -> a
satSucc SaturationMode
SatWrap Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
Index (ElementCount (WithUndefined (BitVector n)))
i), Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
1)
      (Vec n (Index ((2 ^ n) + ((3 ^ n) - (2 ^ n))))
 -> ((BitVector n, Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))),
     Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))))
-> Vec n (Index ((2 ^ n) + ((3 ^ n) - (2 ^ n))))
-> ((BitVector n, Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))),
    Index ((2 ^ n) + ((3 ^ n) - (2 ^ n))))
forall a b. (a -> b) -> a -> b
$ Vec n (Index ((2 ^ n) + ((3 ^ n) - (2 ^ n))))
-> Vec n (Index ((2 ^ n) + ((3 ^ n) - (2 ^ n))))
forall (n :: Nat) a. Vec n a -> Vec n a
reverse
      (Vec n (Index ((2 ^ n) + ((3 ^ n) - (2 ^ n))))
 -> Vec n (Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))))
-> Vec n (Index ((2 ^ n) + ((3 ^ n) - (2 ^ n))))
-> Vec n (Index ((2 ^ n) + ((3 ^ n) - (2 ^ n))))
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) a. KnownNat n => (a -> a) -> a -> Vec n a
iterateI @n (Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
3 Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
-> Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
-> Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
forall a. Num a => a -> a -> a
*) Index ((2 ^ n) + ((3 ^ n) - (2 ^ n)))
1

    stretch :: Bool -> (BitVector n, BitVector n) -> (BitVector n, BitVector n)
stretch Bool
negMBit (BitVector n
bv, (BitVector n -> Int -> BitVector n
forall a. Bits a => a -> Int -> a
`shiftR` Int
1) -> BitVector n
v)
      | Bool
negMBit   = (BitVector n -> Int -> BitVector n
forall a. Bits a => a -> Int -> a
shiftR BitVector n
bv Int
1, ) (BitVector n -> (BitVector n, BitVector n))
-> BitVector n -> (BitVector n, BitVector n)
forall a b. (a -> b) -> a -> b
$ if BitVector n -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit BitVector n
bv Int
0 then BitVector n -> BitVector n
setMsb BitVector n
v else BitVector n
v
      | Bool
otherwise = (BitVector n
bv, BitVector n
v)

    toNat :: BitVector n -> Nat
toNat = Integer -> Nat
forall a. Num a => Integer -> a
fromInteger (Integer -> Nat) -> (BitVector n -> Integer) -> BitVector n -> Nat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BitVector n -> Integer
forall a. Integral a => a -> Integer
toInteger
    setMsb :: BitVector n -> BitVector n
setMsb = BitVector n -> BitVector n -> BitVector n
forall a. Bits a => a -> a -> a
(.|.) (BitVector n -> BitVector n
forall a. Bits a => a -> a
complement (BitVector n -> BitVector n) -> BitVector n -> BitVector n
forall a b. (a -> b) -> a -> b
$ BitVector n -> BitVector n
forall a. Bits a => a -> a
complement BitVector n
0 BitVector n -> Int -> BitVector n
forall a. Bits a => a -> Int -> a
`shiftR` Int
1)

  index :: WithUndefined (BitVector n)
-> Index (ElementCount (WithUndefined (BitVector n)))
index (WithUndefined (BitVector n) -> BitVector n
forall a b. Coercible a b => a -> b
coerce -> bv :: BitVector n
bv@(BV Nat
mask Nat
_))
    | Dict (1 <= (3 ^ n))
Dict <- forall (n :: Nat) (m :: Nat). (1 <= n) => Dict (1 <= (n ^ m))
powPositiveIfPositiveBase @3 @n
    = -- compute the mask induced offset
      Index (3 ^ n) -> Index (3 ^ n)
forall a. Num a => a -> a
negate
        ( (Index (3 ^ n), Index (3 ^ n)) -> Index (3 ^ n)
forall a b. (a, b) -> b
snd
        ((Index (3 ^ n), Index (3 ^ n)) -> Index (3 ^ n))
-> (Index (3 ^ n), Index (3 ^ n)) -> Index (3 ^ n)
forall a b. (a -> b) -> a -> b
$ (Bool
 -> (Index (3 ^ n), Index (3 ^ n))
 -> (Index (3 ^ n), Index (3 ^ n)))
-> (Index (3 ^ n), Index (3 ^ n))
-> Vec n Bool
-> (Index (3 ^ n), Index (3 ^ n))
forall a b (n :: Nat). (a -> b -> b) -> b -> Vec n a -> b
foldr (\Bool
b (Index (3 ^ n)
p, Index (3 ^ n)
a) -> (Index (3 ^ n)
3 Index (3 ^ n) -> Index (3 ^ n) -> Index (3 ^ n)
forall a. Num a => a -> a -> a
* Index (3 ^ n)
p, if Bool
b then Index (3 ^ n)
p Index (3 ^ n) -> Index (3 ^ n) -> Index (3 ^ n)
forall a. Num a => a -> a -> a
+ Index (3 ^ n)
2 Index (3 ^ n) -> Index (3 ^ n) -> Index (3 ^ n)
forall a. Num a => a -> a -> a
* Index (3 ^ n)
a else Index (3 ^ n)
a)) (Index (3 ^ n)
1, Index (3 ^ n)
0)
        (Vec n Bool -> (Index (3 ^ n), Index (3 ^ n)))
-> Vec n Bool -> (Index (3 ^ n), Index (3 ^ n))
forall a b. (a -> b) -> a -> b
$ forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce @(Unsigned n) @(Vec n Bool)
        (Unsigned n -> Vec n Bool) -> Unsigned n -> Vec n Bool
forall a b. (a -> b) -> a -> b
$ Unsigned n -> Unsigned n
forall a. Num a => a -> a
negate
        (Unsigned n -> Unsigned n) -> Unsigned n -> Unsigned n
forall a b. (a -> b) -> a -> b
$ Nat -> Unsigned n
forall (n :: Nat). Nat -> Unsigned n
U Nat
mask
        )
    Index (3 ^ n) -> Index (3 ^ n) -> Index (3 ^ n)
forall a. Num a => a -> a -> a
+ -- re-align the value bits according to the mask
      (Index (3 ^ n) -> Bit -> Index (3 ^ n))
-> Index (3 ^ n) -> Vec n Bit -> Index (3 ^ n)
forall b a (n :: Nat). (b -> a -> b) -> b -> Vec n a -> b
foldl
        ( \Index (3 ^ n)
a (Bit Word
m Word
n) -> if
            | Word
m Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
/= Word
0    -> Index (3 ^ n)
a
            | Word
n Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
0    -> Index (3 ^ n) -> Int -> Index (3 ^ n)
forall a. Bits a => a -> Int -> a
shiftL Index (3 ^ n)
a Int
1
            | Bool
otherwise -> Index (3 ^ n) -> Int -> Index (3 ^ n)
forall a. Bits a => a -> Int -> a
shiftL Index (3 ^ n)
a Int
1 Index (3 ^ n) -> Int -> Index (3 ^ n)
forall a. Bits a => a -> Int -> a
`setBit` Int
0
        ) Index (3 ^ n)
0 (BitVector n -> Vec n Bit
forall (n :: Nat). KnownNat n => BitVector n -> Vec n Bit
bv2v BitVector n
bv)

bvwuSuccMaybe# :: forall n. KnownNat n => BitVector n -> BitVector n
bvwuSuccMaybe# :: forall (n :: Nat). KnownNat n => BitVector n -> BitVector n
bvwuSuccMaybe# (BV Nat
m Nat
n)
  | Nat
n Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
< Nat
mb    = Nat -> Nat -> BitVector n
forall (n :: Nat). Nat -> Nat -> BitVector n
BV Nat
m ((Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1) Nat -> Nat -> Nat
forall a. Bits a => a -> a -> a
.|. Nat
m)
  | Bool
otherwise = Nat -> Nat -> BitVector n
forall (n :: Nat). Nat -> Nat -> BitVector n
BV (Nat
m Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1) (Nat
m Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1)
 where
  BV Nat
_ Nat
mb = BitVector n
forall a. Bounded a => a
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 { forall (n :: Nat) a. BoundedEnumEq n a -> a
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 :: Vec (ElementCount (BoundedEnumEq n a)) (BoundedEnumEq n a)
elements = a -> BoundedEnumEq n a
forall (n :: Nat) a. a -> BoundedEnumEq n a
BoundedEnumEq (a -> BoundedEnumEq n a) -> Vec n a -> Vec n (BoundedEnumEq n a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> a) -> a -> Vec n a
forall (n :: Nat) a. KnownNat n => (a -> a) -> a -> Vec n a
iterateI a -> a
forall a. Enum a => a -> a
succ a
forall a. Bounded a => a
minBound
  lowest :: (1 <= ElementCount (BoundedEnumEq n a)) => BoundedEnumEq n a
lowest = a -> BoundedEnumEq n a
forall (n :: Nat) a. a -> BoundedEnumEq n a
BoundedEnumEq a
forall a. Bounded a => a
minBound
  lowestMaybe :: Maybe (BoundedEnumEq n a)
lowestMaybe = BoundedEnumEq n a -> Maybe (BoundedEnumEq n a)
forall a. a -> Maybe a
Just (BoundedEnumEq n a -> Maybe (BoundedEnumEq n a))
-> BoundedEnumEq n a -> Maybe (BoundedEnumEq n a)
forall a b. (a -> b) -> a -> b
$ a -> BoundedEnumEq n a
forall (n :: Nat) a. a -> BoundedEnumEq n a
BoundedEnumEq a
forall a. Bounded a => a
minBound
  highest :: (1 <= ElementCount (BoundedEnumEq n a)) => BoundedEnumEq n a
highest = a -> BoundedEnumEq n a
forall (n :: Nat) a. a -> BoundedEnumEq n a
BoundedEnumEq a
forall a. Bounded a => a
maxBound
  highestMaybe :: Maybe (BoundedEnumEq n a)
highestMaybe = BoundedEnumEq n a -> Maybe (BoundedEnumEq n a)
forall a. a -> Maybe a
Just (BoundedEnumEq n a -> Maybe (BoundedEnumEq n a))
-> BoundedEnumEq n a -> Maybe (BoundedEnumEq n a)
forall a b. (a -> b) -> a -> b
$ a -> BoundedEnumEq n a
forall (n :: Nat) a. a -> BoundedEnumEq n a
BoundedEnumEq a
forall a. Bounded a => a
maxBound
  predMaybe :: BoundedEnumEq n a -> Maybe (BoundedEnumEq n a)
predMaybe (BoundedEnumEq n a -> a
forall (n :: Nat) a. BoundedEnumEq n a -> a
getBoundedEnumEq -> a
x)
    | a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Bounded a => a
minBound = Maybe (BoundedEnumEq n a)
forall a. Maybe a
Nothing
    | Bool
otherwise     = BoundedEnumEq n a -> Maybe (BoundedEnumEq n a)
forall a. a -> Maybe a
Just (BoundedEnumEq n a -> Maybe (BoundedEnumEq n a))
-> BoundedEnumEq n a -> Maybe (BoundedEnumEq n a)
forall a b. (a -> b) -> a -> b
$ a -> BoundedEnumEq n a
forall (n :: Nat) a. a -> BoundedEnumEq n a
BoundedEnumEq (a -> BoundedEnumEq n a) -> a -> BoundedEnumEq n a
forall a b. (a -> b) -> a -> b
$ a -> a
forall a. Enum a => a -> a
pred a
x
  succMaybe :: BoundedEnumEq n a -> Maybe (BoundedEnumEq n a)
succMaybe (BoundedEnumEq n a -> a
forall (n :: Nat) a. BoundedEnumEq n a -> a
getBoundedEnumEq -> a
x)
    | a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Bounded a => a
maxBound = Maybe (BoundedEnumEq n a)
forall a. Maybe a
Nothing
    | Bool
otherwise     = BoundedEnumEq n a -> Maybe (BoundedEnumEq n a)
forall a. a -> Maybe a
Just (BoundedEnumEq n a -> Maybe (BoundedEnumEq n a))
-> BoundedEnumEq n a -> Maybe (BoundedEnumEq n a)
forall a b. (a -> b) -> a -> b
$  a -> BoundedEnumEq n a
forall (n :: Nat) a. a -> BoundedEnumEq n a
BoundedEnumEq (a -> BoundedEnumEq n a) -> a -> BoundedEnumEq n a
forall a b. (a -> b) -> a -> b
$ a -> a
forall a. Enum a => a -> a
succ a
x
  ith :: Index (ElementCount (BoundedEnumEq n a)) -> BoundedEnumEq n a
ith = a -> BoundedEnumEq n a
forall (n :: Nat) a. a -> BoundedEnumEq n a
BoundedEnumEq (a -> BoundedEnumEq n a)
-> (Index n -> a) -> Index n -> BoundedEnumEq n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a
forall a. Enum a => Int -> a
toEnum (Int -> a) -> (Index n -> Int) -> Index n -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ a -> Int
forall a. Enum a => a -> Int
fromEnum (forall a. Bounded a => a
minBound @a)) (Int -> Int) -> (Index n -> Int) -> Index n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index n -> Int
forall a. Enum a => a -> Int
fromEnum
  index :: BoundedEnumEq n a -> Index (ElementCount (BoundedEnumEq n a))
index = Int -> Index n
forall a. Enum a => Int -> a
toEnum (Int -> Index n)
-> (BoundedEnumEq n a -> Int) -> BoundedEnumEq n a -> Index n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Int -> Int) -> Int -> Int -> Int
forall a b c. (a -> b -> c) -> b -> a -> c
flip (-) (a -> Int
forall a. Enum a => a -> Int
fromEnum (forall a. Bounded a => a
minBound @a))
           (Int -> Int)
-> (BoundedEnumEq n a -> Int) -> BoundedEnumEq n a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Int
forall a. Enum a => a -> Int
fromEnum (a -> Int) -> (BoundedEnumEq n a -> a) -> BoundedEnumEq n a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BoundedEnumEq n a -> a
forall (n :: Nat) a. BoundedEnumEq n a -> a
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 { forall a. FiniteDerive a -> a
getFiniteDerive :: a }

instance Finite a => Enum (FiniteDerive a) where
  succ :: FiniteDerive a -> FiniteDerive a
succ = a -> FiniteDerive a
forall a. a -> FiniteDerive a
FiniteDerive (a -> FiniteDerive a)
-> (FiniteDerive a -> a) -> FiniteDerive a -> FiniteDerive a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe a -> a
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe a -> a)
-> (FiniteDerive a -> Maybe a) -> FiniteDerive a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. Finite a => a -> Maybe a
succMaybe (a -> Maybe a)
-> (FiniteDerive a -> a) -> FiniteDerive a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FiniteDerive a -> a
forall a. FiniteDerive a -> a
getFiniteDerive
  pred :: FiniteDerive a -> FiniteDerive a
pred = a -> FiniteDerive a
forall a. a -> FiniteDerive a
FiniteDerive (a -> FiniteDerive a)
-> (FiniteDerive a -> a) -> FiniteDerive a -> FiniteDerive a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe a -> a
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe a -> a)
-> (FiniteDerive a -> Maybe a) -> FiniteDerive a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. Finite a => a -> Maybe a
predMaybe (a -> Maybe a)
-> (FiniteDerive a -> a) -> FiniteDerive a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FiniteDerive a -> a
forall a. FiniteDerive a -> a
getFiniteDerive
  toEnum :: Int -> FiniteDerive a
toEnum = a -> FiniteDerive a
forall a. a -> FiniteDerive a
FiniteDerive (a -> FiniteDerive a) -> (Int -> a) -> Int -> FiniteDerive a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (ElementCount a) -> a
forall a. Finite a => Index (ElementCount a) -> a
ith (Index (ElementCount a) -> a)
-> (Int -> Index (ElementCount a)) -> Int -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Index (ElementCount a)
forall a. Enum a => Int -> a
toEnum (Int -> Index (ElementCount a))
-> (Int -> Int) -> Int -> Index (ElementCount a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` forall (n :: Nat) a. (Num a, KnownNat n) => a
natToNum @(ElementCount a))
  fromEnum :: FiniteDerive a -> Int
fromEnum = Index (ElementCount a) -> Int
forall a. Enum a => a -> Int
fromEnum (Index (ElementCount a) -> Int)
-> (FiniteDerive a -> Index (ElementCount a))
-> FiniteDerive a
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Index (ElementCount a)
forall a. Finite a => a -> Index (ElementCount a)
index (a -> Index (ElementCount a))
-> (FiniteDerive a -> a)
-> FiniteDerive a
-> Index (ElementCount a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FiniteDerive a -> a
forall a. FiniteDerive a -> a
getFiniteDerive
  enumFrom :: FiniteDerive a -> [FiniteDerive a]
enumFrom FiniteDerive a
x =
    Int -> [FiniteDerive a] -> [FiniteDerive a]
forall a. Int -> [a] -> [a]
take (forall (n :: Nat) a. (Num a, KnownNat n) => a
natToNum @(ElementCount a) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Index (ElementCount a) -> Int
forall a. Enum a => a -> Int
fromEnum (a -> Index (ElementCount a)
forall a. Finite a => a -> Index (ElementCount a)
index (a -> Index (ElementCount a)) -> a -> Index (ElementCount a)
forall a b. (a -> b) -> a -> b
$ FiniteDerive a -> a
forall a. FiniteDerive a -> a
getFiniteDerive FiniteDerive a
x))
      ([FiniteDerive a] -> [FiniteDerive a])
-> [FiniteDerive a] -> [FiniteDerive a]
forall a b. (a -> b) -> a -> b
$ (FiniteDerive a -> FiniteDerive a)
-> FiniteDerive a -> [FiniteDerive a]
forall a. (a -> a) -> a -> [a]
List.iterate FiniteDerive a -> FiniteDerive a
forall a. Enum a => a -> a
succ FiniteDerive a
x
  enumFromTo :: FiniteDerive a -> FiniteDerive a -> [FiniteDerive a]
enumFromTo FiniteDerive a
x FiniteDerive a
y =
    Int -> [FiniteDerive a] -> [FiniteDerive a]
forall a. Int -> [a] -> [a]
take (Index (ElementCount a) -> Int
forall a. Enum a => a -> Int
fromEnum (a -> Index (ElementCount a)
forall a. Finite a => a -> Index (ElementCount a)
index (FiniteDerive a -> a
forall a. FiniteDerive a -> a
getFiniteDerive FiniteDerive a
y) Index (ElementCount a)
-> Index (ElementCount a) -> Index (ElementCount a)
forall a. Num a => a -> a -> a
- a -> Index (ElementCount a)
forall a. Finite a => a -> Index (ElementCount a)
index (FiniteDerive a -> a
forall a. FiniteDerive a -> a
getFiniteDerive FiniteDerive a
x)))
      ([FiniteDerive a] -> [FiniteDerive a])
-> [FiniteDerive a] -> [FiniteDerive a]
forall a b. (a -> b) -> a -> b
$ (FiniteDerive a -> FiniteDerive a)
-> FiniteDerive a -> [FiniteDerive a]
forall a. (a -> a) -> a -> [a]
List.iterate FiniteDerive a -> FiniteDerive a
forall a. Enum a => a -> a
succ FiniteDerive a
x
  enumFromThen :: FiniteDerive a -> FiniteDerive a -> [FiniteDerive a]
enumFromThen = case SNat (ElementCount a) -> UNat (ElementCount a)
forall (n :: Nat). SNat n -> UNat n
toUNat (forall (n :: Nat). KnownNat n => SNat n
SNat @(ElementCount a)) of
    UNat (ElementCount a)
UZero -> (FiniteDerive a -> [FiniteDerive a])
-> FiniteDerive a -> FiniteDerive a -> [FiniteDerive a]
forall a b. a -> b -> a
const ((FiniteDerive a -> [FiniteDerive a])
 -> FiniteDerive a -> FiniteDerive a -> [FiniteDerive a])
-> (FiniteDerive a -> [FiniteDerive a])
-> FiniteDerive a
-> FiniteDerive a
-> [FiniteDerive a]
forall a b. (a -> b) -> a -> b
$ [FiniteDerive a] -> FiniteDerive a -> [FiniteDerive a]
forall a b. a -> b -> a
const []
    USucc UNat n
um -> \FiniteDerive a
x FiniteDerive a
y -> a -> FiniteDerive a
forall a. a -> FiniteDerive a
FiniteDerive (a -> FiniteDerive a)
-> (Index (n + 1) -> a) -> Index (n + 1) -> FiniteDerive a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (n + 1) -> a
Index (ElementCount a) -> a
forall a. Finite a => Index (ElementCount a) -> a
ith (Index (n + 1) -> FiniteDerive a)
-> [Index (n + 1)] -> [FiniteDerive a]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
      [  a -> Index (ElementCount a)
forall a. Finite a => a -> Index (ElementCount a)
index (FiniteDerive a -> a
forall a. FiniteDerive a -> a
getFiniteDerive FiniteDerive a
x)
      ,  a -> Index (ElementCount a)
forall a. Finite a => a -> Index (ElementCount a)
index (FiniteDerive a -> a
forall a. FiniteDerive a -> a
getFiniteDerive FiniteDerive a
y)
      .. SNat n -> Index (n + 1)
forall a (n :: Nat). Num a => SNat n -> a
snatToNum (UNat n -> SNat n
forall (n :: Nat). UNat n -> SNat n
fromUNat UNat n
um)
      ]
  enumFromThenTo :: FiniteDerive a
-> FiniteDerive a -> FiniteDerive a -> [FiniteDerive a]
enumFromThenTo = case SNat (ElementCount a) -> UNat (ElementCount a)
forall (n :: Nat). SNat n -> UNat n
toUNat (forall (n :: Nat). KnownNat n => SNat n
SNat @(ElementCount a)) of
    UNat (ElementCount a)
UZero -> (FiniteDerive a -> FiniteDerive a -> [FiniteDerive a])
-> FiniteDerive a
-> FiniteDerive a
-> FiniteDerive a
-> [FiniteDerive a]
forall a b. a -> b -> a
const ((FiniteDerive a -> FiniteDerive a -> [FiniteDerive a])
 -> FiniteDerive a
 -> FiniteDerive a
 -> FiniteDerive a
 -> [FiniteDerive a])
-> (FiniteDerive a -> FiniteDerive a -> [FiniteDerive a])
-> FiniteDerive a
-> FiniteDerive a
-> FiniteDerive a
-> [FiniteDerive a]
forall a b. (a -> b) -> a -> b
$ (FiniteDerive a -> [FiniteDerive a])
-> FiniteDerive a -> FiniteDerive a -> [FiniteDerive a]
forall a b. a -> b -> a
const ((FiniteDerive a -> [FiniteDerive a])
 -> FiniteDerive a -> FiniteDerive a -> [FiniteDerive a])
-> (FiniteDerive a -> [FiniteDerive a])
-> FiniteDerive a
-> FiniteDerive a
-> [FiniteDerive a]
forall a b. (a -> b) -> a -> b
$ [FiniteDerive a] -> FiniteDerive a -> [FiniteDerive a]
forall a b. a -> b -> a
const []
    USucc UNat n
_ -> \FiniteDerive a
x FiniteDerive a
y FiniteDerive a
z -> a -> FiniteDerive a
forall a. a -> FiniteDerive a
FiniteDerive (a -> FiniteDerive a)
-> (Index (n + 1) -> a) -> Index (n + 1) -> FiniteDerive a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (n + 1) -> a
Index (ElementCount a) -> a
forall a. Finite a => Index (ElementCount a) -> a
ith (Index (n + 1) -> FiniteDerive a)
-> [Index (n + 1)] -> [FiniteDerive a]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
      [  a -> Index (ElementCount a)
forall a. Finite a => a -> Index (ElementCount a)
index (FiniteDerive a -> a
forall a. FiniteDerive a -> a
getFiniteDerive FiniteDerive a
x)
      ,  a -> Index (ElementCount a)
forall a. Finite a => a -> Index (ElementCount a)
index (FiniteDerive a -> a
forall a. FiniteDerive a -> a
getFiniteDerive FiniteDerive a
y)
      .. a -> Index (ElementCount a)
forall a. Finite a => a -> Index (ElementCount a)
index (FiniteDerive a -> a
forall a. FiniteDerive a -> a
getFiniteDerive FiniteDerive a
z)
      ]

instance (Finite a, 1 <= ElementCount a) => Bounded (FiniteDerive a) where
  minBound :: FiniteDerive a
minBound = a -> FiniteDerive a
forall a. a -> FiniteDerive a
FiniteDerive a
forall a. (Finite a, 1 <= ElementCount a) => a
lowest
  maxBound :: FiniteDerive a
maxBound = a -> FiniteDerive a
forall a. a -> FiniteDerive a
FiniteDerive a
forall a. (Finite a, 1 <= ElementCount a) => a
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