Move shape conversion ops to Data.Array.Nested.Convert

1 files changed, 0 insertions, 27 deletions

diff --git a/src/Data/Array/Nested/Ranked/Shape.hs b/src/Data/Array/Nested/Ranked/Shape.hs
index 75a1e5b..326bf61 100644
--- a/src/Data/Array/Nested/Ranked/Shape.hs
+++ b/src/Data/Array/Nested/Ranked/Shape.hs
@@ -40,7 +40,6 @@ import GHC.TypeLits
 import GHC.TypeNats qualified as TN
 
 import Data.Array.Nested.Lemmas
-import Data.Array.Nested.Mixed.Shape
 import Data.Array.Nested.Types
 
 
@@ -213,16 +212,6 @@ ixrZero :: SNat n -> IIxR n
 ixrZero SZ = ZIR
 ixrZero (SS n) = 0 :.: ixrZero n
 
-ixrFromIxX :: IxX sh i -> IxR (Rank sh) i
-ixrFromIxX ZIX = ZIR
-ixrFromIxX (n :.% idx) = n :.: ixrFromIxX idx
-
-ixxFromIxR :: IxR n i -> IxX (Replicate n Nothing) i
-ixxFromIxR ZIR = ZIX
-ixxFromIxR (n :.: (idx :: IxR m i)) =
-  castWith (subst2 @IxX @i (lemReplicateSucc @(Nothing @Nat) @m))
-    (n :.% ixxFromIxR idx)
-
 ixrHead :: IxR (n + 1) i -> i
 ixrHead (IxR list) = listrHead list
 
@@ -278,22 +267,6 @@ instance Show i => Show (ShR n i) where
 
 instance NFData i => NFData (ShR sh i)
 
-shrFromShX :: forall sh. IShX sh -> IShR (Rank sh)
-shrFromShX ZSX = ZSR
-shrFromShX (n :$% idx) = fromSMayNat' n :$: shrFromShX idx
-
--- | Convenience wrapper around 'shrFromShX' that applies 'lemRankReplicate'.
-shrFromShX2 :: forall n. IShX (Replicate n Nothing) -> IShR n
-shrFromShX2 sh
-  | Refl <- lemRankReplicate (Proxy @n)
-  = shrFromShX sh
-
-shxFromShR :: ShR n i -> ShX (Replicate n Nothing) i
-shxFromShR ZSR = ZSX
-shxFromShR (n :$: (idx :: ShR m i)) =
-  castWith (subst2 @ShX @i (lemReplicateSucc @(Nothing @Nat) @m))
-    (SUnknown n :$% shxFromShR idx)
-
 -- | This checks only whether the ranks are equal, not whether the actual
 -- values are.
 shrEqRank :: ShR n i -> ShR n' i -> Maybe (n :~: n')