{-# LANGUAGE TypeOperators, ScopedTypeVariables #-}
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

-- 5 * Fin 13 is at most 5 * 12 = 60, or Fin 61. Is this too tight?
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)