diff options
author | Tom Smeding <tom@tomsmeding.com> | 2024-05-28 17:36:47 +0200 |
---|---|---|
committer | Tom Smeding <tom@tomsmeding.com> | 2024-05-28 17:36:47 +0200 |
commit | 5a802da40e5836ee19d46b9a2c771912dbff010e (patch) | |
tree | 9c794b27f6c861335e007a68dbb559776d1ffaaa /src/Data/Array/Mixed.hs | |
parent | 6b74bff29ea3c21adaeea12921aed057b5858040 (diff) |
applyPerm* functions
Diffstat (limited to 'src/Data/Array/Mixed.hs')
-rw-r--r-- | src/Data/Array/Mixed.hs | 12 |
1 files changed, 10 insertions, 2 deletions
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. -- |