diff options
| author | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2025-12-17 19:06:38 +0100 |
|---|---|---|
| committer | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2025-12-17 23:51:46 +0100 |
| commit | fe034ff95a1f299ed140f37e416b5562cd423457 (patch) | |
| tree | 5caf8da32f3dfd713c9f7ca064adfd3d932fd9c4 /src/Data/Array/Nested/Permutation.hs | |
| parent | 429416f327a94947c0d42ccea8906cd22bae64b4 (diff) | |
Make List?, except ListH, less general
Diffstat (limited to 'src/Data/Array/Nested/Permutation.hs')
| -rw-r--r-- | src/Data/Array/Nested/Permutation.hs | 17 |
1 files changed, 7 insertions, 10 deletions
diff --git a/src/Data/Array/Nested/Permutation.hs b/src/Data/Array/Nested/Permutation.hs index c3d2075..ecdb06d 100644 --- a/src/Data/Array/Nested/Permutation.hs +++ b/src/Data/Array/Nested/Permutation.hs @@ -18,7 +18,6 @@ module Data.Array.Nested.Permutation where import Data.Coerce (coerce) -import Data.Functor.Const import Data.List (sort) import Data.Maybe (fromMaybe) import Data.Proxy @@ -236,33 +235,31 @@ shxPermutePrefix :: Perm is -> IShX sh -> IShX (PermutePrefix is sh) shxPermutePrefix = coerce (listhPermutePrefix @Int) -listxTakeLen :: forall f is sh. Perm is -> ListX sh f -> ListX (TakeLen is sh) f +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" -listxDropLen :: forall f is sh. Perm is -> ListX sh f -> ListX (DropLen is sh) f +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" -listxPermute :: forall f is sh. Perm is -> ListX sh f -> ListX (Permute is sh) f +listxPermute :: forall i is sh. Perm is -> ListX sh i -> ListX (Permute is sh) i listxPermute PNil _ = ZX listxPermute (i `PCons` (is :: Perm is')) (sh :: ListX sh f) = listxIndex i sh ::% listxPermute is sh -listxIndex :: forall f i sh. SNat i -> ListX sh f -> f (Index i sh) +listxIndex :: forall j i sh. SNat i -> ListX sh j -> j listxIndex SZ (n ::% _) = n -listxIndex (SS (i :: SNat i')) ((_ :: f n) ::% (sh :: ListX sh' f)) - | Refl <- lemIndexSucc (Proxy @i') (Proxy @n) (Proxy @sh') - = listxIndex i sh +listxIndex (SS i) (_ ::% sh) = listxIndex i sh listxIndex _ ZX = error "Index into empty shape" -listxPermutePrefix :: forall f is sh. Perm is -> ListX sh f -> ListX (PermutePrefix is sh) f +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) ixxPermutePrefix :: forall i is sh. Perm is -> IxX sh i -> IxX (PermutePrefix is sh) i -ixxPermutePrefix = coerce (listxPermutePrefix @(Const i)) +ixxPermutePrefix = coerce (listxPermutePrefix @i) -- * Operations on permutations |