diff options
Diffstat (limited to 'src/Data/Array/Nested/Mixed')
| -rw-r--r-- | src/Data/Array/Nested/Mixed/Shape.hs | 311 |
1 files changed, 120 insertions, 191 deletions
diff --git a/src/Data/Array/Nested/Mixed/Shape.hs b/src/Data/Array/Nested/Mixed/Shape.hs index a5e3ced..671df2c 100644 --- a/src/Data/Array/Nested/Mixed/Shape.hs +++ b/src/Data/Array/Nested/Mixed/Shape.hs @@ -233,7 +233,7 @@ shxEnum' sh = [fromLin sh suffixes li# | I# li# <- [0 .. shxSize sh - 1]] fromLin _ _ _ = error "impossible" --- * Mixed shape-like lists to be used for ShX and StaticShX +-- * Mixed shapes data SMayNat i n where SUnknown :: i -> SMayNat i Nothing @@ -273,208 +273,158 @@ smnAddMaybe (SKnown n) (SUnknown m) = SUnknown (fromSNat' n + m) smnAddMaybe (SKnown n) (SKnown m) = SKnown (snatPlus n m) -type role ListH nominal representational -type ListH :: [Maybe Nat] -> Type -> Type -data ListH sh i where - ZH :: ListH '[] i - ConsUnknown :: forall sh i. i -> ListH sh i -> ListH (Nothing : sh) i +type role ShX nominal representational +type ShX :: [Maybe Nat] -> Type -> Type +data ShX sh i where + ZSX :: ShX '[] i + ConsUnknown :: forall sh i. i -> ShX sh i -> ShX (Nothing : sh) i -- TODO: bring this UNPACK back when GHC no longer crashes: --- ConsKnown :: forall n sh i. {-# UNPACK #-} SNat n -> ListH sh i -> ListH (Just n : sh) i - ConsKnown :: forall n sh i. SNat n -> ListH sh i -> ListH (Just n : sh) i -deriving instance Ord i => Ord (ListH sh i) +-- ConsKnown :: forall n sh i. {-# UNPACK #-} SNat n -> ShX sh i -> ShX (Just n : sh) i + ConsKnown :: forall n sh i. SNat n -> ShX sh i -> ShX (Just n : sh) i +deriving instance Ord i => Ord (ShX sh i) -- A manually defined instance and this INLINEABLE is needed to specialize -- mdot1Inner (otherwise GHC warns specialization breaks down here). -instance Eq i => Eq (ListH sh i) where +instance Eq i => Eq (ShX sh i) where {-# INLINEABLE (==) #-} - ZH == ZH = True + ZSX == ZSX = True ConsUnknown i1 sh1 == ConsUnknown i2 sh2 = i1 == i2 && sh1 == sh2 ConsKnown _ sh1 == ConsKnown _ sh2 = sh1 == sh2 #ifdef OXAR_DEFAULT_SHOW_INSTANCES -deriving instance Show i => Show (ListH sh i) +deriving instance Show i => Show (ShX sh i) #else -instance Show i => Show (ListH sh i) where - showsPrec _ = listhShow shows +instance Show i => Show (ShX sh i) where + showsPrec _ l = shxShow (fromSMayNat shows (shows . fromSNat)) l #endif -instance NFData i => NFData (ListH sh i) where - rnf ZH = () +instance NFData i => NFData (ShX sh i) where + rnf ZSX = () rnf (x `ConsUnknown` l) = rnf x `seq` rnf l rnf (SNat `ConsKnown` l) = rnf l -data UnconsListHRes i sh1 = - forall n sh. (n : sh ~ sh1) => UnconsListHRes (SMayNat i n) (ListH sh i) -listhUncons :: ListH sh1 i -> Maybe (UnconsListHRes i sh1) -listhUncons (i `ConsUnknown` shl') = Just (UnconsListHRes (SUnknown i) shl') -listhUncons (i `ConsKnown` shl') = Just (UnconsListHRes (SKnown i) shl') -listhUncons ZH = Nothing +instance Functor (ShX sh) where + {-# INLINE fmap #-} + fmap f l = shxFmap (fromSMayNat (SUnknown . f) SKnown) l + +data UnconsShXRes i sh1 = + forall n sh. (n : sh ~ sh1) => UnconsShXRes (SMayNat i n) (ShX sh i) +shxUncons :: ShX sh1 i -> Maybe (UnconsShXRes i sh1) +shxUncons (i `ConsUnknown` shl') = Just (UnconsShXRes (SUnknown i) shl') +shxUncons (i `ConsKnown` shl') = Just (UnconsShXRes (SKnown i) shl') +shxUncons ZSX = Nothing -- | This checks only whether the types are equal; if the elements of the list -- are not singletons, their values may still differ. This corresponds to -- 'testEquality', except on the penultimate type parameter. -listhEqType :: ListH sh i -> ListH sh' i -> Maybe (sh :~: sh') -listhEqType ZH ZH = Just Refl -listhEqType (_ `ConsUnknown` sh) (_ `ConsUnknown` sh') - | Just Refl <- listhEqType sh sh' +shxEqType :: ShX sh i -> ShX sh' i -> Maybe (sh :~: sh') +shxEqType ZSX ZSX = Just Refl +shxEqType (_ `ConsUnknown` sh) (_ `ConsUnknown` sh') + | Just Refl <- shxEqType sh sh' = Just Refl -listhEqType (n `ConsKnown` sh) (m `ConsKnown` sh') +shxEqType (n `ConsKnown` sh) (m `ConsKnown` sh') | Just Refl <- testEquality n m - , Just Refl <- listhEqType sh sh' + , Just Refl <- shxEqType sh sh' = Just Refl -listhEqType _ _ = Nothing +shxEqType _ _ = Nothing -- | This checks whether the two lists actually contain equal values. This is -- more than 'testEquality', and corresponds to @geq@ from @Data.GADT.Compare@ -- in the @some@ package (except on the penultimate type parameter). -listhEqual :: Eq i => ListH sh i -> ListH sh' i -> Maybe (sh :~: sh') -listhEqual ZH ZH = Just Refl -listhEqual (n `ConsUnknown` sh) (m `ConsUnknown` sh') +shxEqual :: Eq i => ShX sh i -> ShX sh' i -> Maybe (sh :~: sh') +shxEqual ZSX ZSX = Just Refl +shxEqual (n `ConsUnknown` sh) (m `ConsUnknown` sh') | n == m - , Just Refl <- listhEqual sh sh' + , Just Refl <- shxEqual sh sh' = Just Refl -listhEqual (n `ConsKnown` sh) (m `ConsKnown` sh') +shxEqual (n `ConsKnown` sh) (m `ConsKnown` sh') | Just Refl <- testEquality n m - , Just Refl <- listhEqual sh sh' + , Just Refl <- shxEqual sh sh' = Just Refl -listhEqual _ _ = Nothing +shxEqual _ _ = Nothing -{-# INLINE listhFmap #-} -listhFmap :: (forall n. SMayNat i n -> SMayNat j n) -> ListH sh i -> ListH sh j -listhFmap _ ZH = ZH -listhFmap f (x `ConsUnknown` xs) = case f (SUnknown x) of - SUnknown y -> y `ConsUnknown` listhFmap f xs -listhFmap f (x `ConsKnown` xs) = case f (SKnown x) of - SKnown y -> y `ConsKnown` listhFmap f xs +{-# INLINE shxFmap #-} +shxFmap :: (forall n. SMayNat i n -> SMayNat j n) -> ShX sh i -> ShX sh j +shxFmap _ ZSX = ZSX +shxFmap f (x `ConsUnknown` xs) = case f (SUnknown x) of + SUnknown y -> y `ConsUnknown` shxFmap f xs +shxFmap f (x `ConsKnown` xs) = case f (SKnown x) of + SKnown y -> y `ConsKnown` shxFmap f xs -{-# INLINE listhFoldMap #-} -listhFoldMap :: Monoid m => (forall n. SMayNat i n -> m) -> ListH sh i -> m -listhFoldMap _ ZH = mempty -listhFoldMap f (x `ConsUnknown` xs) = f (SUnknown x) <> listhFoldMap f xs -listhFoldMap f (x `ConsKnown` xs) = f (SKnown x) <> listhFoldMap f xs +{-# INLINE shxFoldMap #-} +shxFoldMap :: Monoid m => (forall n. SMayNat i n -> m) -> ShX sh i -> m +shxFoldMap _ ZSX = mempty +shxFoldMap f (x `ConsUnknown` xs) = f (SUnknown x) <> shxFoldMap f xs +shxFoldMap f (x `ConsKnown` xs) = f (SKnown x) <> shxFoldMap f xs -listhLength :: ListH sh i -> Int -listhLength = getSum . listhFoldMap (\_ -> Sum 1) +shxLength :: ShX sh i -> Int +shxLength = getSum . shxFoldMap (\_ -> Sum 1) -listhRank :: ListH sh i -> SNat (Rank sh) -listhRank ZH = SNat -listhRank (_ `ConsUnknown` l) | SNat <- listhRank l = SNat -listhRank (_ `ConsKnown` l) | SNat <- listhRank l = SNat +shxRank :: ShX sh i -> SNat (Rank sh) +shxRank ZSX = SNat +shxRank (_ `ConsUnknown` l) | SNat <- shxRank l = SNat +shxRank (_ `ConsKnown` l) | SNat <- shxRank l = SNat -{-# INLINE listhShow #-} -listhShow :: forall sh i. (forall n. SMayNat i n -> ShowS) -> ListH sh i -> ShowS -listhShow f l = showString "[" . go "" l . showString "]" +{-# INLINE shxShow #-} +shxShow :: forall sh i. (forall n. SMayNat i n -> ShowS) -> ShX sh i -> ShowS +shxShow f l = showString "[" . go "" l . showString "]" where - go :: String -> ListH sh' i -> ShowS - go _ ZH = id + go :: String -> ShX sh' i -> ShowS + go _ ZSX = id go prefix (x `ConsUnknown` xs) = showString prefix . f (SUnknown x) . go "," xs go prefix (x `ConsKnown` xs) = showString prefix . f (SKnown x) . go "," xs -listhHead :: ListH (mn ': sh) i -> SMayNat i mn -listhHead (i `ConsUnknown` _) = SUnknown i -listhHead (i `ConsKnown` _) = SKnown i - -listhTail :: ListH (n : sh) i -> ListH sh i -listhTail (_ `ConsUnknown` sh) = sh -listhTail (_ `ConsKnown` sh) = sh +shxHead :: ShX (mn ': sh) i -> SMayNat i mn +shxHead (i `ConsUnknown` _) = SUnknown i +shxHead (i `ConsKnown` _) = SKnown i -listhAppend :: ListH sh i -> ListH sh' i -> ListH (sh ++ sh') i -listhAppend ZH idx' = idx' -listhAppend (i `ConsUnknown` idx) idx' = i `ConsUnknown` listhAppend idx idx' -listhAppend (i `ConsKnown` idx) idx' = i `ConsKnown` listhAppend idx idx' - -listhDrop :: forall i j sh sh'. ListH sh j -> ListH (sh ++ sh') i -> ListH sh' i -listhDrop ZH long = long -listhDrop (_ `ConsUnknown` short) long = case long of - _ `ConsUnknown` long' -> listhDrop short long' -listhDrop (_ `ConsKnown` short) long = case long of - _ `ConsKnown` long' -> listhDrop short long' +shxTail :: ShX (n : sh) i -> ShX sh i +shxTail (_ `ConsUnknown` sh) = sh +shxTail (_ `ConsKnown` sh) = sh -listhInit :: forall i n sh. ListH (n : sh) i -> ListH (Init (n : sh)) i -listhInit (i `ConsUnknown` sh@(_ `ConsUnknown` _)) = i `ConsUnknown` listhInit sh -listhInit (i `ConsUnknown` sh@(_ `ConsKnown` _)) = i `ConsUnknown` listhInit sh -listhInit (_ `ConsUnknown` ZH) = ZH -listhInit (i `ConsKnown` sh@(_ `ConsUnknown` _)) = i `ConsKnown` listhInit sh -listhInit (i `ConsKnown` sh@(_ `ConsKnown` _)) = i `ConsKnown` listhInit sh -listhInit (_ `ConsKnown` ZH) = ZH +shxAppend :: ShX sh i -> ShX sh' i -> ShX (sh ++ sh') i +shxAppend ZSX idx' = idx' +shxAppend (i `ConsUnknown` idx) idx' = i `ConsUnknown` shxAppend idx idx' +shxAppend (i `ConsKnown` idx) idx' = i `ConsKnown` shxAppend idx idx' -listhLast :: forall i n sh. ListH (n : sh) i -> SMayNat i (Last (n : sh)) -listhLast (_ `ConsUnknown` sh@(_ `ConsUnknown` _)) = listhLast sh -listhLast (_ `ConsUnknown` sh@(_ `ConsKnown` _)) = listhLast sh -listhLast (x `ConsUnknown` ZH) = SUnknown x -listhLast (_ `ConsKnown` sh@(_ `ConsUnknown` _)) = listhLast sh -listhLast (_ `ConsKnown` sh@(_ `ConsKnown` _)) = listhLast sh -listhLast (x `ConsKnown` ZH) = SKnown x +shxDropSh :: forall sh sh' i j. ShX sh j -> ShX (sh ++ sh') i -> ShX sh' i +shxDropSh ZSX long = long +shxDropSh (_ `ConsUnknown` short) long = case long of + _ `ConsUnknown` long' -> shxDropSh short long' +shxDropSh (_ `ConsKnown` short) long = case long of + _ `ConsKnown` long' -> shxDropSh short long' --- * Mixed shapes +shxDropSSX :: forall sh sh' i. StaticShX sh -> ShX (sh ++ sh') i -> ShX sh' i +shxDropSSX = coerce (shxDropSh @_ @_ @i @()) --- | This is a newtype over 'ListH'. -type role ShX nominal representational -type ShX :: [Maybe Nat] -> Type -> Type -newtype ShX sh i = ShX (ListH sh i) - deriving (Eq, Ord, NFData) +shxInit :: forall i n sh. ShX (n : sh) i -> ShX (Init (n : sh)) i +shxInit (i `ConsUnknown` sh@(_ `ConsUnknown` _)) = i `ConsUnknown` shxInit sh +shxInit (i `ConsUnknown` sh@(_ `ConsKnown` _)) = i `ConsUnknown` shxInit sh +shxInit (_ `ConsUnknown` ZSX) = ZSX +shxInit (i `ConsKnown` sh@(_ `ConsUnknown` _)) = i `ConsKnown` shxInit sh +shxInit (i `ConsKnown` sh@(_ `ConsKnown` _)) = i `ConsKnown` shxInit sh +shxInit (_ `ConsKnown` ZSX) = ZSX -pattern ZSX :: forall sh i. () => sh ~ '[] => ShX sh i -pattern ZSX = ShX ZH +shxLast :: forall i n sh. ShX (n : sh) i -> SMayNat i (Last (n : sh)) +shxLast (_ `ConsUnknown` sh@(_ `ConsUnknown` _)) = shxLast sh +shxLast (_ `ConsUnknown` sh@(_ `ConsKnown` _)) = shxLast sh +shxLast (x `ConsUnknown` ZSX) = SUnknown x +shxLast (_ `ConsKnown` sh@(_ `ConsUnknown` _)) = shxLast sh +shxLast (_ `ConsKnown` sh@(_ `ConsKnown` _)) = shxLast sh +shxLast (x `ConsKnown` ZSX) = SKnown x pattern (:$%) :: forall {sh1} {i}. forall n sh. (n : sh ~ sh1) => SMayNat i n -> ShX sh i -> ShX sh1 i -pattern i :$% shl <- ShX (listhUncons -> Just (UnconsListHRes i (ShX -> shl))) - where i :$% ShX shl = case i of; SUnknown x -> ShX (x `ConsUnknown` shl); SKnown x -> ShX (x `ConsKnown` shl) +pattern i :$% shl <- (shxUncons -> Just (UnconsShXRes i shl)) + where i :$% shl = case i of; SUnknown x -> x `ConsUnknown` shl; SKnown x -> x `ConsKnown` shl infixr 3 :$% {-# COMPLETE ZSX, (:$%) #-} type IShX sh = ShX sh Int -#ifdef OXAR_DEFAULT_SHOW_INSTANCES -deriving instance Show i => Show (ShX sh i) -#else -instance Show i => Show (ShX sh i) where - showsPrec _ (ShX l) = listhShow (fromSMayNat shows (shows . fromSNat)) l -#endif - -instance Functor (ShX sh) where - {-# INLINE fmap #-} - fmap f (ShX l) = ShX (listhFmap (fromSMayNat (SUnknown . f) SKnown) l) - --- | This checks only whether the types are equal; unknown dimensions might --- still differ. This corresponds to 'testEquality', except on the penultimate --- type parameter. -shxEqType :: ShX sh i -> ShX sh' i -> Maybe (sh :~: sh') -shxEqType ZSX ZSX = Just Refl -shxEqType (SKnown n@SNat :$% sh) (SKnown m@SNat :$% sh') - | Just Refl <- sameNat n m - , Just Refl <- shxEqType sh sh' - = Just Refl -shxEqType (SUnknown _ :$% sh) (SUnknown _ :$% sh') - | Just Refl <- shxEqType sh sh' - = Just Refl -shxEqType _ _ = Nothing - --- | This checks whether all dimensions have the same value. This is more than --- 'testEquality', and corresponds to @geq@ from @Data.GADT.Compare@ in the --- @some@ package (except on the penultimate type parameter). -shxEqual :: Eq i => ShX sh i -> ShX sh' i -> Maybe (sh :~: sh') -shxEqual ZSX ZSX = Just Refl -shxEqual (SKnown n@SNat :$% sh) (SKnown m@SNat :$% sh') - | Just Refl <- sameNat n m - , Just Refl <- shxEqual sh sh' - = Just Refl -shxEqual (SUnknown i :$% sh) (SUnknown j :$% sh') - | i == j - , Just Refl <- shxEqual sh sh' - = Just Refl -shxEqual _ _ = Nothing - -shxLength :: ShX sh i -> Int -shxLength (ShX l) = listhLength l - -shxRank :: ShX sh i -> SNat (Rank sh) -shxRank (ShX l) = listhRank l - -- | The number of elements in an array described by this shape. shxSize :: IShX sh -> Int shxSize ZSX = 1 @@ -483,22 +433,22 @@ shxSize (n :$% sh) = fromSMayNat' n * shxSize sh -- We don't report the size of the list in case of errors in order not to retain the list. {-# INLINEABLE shxFromList #-} shxFromList :: StaticShX sh -> [Int] -> IShX sh -shxFromList (StaticShX topssh) topl = ShX $ go topssh topl +shxFromList (StaticShX topssh) topl = go topssh topl where - go :: ListH sh' () -> [Int] -> ListH sh' Int - go ZH [] = ZH - go ZH _ = error $ "shxFromList: List too long (type says " ++ show (listhLength topssh) ++ ")" + go :: ShX sh' () -> [Int] -> ShX sh' Int + go ZSX [] = ZSX + go ZSX _ = error $ "shxFromList: List too long (type says " ++ show (shxLength topssh) ++ ")" go (ConsKnown sn sh) (i : is) | i == fromSNat' sn = ConsKnown sn (go sh is) | otherwise = error "shxFromList: Value does not match typing" go (ConsUnknown () sh) (i : is) = ConsUnknown i (go sh is) - go _ _ = error $ "shxFromList: List too short (type says " ++ show (listhLength topssh) ++ ")" + go _ _ = error $ "shxFromList: List too short (type says " ++ show (shxLength topssh) ++ ")" {-# INLINEABLE shxToList #-} shxToList :: IShX sh -> [Int] -shxToList (ShX l) = build (\(cons :: i -> is -> is) (nil :: is) -> - let go :: ListH sh Int -> is - go ZH = nil +shxToList l = build (\(cons :: i -> is -> is) (nil :: is) -> + let go :: ShX sh Int -> is + go ZSX = nil go (ConsUnknown i rest) = i `cons` go rest go (ConsKnown sn rest) = fromSNat' sn `cons` go rest in go l) @@ -517,15 +467,6 @@ shxFromSSX2 ZKX = Just ZSX shxFromSSX2 (SKnown n :!% sh) = (SKnown n :$%) <$> shxFromSSX2 sh shxFromSSX2 (SUnknown _ :!% _) = Nothing -shxAppend :: forall sh sh' i. ShX sh i -> ShX sh' i -> ShX (sh ++ sh') i -shxAppend = coerce (listhAppend @_ @i) - -shxHead :: ShX (n : sh) i -> SMayNat i n -shxHead (ShX list) = listhHead list - -shxTail :: ShX (n : sh) i -> ShX sh i -shxTail (ShX list) = ShX (listhTail list) - shxTakeSSX :: forall sh sh' i proxy. proxy sh' -> StaticShX sh -> ShX (sh ++ sh') i -> ShX sh i shxTakeSSX _ ZKX _ = ZSX shxTakeSSX p (_ :!% ssh1) (n :$% sh) = n :$% shxTakeSSX p ssh1 sh @@ -534,12 +475,6 @@ shxTakeSh :: forall sh sh' i proxy. proxy sh' -> ShX sh i -> ShX (sh ++ sh') i - shxTakeSh _ ZSX _ = ZSX shxTakeSh p (_ :$% ssh1) (n :$% sh) = n :$% shxTakeSh p ssh1 sh -shxDropSSX :: forall sh sh' i. StaticShX sh -> ShX (sh ++ sh') i -> ShX sh' i -shxDropSSX = coerce (listhDrop @i @()) - -shxDropSh :: forall sh sh' i. ShX sh i -> ShX (sh ++ sh') i -> ShX sh' i -shxDropSh = coerce (listhDrop @i @i) - {-# INLINEABLE shxTakeIx #-} shxTakeIx :: forall sh sh' i j. Proxy sh' -> IxX sh j -> ShX (sh ++ sh') i -> ShX sh i shxTakeIx _ (IxX ZX) _ = ZSX @@ -550,12 +485,6 @@ shxDropIx :: forall sh sh' i j. IxX sh j -> ShX (sh ++ sh') i -> ShX sh' i shxDropIx ZIX long = long shxDropIx (_ :.% short) long = case long of _ :$% long' -> shxDropIx short long' -shxInit :: forall n sh i. ShX (n : sh) i -> ShX (Init (n : sh)) i -shxInit = coerce (listhInit @i) - -shxLast :: forall n sh i. ShX (n : sh) i -> SMayNat i (Last (n : sh)) -shxLast = coerce (listhLast @i) - {-# INLINE shxZipWith #-} shxZipWith :: (forall n. SMayNat i n -> SMayNat j n -> SMayNat k n) -> ShX sh i -> ShX sh j -> ShX sh k @@ -589,22 +518,22 @@ shxCast' ssh sh = case shxCast ssh sh of -- * Static mixed shapes --- | The part of a shape that is statically known. (A newtype over 'ListH'.) +-- | The part of a shape that is statically known. (A newtype over 'ShX'.) type StaticShX :: [Maybe Nat] -> Type -newtype StaticShX sh = StaticShX (ListH sh ()) +newtype StaticShX sh = StaticShX (ShX sh ()) deriving (NFData) instance Eq (StaticShX sh) where _ == _ = True instance Ord (StaticShX sh) where compare _ _ = EQ pattern ZKX :: forall sh. () => sh ~ '[] => StaticShX sh -pattern ZKX = StaticShX ZH +pattern ZKX = StaticShX ZSX pattern (:!%) :: forall {sh1}. forall n sh. (n : sh ~ sh1) => SMayNat () n -> StaticShX sh -> StaticShX sh1 -pattern i :!% shl <- StaticShX (listhUncons -> Just (UnconsListHRes i (StaticShX -> shl))) +pattern i :!% shl <- StaticShX (shxUncons -> Just (UnconsShXRes i (StaticShX -> shl))) where i :!% StaticShX shl = case i of; SUnknown () -> StaticShX (() `ConsUnknown` shl); SKnown x -> StaticShX (x `ConsKnown` shl) infixr 3 :!% @@ -615,30 +544,30 @@ infixr 3 :!% deriving instance Show (StaticShX sh) #else instance Show (StaticShX sh) where - showsPrec _ (StaticShX l) = listhShow (fromSMayNat shows (shows . fromSNat)) l + showsPrec _ (StaticShX l) = shxShow (fromSMayNat shows (shows . fromSNat)) l #endif instance TestEquality StaticShX where - testEquality (StaticShX l1) (StaticShX l2) = listhEqType l1 l2 + testEquality (StaticShX l1) (StaticShX l2) = shxEqType l1 l2 ssxLength :: StaticShX sh -> Int -ssxLength (StaticShX l) = listhLength l +ssxLength (StaticShX l) = shxLength l ssxRank :: StaticShX sh -> SNat (Rank sh) -ssxRank (StaticShX l) = listhRank l +ssxRank (StaticShX l) = shxRank l -- | @ssxEqType = 'testEquality'@. Provided for consistency. ssxEqType :: StaticShX sh -> StaticShX sh' -> Maybe (sh :~: sh') ssxEqType = testEquality ssxAppend :: StaticShX sh -> StaticShX sh' -> StaticShX (sh ++ sh') -ssxAppend = coerce (listhAppend @_ @()) +ssxAppend = coerce (shxAppend @_ @()) ssxHead :: StaticShX (n : sh) -> SMayNat () n -ssxHead (StaticShX list) = listhHead list +ssxHead (StaticShX list) = shxHead list ssxTail :: StaticShX (n : sh) -> StaticShX sh -ssxTail (StaticShX list) = StaticShX (listhTail list) +ssxTail (StaticShX list) = StaticShX (shxTail list) ssxTakeIx :: forall sh sh' i. Proxy sh' -> IxX sh i -> StaticShX (sh ++ sh') -> StaticShX sh ssxTakeIx _ (IxX ZX) _ = ZKX @@ -649,16 +578,16 @@ ssxDropIx (IxX ZX) long = long ssxDropIx (IxX (_ ::% short)) long = case long of _ :!% long' -> ssxDropIx (IxX short) long' ssxDropSh :: forall sh sh' i. ShX sh i -> StaticShX (sh ++ sh') -> StaticShX sh' -ssxDropSh = coerce (listhDrop @() @i) +ssxDropSh = coerce (shxDropSh @_ @_ @() @i) ssxDropSSX :: forall sh sh'. StaticShX sh -> StaticShX (sh ++ sh') -> StaticShX sh' -ssxDropSSX = coerce (listhDrop @() @()) +ssxDropSSX = coerce (shxDropSh @_ @_ @() @()) ssxInit :: forall n sh. StaticShX (n : sh) -> StaticShX (Init (n : sh)) -ssxInit = coerce (listhInit @()) +ssxInit = coerce (shxInit @()) ssxLast :: forall n sh. StaticShX (n : sh) -> SMayNat () (Last (n : sh)) -ssxLast = coerce (listhLast @()) +ssxLast = coerce (shxLast @()) ssxReplicate :: SNat n -> StaticShX (Replicate n Nothing) ssxReplicate SZ = ZKX |