diff options
| author | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2026-04-04 23:08:58 +0200 |
|---|---|---|
| committer | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2026-04-04 23:52:03 +0200 |
| commit | 67b62499a6d60fed9489f0371a8c841beb0c308f (patch) | |
| tree | b83d488760d2fcc6cf4be73c890824e8e6bc2480 /src/Data/Array/Nested/Ranked | |
| parent | dec7d6c47fe9b783e1a98008a4efffb77df6f393 (diff) | |
Use lazilyConcat for listxAppend
Diffstat (limited to 'src/Data/Array/Nested/Ranked')
| -rw-r--r-- | src/Data/Array/Nested/Ranked/Shape.hs | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/Data/Array/Nested/Ranked/Shape.hs b/src/Data/Array/Nested/Ranked/Shape.hs index 4eef090..687df69 100644 --- a/src/Data/Array/Nested/Ranked/Shape.hs +++ b/src/Data/Array/Nested/Ranked/Shape.hs @@ -119,9 +119,10 @@ listrRank :: ListR n i -> SNat n listrRank ZR = SNat listrRank (_ ::: sh) = snatSucc (listrRank sh) +-- lemReplicatePlusApp requires SNat that would cause overhead (not benchmarked) listrAppend :: forall n m i. ListR n i -> ListR m i -> ListR (n + m) i -listrAppend ZR sh = sh -listrAppend (x ::: xs) sh = x ::: listrAppend xs sh +listrAppend = gcastWith (unsafeCoerceRefl :: Replicate (n + m) (Nothing @Nat) :~: Replicate n Nothing ++ Replicate m Nothing) $ + coerce (listxAppend @_ @_ @i) {-# INLINE listrFromList #-} listrFromList :: SNat n -> [i] -> ListR n i |