Agda.Utils.Permutation

Documentation

data Permutation

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

KillRange Permutation

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT Permutation

DropArgs Permutation

Defined in Agda.TypeChecking.DropArgs

Methods

dropArgs :: Int -> Permutation -> Permutation

PrettyTCM Permutation

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Permutation -> m Doc

EmbPrj Permutation

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Permutation -> S Int32

icod_ :: Permutation -> S Int32

value :: Int32 -> R Permutation

Abstract Permutation

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Permutation -> Permutation

Apply Permutation

Defined in Agda.TypeChecking.Substitute

Methods

apply :: Permutation -> Args -> Permutation

applyE :: Permutation -> Elims -> Permutation

Null Permutation

Defined in Agda.Utils.Permutation

Methods

empty :: Permutation

null :: Permutation -> Bool

DoDrop Permutation

Defined in Agda.Utils.Permutation

Methods

doDrop :: Drop Permutation -> Permutation

dropMore :: Int -> Drop Permutation -> Drop Permutation

unDrop :: Int -> Drop Permutation -> Drop Permutation

Sized Permutation

Defined in Agda.Utils.Permutation

Methods

size :: Permutation -> Int

Generic Permutation

Defined in Agda.Utils.Permutation

Associated Types

type Rep Permutation :: Type -> Type

Methods

from :: Permutation -> Rep Permutation x

to :: Rep Permutation x -> Permutation

Show Permutation

Defined in Agda.Utils.Permutation

Methods

showsPrec :: Int -> Permutation -> ShowS

show :: Permutation -> String

showList :: [Permutation] -> ShowS

NFData Permutation

Defined in Agda.Utils.Permutation

Methods

rnf :: Permutation -> ()

Eq Permutation

Defined in Agda.Utils.Permutation

Methods

(==) :: Permutation -> Permutation -> Bool

(/=) :: Permutation -> Permutation -> Bool

type Rep Permutation

Defined in Agda.Utils.Permutation

type Rep Permutation = D1 ('MetaData "Permutation" "Agda.Utils.Permutation" "Agda-2.6.2.2.20221106-inplace" '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]

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

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

Instances

InversePermute [Maybe a] (IntMap a)

Defined in Agda.Utils.Permutation

Methods

inversePermute :: Permutation -> [Maybe a] -> IntMap a

InversePermute [Maybe a] [Maybe a]

Defined in Agda.Utils.Permutation

Methods

inversePermute :: Permutation -> [Maybe a] -> [Maybe a]

InversePermute [Maybe a] [(Int, a)]

Defined in Agda.Utils.Permutation

Methods

inversePermute :: Permutation -> [Maybe a] -> [(Int, a)]

InversePermute (Int -> a) [Maybe a]

Defined in Agda.Utils.Permutation

Methods

inversePermute :: Permutation -> (Int -> a) -> [Maybe a]

idP :: Int -> Permutation

Identity permutation.

takeP :: Int -> Permutation -> Permutation

Restrict a permutation to work on n elements, discarding picks >=n.

droppedP :: Permutation -> Permutation

Pick the elements that are not picked by the permutation.

liftP :: Int -> Permutation -> 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.

composeP :: Permutation -> Permutation -> Permutation

permute (compose p1 p2) == permute p1 . permute p2

invertP :: Int -> Permutation -> Permutation

invertP err p is the inverse of p where defined, otherwise defaults to err. composeP p (invertP err p) == p

compactP :: Permutation -> Permutation

Turn a possible non-surjective permutation into a surjective permutation.

reverseP :: Permutation -> 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.

flipP :: Permutation -> Permutation

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

expandP i n π in the domain of π replace the ith element by n elements.

topoSort :: (a -> a -> Bool) -> [a] -> Maybe Permutation

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)

Drop (apply) and undrop (abstract)

data Drop a

Delayed dropping which allows undropping.

Constructors

Drop

Fields

• dropN :: Int

  Non-negative number of things to drop.

• dropFrom :: a

  Where to drop from.

Instances

Foldable Drop

Defined in Agda.Utils.Permutation

Methods

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

foldMap :: Monoid m => (a -> m) -> Drop a -> 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

toList :: Drop a -> [a]

null :: Drop a -> Bool

length :: Drop a -> Int

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

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

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

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

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

Traversable Drop

Defined in Agda.Utils.Permutation

Methods

traverse :: Applicative f => (a -> f b) -> Drop a -> f (Drop b)

sequenceA :: Applicative f => Drop (f a) -> f (Drop a)

mapM :: Monad m => (a -> m b) -> Drop a -> m (Drop b)

sequence :: Monad m => Drop (m a) -> m (Drop a)

Functor Drop

Defined in Agda.Utils.Permutation

Methods

fmap :: (a -> b) -> Drop a -> Drop b

(<$) :: a -> Drop b -> Drop a

KillRange a => KillRange (Drop a)

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (Drop a)

EmbPrj a => EmbPrj (Drop a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Drop a -> S Int32

icod_ :: Drop a -> S Int32

value :: Int32 -> R (Drop a)

DoDrop a => Abstract (Drop a)

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Drop a -> Drop a

DoDrop a => Apply (Drop a)

Defined in Agda.TypeChecking.Substitute

Methods

apply :: Drop a -> Args -> Drop a

applyE :: Drop a -> Elims -> Drop a

Show a => Show (Drop a)

Defined in Agda.Utils.Permutation

Methods

showsPrec :: Int -> Drop a -> ShowS

show :: Drop a -> String

showList :: [Drop a] -> ShowS

Eq a => Eq (Drop a)

Defined in Agda.Utils.Permutation

Methods

(==) :: Drop a -> Drop a -> Bool

(/=) :: Drop a -> Drop a -> Bool

Ord a => Ord (Drop a)

Defined in Agda.Utils.Permutation

Methods

compare :: Drop a -> Drop a -> Ordering

(<) :: Drop a -> Drop a -> Bool

(<=) :: Drop a -> Drop a -> Bool

(>) :: Drop a -> Drop a -> Bool

(>=) :: Drop a -> Drop a -> Bool

max :: Drop a -> Drop a -> Drop a

min :: Drop a -> Drop a -> Drop a

class DoDrop a where

Things that support delayed dropping.

Minimal complete definition

doDrop

Methods

doDrop

Arguments

:: Drop a

-> a

Perform the dropping.

dropMore

Arguments

:: Int

-> Drop a

-> Drop a

Drop more.

unDrop

Arguments

:: Int

-> Drop a

-> Drop a

Pick up dropped stuff.

Instances

DoDrop Permutation

Defined in Agda.Utils.Permutation

Methods

doDrop :: Drop Permutation -> Permutation

dropMore :: Int -> Drop Permutation -> Drop Permutation

unDrop :: Int -> Drop Permutation -> Drop Permutation

DoDrop [a]

Defined in Agda.Utils.Permutation

Methods

doDrop :: Drop [a] -> [a]

dropMore :: Int -> Drop [a] -> Drop [a]

unDrop :: Int -> Drop [a] -> Drop [a]