diff options
Diffstat (limited to 'src/Data/Array/Mixed.hs')
-rw-r--r-- | src/Data/Array/Mixed.hs | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/Data/Array/Mixed.hs b/src/Data/Array/Mixed.hs index 17b0ab4..246f8fc 100644 --- a/src/Data/Array/Mixed.hs +++ b/src/Data/Array/Mixed.hs @@ -13,6 +13,8 @@ module Data.Array.Mixed where import qualified Data.Array.RankedS as S +import qualified Data.Array.Ranked as ORB +import Data.Coerce import Data.Kind import Data.Proxy import Data.Type.Equality @@ -347,3 +349,14 @@ sumOuter :: forall sh sh' a. (Storable a, Num a) sumOuter ssh ssh' | Refl <- lemAppNil @sh = sumInner ssh' ssh . transpose2 ssh ssh' + +fromList :: forall n sh a. Storable a + => StaticShapeX (n : sh) -> [XArray sh a] -> XArray (n : sh) a +fromList ssh l + | Dict <- lemKnownINatRankSSX ssh + , Dict <- knownNatFromINat (Proxy @(Rank (n : sh))) + = case ssh of + m@GHC_SNat :$@ _ | natVal m /= fromIntegral (length l) -> + error $ "Data.Array.Mixed.fromList: length of list (" ++ show (length l) ++ ")" ++ + "does not match the type (" ++ show (natVal m) ++ ")" + _ -> XArray (S.ravel (ORB.fromList [length l] (coerce @[XArray sh a] @[S.Array (FromINat (Rank sh)) a] l))) |