diff options
| author | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2025-12-13 14:18:46 +0100 |
|---|---|---|
| committer | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2026-03-15 10:44:58 +0100 |
| commit | 6f131da821fc7a6dbeb0b233146e69ca8eb1d53f (patch) | |
| tree | 49961024d142849e9f3e97ecbcf99d2533440635 /src/Data | |
| parent | 3f589f443369b351eb1ed71ab82329ee75111101 (diff) | |
Implement index conversions as unsafeCoerce
until maybe we make shaped and ranked newtypes over mixed?
Diffstat (limited to 'src/Data')
| -rw-r--r-- | src/Data/Array/Nested/Convert.hs | 21 |
1 files changed, 7 insertions, 14 deletions
diff --git a/src/Data/Array/Nested/Convert.hs b/src/Data/Array/Nested/Convert.hs index 9429f73..32248c4 100644 --- a/src/Data/Array/Nested/Convert.hs +++ b/src/Data/Array/Nested/Convert.hs @@ -42,6 +42,7 @@ import Data.Coerce (coerce) import Data.Proxy import Data.Type.Equality import GHC.TypeLits +import Unsafe.Coerce (unsafeCoerce) import Data.Array.Nested.Lemmas import Data.Array.Nested.Mixed @@ -60,12 +61,10 @@ import Data.Array.Nested.Types -- and ranekd index types as newtypes of the mixed index type -- and similarly for the sized lists ixrFromIxS :: IxS sh i -> IxR (Rank sh) i -ixrFromIxS ZIS = ZIR -ixrFromIxS (i :.$ ix) = i :.: ixrFromIxS ix +ixrFromIxS = unsafeCoerce ixrFromIxX :: IxX sh i -> IxR (Rank sh) i -ixrFromIxX ZIX = ZIR -ixrFromIxX (n :.% idx) = n :.: ixrFromIxX idx +ixrFromIxX = unsafeCoerce shrFromShS :: ShS sh -> IShR (Rank sh) shrFromShS ZSS = ZSR @@ -86,8 +85,7 @@ shrFromShX = coerce -- TODO: remove the ShS now that no KnownNats is inside IxS. ixsFromIxR :: ShS sh -> IxR (Rank sh) i -> IxS sh i -ixsFromIxR ZSS ZIR = ZIS -ixsFromIxR (_ :$$ sh) (n :.: idx) = n :.$ ixsFromIxR sh idx +ixsFromIxR _ = unsafeCoerce -- TODO: if possible, remove the ShS now that no KnownNats is inside IxS. -- | Performs a runtime check that @n@ matches @Rank sh@. Equivalent to the @@ -101,8 +99,7 @@ ixsFromIxR' _ _ = error "ixsFromIxR': index rank does not match shape rank" -- TODO: remove the ShS now that no KnownNats is inside IxS. ixsFromIxX :: ShS sh -> IxX (MapJust sh) i -> IxS sh i -ixsFromIxX ZSS ZIX = ZIS -ixsFromIxX (_ :$$ sh) (n :.% idx) = n :.$ ixsFromIxX sh idx +ixsFromIxX _ = unsafeCoerce -- TODO: if possible, remove the ShS now that no KnownNats is inside IxS. -- | Performs a runtime check that @Rank sh'@ match @Rank sh@. Equivalent to @@ -148,14 +145,10 @@ shsFromSSX = shsFromShX Prelude.. shxFromSSX -- * 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) (Proxy @m))) - (n :.% ixxFromIxR idx) +ixxFromIxR = unsafeCoerce ixxFromIxS :: IxS sh i -> IxX (MapJust sh) i -ixxFromIxS ZIS = ZIX -ixxFromIxS (n :.$ sh) = n :.% ixxFromIxS sh +ixxFromIxS = unsafeCoerce shxFromShR :: ShR n i -> ShX (Replicate n Nothing) i shxFromShR = coerce |