From a872f0e171825654c9559fd963f447b326d88400 Mon Sep 17 00:00:00 2001 From: Tom Smeding Date: Wed, 24 Jul 2024 12:10:05 +0200 Subject: Make ShS an instance of TestEquality --- src/Data/Array/Nested/Internal/Shape.hs | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'src/Data/Array/Nested') 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) -- cgit v1.2.3-70-g09d2