Agda-2.5.1.2: A dependently typed functional programming language and proof assistant

Agda.Utils.Permutation

Synopsis

# Documentation

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 FieldspermRange :: Int permPicks :: [Int]

Instances

 Source # Methods Source # MethodsshowList :: [Permutation] -> ShowS # Source # Methods Source # Methods Source # Methodssize :: Integral n => Permutation -> n Source # Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods

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

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.

Minimal complete definition

inversePermute

Methods

inversePermute :: Permutation -> a -> b Source #

Instances

 InversePermute [Maybe a] [Maybe a] Source # MethodsinversePermute :: Permutation -> [Maybe a] -> [Maybe a] Source # InversePermute [Maybe a] (IntMap a) Source # MethodsinversePermute :: Permutation -> [Maybe a] -> IntMap a Source # InversePermute [Maybe a] [(Int, a)] Source # MethodsinversePermute :: Permutation -> [Maybe a] -> [(Int, a)] Source # InversePermute (Int -> a) [Maybe a] Source # MethodsinversePermute :: Permutation -> (Int -> a) -> [Maybe a] Source #

Identity permutation.

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

Pick the elements that are not picked by the 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.

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

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

Turn a possible non-surjective permutation into a surjective 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.

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 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)

data Drop a Source #

Delayed dropping which allows undropping.

Constructors

 Drop FieldsdropN :: IntNon-negative number of things to drop.dropFrom :: aWhere to drop from.

Instances

 Source # Methodsfmap :: (a -> b) -> Drop a -> Drop b #(<\$) :: a -> Drop b -> Drop a # Source # Methodsfold :: 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 # Source # Methodstraverse :: 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) Source # Methods(==) :: Drop a -> Drop a -> Bool #(/=) :: Drop a -> Drop a -> Bool # Ord a => Ord (Drop a) Source # Methodscompare :: 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) Source # MethodsshowsPrec :: Int -> Drop a -> ShowS #show :: Drop a -> String #showList :: [Drop a] -> ShowS # KillRange a => KillRange (Drop a) Source # Methods DoDrop a => Abstract (Drop a) Source # Methodsabstract :: Telescope -> Drop a -> Drop a Source # DoDrop a => Apply (Drop a) Source # Methodsapply :: Drop a -> Args -> Drop a Source #applyE :: Drop a -> Elims -> Drop a Source #

class DoDrop a where Source #

Things that support delayed dropping.

Minimal complete definition

doDrop

Methods

doDrop :: Drop a -> a Source #

dropMore :: Int -> Drop a -> Drop a Source #

unDrop :: Int -> Drop a -> Drop a Source #

Instances

 Source # Methods DoDrop [a] Source # MethodsdoDrop :: Drop [a] -> [a] Source #dropMore :: Int -> Drop [a] -> Drop [a] Source #unDrop :: Int -> Drop [a] -> Drop [a] Source #