Safe Haskell | None |
---|---|
Language | Haskell98 |
- 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.
inversePermute :: Permutation -> a -> b Source
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 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]
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.
Things that support delayed dropping.
:: Drop a | |
-> a | Perform the dropping. |