Add permId and permShiftNmvecsReplicate

1 files changed, 36 insertions, 0 deletions

diff --git a/src/Data/Array/Nested/Permutation.hs b/src/Data/Array/Nested/Permutation.hs
index ecdb06d..2dd4e3a 100644
--- a/src/Data/Array/Nested/Permutation.hs
+++ b/src/Data/Array/Nested/Permutation.hs
@@ -307,6 +307,42 @@ permShift1 = (SNat @0 `PCons`) . permMapSucc
     permMapSucc PNil = PNil
     permMapSucc ((SNat :: SNat i) `PCons` ns) = SNat @(i + 1) `PCons` permMapSucc ns
 
+type family PermId n where
+  PermId 0 = '[0]
+  PermId n = PermId (n - 1) ++ '[n]
+
+{- Doesn't type-check:
+permId :: SNat n -> Perm (PermId n)
+permId SZ = PCons SZ PNil
+permId (SS k) = permId k `permAppend` PCons (SS k) PNil
+-}
+permId :: forall n. SNat n -> Perm (PermId n)
+permId n = go SZ
+  where
+    go :: forall k l. SNat k -> Perm l
+    go k = if fromSNat' k > fromSNat' n
+           then gcastWith (unsafeCoerceRefl :: (l :~: '[])) $
+                PNil
+           else gcastWith (unsafeCoerceRefl :: (l :~: k : anything)) $
+                k `PCons` go (SS k)
+
+-- Note that the second argument is not a valid permutation.
+permAppend :: Perm l -> Perm l2 -> Perm (l ++ l2)
+permAppend PNil l2 = l2
+permAppend (n `PCons` rest) l2 = n `PCons` permAppend rest l2
+
+type family MapPlusN n is where
+  MapPlusN n '[] = '[]
+  MapPlusN n (i : is) = i + n : MapPlusN n is
+
+-- TODO: instead of permAppend and permShiftN define permComp :: Perm l1 -> Perm l2 -> Perm (l1 ++ MapPlusN (Rank l1) l2), where all three are valid permutations
+permShiftN :: forall n l. SNat n -> Perm l -> Perm (PermId n ++ MapPlusN n l)
+permShiftN n@SNat = (permId n `permAppend`) . permMapPlusN
+  where
+    permMapPlusN :: Perm l1 -> Perm (MapPlusN n l1)
+    permMapPlusN PNil = PNil
+    permMapPlusN ((SNat :: SNat i) `PCons` ns) = SNat @(i + n) `PCons` permMapPlusN ns
+
 
 -- * Lemmas