module Data.Microgroove.Index (
Index(Index#,RZ,RS)
,mkIndex
,checkIndex, checkIndex') where
import Data.Microgroove.Lib
import GHC.TypeLits
newtype Index (xs :: [u]) (x :: u) = Index# Int deriving Show
data Index' xs x where
RZ' :: Index' (x ': xs) x
RS' :: Index xs x -> Index' (y ': xs) x
upIndex :: Index xs x -> Index' xs x
upIndex (Index# i) = case i of
0 -> cast# RZ'
_ -> cast# $ RS' $ Index# $ i1
pattern RZ :: Index (x ': xs) (x :: u)
pattern RZ = Index# 0
pattern RS :: Index (xs :: [u]) (x :: u) -> Index (y ': xs) x
pattern RS i <- (upIndex -> RS' i) where
RS (Index# i) = Index# (1+i)
mkIndex :: forall n xs . (KnownNat n, n <= Length xs 1) => Index xs (xs !! n)
mkIndex = Index# $ intVal @n
checkIndex :: forall (xs :: [*]). KnownNat (Length xs) => Int -> MaybeSome (Index xs)
checkIndex = checkIndex' @Type @xs
checkIndex' :: forall (xs :: [u]). KnownNat (Length xs) => Int -> MaybeSome (Index xs)
checkIndex' i | i < (intVal @(Length xs)) = case someNatVal (fromIntegral i) of
Just (SomeNat (Proxy :: Proxy n)) -> JustSome $ Index# @u @xs @(xs !! n) i
Nothing -> error "Impossible! Negative Vector.length in checkIndex"
| otherwise = None