From 5a802da40e5836ee19d46b9a2c771912dbff010e Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom@tomsmeding.com>
Date: Tue, 28 May 2024 17:36:47 +0200
Subject: applyPerm* functions

---
 src/Data/Array/Mixed.hs | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

(limited to 'src/Data/Array/Mixed.hs')

diff --git a/src/Data/Array/Mixed.hs b/src/Data/Array/Mixed.hs
index 6766d90..4ae89a1 100644
--- a/src/Data/Array/Mixed.hs
+++ b/src/Data/Array/Mixed.hs
@@ -866,6 +866,15 @@ invertPermutation = \perm k ->
     provePermInverse :: HList SNat is -> HList SNat is' -> StaticShX sh -> Maybe (Permute is' (Permute is sh) :~: sh)
     provePermInverse perm perminv ssh = geqStaticShX (ssxPermute perminv (ssxPermute perm ssh)) ssh
 
+applyPermX :: forall f is sh. HList SNat is -> ListX sh f -> ListX (PermutePrefix is sh) f
+applyPermX perm sh = listxAppend (listxPermute perm (listxTakeLen perm sh)) (listxDropLen perm sh)
+
+applyPermIxX :: forall i is sh. HList SNat is -> IxX sh i -> IxX (PermutePrefix is sh) i
+applyPermIxX = coerce (applyPermX @(Const i))
+
+applyPermShX :: forall i is sh. HList SNat is -> ShX sh i -> ShX (PermutePrefix is sh) i
+applyPermShX = coerce (applyPermX @(SMayNat i SNat))
+
 class KnownNatList l where makeNatList :: HList SNat l
 instance KnownNatList '[] where makeNatList = HNil
 instance (KnownNat n, KnownNatList l) => KnownNatList (n : l) where makeNatList = natSing `HCons` makeNatList
@@ -881,8 +890,7 @@ transpose ssh perm (XArray arr)
   , Refl <- lemRankApp (ssxPermute perm (ssxTakeLen perm ssh)) (ssxDropLen perm ssh)
   , Refl <- lemRankPermute (Proxy @(TakeLen is sh)) perm
   , Refl <- lemRankDropLen ssh perm
-  = let perm' = foldHList (\sn -> [fromSNat' sn]) perm :: [Int]
-    in XArray (S.transpose perm' arr)
+  = XArray (S.transpose (permToList perm) arr)
 
 -- | The list argument gives indices into the original dimension list.
 --
-- 
cgit v1.2.3-70-g09d2