Agda.Utils.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.

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) xs: Every index in is 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

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.

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 Agda.TypeChecking.Substitution.liftS, but Permutations operate on de Bruijn LEVELS, not indices.

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 Agda.Syntax.Internal.Patterns.numberPatVars.

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

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

Delayed dropping which allows undropping.

Things that support delayed dropping.