{-# 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 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
(Fin n -> Fin n -> Bool) -> (Fin n -> Fin n -> Bool) -> Eq (Fin n)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
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
Eq, Eq (Fin n)
Eq (Fin n)
-> (Fin n -> Fin n -> Ordering)
-> (Fin n -> Fin n -> Bool)
-> (Fin n -> Fin n -> Bool)
-> (Fin n -> Fin n -> Bool)
-> (Fin n -> Fin n -> Bool)
-> (Fin n -> Fin n -> Fin n)
-> (Fin n -> Fin n -> Fin n)
-> Ord (Fin n)
Fin n -> Fin n -> Bool
Fin n -> Fin n -> Ordering
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
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
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
$cp1Ord :: forall (n :: Nat). Eq (Fin n)
Ord, Typeable (Fin n)
DataType
Constr
Typeable (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))
-> (forall (c :: Type -> Type).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Fin n))
-> (Fin n -> Constr)
-> (Fin n -> DataType)
-> (forall (t :: Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Fin n)))
-> (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)))
-> ((forall b. Data b => b -> b) -> Fin n -> Fin n)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Fin n -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Fin n -> r)
-> (forall u. (forall d. Data d => d -> u) -> Fin n -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Fin n -> u)
-> (forall (m :: Type -> Type).
Monad m =>
(forall d. Data d => d -> m d) -> Fin n -> m (Fin n))
-> (forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Fin n -> m (Fin n))
-> (forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Fin n -> m (Fin n))
-> Data (Fin n)
Fin n -> DataType
Fin n -> Constr
(forall b. Data b => b -> b) -> Fin n -> Fin n
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Fin n -> c (Fin n)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> 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 u. Int -> (forall d. Data d => d -> u) -> Fin n -> u
forall u. (forall d. Data d => d -> u) -> Fin n -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Fin n -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Fin n -> r
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 (m :: Type -> Type).
Monad m =>
(forall d. Data d => d -> m d) -> Fin n -> m (Fin n)
forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Fin n -> m (Fin n)
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)
forall (t :: Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Fin n))
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))
$cFin :: Constr
$tFin :: DataType
gmapMo :: (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 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 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 :: 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 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 :: (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 :: (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 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 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 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 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)
$cp1Data :: forall (n :: Nat). KnownNat n => Typeable (Fin n)
Data)
deriving newtype (Int -> Fin n -> ShowS
[Fin n] -> ShowS
Fin n -> String
(Int -> Fin n -> ShowS)
-> (Fin n -> String) -> ([Fin n] -> ShowS) -> Show (Fin n)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (n :: Nat). Int -> Fin n -> ShowS
forall (n :: Nat). [Fin n] -> ShowS
forall (n :: Nat). Fin n -> String
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
(Fin n -> Portrayal) -> ([Fin n] -> Portrayal) -> Portray (Fin n)
forall a. (a -> Portrayal) -> ([a] -> Portrayal) -> Portray a
forall (n :: Nat). [Fin n] -> Portrayal
forall (n :: Nat). Fin n -> Portrayal
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
(Fin n -> Fin n -> Maybe Portrayal) -> Diff (Fin n)
forall a. (a -> a -> Maybe Portrayal) -> Diff a
forall (n :: Nat). Fin n -> Fin n -> Maybe Portrayal
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 =
((Integer, String) -> Maybe (Fin n, String))
-> [(Integer, String)] -> [(Fin n, String)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\ (Integer
x, String
s') -> (,String
s') (Fin n -> (Fin n, String))
-> Maybe (Fin n) -> Maybe (Fin n, String)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SInt n -> Integer -> Maybe (Fin n)
forall a (n :: Nat). Integral a => SInt n -> a -> Maybe (Fin n)
tryFin SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal Integer
x) ([(Integer, String)] -> [(Fin n, String)])
-> [(Integer, String)] -> [(Fin n, String)]
forall a b. (a -> b) -> a -> b
$
Int -> ReadS Integer
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 = Gen (Fin n)
forall a. (Bounded a, Enum a) => Gen a
arbitraryBoundedEnum
instance NFData (Fin n) where rnf :: Fin n -> ()
rnf (Fin Int
x) = Int -> ()
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 :: SInt n -> Int -> Fin n
fin (SInt n -> Int
forall (n :: Nat). SInt n -> Int
unSInt -> !Int
n) Int
i
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 = String -> Fin n
forall a. HasCallStack => String -> a
error (String -> Fin n) -> String -> Fin n
forall a b. (a -> b) -> a -> b
$ String
"Fin: number out of range " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" < 0"
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n = String -> Fin n
forall a. HasCallStack => String -> a
error (String -> Fin n) -> String -> Fin n
forall a b. (a -> b) -> a -> b
$ String
"Fin: number out of range " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" >= " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n
| Bool
otherwise = Int -> Fin n
forall (n :: Nat). Int -> Fin n
Fin Int
i
{-# INLINE finFromIntegral #-}
finFromIntegral
:: (HasCallStack, Integral a, Show a)
=> SInt n -> a -> Fin n
finFromIntegral :: SInt n -> a -> Fin n
finFromIntegral SInt n
n =
SInt n -> Int -> Fin n
forall (n :: Nat). HasCallStack => SInt n -> Int -> Fin n
fin SInt n
n (Int -> Fin n) -> (a -> Int) -> a -> Fin n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral
{-# INLINE ufin #-}
ufin :: HasCallStack => SInt n -> FinRep -> Fin n
ufin :: SInt n -> Int -> Fin n
ufin SInt n
sn Int
i
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n = String -> Fin n
forall a. HasCallStack => String -> a
error (String -> Fin n) -> String -> Fin n
forall a b. (a -> b) -> a -> b
$ String
"Fin: number out of range " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" >= " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n
| Bool
otherwise = Int -> Fin n
forall (n :: Nat). Int -> Fin n
Fin Int
i
where
n :: Int
n = SInt n -> Int
forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn
knownFin :: (i <= n - 1) => SInt i -> Fin n
knownFin :: SInt i -> Fin n
knownFin = Int -> Fin n
forall a (n :: Nat). Integral a => a -> Fin n
unsafeFin (Int -> Fin n) -> (SInt i -> Int) -> SInt i -> Fin n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SInt i -> Int
forall (n :: Nat). SInt n -> Int
unSInt
{-# INLINE knownFin #-}
{-# INLINE unsafeFin #-}
unsafeFin :: Integral a => a -> Fin n
unsafeFin :: a -> Fin n
unsafeFin = Int -> Fin n
forall (n :: Nat). Int -> Fin n
Fin (Int -> Fin n) -> (a -> Int) -> a -> Fin n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral
tryFin :: Integral a => SInt n -> a -> Maybe (Fin n)
tryFin :: SInt n -> a -> Maybe (Fin n)
tryFin SInt n
n a
x =
if a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
0 Bool -> Bool -> Bool
&& a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< Int -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral (SInt n -> Int
forall (n :: Nat). SInt n -> Int
unSInt SInt n
n)
then Fin n -> Maybe (Fin n)
forall a. a -> Maybe a
Just (Int -> Fin n
forall (n :: Nat). Int -> Fin n
Fin (a -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
x))
else Maybe (Fin n)
forall a. Maybe a
Nothing
finMod :: forall n a . (HasCallStack, Integral a) => SInt n -> a -> Fin n
finMod :: SInt n -> a -> Fin n
finMod SInt n
n = (a, Fin n) -> Fin n
forall a b. (a, b) -> b
snd ((a, Fin n) -> Fin n) -> (a -> (a, Fin n)) -> a -> Fin n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SInt n -> a -> (a, Fin n)
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 :: SInt n -> a -> (a, Fin n)
finDivMod SInt n
sn a
x
| Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = String -> (a, Fin n)
forall a. HasCallStack => String -> a
error String
"finDivMod: zero modulus."
| Bool
otherwise = (Integer -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
d, Int -> Fin n
forall (n :: Nat). Int -> Fin n
Fin (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
m))
where
(Integer
d, Integer
m) = Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
divMod (a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
x :: Integer) Integer
n
n :: Integer
n = Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ SInt n -> Int
forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn
complementFin :: SInt n -> Fin n -> Fin n
complementFin :: SInt n -> Fin n -> Fin n
complementFin SInt n
sn Fin n
x = Int -> Fin n
forall a (n :: Nat). Integral a => a -> Fin n
unsafeFin (SInt n -> Int
forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Fin n -> Int
forall (n :: Nat). Fin n -> Int
finToInt Fin n
x)
finToInt :: Fin n -> Int
finToInt :: Fin n -> Int
finToInt (Fin Int
i) = Int
i
{-# INLINE finToInt #-}
twice :: SInt n -> Fin n -> Fin n
twice :: SInt n -> Fin n -> Fin n
twice SInt n
sn (Fin Int
i) = SInt n -> Int -> Fin n
forall (n :: Nat). HasCallStack => SInt n -> Int -> Fin n
ufin SInt n
sn (Int -> Fin n) -> Int -> Fin n
forall a b. (a -> b) -> a -> b
$ Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
2
half :: Fin n -> Fin n
half :: Fin n -> Fin n
half (Fin Int
n) = Int -> Fin n
forall (n :: Nat). Int -> Fin n
Fin (Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`quot` Int
2)
quarter :: Fin n -> Fin n
quarter :: Fin n -> Fin n
quarter (Fin Int
n) = Int -> Fin n
forall (n :: Nat). Int -> Fin n
Fin (Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`quot` Int
4)
unsafePred :: Fin n -> Fin n
unsafePred :: Fin n -> Fin n
unsafePred (Fin Int
x) = Int -> Fin n
forall (n :: Nat). Int -> Fin n
Fin (Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
{-# INLINE unsafePred #-}
unsafeSucc :: Fin n -> Fin n
unsafeSucc :: Fin n -> Fin n
unsafeSucc (Fin Int
x) = Int -> Fin n
forall (n :: Nat). Int -> Fin n
Fin (Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
{-# INLINE unsafeSucc #-}
enumFin :: SInt n -> [Fin n]
enumFin :: SInt n -> [Fin n]
enumFin SInt n
sn = (Int -> Fin n) -> [Int] -> [Fin n]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Fin n
coerce [Int
0 .. SInt n -> Int
forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
{-# INLINE enumFin #-}
enumFinDown :: SInt n -> [Fin n]
enumFinDown :: SInt n -> [Fin n]
enumFinDown SInt n
sn = (Int -> Fin n) -> [Int] -> [Fin n]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Fin n
coerce [SInt n -> Int
forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1, SInt n -> Int
forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2 .. Int
0]
{-# INLINE enumFinDown #-}
enumDownFrom :: SInt n -> Fin n -> [Fin n]
enumDownFrom :: SInt n -> Fin n -> [Fin n]
enumDownFrom SInt n
_sn (Fin Int
x) = (Int -> Fin n) -> [Int] -> [Fin n]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Fin n
coerce [Int
x, Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 .. Int
0]
{-# INLINE enumDownFrom #-}
enumDownTo :: SInt n -> Fin n -> [Fin n]
enumDownTo :: SInt n -> Fin n -> [Fin n]
enumDownTo SInt n
sn (Fin Int
x) = (Int -> Fin n) -> [Int] -> [Fin n]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Fin n
coerce [SInt n -> Int
forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1, SInt n -> Int
forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2 .. Int
x]
{-# INLINE enumDownTo #-}
enumDownFromTo :: SInt n -> Fin n -> Fin n -> [Fin n]
enumDownFromTo :: SInt n -> Fin n -> Fin n -> [Fin n]
enumDownFromTo SInt n
_sn (Fin Int
x) (Fin Int
y) = (Int -> Fin n) -> [Int] -> [Fin n]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Fin n
coerce [Int
x, Int
x Int -> Int -> Int
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 = Int -> Fin n
forall (n :: Nat). Int -> Fin n
Fin (Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
| Bool
otherwise = String -> Fin n
forall a. HasCallStack => String -> a
error (String -> Fin n) -> String -> Fin n
forall a b. (a -> b) -> a -> b
$
String
"pred @(Fin " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (SInt n -> Int
forall (n :: Nat). SInt n -> Int
unSInt @n SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal) String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
"): no predecessor of 0"
succ :: Fin n -> Fin n
succ (Fin Int
x)
| Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 = Int -> Fin n
forall (n :: Nat). Int -> Fin n
Fin (Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
| Bool
otherwise = String -> Fin n
forall a. HasCallStack => String -> a
error (String -> Fin n) -> String -> Fin n
forall a b. (a -> b) -> a -> b
$
String
"succ @(Fin " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"): no successor of " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n
where !n :: Int
n = SInt n -> Int
forall (n :: Nat). SInt n -> Int
unSInt @n SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
toEnum :: Int -> Fin n
toEnum = SInt n -> Int -> Fin n
forall (n :: Nat). HasCallStack => SInt n -> Int -> Fin n
fin SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
fromEnum :: Fin n -> Int
fromEnum = Fin n -> Int
forall (n :: Nat). Fin n -> Int
finToInt
enumFrom :: Fin n -> [Fin n]
enumFrom (Fin Int
x) =
(Int -> Fin n) -> [Int] -> [Fin n]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Fin n
coerce [Int
x .. SInt n -> Int
forall (n :: Nat). SInt n -> Int
unSInt @n SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
enumFromThen :: Fin n -> Fin n -> [Fin n]
enumFromThen (Fin Int
x) (Fin Int
y) =
(Int -> Fin n) -> [Int] -> [Fin n]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Fin n
coerce [Int
x, Int
y .. SInt n -> Int
forall (n :: Nat). SInt n -> Int
unSInt @n SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
enumFromTo :: Fin n -> Fin n -> [Fin n]
enumFromTo (Fin Int
x) (Fin Int
z) = (Int -> Fin n) -> [Int] -> [Fin n]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Fin n
coerce [Int
x .. Int
z]
enumFromThenTo :: Fin n -> Fin n -> Fin n -> [Fin n]
enumFromThenTo (Fin Int
x) (Fin Int
y) (Fin Int
z) = (Int -> Fin n) -> [Int] -> [Fin n]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Fin n
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 :: Fin n
minFin = Int -> Fin n
forall (n :: Nat). Int -> Fin n
Fin Int
0
maxFin :: 1 <= n => SInt n -> Fin n
maxFin :: SInt n -> Fin n
maxFin SInt n
sn = Int -> Fin n
forall (n :: Nat). Int -> Fin n
Fin (SInt n -> Int
forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
instance FinSize n => Bounded (Fin n) where
minBound :: Fin n
minBound = Fin n
forall (n :: Nat). (1 <= n) => Fin n
minFin
maxBound :: Fin n
maxBound = SInt n -> Fin n
forall (n :: Nat). (1 <= n) => SInt n -> Fin n
maxFin SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
{-# INLINE minBound #-}
{-# INLINE maxBound #-}
instance KnownNat n => Default (Fin n) where
def :: Fin n
def = SInt n -> Int -> Fin n
forall (n :: Nat). HasCallStack => SInt n -> Int -> Fin n
fin SInt n
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 :: SInt n -> String -> Fin n -> Fin n -> a
overflowedError SInt n
sn String
nm Fin n
x Fin n
y = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$
String -> ShowS
showString String
nm ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
String -> ShowS
showString String
" @" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
Int -> ShowS
forall a. Show a => a -> ShowS
shows (SInt n -> Int
forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
String -> ShowS
showString String
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
Fin n -> ShowS
forall a. Show a => a -> ShowS
shows Fin n
x ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
String -> ShowS
showString String
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
Fin n -> ShowS
forall a. Show a => a -> ShowS
shows Fin n
y ShowS -> ShowS
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 :: SInt n -> String -> Fin n -> Fin n -> Int -> a
outOfRangeError SInt n
sn String
nm Fin n
x Fin n
y Int
r = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$
String -> ShowS
showString String
nm ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
String -> ShowS
showString String
" @" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
Int -> ShowS
forall a. Show a => a -> ShowS
shows (SInt n -> Int
forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
String -> ShowS
showString String
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
Fin n -> ShowS
forall a. Show a => a -> ShowS
shows Fin n
x ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
String -> ShowS
showString String
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
Fin n -> ShowS
forall a. Show a => a -> ShowS
shows Fin n
y ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
String -> ShowS
showString String
" = " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
Int -> ShowS
forall a. Show a => a -> ShowS
shows Int
r ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
String
" out of range."
add_ :: SInt n -> Fin n -> Fin n -> Maybe (Bool, FinRep)
add_ :: 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 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
y
in if Int
z Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
x
then Maybe (Bool, Int)
forall a. Maybe a
Nothing
else (Bool, Int) -> Maybe (Bool, Int)
forall a. a -> Maybe a
Just (Int
z Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< SInt n -> Int
forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn, Int
z)
{-# INLINE add_ #-}
sub_ :: Fin n -> Fin n -> Maybe (Bool, FinRep)
sub_ :: Fin n -> Fin n -> Maybe (Bool, Int)
sub_ = \ (Fin Int
x) (Fin Int
y) -> let z :: Int
z = Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
y in (Bool, Int) -> Maybe (Bool, Int)
forall a. a -> Maybe a
Just (Int
z Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0, Int
z)
{-# INLINE sub_ #-}
mul_ :: SInt n -> Fin n -> Fin n -> Maybe (Bool, FinRep)
mul_ :: 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 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
y
in if Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
0 Bool -> Bool -> Bool
&& Int
z Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
y
then Maybe (Bool, Int)
forall a. Maybe a
Nothing
else (Bool, Int) -> Maybe (Bool, Int)
forall a. a -> Maybe a
Just (Int
z Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< SInt n -> Int
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 :: 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) -> SInt n -> Int -> Fin n
forall (n :: Nat) a.
(HasCallStack, Integral a) =>
SInt n -> a -> Fin n
finMod SInt n
sn Int
z
Maybe (Bool, Int)
Nothing -> SInt n -> String -> Fin n -> Fin n -> Fin n
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 :: SInt n -> Fin n -> Fin n -> Fin n
modAdd SInt n
sn = (HasCallStack =>
SInt n
-> String
-> (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n
-> Fin n
-> Fin n)
-> SInt n
-> String
-> (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n
-> Fin n
-> Fin n
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack HasCallStack =>
SInt n
-> String
-> (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n
-> Fin n
-> Fin n
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" (SInt n -> Fin n -> Fin n -> Maybe (Bool, Int)
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 :: SInt n -> Fin n -> Fin n -> Fin n
modSub SInt n
sn = SInt n
-> String
-> (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n
-> Fin n
-> Fin n
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" Fin n -> Fin n -> Maybe (Bool, Int)
forall (n :: Nat). Fin n -> Fin n -> Maybe (Bool, Int)
sub_
{-# INLINEABLE modSub #-}
modMul :: HasCallStack => SInt n -> Fin n -> Fin n -> Fin n
modMul :: SInt n -> Fin n -> Fin n -> Fin n
modMul SInt n
sn = (HasCallStack =>
SInt n
-> String
-> (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n
-> Fin n
-> Fin n)
-> SInt n
-> String
-> (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n
-> Fin n
-> Fin n
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack HasCallStack =>
SInt n
-> String
-> (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n
-> Fin n
-> Fin n
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" (SInt n -> Fin n -> Fin n -> Maybe (Bool, Int)
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 :: SInt n -> Fin n -> Fin n
modNegate SInt n
_ (Fin Int
0) = Int -> Fin n
forall (n :: Nat). Int -> Fin n
Fin Int
0
modNegate SInt n
sn (Fin Int
x) = Int -> Fin n
forall (n :: Nat). Int -> Fin n
Fin (SInt n -> Int
forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn Int -> Int -> Int
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 :: (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) -> Fin n -> Maybe (Fin n)
forall a. a -> Maybe a
Just (Int -> Fin n
forall (n :: Nat). Int -> Fin n
Fin Int
z)
Maybe (Bool, Int)
_ -> Maybe (Fin n)
forall a. Maybe a
Nothing
{-# INLINE mkTry #-}
tryAdd :: SInt n -> Fin n -> Fin n -> Maybe (Fin n)
tryAdd :: SInt n -> Fin n -> Fin n -> Maybe (Fin n)
tryAdd = (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n -> Fin n -> Maybe (Fin n)
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))
-> Fin n -> Fin n -> Maybe (Fin n))
-> (SInt n -> Fin n -> Fin n -> Maybe (Bool, Int))
-> SInt n
-> Fin n
-> Fin n
-> Maybe (Fin n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SInt n -> Fin n -> Fin n -> Maybe (Bool, Int)
forall (n :: Nat). SInt n -> Fin n -> Fin n -> Maybe (Bool, Int)
add_
{-# INLINEABLE tryAdd #-}
trySub :: Fin n -> Fin n -> Maybe (Fin n)
trySub :: Fin n -> Fin n -> Maybe (Fin n)
trySub = (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n -> Fin n -> Maybe (Fin n)
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)
forall (n :: Nat). Fin n -> Fin n -> Maybe (Bool, Int)
sub_
{-# INLINEABLE trySub #-}
tryMul :: SInt n -> Fin n -> Fin n -> Maybe (Fin n)
tryMul :: SInt n -> Fin n -> Fin n -> Maybe (Fin n)
tryMul = (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n -> Fin n -> Maybe (Fin n)
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))
-> Fin n -> Fin n -> Maybe (Fin n))
-> (SInt n -> Fin n -> Fin n -> Maybe (Bool, Int))
-> SInt n
-> Fin n
-> Fin n
-> Maybe (Fin n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SInt n -> Fin n -> Fin n -> Maybe (Bool, Int)
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 :: SInt m -> Fin (d * m) -> (Fin d, Fin m)
divModFin SInt m
sm (Fin Int
x) = (Int -> Fin d
forall (n :: Nat). Int -> Fin n
Fin Int
d, Int -> Fin m
forall (n :: Nat). Int -> Fin n
Fin Int
r)
where
(Int
d, Int
r) = Int -> Int -> (Int, Int)
forall a. Integral a => a -> a -> (a, a)
divMod Int
x (SInt m -> Int
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 :: 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 Int -> Fin n
forall (n :: Nat). Int -> Fin n
Fin Int
z else SInt n -> String -> Fin n -> Fin n -> Int -> Fin n
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 -> SInt n -> String -> Fin n -> Fin n -> Fin n
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 :: SInt n -> Fin n -> Fin n -> Fin n
chkAdd SInt n
sn = (HasCallStack =>
SInt n
-> String
-> (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n
-> Fin n
-> Fin n)
-> SInt n
-> String
-> (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n
-> Fin n
-> Fin n
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack HasCallStack =>
SInt n
-> String
-> (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n
-> Fin n
-> Fin n
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" (SInt n -> Fin n -> Fin n -> Maybe (Bool, Int)
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 :: SInt n -> Fin n -> Fin n -> Fin n
chkSub SInt n
sn = (HasCallStack =>
SInt n
-> String
-> (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n
-> Fin n
-> Fin n)
-> SInt n
-> String
-> (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n
-> Fin n
-> Fin n
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack HasCallStack =>
SInt n
-> String
-> (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n
-> Fin n
-> Fin n
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" Fin n -> Fin n -> Maybe (Bool, Int)
forall (n :: Nat). Fin n -> Fin n -> Maybe (Bool, Int)
sub_
{-# INLINEABLE chkSub #-}
chkMul :: HasCallStack => SInt n -> Fin n -> Fin n -> Fin n
chkMul :: SInt n -> Fin n -> Fin n -> Fin n
chkMul SInt n
sn = (HasCallStack =>
SInt n
-> String
-> (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n
-> Fin n
-> Fin n)
-> SInt n
-> String
-> (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n
-> Fin n
-> Fin n
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack HasCallStack =>
SInt n
-> String
-> (Fin n -> Fin n -> Maybe (Bool, Int))
-> Fin n
-> Fin n
-> Fin n
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" (SInt n -> Fin n -> Fin n -> Maybe (Bool, Int)
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 :: Attenuation (Fin n) (Fin m)
attLT = Attenuation (Fin n) (Fin m)
forall k (a :: k) (b :: k). Coercible a b => Attenuation a b
coercible
attPlus :: Attenuation (Fin n) (Fin (n + k))
attPlus :: Attenuation (Fin n) (Fin (n + k))
attPlus = Attenuation (Fin n) (Fin (n + k))
forall k (a :: k) (b :: k). Coercible a b => Attenuation a b
coercible
attMinus :: Attenuation (Fin (n - k)) (Fin n)
attMinus :: Attenuation (Fin (n - k)) (Fin n)
attMinus = Attenuation (Fin (n - k)) (Fin n)
forall k (a :: k) (b :: k). Coercible a b => Attenuation a b
coercible
attInt :: Attenuation (Fin n) Int
attInt :: Attenuation (Fin n) Int
attInt = Attenuation (Fin n) Int
forall k (a :: k) (b :: k). Coercible a b => Attenuation a b
coercible
unsafeCoFin :: Coercion (Fin n) (Fin m)
unsafeCoFin :: Coercion (Fin n) (Fin m)
unsafeCoFin = Coercion (Fin n) (Fin m)
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
unsafeCoInt :: Coercion (Fin n) Int
unsafeCoInt :: Coercion (Fin n) Int
unsafeCoInt = Coercion (Fin n) Int
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
weaken :: Fin n -> Fin (n+1)
weaken :: Fin n -> Fin (n + 1)
weaken (Fin Int
x) = Int -> Fin (n + 1)
forall (n :: Nat). Int -> Fin n
Fin Int
x
strengthen :: SInt n -> Fin (n+1) -> Maybe (Fin n)
strengthen :: SInt n -> Fin (n + 1) -> Maybe (Fin n)
strengthen SInt n
sn (Fin Int
x) = if Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== SInt n -> Int
forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn then Maybe (Fin n)
forall a. Maybe a
Nothing else Fin n -> Maybe (Fin n)
forall a. a -> Maybe a
Just (Int -> Fin n
forall (n :: Nat). Int -> Fin n
Fin Int
x)
shiftFin :: SInt m -> Fin n -> Fin (m+n)
shiftFin :: SInt m -> Fin n -> Fin (m + n)
shiftFin SInt m
sm (Fin Int
x) = Int -> Fin (m + n)
forall (n :: Nat). Int -> Fin n
Fin (SInt m -> Int
forall (n :: Nat). SInt n -> Int
unSInt SInt m
sm Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
x)
tryUnshiftFin :: SInt m -> SInt n -> Fin (m+n) -> Maybe (Fin n)
tryUnshiftFin :: SInt m -> SInt n -> Fin (m + n) -> Maybe (Fin n)
tryUnshiftFin SInt m
sm SInt n
sn (Fin Int
x) = SInt n -> Int -> Maybe (Fin n)
forall a (n :: Nat). Integral a => SInt n -> a -> Maybe (Fin n)
tryFin SInt n
sn (Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- SInt m -> Int
forall (n :: Nat). SInt n -> Int
unSInt SInt m
sm)
unshiftFin :: HasCallStack => SInt m -> SInt n -> Fin (m+n) -> Fin n
unshiftFin :: SInt m -> SInt n -> Fin (m + n) -> Fin n
unshiftFin SInt m
sm SInt n
sn (Fin Int
x) = SInt n -> Int -> Fin n
forall (n :: Nat). HasCallStack => SInt n -> Int -> Fin n
fin SInt n
sn (Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- SInt m -> Int
forall (n :: Nat). SInt n -> Int
unSInt SInt m
sm)
splitFin :: SInt m -> Fin (m + n) -> Either (Fin m) (Fin n)
splitFin :: SInt m -> Fin (m + n) -> Either (Fin m) (Fin n)
splitFin SInt m
sm (Fin Int
x)
| Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< SInt m -> Int
forall (n :: Nat). SInt n -> Int
unSInt SInt m
sm = Fin m -> Either (Fin m) (Fin n)
forall a b. a -> Either a b
Left (Fin m -> Either (Fin m) (Fin n))
-> Fin m -> Either (Fin m) (Fin n)
forall a b. (a -> b) -> a -> b
$ Int -> Fin m
forall (n :: Nat). Int -> Fin n
Fin Int
x
| Bool
otherwise = Fin n -> Either (Fin m) (Fin n)
forall a b. b -> Either a b
Right (Fin n -> Either (Fin m) (Fin n))
-> Fin n -> Either (Fin m) (Fin n)
forall a b. (a -> b) -> a -> b
$ Int -> Fin n
forall (n :: Nat). Int -> Fin n
Fin (Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- SInt m -> Int
forall (n :: Nat). SInt n -> Int
unSInt SInt m
sm)
concatFin :: SInt m -> Either (Fin m) (Fin n) -> Fin (m + n)
concatFin :: 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) -> Int -> Fin (m + n)
forall (n :: Nat). Int -> Fin n
Fin Int
x
Right Fin n
x -> SInt m -> Fin n -> Fin (m + n)
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 :: Fin m -> Fin n
embed (Fin Int
i) = Int -> Fin n
forall (n :: Nat). Int -> Fin n
Fin Int
i
{-# INLINE unembed #-}
unembed :: HasCallStack => SInt n -> Fin m -> Fin n
unembed :: SInt n -> Fin m -> Fin n
unembed SInt n
sn (Fin Int
i) = SInt n -> Int -> Fin n
forall (n :: Nat). HasCallStack => SInt n -> Int -> Fin n
ufin SInt n
sn Int
i
tryUnembed :: SInt n -> Fin m -> Maybe (Fin n)
tryUnembed :: SInt n -> Fin m -> Maybe (Fin n)
tryUnembed SInt n
sn (Fin Int
i) = SInt n -> Int -> Maybe (Fin n)
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 :: SInt n -> Fin m -> Fin n -> Fin (m * n)
crossFin SInt n
sn (Fin Int
x) (Fin Int
y) = Int -> Fin (m * n)
forall (n :: Nat). Int -> Fin n
Fin (Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
* SInt n -> Int
forall (n :: Nat). SInt n -> Int
unSInt SInt n
sn Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
y)