diff options
Diffstat (limited to 'src/Data/Array/Nested/Ranked')
| -rw-r--r-- | src/Data/Array/Nested/Ranked/Shape.hs | 13 |
1 files changed, 5 insertions, 8 deletions
diff --git a/src/Data/Array/Nested/Ranked/Shape.hs b/src/Data/Array/Nested/Ranked/Shape.hs index 2166123..4eef090 100644 --- a/src/Data/Array/Nested/Ranked/Shape.hs +++ b/src/Data/Array/Nested/Ranked/Shape.hs @@ -28,6 +28,7 @@ module Data.Array.Nested.Ranked.Shape where import Control.DeepSeq (NFData(..)) +import Control.Exception (assert) import Data.Coerce (coerce) import Data.Foldable qualified as Foldable import Data.Kind (Type) @@ -40,6 +41,7 @@ import GHC.TypeLits import GHC.TypeNats qualified as TN import Data.Array.Nested.Lemmas +import Data.Array.Nested.Mixed.ListX import Data.Array.Nested.Mixed.Shape import Data.Array.Nested.Permutation import Data.Array.Nested.Types @@ -121,15 +123,10 @@ listrAppend :: forall n m i. ListR n i -> ListR m i -> ListR (n + m) i listrAppend ZR sh = sh listrAppend (x ::: xs) sh = x ::: listrAppend xs sh +{-# INLINE listrFromList #-} listrFromList :: SNat n -> [i] -> ListR n i -listrFromList topsn topl = go topsn topl - where - go :: SNat n' -> [i] -> ListR n' i - go SZ [] = ZR - go (SS n) (i : is) = i ::: go n is - go _ _ = error $ "listrFromList: Mismatched list length (type says " - ++ show (fromSNat topsn) ++ ", list has length " - ++ show (length topl) ++ ")" +listrFromList topsn topl = assert (fromSNat' topsn == length topl) + $ ListR $ IsList.fromList topl listrHead :: ListR (n + 1) i -> i listrHead (i ::: _) = i |