| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Agda.Utils.Permutation
Contents
- data Permutation = Perm {}
- permute :: Permutation -> [a] -> [a]
- safePermute :: Permutation -> [a] -> [Maybe a]
- class InversePermute a b where
- inversePermute :: Permutation -> a -> b
- idP :: Int -> Permutation
- takeP :: Int -> Permutation -> Permutation
- droppedP :: Permutation -> Permutation
- liftP :: Int -> Permutation -> Permutation
- composeP :: Permutation -> Permutation -> Permutation
- invertP :: Int -> Permutation -> Permutation
- compactP :: Permutation -> Permutation
- reverseP :: Permutation -> Permutation
- flipP :: 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
safePermute :: Permutation -> [a] -> [Maybe a] Source
class InversePermute a b where Source
Invert a Permutation on a partial finite int map.
inversePermute perm f = f'
such that permute perm f' = f
Example, with map represented as [Maybe a]:
f = [Nothing, Just a, Just b ]
perm = Perm 4 [3,0,2]
f' = [ Just a , Nothing , Just b , Nothing ]
Zipping perm with f gives [(0,a),(2,b)], after compression
with catMaybes. This is an IntMap which can easily
written out into a substitution again.
Methods
inversePermute :: Permutation -> a -> b Source
Instances
| InversePermute [Maybe a] [Maybe a] Source | |
| InversePermute [Maybe a] (IntMap a) Source | |
| InversePermute [Maybe a] [(Int, a)] Source | |
| InversePermute (Int -> a) [Maybe a] Source |
idP :: Int -> Permutation Source
Identity permutation.
takeP :: Int -> Permutation -> Permutation Source
Restrict a permutation to work on n elements, discarding picks >=n.
droppedP :: Permutation -> Permutation Source
Pick the elements that are not picked by the permutation.
liftP :: Int -> Permutation -> Permutation Source
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 Source
permute (compose p1 p2) == permute p1 . permute p2
invertP :: Int -> Permutation -> Permutation Source
invertP err p is the inverse of p where defined,
otherwise defaults to err.
composeP p (invertP err p) == p
compactP :: Permutation -> Permutation Source
Turn a possible non-surjective permutation into a surjective permutation.
reverseP :: Permutation -> Permutation Source
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]
With reverseP, you can convert a permutation on de Bruijn indices
to one on de Bruijn levels, and vice versa.
flipP :: Permutation -> Permutation Source
permPicks (flipP p) = permute p (downFrom (permRange p))
or
permute (flipP (Perm n xs)) [0..n-1] = permute (Perm n xs) (downFrom n)
Can be use to turn a permutation from (de Bruijn) levels to levels to one from levels to indices.
See numberPatVars.
expandP :: Int -> Int -> Permutation -> Permutation Source
expandP i n π in the domain of π replace the ith element by n elements.
topoSort :: (a -> a -> Bool) -> [a] -> Maybe Permutation Source
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 | |
Things that support delayed dropping.
Minimal complete definition
Methods
Arguments
| :: Drop a | |
| -> a | Perform the dropping. |
Instances