module Data.Fin where
import Data.Nat
newtype Fin n = Fin Int
deriving (Show, Eq, Ord)
zero :: Fin (S n)
zero = Fin 0
succ :: Fin n -> Fin (S n)
succ (Fin n) = Fin (n + 1)
pred :: Fin n -> Fin n
pred (Fin 0) = Fin 0
pred (Fin n) = Fin (n 1)
addFin :: Fin x -> Fin y -> Fin (x :+: y)
addFin (Fin x) (Fin y) = Fin $ x + y
mulFin :: Fin x -> Fin y -> Fin (x :*: y)
mulFin (Fin x) (Fin y) = Fin $ x * y
mulNatFin :: forall x y . Reify x => Fin (S y) -> Fin (S (x :*: y))
mulNatFin (Fin y) = Fin $ natToInt (witnessNat :: Nat x) * y
raise :: Fin n -> Fin (n :+: k)
raise (Fin i) = Fin i
intToFin :: forall n . Reify n => Int -> Maybe (Fin n)
intToFin i | i >= natToInt (witnessNat :: Nat n) || i < 0 = Nothing
| otherwise = Just (Fin i)
finToInt :: Fin n -> Int
finToInt (Fin i) = i
natToFin :: forall n . Reify n => Fin (S n)
natToFin = Fin $ natToInt (witnessNat :: Nat n)