Agda-2.6.0: 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]
Instances
 Source # Instance detailsDefined in Agda.Utils.Permutation Methods Source # Instance detailsDefined in Agda.Utils.Permutation Methodsgfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Permutation -> c Permutation #gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Permutation #dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Permutation) #dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Permutation) #gmapT :: (forall b. Data b => b -> b) -> Permutation -> Permutation #gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Permutation -> r #gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Permutation -> r #gmapQ :: (forall d. Data d => d -> u) -> Permutation -> [u] #gmapQi :: Int -> (forall d. Data d => d -> u) -> Permutation -> u #gmapM :: Monad m => (forall d. Data d => d -> m d) -> Permutation -> m Permutation #gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Permutation -> m Permutation #gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Permutation -> m Permutation # Source # Instance detailsDefined in Agda.Utils.Permutation MethodsshowList :: [Permutation] -> ShowS # Source # Instance detailsDefined in Agda.Utils.Permutation Methods Source # Instance detailsDefined in Agda.Utils.Permutation Methods Source # Instance detailsDefined in Agda.Utils.Permutation Methods Source # Instance detailsDefined in Agda.Utils.Permutation Methods Source # Instance detailsDefined in Agda.TypeChecking.Substitute Methods Source # Instance detailsDefined in Agda.TypeChecking.Substitute Methods Source # Instance details Methods Source # Instance detailsDefined in Agda.TypeChecking.Pretty Methods Source # Instance detailsDefined in Agda.TypeChecking.DropArgs Methods

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 # Instance detailsDefined in Agda.Utils.Permutation MethodsinversePermute :: Permutation -> [Maybe a] -> [Maybe a] Source # InversePermute [Maybe a] (IntMap a) Source # Instance detailsDefined in Agda.Utils.Permutation MethodsinversePermute :: Permutation -> [Maybe a] -> IntMap a Source # InversePermute [Maybe a] [(Int, a)] Source # Instance detailsDefined in Agda.Utils.Permutation MethodsinversePermute :: Permutation -> [Maybe a] -> [(Int, a)] Source # InversePermute (Int -> a) [Maybe a] Source # Instance detailsDefined in Agda.Utils.Permutation MethodsinversePermute :: Permutation -> (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 # Instance detailsDefined in Agda.Utils.Permutation Methodsfmap :: (a -> b) -> Drop a -> Drop b #(<\$) :: a -> Drop b -> Drop a # Source # Instance detailsDefined in Agda.Utils.Permutation Methodsfold :: 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 #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 # Source # Instance detailsDefined in Agda.Utils.Permutation Methodstraverse :: 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) # Eq a => Eq (Drop a) Source # Instance detailsDefined in Agda.Utils.Permutation Methods(==) :: Drop a -> Drop a -> Bool #(/=) :: Drop a -> Drop a -> Bool # Data a => Data (Drop a) Source # Instance detailsDefined in Agda.Utils.Permutation Methodsgfoldl :: (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 # Instance detailsDefined in Agda.Utils.Permutation Methodscompare :: 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 # Show a => Show (Drop a) Source # Instance detailsDefined in Agda.Utils.Permutation MethodsshowsPrec :: Int -> Drop a -> ShowS #show :: Drop a -> String #showList :: [Drop a] -> ShowS # KillRange a => KillRange (Drop a) Source # Instance detailsDefined in Agda.Utils.Permutation Methods DoDrop a => Abstract (Drop a) Source # Instance detailsDefined in Agda.TypeChecking.Substitute Methodsabstract :: Telescope -> Drop a -> Drop a Source # DoDrop a => Apply (Drop a) Source # Instance detailsDefined in Agda.TypeChecking.Substitute Methodsapply :: Drop a -> Args -> Drop a Source #applyE :: Drop a -> Elims -> Drop a Source # EmbPrj a => EmbPrj (Drop a) Source # Instance details Methodsicode :: Drop a -> S Int32 Source #icod_ :: Drop a -> S Int32 Source #value :: Int32 -> R (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 # Instance detailsDefined in Agda.Utils.Permutation Methods DoDrop [a] Source # Instance detailsDefined in Agda.Utils.Permutation MethodsdoDrop :: Drop [a] -> [a] Source #dropMore :: Int -> Drop [a] -> Drop [a] Source #unDrop :: Int -> Drop [a] -> Drop [a] Source #