diff options
Diffstat (limited to 'src/Data/Array/Nested/Permutation.hs')
| -rw-r--r-- | src/Data/Array/Nested/Permutation.hs | 36 |
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 |
