Agda.Utils.Permutation

Documentation

data Permutation

permute [1,2,0] [x0,x1,x2] = [x1,x2,x0]

Agda typing would be: Perm : {m : Nat}(n : Nat) -> Vec (Fin n) m -> Permutation m is the size of the permutation.

Constructors

Perm

Fields

permRange :: Int

permPicks :: [Int]

Instances

Eq Permutation

Show Permutation

Typeable Permutation

Sized Permutation

Abstract Permutation

Apply Permutation

DropArgs Permutation

EmbPrj Permutation

permute :: Permutation -> [a] -> [a]

permute [1,2,0] [x0,x1,x2] = [x1,x2,x0] More precisely, permute indices list = sublist, generates sublist from list by picking the elements of list as indicated by indices. permute [1,3,0] [x0,x1,x2,x3] = [x1,x3,x0]

Agda typing: permute (Perm {m} n is) : Vec A m -> Vec A n

idP :: Int -> Permutation

takeP :: Int -> Permutation -> Permutation

liftP :: Int -> Permutation -> Permutation

liftP k takes a Perm {m} n to a Perm {m+k} (n+k). Analogous to liftS, but Permutations operate on de Bruijn LEVELS, not indices.

composeP :: Permutation -> Permutation -> Permutation

permute (compose p1 p2) == permute p1 . permute p2

invertP :: Permutation -> Permutation

compactP :: Permutation -> Permutation

Turn a possible non-surjective permutation into a surjective permutation.

reverseP :: Permutation -> Permutation

permute (reverseP p) xs ==
    reverse $ permute p $ reverse xs

Example: permute (reverseP (Perm 4 [1,3,0])) [x0,x1,x2,x3] == permute (Perm 4 $ map (3-) [0,3,1]) [x0,x1,x2,x3] == permute (Perm 4 [3,0,2]) [x0,x1,x2,x3] == [x3,x0,x2] == reverse [x2,x0,x3] == reverse $ permute (Perm 4 [1,3,0]) [x3,x2,x1,x0] == reverse $ permute (Perm 4 [1,3,0]) $ reverse [x0,x1,x2,x3]

expandP :: Int -> Int -> Permutation -> Permutation

expandP i n π in the domain of π replace the ith element by n elements.

topoSort :: (a -> a -> Bool) -> [a] -> Maybe Permutation

Stable topologic sort. The first argument decides whether its first argument is an immediate parent to its second argument.