Agda-2.6.4.2: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Utils.Permutation

Synopsis

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

Instances

Instances details
KillRange Permutation Source # 
Instance details

Defined in Agda.Syntax.Position

DropArgs Permutation Source # 
Instance details

Defined in Agda.TypeChecking.DropArgs

PrettyTCM Permutation Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

EmbPrj Permutation Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Abstract Permutation Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply Permutation Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Null Permutation Source # 
Instance details

Defined in Agda.Utils.Permutation

DoDrop Permutation Source # 
Instance details

Defined in Agda.Utils.Permutation

Sized Permutation Source # 
Instance details

Defined in Agda.Utils.Permutation

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.6.4.2-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])))
Show Permutation Source # 
Instance details

Defined in Agda.Utils.Permutation

NFData Permutation Source # 
Instance details

Defined in Agda.Utils.Permutation

Methods

rnf :: Permutation -> () #

Eq Permutation Source # 
Instance details

Defined in Agda.Utils.Permutation

type Rep Permutation Source # 
Instance details

Defined in Agda.Utils.Permutation

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

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
Foldable Drop Source # 
Instance details

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 Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.Utils.Permutation

Methods

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

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

KillRange a => KillRange (Drop a) Source # 
Instance details

Defined in Agda.Syntax.Position

EmbPrj a => EmbPrj (Drop a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Drop a -> S Int32 Source #

icod_ :: Drop a -> S Int32 Source #

value :: Int32 -> 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 #

show :: Drop a -> String #

showList :: [Drop a] -> ShowS #

Eq a => Eq (Drop a) Source # 
Instance details

Defined in Agda.Utils.Permutation

Methods

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

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

Ord a => Ord (Drop a) Source # 
Instance details

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

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 #