diff options
| author | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2025-12-13 14:18:46 +0100 |
|---|---|---|
| committer | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2025-12-13 21:39:33 +0100 |
| commit | f2129e063bc5ee6241b2cf0891f8f39c8265ccb7 (patch) | |
| tree | 13e18074aaa1803faf30ea8b4ba0e7ff90a38979 /src | |
| parent | 2d837a1b4ef2914ac4bc8e012b31ff7abd4d2246 (diff) | |
Implement index conversions as unsafeCoerce
until maybe we make shaped and ranked newtypes over mixed?
Diffstat (limited to 'src')
| -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 3d0da37..da1c384 100644 --- a/src/Data/Array/Nested/Convert.hs +++ b/src/Data/Array/Nested/Convert.hs @@ -41,6 +41,7 @@ import Control.Category import Data.Proxy import Data.Type.Equality import GHC.TypeLits +import Unsafe.Coerce (unsafeCoerce) import Data.Array.Nested.Lemmas import Data.Array.Nested.Mixed @@ -56,12 +57,10 @@ import Data.Array.Nested.Types -- * To ranked 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 @@ -77,8 +76,7 @@ shrFromShS (n :$$ sh) = fromSNat' n :$: shrFromShS sh -- 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 @@ -92,8 +90,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 @@ -137,14 +134,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 ZSR = ZSX |