Safe Haskell | None |
---|---|

Language | Haskell2010 |

## Synopsis

- data Permutation = Perm {}
- permute :: Permutation -> [a] -> [a]
- safePermute :: Permutation -> [a] -> [Maybe a]
- class InversePermute a b where
- inversePermute :: Permutation -> a -> b

- idP :: Int -> Permutation
- takeP :: Int -> Permutation -> Permutation
- droppedP :: Permutation -> Permutation
- liftP :: Int -> Permutation -> Permutation
- composeP :: Permutation -> Permutation -> Permutation
- invertP :: Int -> Permutation -> Permutation
- compactP :: Permutation -> Permutation
- reverseP :: Permutation -> Permutation
- flipP :: Permutation -> Permutation
- expandP :: Int -> Int -> Permutation -> Permutation
- topoSort :: (a -> a -> Bool) -> [a] -> Maybe Permutation
- data Drop a = Drop {}
- class DoDrop a where

# Documentation

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.

## Instances

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`

safePermute :: Permutation -> [a] -> [Maybe a] Source #

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 #

## Instances

InversePermute [Maybe a] [Maybe a] Source # | |

Defined in Agda.Utils.Permutation inversePermute :: Permutation -> [Maybe a] -> [Maybe a] Source # | |

InversePermute [Maybe a] (IntMap a) Source # | |

Defined in Agda.Utils.Permutation inversePermute :: Permutation -> [Maybe a] -> IntMap a Source # | |

InversePermute [Maybe a] [(Int, a)] Source # | |

Defined in Agda.Utils.Permutation inversePermute :: Permutation -> [Maybe a] -> [(Int, a)] Source # | |

InversePermute (Int -> a) [Maybe a] Source # | |

Defined in Agda.Utils.Permutation inversePermute :: Permutation -> (Int -> a) -> [Maybe a] 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 *i*th 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)

Delayed dropping which allows undropping.

## Instances

Functor Drop Source # | |

Foldable Drop Source # | |

Defined in Agda.Utils.Permutation fold :: Monoid m => Drop m -> m # foldMap :: Monoid m => (a -> m) -> Drop a -> m # foldr :: (a -> b -> b) -> b -> Drop a -> b # foldr' :: (a -> b -> b) -> b -> Drop a -> b # foldl :: (b -> a -> b) -> b -> Drop a -> b # foldl' :: (b -> a -> b) -> b -> Drop a -> b # foldr1 :: (a -> a -> a) -> Drop a -> a # foldl1 :: (a -> a -> a) -> Drop a -> a # elem :: Eq a => a -> Drop a -> Bool # maximum :: Ord a => Drop a -> a # | |

Traversable Drop Source # | |

Eq a => Eq (Drop a) Source # | |

Data a => Data (Drop a) Source # | |

Defined in Agda.Utils.Permutation gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Drop a -> c (Drop a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Drop a) # toConstr :: Drop a -> Constr # dataTypeOf :: Drop a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Drop a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Drop a)) # gmapT :: (forall b. Data b => b -> b) -> Drop a -> Drop a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Drop a -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Drop a -> r # gmapQ :: (forall d. Data d => d -> u) -> Drop a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Drop a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Drop a -> m (Drop a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Drop a -> m (Drop a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Drop a -> m (Drop a) # | |

Ord a => Ord (Drop a) Source # | |

Show a => Show (Drop a) Source # | |

KillRange a => KillRange (Drop a) Source # | |

Defined in Agda.Utils.Permutation killRange :: KillRangeT (Drop a) Source # | |

DoDrop a => Abstract (Drop a) Source # | |

DoDrop a => Apply (Drop a) Source # | |

EmbPrj a => EmbPrj (Drop a) Source # | |

Things that support delayed dropping.

:: Drop a | |

-> a | Perform the dropping. |

## Instances

DoDrop Permutation Source # | |

Defined in Agda.Utils.Permutation doDrop :: Drop Permutation -> Permutation Source # dropMore :: Int -> Drop Permutation -> Drop Permutation Source # unDrop :: Int -> Drop Permutation -> Drop Permutation Source # | |

DoDrop [a] Source # | |