0 | module Data.Permutation
 1 |
 2 | import Data.List
 3 | import Data.Vect
 4 | import Data.NumIdr.Interfaces
 5 |
 6 | %default total
 7 |
 8 | ||| A permutation in `n` elements.
 9 | |||
10 | ||| Permutations are internally stored as a list of elements to swap in
11 | ||| right-to-left order. This allows for easy composition and inversion of
12 | ||| permutation values.
13 | export
14 | record Permutation n where
15 |   constructor MkPerm
16 |   swaps : List (Fin n, Fin n)
17 |
18 |
19 | ||| Construct a permutation that swaps two elements.
20 | export
21 | swap : (i,j : Fin n) -> Permutation n
22 | swap x y = MkPerm [(x,y)]
23 |
24 | ||| Construct a permutation that makes the listed swaps in right-to-left order.
25 | export
26 | swaps : List (Fin n, Fin n) -> Permutation n
27 | swaps = MkPerm
28 |
29 | ||| Add a swap to the end of a permutation.
30 | |||
31 | ||| `appendSwap sw p = swap sw *. p`
32 | export
33 | appendSwap : (i,j : Fin n) -> Permutation n -> Permutation n
34 | appendSwap i j (MkPerm a) = MkPerm ((i,j)::a)
35 |
36 | ||| Add a swap to the beginning of a permutation.
37 | |||
38 | ||| `prependSwap sw p = p *. swap sw`
39 | export
40 | prependSwap : (i,j : Fin n) -> Permutation n -> Permutation n
41 | prependSwap i j (MkPerm a) = MkPerm (a `snoc` (i,j))
42 |
43 |
44 | mon : Monoid (a -> a)
45 | mon = MkMonoid @{MkSemigroup (.)} id
46 |
47 |
48 | ||| Swap two elements of a `Vect`.
49 | export
50 | swapElems : (i,j : Fin n) -> Vect n a -> Vect n a
51 | swapElems i j v =
52 |   if i == j then v
53 |   else let x = index i v
54 |            y = index j v
55 |            in replaceAt j x $ replaceAt i y v
56 |
57 | ||| Permute the elements of a `Vect`.
58 | export
59 | permuteVect : Permutation n -> Vect n a -> Vect n a
60 | permuteVect p = foldMap @{%search} @{mon} (uncurry swapElems) p.swaps
61 |
62 |
63 | ||| Construct a function that swaps two values.
64 | export
65 | swapValues : (i,j : Fin n) -> Nat -> Nat
66 | swapValues i j x = if x == cast i then cast j
67 |                    else if x == cast j then cast i
68 |                    else x
69 |
70 | ||| Construct a function that permutes values.
71 | export
72 | permuteValues : Permutation n -> Nat -> Nat
73 | permuteValues p = foldMap @{%search} @{mon} (uncurry swapValues) p.swaps
74 |
75 |
76 |
77 | export
78 | Show (Permutation n) where
79 |   showPrec p (MkPerm a) = showCon p "swaps" $ showArg a
80 |
81 | export
82 | Mult (Permutation n) (Permutation n) (Permutation n) where
83 |   MkPerm a *. MkPerm b = MkPerm (a ++ b)
84 |
85 | export
86 | MultMonoid (Permutation n) where
87 |   identity = MkPerm []
88 |
89 | export
90 | MultGroup (Permutation n) where
91 |   inverse (MkPerm a) = MkPerm (reverse a)
92 |