From 0d06aadc72635011ef4c2ac4d7f45ece42817470 Mon Sep 17 00:00:00 2001 From: Tom Smeding Date: Fri, 29 Nov 2024 15:59:32 +0100 Subject: scastToMixed, weakly-typed version of stoMixed --- src/Data/Array/Nested/Internal/Shaped.hs | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'src/Data/Array/Nested') 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 -- cgit v1.2.3-70-g09d2