aboutsummaryrefslogtreecommitdiff
path: root/src/Data/Array/Mixed
diff options
context:
space:
mode:
authorTom Smeding <tom@tomsmeding.com>2024-06-13 13:09:04 +0200
committerTom Smeding <tom@tomsmeding.com>2024-06-13 13:09:04 +0200
commit20173c939486ed6e27b8170e94f666d8ae3df152 (patch)
tree36c02005c3f2a20567388c6291e54bc2e4a4e6db /src/Data/Array/Mixed
parent275847827d7550436eaf8cd10969f1430dae821d (diff)
Rename *LengthSNat to *Rank
Diffstat (limited to 'src/Data/Array/Mixed')
-rw-r--r--src/Data/Array/Mixed/Permutation.hs8
-rw-r--r--src/Data/Array/Mixed/Shape.hs14
-rw-r--r--src/Data/Array/Mixed/XArray.hs2
3 files changed, 10 insertions, 14 deletions
diff --git a/src/Data/Array/Mixed/Permutation.hs b/src/Data/Array/Mixed/Permutation.hs
index ca99b02..331d5e0 100644
--- a/src/Data/Array/Mixed/Permutation.hs
+++ b/src/Data/Array/Mixed/Permutation.hs
@@ -45,9 +45,9 @@ infixr 5 `PCons`
deriving instance Show (Perm list)
deriving instance Eq (Perm list)
-permLengthSNat :: Perm list -> SNat (Rank list)
-permLengthSNat PNil = SNat
-permLengthSNat (_ `PCons` l) | SNat <- permLengthSNat l = SNat
+permRank :: Perm list -> SNat (Rank list)
+permRank PNil = SNat
+permRank (_ `PCons` l) | SNat <- permRank l = SNat
permFromList :: [Int] -> (forall list. Perm list -> r) -> r
permFromList [] k = k PNil
@@ -67,7 +67,7 @@ permToList' = map fromIntegral . permToList
-- then @Nothing@ is returned.
permCheckPermutation :: forall r list. Perm list -> (IsPermutation list => r) -> Maybe r
permCheckPermutation = \p k ->
- let n = permLengthSNat p
+ let n = permRank p
in case (provePerm1 (Proxy @list) n p, provePerm2 (SNat @0) n p) of
(Just Refl, Just Refl) -> Just k
_ -> Nothing
diff --git a/src/Data/Array/Mixed/Shape.hs b/src/Data/Array/Mixed/Shape.hs
index e46105d..95cd4ef 100644
--- a/src/Data/Array/Mixed/Shape.hs
+++ b/src/Data/Array/Mixed/Shape.hs
@@ -81,9 +81,9 @@ listxFold f (x ::% xs) = f x <> listxFold f xs
listxLength :: ListX sh f -> Int
listxLength = getSum . listxFold (\_ -> Sum 1)
-listxLengthSNat :: ListX sh f -> SNat (Rank sh)
-listxLengthSNat ZX = SNat
-listxLengthSNat (_ ::% l) | SNat <- listxLengthSNat l = SNat
+listxRank :: ListX sh f -> SNat (Rank sh)
+listxRank ZX = SNat
+listxRank (_ ::% l) | SNat <- listxRank l = SNat
listxShow :: forall sh f. (forall n. f n -> ShowS) -> ListX sh f -> ShowS
listxShow f l = showString "[" . go "" l . showString "]"
@@ -265,8 +265,8 @@ instance NFData i => NFData (ShX sh i) where
shxLength :: ShX sh i -> Int
shxLength (ShX l) = listxLength l
-shxLengthSNat :: ShX sh f -> SNat (Rank sh)
-shxLengthSNat (ShX list) = listxLengthSNat list
+shxRank :: ShX sh f -> SNat (Rank sh)
+shxRank (ShX list) = listxRank list
-- | This is more than @geq@: it also checks that the integers (the unknown
-- dimensions) are the same.
@@ -344,10 +344,6 @@ shxEnum = \sh -> go sh id []
go ZSX f = (f ZIX :)
go (n :$% sh) f = foldr (.) id [go sh (f . (i :.%)) | i <- [0 .. fromSMayNat' n - 1]]
-shxRank :: ShX sh f -> SNat (Rank sh)
-shxRank ZSX = SNat
-shxRank (_ :$% sh) | SNat <- shxRank sh = SNat
-
-- * Static mixed shapes
diff --git a/src/Data/Array/Mixed/XArray.hs b/src/Data/Array/Mixed/XArray.hs
index 20f5c7a..08295cd 100644
--- a/src/Data/Array/Mixed/XArray.hs
+++ b/src/Data/Array/Mixed/XArray.hs
@@ -258,7 +258,7 @@ sumInner ssh ssh' arr
go :: XArray (sh ++ '[Flatten sh']) a -> XArray sh a
go (XArray arr')
| Refl <- lemRankApp ssh ssh'F
- , let sn = listxLengthSNat (let StaticShX l = ssh in l)
+ , let sn = listxRank (let StaticShX l = ssh in l)
= XArray (numEltSum1Inner sn arr')
in go $