{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
module Data.Fin.Int.Explicit
(
Fin, FinSize
, fin, finFromIntegral, knownFin, tryFin, finMod, finDivMod, finToInt
, embed, unembed, tryUnembed
, shiftFin, unshiftFin, tryUnshiftFin, splitFin, concatFin
, weaken, strengthen
, minFin, maxFin
, enumFin, enumFinDown, enumDownFrom, enumDownTo, enumDownFromTo
, tryAdd, trySub, tryMul
, chkAdd, chkSub, chkMul
, modAdd, modSub, modMul, modNegate
, divModFin
, complementFin, twice, half, quarter
, crossFin
, attLT, attPlus, attMinus, attInt
, unsafeFin, unsafePred, unsafeSucc, unsafeCoFin, unsafeCoInt
) where
import Control.DeepSeq (NFData(rnf))
import Data.Coerce (coerce)
import Data.Data (Data)
import Data.Maybe (mapMaybe)
import Data.Type.Coercion (Coercion(..))
import GHC.Stack (HasCallStack, withFrozenCallStack)
import GHC.TypeNats
( type (*), type (+), type (-), type (<=)
, Nat, KnownNat
)
import Data.Default.Class (Default(..))
import Data.Portray (Portray)
import Data.Portray.Diff (Diff)
import Data.Type.Attenuation
( Attenuation, coercible
#if MIN_VERSION_attenuation(0, 2, 0)
, Attenuable(..)
#endif
)
import Test.QuickCheck (Arbitrary(..), arbitraryBoundedEnum)
import Data.SInt (SInt, unSInt, sintVal)
type FinRep = Int
newtype Fin (n :: Nat) = Fin FinRep
deriving (Fin n -> Fin n -> Bool
forall (n :: Nat). Fin n -> Fin n -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Fin n -> Fin n -> Bool
$c/= :: forall (n :: Nat). Fin n -> Fin n -> Bool
== :: Fin n -> Fin n -> Bool
$c== :: forall (n :: Nat). Fin n -> Fin n -> Bool
Eq, Fin n -> Fin n -> Bool
Fin n -> Fin n -> Ordering
Fin n -> Fin n -> Fin n
forall (n :: Nat). Eq (Fin n)
forall (n :: Nat). Fin n -> Fin n -> Bool
forall (n :: Nat). Fin n -> Fin n -> Ordering
forall (n :: Nat). Fin n -> Fin n -> Fin n
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
min :: Fin n -> Fin n -> Fin n
$cmin :: forall (n :: Nat). Fin n -> Fin n -> Fin n
max :: Fin n -> Fin n -> Fin n
$cmax :: forall (n :: Nat). Fin n -> Fin n -> Fin n
>= :: Fin n -> Fin n -> Bool
$c>= :: forall (n :: Nat). Fin n -> Fin n -> Bool
> :: Fin n -> Fin n -> Bool
$c> :: forall (n :: Nat). Fin n -> Fin n -> Bool
<= :: Fin n -> Fin n -> Bool
$c<= :: forall (n :: Nat). Fin n -> Fin n -> Bool
< :: Fin n -> Fin n -> Bool
$c< :: forall (n :: Nat). Fin n -> Fin n -> Bool
compare :: Fin n -> Fin n -> Ordering
$ccompare :: forall (n :: Nat). Fin n -> Fin n -> Ordering
Ord, Fin n -> DataType
Fin n -> Constr
forall {n :: Nat}. KnownNat n => Typeable (Fin n)
forall (n :: Nat). KnownNat n => Fin n -> DataType
forall (n :: Nat). KnownNat n => Fin n -> Constr
forall (n :: Nat).
KnownNat n =>
(forall b. Data b => b -> b) -> Fin n -> Fin n
forall (n :: Nat) u.
KnownNat n =>
Int -> (forall d. Data d => d -> u) -> Fin n -> u
forall (n :: Nat) u.
KnownNat n =>
(forall d. Data d => d -> u) -> Fin n -> [u]
forall (n :: Nat) r r'.
KnownNat n =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Fin n -> r
forall (n :: Nat) r r'.
KnownNat n =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Fin n -> r
forall (n :: Nat) (m :: Type -> Type).
(KnownNat n, Monad m) =>
(forall d. Data d => d -> m d) -> Fin n -> m (Fin n)
forall (n :: Nat) (m :: Type -> Type).
(KnownNat n, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Fin n -> m (Fin n)
forall (n :: Nat) (c :: Type -> Type).
KnownNat n =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Fin n)
forall (n :: Nat) (c :: Type -> Type).
KnownNat n =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Fin n -> c (Fin n)
forall (n :: Nat) (t :: Type -> Type) (c :: Type -> Type).
(KnownNat n, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Fin n))
forall (n :: Nat) (t :: Type -> Type -> Type) (c :: Type -> Type).
(KnownNat n, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Fin n))
forall a.
Typeable a
-> (forall (c :: Type -> Type).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: Type -> Type).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: Type -> Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: Type -> Type).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall (c :: Type -> Type).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Fin n)
forall (c :: Type -> Type).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Fin n -> c (Fin n)
gmapMo :: forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Fin n -> m (Fin n)
$cgmapMo :: forall (n :: Nat) (m :: Type -> Type).
(KnownNat n, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Fin n -> m (Fin n)
gmapMp :: forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Fin n -> m (Fin n)
$cgmapMp :: forall (n :: Nat) (m :: Type -> Type).
(KnownNat n, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Fin n -> m (Fin n)
gmapM :: forall (m :: Type -> Type).
Monad m =>
(forall d. Data d => d -> m d) -> Fin n -> m (Fin n)
$cgmapM :: forall (n :: Nat) (m :: Type -> Type).
(KnownNat n, Monad m) =>
(forall d. Data d => d -> m d) -> Fin n -> m (Fin n)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Fin n -> u
$cgmapQi :: forall (n :: Nat) u.
KnownNat n =>
Int -> (forall d. Data d => d -> u) -> Fin n -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Fin n -> [u]
$cgmapQ :: forall (n :: Nat) u.
KnownNat n =>
(forall d. Data d => d -> u) -> Fin n -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Fin n -> r
$cgmapQr :: forall (n :: Nat) r r'.
KnownNat n =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Fin n -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Fin n -> r
$cgmapQl :: forall (n :: Nat) r r'.
KnownNat n =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Fin n -> r
gmapT :: (forall b. Data b => b -> b) -> Fin n -> Fin n
$cgmapT :: forall (n :: Nat).
KnownNat n =>
(forall b. Data b => b -> b) -> Fin n -> Fin n
dataCast2 :: forall (t :: Type -> Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Fin n))
$cdataCast2 :: forall (n :: Nat) (t :: Type -> Type -> Type) (c :: Type -> Type).
(KnownNat n, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Fin n))
dataCast1 :: forall (t :: Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Fin n))
$cdataCast1 :: forall (n :: Nat) (t :: Type -> Type) (c :: Type -> Type).
(KnownNat n, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Fin n))
dataTypeOf :: Fin n -> DataType
$cdataTypeOf :: forall (n :: Nat). KnownNat n => Fin n -> DataType
toConstr :: Fin n -> Constr
$ctoConstr :: forall (n :: Nat). KnownNat n => Fin n -> Constr
gunfold :: forall (c :: Type -> Type).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Fin n)
$cgunfold :: forall (n :: Nat) (c :: Type -> Type).
KnownNat n =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Fin n)
gfoldl :: forall (c :: Type -> Type).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Fin n -> c (Fin n)
$cgfoldl :: forall (n :: Nat) (c :: Type -> Type).
KnownNat n =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Fin n -> c (Fin n)
Data)
deriving newtype (Int -> Fin n -> ShowS
[Fin n] -> ShowS
Fin n -> String
forall (n :: Nat). Int -> Fin n -> ShowS
forall (n :: Nat). [Fin n] -> ShowS
forall (n :: Nat). Fin n -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Fin n] -> ShowS
$cshowList :: forall (n :: Nat). [Fin n] -> ShowS
show :: Fin n -> String
$cshow :: forall (n :: Nat). Fin n -> String
showsPrec :: Int -> Fin n -> ShowS
$cshowsPrec :: forall (n :: Nat). Int -> Fin n -> ShowS
Show, [Fin n] -> Portrayal
Fin n -> Portrayal
forall (n :: Nat). [Fin n] -> Portrayal
forall (n :: Nat). Fin n -> Portrayal
forall a. (a -> Portrayal) -> ([a] -> Portrayal) -> Portray a
portrayList :: [Fin n] -> Portrayal
$cportrayList :: forall (n :: Nat). [Fin n] -> Portrayal
portray :: Fin n -> Portrayal
$cportray :: forall (n :: Nat). Fin n -> Portrayal
Portray, Fin n -> Fin n -> Maybe Portrayal
forall (n :: Nat). Fin n -> Fin n -> Maybe Portrayal
forall a. (a -> a -> Maybe Portrayal) -> Diff a
diff :: Fin n -> Fin n -> Maybe Portrayal
$cdiff :: forall (n :: Nat). Fin n -> Fin n -> Maybe Portrayal
Diff)
type role Fin nominal
type FinSize n = (KnownNat n, 1 <= n)
instance KnownNat n => Read (Fin n) where
readsPrec :: Int -> ReadS (Fin n)
readsPrec Int
p String
s =
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\ (Integer
x, String
s') -> (,String
s') forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (n :: Nat). Integral a => SInt n -> a -> Maybe (Fin n)
tryFin forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal Integer
x) forall a b. (a -> b) -> a -> b
$
forall a. Read a => Int -> ReadS a
readsPrec @Integer Int
p String
s
instance FinSize n => Arbitrary (Fin n) where
arbitrary :: Gen (Fin n)
arbitrary = forall a. (Bounded a, Enum a) => Gen a
arbitraryBoundedEnum
instance NFData (Fin n) where rnf :: Fin n -> ()
rnf (Fin Int
x) = forall a. NFData a => a -> ()
rnf Int
x
#if MIN_VERSION_attenuation(0,2,0)
instance Attenuable (Fin n) Int
instance m <= n => Attenuable (Fin m) (Fin n)
#endif
{-# INLINE fin #-}
fin :: HasCallStack => SInt n -> Int -> Fin n
fin :: forall (n :: Nat). HasCallStack => SInt n -> Int -> Fin n
fin (forall (n :: Nat). SInt n -> Int
unSInt -> !Int
n) Int
i
| Int
i forall a. Ord a => a -> a -> Bool
< Int
0 = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Fin: number out of range " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
" < 0"
| Int
i forall a. Ord a => a -> a -> Bool
>= Int
n = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Fin: number out of range " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
" >= " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n
| Bool
otherwise = forall (n :: Nat). Int -> Fin n
Fin Int
i
{-# INLINE finFromIntegral #-}
finFromIntegral
:: (HasCallStack, Integral a, Show a)
=> SInt n -> a -> Fin n
finFromIntegral :: forall a (n :: Nat).
(HasCallStack, Integral a, Show a) =>
SInt n -> a -> Fin n
finFromIntegral SInt n
n =
forall (n :: Nat). HasCallStack => SInt n -> Int -> Fin n
fin SInt n
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral
{-# INLINE ufin #-}
ufin :: HasCallStack => SInt n -> FinRep -> Fin n
ufin :: forall (n :: Nat). HasCallStack => SInt n -> Int -> Fin n
ufin SInt n
sn Int
i
| Int
i forall a. Ord a => a -> a -> Bool
>= Int
n = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Fin: number out of range " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
" >= " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n
| Bool
otherwise = forall (n :: Nat). Int -> Fin n
Fin Int
i
where
n :: Int
n = forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn
knownFin :: (i <= n - 1) => SInt i -> Fin n
knownFin :: forall (i :: Nat) (n :: Nat). (i <= (n - 1)) => SInt i -> Fin n
knownFin = forall a (n :: Nat). Integral a => a -> Fin n
unsafeFin forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). SInt n -> Int
unSInt
{-# INLINE knownFin #-}
{-# INLINE unsafeFin #-}
unsafeFin :: Integral a => a -> Fin n
unsafeFin :: forall a (n :: Nat). Integral a => a -> Fin n
unsafeFin = forall (n :: Nat). Int -> Fin n
Fin forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral
tryFin :: Integral a => SInt n -> a -> Maybe (Fin n)
tryFin :: forall a (n :: Nat). Integral a => SInt n -> a -> Maybe (Fin n)
tryFin SInt n
n a
x =
if a
x forall a. Ord a => a -> a -> Bool
>= a
0 Bool -> Bool -> Bool
&& a
x forall a. Ord a => a -> a -> Bool
< forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (n :: Nat). SInt n -> Int
unSInt SInt n
n)
then forall a. a -> Maybe a
Just (forall (n :: Nat). Int -> Fin n
Fin (forall a b. (Integral a, Num b) => a -> b
fromIntegral a
x))
else forall a. Maybe a
Nothing
finMod :: forall n a . (HasCallStack, Integral a) => SInt n -> a -> Fin n
finMod :: forall (n :: Nat) a.
(HasCallStack, Integral a) =>
SInt n -> a -> Fin n
finMod SInt n
n = forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat) a.
(HasCallStack, Integral a) =>
SInt n -> a -> (a, Fin n)
finDivMod SInt n
n
finDivMod
:: forall n a
. (HasCallStack, Integral a)
=> SInt n -> a -> (a, Fin n)
finDivMod :: forall (n :: Nat) a.
(HasCallStack, Integral a) =>
SInt n -> a -> (a, Fin n)
finDivMod SInt n
sn a
x
| Integer
n forall a. Eq a => a -> a -> Bool
== Integer
0 = forall a. HasCallStack => String -> a
error String
"finDivMod: zero modulus."
| Bool
otherwise = (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
d, forall (n :: Nat). Int -> Fin n
Fin (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
m))
where
(Integer
d, Integer
m) = forall a. Integral a => a -> a -> (a, a)
divMod (forall a b. (Integral a, Num b) => a -> b
fromIntegral a
x :: Integer) Integer
n
n :: Integer
n = forall a. Integral a => a -> Integer
toInteger forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn
complementFin :: SInt n -> Fin n -> Fin n
complementFin :: forall (n :: Nat). SInt n -> Fin n -> Fin n
complementFin SInt n
sn Fin n
x = forall a (n :: Nat). Integral a => a -> Fin n
unsafeFin (forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn forall a. Num a => a -> a -> a
- Int
1 forall a. Num a => a -> a -> a
- forall (n :: Nat). Fin n -> Int
finToInt Fin n
x)
finToInt :: Fin n -> Int
finToInt :: forall (n :: Nat). Fin n -> Int
finToInt (Fin Int
i) = Int
i
{-# INLINE finToInt #-}
twice :: SInt n -> Fin n -> Fin n
twice :: forall (n :: Nat). SInt n -> Fin n -> Fin n
twice SInt n
sn (Fin Int
i) = forall (n :: Nat). HasCallStack => SInt n -> Int -> Fin n
ufin SInt n
sn forall a b. (a -> b) -> a -> b
$ Int
i forall a. Num a => a -> a -> a
* Int
2
half :: Fin n -> Fin n
half :: forall (n :: Nat). Fin n -> Fin n
half (Fin Int
n) = forall (n :: Nat). Int -> Fin n
Fin (Int
n forall a. Integral a => a -> a -> a
`quot` Int
2)
quarter :: Fin n -> Fin n
quarter :: forall (n :: Nat). Fin n -> Fin n
quarter (Fin Int
n) = forall (n :: Nat). Int -> Fin n
Fin (Int
n forall a. Integral a => a -> a -> a
`quot` Int
4)
unsafePred :: Fin n -> Fin n
unsafePred :: forall (n :: Nat). Fin n -> Fin n
unsafePred (Fin Int
x) = forall (n :: Nat). Int -> Fin n
Fin (Int
x forall a. Num a => a -> a -> a
- Int
1)
{-# INLINE unsafePred #-}
unsafeSucc :: Fin n -> Fin n
unsafeSucc :: forall (n :: Nat). Fin n -> Fin n
unsafeSucc (Fin Int
x) = forall (n :: Nat). Int -> Fin n
Fin (Int
x forall a. Num a => a -> a -> a
+ Int
1)
{-# INLINE unsafeSucc #-}
enumFin :: SInt n -> [Fin n]
enumFin :: forall (n :: Nat). SInt n -> [Fin n]
enumFin SInt n
sn = forall a b. (a -> b) -> [a] -> [b]
map coerce :: forall a b. Coercible a b => a -> b
coerce [Int
0 .. forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn forall a. Num a => a -> a -> a
- Int
1]
{-# INLINE enumFin #-}
enumFinDown :: SInt n -> [Fin n]
enumFinDown :: forall (n :: Nat). SInt n -> [Fin n]
enumFinDown SInt n
sn = forall a b. (a -> b) -> [a] -> [b]
map coerce :: forall a b. Coercible a b => a -> b
coerce [forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn forall a. Num a => a -> a -> a
- Int
1, forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn forall a. Num a => a -> a -> a
- Int
2 .. Int
0]
{-# INLINE enumFinDown #-}
enumDownFrom :: SInt n -> Fin n -> [Fin n]
enumDownFrom :: forall (n :: Nat). SInt n -> Fin n -> [Fin n]
enumDownFrom SInt n
_sn (Fin Int
x) = forall a b. (a -> b) -> [a] -> [b]
map coerce :: forall a b. Coercible a b => a -> b
coerce [Int
x, Int
x forall a. Num a => a -> a -> a
- Int
1 .. Int
0]
{-# INLINE enumDownFrom #-}
enumDownTo :: SInt n -> Fin n -> [Fin n]
enumDownTo :: forall (n :: Nat). SInt n -> Fin n -> [Fin n]
enumDownTo SInt n
sn (Fin Int
x) = forall a b. (a -> b) -> [a] -> [b]
map coerce :: forall a b. Coercible a b => a -> b
coerce [forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn forall a. Num a => a -> a -> a
- Int
1, forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn forall a. Num a => a -> a -> a
- Int
2 .. Int
x]
{-# INLINE enumDownTo #-}
enumDownFromTo :: SInt n -> Fin n -> Fin n -> [Fin n]
enumDownFromTo :: forall (n :: Nat). SInt n -> Fin n -> Fin n -> [Fin n]
enumDownFromTo SInt n
_sn (Fin Int
x) (Fin Int
y) = forall a b. (a -> b) -> [a] -> [b]
map coerce :: forall a b. Coercible a b => a -> b
coerce [Int
x, Int
x forall a. Num a => a -> a -> a
- Int
1 .. Int
y]
{-# INLINE enumDownFromTo #-}
instance KnownNat n => Enum (Fin n) where
pred :: Fin n -> Fin n
pred (Fin Int
x)
| Int
x forall a. Ord a => a -> a -> Bool
> Int
0 = forall (n :: Nat). Int -> Fin n
Fin (Int
x forall a. Num a => a -> a -> a
- Int
1)
| Bool
otherwise = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$
String
"pred @(Fin " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (n :: Nat). SInt n -> Int
unSInt @n forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal) forall a. [a] -> [a] -> [a]
++
String
"): no predecessor of 0"
succ :: Fin n -> Fin n
succ (Fin Int
x)
| Int
x forall a. Ord a => a -> a -> Bool
< Int
n forall a. Num a => a -> a -> a
- Int
1 = forall (n :: Nat). Int -> Fin n
Fin (Int
x forall a. Num a => a -> a -> a
+ Int
1)
| Bool
otherwise = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$
String
"succ @(Fin " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n forall a. [a] -> [a] -> [a]
++ String
"): no successor of " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n
where !n :: Int
n = forall (n :: Nat). SInt n -> Int
unSInt @n forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
toEnum :: Int -> Fin n
toEnum = forall (n :: Nat). HasCallStack => SInt n -> Int -> Fin n
fin forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
fromEnum :: Fin n -> Int
fromEnum = forall (n :: Nat). Fin n -> Int
finToInt
enumFrom :: Fin n -> [Fin n]
enumFrom (Fin Int
x) =
forall a b. (a -> b) -> [a] -> [b]
map coerce :: forall a b. Coercible a b => a -> b
coerce [Int
x .. forall (n :: Nat). SInt n -> Int
unSInt @n forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal forall a. Num a => a -> a -> a
- Int
1]
enumFromThen :: Fin n -> Fin n -> [Fin n]
enumFromThen (Fin Int
x) (Fin Int
y) =
forall a b. (a -> b) -> [a] -> [b]
map coerce :: forall a b. Coercible a b => a -> b
coerce [Int
x, Int
y .. forall (n :: Nat). SInt n -> Int
unSInt @n forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal forall a. Num a => a -> a -> a
- Int
1]
enumFromTo :: Fin n -> Fin n -> [Fin n]
enumFromTo (Fin Int
x) (Fin Int
z) = forall a b. (a -> b) -> [a] -> [b]
map coerce :: forall a b. Coercible a b => a -> b
coerce [Int
x .. Int
z]
enumFromThenTo :: Fin n -> Fin n -> Fin n -> [Fin n]
enumFromThenTo (Fin Int
x) (Fin Int
y) (Fin Int
z) = forall a b. (a -> b) -> [a] -> [b]
map coerce :: forall a b. Coercible a b => a -> b
coerce [Int
x, Int
y .. Int
z]
{-# INLINE pred #-}
{-# INLINE succ #-}
{-# INLINE toEnum #-}
{-# INLINE fromEnum #-}
{-# INLINE enumFrom #-}
{-# INLINE enumFromThen #-}
{-# INLINE enumFromTo #-}
{-# INLINE enumFromThenTo #-}
minFin :: 1 <= n => Fin n
minFin :: forall (n :: Nat). (1 <= n) => Fin n
minFin = forall (n :: Nat). Int -> Fin n
Fin Int
0
maxFin :: 1 <= n => SInt n -> Fin n
maxFin :: forall (n :: Nat). (1 <= n) => SInt n -> Fin n
maxFin SInt n
sn = forall (n :: Nat). Int -> Fin n
Fin (forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn forall a. Num a => a -> a -> a
- Int
1)
instance FinSize n => Bounded (Fin n) where
minBound :: Fin n
minBound = forall (n :: Nat). (1 <= n) => Fin n
minFin
maxBound :: Fin n
maxBound = forall (n :: Nat). (1 <= n) => SInt n -> Fin n
maxFin forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
{-# INLINE minBound #-}
{-# INLINE maxBound #-}
instance KnownNat n => Default (Fin n) where
def :: Fin n
def = forall (n :: Nat). HasCallStack => SInt n -> Int -> Fin n
fin forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal (Int
0 :: FinRep)
overflowedError
:: forall n a
. HasCallStack
=> SInt n -> String -> Fin n -> Fin n -> a
overflowedError :: forall (n :: Nat) a.
HasCallStack =>
SInt n -> String -> Fin n -> Fin n -> a
overflowedError SInt n
sn String
nm Fin n
x Fin n
y = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$
String -> ShowS
showString String
nm forall b c a. (b -> c) -> (a -> b) -> a -> c
.
String -> ShowS
showString String
" @" forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall a. Show a => a -> ShowS
shows (forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
String -> ShowS
showString String
" " forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall a. Show a => a -> ShowS
shows Fin n
x forall b c a. (b -> c) -> (a -> b) -> a -> c
.
String -> ShowS
showString String
" " forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall a. Show a => a -> ShowS
shows Fin n
y forall a b. (a -> b) -> a -> b
$
String
" overflowed FinRep."
outOfRangeError
:: forall n a
. HasCallStack
=> SInt n -> String -> Fin n -> Fin n -> FinRep -> a
outOfRangeError :: forall (n :: Nat) a.
HasCallStack =>
SInt n -> String -> Fin n -> Fin n -> Int -> a
outOfRangeError SInt n
sn String
nm Fin n
x Fin n
y Int
r = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$
String -> ShowS
showString String
nm forall b c a. (b -> c) -> (a -> b) -> a -> c
.
String -> ShowS
showString String
" @" forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall a. Show a => a -> ShowS
shows (forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
String -> ShowS
showString String
" " forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall a. Show a => a -> ShowS
shows Fin n
x forall b c a. (b -> c) -> (a -> b) -> a -> c
.
String -> ShowS
showString String
" " forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall a. Show a => a -> ShowS
shows Fin n
y forall b c a. (b -> c) -> (a -> b) -> a -> c
.
String -> ShowS
showString String
" = " forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall a. Show a => a -> ShowS
shows Int
r forall a b. (a -> b) -> a -> b
$
String
" out of range."
add_ :: SInt n -> Fin n -> Fin n -> Maybe (Bool, FinRep)
add_ :: forall (n :: Nat). SInt n -> Fin n -> Fin n -> Maybe (Bool, Int)
add_ SInt n
sn = \ (Fin Int
x) (Fin Int
y) ->
let z :: Int
z = Int
x forall a. Num a => a -> a -> a
+ Int
y
in if Int
z forall a. Ord a => a -> a -> Bool
< Int
x
then forall a. Maybe a
Nothing
else forall a. a -> Maybe a
Just (Int
z forall a. Ord a => a -> a -> Bool
< forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn, Int
z)
{-# INLINE add_ #-}
sub_ :: Fin n -> Fin n -> Maybe (Bool, FinRep)
sub_ :: forall (n :: Nat). Fin n -> Fin n -> Maybe (Bool, Int)
sub_ = \ (Fin Int
x) (Fin Int
y) -> let z :: Int
z = Int
x forall a. Num a => a -> a -> a
- Int
y in forall a. a -> Maybe a
Just (Int
z forall a. Ord a => a -> a -> Bool
>= Int
0, Int
z)
{-# INLINE sub_ #-}
mul_ :: SInt n -> Fin n -> Fin n -> Maybe (Bool, FinRep)
mul_ :: forall (n :: Nat). SInt n -> Fin n -> Fin n -> Maybe (Bool, Int)
mul_ SInt n
sn = \ (Fin Int
x) (Fin Int
y) ->
let z :: Int
z = Int
x forall a. Num a => a -> a -> a
* Int
y
in if Int
x forall a. Eq a => a -> a -> Bool
/= Int
0 Bool -> Bool -> Bool
&& Int
z forall a. Integral a => a -> a -> a
`div` Int
x forall a. Eq a => a -> a -> Bool
/= Int
y
then forall a. Maybe a
Nothing
else forall a. a -> Maybe a
Just (Int
z forall a. Ord a => a -> a -> Bool
< forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn, Int
z)
{-# INLINE mul_ #-}
mkMod
:: HasCallStack
=> SInt n
-> String
-> (Fin n -> Fin n -> Maybe (Bool, FinRep)) -> Fin n -> Fin n -> Fin n
mkMod :: forall (n :: Nat).
HasCallStack =>
SInt n
-> String
-> (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n
-> Fin n
-> Fin n
mkMod SInt n
sn String
nm Fin n -> Fin n -> Maybe (Bool, Int)
op = \ Fin n
x Fin n
y -> case Fin n
x Fin n -> Fin n -> Maybe (Bool, Int)
`op` Fin n
y of
Just (Bool
_ok, Int
z) -> forall (n :: Nat) a.
(HasCallStack, Integral a) =>
SInt n -> a -> Fin n
finMod SInt n
sn Int
z
Maybe (Bool, Int)
Nothing -> forall (n :: Nat) a.
HasCallStack =>
SInt n -> String -> Fin n -> Fin n -> a
overflowedError SInt n
sn String
nm Fin n
x Fin n
y
{-# INLINE mkMod #-}
modAdd :: HasCallStack => SInt n -> Fin n -> Fin n -> Fin n
modAdd :: forall (n :: Nat).
HasCallStack =>
SInt n -> Fin n -> Fin n -> Fin n
modAdd SInt n
sn = forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack forall (n :: Nat).
HasCallStack =>
SInt n
-> String
-> (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n
-> Fin n
-> Fin n
mkMod SInt n
sn String
"modAdd" (forall (n :: Nat). SInt n -> Fin n -> Fin n -> Maybe (Bool, Int)
add_ SInt n
sn)
{-# INLINEABLE modAdd #-}
modSub :: SInt n -> Fin n -> Fin n -> Fin n
modSub :: forall (n :: Nat). SInt n -> Fin n -> Fin n -> Fin n
modSub SInt n
sn = forall (n :: Nat).
HasCallStack =>
SInt n
-> String
-> (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n
-> Fin n
-> Fin n
mkMod SInt n
sn String
"modSub" forall (n :: Nat). Fin n -> Fin n -> Maybe (Bool, Int)
sub_
{-# INLINEABLE modSub #-}
modMul :: HasCallStack => SInt n -> Fin n -> Fin n -> Fin n
modMul :: forall (n :: Nat).
HasCallStack =>
SInt n -> Fin n -> Fin n -> Fin n
modMul SInt n
sn = forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack forall (n :: Nat).
HasCallStack =>
SInt n
-> String
-> (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n
-> Fin n
-> Fin n
mkMod SInt n
sn String
"modMul" (forall (n :: Nat). SInt n -> Fin n -> Fin n -> Maybe (Bool, Int)
mul_ SInt n
sn)
{-# INLINEABLE modMul #-}
modNegate :: SInt n -> Fin n -> Fin n
modNegate :: forall (n :: Nat). SInt n -> Fin n -> Fin n
modNegate SInt n
_ (Fin Int
0) = forall (n :: Nat). Int -> Fin n
Fin Int
0
modNegate SInt n
sn (Fin Int
x) = forall (n :: Nat). Int -> Fin n
Fin (forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn forall a. Num a => a -> a -> a
- Int
x)
mkTry
:: (Fin n -> Fin n -> Maybe (Bool, FinRep))
-> Fin n -> Fin n -> Maybe (Fin n)
mkTry :: forall (n :: Nat).
(Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n -> Fin n -> Maybe (Fin n)
mkTry Fin n -> Fin n -> Maybe (Bool, Int)
op = \Fin n
x Fin n
y -> case Fin n -> Fin n -> Maybe (Bool, Int)
op Fin n
x Fin n
y of
Just (Bool
True, Int
z) -> forall a. a -> Maybe a
Just (forall (n :: Nat). Int -> Fin n
Fin Int
z)
Maybe (Bool, Int)
_ -> forall a. Maybe a
Nothing
{-# INLINE mkTry #-}
tryAdd :: SInt n -> Fin n -> Fin n -> Maybe (Fin n)
tryAdd :: forall (n :: Nat). SInt n -> Fin n -> Fin n -> Maybe (Fin n)
tryAdd = forall (n :: Nat).
(Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n -> Fin n -> Maybe (Fin n)
mkTry forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). SInt n -> Fin n -> Fin n -> Maybe (Bool, Int)
add_
{-# INLINEABLE tryAdd #-}
trySub :: Fin n -> Fin n -> Maybe (Fin n)
trySub :: forall (n :: Nat). Fin n -> Fin n -> Maybe (Fin n)
trySub = forall (n :: Nat).
(Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n -> Fin n -> Maybe (Fin n)
mkTry forall (n :: Nat). Fin n -> Fin n -> Maybe (Bool, Int)
sub_
{-# INLINEABLE trySub #-}
tryMul :: SInt n -> Fin n -> Fin n -> Maybe (Fin n)
tryMul :: forall (n :: Nat). SInt n -> Fin n -> Fin n -> Maybe (Fin n)
tryMul = forall (n :: Nat).
(Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n -> Fin n -> Maybe (Fin n)
mkTry forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). SInt n -> Fin n -> Fin n -> Maybe (Bool, Int)
mul_
{-# INLINEABLE tryMul #-}
divModFin :: SInt m -> Fin (d * m) -> (Fin d, Fin m)
divModFin :: forall (m :: Nat) (d :: Nat).
SInt m -> Fin (d * m) -> (Fin d, Fin m)
divModFin SInt m
sm (Fin Int
x) = (forall (n :: Nat). Int -> Fin n
Fin Int
d, forall (n :: Nat). Int -> Fin n
Fin Int
r)
where
(Int
d, Int
r) = forall a. Integral a => a -> a -> (a, a)
divMod Int
x (forall (n :: Nat). SInt n -> Int
unSInt SInt m
sm)
{-# INLINEABLE divModFin #-}
mkChk
:: HasCallStack
=> SInt n
-> String
-> (Fin n -> Fin n -> Maybe (Bool, FinRep))
-> Fin n -> Fin n -> Fin n
mkChk :: forall (n :: Nat).
HasCallStack =>
SInt n
-> String
-> (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n
-> Fin n
-> Fin n
mkChk SInt n
sn String
nm Fin n -> Fin n -> Maybe (Bool, Int)
op = \Fin n
x Fin n
y -> case Fin n -> Fin n -> Maybe (Bool, Int)
op Fin n
x Fin n
y of
Just (Bool
ok, Int
z) -> if Bool
ok then forall (n :: Nat). Int -> Fin n
Fin Int
z else forall (n :: Nat) a.
HasCallStack =>
SInt n -> String -> Fin n -> Fin n -> Int -> a
outOfRangeError SInt n
sn String
nm Fin n
x Fin n
y Int
z
Maybe (Bool, Int)
Nothing -> forall (n :: Nat) a.
HasCallStack =>
SInt n -> String -> Fin n -> Fin n -> a
overflowedError SInt n
sn String
nm Fin n
x Fin n
y
{-# INLINE mkChk #-}
chkAdd :: HasCallStack => SInt n -> Fin n -> Fin n -> Fin n
chkAdd :: forall (n :: Nat).
HasCallStack =>
SInt n -> Fin n -> Fin n -> Fin n
chkAdd SInt n
sn = forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack forall (n :: Nat).
HasCallStack =>
SInt n
-> String
-> (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n
-> Fin n
-> Fin n
mkChk SInt n
sn String
"chkAdd" (forall (n :: Nat). SInt n -> Fin n -> Fin n -> Maybe (Bool, Int)
add_ SInt n
sn)
{-# INLINEABLE chkAdd #-}
chkSub :: HasCallStack => SInt n -> Fin n -> Fin n -> Fin n
chkSub :: forall (n :: Nat).
HasCallStack =>
SInt n -> Fin n -> Fin n -> Fin n
chkSub SInt n
sn = forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack forall (n :: Nat).
HasCallStack =>
SInt n
-> String
-> (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n
-> Fin n
-> Fin n
mkChk SInt n
sn String
"chkSub" forall (n :: Nat). Fin n -> Fin n -> Maybe (Bool, Int)
sub_
{-# INLINEABLE chkSub #-}
chkMul :: HasCallStack => SInt n -> Fin n -> Fin n -> Fin n
chkMul :: forall (n :: Nat).
HasCallStack =>
SInt n -> Fin n -> Fin n -> Fin n
chkMul SInt n
sn = forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack forall (n :: Nat).
HasCallStack =>
SInt n
-> String
-> (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n
-> Fin n
-> Fin n
mkChk SInt n
sn String
"chkMul" (forall (n :: Nat). SInt n -> Fin n -> Fin n -> Maybe (Bool, Int)
mul_ SInt n
sn)
{-# INLINEABLE chkMul #-}
attLT :: (n <= m) => Attenuation (Fin n) (Fin m)
attLT :: forall (m :: Nat) (n :: Nat).
(m <= n) =>
Attenuation (Fin m) (Fin n)
attLT = forall {k} (a :: k) (b :: k). Coercible a b => Attenuation a b
coercible
attPlus :: Attenuation (Fin n) (Fin (n + k))
attPlus :: forall (n :: Nat) (k :: Nat). Attenuation (Fin n) (Fin (n + k))
attPlus = forall {k} (a :: k) (b :: k). Coercible a b => Attenuation a b
coercible
attMinus :: Attenuation (Fin (n - k)) (Fin n)
attMinus :: forall (n :: Nat) (k :: Nat). Attenuation (Fin (n - k)) (Fin n)
attMinus = forall {k} (a :: k) (b :: k). Coercible a b => Attenuation a b
coercible
attInt :: Attenuation (Fin n) Int
attInt :: forall (n :: Nat). Attenuation (Fin n) Int
attInt = forall {k} (a :: k) (b :: k). Coercible a b => Attenuation a b
coercible
unsafeCoFin :: Coercion (Fin n) (Fin m)
unsafeCoFin :: forall (n :: Nat) (m :: Nat). Coercion (Fin n) (Fin m)
unsafeCoFin = forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
unsafeCoInt :: Coercion (Fin n) Int
unsafeCoInt :: forall (n :: Nat). Coercion (Fin n) Int
unsafeCoInt = forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
weaken :: Fin n -> Fin (n+1)
weaken :: forall (n :: Nat). Fin n -> Fin (n + 1)
weaken (Fin Int
x) = forall (n :: Nat). Int -> Fin n
Fin Int
x
strengthen :: SInt n -> Fin (n+1) -> Maybe (Fin n)
strengthen :: forall (n :: Nat). SInt n -> Fin (n + 1) -> Maybe (Fin n)
strengthen SInt n
sn (Fin Int
x) = if Int
x forall a. Eq a => a -> a -> Bool
== forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn then forall a. Maybe a
Nothing else forall a. a -> Maybe a
Just (forall (n :: Nat). Int -> Fin n
Fin Int
x)
shiftFin :: SInt m -> Fin n -> Fin (m+n)
shiftFin :: forall (m :: Nat) (n :: Nat). SInt m -> Fin n -> Fin (m + n)
shiftFin SInt m
sm (Fin Int
x) = forall (n :: Nat). Int -> Fin n
Fin (forall (n :: Nat). SInt n -> Int
unSInt SInt m
sm forall a. Num a => a -> a -> a
+ Int
x)
tryUnshiftFin :: SInt m -> SInt n -> Fin (m+n) -> Maybe (Fin n)
tryUnshiftFin :: forall (m :: Nat) (n :: Nat).
SInt m -> SInt n -> Fin (m + n) -> Maybe (Fin n)
tryUnshiftFin SInt m
sm SInt n
sn (Fin Int
x) = forall a (n :: Nat). Integral a => SInt n -> a -> Maybe (Fin n)
tryFin SInt n
sn (Int
x forall a. Num a => a -> a -> a
- forall (n :: Nat). SInt n -> Int
unSInt SInt m
sm)
unshiftFin :: HasCallStack => SInt m -> SInt n -> Fin (m+n) -> Fin n
unshiftFin :: forall (m :: Nat) (n :: Nat).
HasCallStack =>
SInt m -> SInt n -> Fin (m + n) -> Fin n
unshiftFin SInt m
sm SInt n
sn (Fin Int
x) = forall (n :: Nat). HasCallStack => SInt n -> Int -> Fin n
fin SInt n
sn (Int
x forall a. Num a => a -> a -> a
- forall (n :: Nat). SInt n -> Int
unSInt SInt m
sm)
splitFin :: SInt m -> Fin (m + n) -> Either (Fin m) (Fin n)
splitFin :: forall (m :: Nat) (n :: Nat).
SInt m -> Fin (m + n) -> Either (Fin m) (Fin n)
splitFin SInt m
sm (Fin Int
x)
| Int
x forall a. Ord a => a -> a -> Bool
< forall (n :: Nat). SInt n -> Int
unSInt SInt m
sm = forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). Int -> Fin n
Fin Int
x
| Bool
otherwise = forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). Int -> Fin n
Fin (Int
x forall a. Num a => a -> a -> a
- forall (n :: Nat). SInt n -> Int
unSInt SInt m
sm)
concatFin :: SInt m -> Either (Fin m) (Fin n) -> Fin (m + n)
concatFin :: forall (m :: Nat) (n :: Nat).
SInt m -> Either (Fin m) (Fin n) -> Fin (m + n)
concatFin SInt m
sm Either (Fin m) (Fin n)
e = case Either (Fin m) (Fin n)
e of
Left (Fin Int
x) -> forall (n :: Nat). Int -> Fin n
Fin Int
x
Right Fin n
x -> forall (m :: Nat) (n :: Nat). SInt m -> Fin n -> Fin (m + n)
shiftFin SInt m
sm Fin n
x
{-# INLINE embed #-}
embed :: (m <= n) => Fin m -> Fin n
embed :: forall (m :: Nat) (n :: Nat). (m <= n) => Fin m -> Fin n
embed (Fin Int
i) = forall (n :: Nat). Int -> Fin n
Fin Int
i
{-# INLINE unembed #-}
unembed :: HasCallStack => SInt n -> Fin m -> Fin n
unembed :: forall (n :: Nat) (m :: Nat).
HasCallStack =>
SInt n -> Fin m -> Fin n
unembed SInt n
sn (Fin Int
i) = forall (n :: Nat). HasCallStack => SInt n -> Int -> Fin n
ufin SInt n
sn Int
i
tryUnembed :: SInt n -> Fin m -> Maybe (Fin n)
tryUnembed :: forall (n :: Nat) (m :: Nat). SInt n -> Fin m -> Maybe (Fin n)
tryUnembed SInt n
sn (Fin Int
i) = forall a (n :: Nat). Integral a => SInt n -> a -> Maybe (Fin n)
tryFin SInt n
sn Int
i
crossFin :: SInt n -> Fin m -> Fin n -> Fin (m * n)
crossFin :: forall (n :: Nat) (m :: Nat).
SInt n -> Fin m -> Fin n -> Fin (m * n)
crossFin SInt n
sn (Fin Int
x) (Fin Int
y) = forall (n :: Nat). Int -> Fin n
Fin (Int
x forall a. Num a => a -> a -> a
* forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn forall a. Num a => a -> a -> a
+ Int
y)