diff options
| author | Tom Smeding <tom@tomsmeding.com> | 2024-07-24 12:10:05 +0200 |
|---|---|---|
| committer | Tom Smeding <tom@tomsmeding.com> | 2024-07-24 12:10:05 +0200 |
| commit | a872f0e171825654c9559fd963f447b326d88400 (patch) | |
| tree | 84785c8f6cc1d87485ba4d193c2290e1c239687f /src | |
| parent | f42b2b139ed8377bcf63d7a28db237350d3cb773 (diff) | |
Make ShS an instance of TestEquality
Diffstat (limited to 'src')
| -rw-r--r-- | src/Data/Array/Nested/Internal/Shape.hs | 11 |
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) |