diff options
Diffstat (limited to 'src/Data/Array/Mixed')
| -rw-r--r-- | src/Data/Array/Mixed/Permutation.hs | 8 | ||||
| -rw-r--r-- | src/Data/Array/Mixed/Shape.hs | 14 | ||||
| -rw-r--r-- | src/Data/Array/Mixed/XArray.hs | 2 | 
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 $ | 
