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/Data/Array/Nested/Ranked/Shape.hs | |
| parent | 84c0878bbae11dbcab0f5b342386a20f716d2397 (diff) | |
Tweak sized list type synonyms slightly
Diffstat (limited to 'src/Data/Array/Nested/Ranked/Shape.hs')
| -rw-r--r-- | src/Data/Array/Nested/Ranked/Shape.hs | 26 |
1 files changed, 13 insertions, 13 deletions
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, (:$:) #-} |
