diff options
| author | Tom Smeding <tom@tomsmeding.com> | 2024-11-29 15:59:32 +0100 |
|---|---|---|
| committer | Tom Smeding <tom@tomsmeding.com> | 2024-11-29 15:59:32 +0100 |
| commit | 0d06aadc72635011ef4c2ac4d7f45ece42817470 (patch) | |
| tree | 6a707ad698528282cfc4f71f0ab22fef14880d69 /src/Data/Array/Nested | |
| parent | dd21ebafeeeb2abc222b3525e136d4ba6a769176 (diff) | |
scastToMixed, weakly-typed version of stoMixed
Diffstat (limited to 'src/Data/Array/Nested')
| -rw-r--r-- | src/Data/Array/Nested/Internal/Shaped.hs | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/Data/Array/Nested/Internal/Shaped.hs b/src/Data/Array/Nested/Internal/Shaped.hs index 5d3eba1..76e0e6d 100644 --- a/src/Data/Array/Nested/Internal/Shaped.hs +++ b/src/Data/Array/Nested/Internal/Shaped.hs @@ -483,3 +483,13 @@ mcastToShaped arr targetsh stoMixed :: forall sh a. Shaped sh a -> Mixed (MapJust sh) a stoMixed (Shaped arr) = arr + +-- | A more weakly-typed version of 'stoMixed' that does a runtime shape +-- compatibility check. +scastToMixed :: forall sh sh' a. (Elt a, Rank sh ~ Rank sh') + => IShX sh' -> Shaped sh a -> Mixed sh' a +scastToMixed shx (Shaped arr) + | Refl <- lemAppNil @sh' + , Refl <- lemAppNil @(MapJust sh) + , Refl <- lemRankMapJust (shCvtXS' @sh (mshape arr)) + = mcast (ssxFromShape (mshape arr)) shx (Proxy @'[]) arr |