module Data.Type.Fin where
import Data.Type.Nat
import Type.Class.Higher
import Type.Class.Known
import Type.Class.Witness
import Type.Family.Constraint
import Type.Family.Nat
data Fin :: N -> * where
FZ :: Fin (S n)
FS :: !(Fin n) -> Fin (S n)
deriving instance Eq (Fin n)
deriving instance Ord (Fin n)
deriving instance Show (Fin n)
instance Eq1 Fin
instance Ord1 Fin
instance Show1 Fin
instance Read1 Fin where
readsPrec1 d = readParen (d > 10) $ \s0 ->
[ (Some FZ,s1)
| ("FZ",s1) <- lex s0
] ++
[ (n >>- Some . FS,s2)
| ("FS",s1) <- lex s0
, (n,s2) <- readsPrec1 11 s1
]
instance (Known Nat n, Pos n) => Enum (Fin n) where
toEnum n
| n <= 0 = FZ
| otherwise = case (known :: Nat n) of
S_ Z_ -> FZ
S_ S_{} -> FS $ toEnum (n1)
fromEnum = fin
instance (Known Nat n, Pos n) => Bounded (Fin n) where
minBound = FZ
maxBound = case (known :: Nat n) of
S_ Z_ -> FZ
S_ S_{} -> FS maxBound
elimFin :: (forall x. p (S x))
-> (forall x. Fin x -> p x -> p (S x))
-> Fin n -> p n
elimFin z s = \case
FZ -> z
FS n -> s n $ elimFin z s n
fins :: Nat n -> [Fin n]
fins = \case
Z_ -> []
S_ x -> FZ : map FS (fins x)
fin :: Fin n -> Int
fin = \case
FZ -> 0
FS x -> succ $ fin x
finZ :: Fin Z -> Void
finZ = impossible
weaken :: Fin n -> Fin (S n)
weaken = \case
FZ -> FZ
FS n -> FS $ weaken n
without :: Fin n -> Fin n -> Maybe (Fin (Pred n))
without = \case
FZ -> \case
FZ -> Nothing
FS y -> Just y
FS x -> \case
FZ -> Just FZ \\ x
FS y -> FS <$> without x y \\ x
finNat :: Fin x -> Some Nat
finNat = \case
FZ -> Some Z_
FS x -> withSome (Some . S_) $ finNat x
instance (n' ~ Pred n) => Witness ØC (S n' ~ n) (Fin n) where
type WitnessC ØC (S n' ~ n) (Fin n) = (n' ~ Pred n)
(\\) r = \case
FZ -> r
FS _ -> r