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 4cc58dd..bce85b0 100644 --- a/src/Data/Array/Nested/Internal/Shape.hs +++ b/src/Data/Array/Nested/Internal/Shape.hs @@ -85,14 +85,14 @@ listrIndex SZ (x ::: _) = x listrIndex (SS i) (_ ::: xs) | Refl <- lemLeqSuccSucc (Proxy @k) (Proxy @n) = listrIndex i xs listrIndex _ ZR = error "k + 1 <= 0" -listrToSNat :: ListR n i -> SNat n -listrToSNat ZR = SNat -listrToSNat (_ ::: (l :: ListR n i)) | SNat <- listrToSNat l, Dict <- lemKnownNatSucc @n = SNat +listrLengthSNat :: ListR n i -> SNat n +listrLengthSNat ZR = SNat +listrLengthSNat (_ ::: (sh :: ListR n i)) = snatSucc (listrLengthSNat sh) listrPermutePrefix :: forall i n. [Int] -> ListR n i -> ListR n i listrPermutePrefix = \perm sh -> listrFromList perm $ \sperm -> - case (listrToSNat sperm, listrToSNat sh) of + case (listrLengthSNat sperm, listrLengthSNat 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 @@ -156,8 +156,8 @@ ixCvtRX (n :.: (idx :: IxR m Int)) = ixrTail :: IxR (n + 1) i -> IxR n i ixrTail (IxR list) = IxR (listrTail list) -ixrToSNat :: IxR n i -> SNat n -ixrToSNat (IxR sh) = listrToSNat sh +ixrLengthSNat :: IxR n i -> SNat n +ixrLengthSNat (IxR sh) = listrLengthSNat sh ixrPermutePrefix :: forall n i. [Int] -> IxR n i -> IxR n i ixrPermutePrefix = coerce (listrPermutePrefix @i) @@ -219,8 +219,8 @@ shrSize (n :$: sh) = n * shrSize sh shrTail :: ShR (n + 1) i -> ShR n i shrTail (ShR list) = ShR (listrTail list) -shrToSNat :: ShR n i -> SNat n -shrToSNat (ShR sh) = listrToSNat sh +shrLengthSNat :: ShR n i -> SNat n +shrLengthSNat (ShR sh) = listrLengthSNat sh shrPermutePrefix :: forall n i. [Int] -> ShR n i -> ShR n i shrPermutePrefix = coerce (listrPermutePrefix @i) |