aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Data/Array/Nested/Permutation.hs56
-rw-r--r--src/Data/Array/Nested/Shaped.hs4
-rw-r--r--src/Data/Array/Nested/Shaped/Shape.hs14
-rw-r--r--src/Data/Array/XArray.hs2
4 files changed, 38 insertions, 38 deletions
diff --git a/src/Data/Array/Nested/Permutation.hs b/src/Data/Array/Nested/Permutation.hs
index f4ce90b..d2557b6 100644
--- a/src/Data/Array/Nested/Permutation.hs
+++ b/src/Data/Array/Nested/Permutation.hs
@@ -171,17 +171,17 @@ type family DropLen ref l where
DropLen '[] l = l
DropLen (_ : ref) (_ : xs) = DropLen ref xs
-listhTakeLen :: forall i is sh. Perm is -> ListH sh i -> ListH (TakeLen is sh) i
-listhTakeLen PNil _ = ZH
-listhTakeLen (_ `PCons` is) (n `ConsUnknown` sh) = n `ConsUnknown` listhTakeLen is sh
-listhTakeLen (_ `PCons` is) (n `ConsKnown` sh) = n `ConsKnown` listhTakeLen is sh
-listhTakeLen (_ `PCons` _) ZH = error "Permutation longer than shape"
+listhTakeLenPerm :: forall i is sh. Perm is -> ListH sh i -> ListH (TakeLen is sh) i
+listhTakeLenPerm PNil _ = ZH
+listhTakeLenPerm (_ `PCons` is) (n `ConsUnknown` sh) = n `ConsUnknown` listhTakeLenPerm is sh
+listhTakeLenPerm (_ `PCons` is) (n `ConsKnown` sh) = n `ConsKnown` listhTakeLenPerm is sh
+listhTakeLenPerm (_ `PCons` _) ZH = error "Permutation longer than shape"
-listhDropLen :: forall i is sh. Perm is -> ListH sh i -> ListH (DropLen is sh) i
-listhDropLen PNil sh = sh
-listhDropLen (_ `PCons` is) (_ `ConsUnknown` sh) = listhDropLen is sh
-listhDropLen (_ `PCons` is) (_ `ConsKnown` sh) = listhDropLen is sh
-listhDropLen (_ `PCons` _) ZH = error "Permutation longer than shape"
+listhDropLenPerm :: forall i is sh. Perm is -> ListH sh i -> ListH (DropLen is sh) i
+listhDropLenPerm PNil sh = sh
+listhDropLenPerm (_ `PCons` is) (_ `ConsUnknown` sh) = listhDropLenPerm is sh
+listhDropLenPerm (_ `PCons` is) (_ `ConsKnown` sh) = listhDropLenPerm is sh
+listhDropLenPerm (_ `PCons` _) ZH = error "Permutation longer than shape"
listhPermute :: forall i is sh. Perm is -> ListH sh i -> ListH (Permute is sh) i
listhPermute PNil _ = ZH
@@ -202,13 +202,13 @@ listhIndex (SS (i :: SNat k')) ((_ :: SNat n) `ConsKnown` (sh :: ListH sh' i))
listhIndex _ ZH = error "Index into empty shape"
listhPermutePrefix :: forall i is sh. Perm is -> ListH sh i -> ListH (PermutePrefix is sh) i
-listhPermutePrefix perm sh = listhAppend (listhPermute perm (listhTakeLen perm sh)) (listhDropLen perm sh)
+listhPermutePrefix perm sh = listhAppend (listhPermute perm (listhTakeLenPerm perm sh)) (listhDropLenPerm perm sh)
-ssxTakeLen :: forall is sh. Perm is -> StaticShX sh -> StaticShX (TakeLen is sh)
-ssxTakeLen = coerce (listhTakeLen @())
+ssxTakeLenPerm :: forall is sh. Perm is -> StaticShX sh -> StaticShX (TakeLen is sh)
+ssxTakeLenPerm = coerce (listhTakeLenPerm @())
-ssxDropLen :: Perm is -> StaticShX sh -> StaticShX (DropLen is sh)
-ssxDropLen = coerce (listhDropLen @())
+ssxDropLenPerm :: Perm is -> StaticShX sh -> StaticShX (DropLen is sh)
+ssxDropLenPerm = coerce (listhDropLenPerm @())
ssxPermute :: Perm is -> StaticShX sh -> StaticShX (Permute is sh)
ssxPermute = coerce (listhPermute @())
@@ -219,11 +219,11 @@ ssxIndex k = coerce (listhIndex @() k)
ssxPermutePrefix :: Perm is -> StaticShX sh -> StaticShX (PermutePrefix is sh)
ssxPermutePrefix = coerce (listhPermutePrefix @())
-shxTakeLen :: forall is sh. Perm is -> IShX sh -> IShX (TakeLen is sh)
-shxTakeLen = coerce (listhTakeLen @Int)
+shxTakeLenPerm :: forall is sh. Perm is -> IShX sh -> IShX (TakeLen is sh)
+shxTakeLenPerm = coerce (listhTakeLenPerm @Int)
-shxDropLen :: Perm is -> IShX sh -> IShX (DropLen is sh)
-shxDropLen = coerce (listhDropLen @Int)
+shxDropLenPerm :: Perm is -> IShX sh -> IShX (DropLen is sh)
+shxDropLenPerm = coerce (listhDropLenPerm @Int)
shxPermute :: Perm is -> IShX sh -> IShX (Permute is sh)
shxPermute = coerce (listhPermute @Int)
@@ -235,15 +235,15 @@ shxPermutePrefix :: Perm is -> IShX sh -> IShX (PermutePrefix is sh)
shxPermutePrefix = coerce (listhPermutePrefix @Int)
-listxTakeLen :: forall i is sh. Perm is -> ListX sh i -> ListX (TakeLen is sh) i
-listxTakeLen PNil _ = ZX
-listxTakeLen (_ `PCons` is) (n ::% sh) = n ::% listxTakeLen is sh
-listxTakeLen (_ `PCons` _) ZX = error "Permutation longer than shape"
+listxTakeLenPerm :: forall i is sh. Perm is -> ListX sh i -> ListX (TakeLen is sh) i
+listxTakeLenPerm PNil _ = ZX
+listxTakeLenPerm (_ `PCons` is) (n ::% sh) = n ::% listxTakeLenPerm is sh
+listxTakeLenPerm (_ `PCons` _) ZX = error "Permutation longer than shape"
-listxDropLen :: forall i is sh. Perm is -> ListX sh i -> ListX (DropLen is sh) i
-listxDropLen PNil sh = sh
-listxDropLen (_ `PCons` is) (_ ::% sh) = listxDropLen is sh
-listxDropLen (_ `PCons` _) ZX = error "Permutation longer than shape"
+listxDropLenPerm :: forall i is sh. Perm is -> ListX sh i -> ListX (DropLen is sh) i
+listxDropLenPerm PNil sh = sh
+listxDropLenPerm (_ `PCons` is) (_ ::% sh) = listxDropLenPerm is sh
+listxDropLenPerm (_ `PCons` _) ZX = error "Permutation longer than shape"
listxPermute :: forall i is sh. Perm is -> ListX sh i -> ListX (Permute is sh) i
listxPermute PNil _ = ZX
@@ -256,7 +256,7 @@ listxIndex (SS i) (_ ::% sh) = listxIndex i sh
listxIndex _ ZX = error "Index into empty shape"
listxPermutePrefix :: forall i is sh. Perm is -> ListX sh i -> ListX (PermutePrefix is sh) i
-listxPermutePrefix perm sh = listxAppend (listxPermute perm (listxTakeLen perm sh)) (listxDropLen perm sh)
+listxPermutePrefix perm sh = listxAppend (listxPermute perm (listxTakeLenPerm perm sh)) (listxDropLenPerm perm sh)
ixxPermutePrefix :: forall i is sh. Perm is -> IxX sh i -> IxX (PermutePrefix is sh) i
ixxPermutePrefix = coerce (listxPermutePrefix @i)
diff --git a/src/Data/Array/Nested/Shaped.hs b/src/Data/Array/Nested/Shaped.hs
index d57106a..62867a1 100644
--- a/src/Data/Array/Nested/Shaped.hs
+++ b/src/Data/Array/Nested/Shaped.hs
@@ -116,8 +116,8 @@ stranspose perm sarr@(Shaped arr)
| Refl <- lemRankMapJust (sshape sarr)
, Refl <- lemTakeLenMapJust perm (sshape sarr)
, Refl <- lemDropLenMapJust perm (sshape sarr)
- , Refl <- lemPermuteMapJust perm (shsTakeLen perm (sshape sarr))
- , Refl <- lemMapJustApp (shsPermute perm (shsTakeLen perm (sshape sarr))) (Proxy @(DropLen is sh))
+ , Refl <- lemPermuteMapJust perm (shsTakeLenPerm perm (sshape sarr))
+ , Refl <- lemMapJustApp (shsPermute perm (shsTakeLenPerm perm (sshape sarr))) (Proxy @(DropLen is sh))
= Shaped (mtranspose perm arr)
sappend :: Elt a => Shaped (n : sh) a -> Shaped (m : sh) a -> Shaped (n + m : sh) a
diff --git a/src/Data/Array/Nested/Shaped/Shape.hs b/src/Data/Array/Nested/Shaped/Shape.hs
index ef91c7b..f83a065 100644
--- a/src/Data/Array/Nested/Shaped/Shape.hs
+++ b/src/Data/Array/Nested/Shaped/Shape.hs
@@ -424,17 +424,17 @@ shsAppend =
:: MapJust sh ++ MapJust sh' :~: MapJust (sh ++ sh')) $
coerce (shxAppend @_ @_ @Int)
-shsTakeLen :: forall is sh. Perm is -> ShS sh -> ShS (TakeLen is sh)
-shsTakeLen =
+shsTakeLenPerm :: forall is sh. Perm is -> ShS sh -> ShS (TakeLen is sh)
+shsTakeLenPerm =
gcastWith (unsafeCoerceRefl
:: TakeLen is (MapJust sh) :~: MapJust (TakeLen is sh)) $
- coerce shxTakeLen
+ coerce shxTakeLenPerm
-shsDropLen :: forall is sh. Perm is -> ShS sh -> ShS (DropLen is sh)
-shsDropLen =
+shsDropLenPerm :: forall is sh. Perm is -> ShS sh -> ShS (DropLen is sh)
+shsDropLenPerm =
gcastWith (unsafeCoerceRefl
:: DropLen is (MapJust sh) :~: MapJust (DropLen is sh)) $
- coerce shxDropLen
+ coerce shxDropLenPerm
shsPermute :: forall is sh. Perm is -> ShS sh -> ShS (Permute is sh)
shsPermute =
@@ -455,7 +455,7 @@ shsPermutePrefix perm (ShS shx)
| Refl <- lemTakeLenMapJust perm sh
, Refl <- lemDropLenMapJust perm sh
, Refl <- lemPermuteMapJust perm sh
- , Refl <- lemMapJustApp (shsPermute perm (shsTakeLen perm sh)) (shsDropLen perm sh) -}
+ , Refl <- lemMapJustApp (shsPermute perm (shsTakeLenPerm perm sh)) (shsDropLenPerm perm sh) -}
= gcastWith (unsafeCoerceRefl
:: Permute is (TakeLen is (MapJust sh))
++ DropLen is (MapJust sh)
diff --git a/src/Data/Array/XArray.hs b/src/Data/Array/XArray.hs
index 42aff93..9f3ee34 100644
--- a/src/Data/Array/XArray.hs
+++ b/src/Data/Array/XArray.hs
@@ -232,7 +232,7 @@ transpose :: forall is sh a. (IsPermutation is, Rank is <= Rank sh)
-> XArray (PermutePrefix is sh) a
transpose ssh perm (XArray arr)
| Dict <- lemKnownNatRankSSX ssh
- , Refl <- lemRankApp (ssxPermute perm (ssxTakeLen perm ssh)) (ssxDropLen perm ssh)
+ , Refl <- lemRankApp (ssxPermute perm (ssxTakeLenPerm perm ssh)) (ssxDropLenPerm perm ssh)
, Refl <- lemRankPermute (Proxy @(TakeLen is sh)) perm
, Refl <- lemRankDropLen ssh perm
#if MIN_VERSION_GLASGOW_HASKELL(9,8,0,0)
generated by cgit v1.3 (git 2.53.0) at 2026-04-10 00:17:34 +0200