aboutsummaryrefslogtreecommitdiff
path: root/src/Data/Array/Nested/Permutation.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/Data/Array/Nested/Permutation.hs')
-rw-r--r--src/Data/Array/Nested/Permutation.hs36
1 files changed, 18 insertions, 18 deletions
diff --git a/src/Data/Array/Nested/Permutation.hs b/src/Data/Array/Nested/Permutation.hs
index e520e0f..f1485b3 100644
--- a/src/Data/Array/Nested/Permutation.hs
+++ b/src/Data/Array/Nested/Permutation.hs
@@ -172,60 +172,60 @@ type family DropLen ref l where
DropLen '[] l = l
DropLen (_ : ref) (_ : xs) = DropLen ref xs
-listhTakeLen :: forall f is sh. Perm is -> ListH sh f -> ListH (TakeLen is sh) f
+listhTakeLen :: forall i is sh. Perm is -> ListH sh i -> ListH (TakeLen is sh) i
listhTakeLen PNil _ = ZH
listhTakeLen (_ `PCons` is) (n ::# sh) = n ::# listhTakeLen is sh
listhTakeLen (_ `PCons` _) ZH = error "Permutation longer than shape"
-listhDropLen :: forall f is sh. Perm is -> ListH sh f -> ListH (DropLen is sh) f
+listhDropLen :: forall i is sh. Perm is -> ListH sh i -> ListH (DropLen is sh) i
listhDropLen PNil sh = sh
listhDropLen (_ `PCons` is) (_ ::# sh) = listhDropLen is sh
listhDropLen (_ `PCons` _) ZH = error "Permutation longer than shape"
-listhPermute :: forall f is sh. Perm is -> ListH sh f -> ListH (Permute is sh) f
+listhPermute :: forall i is sh. Perm is -> ListH sh i -> ListH (Permute is sh) i
listhPermute PNil _ = ZH
-listhPermute (i `PCons` (is :: Perm is')) (sh :: ListH sh f) =
+listhPermute (i `PCons` (is :: Perm is')) (sh :: ListH sh i) =
listhIndex (Proxy @is') (Proxy @sh) i sh ::# listhPermute is sh
-listhIndex :: forall f is shT i sh. Proxy is -> Proxy shT -> SNat i -> ListH sh f -> f (Index i sh)
+listhIndex :: forall i is shT k sh. Proxy is -> Proxy shT -> SNat k -> ListH sh i -> SMayNat i (Index k sh)
listhIndex _ _ SZ (n ::# _) = n
-listhIndex p pT (SS (i :: SNat i')) ((_ :: f n) ::# (sh :: ListH sh' f))
- | Refl <- lemIndexSucc (Proxy @i') (Proxy @n) (Proxy @sh')
+listhIndex p pT (SS (i :: SNat k')) ((_ :: SMayNat i n) ::# (sh :: ListH sh' i))
+ | Refl <- lemIndexSucc (Proxy @k') (Proxy @n) (Proxy @sh')
= listhIndex p pT i sh
listhIndex _ _ _ ZH = error "Index into empty shape"
-listhPermutePrefix :: forall f is sh. Perm is -> ListH sh f -> ListH (PermutePrefix is sh) f
+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)
ssxTakeLen :: forall is sh. Perm is -> StaticShX sh -> StaticShX (TakeLen is sh)
-ssxTakeLen = coerce (listhTakeLen @(SMayNat ()))
+ssxTakeLen = coerce (listhTakeLen @())
ssxDropLen :: Perm is -> StaticShX sh -> StaticShX (DropLen is sh)
-ssxDropLen = coerce (listhDropLen @(SMayNat ()))
+ssxDropLen = coerce (listhDropLen @())
ssxPermute :: Perm is -> StaticShX sh -> StaticShX (Permute is sh)
-ssxPermute = coerce (listhPermute @(SMayNat ()))
+ssxPermute = coerce (listhPermute @())
ssxIndex :: Proxy is -> Proxy shT -> SNat i -> StaticShX sh -> SMayNat () (Index i sh)
-ssxIndex p1 p2 i = coerce (listhIndex @(SMayNat ()) p1 p2 i)
+ssxIndex p1 p2 i = coerce (listhIndex @() p1 p2 i)
ssxPermutePrefix :: Perm is -> StaticShX sh -> StaticShX (PermutePrefix is sh)
-ssxPermutePrefix = coerce (listhPermutePrefix @(SMayNat ()))
+ssxPermutePrefix = coerce (listhPermutePrefix @())
shxTakeLen :: forall is sh. Perm is -> IShX sh -> IShX (TakeLen is sh)
-shxTakeLen = coerce (listhTakeLen @(SMayNat Int))
+shxTakeLen = coerce (listhTakeLen @Int)
shxDropLen :: Perm is -> IShX sh -> IShX (DropLen is sh)
-shxDropLen = coerce (listhDropLen @(SMayNat Int))
+shxDropLen = coerce (listhDropLen @Int)
shxPermute :: Perm is -> IShX sh -> IShX (Permute is sh)
-shxPermute = coerce (listhPermute @(SMayNat Int))
+shxPermute = coerce (listhPermute @Int)
shxIndex :: Proxy is -> Proxy shT -> SNat i -> IShX sh -> SMayNat Int (Index i sh)
-shxIndex p1 p2 i = coerce (listhIndex @(SMayNat Int) p1 p2 i)
+shxIndex p1 p2 i = coerce (listhIndex @Int p1 p2 i)
shxPermutePrefix :: Perm is -> IShX sh -> IShX (PermutePrefix is sh)
-shxPermutePrefix = coerce (listhPermutePrefix @(SMayNat Int))
+shxPermutePrefix = coerce (listhPermutePrefix @Int)
listxTakeLen :: forall f is sh. Perm is -> ListX sh f -> ListX (TakeLen is sh) f