| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Utils.Permutation
Synopsis
- 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
- 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
| Eq Permutation Source # | |
Defined in Agda.Utils.Permutation | |
| Data Permutation Source # | |
Defined in Agda.Utils.Permutation Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Permutation -> c Permutation gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Permutation toConstr :: Permutation -> Constr dataTypeOf :: Permutation -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Permutation) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Permutation) gmapT :: (forall b. Data b => b -> b) -> Permutation -> Permutation gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Permutation -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Permutation -> r gmapQ :: (forall d. Data d => d -> u) -> Permutation -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Permutation -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Permutation -> m Permutation gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Permutation -> m Permutation gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Permutation -> m Permutation | |
| Show Permutation Source # | |
Defined in Agda.Utils.Permutation Methods showsPrec :: Int -> Permutation -> ShowS show :: Permutation -> String showList :: [Permutation] -> ShowS | |
| Generic Permutation Source # | |
Defined in Agda.Utils.Permutation Associated Types type Rep Permutation :: Type -> Type | |
| NFData Permutation Source # | |
Defined in Agda.Utils.Permutation Methods rnf :: Permutation -> () | |
| Null Permutation Source # | |
Defined in Agda.Utils.Permutation | |
| Sized Permutation Source # | |
Defined in Agda.Utils.Permutation Methods size :: Permutation -> Int Source # | |
| 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 # | |
| KillRange Permutation Source # | |
Defined in Agda.Syntax.Position Methods | |
| Abstract Permutation Source # | |
Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Permutation -> Permutation Source # | |
| Apply Permutation Source # | |
Defined in Agda.TypeChecking.Substitute Methods apply :: Permutation -> Args -> Permutation Source # applyE :: Permutation -> Elims -> Permutation Source # | |
| EmbPrj Permutation Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Permutation -> S Int32 Source # icod_ :: Permutation -> S Int32 Source # value :: Int32 -> R Permutation Source # | |
| PrettyTCM Permutation Source # | |
Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Permutation -> m Doc Source # | |
| DropArgs Permutation Source # | |
Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> Permutation -> Permutation Source # | |
| type Rep Permutation Source # | |
Defined in Agda.Utils.Permutation type Rep Permutation = D1 ('MetaData "Permutation" "Agda.Utils.Permutation" "Agda-2.6.2-2fIO0qzLA6fLZRIj4yF8z4" 'False) (C1 ('MetaCons "Perm" 'PrefixI 'True) (S1 ('MetaSel ('Just "permRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Just "permPicks") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Int]))) | |
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 # | |
Defined in Agda.Utils.Permutation Methods inversePermute :: Permutation -> [Maybe a] -> [Maybe a] Source # | |
| InversePermute [Maybe a] (IntMap a) Source # | |
Defined in Agda.Utils.Permutation Methods inversePermute :: Permutation -> [Maybe a] -> IntMap 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.
topoSortM :: Monad m => (a -> a -> m Bool) -> [a] -> m (Maybe Permutation) Source #
Drop (apply) and undrop (abstract)
Delayed dropping which allows undropping.
Constructors
| Drop | |
Instances
| Functor Drop Source # | |
| 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 # | |
| Eq a => Eq (Drop a) Source # | |
| Data a => Data (Drop a) Source # | |
Defined in Agda.Utils.Permutation Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Drop a -> c (Drop a) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Drop a) dataTypeOf :: Drop a -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Drop a)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Drop a)) gmapT :: (forall b. Data b => b -> b) -> Drop a -> Drop a gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Drop a -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Drop a -> r gmapQ :: (forall d. Data d => d -> u) -> Drop a -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Drop a -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Drop a -> m (Drop a) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Drop a -> m (Drop a) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Drop a -> m (Drop a) | |
| Ord a => Ord (Drop a) Source # | |
| Show a => Show (Drop a) Source # | |
| KillRange a => KillRange (Drop a) Source # | |
Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (Drop a) Source # | |
| DoDrop a => Abstract (Drop a) Source # | |
| DoDrop a => Apply (Drop a) Source # | |
| EmbPrj a => EmbPrj (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 # | |