diff options
| author | Tom Smeding <tom@tomsmeding.com> | 2024-06-03 21:27:55 +0200 |
|---|---|---|
| committer | Tom Smeding <tom@tomsmeding.com> | 2024-06-03 21:27:55 +0200 |
| commit | 3286a65fe6e4735aaadef5addecbe3c3f7ed3468 (patch) | |
| tree | fb8787a3bc2b2740733a110c21c580d0c56b9381 /src/Data/Array/Nested/Internal/Shape.hs | |
| parent | ac061cf450b1c8e153de06f7b12256914c496788 (diff) | |
Rename *ToSNat to *LengthSNat
For consistency with existing functions
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) |