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 :: Nat x -> Fin (S y) -> Fin (S (x :*: y))
mulNatFin x (Fin y) = Fin $ natToInt x * y
raise :: k -> Fin n -> Fin (n :+: k)
raise _ (Fin i) = Fin i
intToFin :: Int -> Nat n -> Maybe (Fin n)
intToFin i n | i >= natToInt n || i < 0 = Nothing
| otherwise = Just (Fin i)
finToInt :: Fin n -> Int
finToInt (Fin i) = i
natToFin :: Nat n -> Fin (S n)
natToFin = Fin . natToInt