diff options
Diffstat (limited to 'src/Data/Array')
| -rw-r--r-- | src/Data/Array/Nested/Mixed/ListX.hs | 20 |
1 files changed, 15 insertions, 5 deletions
diff --git a/src/Data/Array/Nested/Mixed/ListX.hs b/src/Data/Array/Nested/Mixed/ListX.hs index e89d1c8..ae3c89f 100644 --- a/src/Data/Array/Nested/Mixed/ListX.hs +++ b/src/Data/Array/Nested/Mixed/ListX.hs @@ -42,10 +42,10 @@ import Data.Array.Nested.Types -- * Mixed lists implementation +-- | Data invariant: each element is in WHNF (the spine may be be not forced). type role ListX nominal representational type ListX :: [Maybe Nat] -> Type -> Type newtype ListX sh i = ListX [i] - -- data invariant: each element is in WHNF; the spine maybe be not forced deriving (Eq, Ord, NFData, Foldable) pattern ZX :: forall sh i. () => sh ~ '[] => ListX sh i @@ -62,28 +62,38 @@ pattern (::%) :: forall {sh1} {i}. forall n sh. (n : sh ~ sh1) => i -> ListX sh i -> ListX sh1 i -pattern i ::% sh <- (listxUncons -> Just (UnconsListXRes sh i)) - where !i ::% ListX !sh = ListX (i : sh) +pattern i ::% l <- (listxUncons -> Just (UnconsListXRes l i)) + where !i ::% ListX !l = ListX (i : l) infixr 3 ::% data UnconsListXRes i sh1 = forall n sh. (n : sh ~ sh1) => UnconsListXRes (ListX sh i) i {-# INLINE listxUncons #-} listxUncons :: forall sh1 i. ListX sh1 i -> Maybe (UnconsListXRes i sh1) -listxUncons (ListX (i : sh')) = gcastWith (unsafeCoerceRefl :: Head sh1 ': Tail sh1 :~: sh1) $ - Just (UnconsListXRes (ListX @(Tail sh1) sh') i) +listxUncons (ListX (i : l)) = gcastWith (unsafeCoerceRefl :: Head sh1 ': Tail sh1 :~: sh1) $ + Just (UnconsListXRes (ListX @(Tail sh1) l) i) listxUncons (ListX []) = Nothing {-# COMPLETE ZX, (::%) #-} +-- | This operation may not preserve the data invariant for ListX, +-- regardless whether the invariant holds for the argument list. +-- It's the user's obligation to honor the data invariant, +-- e.g., by forcing all new elements of the resulting list at the end. {-# INLINE lazily #-} lazily :: ([a] -> [b]) -> ListX sh a -> ListX sh b lazily f (ListX l) = ListX $ f l +-- | This operation may not preserve the data invariant for ListX, +-- regardless whether the invariant holds for the argument lists. +-- It's the user's obligation to honor the data invariant, +-- e.g., by forcing all new elements of the resulting list at the end. {-# INLINE lazilyConcat #-} lazilyConcat :: ([a] -> [b] -> [c]) -> ListX sh a -> ListX sh' b -> ListX (sh ++ sh') c lazilyConcat f (ListX l) (ListX k) = ListX $ f l k +-- | This operation honours the data invariant for @ListX@ by forcing +-- all elements of the resulting list at the end. {-# INLINE lazilyForce #-} lazilyForce :: ([a] -> [b]) -> ListX sh a -> ListX sh b lazilyForce f (ListX l) = let res = f l |