aboutsummaryrefslogtreecommitdiff
path: root/src/Data/Array/Nested/Ranked/Shape.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/Data/Array/Nested/Ranked/Shape.hs')
-rw-r--r--src/Data/Array/Nested/Ranked/Shape.hs26
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, (:$:) #-}