Create Data.Permutation

src/Data/NumIdr/Array/Coords.idr

@@ -9,7 +9,7 @@ import Data.NP
 
 
 -- A Nat-based range function with better semantics
-public export
+export
 range : Nat -> Nat -> List Nat
 range x y = if x < y then assert_total $ takeBefore (>= y) (countFrom x S)
                      else []

src/Data/NumIdr/Matrix.idr

@@ -92,12 +92,12 @@ indexNB m n = indexNB [m,n]
 ||| Return a row of the matrix as a vector.
 export
 getRow : Fin m -> Matrix m n a -> Vector n a
-getRow r mat = rewrite sym (rangeLenZ n) in mat !!.. [One r, All]
+getRow r mat = rewrite sym (rangeLenZ n) in mat!!..[One r, All]
 
 ||| Return a column of the matrix as a vector.
 export
 getColumn : Fin n -> Matrix m n a -> Vector m a
-getColumn c mat = rewrite sym (rangeLenZ m) in mat !!.. [All, One c]
+getColumn c mat = rewrite sym (rangeLenZ m) in mat!!..[All, One c]
 
 
 export
@@ -114,7 +114,7 @@ diagonal mat with (viewShape mat)
 -- TODO: throw an actual proof in here to avoid the unsafety
 export
 minor : Fin (S m) -> Fin (S n) -> Matrix (S m) (S n) a -> Matrix m n a
-minor i j mat = believe_me $ mat !!.. [Filter (/=i), Filter (/=j)]
+minor i j mat = believe_me $ mat!!..[Filter (/=i), Filter (/=j)]
 
 
 --------------------------------------------------------------------------------

src/Data/Permutation.idr

@@ -0,0 +1,64 @@
+module Data.Permutation
+
+import Data.List
+import Data.Vect
+import Data.NumIdr.Multiply
+
+
+export
+record Permutation n where
+  constructor MkPerm
+  swaps : List (Fin n, Fin n)
+
+
+export
+swap : (i,j : Fin n) -> Permutation n
+swap x y = MkPerm [(x,y)]
+
+export
+appendSwap : (i,j : Fin n) -> Permutation n -> Permutation n
+appendSwap i j (MkPerm a) = MkPerm ((i,j)::a)
+
+export
+prependSwap : (i,j : Fin n) -> Permutation n -> Permutation n
+prependSwap i j (MkPerm a) = MkPerm (a `snoc` (i,j))
+
+
+mon : Monoid (a -> a)
+mon = MkMonoid @{MkSemigroup (.)} id
+
+
+export
+swapElems : (i,j : Fin n) -> Vect n a -> Vect n a
+swapElems i j v =
+  if i == j then v
+  else let x = index i v
+           y = index j v
+           in replaceAt j x $ replaceAt i y v
+
+export
+permuteVect : Permutation n -> Vect n a -> Vect n a
+permuteVect p = foldMap @{%search} @{mon} (\(i,j) => swapElems i j) p.swaps
+
+
+export
+swapValues : (i,j : Fin n) -> Nat -> Nat
+swapValues i j x = if x == cast i then cast j
+                   else if x == cast j then cast i
+                   else x
+
+export
+permuteValues : Permutation n -> Nat -> Nat
+permuteValues p = foldMap @{%search} @{mon} (\(i,j) => swapValues i j) p.swaps
+
+export
+Mult (Permutation n) (Permutation n) (Permutation n) where
+  MkPerm a *. MkPerm b = MkPerm (a ++ b)
+
+export
+MultMonoid (Permutation n) where
+  identity = MkPerm []
+
+export
+MultGroup (Permutation n) where
+  inverse (MkPerm a) = MkPerm (reverse a)