Agda-2.4.2.4: 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]

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.

Methods

inversePermute :: Permutation -> a -> b Source

Instances

 InversePermute [Maybe a] [Maybe a] Source InversePermute [Maybe a] (IntMap a) Source InversePermute [Maybe a] [(Int, a)] Source InversePermute (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 Source Source Eq a => Eq (Drop a) Source Ord a => Ord (Drop a) Source Show a => Show (Drop a) Source KillRange a => KillRange (Drop a) Source DoDrop a => Abstract (Drop a) Source DoDrop a => Apply (Drop a) Source EmbPrj a => EmbPrj (Drop a) Source

class DoDrop a where Source

Things that support delayed dropping.

Minimal complete definition

doDrop

Methods

Arguments

 :: Drop a -> a Perform the dropping.

Arguments

 :: Int -> Drop a -> Drop a Drop more.

Arguments

 :: Int -> Drop a -> Drop a Pick up dropped stuff.

Instances

 Source DoDrop [a] Source