Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone





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.




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

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

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)

data Drop a Source

Delayed dropping which allows undropping.




dropN :: Int

Non-negative number of things to drop.

dropFrom :: a

Where to drop from.

class DoDrop a where Source

Things that support delayed dropping.

Minimal complete definition



doDrop Source


:: Drop a 
-> a

Perform the dropping.

dropMore Source


:: Int 
-> Drop a 
-> Drop a

Drop more.

unDrop Source


:: Int 
-> Drop a 
-> Drop a

Pick up dropped stuff.

Test data generator

Properties, see Agda.Utils.Permutation.Tests.