Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Utils.Permutation

Contents

- Drop (apply) and undrop (abstract)

Synopsis

- data Permutation = Perm {
  - permRange :: Int
  - permPicks :: [Int]
  }
- permute :: Permutation -> [a] -> [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
- topoSortM :: Monad m => (a -> a -> m Bool) -> [a] -> m (Maybe Permutation)
- data Drop a = Drop {
  - dropN :: Int
  - dropFrom :: a
  }
- class DoDrop a where
  - doDrop :: Drop a -> a
  - dropMore :: Int -> Drop a -> Drop a
  - unDrop :: Int -> Drop a -> Drop a

# 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.

Constructors

Perm |

Fields

- permRange :: Int
- permPicks :: [Int]

#### Instances

Instances details

KillRange Permutation Source # |
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT Permutation Source #
DropArgs Permutation Source # |
Instance details Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> Permutation -> Permutation Source #
PrettyTCM Permutation Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Permutation -> m Doc Source #
EmbPrj Permutation Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Permutation -> S Word32 Source # icod_ :: Permutation -> S Word32 Source # value :: Word32 -> R Permutation Source #
Abstract Permutation Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Permutation -> Permutation Source #
Apply Permutation Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Permutation -> Args -> Permutation Source # applyE :: Permutation -> Elims -> Permutation Source #
Null Permutation Source # |
Instance details Defined in Agda.Utils.Permutation Methods empty :: Permutation Source # null :: Permutation -> Bool Source #
DoDrop Permutation Source # |
Instance details Defined in Agda.Utils.Permutation Methods doDrop :: Drop Permutation -> Permutation Source # dropMore :: Int -> Drop Permutation -> Drop Permutation Source # unDrop :: Int -> Drop Permutation -> Drop Permutation Source #
Sized Permutation Source # |
Instance details Defined in Agda.Utils.Permutation Methods size :: Permutation -> Int Source # natSize :: Permutation -> Peano Source #
NFData Permutation Source # |
Instance details Defined in Agda.Utils.Permutation Methods rnf :: Permutation -> () Source #
Generic Permutation Source # |

Instance details

Defined in Agda.Utils.Permutation

Associated Types

type Rep Permutation |

Instance details

Defined in Agda.Utils.Permutation

type Rep Permutation = D1 ('MetaData "Permutation" "Agda.Utils.Permutation" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "Perm" 'PrefixI 'True) (S1 ('MetaSel ('Just "permRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Just "permPicks") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Int])))

Methods

from :: Permutation -> Rep Permutation x Source #

to :: Rep Permutation x -> Permutation Source #

Show Permutation Source # |
Instance details Defined in Agda.Utils.Permutation Methods showsPrec :: Int -> Permutation -> ShowS Source # show :: Permutation -> String Source # showList :: [Permutation] -> ShowS Source #
Eq Permutation Source # |
Instance details Defined in Agda.Utils.Permutation Methods (==) :: Permutation -> Permutation -> Bool Source # (/=) :: Permutation -> Permutation -> Bool Source #
type Rep Permutation Source # |

Instance details

Defined in Agda.Utils.Permutation

type Rep Permutation = D1 ('MetaData "Permutation" "Agda.Utils.Permutation" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "Perm" 'PrefixI 'True) (S1 ('MetaSel ('Just "permRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Just "permPicks") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [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`

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`

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

Instances details

InversePermute [Maybe a] (IntMap a) Source # |
Instance details Defined in Agda.Utils.Permutation Methods inversePermute :: Permutation -> [Maybe a] -> IntMap a Source #
InversePermute [Maybe a] [Maybe a] Source # |
Instance details Defined in Agda.Utils.Permutation Methods inversePermute :: Permutation -> [Maybe a] -> [Maybe a] Source #
InversePermute [Maybe a] [(Int, a)] Source # |
Instance details Defined in Agda.Utils.Permutation Methods inversePermute :: Permutation -> [Maybe a] -> [(Int, a)] Source #
InversePermute (Int -> a) [Maybe a] Source # |
Instance details Defined in Agda.Utils.Permutation Methods 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 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.

topoSortM :: Monad m => (a -> a -> m Bool) -> [a] -> m (Maybe Permutation) Source #

# Drop (apply) and undrop (abstract)

data Drop a Source #

Delayed dropping which allows undropping.

Constructors

Drop |

Fields

- dropN :: Int

  Non-negative number of things to drop.

- dropFrom :: a

  Where to drop from.

#### Instances

Instances details

Functor Drop Source # |
Instance details Defined in Agda.Utils.Permutation Methods fmap :: (a -> b) -> Drop a -> Drop b Source # (<$) :: a -> Drop b -> Drop a Source #
Foldable Drop Source # |

Instance details

Defined in Agda.Utils.Permutation

Methods

fold :: Monoid m => Drop m -> m Source #

foldMap :: Monoid m => (a -> m) -> Drop a -> m Source #

foldMap' :: Monoid m => (a -> m) -> Drop a -> m Source #

foldr :: (a -> b -> b) -> b -> Drop a -> b Source #

foldr' :: (a -> b -> b) -> b -> Drop a -> b Source #

foldl :: (b -> a -> b) -> b -> Drop a -> b Source #

foldl' :: (b -> a -> b) -> b -> Drop a -> b Source #

foldr1 :: (a -> a -> a) -> Drop a -> a Source #

foldl1 :: (a -> a -> a) -> Drop a -> a Source #

toList :: Drop a -> [a] Source #

null :: Drop a -> Bool Source #

length :: Drop a -> Int Source #

elem :: Eq a => a -> Drop a -> Bool Source #

maximum :: Ord a => Drop a -> a Source #

minimum :: Ord a => Drop a -> a Source #

sum :: Num a => Drop a -> a Source #

product :: Num a => Drop a -> a Source #

Traversable Drop Source # |
Instance details Defined in Agda.Utils.Permutation Methods traverse :: Applicative f => (a -> f b) -> Drop a -> f (Drop b) Source # sequenceA :: Applicative f => Drop (f a) -> f (Drop a) Source # mapM :: Monad m => (a -> m b) -> Drop a -> m (Drop b) Source # sequence :: Monad m => Drop (m a) -> m (Drop a) Source #
KillRange a => KillRange (Drop a) Source # |
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (Drop a) Source #
EmbPrj a => EmbPrj (Drop a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Drop a -> S Word32 Source # icod_ :: Drop a -> S Word32 Source # value :: Word32 -> R (Drop a) Source #
DoDrop a => Abstract (Drop a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Drop a -> Drop a Source #
DoDrop a => Apply (Drop a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Drop a -> Args -> Drop a Source # applyE :: Drop a -> Elims -> Drop a Source #
Show a => Show (Drop a) Source # |
Instance details Defined in Agda.Utils.Permutation Methods showsPrec :: Int -> Drop a -> ShowS Source # show :: Drop a -> String Source # showList :: [Drop a] -> ShowS Source #
Eq a => Eq (Drop a) Source # |
Instance details Defined in Agda.Utils.Permutation Methods (==) :: Drop a -> Drop a -> Bool Source # (/=) :: Drop a -> Drop a -> Bool Source #
Ord a => Ord (Drop a) Source # |
Instance details Defined in Agda.Utils.Permutation Methods compare :: Drop a -> Drop a -> Ordering Source # (<) :: Drop a -> Drop a -> Bool Source # (<=) :: Drop a -> Drop a -> Bool Source # (>) :: Drop a -> Drop a -> Bool Source # (>=) :: Drop a -> Drop a -> Bool Source # max :: Drop a -> Drop a -> Drop a Source # min :: Drop a -> Drop a -> Drop a Source #

class DoDrop a where Source #

Things that support delayed dropping.

Minimal complete definition

doDrop

Methods

doDrop Source #

Arguments

:: Drop a |
-> a | Perform the dropping.

dropMore Source #

Arguments

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

unDrop Source #

Arguments

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

#### Instances

Instances details

DoDrop Permutation Source # |
Instance details Defined in Agda.Utils.Permutation Methods doDrop :: Drop Permutation -> Permutation Source # dropMore :: Int -> Drop Permutation -> Drop Permutation Source # unDrop :: Int -> Drop Permutation -> Drop Permutation Source #
DoDrop [a] Source # |
Instance details Defined in Agda.Utils.Permutation Methods doDrop :: Drop [a] -> [a] Source # dropMore :: Int -> Drop [a] -> Drop [a] Source # unDrop :: Int -> Drop [a] -> Drop [a] Source #