diff options
Diffstat (limited to 'src/Data/Array/Nested/Internal/Shape.hs')
| -rw-r--r-- | src/Data/Array/Nested/Internal/Shape.hs | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/Data/Array/Nested/Internal/Shape.hs b/src/Data/Array/Nested/Internal/Shape.hs index 7d95f61..4fa4284 100644 --- a/src/Data/Array/Nested/Internal/Shape.hs +++ b/src/Data/Array/Nested/Internal/Shape.hs @@ -91,14 +91,14 @@ listrIndex SZ (x ::: _) = x listrIndex (SS i) (_ ::: xs) | Refl <- lemLeqSuccSucc (Proxy @k) (Proxy @n) = listrIndex i xs listrIndex _ ZR = error "k + 1 <= 0" -listrLengthSNat :: ListR n i -> SNat n -listrLengthSNat ZR = SNat -listrLengthSNat (_ ::: (sh :: ListR n i)) = snatSucc (listrLengthSNat sh) +listrRank :: ListR n i -> SNat n +listrRank ZR = SNat +listrRank (_ ::: (sh :: ListR n i)) = snatSucc (listrRank sh) listrPermutePrefix :: forall i n. [Int] -> ListR n i -> ListR n i listrPermutePrefix = \perm sh -> listrFromList perm $ \sperm -> - case (listrLengthSNat sperm, listrLengthSNat sh) of + case (listrRank sperm, listrRank sh) of (permlen@SNat, shlen@SNat) -> case cmpNat permlen shlen of LTI -> let (pre, post) = listrSplitAt permlen sh in listrAppend (applyPermRFull permlen sperm pre) post EQI -> let (pre, post) = listrSplitAt permlen sh in listrAppend (applyPermRFull permlen sperm pre) post @@ -168,8 +168,8 @@ ixrTail (IxR list) = IxR (listrTail list) ixrAppend :: forall n m i. IxR n i -> IxR m i -> IxR (n + m) i ixrAppend = coerce (listrAppend @_ @i) -ixrLengthSNat :: IxR n i -> SNat n -ixrLengthSNat (IxR sh) = listrLengthSNat sh +ixrRank :: IxR n i -> SNat n +ixrRank (IxR sh) = listrRank sh ixrPermutePrefix :: forall n i. [Int] -> IxR n i -> IxR n i ixrPermutePrefix = coerce (listrPermutePrefix @i) @@ -237,8 +237,8 @@ shrTail (ShR list) = ShR (listrTail list) shrAppend :: forall n m i. ShR n i -> ShR m i -> ShR (n + m) i shrAppend = coerce (listrAppend @_ @i) -shrLengthSNat :: ShR n i -> SNat n -shrLengthSNat (ShR sh) = listrLengthSNat sh +shrRank :: ShR n i -> SNat n +shrRank (ShR sh) = listrRank sh shrPermutePrefix :: forall n i. [Int] -> ShR n i -> ShR n i shrPermutePrefix = coerce (listrPermutePrefix @i) |