Agda.Utils.Permutation

Documentation

data Permutation

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.

Constructors

Perm

Fields

• permRange :: Int
• permPicks :: [Int]

Instances

Eq Permutation

Methods

(==) :: Permutation -> Permutation -> Bool

(/=) :: Permutation -> Permutation -> Bool

Show Permutation

Methods

showsPrec :: Int -> Permutation -> ShowS

show :: Permutation -> String

showList :: [Permutation] -> ShowS

Null Permutation

Methods

empty :: Permutation

null :: Permutation -> Bool

Sized Permutation

Methods

size :: Integral n => Permutation -> n

KillRange Permutation

Methods

killRange :: KillRangeT Permutation

DoDrop Permutation

Methods

doDrop :: Drop Permutation -> Permutation

dropMore :: Int -> Drop Permutation -> Drop Permutation

unDrop :: Int -> Drop Permutation -> Drop Permutation

DropArgs Permutation

Methods

dropArgs :: Int -> Permutation -> Permutation

PrettyTCM Permutation

Methods

prettyTCM :: Permutation -> TCM Doc

permute :: Permutation -> [a] -> [a]

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]

class InversePermute a b where

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.

Minimal complete definition

inversePermute

Methods

inversePermute :: Permutation -> a -> b

Instances

InversePermute [Maybe a] [Maybe a]

Methods

inversePermute :: Permutation -> [Maybe a] -> [Maybe a]

InversePermute [Maybe a] (IntMap a)

Methods

inversePermute :: Permutation -> [Maybe a] -> IntMap a

InversePermute [Maybe a] [(Int, a)]

Methods

inversePermute :: Permutation -> [Maybe a] -> [(Int, a)]

InversePermute (Int -> a) [Maybe a]

Methods

inversePermute :: Permutation -> (Int -> a) -> [Maybe a]

idP :: Int -> Permutation

Identity permutation.

takeP :: Int -> Permutation -> Permutation

Restrict a permutation to work on n elements, discarding picks >=n.

droppedP :: Permutation -> Permutation

Pick the elements that are not picked by the permutation.

liftP :: Int -> Permutation -> Permutation

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

permute (compose p1 p2) == permute p1 . permute p2

invertP :: Int -> Permutation -> Permutation

invertP err p is the inverse of p where defined, otherwise defaults to err. composeP p (invertP err p) == p

compactP :: Permutation -> Permutation

Turn a possible non-surjective permutation into a surjective permutation.

reverseP :: Permutation -> Permutation

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

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

expandP i n π in the domain of π replace the ith element by n elements.

topoSort :: (a -> a -> Bool) -> [a] -> Maybe Permutation

Stable topologic sort. The first argument decides whether its first argument is an immediate parent to its second argument.

Drop (apply) and undrop (abstract)

data Drop a

Delayed dropping which allows undropping.

Constructors

Drop

Fields

• dropN :: Int

  Non-negative number of things to drop.

• dropFrom :: a

  Where to drop from.

Instances

Functor Drop

Methods

fmap :: (a -> b) -> Drop a -> Drop b

(<$) :: a -> Drop b -> Drop a

Foldable Drop

Methods

fold :: Monoid m => Drop m -> 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

toList :: Drop a -> [a]

null :: Drop a -> Bool

length :: Drop a -> Int

elem :: Eq a => a -> Drop a -> Bool

maximum :: Ord a => Drop a -> a

minimum :: Ord a => Drop a -> a

sum :: Num a => Drop a -> a

product :: Num a => Drop a -> a

Traversable Drop

Methods

traverse :: Applicative f => (a -> f b) -> Drop a -> f (Drop b)

sequenceA :: Applicative f => Drop (f a) -> f (Drop a)

mapM :: Monad m => (a -> m b) -> Drop a -> m (Drop b)

sequence :: Monad m => Drop (m a) -> m (Drop a)

Eq a => Eq (Drop a)

Methods

(==) :: Drop a -> Drop a -> Bool

(/=) :: Drop a -> Drop a -> Bool

Ord a => Ord (Drop a)

Methods

compare :: Drop a -> Drop a -> Ordering

(<) :: Drop a -> Drop a -> Bool

(<=) :: Drop a -> Drop a -> Bool

(>) :: Drop a -> Drop a -> Bool

(>=) :: Drop a -> Drop a -> Bool

max :: Drop a -> Drop a -> Drop a

min :: Drop a -> Drop a -> Drop a

Show a => Show (Drop a)

Methods

showsPrec :: Int -> Drop a -> ShowS

show :: Drop a -> String

showList :: [Drop a] -> ShowS

KillRange a => KillRange (Drop a)

Methods

killRange :: KillRangeT (Drop a)

class DoDrop a where

Things that support delayed dropping.

Minimal complete definition

doDrop

Methods

doDrop :: Drop a -> a

dropMore :: Int -> Drop a -> Drop a

unDrop :: Int -> Drop a -> Drop a

Instances

DoDrop Permutation

Methods

doDrop :: Drop Permutation -> Permutation

dropMore :: Int -> Drop Permutation -> Drop Permutation

unDrop :: Int -> Drop Permutation -> Drop Permutation

DoDrop [a]

Methods

doDrop :: Drop [a] -> [a]

dropMore :: Int -> Drop [a] -> Drop [a]

unDrop :: Int -> Drop [a] -> Drop [a]