{-# 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 :: forall (n :: Nat). (HasCallStack, KnownNat n) => Int -> Fin n
fin = forall (n :: Nat). HasCallStack => SInt n -> Int -> Fin n
E.fin 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 :: forall (n :: Nat) a.
(HasCallStack, KnownNat n, Integral a, Show a) =>
a -> Fin n
finFromIntegral = forall a (n :: Nat).
(HasCallStack, Integral a, Show a) =>
SInt n -> a -> Fin n
E.finFromIntegral forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
knownFin :: forall i n. (KnownNat i, i <= n - 1) => Fin n
knownFin :: forall (i :: Nat) (n :: Nat). (KnownNat i, i <= (n - 1)) => Fin n
knownFin = forall (i :: Nat) (n :: Nat). (i <= (n - 1)) => SInt i -> Fin n
E.knownFin (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 :: forall (n :: Nat) a. (Integral a, KnownNat n) => a -> Maybe (Fin n)
tryFin = forall a (n :: Nat). Integral a => SInt n -> a -> Maybe (Fin n)
E.tryFin forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
finMod :: forall n a . (HasCallStack, Integral a, KnownNat n) => a -> Fin n
finMod :: forall (n :: Nat) a.
(HasCallStack, Integral a, KnownNat n) =>
a -> Fin n
finMod = forall (n :: Nat) a.
(HasCallStack, Integral a) =>
SInt n -> a -> Fin n
E.finMod forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
finDivMod
:: forall n a
. (HasCallStack, Integral a, KnownNat n)
=> a -> (a, Fin n)
finDivMod :: forall (n :: Nat) a.
(HasCallStack, Integral a, KnownNat n) =>
a -> (a, Fin n)
finDivMod = forall (n :: Nat) a.
(HasCallStack, Integral a) =>
SInt n -> a -> (a, Fin n)
E.finDivMod forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
complementFin :: forall n. (KnownNat n) => Fin n -> Fin n
complementFin :: forall (n :: Nat). KnownNat n => Fin n -> Fin n
complementFin = forall (n :: Nat). SInt n -> Fin n -> Fin n
E.complementFin forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
twice :: KnownNat n => Fin n -> Fin n
twice :: forall (n :: Nat). KnownNat n => Fin n -> Fin n
twice = forall (n :: Nat). SInt n -> Fin n -> Fin n
E.twice forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
maxFin :: (1 <= n, KnownNat n) => Fin n
maxFin :: forall (n :: Nat). (1 <= n, KnownNat n) => Fin n
maxFin = forall (n :: Nat). (1 <= n) => SInt n -> Fin n
E.maxFin forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
{-# INLINE maxFin #-}
enumFin :: forall n. KnownNat n => [Fin n]
enumFin :: forall (n :: Nat). KnownNat n => [Fin n]
enumFin = forall (n :: Nat). SInt n -> [Fin n]
E.enumFin forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
{-# INLINE enumFin #-}
enumFinDown :: forall n. KnownNat n => [Fin n]
enumFinDown :: forall (n :: Nat). KnownNat n => [Fin n]
enumFinDown = forall (n :: Nat). SInt n -> [Fin n]
E.enumFinDown forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
{-# INLINE enumFinDown #-}
enumDownFrom :: forall n. KnownNat n => Fin n -> [Fin n]
enumDownFrom :: forall (n :: Nat). KnownNat n => Fin n -> [Fin n]
enumDownFrom = forall (n :: Nat). SInt n -> Fin n -> [Fin n]
E.enumDownFrom forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
{-# INLINE enumDownFrom #-}
enumDownTo :: forall n. KnownNat n => Fin n -> [Fin n]
enumDownTo :: forall (n :: Nat). KnownNat n => Fin n -> [Fin n]
enumDownTo = forall (n :: Nat). SInt n -> Fin n -> [Fin n]
E.enumDownTo forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
{-# INLINE enumDownTo #-}
enumDownFromTo :: forall n. KnownNat n => Fin n -> Fin n -> [Fin n]
enumDownFromTo :: forall (n :: Nat). KnownNat n => Fin n -> Fin n -> [Fin n]
enumDownFromTo = forall (n :: Nat). SInt n -> Fin n -> Fin n -> [Fin n]
E.enumDownFromTo forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
{-# INLINE enumDownFromTo #-}
modAdd, (+%) :: forall n. (HasCallStack, KnownNat n) => Fin n -> Fin n -> Fin n
modAdd :: forall (n :: Nat).
(HasCallStack, KnownNat n) =>
Fin n -> Fin n -> Fin n
modAdd = forall (n :: Nat).
HasCallStack =>
SInt n -> Fin n -> Fin n -> Fin n
E.modAdd forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
+% :: forall (n :: Nat).
(HasCallStack, KnownNat n) =>
Fin n -> Fin n -> Fin n
(+%) = forall (n :: Nat).
HasCallStack =>
SInt n -> Fin n -> Fin n -> Fin n
E.modAdd forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
{-# INLINEABLE modAdd #-}
{-# INLINEABLE (+%) #-}
(-%) :: forall n. KnownNat n => Fin n -> Fin n -> Fin n
-% :: forall (n :: Nat). KnownNat n => Fin n -> Fin n -> Fin n
(-%) = forall (n :: Nat). SInt n -> Fin n -> Fin n -> Fin n
E.modSub forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
{-# INLINEABLE (-%) #-}
modMul, (*%) :: forall n. (HasCallStack, KnownNat n) => Fin n -> Fin n -> Fin n
modMul :: forall (n :: Nat).
(HasCallStack, KnownNat n) =>
Fin n -> Fin n -> Fin n
modMul = forall (n :: Nat).
HasCallStack =>
SInt n -> Fin n -> Fin n -> Fin n
E.modMul forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
*% :: forall (n :: Nat).
(HasCallStack, KnownNat n) =>
Fin n -> Fin n -> Fin n
(*%) = forall (n :: Nat).
HasCallStack =>
SInt n -> Fin n -> Fin n -> Fin n
E.modMul forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
{-# INLINEABLE modMul #-}
{-# INLINEABLE (*%) #-}
modNegate :: forall n. KnownNat n => Fin n -> Fin n
modNegate :: forall (n :: Nat). KnownNat n => Fin n -> Fin n
modNegate = forall (n :: Nat). SInt n -> Fin n -> Fin n
E.modNegate forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
tryAdd, (+?) :: KnownNat n => Fin n -> Fin n -> Maybe (Fin n)
tryAdd :: forall (n :: Nat). KnownNat n => Fin n -> Fin n -> Maybe (Fin n)
tryAdd = forall (n :: Nat). SInt n -> Fin n -> Fin n -> Maybe (Fin n)
E.tryAdd forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
+? :: forall (n :: Nat). KnownNat n => Fin n -> Fin n -> Maybe (Fin n)
(+?) = forall (n :: Nat). SInt n -> Fin n -> Fin n -> Maybe (Fin n)
E.tryAdd forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
{-# INLINEABLE tryAdd #-}
{-# INLINEABLE (+?) #-}
(-?) :: KnownNat n => Fin n -> Fin n -> Maybe (Fin n)
-? :: forall (n :: Nat). KnownNat 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 :: forall (n :: Nat). KnownNat n => Fin n -> Fin n -> Maybe (Fin n)
tryMul = forall (n :: Nat). SInt n -> Fin n -> Fin n -> Maybe (Fin n)
E.tryMul forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
*? :: forall (n :: Nat). KnownNat n => Fin n -> Fin n -> Maybe (Fin n)
(*?) = forall (n :: Nat). SInt n -> Fin n -> Fin n -> Maybe (Fin n)
E.tryMul 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 :: forall (m :: Nat) (d :: Nat).
KnownNat m =>
Fin (d * m) -> (Fin d, Fin m)
divModFin = forall (m :: Nat) (d :: Nat).
SInt m -> Fin (d * m) -> (Fin d, Fin m)
E.divModFin forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
chkAdd, (+!) :: (HasCallStack, KnownNat n) => Fin n -> Fin n -> Fin n
chkAdd :: forall (n :: Nat).
(HasCallStack, KnownNat n) =>
Fin n -> Fin n -> Fin n
chkAdd = forall (n :: Nat).
HasCallStack =>
SInt n -> Fin n -> Fin n -> Fin n
E.chkAdd forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
+! :: forall (n :: Nat).
(HasCallStack, KnownNat n) =>
Fin n -> Fin n -> Fin n
(+!) = forall (n :: Nat).
HasCallStack =>
SInt n -> Fin n -> Fin n -> Fin n
E.chkAdd forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
{-# INLINEABLE chkAdd #-}
{-# INLINEABLE (+!) #-}
chkSub, (-!) :: (HasCallStack, KnownNat n) => Fin n -> Fin n -> Fin n
chkSub :: forall (n :: Nat).
(HasCallStack, KnownNat n) =>
Fin n -> Fin n -> Fin n
chkSub = forall (n :: Nat).
HasCallStack =>
SInt n -> Fin n -> Fin n -> Fin n
E.chkSub forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
-! :: forall (n :: Nat).
(HasCallStack, KnownNat n) =>
Fin n -> Fin n -> Fin n
(-!) = forall (n :: Nat).
HasCallStack =>
SInt n -> Fin n -> Fin n -> Fin n
E.chkSub forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
{-# INLINEABLE chkSub #-}
{-# INLINEABLE (-!) #-}
chkMul, (*!) :: (HasCallStack, KnownNat n) => Fin n -> Fin n -> Fin n
chkMul :: forall (n :: Nat).
(HasCallStack, KnownNat n) =>
Fin n -> Fin n -> Fin n
chkMul = forall (n :: Nat).
HasCallStack =>
SInt n -> Fin n -> Fin n -> Fin n
E.chkMul forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
*! :: forall (n :: Nat).
(HasCallStack, KnownNat n) =>
Fin n -> Fin n -> Fin n
(*!) = forall (n :: Nat).
HasCallStack =>
SInt n -> Fin n -> Fin n -> Fin n
E.chkMul forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
{-# INLINEABLE chkMul #-}
{-# INLINEABLE (*!) #-}
strengthen :: forall n. KnownNat n => Fin (n+1) -> Maybe (Fin n)
strengthen :: forall (n :: Nat). KnownNat n => Fin (n + 1) -> Maybe (Fin n)
strengthen = forall (n :: Nat). SInt n -> Fin (n + 1) -> Maybe (Fin n)
E.strengthen forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
shiftFin :: forall m n. KnownNat m => Fin n -> Fin (m+n)
shiftFin :: forall (m :: Nat) (n :: Nat). KnownNat m => Fin n -> Fin (m + n)
shiftFin = forall (m :: Nat) (n :: Nat). SInt m -> Fin n -> Fin (m + n)
E.shiftFin forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
unshiftFin
:: forall m n
. (HasCallStack, KnownNat m, KnownNat n)
=> Fin (m+n) -> Fin n
unshiftFin :: forall (m :: Nat) (n :: Nat).
(HasCallStack, KnownNat m, KnownNat n) =>
Fin (m + n) -> Fin n
unshiftFin = forall (m :: Nat) (n :: Nat).
HasCallStack =>
SInt m -> SInt n -> Fin (m + n) -> Fin n
E.unshiftFin forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
tryUnshiftFin
:: forall m n
. (KnownNat m, KnownNat n)
=> Fin (m+n) -> Maybe (Fin n)
tryUnshiftFin :: forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
Fin (m + n) -> Maybe (Fin n)
tryUnshiftFin = forall (m :: Nat) (n :: Nat).
SInt m -> SInt n -> Fin (m + n) -> Maybe (Fin n)
E.tryUnshiftFin forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
splitFin :: forall m n. KnownNat m => Fin (m + n) -> Either (Fin m) (Fin n)
splitFin :: forall (m :: Nat) (n :: Nat).
KnownNat 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)
E.splitFin forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
concatFin :: forall m n. KnownNat m => Either (Fin m) (Fin n) -> Fin (m + n)
concatFin :: forall (m :: Nat) (n :: Nat).
KnownNat 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)
E.concatFin forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
{-# INLINE unembed #-}
unembed :: (HasCallStack, KnownNat n) => Fin m -> Fin n
unembed :: forall (n :: Nat) (m :: Nat).
(HasCallStack, KnownNat n) =>
Fin m -> Fin n
unembed = forall (n :: Nat) (m :: Nat).
HasCallStack =>
SInt n -> Fin m -> Fin n
E.unembed forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
{-# INLINE tryUnembed #-}
tryUnembed :: KnownNat n => Fin m -> Maybe (Fin n)
tryUnembed :: forall (n :: Nat) (m :: Nat). KnownNat n => Fin m -> Maybe (Fin n)
tryUnembed = forall (n :: Nat) (m :: Nat). SInt n -> Fin m -> Maybe (Fin n)
E.tryUnembed forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
crossFin :: forall m n. KnownNat n => Fin m -> Fin n -> Fin (m * n)
crossFin :: forall (m :: Nat) (n :: Nat).
KnownNat n =>
Fin m -> Fin n -> Fin (m * n)
crossFin = forall (n :: Nat) (m :: Nat).
SInt n -> Fin m -> Fin n -> Fin (m * n)
E.crossFin forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal