permute -package:combinatorial

The parser permute perm parses a permutation of parser described by perm. For example, suppose we want to parse a permutation of: an optional string of a's, the character b and an optional c. This can be described by:

test  = permute (tuple <$?> ("",many1 (char 'a'))
<||> char 'b'
<|?> ('_',char 'c'))
where
tuple a b c  = (a,b,c)

The parser permute perm parses a permutation of parser described by perm. For example, suppose we want to parse a permutation of: an optional string of a's, the character b and an optional c. This can be described by:

test  = permute (tuple <$?> ("",some (char 'a'))
<||> char 'b'
<|?> ('_',char 'c'))
where
tuple a b c  = (a,b,c)

Generate the next permutation of the sequence, returns False if this is the last permutation. Unimplemented

Forward permutation specified by an index mapping, ix. The result vector is initialized by the given defaults, def, and an further values that are permuted into the result are added to the current value using the given combination function, f. The combination function must be associative and commutative.

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

apply the permutation to a vector

Not on Stackage, so not searched. Generalised permutation parser combinator

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)

Constuct bin permutation from function.

Constuct bin permutation from table

Swap adjacent independent actions in the trace if a predicate holds.

Not on Stackage, so not searched. Permutations of effectful computations

O(n) Yield the vector obtained by replacing each element i of the index vector by xs!i. This is equivalent to map (xs!) is but is often much more efficient.

backpermute <a,b,c,d> <0,3,2,3,1,0> = <a,d,c,d,b,a>

Same as backpermute but without bounds checking.

O(n) Yield the vector obtained by replacing each element i of the index vector by xs!i. This is equivalent to map (xs!) is but is often much more efficient.

backpermute <a,b,c,d> <0,3,2,3,1,0> = <a,d,c,d,b,a>

O(n) Yield the vector obtained by replacing each element i of the index vector by xs!i. This is equivalent to map (xs!) is but is often much more efficient.

backpermute <a,b,c,d> <0,3,2,3,1,0> = <a,d,c,d,b,a>

Same as backpermute but without bounds checking.

O(n) Yield the vector obtained by replacing each element i of the index vector by xs!i. This is equivalent to map (xs!) is but is often much more efficient.

backpermute <a,b,c,d> <0,3,2,3,1,0> = <a,d,c,d,b,a>

Same as backpermute but without bounds checking.

Same as backpermute but without bounds checking.

Backwards permutation of an array's elements.

Default backwards permutation of an array's elements. If the function returns Nothing then the value at that index is taken from the default array (arrDft)