diff options
| author | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2025-12-11 14:08:18 +0100 |
|---|---|---|
| committer | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2026-03-15 10:35:21 +0100 |
| commit | 01a79440952d789184101fc1aad277c00d010a25 (patch) | |
| tree | 9d41db480536f9e856bdc058351adacd6b10e99e /src/Data/Array/Nested/Convert.hs | |
| parent | 816249cd59a7e243bec82651e2def22f8c3b439c (diff) | |
Make ShS a newtype over ShX
TODO: use lemmas in place of the unsafeCoerceRefl
Diffstat (limited to 'src/Data/Array/Nested/Convert.hs')
| -rw-r--r-- | src/Data/Array/Nested/Convert.hs | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/Data/Array/Nested/Convert.hs b/src/Data/Array/Nested/Convert.hs index 8c88d23..3d0da37 100644 --- a/src/Data/Array/Nested/Convert.hs +++ b/src/Data/Array/Nested/Convert.hs @@ -75,12 +75,12 @@ shrFromShS (n :$$ sh) = fromSNat' n :$: shrFromShS sh -- * To shaped --- TODO: these take a ShS because there are KnownNats inside IxS. - +-- 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 +-- 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 -- following, but more efficient: -- @@ -90,11 +90,12 @@ ixsFromIxR' ZSS ZIR = ZIS ixsFromIxR' (_ :$$ sh) (n :.: idx) = n :.$ ixsFromIxR' sh idx ixsFromIxR' _ _ = error "ixsFromIxR': index rank does not match shape rank" --- TODO: this takes a ShS because there are KnownNats inside IxS. +-- 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 +-- 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 -- the following, but more efficient: -- |