| Safe Haskell | None |
|---|
Agda.Utils.Permutation
- data Permutation = Perm {}
- permute :: Permutation -> [a] -> [a]
- idP :: Int -> Permutation
- takeP :: Int -> Permutation -> Permutation
- droppedP :: Permutation -> Permutation
- liftP :: Int -> Permutation -> Permutation
- composeP :: Permutation -> Permutation -> Permutation
- invertP :: Permutation -> Permutation
- compactP :: Permutation -> Permutation
- reverseP :: Permutation -> Permutation
- expandP :: Int -> Int -> Permutation -> Permutation
- topoSort :: (a -> a -> Bool) -> [a] -> Maybe Permutation
- data Drop a = Drop {}
- class DoDrop a where
Documentation
data Permutation Source
Partial permutations. Examples:
permute [1,2,0] [x0,x1,x2] = [x1,x2,x0] (proper permutation).
permute [1,0] [x0,x1,x2] = [x1,x0] (partial permuation).
permute [1,0,1,2] [x0,x1,x2] = [x1,x0,x1,x2] (not a permutation because not invertible).
Agda typing would be:
Perm : {m : Nat}(n : Nat) -> Vec (Fin n) m -> Permutation
m is the size of the permutation.
permute :: Permutation -> [a] -> [a]Source
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 -> PermutationSource
Identity permutation.
takeP :: Int -> Permutation -> PermutationSource
Restrict a permutation to work on n elements, discarding picks >=n.
droppedP :: Permutation -> PermutationSource
Pick the elements that are not picked by the permutation.
liftP :: Int -> Permutation -> PermutationSource
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 -> PermutationSource
permute (compose p1 p2) == permute p1 . permute p2
compactP :: Permutation -> PermutationSource
Turn a possible non-surjective permutation into a surjective permutation.
reverseP :: Permutation -> PermutationSource
permute (reverseP p) xs ==
reverse $ permute p $ reverse xsExample:
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 -> PermutationSource
topoSort :: (a -> a -> Bool) -> [a] -> Maybe PermutationSource
Stable topologic sort. The first argument decides whether its first argument is an immediate parent to its second argument.
Drop (apply) and undrop (abstract)
Delayed dropping which allows undropping.
Constructors
| Drop | |