diff options
| author | Tom Smeding <tom@tomsmeding.com> | 2025-10-02 14:12:15 +0200 |
|---|---|---|
| committer | Tom Smeding <tom@tomsmeding.com> | 2025-10-02 14:12:15 +0200 |
| commit | 2018dc3476c1a1b723f8c7106d628bd0da8cb49c (patch) | |
| tree | 12255ef1856abc5a7f618c0190a073a5655319bc /src/Data/Array | |
| parent | ef72e54cf6bcee7124058364fea15b4d1bd62cd7 (diff) | |
Diffstat (limited to 'src/Data/Array')
| -rw-r--r-- | src/Data/Array/Nested/Convert.hs | 1 | ||||
| -rw-r--r-- | src/Data/Array/Nested/Permutation.hs | 1 | ||||
| -rw-r--r-- | src/Data/Array/Nested/Ranked/Shape.hs | 5 |
3 files changed, 2 insertions, 5 deletions
diff --git a/src/Data/Array/Nested/Convert.hs b/src/Data/Array/Nested/Convert.hs index a260dc0..8c88d23 100644 --- a/src/Data/Array/Nested/Convert.hs +++ b/src/Data/Array/Nested/Convert.hs @@ -80,7 +80,6 @@ shrFromShS (n :$$ sh) = fromSNat' n :$: shrFromShS sh ixsFromIxR :: ShS sh -> IxR (Rank sh) i -> IxS sh i ixsFromIxR ZSS ZIR = ZIS ixsFromIxR (_ :$$ sh) (n :.: idx) = n :.$ ixsFromIxR sh idx -ixsFromIxR _ _ = error "unreachable" -- | Performs a runtime check that @n@ matches @Rank sh@. Equivalent to the -- following, but more efficient: diff --git a/src/Data/Array/Nested/Permutation.hs b/src/Data/Array/Nested/Permutation.hs index 1a0fd22..045b18f 100644 --- a/src/Data/Array/Nested/Permutation.hs +++ b/src/Data/Array/Nested/Permutation.hs @@ -283,6 +283,7 @@ lemRankDropLen (_ :!% sh) (_ `PCons` is) = unsafeCoerceRefl #endif lemRankDropLen (_ :!% _) PNil = Refl +lemRankDropLen ZKX (_ `PCons` _) = error "1 <= 0" lemIndexSucc :: Proxy i -> Proxy a -> Proxy l -> Index (i + 1) (a : l) :~: Index i l diff --git a/src/Data/Array/Nested/Ranked/Shape.hs b/src/Data/Array/Nested/Ranked/Shape.hs index 88a550c..488b4d8 100644 --- a/src/Data/Array/Nested/Ranked/Shape.hs +++ b/src/Data/Array/Nested/Ranked/Shape.hs @@ -115,21 +115,17 @@ listrFromList (x : xs) k = listrFromList xs $ \l -> k (x ::: l) listrHead :: ListR (n + 1) i -> i listrHead (i ::: _) = i -listrHead ZR = error "unreachable" listrTail :: ListR (n + 1) i -> ListR n i listrTail (_ ::: sh) = sh -listrTail ZR = error "unreachable" listrInit :: ListR (n + 1) i -> ListR n i listrInit (n ::: sh@(_ ::: _)) = n ::: listrInit sh listrInit (_ ::: ZR) = ZR -listrInit ZR = error "unreachable" listrLast :: ListR (n + 1) i -> i listrLast (_ ::: sh@(_ ::: _)) = listrLast sh listrLast (n ::: ZR) = n -listrLast ZR = error "unreachable" -- | Performs a runtime check that the lengths are identical. listrCast :: SNat n' -> ListR n i -> ListR n' i @@ -138,6 +134,7 @@ listrCast = listrCastWithName "listrCast" listrIndex :: forall k n i. (k + 1 <= n) => SNat k -> ListR n i -> i listrIndex SZ (x ::: _) = x listrIndex (SS i) (_ ::: xs) | Refl <- lemLeqSuccSucc (Proxy @k) (Proxy @n) = listrIndex i xs +listrIndex _ ZR = error "k + 1 <= 0" listrZip :: ListR n i -> ListR n j -> ListR n (i, j) listrZip ZR ZR = ZR |