{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}

module Data.TypeNat.Fin (

    Fin(..)

  , ix1
  , ix2
  , ix3
  , ix4
  , ix5
  , ix6
  , ix7
  , ix8
  , ix9
  , ix10

  , safeIndex
  , safeUpdate

  , module Data.TypeNat.Nat

  ) where

import Data.TypeNat.Nat
import Data.TypeNat.Vect

-- | Finite set datatype.
data Fin :: Nat -> * where
  FZ :: Fin (S n)
  FS :: Fin k -> Fin (S k)

ix1 :: Fin ('S n)
ix1 = Fin ('S n)
forall (n :: Nat). Fin ('S n)
FZ
ix2 :: Fin ('S ('S n))
ix2 = Fin ('S n) -> Fin ('S ('S n))
forall (k :: Nat). Fin k -> Fin ('S k)
FS Fin ('S n)
forall (n :: Nat). Fin ('S n)
ix1
ix3 :: Fin ('S ('S ('S n)))
ix3 = Fin ('S ('S n)) -> Fin ('S ('S ('S n)))
forall (k :: Nat). Fin k -> Fin ('S k)
FS Fin ('S ('S n))
forall (n :: Nat). Fin ('S ('S n))
ix2
ix4 :: Fin ('S ('S ('S ('S n))))
ix4 = Fin ('S ('S ('S n))) -> Fin ('S ('S ('S ('S n))))
forall (k :: Nat). Fin k -> Fin ('S k)
FS Fin ('S ('S ('S n)))
forall (n :: Nat). Fin ('S ('S ('S n)))
ix3
ix5 :: Fin ('S ('S ('S ('S ('S n)))))
ix5 = Fin ('S ('S ('S ('S n)))) -> Fin ('S ('S ('S ('S ('S n)))))
forall (k :: Nat). Fin k -> Fin ('S k)
FS Fin ('S ('S ('S ('S n))))
forall (n :: Nat). Fin ('S ('S ('S ('S n))))
ix4
ix6 :: Fin ('S ('S ('S ('S ('S ('S n))))))
ix6 = Fin ('S ('S ('S ('S ('S n)))))
-> Fin ('S ('S ('S ('S ('S ('S n))))))
forall (k :: Nat). Fin k -> Fin ('S k)
FS Fin ('S ('S ('S ('S ('S n)))))
forall (n :: Nat). Fin ('S ('S ('S ('S ('S n)))))
ix5
ix7 :: Fin ('S ('S ('S ('S ('S ('S ('S n)))))))
ix7 = Fin ('S ('S ('S ('S ('S ('S n))))))
-> Fin ('S ('S ('S ('S ('S ('S ('S n)))))))
forall (k :: Nat). Fin k -> Fin ('S k)
FS Fin ('S ('S ('S ('S ('S ('S n))))))
forall (n :: Nat). Fin ('S ('S ('S ('S ('S ('S n))))))
ix6
ix8 :: Fin ('S ('S ('S ('S ('S ('S ('S ('S n))))))))
ix8 = Fin ('S ('S ('S ('S ('S ('S ('S n)))))))
-> Fin ('S ('S ('S ('S ('S ('S ('S ('S n))))))))
forall (k :: Nat). Fin k -> Fin ('S k)
FS Fin ('S ('S ('S ('S ('S ('S ('S n)))))))
forall (n :: Nat). Fin ('S ('S ('S ('S ('S ('S ('S n)))))))
ix7
ix9 :: Fin ('S ('S ('S ('S ('S ('S ('S ('S ('S n)))))))))
ix9 = Fin ('S ('S ('S ('S ('S ('S ('S ('S n))))))))
-> Fin ('S ('S ('S ('S ('S ('S ('S ('S ('S n)))))))))
forall (k :: Nat). Fin k -> Fin ('S k)
FS Fin ('S ('S ('S ('S ('S ('S ('S ('S n))))))))
forall (n :: Nat). Fin ('S ('S ('S ('S ('S ('S ('S ('S n))))))))
ix8
ix10 :: Fin ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))))
ix10 = Fin ('S ('S ('S ('S ('S ('S ('S ('S ('S n)))))))))
-> Fin ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))))
forall (k :: Nat). Fin k -> Fin ('S k)
FS Fin ('S ('S ('S ('S ('S ('S ('S ('S ('S n)))))))))
forall (n :: Nat).
Fin ('S ('S ('S ('S ('S ('S ('S ('S ('S n)))))))))
ix9

-- | Safely index a Vect.
safeIndex :: Fin n -> Vect n a -> a
safeIndex :: Fin n -> Vect n a -> a
safeIndex Fin n
FZ (VCons a
a Vect n a
_) = a
a
safeIndex (FS Fin k
x) (VCons a
_ Vect n a
v) = Fin k -> Vect k a -> a
forall (n :: Nat) a. Fin n -> Vect n a -> a
safeIndex Fin k
x Vect k a
Vect n a
v

-- | Safely update a Vect.
safeUpdate :: Fin n -> (a -> a) -> Vect n a -> Vect n a
safeUpdate :: Fin n -> (a -> a) -> Vect n a -> Vect n a
safeUpdate Fin n
FZ a -> a
f (VCons a
x Vect n a
rest) = a -> Vect n a -> Vect ('S n) a
forall a (n :: Nat). a -> Vect n a -> Vect ('S n) a
VCons (a -> a
f a
x) Vect n a
rest
safeUpdate (FS Fin k
fs) a -> a
f (VCons a
x Vect n a
rest) = a -> Vect k a -> Vect ('S k) a
forall a (n :: Nat). a -> Vect n a -> Vect ('S n) a
VCons a
x (Fin k -> (a -> a) -> Vect k a -> Vect k a
forall (n :: Nat) a. Fin n -> (a -> a) -> Vect n a -> Vect n a
safeUpdate Fin k
fs a -> a
f Vect k a
Vect n a
rest)