2 files changed, 0 insertions, 145 deletions
diff --git a/src/Data/Array/Nested/Internal/Convert.hs b/src/Data/Array/Nested/Internal/Convert.hs
deleted file mode 100644
index 611b45e..0000000
--- a/src/Data/Array/Nested/Internal/Convert.hs
+++ /dev/null
@@ -1,86 +0,0 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeAbstractions #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE TypeOperators #-}
-module Data.Array.Nested.Internal.Convert where
-
-import Control.Category
-import Data.Proxy
-import Data.Type.Equality
-
-import Data.Array.Mixed.Lemmas
-import Data.Array.Mixed.Types
-import Data.Array.Nested.Internal.Lemmas
-import Data.Array.Nested.Mixed
-import Data.Array.Nested.Ranked
-import Data.Array.Nested.Shaped
-import Data.Array.Nested.Mixed.Shape
-import Data.Array.Nested.Shaped.Shape
-
-
-stoRanked :: Elt a => Shaped sh a -> Ranked (Rank sh) a
-stoRanked sarr@(Shaped arr)
-  | Refl <- lemRankMapJust (sshape sarr)
-  = mtoRanked arr
-
-rcastToShaped :: Elt a => Ranked (Rank sh) a -> ShS sh -> Shaped sh a
-rcastToShaped (Ranked arr) targetsh
-  | Refl <- lemRankReplicate (shxRank (shCvtSX targetsh))
-  , Refl <- lemRankMapJust targetsh
-  = mcastToShaped arr targetsh
-
--- | The only constructor that performs runtime shape checking is 'CastXS''.
--- For the other construtors, the types ensure that the shapes are already
--- compatible. To convert between 'Ranked' and 'Shaped', go via 'Mixed'.
-data Castable a b where
-  CastId  :: Castable a a
-  CastCmp :: Castable b c -> Castable a b -> Castable a c
-
-  CastRX  :: Castable a b -> Castable (Ranked n a)           (Mixed (Replicate n Nothing) b)
-  CastSX  :: Castable a b -> Castable (Shaped sh a)          (Mixed (MapJust sh) b)
-
-  CastXR  :: Castable a b -> Castable (Mixed sh a)           (Ranked (Rank sh) b)
-  CastXS  :: Castable a b -> Castable (Mixed (MapJust sh) a) (Shaped sh b)
-  CastXS' :: (Rank sh ~ Rank sh', Elt b) => ShS sh'
-          -> Castable a b -> Castable (Mixed sh a)           (Shaped sh' b)
-
-  CastRR  :: Castable a b -> Castable (Ranked n a)           (Ranked n b)
-  CastSS  :: Castable a b -> Castable (Shaped sh a)          (Shaped sh b)
-  CastXX  :: Castable a b -> Castable (Mixed sh a)           (Mixed sh b)
-
-instance Category Castable where
-  id = CastId
-  (.) = CastCmp
-
-castCastable :: (Elt a, Elt b) => Castable a b -> a -> b
-castCastable = \c x -> munScalar (go c (mscalar x))
-  where
-    -- The 'esh' is the extension shape: the casting happens under a whole
-    -- bunch of additional dimensions that it does not touch. These dimensions
-    -- are 'esh'.
-    -- The strategy is to unwind step-by-step to a large Mixed array, and to
-    -- perform the required checks and castings when re-nesting back up.
-    go :: Castable a b -> Mixed esh a -> Mixed esh b
-    go CastId x = x
-    go (CastCmp c1 c2) x = go c1 (go c2 x)
-    go (CastRX c) (M_Ranked (M_Nest esh x)) = M_Nest esh (go c x)
-    go (CastSX c) (M_Shaped (M_Nest esh x)) = M_Nest esh (go c x)
-    go (CastXR @_ @_ @sh c) (M_Nest @esh esh x) =
-      M_Ranked (M_Nest esh (mcastSafe @(MCastApp esh sh esh (Replicate (Rank sh) Nothing) MCastId MCastForget) Proxy
-                                      (go c x)))
-    go (CastXS c) (M_Nest esh x) = M_Shaped (M_Nest esh (go c x))
-    go (CastXS' @sh @sh' sh' c) (M_Nest @esh esh x)
-      | Refl <- lemRankAppMapJust (Proxy @esh) (Proxy @sh) (Proxy @sh')
-      = M_Shaped (M_Nest esh (mcast (ssxFromShape (shxAppend esh (shCvtSX sh')))
-                                    (go c x)))
-    go (CastRR c) (M_Ranked (M_Nest esh x)) = M_Ranked (M_Nest esh (go c x))
-    go (CastSS c) (M_Shaped (M_Nest esh x)) = M_Shaped (M_Nest esh (go c x))
-    go (CastXX c) (M_Nest esh x) = M_Nest esh (go c x)
-
-    lemRankAppMapJust :: Rank sh ~ Rank sh'
-                      => Proxy esh -> Proxy sh -> Proxy sh'
-                      -> Rank (esh ++ sh) :~: Rank (esh ++ MapJust sh')
-    lemRankAppMapJust _ _ _ = unsafeCoerceRefl
diff --git a/src/Data/Array/Nested/Internal/Lemmas.hs b/src/Data/Array/Nested/Internal/Lemmas.hs
deleted file mode 100644
index f4bad70..0000000
--- a/src/Data/Array/Nested/Internal/Lemmas.hs
+++ /dev/null
@@ -1,59 +0,0 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE TypeOperators #-}
-module Data.Array.Nested.Internal.Lemmas where
-
-import Data.Proxy
-import Data.Type.Equality
-import GHC.TypeLits
-
-import Data.Array.Mixed.Lemmas
-import Data.Array.Mixed.Permutation
-import Data.Array.Mixed.Types
-import Data.Array.Nested.Mixed.Shape
-import Data.Array.Nested.Shaped.Shape
-
-
-lemRankMapJust :: ShS sh -> Rank (MapJust sh) :~: Rank sh
-lemRankMapJust ZSS = Refl
-lemRankMapJust (_ :$$ sh') | Refl <- lemRankMapJust sh' = Refl
-
-lemMapJustApp :: ShS sh1 -> Proxy sh2
-              -> MapJust (sh1 ++ sh2) :~: MapJust sh1 ++ MapJust sh2
-lemMapJustApp ZSS _ = Refl
-lemMapJustApp (_ :$$ sh) p | Refl <- lemMapJustApp sh p = Refl
-
-lemTakeLenMapJust :: Perm is -> ShS sh -> TakeLen is (MapJust sh) :~: MapJust (TakeLen is sh)
-lemTakeLenMapJust PNil _ = Refl
-lemTakeLenMapJust (_ `PCons` is) (_ :$$ sh) | Refl <- lemTakeLenMapJust is sh = Refl
-lemTakeLenMapJust (_ `PCons` _) ZSS = error "TakeLen of empty"
-
-lemDropLenMapJust :: Perm is -> ShS sh -> DropLen is (MapJust sh) :~: MapJust (DropLen is sh)
-lemDropLenMapJust PNil _ = Refl
-lemDropLenMapJust (_ `PCons` is) (_ :$$ sh) | Refl <- lemDropLenMapJust is sh = Refl
-lemDropLenMapJust (_ `PCons` _) ZSS = error "DropLen of empty"
-
-lemIndexMapJust :: SNat i -> ShS sh -> Index i (MapJust sh) :~: Just (Index i sh)
-lemIndexMapJust SZ (_ :$$ _) = Refl
-lemIndexMapJust (SS (i :: SNat i')) ((_ :: SNat n) :$$ (sh :: ShS sh'))
-  | Refl <- lemIndexMapJust i sh
-  , Refl <- lemIndexSucc (Proxy @i') (Proxy @(Just n)) (Proxy @(MapJust sh'))
-  , Refl <- lemIndexSucc (Proxy @i') (Proxy @n) (Proxy @sh')
-  = Refl
-lemIndexMapJust _ ZSS = error "Index of empty"
-
-lemPermuteMapJust :: Perm is -> ShS sh -> Permute is (MapJust sh) :~: MapJust (Permute is sh)
-lemPermuteMapJust PNil _ = Refl
-lemPermuteMapJust (i `PCons` is) sh
-  | Refl <- lemPermuteMapJust is sh
-  , Refl <- lemIndexMapJust i sh
-  = Refl
-
-lemKnownMapJust :: forall sh. KnownShS sh => Proxy sh -> Dict KnownShX (MapJust sh)
-lemKnownMapJust _ = lemKnownShX (go (knownShS @sh))
-  where
-    go :: ShS sh' -> StaticShX (MapJust sh')
-    go ZSS = ZKX
-    go (n :$$ sh) = SKnown n :!% go sh