Agda-2.2.10: A dependently typed functional programming language and proof assistant

Agda.Utils.Permutation

Synopsis

- data Permutation = Perm Integer [Integer]
- permute :: Permutation -> [a] -> [a]
- idP :: Integer -> Permutation
- takeP :: Integer -> Permutation -> Permutation
- composeP :: Permutation -> Permutation -> Permutation
- invertP :: Permutation -> Permutation
- compactP :: Permutation -> Permutation
- reverseP :: Permutation -> Permutation
- expandP :: Integer -> Integer -> Permutation -> Permutation
- topoSort :: (a -> a -> Bool) -> [a] -> Maybe Permutation

# Documentation

data Permutation

    permute [2,3,1] [x,y,z] = [y,z,x]

Constructors

Perm Integer [Integer] |

Instances

Eq Permutation |
Data Permutation |
Show Permutation |
Typeable Permutation |
Sized Permutation |
Abstract Permutation |
Apply Permutation |
EmbPrj Permutation |

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

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

idP :: Integer -> Permutation

takeP :: Integer -> Permutation -> Permutation

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

expandP :: Integer -> Integer -> 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.