aboutsummaryrefslogtreecommitdiff
path: root/src/Data
diff options
context:
space:
mode:
Diffstat (limited to 'src/Data')
-rw-r--r--src/Data/Array/Mixed/Shape.hs16
1 files changed, 16 insertions, 0 deletions
diff --git a/src/Data/Array/Mixed/Shape.hs b/src/Data/Array/Mixed/Shape.hs
index 1285aa1..a8f58ef 100644
--- a/src/Data/Array/Mixed/Shape.hs
+++ b/src/Data/Array/Mixed/Shape.hs
@@ -70,6 +70,14 @@ listxUncons :: ListX sh1 f -> Maybe (UnconsListXRes f sh1)
listxUncons (i ::% shl') = Just (UnconsListXRes shl' i)
listxUncons ZX = Nothing
+listxEq :: TestEquality f => ListX sh f -> ListX sh' f -> Maybe (sh :~: sh')
+listxEq ZX ZX = Just Refl
+listxEq (n ::% sh) (m ::% sh')
+ | Just Refl <- testEquality n m
+ , Just Refl <- listxEq sh sh'
+ = Just Refl
+listxEq _ _ = Nothing
+
listxFmap :: (forall n. f n -> g n) -> ListX sh f -> ListX sh g
listxFmap _ ZX = ZX
listxFmap f (x ::% xs) = f x ::% listxFmap f xs
@@ -224,6 +232,11 @@ instance (NFData i, forall m. NFData (f m)) => NFData (SMayNat i f n) where
rnf (SUnknown i) = rnf i
rnf (SKnown x) = rnf x
+instance TestEquality f => TestEquality (SMayNat i f) where
+ testEquality SUnknown{} SUnknown{} = Just Refl
+ testEquality (SKnown n) (SKnown m) | Just Refl <- testEquality n m = Just Refl
+ testEquality _ _ = Nothing
+
fromSMayNat :: (n ~ Nothing => i -> r)
-> (forall m. n ~ Just m => f m -> r)
-> SMayNat i f n -> r
@@ -388,6 +401,9 @@ infixr 3 :!%
instance Show (StaticShX sh) where
showsPrec _ (StaticShX l) = listxShow (fromSMayNat shows (shows . fromSNat)) l
+instance TestEquality StaticShX where
+ testEquality (StaticShX l1) (StaticShX l2) = listxEq l1 l2
+
ssxLength :: StaticShX sh -> Int
ssxLength (StaticShX l) = listxLength l