diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Data/Array/Mixed.hs | 16 | ||||
| -rw-r--r-- | src/Data/Array/Nested/Internal.hs | 116 |
2 files changed, 86 insertions, 46 deletions
diff --git a/src/Data/Array/Mixed.hs b/src/Data/Array/Mixed.hs index d2765b6..8b90547 100644 --- a/src/Data/Array/Mixed.hs +++ b/src/Data/Array/Mixed.hs @@ -47,17 +47,17 @@ lemAppAssoc _ _ _ = unsafeCoerce Refl -- TODO: ListX? But if so, why is StaticShapeX not defined as a newtype -- over IxX (so that we can make IxX and StaticShapeX a newtype over ListX)? -type IxX :: Type -> [Maybe Nat] -> Type -data IxX i sh where - ZIX :: IxX i '[] - (:.@) :: forall n sh i. i -> IxX i sh -> IxX i (Just n : sh) - (:.?) :: forall sh i. i -> IxX i sh -> IxX i (Nothing : sh) -deriving instance Show i => Show (IxX i sh) -deriving instance Eq i => Eq (IxX i sh) +type IxX :: [Maybe Nat] -> Type -> Type +data IxX sh i where + ZIX :: IxX '[] i + (:.@) :: forall n sh i. i -> IxX sh i -> IxX (Just n : sh) i + (:.?) :: forall sh i. i -> IxX sh i -> IxX (Nothing : sh) i +deriving instance Show i => Show (IxX sh i) +deriving instance Eq i => Eq (IxX sh i) infixr 3 :.@ infixr 3 :.? -type IIxX = IxX Int +type IIxX sh = IxX sh Int -- | The part of a shape that is statically known. type StaticShapeX :: [Maybe Nat] -> Type diff --git a/src/Data/Array/Nested/Internal.hs b/src/Data/Array/Nested/Internal.hs index 9cabdc6..b758e55 100644 --- a/src/Data/Array/Nested/Internal.hs +++ b/src/Data/Array/Nested/Internal.hs @@ -1,8 +1,10 @@ {-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE DerivingVia #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE PolyKinds #-} @@ -850,59 +852,78 @@ instance (KnownINat n, Storable a, Num a) => Num (Ranked n (Primitive a)) where deriving via Ranked n (Primitive Int) instance KnownINat n => Num (Ranked n Int) deriving via Ranked n (Primitive Double) instance KnownINat n => Num (Ranked n Double) -type ListR :: Type -> INat -> Type -data ListR i n where - ZR :: ListR i Z - (:::) :: forall n i. i -> ListR i n -> ListR i (S n) -deriving instance Show i => Show (ListR i n) -deriving instance Eq i => Eq (ListR i n) +type ListR :: INat -> Type -> Type +data ListR n i where + ZR :: ListR Z i + (:::) :: forall n i. i -> ListR n i -> ListR (S n) i +deriving instance Show i => Show (ListR n i) +deriving instance Eq i => Eq (ListR n i) infixr 3 ::: +deriving stock instance Functor (ListR n) + +instance Foldable (ListR n) where + foldr f z l = foldr f z (listRToList l) + +listRToList :: ListR n i -> [i] +listRToList ZR = [] +listRToList (i ::: is) = i : listRToList is + -- | An index into a rank-typed array. -type IxR :: Type -> INat -> Type -newtype IxR i n = IxR (ListR i n) +type IxR :: INat -> Type -> Type +newtype IxR n i = IxR (ListR n i) deriving (Show, Eq) -pattern ZIR :: forall n i. () => n ~ Z => IxR i n +deriving newtype instance Functor (IxR n) + +instance Foldable (IxR n) where + foldr f z (IxR l) = foldr f z l + +pattern ZIR :: forall n i. () => n ~ Z => IxR n i pattern ZIR = IxR ZR pattern (:.:) :: forall {n1} {i}. forall n. ((S n) ~ n1) - => i -> IxR i n -> IxR i n1 + => i -> IxR n i -> IxR n1 i pattern i :.: sh <- (unconsIxR -> Just (UnconsIxRRes sh i)) where i :.: (IxR sh) = IxR (i ::: sh) {-# COMPLETE ZIR, (:.:) #-} infixr 3 :.: data UnconsIxRRes i n1 = - forall n. ((S n) ~ n1) => UnconsIxRRes (IxR i n) i -unconsIxR :: IxR i n1 -> Maybe (UnconsIxRRes i n1) + forall n. ((S n) ~ n1) => UnconsIxRRes (IxR n i) i +unconsIxR :: IxR n1 i -> Maybe (UnconsIxRRes i n1) unconsIxR (IxR sh) = case sh of i ::: sh' -> Just (UnconsIxRRes (IxR sh') i) ZR -> Nothing -type IIxR = IxR Int +type IIxR n = IxR n Int -type StaticShapeR :: Type -> INat -> Type -newtype StaticShapeR i n = StaticShapeR (ListR i n) +type StaticShapeR :: INat -> Type -> Type +newtype StaticShapeR n i = StaticShapeR (ListR n i) deriving (Show, Eq) -pattern ZSR :: forall n i. () => n ~ Z => StaticShapeR i n +deriving newtype instance Functor (StaticShapeR n) + +instance Foldable (StaticShapeR n) where + foldr f z (StaticShapeR l) = foldr f z l + +pattern ZSR :: forall n i. () => n ~ Z => StaticShapeR n i pattern ZSR = StaticShapeR ZR pattern (:$:) :: forall {n1} {i}. forall n. ((S n) ~ n1) - => i -> StaticShapeR i n -> StaticShapeR i n1 + => i -> StaticShapeR n i -> StaticShapeR n1 i pattern i :$: sh <- (unconsStaticShapeR -> Just (UnconsStaticShapeRRes sh i)) where i :$: (StaticShapeR sh) = StaticShapeR (i ::: sh) {-# COMPLETE ZSR, (:$:) #-} infixr 3 :$: data UnconsStaticShapeRRes i n1 = - forall n. ((S n) ~ n1) => UnconsStaticShapeRRes (StaticShapeR i n) i -unconsStaticShapeR :: StaticShapeR i n1 -> Maybe (UnconsStaticShapeRRes i n1) + forall n. ((S n) ~ n1) => UnconsStaticShapeRRes (StaticShapeR n i) i +unconsStaticShapeR :: StaticShapeR n1 i -> Maybe (UnconsStaticShapeRRes i n1) unconsStaticShapeR (StaticShapeR sh) = case sh of i ::: sh' -> Just (UnconsStaticShapeRRes (StaticShapeR sh') i) ZR -> Nothing @@ -1043,64 +1064,83 @@ instance (KnownShape sh, Storable a, Num a) => Num (Shaped sh (Primitive a)) whe deriving via Shaped sh (Primitive Int) instance KnownShape sh => Num (Shaped sh Int) deriving via Shaped sh (Primitive Double) instance KnownShape sh => Num (Shaped sh Double) -type ListS :: Type -> [Nat] -> Type -data ListS i n where - ZS :: ListS i '[] - (::$) :: forall n sh i. i -> ListS i sh -> ListS i (n : sh) -deriving instance Show i => Show (ListS i n) -deriving instance Eq i => Eq (ListS i n) +type ListS :: [Nat] -> Type -> Type +data ListS sh i where + ZS :: ListS '[] i + (::$) :: forall n sh i. i -> ListS sh i -> ListS (n : sh) i +deriving instance Show i => Show (ListS sh i) +deriving instance Eq i => Eq (ListS sh i) infixr 3 ::$ +deriving stock instance Functor (ListS sh) + +instance Foldable (ListS sh) where + foldr f z l = foldr f z (listSToList l) + +listSToList :: ListS sh i -> [i] +listSToList ZS = [] +listSToList (i ::$ is) = i : listSToList is + -- | An index into a shape-typed array. -- -- For convenience, this contains regular 'Int's instead of bounded integers -- (traditionally called \"@Fin@\"). Note that because the shape of a -- shape-typed array is known statically, you can also retrieve the array shape -- from a 'KnownShape' dictionary. -type IxS :: Type -> [Nat] -> Type -newtype IxS i sh = IxS (ListS i sh) +type IxS :: [Nat] -> Type -> Type +newtype IxS sh i = IxS (ListS sh i) deriving (Show, Eq) -pattern ZIS :: forall sh i. () => sh ~ '[] => IxS i sh +deriving newtype instance Functor (IxS sh) + +instance Foldable (IxS sh) where + foldr f z (IxS l) = foldr f z l + +pattern ZIS :: forall sh i. () => sh ~ '[] => IxS sh i pattern ZIS = IxS ZS pattern (:.$) :: forall {sh1} {i}. forall n sh. (n : sh ~ sh1) - => i -> IxS i sh -> IxS i sh1 + => i -> IxS sh i -> IxS sh1 i pattern i :.$ shl <- (unconsIxS -> Just (UnconsIxSRes shl i)) where i :.$ (IxS shl) = IxS (i ::$ shl) {-# COMPLETE ZIS, (:.$) #-} infixr 3 :.$ data UnconsIxSRes i sh1 = - forall n sh. (n : sh ~ sh1) => UnconsIxSRes (IxS i sh) i -unconsIxS :: IxS i sh1 -> Maybe (UnconsIxSRes i sh1) + forall n sh. (n : sh ~ sh1) => UnconsIxSRes (IxS sh i) i +unconsIxS :: IxS sh1 i -> Maybe (UnconsIxSRes i sh1) unconsIxS (IxS shl) = case shl of i ::$ shl' -> Just (UnconsIxSRes (IxS shl') i) ZS -> Nothing -type IIxS = IxS Int +type IIxS sh = IxS sh Int -type StaticShapeS :: Type -> [Nat] -> Type -newtype StaticShapeS i sh = StaticShapeS (ListS i sh) +type StaticShapeS :: [Nat] -> Type -> Type +newtype StaticShapeS sh i = StaticShapeS (ListS sh i) deriving (Show, Eq) -pattern ZSS :: forall sh i. () => sh ~ '[] => StaticShapeS i sh +deriving newtype instance Functor (StaticShapeS sh) + +instance Foldable (StaticShapeS sh) where + foldr f z (StaticShapeS l) = foldr f z l + +pattern ZSS :: forall sh i. () => sh ~ '[] => StaticShapeS sh i pattern ZSS = StaticShapeS ZS pattern (:$$) :: forall {sh1} {i}. forall n sh. (n : sh ~ sh1) - => i -> StaticShapeS i sh -> StaticShapeS i sh1 + => i -> StaticShapeS sh i -> StaticShapeS sh1 i pattern i :$$ shl <- (unconsStaticShapeS -> Just (UnconsStaticShapeSRes shl i)) where i :$$ (StaticShapeS shl) = StaticShapeS (i ::$ shl) {-# COMPLETE ZSS, (:$$) #-} infixr 3 :$$ data UnconsStaticShapeSRes i sh1 = - forall n sh. (n : sh ~ sh1) => UnconsStaticShapeSRes (StaticShapeS i sh) i -unconsStaticShapeS :: StaticShapeS i sh1 -> Maybe (UnconsStaticShapeSRes i sh1) + forall n sh. (n : sh ~ sh1) => UnconsStaticShapeSRes (StaticShapeS sh i) i +unconsStaticShapeS :: StaticShapeS sh1 i -> Maybe (UnconsStaticShapeSRes i sh1) unconsStaticShapeS (StaticShapeS shl) = case shl of i ::$ shl' -> Just (UnconsStaticShapeSRes (StaticShapeS shl') i) ZS -> Nothing |