Safe Haskell	None
Language	Haskell2010

Data.Array.Nested.Permutation

Contents

Permutations
- Applying permutations
Operations on permutations
Lemmas

Synopsis

data Perm (list :: [Nat]) where
- PNil :: Perm ('[] :: [Nat])
- PCons :: forall (a :: Nat) (l :: [Nat]). SNat a -> Perm l -> Perm (a ': l)
permRank :: forall (list :: [Nat]). Perm list -> SNat (Rank list)
permFromList :: [Int] -> (forall (list :: [Nat]). Perm list -> r) -> r
permToList :: forall (list :: [Nat]). Perm list -> [Natural]
permToList' :: forall (list :: [Nat]). Perm list -> [Int]
permCheckPermutation :: forall r (list :: [Nat]). Perm list -> (IsPermutation list => r) -> Maybe r
class KnownPerm (l :: [Nat]) where
- makePerm :: Perm l
withKnownPerm :: forall (l :: [Nat]) r. Perm l -> (KnownPerm l => r) -> r
type PermR = [Int]
type family Elem (x :: a) (l :: [a]) :: Bool where ...
type family AllElem' (as :: [a]) (bs :: [a]) :: Bool where ...
type AllElem (as :: [a]) (bs :: [a]) = Assert (AllElem' as bs) (TypeError ((('Text "The elements of " ':<>: 'ShowType as) ':<>: 'Text " are not all in ") ':<>: 'ShowType bs) :: Constraint)
type family Count (i :: Natural) (n :: Natural) :: [Natural] where ...
type IsPermutation (as :: [Natural]) = (AllElem as (Count 0 (Rank as)), AllElem (Count 0 (Rank as)) as)
type family Index (i :: Natural) (sh :: [k]) :: k where ...
type family Permute (is :: [Natural]) (sh :: [a]) :: [a] where ...
type PermutePrefix (is :: [Natural]) (sh :: [a]) = Permute is (TakeLen is sh) ++ DropLen is sh
type family TakeLen (ref :: [a1]) (l :: [a]) :: [a] where ...
type family DropLen (ref :: [a1]) (l :: [a]) :: [a] where ...
listxTakeLen :: forall (f :: Maybe Nat -> Type) (is :: [Nat]) (sh :: [Maybe Nat]). Perm is -> ListX sh f -> ListX (TakeLen is sh) f
listxDropLen :: forall (f :: Maybe Nat -> Type) (is :: [Nat]) (sh :: [Maybe Nat]). Perm is -> ListX sh f -> ListX (DropLen is sh) f
listxPermute :: forall (f :: Maybe Nat -> Type) (is :: [Nat]) (sh :: [Maybe Nat]). Perm is -> ListX sh f -> ListX (Permute is sh) f
listxIndex :: forall {k1} {k2} f (is :: k1) (shT :: k2) (i :: Nat) (sh :: [Maybe Nat]). Proxy is -> Proxy shT -> SNat i -> ListX sh f -> f (Index i sh)
listxPermutePrefix :: forall (f :: Maybe Nat -> Type) (is :: [Nat]) (sh :: [Maybe Nat]). Perm is -> ListX sh f -> ListX (PermutePrefix is sh) f
ixxPermutePrefix :: forall i (is :: [Nat]) (sh :: [Maybe Nat]). Perm is -> IxX sh i -> IxX (PermutePrefix is sh) i
ssxTakeLen :: forall (is :: [Nat]) (sh :: [Maybe Nat]). Perm is -> StaticShX sh -> StaticShX (TakeLen is sh)
ssxDropLen :: forall (is :: [Nat]) (sh :: [Maybe Nat]). Perm is -> StaticShX sh -> StaticShX (DropLen is sh)
ssxPermute :: forall (is :: [Nat]) (sh :: [Maybe Nat]). Perm is -> StaticShX sh -> StaticShX (Permute is sh)
ssxIndex :: forall {k1} {k2} (is :: k1) (shT :: k2) (i :: Nat) (sh :: [Maybe Nat]). Proxy is -> Proxy shT -> SNat i -> StaticShX sh -> SMayNat () SNat (Index i sh)
ssxPermutePrefix :: forall (is :: [Nat]) (sh :: [Maybe Nat]). Perm is -> StaticShX sh -> StaticShX (PermutePrefix is sh)
shxPermutePrefix :: forall (is :: [Nat]) (sh :: [Maybe Nat]). Perm is -> IShX sh -> IShX (PermutePrefix is sh)
permInverse :: forall (is :: [Nat]) r. Perm is -> (forall (is' :: [Natural]). IsPermutation is' => Perm is' -> (forall (sh :: [Maybe Nat]). Rank sh ~ Rank is => StaticShX sh -> Permute is' (Permute is sh) :~: sh) -> r) -> r
type family MapSucc (is :: [Natural]) :: [Natural] where ...
permShift1 :: forall (l :: [Nat]). Perm l -> Perm (0 ': MapSucc l)
lemRankPermute :: forall {a} (sh :: [a]) (is :: [Nat]). Proxy sh -> Perm is -> Rank (Permute is sh) :~: Rank is
lemRankDropLen :: forall (is :: [Nat]) (sh :: [Maybe Nat]). Rank is <= Rank sh => StaticShX sh -> Perm is -> Rank (DropLen is sh) :~: (Rank sh - Rank is)
lemIndexSucc :: forall {k} (i :: Natural) (a :: k) (l :: [k]). Proxy i -> Proxy a -> Proxy l -> Index (i + 1) (a ': l) :~: Index i l

Permutations

data Perm (list :: [Nat]) where Source #

A "backward" permutation of a dimension list. The operation on the dimension list is most similar to backpermute; see Permute for code that implements this.

Constructors

PNil :: Perm ('[] :: [Nat])
PCons :: forall (a :: Nat) (l :: [Nat]). SNat a -> Perm l -> Perm (a ': l) infixr 5

Instances

Instances details

Show (Perm list) Source #
Instance details Defined in Data.Array.Nested.Permutation Methods showsPrec :: Int -> Perm list -> ShowS # show :: Perm list -> String # showList :: [Perm list] -> ShowS #
Eq (Perm list) Source #
Instance details Defined in Data.Array.Nested.Permutation Methods (==) :: Perm list -> Perm list -> Bool # (/=) :: Perm list -> Perm list -> Bool #
TestEquality Perm Source #
Instance details Defined in Data.Array.Nested.Permutation Methods testEquality :: forall (a :: [Nat]) (b :: [Nat]). Perm a -> Perm b -> Maybe (a :~: b) #

permRank :: forall (list :: [Nat]). Perm list -> SNat (Rank list) Source #

permFromList :: [Int] -> (forall (list :: [Nat]). Perm list -> r) -> r Source #

permToList :: forall (list :: [Nat]). Perm list -> [Natural] Source #

permToList' :: forall (list :: [Nat]). Perm list -> [Int] Source #

permCheckPermutation :: forall r (list :: [Nat]). Perm list -> (IsPermutation list => r) -> Maybe r Source #

When called as permCheckPermutation p k, if p is a permutation of [0 .. length (permToList p) - 1], Just k is returned. If it isn't, then Nothing is returned.

class KnownPerm (l :: [Nat]) where Source #

Utility class for generating permutations from type class information.

Methods

makePerm :: Perm l Source #

Instances

Instances details

KnownPerm ('[] :: [Nat]) Source #
Instance details Defined in Data.Array.Nested.Permutation Methods makePerm :: Perm ('[] :: [Nat]) Source #
(KnownNat n, KnownPerm l) => KnownPerm (n ': l) Source #
Instance details Defined in Data.Array.Nested.Permutation Methods makePerm :: Perm (n ': l) Source #

withKnownPerm :: forall (l :: [Nat]) r. Perm l -> (KnownPerm l => r) -> r Source #

type PermR = [Int] Source #

Untyped permutations for ranked arrays

Applying permutations

type family Elem (x :: a) (l :: [a]) :: Bool where ... Source #

Equations

Elem (x :: a) ('[] :: [a]) = 'False
Elem (x :: a) (x ': _1 :: [a]) = 'True
Elem (x :: a) (_1 ': ys :: [a]) = Elem x ys

type family AllElem' (as :: [a]) (bs :: [a]) :: Bool where ... Source #

Equations

AllElem' ('[] :: [a]) (bs :: [a]) = 'True
AllElem' (a2 ': as :: [a1]) (bs :: [a1]) = Elem a2 bs && AllElem' as bs

type AllElem (as :: [a]) (bs :: [a]) = Assert (AllElem' as bs) (TypeError ((('Text "The elements of " ':<>: 'ShowType as) ':<>: 'Text " are not all in ") ':<>: 'ShowType bs) :: Constraint) Source #

type family Count (i :: Natural) (n :: Natural) :: [Natural] where ... Source #

Equations

Count n n = '[] :: [Natural]
Count i n = i ': Count (i + 1) n

type IsPermutation (as :: [Natural]) = (AllElem as (Count 0 (Rank as)), AllElem (Count 0 (Rank as)) as) Source #

type family Index (i :: Natural) (sh :: [k]) :: k where ... Source #

Equations

Index 0 (n ': sh :: [k]) = n
Index i (_1 ': sh :: [k]) = Index (i - 1) sh

type family Permute (is :: [Natural]) (sh :: [a]) :: [a] where ... Source #

Equations

Permute ('[] :: [Natural]) (sh :: [a]) = '[] :: [a]
Permute (i ': is) (sh :: [a]) = Index i sh ': Permute is sh

type PermutePrefix (is :: [Natural]) (sh :: [a]) = Permute is (TakeLen is sh) ++ DropLen is sh Source #

type family TakeLen (ref :: [a1]) (l :: [a]) :: [a] where ... Source #

Equations

TakeLen ('[] :: [a2]) (l :: [a1]) = '[] :: [a1]
TakeLen (_1 ': ref :: [a1]) (x ': xs :: [a2]) = x ': TakeLen ref xs

type family DropLen (ref :: [a1]) (l :: [a]) :: [a] where ... Source #

Equations

DropLen ('[] :: [a2]) (l :: [a1]) = l
DropLen (_1 ': ref :: [a1]) (_2 ': xs :: [a2]) = DropLen ref xs

listxTakeLen :: forall (f :: Maybe Nat -> Type) (is :: [Nat]) (sh :: [Maybe Nat]). Perm is -> ListX sh f -> ListX (TakeLen is sh) f Source #

listxDropLen :: forall (f :: Maybe Nat -> Type) (is :: [Nat]) (sh :: [Maybe Nat]). Perm is -> ListX sh f -> ListX (DropLen is sh) f Source #

listxPermute :: forall (f :: Maybe Nat -> Type) (is :: [Nat]) (sh :: [Maybe Nat]). Perm is -> ListX sh f -> ListX (Permute is sh) f Source #

listxIndex :: forall {k1} {k2} f (is :: k1) (shT :: k2) (i :: Nat) (sh :: [Maybe Nat]). Proxy is -> Proxy shT -> SNat i -> ListX sh f -> f (Index i sh) Source #

listxPermutePrefix :: forall (f :: Maybe Nat -> Type) (is :: [Nat]) (sh :: [Maybe Nat]). Perm is -> ListX sh f -> ListX (PermutePrefix is sh) f Source #

ixxPermutePrefix :: forall i (is :: [Nat]) (sh :: [Maybe Nat]). Perm is -> IxX sh i -> IxX (PermutePrefix is sh) i Source #

ssxTakeLen :: forall (is :: [Nat]) (sh :: [Maybe Nat]). Perm is -> StaticShX sh -> StaticShX (TakeLen is sh) Source #

ssxDropLen :: forall (is :: [Nat]) (sh :: [Maybe Nat]). Perm is -> StaticShX sh -> StaticShX (DropLen is sh) Source #

ssxPermute :: forall (is :: [Nat]) (sh :: [Maybe Nat]). Perm is -> StaticShX sh -> StaticShX (Permute is sh) Source #

ssxIndex :: forall {k1} {k2} (is :: k1) (shT :: k2) (i :: Nat) (sh :: [Maybe Nat]). Proxy is -> Proxy shT -> SNat i -> StaticShX sh -> SMayNat () SNat (Index i sh) Source #

ssxPermutePrefix :: forall (is :: [Nat]) (sh :: [Maybe Nat]). Perm is -> StaticShX sh -> StaticShX (PermutePrefix is sh) Source #

shxPermutePrefix :: forall (is :: [Nat]) (sh :: [Maybe Nat]). Perm is -> IShX sh -> IShX (PermutePrefix is sh) Source #

Operations on permutations

permInverse :: forall (is :: [Nat]) r. Perm is -> (forall (is' :: [Natural]). IsPermutation is' => Perm is' -> (forall (sh :: [Maybe Nat]). Rank sh ~ Rank is => StaticShX sh -> Permute is' (Permute is sh) :~: sh) -> r) -> r Source #

type family MapSucc (is :: [Natural]) :: [Natural] where ... Source #

Equations

MapSucc ('[] :: [Natural]) = '[] :: [Natural]
MapSucc (i ': is) = (i + 1) ': MapSucc is

permShift1 :: forall (l :: [Nat]). Perm l -> Perm (0 ': MapSucc l) Source #

Lemmas

lemRankPermute :: forall {a} (sh :: [a]) (is :: [Nat]). Proxy sh -> Perm is -> Rank (Permute is sh) :~: Rank is Source #

lemRankDropLen :: forall (is :: [Nat]) (sh :: [Maybe Nat]). Rank is <= Rank sh => StaticShX sh -> Perm is -> Rank (DropLen is sh) :~: (Rank sh - Rank is) Source #

lemIndexSucc :: forall {k} (i :: Natural) (a :: k) (l :: [k]). Proxy i -> Proxy a -> Proxy l -> Index (i + 1) (a ': l) :~: Index i l Source #