aboutsummaryrefslogtreecommitdiff
path: root/src/Data
diff options
context:
space:
mode:
Diffstat (limited to 'src/Data')
-rw-r--r--src/Data/Array/Nested/Internal/Shape.hs11
1 files changed, 11 insertions, 0 deletions
diff --git a/src/Data/Array/Nested/Internal/Shape.hs b/src/Data/Array/Nested/Internal/Shape.hs
index 0d75b04..99cca06 100644
--- a/src/Data/Array/Nested/Internal/Shape.hs
+++ b/src/Data/Array/Nested/Internal/Shape.hs
@@ -314,6 +314,14 @@ listsUncons :: ListS sh1 f -> Maybe (UnconsListSRes f sh1)
listsUncons (x ::$ sh') = Just (UnconsListSRes sh' x)
listsUncons ZS = Nothing
+listsEq :: TestEquality f => ListS sh f -> ListS sh' f -> Maybe (sh :~: sh')
+listsEq ZS ZS = Just Refl
+listsEq (n ::$ sh) (m ::$ sh')
+ | Just Refl <- testEquality n m
+ , Just Refl <- listsEq sh sh'
+ = Just Refl
+listsEq _ _ = Nothing
+
listsFmap :: (forall n. f n -> g n) -> ListS sh f -> ListS sh g
listsFmap _ ZS = ZS
listsFmap f (x ::$ xs) = f x ::$ listsFmap f xs
@@ -473,6 +481,9 @@ infixr 3 :$$
instance Show (ShS sh) where
showsPrec _ (ShS l) = listsShow (shows . fromSNat) l
+instance TestEquality ShS where
+ testEquality (ShS l1) (ShS l2) = listsEq l1 l2
+
shsLength :: ShS sh -> Int
shsLength (ShS l) = getSum (listsFold (\_ -> Sum 1) l)