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

1 files changed, 47 insertions, 4 deletions

diff --git a/src/Data/Array/Nested/Convert.hs b/src/Data/Array/Nested/Convert.hs
index 73055db..b3a2c63 100644
--- a/src/Data/Array/Nested/Convert.hs
+++ b/src/Data/Array/Nested/Convert.hs
@@ -8,7 +8,9 @@
 {-# LANGUAGE TypeOperators #-}
 module Data.Array.Nested.Convert (
   -- * Shape/index/list casting functions
-  ixrFromIxS, shrFromShS,
+  ixrFromIxS, ixrFromIxX, shrFromShS, shrFromShX, shrFromShX2,
+  ixsFromIxX, shsFromShX,
+  ixxFromIxR, ixxFromIxS, shxFromShR, shxFromShS,
 
   -- * Array conversions
   castCastable,
@@ -27,6 +29,7 @@ module Data.Array.Nested.Convert (
 import Control.Category
 import Data.Proxy
 import Data.Type.Equality
+import GHC.TypeLits
 
 import Data.Array.Nested.Lemmas
 import Data.Array.Nested.Mixed
@@ -39,10 +42,26 @@ import Data.Array.Nested.Types
 
 -- * Shape/index/list casting functions
 
+-- * To ranked
+
 ixrFromIxS :: IxS sh i -> IxR (Rank sh) i
 ixrFromIxS ZIS = ZIR
 ixrFromIxS (i :.$ ix) = i :.: ixrFromIxS ix
 
+ixrFromIxX :: IxX sh i -> IxR (Rank sh) i
+ixrFromIxX ZIX = ZIR
+ixrFromIxX (n :.% idx) = n :.: ixrFromIxX idx
+
+shrFromShS :: ShS sh -> IShR (Rank sh)
+shrFromShS ZSS = ZSR
+shrFromShS (n :$$ sh) = fromSNat' n :$: shrFromShS sh
+
+-- shrFromShX re-exported
+
+-- shrFromShX2 re-exported
+
+-- * To shaped
+
 -- ixsFromIxR :: IIxR (Rank sh) -> IIxS sh
 -- ixsFromIxR = \ix -> go ix _
 --   where
@@ -50,9 +69,33 @@ ixrFromIxS (i :.$ ix) = i :.: ixrFromIxS ix
 --     go ZIR k = k ZIS
 --     go (i :.: ix) k = go ix (i :.$)
 
-shrFromShS :: ShS sh -> IShR (Rank sh)
-shrFromShS ZSS = ZSR
-shrFromShS (n :$$ sh) = fromSNat' n :$: shrFromShS sh
+ixsFromIxX :: ShS sh -> IxX (MapJust sh) i -> IxS sh i
+ixsFromIxX ZSS ZIX = ZIS
+ixsFromIxX (_ :$$ sh) (n :.% idx) = n :.$ ixsFromIxX sh idx
+
+-- shsFromShX re-exported
+
+-- * To mixed
+
+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)
+
+ixxFromIxS :: IxS sh i -> IxX (MapJust sh) i
+ixxFromIxS ZIS = ZIX
+ixxFromIxS (n :.$ sh) = n :.% ixxFromIxS 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)
+
+shxFromShS :: ShS sh -> IShX (MapJust sh)
+shxFromShS ZSS = ZSX
+shxFromShS (n :$$ sh) = SKnown n :$% shxFromShS sh
 
 
 -- * Array conversions