permute package:Agda

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

freely intersperse options and non-options

Like permuteTel, but start with a context.

Permute telescope: permutes or drops the types in the telescope according to the given permutation. Assumes that the permutation preserves the dependencies in the telescope. For example (Andreas, 2016-12-18, issue #2344): tel = (A : Set) (X : _18 A) (i : Fin (_m_23 A X)) tel (de Bruijn) = 2:Set, 1:_18 0, 0:Fin(_m_23 1 0) flattenTel tel = 2:Set, 1:_18 0, 0:Fin(_m_23 1 0) |- [ Set, _18 2, Fin (_m_23 2 1) ] perm = 0,1,2 -> 0,1 (picks the first two) renaming _ perm = [var 0, var 1, error] -- THE WRONG RENAMING! renaming _ (flipP perm) = [error, var 1, var 0] -- The correct renaming! apply to flattened tel = ... |- [ Set, _18 1, Fin (_m_23 1 0) ] permute perm it = ... |- [ Set, _18 1 ] unflatten (de Bruijn) = 1:Set, 0: _18 0 unflatten = (A : Set) (X : _18 A)

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.