Get rid of ListH

1 files changed, 32 insertions, 46 deletions

diff --git a/src/Data/Array/Nested/Permutation.hs b/src/Data/Array/Nested/Permutation.hs
index b6e5f47..ee79ecf 100644
--- a/src/Data/Array/Nested/Permutation.hs
+++ b/src/Data/Array/Nested/Permutation.hs
@@ -172,68 +172,54 @@ type family DropLen ref l where
   DropLen '[] l = l
   DropLen (_ : ref) (_ : xs) = DropLen ref xs
 
-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"
+shxTakeLenPerm :: forall i is sh. Perm is -> ShX sh i -> ShX (TakeLen is sh) i
+shxTakeLenPerm PNil _ = ZSX
+shxTakeLenPerm (_ `PCons` is) (n `ConsUnknown` sh) = n `ConsUnknown` shxTakeLenPerm is sh
+shxTakeLenPerm (_ `PCons` is) (n `ConsKnown` sh) = n `ConsKnown` shxTakeLenPerm is sh
+shxTakeLenPerm (_ `PCons` _) ZSX = 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"
+shxDropLenPerm :: forall i is sh. Perm is -> ShX sh i -> ShX (DropLen is sh) i
+shxDropLenPerm PNil sh = sh
+shxDropLenPerm (_ `PCons` is) (_ `ConsUnknown` sh) = shxDropLenPerm is sh
+shxDropLenPerm (_ `PCons` is) (_ `ConsKnown` sh) = shxDropLenPerm is sh
+shxDropLenPerm (_ `PCons` _) ZSX = error "Permutation longer than shape"
 
-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 i) =
-  case listhIndex i sh of
-    SUnknown x -> x `ConsUnknown` listhPermute is sh
-    SKnown x -> x `ConsKnown` listhPermute is sh
+shxPermute :: forall i is sh. Perm is -> ShX sh i -> ShX (Permute is sh) i
+shxPermute PNil _ = ZSX
+shxPermute (i `PCons` (is :: Perm is')) (sh :: ShX sh i) =
+  case shxIndex i sh of
+    SUnknown x -> x `ConsUnknown` shxPermute is sh
+    SKnown x -> x `ConsKnown` shxPermute is sh
 
-listhIndex :: forall i k sh. SNat k -> ListH sh i -> SMayNat i (Index k sh)
-listhIndex SZ (n `ConsUnknown` _) = SUnknown n
-listhIndex SZ (n `ConsKnown` _) = SKnown n
-listhIndex (SS (i :: SNat k')) ((_ :: i) `ConsUnknown` (sh :: ListH sh' i))
+shxIndex :: forall i k sh. SNat k -> ShX sh i -> SMayNat i (Index k sh)
+shxIndex SZ (n `ConsUnknown` _) = SUnknown n
+shxIndex SZ (n `ConsKnown` _) = SKnown n
+shxIndex (SS (i :: SNat k')) ((_ :: i) `ConsUnknown` (sh :: ShX sh' i))
   | Refl <- lemIndexSucc (Proxy @k') (Proxy @Nothing) (Proxy @sh')
-  = listhIndex i sh
-listhIndex (SS (i :: SNat k')) ((_ :: SNat n) `ConsKnown` (sh :: ListH sh' i))
+  = shxIndex i sh
+shxIndex (SS (i :: SNat k')) ((_ :: SNat n) `ConsKnown` (sh :: ShX sh' i))
   | Refl <- lemIndexSucc (Proxy @k') (Proxy @(Just n)) (Proxy @sh')
-  = listhIndex i sh
-listhIndex _ ZH = error "Index into empty shape"
+  = shxIndex i sh
+shxIndex _ ZSX = error "Index into empty shape"
+
+shxPermutePrefix :: forall i is sh. Perm is -> ShX sh i -> ShX (PermutePrefix is sh) i
+shxPermutePrefix perm sh = shxAppend (shxPermute perm (shxTakeLenPerm perm sh)) (shxDropLenPerm perm sh)
 
-listhPermutePrefix :: forall i is sh. Perm is -> ListH sh i -> ListH (PermutePrefix is sh) i
-listhPermutePrefix perm sh = listhAppend (listhPermute perm (listhTakeLenPerm perm sh)) (listhDropLenPerm perm sh)
 
 ssxTakeLenPerm :: forall is sh. Perm is -> StaticShX sh -> StaticShX (TakeLen is sh)
-ssxTakeLenPerm = coerce (listhTakeLenPerm @())
+ssxTakeLenPerm = coerce (shxTakeLenPerm @())
 
 ssxDropLenPerm :: Perm is -> StaticShX sh -> StaticShX (DropLen is sh)
-ssxDropLenPerm = coerce (listhDropLenPerm @())
+ssxDropLenPerm = coerce (shxDropLenPerm @())
 
 ssxPermute :: Perm is -> StaticShX sh -> StaticShX (Permute is sh)
-ssxPermute = coerce (listhPermute @())
+ssxPermute = coerce (shxPermute @())
 
 ssxIndex :: SNat k -> StaticShX sh -> SMayNat () (Index k sh)
-ssxIndex k = coerce (listhIndex @() k)
+ssxIndex k = coerce (shxIndex @() k)
 
 ssxPermutePrefix :: Perm is -> StaticShX sh -> StaticShX (PermutePrefix is sh)
-ssxPermutePrefix = coerce (listhPermutePrefix @())
-
-shxTakeLenPerm :: forall is sh. Perm is -> IShX sh -> IShX (TakeLen is sh)
-shxTakeLenPerm = coerce (listhTakeLenPerm @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)
-
-shxIndex :: forall k sh i. SNat k -> ShX sh i -> SMayNat i (Index k sh)
-shxIndex k = coerce (listhIndex @i k)
-
-shxPermutePrefix :: Perm is -> IShX sh -> IShX (PermutePrefix is sh)
-shxPermutePrefix = coerce (listhPermutePrefix @Int)
+ssxPermutePrefix = coerce (shxPermutePrefix @())
 
 
 listxTakeLenPerm :: forall i is sh. Perm is -> ListX sh i -> ListX (TakeLen is sh) i