From eea22885eccfe6f720a24682346159853d386434 Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom@tomsmeding.com>
Date: Fri, 31 May 2024 08:58:35 +0200
Subject: Rename some commuting lemmas to better names

---
 src/Data/Array/Nested/Internal/Lemmas.hs | 40 ++++++++++++++++----------------
 src/Data/Array/Nested/Internal/Shaped.hs |  6 ++---
 2 files changed, 23 insertions(+), 23 deletions(-)

(limited to 'src/Data')

diff --git a/src/Data/Array/Nested/Internal/Lemmas.hs b/src/Data/Array/Nested/Internal/Lemmas.hs
index 5ce5373..f894f78 100644
--- a/src/Data/Array/Nested/Internal/Lemmas.hs
+++ b/src/Data/Array/Nested/Internal/Lemmas.hs
@@ -25,30 +25,30 @@ lemMapJustApp :: ShS sh1 -> Proxy sh2
 lemMapJustApp ZSS _ = Refl
 lemMapJustApp (_ :$$ sh) p | Refl <- lemMapJustApp sh p = Refl
 
-lemMapJustTakeLen :: Perm is -> ShS sh -> TakeLen is (MapJust sh) :~: MapJust (TakeLen is sh)
-lemMapJustTakeLen PNil _ = Refl
-lemMapJustTakeLen (_ `PCons` is) (_ :$$ sh) | Refl <- lemMapJustTakeLen is sh = Refl
-lemMapJustTakeLen (_ `PCons` _) ZSS = error "TakeLen of empty"
-
-lemMapJustDropLen :: Perm is -> ShS sh -> DropLen is (MapJust sh) :~: MapJust (DropLen is sh)
-lemMapJustDropLen PNil _ = Refl
-lemMapJustDropLen (_ `PCons` is) (_ :$$ sh) | Refl <- lemMapJustDropLen is sh = Refl
-lemMapJustDropLen (_ `PCons` _) ZSS = error "DropLen of empty"
-
-lemMapJustIndex :: SNat i -> ShS sh -> Index i (MapJust sh) :~: Just (Index i sh)
-lemMapJustIndex SZ (_ :$$ _) = Refl
-lemMapJustIndex (SS (i :: SNat i')) ((_ :: SNat n) :$$ (sh :: ShS sh'))
-  | Refl <- lemMapJustIndex i sh
+lemTakeLenMapJust :: Perm is -> ShS sh -> TakeLen is (MapJust sh) :~: MapJust (TakeLen is sh)
+lemTakeLenMapJust PNil _ = Refl
+lemTakeLenMapJust (_ `PCons` is) (_ :$$ sh) | Refl <- lemTakeLenMapJust is sh = Refl
+lemTakeLenMapJust (_ `PCons` _) ZSS = error "TakeLen of empty"
+
+lemDropLenMapJust :: Perm is -> ShS sh -> DropLen is (MapJust sh) :~: MapJust (DropLen is sh)
+lemDropLenMapJust PNil _ = Refl
+lemDropLenMapJust (_ `PCons` is) (_ :$$ sh) | Refl <- lemDropLenMapJust is sh = Refl
+lemDropLenMapJust (_ `PCons` _) ZSS = error "DropLen of empty"
+
+lemIndexMapJust :: SNat i -> ShS sh -> Index i (MapJust sh) :~: Just (Index i sh)
+lemIndexMapJust SZ (_ :$$ _) = Refl
+lemIndexMapJust (SS (i :: SNat i')) ((_ :: SNat n) :$$ (sh :: ShS sh'))
+  | Refl <- lemIndexMapJust i sh
   , Refl <- lemIndexSucc (Proxy @i') (Proxy @(Just n)) (Proxy @(MapJust sh'))
   , Refl <- lemIndexSucc (Proxy @i') (Proxy @n) (Proxy @sh')
   = Refl
-lemMapJustIndex _ ZSS = error "Index of empty"
+lemIndexMapJust _ ZSS = error "Index of empty"
 
-lemMapJustPermute :: Perm is -> ShS sh -> Permute is (MapJust sh) :~: MapJust (Permute is sh)
-lemMapJustPermute PNil _ = Refl
-lemMapJustPermute (i `PCons` is) sh
-  | Refl <- lemMapJustPermute is sh
-  , Refl <- lemMapJustIndex i sh
+lemPermuteMapJust :: Perm is -> ShS sh -> Permute is (MapJust sh) :~: MapJust (Permute is sh)
+lemPermuteMapJust PNil _ = Refl
+lemPermuteMapJust (i `PCons` is) sh
+  | Refl <- lemPermuteMapJust is sh
+  , Refl <- lemIndexMapJust i sh
   = Refl
 
 lemKnownMapJust :: forall sh. KnownShS sh => Proxy sh -> Dict KnownShX (MapJust sh)
diff --git a/src/Data/Array/Nested/Internal/Shaped.hs b/src/Data/Array/Nested/Internal/Shaped.hs
index afa91eb..06c87b0 100644
--- a/src/Data/Array/Nested/Internal/Shaped.hs
+++ b/src/Data/Array/Nested/Internal/Shaped.hs
@@ -254,9 +254,9 @@ stranspose :: forall is sh a. (IsPermutation is, Rank is <= Rank sh, Elt a)
            => Perm is -> Shaped sh a -> Shaped (PermutePrefix is sh) a
 stranspose perm sarr@(Shaped arr)
   | Refl <- lemRankMapJust (sshape sarr)
-  , Refl <- lemMapJustTakeLen perm (sshape sarr)
-  , Refl <- lemMapJustDropLen perm (sshape sarr)
-  , Refl <- lemMapJustPermute perm (shsTakeLen perm (sshape sarr))
+  , Refl <- lemTakeLenMapJust perm (sshape sarr)
+  , Refl <- lemDropLenMapJust perm (sshape sarr)
+  , Refl <- lemPermuteMapJust perm (shsTakeLen perm (sshape sarr))
   , Refl <- lemMapJustApp (shsPermute perm (shsTakeLen perm (sshape sarr))) (Proxy @(DropLen is sh))
   = Shaped (mtranspose perm arr)
 
-- 
cgit v1.2.3-70-g09d2