diff options
| author | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2026-04-05 18:30:30 +0200 |
|---|---|---|
| committer | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2026-04-05 18:33:37 +0200 |
| commit | 574468a37a0e662c5d63d1cf3f8f876b11b4e332 (patch) | |
| tree | d6015b45903ad21b04533d0bef52cfd38fca5d01 /src | |
| parent | 84c0878bbae11dbcab0f5b342386a20f716d2397 (diff) | |
Tweak sized list type synonyms slightly
Diffstat (limited to 'src')
| -rw-r--r-- | src/Data/Array/Nested/Mixed/ListX.hs | 9 | ||||
| -rw-r--r-- | src/Data/Array/Nested/Mixed/Shape.hs | 14 | ||||
| -rw-r--r-- | src/Data/Array/Nested/Ranked/Shape.hs | 26 | ||||
| -rw-r--r-- | src/Data/Array/Nested/Shaped/Shape.hs | 19 |
4 files changed, 34 insertions, 34 deletions
diff --git a/src/Data/Array/Nested/Mixed/ListX.hs b/src/Data/Array/Nested/Mixed/ListX.hs index ae3c89f..048003f 100644 --- a/src/Data/Array/Nested/Mixed/ListX.hs +++ b/src/Data/Array/Nested/Mixed/ListX.hs @@ -48,6 +48,7 @@ type ListX :: [Maybe Nat] -> Type -> Type newtype ListX sh i = ListX [i] deriving (Eq, Ord, NFData, Foldable) +{-# INLINE ZX #-} pattern ZX :: forall sh i. () => sh ~ '[] => ListX sh i pattern ZX <- (listxNull -> Just Refl) where ZX = ListX [] @@ -62,16 +63,16 @@ pattern (::%) :: forall {sh1} {i}. forall n sh. (n : sh ~ sh1) => i -> ListX sh i -> ListX sh1 i -pattern i ::% l <- (listxUncons -> Just (UnconsListXRes l i)) +pattern i ::% l <- (listxUncons -> Just (UnconsListXRes i l)) where !i ::% ListX !l = ListX (i : l) infixr 3 ::% data UnconsListXRes i sh1 = - forall n sh. (n : sh ~ sh1) => UnconsListXRes (ListX sh i) i + forall n sh. (n : sh ~ sh1) => UnconsListXRes i (ListX sh i) {-# INLINE listxUncons #-} listxUncons :: forall sh1 i. ListX sh1 i -> Maybe (UnconsListXRes i sh1) listxUncons (ListX (i : l)) = gcastWith (unsafeCoerceRefl :: Head sh1 ': Tail sh1 :~: sh1) $ - Just (UnconsListXRes (ListX @(Tail sh1) l) i) + Just (UnconsListXRes i (ListX @(Tail sh1) l)) listxUncons (ListX []) = Nothing {-# COMPLETE ZX, (::%) #-} @@ -123,7 +124,7 @@ instance Functor (ListX l) where let fmap' [] = [] fmap' (x : xs) = let y = f x rest = fmap' xs - in y `seq` rest `seq` y : rest + in y `seq` rest `seq` (y : rest) in ListX $ fmap' l -- | Very untyped: not even length is checked (at runtime). diff --git a/src/Data/Array/Nested/Mixed/Shape.hs b/src/Data/Array/Nested/Mixed/Shape.hs index 54a945b..25cecb5 100644 --- a/src/Data/Array/Nested/Mixed/Shape.hs +++ b/src/Data/Array/Nested/Mixed/Shape.hs @@ -107,8 +107,8 @@ pattern (:.%) :: forall {sh1} {i}. forall n sh. (n : sh ~ sh1) => i -> IxX sh i -> IxX sh1 i -pattern i :.% sh <- IxX (i ::% (IxX -> sh)) - where i :.% IxX sh = IxX (i ::% sh) +pattern i :.% l <- IxX (i ::% (IxX -> l)) + where i :.% IxX l = IxX (i ::% l) infixr 3 :.% {-# COMPLETE ZIX, (:.%) #-} @@ -305,10 +305,10 @@ instance NFData i => NFData (ListH sh i) where rnf (SNat `ConsKnown` l) = rnf l data UnconsListHRes i sh1 = - forall n sh. (n : sh ~ sh1) => UnconsListHRes (ListH sh i) (SMayNat i n) + forall n sh. (n : sh ~ sh1) => UnconsListHRes (SMayNat i n) (ListH sh i) listhUncons :: ListH sh1 i -> Maybe (UnconsListHRes i sh1) -listhUncons (i `ConsUnknown` shl') = Just (UnconsListHRes shl' (SUnknown i)) -listhUncons (i `ConsKnown` shl') = Just (UnconsListHRes shl' (SKnown i)) +listhUncons (i `ConsUnknown` shl') = Just (UnconsListHRes (SUnknown i) shl') +listhUncons (i `ConsKnown` shl') = Just (UnconsListHRes (SKnown i) shl') listhUncons ZH = Nothing -- | This checks only whether the types are equal; if the elements of the list @@ -422,7 +422,7 @@ pattern (:$%) :: forall {sh1} {i}. forall n sh. (n : sh ~ sh1) => SMayNat i n -> ShX sh i -> ShX sh1 i -pattern i :$% shl <- ShX (listhUncons -> Just (UnconsListHRes (ShX -> shl) i)) +pattern i :$% shl <- ShX (listhUncons -> Just (UnconsListHRes i (ShX -> shl))) where i :$% ShX shl = case i of; SUnknown x -> ShX (x `ConsUnknown` shl); SKnown x -> ShX (x `ConsKnown` shl) infixr 3 :$% @@ -605,7 +605,7 @@ pattern (:!%) :: forall {sh1}. forall n sh. (n : sh ~ sh1) => SMayNat () n -> StaticShX sh -> StaticShX sh1 -pattern i :!% shl <- StaticShX (listhUncons -> Just (UnconsListHRes (StaticShX -> shl) i)) +pattern i :!% shl <- StaticShX (listhUncons -> Just (UnconsListHRes i (StaticShX -> shl))) where i :!% StaticShX shl = case i of; SUnknown () -> StaticShX (() `ConsUnknown` shl); SKnown x -> StaticShX (x `ConsKnown` shl) infixr 3 :!% diff --git a/src/Data/Array/Nested/Ranked/Shape.hs b/src/Data/Array/Nested/Ranked/Shape.hs index 687df69..d35383f 100644 --- a/src/Data/Array/Nested/Ranked/Shape.hs +++ b/src/Data/Array/Nested/Ranked/Shape.hs @@ -66,18 +66,18 @@ pattern (:::) :: forall {n1} {i}. forall n. (n + 1 ~ n1) => i -> ListR n i -> ListR n1 i -pattern i ::: sh <- (listrUncons -> Just (UnconsListRRes sh i)) - where i ::: ListR sh | Refl <- lemReplicateSucc2 (Proxy @n1) Refl = ListR (i ::% sh) +pattern i ::: l <- (listrUncons -> Just (UnconsListRRes i l)) + where i ::: ListR l | Refl <- lemReplicateSucc2 (Proxy @n1) Refl = ListR (i ::% l) infixr 3 ::: data UnconsListRRes i n1 = - forall n. (n + 1 ~ n1) => UnconsListRRes (ListR n i) i + forall n. (n + 1 ~ n1) => UnconsListRRes i (ListR n i) listrUncons :: forall n1 i. ListR n1 i -> Maybe (UnconsListRRes i n1) -listrUncons (ListR ((::%) @n' @sh' x sh')) - | Refl <- lemReplicateHead (Proxy @n') (Proxy @sh') (Proxy @Nothing) (Proxy @n1) Refl - , Refl <- lemReplicateCons (Proxy @sh') (Proxy @n1) Refl - , Refl <- lemReplicateCons2 (Proxy @sh') (Proxy @n1) Refl = - Just (UnconsListRRes (ListR @(Rank sh') sh') x) +listrUncons (ListR ((::%) @n @sh i l)) + | Refl <- lemReplicateHead (Proxy @n) (Proxy @sh) (Proxy @Nothing) (Proxy @n1) Refl + , Refl <- lemReplicateCons (Proxy @sh) (Proxy @n1) Refl + , Refl <- lemReplicateCons2 (Proxy @sh) (Proxy @n1) Refl = + Just (UnconsListRRes i (ListR @(Rank sh) l)) listrUncons (ListR _) = Nothing {-# COMPLETE ZR, (:::) #-} @@ -207,8 +207,8 @@ pattern (:.:) :: forall {n1} {i}. forall n. (n + 1 ~ n1) => i -> IxR n i -> IxR n1 i -pattern i :.: sh <- IxR (i ::: (IxR -> sh)) - where i :.: IxR sh = IxR (i ::: sh) +pattern i :.: l <- IxR (i ::: (IxR -> l)) + where i :.: IxR l = IxR (i ::: l) infixr 3 :.: {-# COMPLETE ZIR, (:.:) #-} @@ -310,17 +310,17 @@ pattern (:$:) :: forall {n1} {i}. forall n. (n + 1 ~ n1) => i -> ShR n i -> ShR n1 i -pattern i :$: sh <- (shrUncons -> Just (UnconsShRRes sh i)) +pattern i :$: sh <- (shrUncons -> Just (UnconsShRRes i sh)) where i :$: ShR sh | Refl <- lemReplicateSucc2 (Proxy @n1) Refl = ShR (SUnknown i :$% sh) infixr 3 :$: data UnconsShRRes i n1 = - forall n. (n + 1 ~ n1) => UnconsShRRes (ShR n i) i + forall n. (n + 1 ~ n1) => UnconsShRRes i (ShR n i) shrUncons :: forall n1 i. ShR n1 i -> Maybe (UnconsShRRes i n1) shrUncons (ShR (SUnknown x :$% (sh' :: ShX sh' i))) | Refl <- lemReplicateCons (Proxy @sh') (Proxy @n1) Refl , Refl <- lemReplicateCons2 (Proxy @sh') (Proxy @n1) Refl - = Just (UnconsShRRes (ShR sh') x) + = Just (UnconsShRRes x (ShR sh')) shrUncons (ShR _) = Nothing {-# COMPLETE ZSR, (:$:) #-} diff --git a/src/Data/Array/Nested/Shaped/Shape.hs b/src/Data/Array/Nested/Shaped/Shape.hs index fe55d1a..bec2495 100644 --- a/src/Data/Array/Nested/Shaped/Shape.hs +++ b/src/Data/Array/Nested/Shaped/Shape.hs @@ -63,16 +63,16 @@ pattern (::$) :: forall {sh1} {i}. forall n sh. (n : sh ~ sh1) => i -> ListS sh i -> ListS sh1 i -pattern i ::$ sh <- (listsUncons -> Just (UnconsListSRes sh i)) - where i ::$ ListS sh = ListS (i ::% sh) +pattern i ::$ l <- (listsUncons -> Just (UnconsListSRes i l)) + where i ::$ ListS l = ListS (i ::% l) infixr 3 ::$ data UnconsListSRes i sh1 = - forall n sh. (n : sh ~ sh1) => UnconsListSRes (ListS sh i) i + forall n sh. (n : sh ~ sh1) => UnconsListSRes i (ListS sh i) listsUncons :: forall sh1 i. ListS sh1 i -> Maybe (UnconsListSRes i sh1) -listsUncons (ListS (x ::% sh')) | Refl <- lemMapJustHead (Proxy @sh1) - , Refl <- lemMapJustCons @sh1 Refl = - Just (UnconsListSRes (ListS sh') x) +listsUncons (ListS (i ::% l)) | Refl <- lemMapJustHead (Proxy @sh1) + , Refl <- lemMapJustCons @sh1 Refl = + Just (UnconsListSRes i (ListS l)) listsUncons (ListS _) = Nothing {-# COMPLETE ZS, (::$) #-} @@ -171,8 +171,8 @@ pattern (:.$) :: forall {sh1} {i}. forall n sh. (n : sh ~ sh1) => i -> IxS sh i -> IxS sh1 i -pattern i :.$ sh <- IxS (i ::$ (IxS -> sh)) - where i :.$ IxS sh = IxS (i ::$ sh) +pattern i :.$ l <- IxS (i ::$ (IxS -> l)) + where i :.$ IxS l = IxS (i ::$ l) infixr 3 :.$ {-# COMPLETE ZIS, (:.$) #-} @@ -289,8 +289,7 @@ infixr 3 :$$ data UnconsShSRes sh1 = forall n sh. (n : sh ~ sh1) => UnconsShSRes (SNat n) (ShS sh) shsUncons :: forall sh1. ShS sh1 -> Maybe (UnconsShSRes sh1) -shsUncons (ShS (SKnown x :$% sh')) - | Refl <- lemMapJustCons @sh1 Refl +shsUncons (ShS (SKnown x :$% sh')) | Refl <- lemMapJustCons @sh1 Refl = Just (UnconsShSRes x (ShS sh')) shsUncons (ShS _) = Nothing |
