| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Utils.Permutation
Synopsis
- data Permutation = Perm {}
- permute :: Permutation -> [a] -> [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
- topoSortM :: Monad m => (a -> a -> m Bool) -> [a] -> m (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.
Instances
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
Precondition for permute (Perm _ is) xsis
must be non-negative and, if xs is finite, then every index must
also be smaller than the length of xs.
The implementation is supposed to be extensionally equal to the
following one (if different exceptions are identified), but in some
cases more efficient:
permute (Perm _ is) xs = map (xs !!) is
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] (IntMap a) Source # | |
Defined in Agda.Utils.Permutation Methods inversePermute :: Permutation -> [Maybe a] -> IntMap a Source # | |
| InversePermute [Maybe a] [Maybe a] Source # | |
Defined in Agda.Utils.Permutation Methods inversePermute :: Permutation -> [Maybe a] -> [Maybe a] Source # | |
| InversePermute [Maybe a] [(Int, a)] Source # | |
Defined in Agda.Utils.Permutation Methods inversePermute :: Permutation -> [Maybe a] -> [(Int, a)] Source # | |
| InversePermute (Int -> a) [Maybe a] Source # | |
Defined in Agda.Utils.Permutation Methods inversePermute :: Permutation -> (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 | |
Instances
| Foldable Drop Source # | |
Defined in Agda.Utils.Permutation Methods fold :: Monoid m => Drop m -> m # foldMap :: Monoid m => (a -> m) -> Drop a -> m # foldMap' :: Monoid m => (a -> m) -> Drop a -> m # foldr :: (a -> b -> b) -> b -> Drop a -> b # foldr' :: (a -> b -> b) -> b -> Drop a -> b # foldl :: (b -> a -> b) -> b -> Drop a -> b # foldl' :: (b -> a -> b) -> b -> Drop a -> b # foldr1 :: (a -> a -> a) -> Drop a -> a # foldl1 :: (a -> a -> a) -> Drop a -> a # elem :: Eq a => a -> Drop a -> Bool # maximum :: Ord a => Drop a -> a # | |
| Traversable Drop Source # | |
| Functor Drop Source # | |
| KillRange a => KillRange (Drop a) Source # | |
Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (Drop a) Source # | |
| EmbPrj a => EmbPrj (Drop a) Source # | |
| DoDrop a => Abstract (Drop a) Source # | |
| DoDrop a => Apply (Drop a) Source # | |
| Show a => Show (Drop a) Source # | |
| Eq a => Eq (Drop a) Source # | |
| Ord a => Ord (Drop a) Source # | |
Things that support delayed dropping.
Minimal complete definition
Methods
Arguments
| :: Drop a | |
| -> a | Perform the dropping. |
Instances
| DoDrop Permutation Source # | |
Defined in Agda.Utils.Permutation Methods doDrop :: Drop Permutation -> Permutation Source # dropMore :: Int -> Drop Permutation -> Drop Permutation Source # unDrop :: Int -> Drop Permutation -> Drop Permutation Source # | |
| DoDrop [a] Source # | |