{-# LANGUAGE TypeApplications #-}

-- | See 'Permutation'
module Data.Fin.Permutation (Permutation, apply, unapply, swap, orbit, cycles) where

import Prelude (Functor (..), Applicative (..), Eq (..), Show (..), Bool (..), ($), (<$>), otherwise, snd, flip, curry, uncurry)
import Algebra
import Control.Category (Category (..))
import Data.Fin
import Data.Fin.List hiding (swap)
import qualified Data.Fin.List as L
import Data.Foldable (elem, minimum, toList)
import Data.Functor.Compose (Compose (..))
import Data.List.NonEmpty (NonEmpty (..))
import Data.Natural.Class (Natural (..))
import qualified Data.Peano as P
import Data.Universe.Class

-- | Permutation of @n@ elements
--
-- Any permutation can be expressed as a product of transpositions. Ergo, construct with 'Semigroup' operations and `swap`.
data Permutation n where
    PZ :: Permutation P.Zero
    PS :: Fin (P.Succ n) -> Permutation n -> Permutation (P.Succ n)

deriving instance Eq (Permutation n)
deriving instance Show (Permutation n)

instance Natural n => Universe (Permutation n) where
    universe :: [Permutation n]
universe = Compose [] Permutation n -> [Permutation n]
forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (Compose [] Permutation n -> [Permutation n])
-> Compose [] Permutation n -> [Permutation n]
forall a b. (a -> b) -> a -> b
$ Compose [] Permutation 'Zero
-> (forall (m :: Peano).
    Natural m =>
    Compose [] Permutation ('Succ m))
-> Compose [] Permutation n
forall (n :: Peano) (f :: Peano -> *).
Natural n =>
f 'Zero -> (forall (m :: Peano). Natural m => f ('Succ m)) -> f n
natural ([Permutation 'Zero] -> Compose [] Permutation 'Zero
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose [Permutation 'Zero
PZ]) ([Permutation ('Succ m)] -> Compose [] Permutation ('Succ m)
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose ([Permutation ('Succ m)] -> Compose [] Permutation ('Succ m))
-> [Permutation ('Succ m)] -> Compose [] Permutation ('Succ m)
forall a b. (a -> b) -> a -> b
$ Fin ('Succ m) -> Permutation m -> Permutation ('Succ m)
forall (n :: Peano).
Fin ('Succ n) -> Permutation n -> Permutation ('Succ n)
PS (Fin ('Succ m) -> Permutation m -> Permutation ('Succ m))
-> [Fin ('Succ m)] -> [Permutation m -> Permutation ('Succ m)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> List ('Succ m) (Fin ('Succ m)) -> [Fin ('Succ m)]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList List ('Succ m) (Fin ('Succ m))
forall (n :: Peano). Natural n => List n (Fin n)
enum [Permutation m -> Permutation ('Succ m)]
-> [Permutation m] -> [Permutation ('Succ m)]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Permutation m]
forall a. Universe a => [a]
universe)

instance Natural n => Finite (Permutation n)

apply :: Permutation n -> List n a -> List n a
apply :: Permutation n -> List n a -> List n a
apply PZ Nil = List n a
forall a. List 'Zero a
Nil
apply (PS Zero p :: Permutation n
p) (a :: a
a:.as :: List n a
as) = a
aa -> List n a -> List ('Succ n) a
forall a (n :: Peano). a -> List n a -> List ('Succ n) a
:.Permutation n -> List n a -> List n a
forall (n :: Peano) a. Permutation n -> List n a -> List n a
apply Permutation n
p List n a
List n a
as
apply (PS (Succ n :: Fin n
n) p :: Permutation n
p) (a :: a
a:.as :: List n a
as) = (a -> List n a -> List ('Succ n) a)
-> (a, List n a) -> List ('Succ n) a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> List n a -> List ('Succ n) a
forall a (n :: Peano). a -> List n a -> List ('Succ n) a
(:.) ((a, List n a) -> List n a) -> (a, List n a) -> List n a
forall a b. (a -> b) -> a -> b
$ Fin n -> (a -> (a, a)) -> List n a -> (a, List n a)
forall (f :: * -> *) (n :: Peano) a.
Functor f =>
Fin n -> (a -> f a) -> List n a -> f (List n a)
at Fin n
n ((a -> a -> (a, a)) -> a -> a -> (a, a)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (,) a
a) (Permutation n -> List n a -> List n a
forall (n :: Peano) a. Permutation n -> List n a -> List n a
apply Permutation n
p List n a
List n a
as)

unapply :: Permutation n -> List n a -> List n a
unapply :: Permutation n -> List n a -> List n a
unapply PZ Nil = List n a
forall a. List 'Zero a
Nil
unapply (PS Zero p :: Permutation n
p) (a :: a
a:.as :: List n a
as) = a
aa -> List n a -> List ('Succ n) a
forall a (n :: Peano). a -> List n a -> List ('Succ n) a
:.Permutation n -> List n a -> List n a
forall (n :: Peano) a. Permutation n -> List n a -> List n a
unapply Permutation n
p List n a
List n a
as
unapply (PS (Succ n :: Fin n
n) p :: Permutation n
p) (a :: a
a:.as :: List n a
as) = Permutation ('Succ n) -> List ('Succ n) a -> List ('Succ n) a
forall (n :: Peano) a. Permutation n -> List n a -> List n a
unapply (Fin ('Succ n) -> Permutation n -> Permutation ('Succ n)
forall (n :: Peano).
Fin ('Succ n) -> Permutation n -> Permutation ('Succ n)
PS Fin ('Succ n)
forall (n :: Peano). Fin ('Succ n)
Zero Permutation n
p) (List ('Succ n) a -> List ('Succ n) a)
-> ((a, List n a) -> List ('Succ n) a)
-> (a, List n a)
-> List ('Succ n) a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (a -> List n a -> List ('Succ n) a)
-> (a, List n a) -> List ('Succ n) a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> List n a -> List ('Succ n) a
forall a (n :: Peano). a -> List n a -> List ('Succ n) a
(:.) ((a, List n a) -> List n a) -> (a, List n a) -> List n a
forall a b. (a -> b) -> a -> b
$ Fin n -> (a -> (a, a)) -> List n a -> (a, List n a)
forall (f :: * -> *) (n :: Peano) a.
Functor f =>
Fin n -> (a -> f a) -> List n a -> f (List n a)
at Fin n
n ((a -> a -> (a, a)) -> a -> a -> (a, a)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (,) a
a) List n a
List n a
as

instance Natural n => Semigroup (Permutation n) where
    <> :: Permutation n -> Permutation n -> Permutation n
(<>) = Op₂ Permutation Permutation n
-> Permutation n -> Permutation n -> Permutation n
forall k (a :: k -> *) (b :: k -> *) (n :: k).
Op₂ a b n -> a n -> a n -> b n
unOp₂ (Op₂ Permutation Permutation n
 -> Permutation n -> Permutation n -> Permutation n)
-> Op₂ Permutation Permutation n
-> Permutation n
-> Permutation n
-> Permutation n
forall a b. (a -> b) -> a -> b
$ Op₂ Permutation Permutation 'Zero
-> (forall (m :: Peano).
    Natural m =>
    Op₂ Permutation Permutation ('Succ m))
-> Op₂ Permutation Permutation n
forall (n :: Peano) (f :: Peano -> *).
Natural n =>
f 'Zero -> (forall (m :: Peano). Natural m => f ('Succ m)) -> f n
natural ((Permutation 'Zero -> Permutation 'Zero -> Permutation 'Zero)
-> Op₂ Permutation Permutation 'Zero
forall k (a :: k -> *) (b :: k -> *) (n :: k).
(a n -> a n -> b n) -> Op₂ a b n
Op₂ ((Permutation 'Zero -> Permutation 'Zero -> Permutation 'Zero)
 -> Op₂ Permutation Permutation 'Zero)
-> (((Permutation 'Zero, Permutation 'Zero) -> Permutation 'Zero)
    -> Permutation 'Zero -> Permutation 'Zero -> Permutation 'Zero)
-> ((Permutation 'Zero, Permutation 'Zero) -> Permutation 'Zero)
-> Op₂ Permutation Permutation 'Zero
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ((Permutation 'Zero, Permutation 'Zero) -> Permutation 'Zero)
-> Permutation 'Zero -> Permutation 'Zero -> Permutation 'Zero
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (((Permutation 'Zero, Permutation 'Zero) -> Permutation 'Zero)
 -> Op₂ Permutation Permutation 'Zero)
-> ((Permutation 'Zero, Permutation 'Zero) -> Permutation 'Zero)
-> Op₂ Permutation Permutation 'Zero
forall a b. (a -> b) -> a -> b
$ \ (PZ, PZ) -> Permutation 'Zero
PZ) ((forall (m :: Peano).
  Natural m =>
  Op₂ Permutation Permutation ('Succ m))
 -> Op₂ Permutation Permutation n)
-> (forall (m :: Peano).
    Natural m =>
    Op₂ Permutation Permutation ('Succ m))
-> Op₂ Permutation Permutation n
forall a b. (a -> b) -> a -> b
$ (Permutation ('Succ m)
 -> Permutation ('Succ m) -> Permutation ('Succ m))
-> Op₂ Permutation Permutation ('Succ m)
forall k (a :: k -> *) (b :: k -> *) (n :: k).
(a n -> a n -> b n) -> Op₂ a b n
Op₂ ((Permutation ('Succ m)
  -> Permutation ('Succ m) -> Permutation ('Succ m))
 -> Op₂ Permutation Permutation ('Succ m))
-> (((Permutation ('Succ m), Permutation ('Succ m))
     -> Permutation ('Succ m))
    -> Permutation ('Succ m)
    -> Permutation ('Succ m)
    -> Permutation ('Succ m))
-> ((Permutation ('Succ m), Permutation ('Succ m))
    -> Permutation ('Succ m))
-> Op₂ Permutation Permutation ('Succ m)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ((Permutation ('Succ m), Permutation ('Succ m))
 -> Permutation ('Succ m))
-> Permutation ('Succ m)
-> Permutation ('Succ m)
-> Permutation ('Succ m)
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (((Permutation ('Succ m), Permutation ('Succ m))
  -> Permutation ('Succ m))
 -> Op₂ Permutation Permutation ('Succ m))
-> ((Permutation ('Succ m), Permutation ('Succ m))
    -> Permutation ('Succ m))
-> Op₂ Permutation Permutation ('Succ m)
forall a b. (a -> b) -> a -> b
$ \ case
        (PS m :: Fin ('Succ n)
m p :: Permutation n
p, PS Zero q) -> Fin ('Succ n) -> Permutation n -> Permutation ('Succ n)
forall (n :: Peano).
Fin ('Succ n) -> Permutation n -> Permutation ('Succ n)
PS Fin ('Succ n)
m (Permutation n
p Permutation n -> Permutation n -> Permutation n
forall a. Semigroup a => a -> a -> a
<> Permutation n
Permutation n
q)
        (PS m :: Fin ('Succ n)
m p :: Permutation n
p, PS n q) -> case Permutation ('Succ n) -> Permutation ('Succ n)
forall a. Group a => a -> a
invert (Fin ('Succ n) -> Permutation n -> Permutation ('Succ n)
forall (n :: Peano).
Fin ('Succ n) -> Permutation n -> Permutation ('Succ n)
PS Fin ('Succ n)
n (Permutation n -> Permutation n
forall a. Group a => a -> a
invert Permutation n
p)) of
            PS o :: Fin ('Succ n)
o r :: Permutation n
r -> case (Fin ('Succ n)
m, Fin ('Succ n)
o) of
                (Zero, _) -> Fin ('Succ n) -> Permutation n -> Permutation ('Succ n)
forall (n :: Peano).
Fin ('Succ n) -> Permutation n -> Permutation ('Succ n)
PS Fin ('Succ n)
o (Permutation n
r Permutation n -> Permutation n -> Permutation n
forall a. Semigroup a => a -> a -> a
<> Permutation n
Permutation n
q)
                (_, Zero) -> Fin ('Succ n) -> Permutation n -> Permutation ('Succ n)
forall (n :: Peano).
Fin ('Succ n) -> Permutation n -> Permutation ('Succ n)
PS Fin ('Succ n)
m (Permutation n
r Permutation n -> Permutation n -> Permutation n
forall a. Semigroup a => a -> a -> a
<> Permutation n
Permutation n
q)
                (Succ m :: Fin n
m, Succ o :: Fin n
o) -> Fin ('Succ n) -> Permutation n -> Permutation ('Succ n)
forall (n :: Peano).
Fin ('Succ n) -> Permutation n -> Permutation ('Succ n)
PS (Fin n -> Fin ('Succ n)
forall (n :: Peano). Fin n -> Fin ('Succ n)
Succ Fin n
o) (Fin n -> Fin n -> Permutation n
forall (n :: Peano). Natural n => Fin n -> Fin n -> Permutation n
swap Fin n
m Fin n
Fin n
o Permutation n -> Permutation n -> Permutation n
forall a. Semigroup a => a -> a -> a
<> Permutation n
r Permutation n -> Permutation n -> Permutation n
forall a. Semigroup a => a -> a -> a
<> Permutation n
Permutation n
q)

instance Natural n => Monoid (Permutation n) where
    mempty :: Permutation n
mempty = Permutation 'Zero
-> (forall (m :: Peano). Natural m => Permutation ('Succ m))
-> Permutation n
forall (n :: Peano) (f :: Peano -> *).
Natural n =>
f 'Zero -> (forall (m :: Peano). Natural m => f ('Succ m)) -> f n
natural Permutation 'Zero
PZ ((forall (m :: Peano). Natural m => Permutation ('Succ m))
 -> Permutation n)
-> (forall (m :: Peano). Natural m => Permutation ('Succ m))
-> Permutation n
forall a b. (a -> b) -> a -> b
$ Fin ('Succ m) -> Permutation m -> Permutation ('Succ m)
forall (n :: Peano).
Fin ('Succ n) -> Permutation n -> Permutation ('Succ n)
PS Fin ('Succ m)
forall (n :: Peano). Fin ('Succ n)
Zero Permutation m
forall a. Monoid a => a
mempty

instance Natural n => Group (Permutation n) where
    invert :: Permutation n -> Permutation n
invert = (List n (Fin n), Permutation n) -> Permutation n
forall a b. (a, b) -> b
snd ((List n (Fin n), Permutation n) -> Permutation n)
-> (Permutation n -> (List n (Fin n), Permutation n))
-> Permutation n
-> Permutation n
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Permutation n -> (List n (Fin n), Permutation n)
forall (n :: Peano).
Permutation n -> (List n (Fin n), Permutation n)
go
      where
        go :: ∀ n . Permutation n -> (List n (Fin n), Permutation n)
        go :: Permutation n -> (List n (Fin n), Permutation n)
go PZ = (List n (Fin n)
forall a. List 'Zero a
Nil, Permutation n
Permutation 'Zero
PZ)
        go (PS n :: Fin ('Succ n)
n p :: Permutation n
p) = (List n (Fin n)
List ('Succ n) (Fin ('Succ n))
ms, Fin ('Succ n) -> Permutation n -> Permutation ('Succ n)
forall (n :: Peano).
Fin ('Succ n) -> Permutation n -> Permutation ('Succ n)
PS Fin ('Succ n)
m Permutation n
q)
          where (ns :: List n (Fin n)
ns, q :: Permutation n
q) = Permutation n -> (List n (Fin n), Permutation n)
forall (n :: Peano).
Permutation n -> (List n (Fin n), Permutation n)
go Permutation n
p
                ms :: List ('Succ n) (Fin ('Succ n))
ms@(m:._) = Fin ('Succ n)
-> Fin ('Succ n)
-> List ('Succ n) (Fin ('Succ n))
-> List ('Succ n) (Fin ('Succ n))
forall (n :: Peano) a. Fin n -> Fin n -> List n a -> List n a
L.swap Fin ('Succ n)
forall (n :: Peano). Fin ('Succ n)
Zero Fin ('Succ n)
n (List ('Succ n) (Fin ('Succ n)) -> List ('Succ n) (Fin ('Succ n)))
-> List ('Succ n) (Fin ('Succ n)) -> List ('Succ n) (Fin ('Succ n))
forall a b. (a -> b) -> a -> b
$ Fin ('Succ n)
forall (n :: Peano). Fin ('Succ n)
ZeroFin ('Succ n)
-> List n (Fin ('Succ n)) -> List ('Succ n) (Fin ('Succ n))
forall a (n :: Peano). a -> List n a -> List ('Succ n) a
:.(Fin n -> Fin ('Succ n)
forall (n :: Peano). Fin n -> Fin ('Succ n)
Succ (Fin n -> Fin ('Succ n))
-> List n (Fin n) -> List n (Fin ('Succ n))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> List n (Fin n)
ns)

-- | Transposition of the giventh elements
swap :: Natural n => Fin n -> Fin n -> Permutation n
swap :: Fin n -> Fin n -> Permutation n
swap = Op₂ Fin Permutation n -> Fin n -> Fin n -> Permutation n
forall k (a :: k -> *) (b :: k -> *) (n :: k).
Op₂ a b n -> a n -> a n -> b n
unOp₂ (Op₂ Fin Permutation n -> Fin n -> Fin n -> Permutation n)
-> Op₂ Fin Permutation n -> Fin n -> Fin n -> Permutation n
forall a b. (a -> b) -> a -> b
$ Op₂ Fin Permutation 'Zero
-> (forall (m :: Peano).
    Natural m =>
    Op₂ Fin Permutation ('Succ m))
-> Op₂ Fin Permutation n
forall (n :: Peano) (f :: Peano -> *).
Natural n =>
f 'Zero -> (forall (m :: Peano). Natural m => f ('Succ m)) -> f n
natural ((Fin 'Zero -> Fin 'Zero -> Permutation 'Zero)
-> Op₂ Fin Permutation 'Zero
forall k (a :: k -> *) (b :: k -> *) (n :: k).
(a n -> a n -> b n) -> Op₂ a b n
Op₂ ((Fin 'Zero -> Fin 'Zero -> Permutation 'Zero)
 -> Op₂ Fin Permutation 'Zero)
-> (Fin 'Zero -> Fin 'Zero -> Permutation 'Zero)
-> Op₂ Fin Permutation 'Zero
forall a b. (a -> b) -> a -> b
$ \ case) ((forall (m :: Peano). Natural m => Op₂ Fin Permutation ('Succ m))
 -> Op₂ Fin Permutation n)
-> (forall (m :: Peano).
    Natural m =>
    Op₂ Fin Permutation ('Succ m))
-> Op₂ Fin Permutation n
forall a b. (a -> b) -> a -> b
$ (Fin ('Succ m) -> Fin ('Succ m) -> Permutation ('Succ m))
-> Op₂ Fin Permutation ('Succ m)
forall k (a :: k -> *) (b :: k -> *) (n :: k).
(a n -> a n -> b n) -> Op₂ a b n
Op₂ ((Fin ('Succ m) -> Fin ('Succ m) -> Permutation ('Succ m))
 -> Op₂ Fin Permutation ('Succ m))
-> (((Fin ('Succ m), Fin ('Succ m)) -> Permutation ('Succ m))
    -> Fin ('Succ m) -> Fin ('Succ m) -> Permutation ('Succ m))
-> ((Fin ('Succ m), Fin ('Succ m)) -> Permutation ('Succ m))
-> Op₂ Fin Permutation ('Succ m)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ((Fin ('Succ m), Fin ('Succ m)) -> Permutation ('Succ m))
-> Fin ('Succ m) -> Fin ('Succ m) -> Permutation ('Succ m)
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (((Fin ('Succ m), Fin ('Succ m)) -> Permutation ('Succ m))
 -> Op₂ Fin Permutation ('Succ m))
-> ((Fin ('Succ m), Fin ('Succ m)) -> Permutation ('Succ m))
-> Op₂ Fin Permutation ('Succ m)
forall a b. (a -> b) -> a -> b
$ \ case
    (Zero, Zero) -> Permutation ('Succ m)
forall a. Monoid a => a
mempty
    (Succ m :: Fin n
m, Succ n) -> Fin ('Succ n) -> Permutation n -> Permutation ('Succ n)
forall (n :: Peano).
Fin ('Succ n) -> Permutation n -> Permutation ('Succ n)
PS Fin ('Succ n)
forall (n :: Peano). Fin ('Succ n)
Zero (Fin n -> Fin n -> Permutation n
forall (n :: Peano). Natural n => Fin n -> Fin n -> Permutation n
swap Fin n
m Fin n
Fin n
n)
    (Zero, Succ n) -> Fin ('Succ n) -> Permutation n -> Permutation ('Succ n)
forall (n :: Peano).
Fin ('Succ n) -> Permutation n -> Permutation ('Succ n)
PS (Fin n -> Fin ('Succ n)
forall (n :: Peano). Fin n -> Fin ('Succ n)
Succ Fin n
n) Permutation n
forall a. Monoid a => a
mempty
    (Succ m :: Fin n
m, Zero) -> Fin ('Succ n) -> Permutation n -> Permutation ('Succ n)
forall (n :: Peano).
Fin ('Succ n) -> Permutation n -> Permutation ('Succ n)
PS (Fin n -> Fin ('Succ n)
forall (n :: Peano). Fin n -> Fin ('Succ n)
Succ Fin n
m) Permutation n
forall a. Monoid a => a
mempty

newtype Op₂ a b n = Op₂ { Op₂ a b n -> a n -> a n -> b n
unOp₂ :: a n -> a n -> b n }

-- | Orbit of the given index under the given permutation
orbit :: Natural n => Permutation n -> Fin n -> NonEmpty (Fin n)
orbit :: Permutation n -> Fin n -> NonEmpty (Fin n)
orbit p :: Permutation n
p n :: Fin n
n = case (List n (Fin n) -> Fin n -> Fin n
forall (n :: Peano) a. List n a -> Fin n -> a
!! Fin n
n) (List n (Fin n) -> Fin n)
-> Stream (List n (Fin n)) -> Stream (Fin n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (List n (Fin n) -> List n (Fin n))
-> List n (Fin n) -> Stream (List n (Fin n))
forall a. (a -> a) -> a -> Stream a
iterate (Permutation n -> List n (Fin n) -> List n (Fin n)
forall (n :: Peano) a. Permutation n -> List n a -> List n a
apply Permutation n
p) List n (Fin n)
forall (n :: Peano). Natural n => List n (Fin n)
enum of
    a :: Fin n
a:<as :: Stream (Fin n)
as -> Fin n
aFin n -> [Fin n] -> NonEmpty (Fin n)
forall a. a -> [a] -> NonEmpty a
:|(Fin n -> Bool) -> Stream (Fin n) -> [Fin n]
forall a. (a -> Bool) -> Stream a -> [a]
takeWhile (Fin n -> Fin n -> Bool
forall a. Eq a => a -> a -> Bool
/= Fin n
a) Stream (Fin n)
as

-- | All the cycles of the given permutation, which are necessarily disjoint
cycles :: ∀ n . Natural n => Permutation (P.Succ n) -> NonEmpty (NonEmpty (Fin (P.Succ n)))
cycles :: Permutation ('Succ n) -> NonEmpty (NonEmpty (Fin ('Succ n)))
cycles p :: Permutation ('Succ n)
p = (NonEmpty (Fin ('Succ n)) -> Fin ('Succ n))
-> NonEmpty (NonEmpty (Fin ('Succ n)))
-> NonEmpty (NonEmpty (Fin ('Succ n)))
forall b a. Eq b => (a -> b) -> NonEmpty a -> NonEmpty a
nubOn NonEmpty (Fin ('Succ n)) -> Fin ('Succ n)
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum (NonEmpty (NonEmpty (Fin ('Succ n)))
 -> NonEmpty (NonEmpty (Fin ('Succ n))))
-> NonEmpty (NonEmpty (Fin ('Succ n)))
-> NonEmpty (NonEmpty (Fin ('Succ n)))
forall a b. (a -> b) -> a -> b
$ Permutation ('Succ n) -> Fin ('Succ n) -> NonEmpty (Fin ('Succ n))
forall (n :: Peano).
Natural n =>
Permutation n -> Fin n -> NonEmpty (Fin n)
orbit Permutation ('Succ n)
p (Fin ('Succ n) -> NonEmpty (Fin ('Succ n)))
-> NonEmpty (Fin ('Succ n)) -> NonEmpty (NonEmpty (Fin ('Succ n)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> case Natural ('Succ n) => List ('Succ n) (Fin ('Succ n))
forall (n :: Peano). Natural n => List n (Fin n)
enum @(P.Succ n) of n :: Fin ('Succ n)
n:.ns :: List n (Fin ('Succ n))
ns -> Fin ('Succ n)
nFin ('Succ n) -> [Fin ('Succ n)] -> NonEmpty (Fin ('Succ n))
forall a. a -> [a] -> NonEmpty a
:|List n (Fin ('Succ n)) -> [Fin ('Succ n)]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList List n (Fin ('Succ n))
ns

infixr 5 :<
data Stream a = a :< Stream a
  deriving (a -> Stream b -> Stream a
(a -> b) -> Stream a -> Stream b
(forall a b. (a -> b) -> Stream a -> Stream b)
-> (forall a b. a -> Stream b -> Stream a) -> Functor Stream
forall a b. a -> Stream b -> Stream a
forall a b. (a -> b) -> Stream a -> Stream b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Stream b -> Stream a
$c<$ :: forall a b. a -> Stream b -> Stream a
fmap :: (a -> b) -> Stream a -> Stream b
$cfmap :: forall a b. (a -> b) -> Stream a -> Stream b
Functor)

iterate :: (a -> a) -> a -> Stream a
iterate :: (a -> a) -> a -> Stream a
iterate f :: a -> a
f a :: a
a = a
a a -> Stream a -> Stream a
forall a. a -> Stream a -> Stream a
:< (a -> a
f (a -> a) -> Stream a -> Stream a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> a) -> a -> Stream a
forall a. (a -> a) -> a -> Stream a
iterate a -> a
f a
a)

takeWhile :: (a -> Bool) -> Stream a -> [a]
takeWhile :: (a -> Bool) -> Stream a -> [a]
takeWhile f :: a -> Bool
f (a :: a
a:<as :: Stream a
as) | a -> Bool
f a
a = a
aa -> [a] -> [a]
forall a. a -> [a] -> [a]
:(a -> Bool) -> Stream a -> [a]
forall a. (a -> Bool) -> Stream a -> [a]
takeWhile a -> Bool
f Stream a
as
                    | Bool
otherwise = []

nubOn :: Eq b => (a -> b) -> NonEmpty a -> NonEmpty a
nubOn :: (a -> b) -> NonEmpty a -> NonEmpty a
nubOn f :: a -> b
f (a :: a
a:|as :: [a]
as) = a
aa -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:|[b] -> [a] -> [a]
go [a -> b
f a
a] [a]
as
  where go :: [b] -> [a] -> [a]
go _ [] = []
        go bs :: [b]
bs (a :: a
a:as :: [a]
as) | b
b b -> [b] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [b]
bs = [b] -> [a] -> [a]
go [b]
bs [a]
as
                     | Bool
otherwise   = a
aa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[b] -> [a] -> [a]
go (b
bb -> [b] -> [b]
forall a. a -> [a] -> [a]
:[b]
bs) [a]
as
          where b :: b
b = a -> b
f a
a