{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Data.Fin.Int
(
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 Data.SInt (sintVal)
import GHC.Stack (HasCallStack)
import GHC.TypeNats (type (*), type (+), type (-), type (<=), KnownNat)
import Data.Fin.Int.Explicit
( Fin, FinSize, unsafeFin, unsafeSucc, unsafePred
, unsafeCoFin, unsafeCoInt
, attInt, attMinus, attPlus, attLT
, half, quarter
, embed, weaken, finToInt
, modSub, trySub, minFin
)
import qualified Data.Fin.Int.Explicit as E
{-# INLINE fin #-}
fin :: forall n. (HasCallStack, KnownNat n) => Int -> Fin n
fin :: Int -> Fin n
fin = SInt n -> Int -> Fin n
forall (n :: Nat). HasCallStack => SInt n -> Int -> Fin n
E.fin SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
{-# INLINE finFromIntegral #-}
finFromIntegral
:: forall n a
. (HasCallStack, KnownNat n, Integral a, Show a)
=> a -> Fin n
finFromIntegral :: a -> Fin n
finFromIntegral = SInt n -> a -> Fin n
forall a (n :: Nat).
(HasCallStack, Integral a, Show a) =>
SInt n -> a -> Fin n
E.finFromIntegral SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
knownFin :: forall i n. (KnownNat i, i <= n - 1) => Fin n
knownFin :: Fin n
knownFin = SInt i -> Fin n
forall (i :: Nat) (n :: Nat). (i <= (n - 1)) => SInt i -> Fin n
E.knownFin ((HasCallStack, KnownNat i) => SInt i
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal @i)
{-# INLINE knownFin #-}
tryFin :: forall n a. (Integral a, KnownNat n) => a -> Maybe (Fin n)
tryFin :: a -> Maybe (Fin n)
tryFin = SInt n -> a -> Maybe (Fin n)
forall a (n :: Nat). Integral a => SInt n -> a -> Maybe (Fin n)
E.tryFin SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
finMod :: forall n a . (HasCallStack, Integral a, KnownNat n) => a -> Fin n
finMod :: a -> Fin n
finMod = SInt n -> a -> Fin n
forall (n :: Nat) a.
(HasCallStack, Integral a) =>
SInt n -> a -> Fin n
E.finMod SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
finDivMod
:: forall n a
. (HasCallStack, Integral a, KnownNat n)
=> a -> (a, Fin n)
finDivMod :: a -> (a, Fin n)
finDivMod = SInt n -> a -> (a, Fin n)
forall (n :: Nat) a.
(HasCallStack, Integral a) =>
SInt n -> a -> (a, Fin n)
E.finDivMod SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
complementFin :: forall n. (KnownNat n) => Fin n -> Fin n
complementFin :: Fin n -> Fin n
complementFin = SInt n -> Fin n -> Fin n
forall (n :: Nat). SInt n -> Fin n -> Fin n
E.complementFin SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
twice :: KnownNat n => Fin n -> Fin n
twice :: Fin n -> Fin n
twice = SInt n -> Fin n -> Fin n
forall (n :: Nat). SInt n -> Fin n -> Fin n
E.twice SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
maxFin :: (1 <= n, KnownNat n) => Fin n
maxFin :: Fin n
maxFin = SInt n -> Fin n
forall (n :: Nat). (1 <= n) => SInt n -> Fin n
E.maxFin SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
{-# INLINE maxFin #-}
enumFin :: forall n. KnownNat n => [Fin n]
enumFin :: [Fin n]
enumFin = SInt n -> [Fin n]
forall (n :: Nat). SInt n -> [Fin n]
E.enumFin SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
{-# INLINE enumFin #-}
enumFinDown :: forall n. KnownNat n => [Fin n]
enumFinDown :: [Fin n]
enumFinDown = SInt n -> [Fin n]
forall (n :: Nat). SInt n -> [Fin n]
E.enumFinDown SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
{-# INLINE enumFinDown #-}
enumDownFrom :: forall n. KnownNat n => Fin n -> [Fin n]
enumDownFrom :: Fin n -> [Fin n]
enumDownFrom = SInt n -> Fin n -> [Fin n]
forall (n :: Nat). SInt n -> Fin n -> [Fin n]
E.enumDownFrom SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
{-# INLINE enumDownFrom #-}
enumDownTo :: forall n. KnownNat n => Fin n -> [Fin n]
enumDownTo :: Fin n -> [Fin n]
enumDownTo = SInt n -> Fin n -> [Fin n]
forall (n :: Nat). SInt n -> Fin n -> [Fin n]
E.enumDownTo SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
{-# INLINE enumDownTo #-}
enumDownFromTo :: forall n. KnownNat n => Fin n -> Fin n -> [Fin n]
enumDownFromTo :: Fin n -> Fin n -> [Fin n]
enumDownFromTo = SInt n -> Fin n -> Fin n -> [Fin n]
forall (n :: Nat). SInt n -> Fin n -> Fin n -> [Fin n]
E.enumDownFromTo SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
{-# INLINE enumDownFromTo #-}
modAdd, (+%) :: forall n. (HasCallStack, KnownNat n) => Fin n -> Fin n -> Fin n
modAdd :: Fin n -> Fin n -> Fin n
modAdd = SInt n -> Fin n -> Fin n -> Fin n
forall (n :: Nat).
HasCallStack =>
SInt n -> Fin n -> Fin n -> Fin n
E.modAdd SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
+% :: Fin n -> Fin n -> Fin n
(+%) = SInt n -> Fin n -> Fin n -> Fin n
forall (n :: Nat).
HasCallStack =>
SInt n -> Fin n -> Fin n -> Fin n
E.modAdd SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
{-# INLINEABLE modAdd #-}
{-# INLINEABLE (+%) #-}
(-%) :: forall n. KnownNat n => Fin n -> Fin n -> Fin n
-% :: Fin n -> Fin n -> Fin n
(-%) = SInt n -> Fin n -> Fin n -> Fin n
forall (n :: Nat). SInt n -> Fin n -> Fin n -> Fin n
E.modSub SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
{-# INLINEABLE (-%) #-}
modMul, (*%) :: forall n. (HasCallStack, KnownNat n) => Fin n -> Fin n -> Fin n
modMul :: Fin n -> Fin n -> Fin n
modMul = SInt n -> Fin n -> Fin n -> Fin n
forall (n :: Nat).
HasCallStack =>
SInt n -> Fin n -> Fin n -> Fin n
E.modMul SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
*% :: Fin n -> Fin n -> Fin n
(*%) = SInt n -> Fin n -> Fin n -> Fin n
forall (n :: Nat).
HasCallStack =>
SInt n -> Fin n -> Fin n -> Fin n
E.modMul SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
{-# INLINEABLE modMul #-}
{-# INLINEABLE (*%) #-}
modNegate :: forall n. KnownNat n => Fin n -> Fin n
modNegate :: Fin n -> Fin n
modNegate = SInt n -> Fin n -> Fin n
forall (n :: Nat). SInt n -> Fin n -> Fin n
E.modNegate SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
tryAdd, (+?) :: KnownNat n => Fin n -> Fin n -> Maybe (Fin n)
tryAdd :: Fin n -> Fin n -> Maybe (Fin n)
tryAdd = SInt n -> Fin n -> Fin n -> Maybe (Fin n)
forall (n :: Nat). SInt n -> Fin n -> Fin n -> Maybe (Fin n)
E.tryAdd SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
+? :: Fin n -> Fin n -> Maybe (Fin n)
(+?) = SInt n -> Fin n -> Fin n -> Maybe (Fin n)
forall (n :: Nat). SInt n -> Fin n -> Fin n -> Maybe (Fin n)
E.tryAdd SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
{-# INLINEABLE tryAdd #-}
{-# INLINEABLE (+?) #-}
(-?) :: KnownNat n => Fin n -> Fin n -> Maybe (Fin n)
-? :: Fin n -> Fin n -> Maybe (Fin n)
(-?) = Fin n -> Fin n -> Maybe (Fin n)
forall (n :: Nat). Fin n -> Fin n -> Maybe (Fin n)
E.trySub
{-# INLINEABLE (-?) #-}
tryMul, (*?) :: KnownNat n => Fin n -> Fin n -> Maybe (Fin n)
tryMul :: Fin n -> Fin n -> Maybe (Fin n)
tryMul = SInt n -> Fin n -> Fin n -> Maybe (Fin n)
forall (n :: Nat). SInt n -> Fin n -> Fin n -> Maybe (Fin n)
E.tryMul SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
*? :: Fin n -> Fin n -> Maybe (Fin n)
(*?) = SInt n -> Fin n -> Fin n -> Maybe (Fin n)
forall (n :: Nat). SInt n -> Fin n -> Fin n -> Maybe (Fin n)
E.tryMul SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
{-# INLINEABLE tryMul #-}
{-# INLINEABLE (*?) #-}
divModFin :: forall m d. KnownNat m => Fin (d * m) -> (Fin d, Fin m)
divModFin :: Fin (d * m) -> (Fin d, Fin m)
divModFin = SInt m -> Fin (d * m) -> (Fin d, Fin m)
forall (m :: Nat) (d :: Nat).
SInt m -> Fin (d * m) -> (Fin d, Fin m)
E.divModFin SInt m
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
chkAdd, (+!) :: (HasCallStack, KnownNat n) => Fin n -> Fin n -> Fin n
chkAdd :: Fin n -> Fin n -> Fin n
chkAdd = SInt n -> Fin n -> Fin n -> Fin n
forall (n :: Nat).
HasCallStack =>
SInt n -> Fin n -> Fin n -> Fin n
E.chkAdd SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
+! :: Fin n -> Fin n -> Fin n
(+!) = SInt n -> Fin n -> Fin n -> Fin n
forall (n :: Nat).
HasCallStack =>
SInt n -> Fin n -> Fin n -> Fin n
E.chkAdd SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
{-# INLINEABLE chkAdd #-}
{-# INLINEABLE (+!) #-}
chkSub, (-!) :: (HasCallStack, KnownNat n) => Fin n -> Fin n -> Fin n
chkSub :: Fin n -> Fin n -> Fin n
chkSub = SInt n -> Fin n -> Fin n -> Fin n
forall (n :: Nat).
HasCallStack =>
SInt n -> Fin n -> Fin n -> Fin n
E.chkSub SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
-! :: Fin n -> Fin n -> Fin n
(-!) = SInt n -> Fin n -> Fin n -> Fin n
forall (n :: Nat).
HasCallStack =>
SInt n -> Fin n -> Fin n -> Fin n
E.chkSub SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
{-# INLINEABLE chkSub #-}
{-# INLINEABLE (-!) #-}
chkMul, (*!) :: (HasCallStack, KnownNat n) => Fin n -> Fin n -> Fin n
chkMul :: Fin n -> Fin n -> Fin n
chkMul = SInt n -> Fin n -> Fin n -> Fin n
forall (n :: Nat).
HasCallStack =>
SInt n -> Fin n -> Fin n -> Fin n
E.chkMul SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
*! :: Fin n -> Fin n -> Fin n
(*!) = SInt n -> Fin n -> Fin n -> Fin n
forall (n :: Nat).
HasCallStack =>
SInt n -> Fin n -> Fin n -> Fin n
E.chkMul SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
{-# INLINEABLE chkMul #-}
{-# INLINEABLE (*!) #-}
strengthen :: forall n. KnownNat n => Fin (n+1) -> Maybe (Fin n)
strengthen :: Fin (n + 1) -> Maybe (Fin n)
strengthen = SInt n -> Fin (n + 1) -> Maybe (Fin n)
forall (n :: Nat). SInt n -> Fin (n + 1) -> Maybe (Fin n)
E.strengthen SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
shiftFin :: forall m n. KnownNat m => Fin n -> Fin (m+n)
shiftFin :: Fin n -> Fin (m + n)
shiftFin = SInt m -> Fin n -> Fin (m + n)
forall (m :: Nat) (n :: Nat). SInt m -> Fin n -> Fin (m + n)
E.shiftFin SInt m
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
unshiftFin
:: forall m n
. (HasCallStack, KnownNat m, KnownNat n)
=> Fin (m+n) -> Fin n
unshiftFin :: Fin (m + n) -> Fin n
unshiftFin = SInt m -> SInt n -> Fin (m + n) -> Fin n
forall (m :: Nat) (n :: Nat).
HasCallStack =>
SInt m -> SInt n -> Fin (m + n) -> Fin n
E.unshiftFin SInt m
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
tryUnshiftFin
:: forall m n
. (KnownNat m, KnownNat n)
=> Fin (m+n) -> Maybe (Fin n)
tryUnshiftFin :: Fin (m + n) -> Maybe (Fin n)
tryUnshiftFin = SInt m -> SInt n -> Fin (m + n) -> Maybe (Fin n)
forall (m :: Nat) (n :: Nat).
SInt m -> SInt n -> Fin (m + n) -> Maybe (Fin n)
E.tryUnshiftFin SInt m
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
splitFin :: forall m n. KnownNat m => Fin (m + n) -> Either (Fin m) (Fin n)
splitFin :: Fin (m + n) -> Either (Fin m) (Fin n)
splitFin = SInt m -> Fin (m + n) -> Either (Fin m) (Fin n)
forall (m :: Nat) (n :: Nat).
SInt m -> Fin (m + n) -> Either (Fin m) (Fin n)
E.splitFin SInt m
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
concatFin :: forall m n. KnownNat m => Either (Fin m) (Fin n) -> Fin (m + n)
concatFin :: Either (Fin m) (Fin n) -> Fin (m + n)
concatFin = SInt m -> Either (Fin m) (Fin n) -> Fin (m + n)
forall (m :: Nat) (n :: Nat).
SInt m -> Either (Fin m) (Fin n) -> Fin (m + n)
E.concatFin SInt m
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
{-# INLINE unembed #-}
unembed :: (HasCallStack, KnownNat n) => Fin m -> Fin n
unembed :: Fin m -> Fin n
unembed = SInt n -> Fin m -> Fin n
forall (n :: Nat) (m :: Nat).
HasCallStack =>
SInt n -> Fin m -> Fin n
E.unembed SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
{-# INLINE tryUnembed #-}
tryUnembed :: KnownNat n => Fin m -> Maybe (Fin n)
tryUnembed :: Fin m -> Maybe (Fin n)
tryUnembed = SInt n -> Fin m -> Maybe (Fin n)
forall (n :: Nat) (m :: Nat). SInt n -> Fin m -> Maybe (Fin n)
E.tryUnembed SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
crossFin :: forall m n. KnownNat n => Fin m -> Fin n -> Fin (m * n)
crossFin :: Fin m -> Fin n -> Fin (m * n)
crossFin = SInt n -> Fin m -> Fin n -> Fin (m * n)
forall (n :: Nat) (m :: Nat).
SInt n -> Fin m -> Fin n -> Fin (m * n)
E.crossFin SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal