diff options
Diffstat (limited to 'src/Data/Array/Nested/Convert.hs')
| -rw-r--r-- | src/Data/Array/Nested/Convert.hs | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/src/Data/Array/Nested/Convert.hs b/src/Data/Array/Nested/Convert.hs index 226a425..9429f73 100644 --- a/src/Data/Array/Nested/Convert.hs +++ b/src/Data/Array/Nested/Convert.hs @@ -15,7 +15,7 @@ module Data.Array.Nested.Convert ( -- * Shape\/index\/list casting functions -- ** To ranked - ixrFromIxS, ixrFromIxX, shrFromShS, shrFromShX, shrFromShX2, + ixrFromIxS, ixrFromIxX, shrFromShS, shrFromShXAnyShape, shrFromShX, listrCast, ixrCast, shrCast, -- ** To shaped ixsFromIxR, ixsFromIxR', ixsFromIxX, ixsFromIxX', withShsFromShR, shsFromShX, withShsFromShX, shsFromSSX, @@ -71,8 +71,13 @@ shrFromShS :: ShS sh -> IShR (Rank sh) shrFromShS ZSS = ZSR shrFromShS (n :$$ sh) = fromSNat' n :$: shrFromShS sh --- shrFromShX re-exported --- shrFromShX2 re-exported +shrFromShXAnyShape :: IShX sh -> IShR (Rank sh) +shrFromShXAnyShape ZSX = ZSR +shrFromShXAnyShape (n :$% idx) = fromSMayNat' n :$: shrFromShXAnyShape idx + +shrFromShX :: IShX (Replicate n Nothing) -> IShR n +shrFromShX = coerce + -- listrCast re-exported -- ixrCast re-exported -- shrCast re-exported @@ -153,10 +158,7 @@ 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) (Proxy @m))) - (SUnknown n :$% shxFromShR idx) +shxFromShR = coerce shxFromShS :: ShS sh -> IShX (MapJust sh) shxFromShS = coerce |