module Data.Fin (
Fin (..),
natToFin, toFin, unsafeToFin, fromFin,
finZ, finS, finLast,
absurd,
weaken, weakenN, strengthen,
shift,
finAdd, finAddN,
finSub, finSubN,
finMult
) where
import GHC.TypeLits
import Data.Proxy
import Data.Typeable
import Unsafe.Coerce
newtype Fin s (n :: Nat) = Fin s
deriving (Typeable)
deriving instance Ord s => Ord (Fin s n)
deriving instance Eq s => Eq (Fin s n)
deriving instance Show s => Show (Fin s n)
finZ :: (Integral s, KnownNat (n + 1)) => Fin s (n + 1)
finZ = Fin 0
finS :: (Integral s, KnownNat n, KnownNat (n + 1)) => Fin s n -> Fin s (n + 1)
finS (Fin x) = Fin x
finLast :: forall s n. (Integral s, KnownNat n, KnownNat (n + 1)) => Fin s (n + 1)
finLast = unsafeToFin $ fromIntegral $ natVal (Proxy :: Proxy n)
absurd :: Fin s 0 -> a
absurd = unsafeCoerce
natToFin :: (Integral s, KnownNat n, KnownNat (m + 1), n <= m) => proxy n -> Fin s (m + 1)
natToFin = unsafeToFin . fromIntegral . natVal
toFin :: forall s n. (Integral s, KnownNat (n :: Nat)) => s -> Maybe (Fin s n)
toFin x
| x < 0 = Nothing
| x < fromIntegral (natVal (Proxy :: Proxy n)) = Just $ Fin x
| otherwise = Nothing
unsafeToFin :: (Integral s, KnownNat n) => s -> Fin s n
unsafeToFin = Fin
fromFin :: Fin s n -> s
fromFin (Fin x) = x
weaken :: (Integral s, KnownNat (n + 1)) => Fin s n -> Fin s (n + 1)
weaken (Fin x) = unsafeToFin x
weakenN :: (Integral s, KnownNat (n + m)) => proxy m -> Fin s n -> Fin s (n + m)
weakenN _ (Fin x) = unsafeToFin x
strengthen :: forall n s. (KnownNat n, Integral s, Ord s) => Fin s (n + 1) -> Either (Fin s (n + 1)) (Fin s n)
strengthen x'@(Fin x)
| x < fromIntegral (natVal (Proxy :: Proxy n)) = Right $ unsafeToFin x
| otherwise = Left x'
shift :: (KnownNat (m + n), Integral s) => proxy m -> Fin s n -> Fin s (m + n)
shift _ (Fin x) = unsafeToFin x
finAdd :: (Integral s, KnownNat (n + m)) => Fin s n -> Fin s m -> Fin s (n + m)
finAdd (Fin x) (Fin y) = unsafeToFin $ x + y
finAddN :: forall n s. (KnownNat n, Integral s, Ord s) => Fin s n -> s -> Either (Fin s n) (Fin s n)
finAddN x@(Fin x') y
| fromIntegral (natVal (Proxy :: Proxy n)) x' > y = Right $ Fin (x' + y)
| otherwise = Left x
finSub :: (KnownNat n, Ord s, Integral s) => Fin s n -> Fin s m -> Either (Fin s n) (Fin s n)
finSub x (Fin y) = finSubN x y
finSubN :: (KnownNat n, Ord s, Integral s) => Fin s n -> s -> Either (Fin s n) (Fin s n)
finSubN x'@(Fin x) y
| y <= x = Right $ unsafeToFin $ x y
| otherwise = Left $ x'
finMult :: (KnownNat (n * m), Integral s) => Fin s n -> Fin s m -> Fin s (n * m)
finMult (Fin x) (Fin y) = unsafeToFin $ x * y