diff options
| author | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2025-12-15 22:17:34 +0100 |
|---|---|---|
| committer | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2025-12-16 09:55:09 +0100 |
| commit | 824078db9bc0b26bdde282f28ce7805c634101e2 (patch) | |
| tree | 20c931ca2fc2e1bf0bf0a61df764663949f3aa95 /src/Data/Array/Nested/Permutation.hs | |
| parent | 8579a03c5ae8f4812b72d477251a614d820dd1fc (diff) | |
Simplify the signature of fooIndex
Diffstat (limited to 'src/Data/Array/Nested/Permutation.hs')
| -rw-r--r-- | src/Data/Array/Nested/Permutation.hs | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/src/Data/Array/Nested/Permutation.hs b/src/Data/Array/Nested/Permutation.hs index 8b46d81..e458806 100644 --- a/src/Data/Array/Nested/Permutation.hs +++ b/src/Data/Array/Nested/Permutation.hs @@ -185,14 +185,14 @@ listxDropLen (_ `PCons` _) ZX = error "Permutation longer than shape" listxPermute :: forall f is sh. Perm is -> ListX sh f -> ListX (Permute is sh) f listxPermute PNil _ = ZX listxPermute (i `PCons` (is :: Perm is')) (sh :: ListX sh f) = - listxIndex (Proxy @is') (Proxy @sh) i sh ::% listxPermute is sh + listxIndex i sh ::% listxPermute is sh -listxIndex :: forall f is shT i sh. Proxy is -> Proxy shT -> SNat i -> ListX sh f -> f (Index i sh) -listxIndex _ _ SZ (n ::% _) = n -listxIndex p pT (SS (i :: SNat i')) ((_ :: f n) ::% (sh :: ListX sh' f)) +listxIndex :: forall f i sh. SNat i -> ListX sh f -> f (Index i sh) +listxIndex SZ (n ::% _) = n +listxIndex (SS (i :: SNat i')) ((_ :: f n) ::% (sh :: ListX sh' f)) | Refl <- lemIndexSucc (Proxy @i') (Proxy @n) (Proxy @sh') - = listxIndex p pT i sh -listxIndex _ _ _ ZX = error "Index into empty shape" + = 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 perm sh = listxAppend (listxPermute perm (listxTakeLen perm sh)) (listxDropLen perm sh) @@ -209,8 +209,8 @@ ssxDropLen = coerce (listxDropLen @(SMayNat ())) ssxPermute :: Perm is -> StaticShX sh -> StaticShX (Permute is sh) ssxPermute = coerce (listxPermute @(SMayNat ())) -ssxIndex :: Proxy is -> Proxy shT -> SNat i -> StaticShX sh -> SMayNat () (Index i sh) -ssxIndex p1 p2 i = coerce (listxIndex @(SMayNat ()) p1 p2 i) +ssxIndex :: SNat i -> StaticShX sh -> SMayNat () (Index i sh) +ssxIndex i = coerce (listxIndex @(SMayNat ()) i) ssxPermutePrefix :: Perm is -> StaticShX sh -> StaticShX (PermutePrefix is sh) ssxPermutePrefix = coerce (listxPermutePrefix @(SMayNat ())) @@ -224,8 +224,8 @@ shxDropLen = coerce (listxDropLen @(SMayNat Int)) shxPermute :: Perm is -> IShX sh -> IShX (Permute is sh) shxPermute = coerce (listxPermute @(SMayNat Int)) -shxIndex :: Proxy is -> Proxy shT -> SNat i -> IShX sh -> SMayNat Int (Index i sh) -shxIndex p1 p2 i = coerce (listxIndex @(SMayNat Int) p1 p2 i) +shxIndex :: SNat i -> IShX sh -> SMayNat Int (Index i sh) +shxIndex i = coerce (listxIndex @(SMayNat Int) i) shxPermutePrefix :: Perm is -> IShX sh -> IShX (PermutePrefix is sh) shxPermutePrefix = coerce (listxPermutePrefix @(SMayNat Int)) |