{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}

-- |

-- Module      : OAlg.Entity.Sequence.Permutation

-- Description : permutations on totally ordered index types

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

--

-- permutations on totally ordered index types @__i__@ to permute the items of sequences.

module OAlg.Entity.Sequence.Permutation
  (
    -- * Permutation

    Permutation(), pmt, swap

    -- * Permutable

  , PermutableSequence(..), permuteByN

    -- * Signum

  , pmtSign, splitCycles, splitCycle, Cycle(..)  

    -- * Form

  , PermutationForm(..), pmf

    -- * X

  , xPermutation, xPermutationB, xPermutationN
  , xMltPermutation

    -- * Propositions

  , prpPermutation
  , prpPermutableSequence
  , prpOprPermutation
  ) where

import Control.Monad hiding (sequence)

import Data.List as L (map,zip,repeat,(++),head,tail,splitAt,reverse,span)
import Data.Foldable
import Data.Proxy

import OAlg.Prelude

import OAlg.Data.Filterable
import OAlg.Data.Canonical
import OAlg.Data.Reducible
import OAlg.Data.Constructable
import OAlg.Data.Symbol (Symbol())

import OAlg.Entity.Product

import OAlg.Entity.Sequence.Definition as D
import OAlg.Entity.Sequence.PSequence
import OAlg.Entity.Sequence.CSequence
import OAlg.Entity.Sequence.Set

import OAlg.Structure.PartiallyOrdered
import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative
import OAlg.Structure.Additive
import OAlg.Structure.Exponential
import OAlg.Structure.Operational
import OAlg.Structure.Number.Definition (mod)

--------------------------------------------------------------------------------

-- PermutationForm -


-- | form of a permutation from @__i__@ to @__i__@ which is given by 'pmf'.

--

--  __Property__ Let @p = 'PermutationForm' jis@ be in @'PermutationForm' __i__@, then

-- holds: @'support' z p '==' 'image' z p@ for some proxy @z@ in @__z__ __i__@.

--

-- The partial sequence @ijs@ is called the __/relevant part/__ of @p@.

newtype PermutationForm i = PermutationForm (PSequence i i) deriving (Int -> PermutationForm i -> ShowS
[PermutationForm i] -> ShowS
PermutationForm i -> String
(Int -> PermutationForm i -> ShowS)
-> (PermutationForm i -> String)
-> ([PermutationForm i] -> ShowS)
-> Show (PermutationForm i)
forall i. Show i => Int -> PermutationForm i -> ShowS
forall i. Show i => [PermutationForm i] -> ShowS
forall i. Show i => PermutationForm i -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall i. Show i => Int -> PermutationForm i -> ShowS
showsPrec :: Int -> PermutationForm i -> ShowS
$cshow :: forall i. Show i => PermutationForm i -> String
show :: PermutationForm i -> String
$cshowList :: forall i. Show i => [PermutationForm i] -> ShowS
showList :: [PermutationForm i] -> ShowS
Show,PermutationForm i -> PermutationForm i -> Bool
(PermutationForm i -> PermutationForm i -> Bool)
-> (PermutationForm i -> PermutationForm i -> Bool)
-> Eq (PermutationForm i)
forall i. Eq i => PermutationForm i -> PermutationForm i -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall i. Eq i => PermutationForm i -> PermutationForm i -> Bool
== :: PermutationForm i -> PermutationForm i -> Bool
$c/= :: forall i. Eq i => PermutationForm i -> PermutationForm i -> Bool
/= :: PermutationForm i -> PermutationForm i -> Bool
Eq,PermutationForm i -> N
(PermutationForm i -> N) -> LengthN (PermutationForm i)
forall i. PermutationForm i -> N
forall x. (x -> N) -> LengthN x
$clengthN :: forall i. PermutationForm i -> N
lengthN :: PermutationForm i -> N
LengthN)

instance Ord i => Sequence PermutationForm i i where
  list :: forall (p :: * -> *). p i -> PermutationForm i -> [(i, i)]
list p i
p (PermutationForm PSequence i i
xs) = p i -> PSequence i i -> [(i, i)]
forall (p :: * -> *). p i -> PSequence i i -> [(i, i)]
forall (s :: * -> *) i x (p :: * -> *).
Sequence s i x =>
p i -> s x -> [(x, i)]
list p i
p PSequence i i
xs
  
--------------------------------------------------------------------------------

-- pmf -


-- | the associated function @__i__@ to @__i__@ and is given by:

--

-- __Definition__ Let @p = 'PermutationForm' jis@ be in @'PermutationForm' __i__@

-- then @'pmf' p i@ is defined by: If there exists an @(j,i')@ in @'psqxs' jis@ with

-- @i' '==' i@ then @'pmf' p i = j@ else @'pmf' p i = i@.

--

-- __Note__

--

-- (1) If the partial sequence @ijs@ is 'valid', then for all @i@ in @__i__@ there exists

-- at most one @(_,i')@ in @'psqxs' jis@ such that @i' '==' i@. As such, the function

-- @'pmf' p@ is well defined.

--

-- (2) If the permutation form @p@ itself is 'valid' than @'pmf' p@ is a bijection

-- and as such a permutation of @__i__@.

--

-- (3) The behavior of 'pmf' differs from '??' as its evaluation will not end up in a

-- 'IndexOutOfSupport'-exception.

pmf :: Ord i => PermutationForm i -> i -> i
pmf :: forall i. Ord i => PermutationForm i -> i -> i
pmf (PermutationForm PSequence i i
jis) i
i = case PSequence i i
jis PSequence i i -> i -> Maybe i
forall (s :: * -> *) i x. Sequence s i x => s x -> i -> Maybe x
?? i
i of
  Just i
j -> i
j
  Maybe i
_      -> i
i

--------------------------------------------------------------------------------

-- pmfMlt -


-- | @'pmfMlt' p q@ is the composition of @p@ and @q@, which is given by the

-- composition of there associated functions @'pmf' p '.' 'pmf' q@.

pmfMlt :: Ord i => PermutationForm i -> PermutationForm i -> PermutationForm i
pmfMlt :: forall i.
Ord i =>
PermutationForm i -> PermutationForm i -> PermutationForm i
pmfMlt (PermutationForm PSequence i i
kjs) (PermutationForm PSequence i i
jis) = PSequence i i -> PermutationForm i
forall i. PSequence i i -> PermutationForm i
PermutationForm PSequence i i
kis where
  kis :: PSequence i i
kis = [(i, i)] -> PSequence i i
forall i x. [(x, i)] -> PSequence i x
PSequence ([(i, i)] -> PSequence i i) -> [(i, i)] -> PSequence i i
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(i, i)] -> [(i, i)]
forall b a. Ord b => [(a, b)] -> [(a, b)]
sortSnd ([(i, i)] -> [(i, i)]) -> [(i, i)] -> [(i, i)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (PSequence i i -> [(i, i)]
forall i x. PSequence i x -> [(x, i)]
psqxs PSequence i i
kjs [(i, i)] -> [(i, i)] -> [(i, i)]
forall {a}. Ord a => [(a, a)] -> [(a, a)] -> [(a, a)]
* [(i, i)] -> [(i, i)]
forall a b. Ord a => [(a, b)] -> [(a, b)]
sortFst (PSequence i i -> [(i, i)]
forall i x. PSequence i x -> [(x, i)]
psqxs PSequence i i
jis))
  
  [] * :: [(a, a)] -> [(a, a)] -> [(a, a)]
* [(a, a)]
jis = [(a, a)]
jis
  [(a, a)]
kjs * [] = [(a, a)]
kjs
  kjs :: [(a, a)]
kjs@((a
k,a
j):[(a, a)]
kjs') * jis :: [(a, a)]
jis@((a
j',a
i):[(a, a)]
jis') = case a
j a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` a
j' of
    Ordering
LT -> (a
k,a
j)(a, a) -> [(a, a)] -> [(a, a)]
forall a. a -> [a] -> [a]
:([(a, a)]
kjs' [(a, a)] -> [(a, a)] -> [(a, a)]
* [(a, a)]
jis)
    Ordering
EQ -> (a
k,a
i)(a, a) -> [(a, a)] -> [(a, a)]
forall a. a -> [a] -> [a]
:([(a, a)]
kjs' [(a, a)] -> [(a, a)] -> [(a, a)]
* [(a, a)]
jis')
    Ordering
GT -> (a
j',a
i)(a, a) -> [(a, a)] -> [(a, a)]
forall a. a -> [a] -> [a]
:([(a, a)]
kjs [(a, a)] -> [(a, a)] -> [(a, a)]
* [(a, a)]
jis')

--------------------------------------------------------------------------------

-- pmfOprPsq -


-- | @'pmfOprPsq' xs p@ applies the permutation form @p@ - from right - to the partial

-- sequence @xs@, which is given by the composition of there associated functions

-- @('??') xs '.' 'pmf' p@.

pmfOprPsq :: Ord i => PSequence i x -> PermutationForm i -> PSequence i x
pmfOprPsq :: forall i x.
Ord i =>
PSequence i x -> PermutationForm i -> PSequence i x
pmfOprPsq PSequence i x
xjs (PermutationForm PSequence i i
jis) = [(x, i)] -> PSequence i x
forall i x. [(x, i)] -> PSequence i x
PSequence ([(x, i)] -> [(x, i)]
forall b a. Ord b => [(a, b)] -> [(a, b)]
sortSnd [(x, i)]
xis [(x, i)] -> [(x, i)] -> [(x, i)]
forall a. [a] -> [a] -> [a]
++ [(x, i)]
xis') where
  ([(x, i)]
xis,[(x, i)]
xis') = PSequence i x -> [(x, i)]
forall i x. PSequence i x -> [(x, i)]
psqxs PSequence i x
xjs [(x, i)] -> [(i, i)] -> ([(x, i)], [(x, i)])
forall {b} {a}.
Ord b =>
[(a, b)] -> [(b, b)] -> ([(a, b)], [(a, b)])
* [(i, i)] -> [(i, i)]
forall a b. Ord a => [(a, b)] -> [(a, b)]
sortFst (PSequence i i -> [(i, i)]
forall i x. PSequence i x -> [(x, i)]
psqxs PSequence i i
jis)

  [] * :: [(a, b)] -> [(b, b)] -> ([(a, b)], [(a, b)])
* [(b, b)]
_                               = ([],[])
  [(a, b)]
xjs * []                             = ([],[(a, b)]
xjs)
  xjs :: [(a, b)]
xjs@((a
x,b
j):[(a, b)]
xjs') * jis :: [(b, b)]
jis@((b
j',b
i):[(b, b)]
jis') = case b
j b -> b -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` b
j' of
    Ordering
LT -> ((a
x,b
j)(a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
:[(a, b)]
xis,[(a, b)]
xis') where ([(a, b)]
xis,[(a, b)]
xis') = [(a, b)]
xjs' [(a, b)] -> [(b, b)] -> ([(a, b)], [(a, b)])
* [(b, b)]
jis
    Ordering
EQ -> ((a
x,b
i)(a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
:[(a, b)]
xis,[(a, b)]
xis') where ([(a, b)]
xis,[(a, b)]
xis') = [(a, b)]
xjs' [(a, b)] -> [(b, b)] -> ([(a, b)], [(a, b)])
* [(b, b)]
jis'
    Ordering
GT -> [(a, b)]
xjs [(a, b)] -> [(b, b)] -> ([(a, b)], [(a, b)])
* [(b, b)]
jis'

--------------------------------------------------------------------------------

-- pmfOprLst -


-- | @'pmfOprPsq' xs p@ applies the permutation form @p@ - from right - to the list

-- @xs@, which is given by 'pmfOprPsq' applied to @'PSequence' (xs `'zip` [0..])@.

--

-- __Note__ If @'It' ('lengthN' xs) '<=' u@ - where @(_,u) = 'OAlg.Entity.Sequence.Definition.span' p@

-- - then no exception will be thrown, but the 'lengthN' of the resulting list may be smaller!

pmfOprLst :: [x] -> PermutationForm N -> [x]
pmfOprLst :: forall x. [x] -> PermutationForm N -> [x]
pmfOprLst [x]
xs PermutationForm N
p = PSequence N x -> [x]
forall a b. Projectible a b => b -> a
prj (PSequence N x
xs' PSequence N x -> PermutationForm N -> PSequence N x
forall i x.
Ord i =>
PSequence i x -> PermutationForm i -> PSequence i x
`pmfOprPsq` PermutationForm N
p) where
  xs' :: PSequence N x
xs' = ([x] -> PSequence N x
forall {x}. [x] -> PSequence N x
forall a b. Embeddable a b => a -> b
inj :: [x] -> PSequence N x) [x]
xs

--------------------------------------------------------------------------------

-- pmfOprPsy -


type I = N
type WordN x = [(x,N)]

-- | permutes the product symbol by the given permeation form.

pmfOprPsy :: Entity x => CSequence x -> PermutationForm N -> CSequence x
pmfOprPsy :: forall x.
Entity x =>
CSequence x -> PermutationForm N -> CSequence x
pmfOprPsy (ProductSymbol Product N (U x)
xjs) PermutationForm N
p = CSequence x
xis where
  xis :: CSequence x
xis = Form (CSequence x) -> CSequence x
ProductForm N (U x) -> CSequence x
forall x. Constructable x => Form x -> x
make (ProductForm N (U x) -> CSequence x)
-> ProductForm N (U x) -> CSequence x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Point (U x) -> Word N (U x) -> ProductForm N (U x)
forall r a. Semiring r => Point a -> Word r a -> ProductForm r a
wrdprf () (Word N (U x) -> ProductForm N (U x))
-> Word N (U x) -> ProductForm N (U x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(U x, N)] -> Word N (U x)
forall r a. [(a, r)] -> Word r a
Word ([(U x, N)] -> Word N (U x)) -> [(U x, N)] -> Word N (U x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Span N -> N -> [(U x, N)] -> PermutationForm N -> [(U x, N)]
forall u. Span N -> N -> WordN u -> PermutationForm N -> WordN u
opr (Maybe N -> PermutationForm N -> Span N
forall (s :: * -> *) i x (p :: * -> *).
Sequence s i x =>
p i -> s x -> Span i
D.span (N -> Maybe N
forall a. a -> Maybe a
Just (N
0::N)) PermutationForm N
p) N
0 (Word N (U x) -> [(U x, N)]
forall r a. Word r a -> [(a, r)]
fromWord (Word N (U x) -> [(U x, N)]) -> Word N (U x) -> [(U x, N)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Product N (U x) -> Word N (U x)
forall r a. (Integral r, Oriented a) => Product r a -> Word r a
prwrd Product N (U x)
xjs) PermutationForm N
p

  expand :: N -> (u,N) -> [(u,I)]
  expand :: forall u. N -> (u, N) -> [(u, N)]
expand N
k (u
u,N
l) = (N -> [u] -> [u]
forall a. N -> [a] -> [a]
takeN N
l ([u] -> [u]) -> [u] -> [u]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ u -> [u]
forall a. a -> [a]
repeat u
u) [u] -> [N] -> [(u, N)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [N
k..]

  opr :: Span N -> N -> WordN u -> PermutationForm N -> WordN u
  opr :: forall u. Span N -> N -> WordN u -> PermutationForm N -> WordN u
opr (Closure N
l,Closure N
h) N
_ WordN u
w PermutationForm N
_ | Closure N
h Closure N -> Closure N -> Bool
forall a. Ord a => a -> a -> Bool
<= Closure N
l         = WordN u
w -- empty span

  opr Span N
_ N
_ [] PermutationForm N
_                     = []
  opr (Closure N
l,Closure N
h) N
k ((u, N)
w:WordN u
ws) PermutationForm N
p | N -> Closure N
forall x. x -> Closure x
It N
k' Closure N -> Closure N -> Bool
forall a. Ord a => a -> a -> Bool
< Closure N
l = (u, N)
w (u, N) -> WordN u -> WordN u
forall a. a -> [a] -> [a]
: Span N -> N -> WordN u -> PermutationForm N -> WordN u
forall u. Span N -> N -> WordN u -> PermutationForm N -> WordN u
opr (Closure N
l,Closure N
h) N
k' WordN u
ws PermutationForm N
p
                        | Closure N
h Closure N -> Closure N -> Bool
forall a. Ord a => a -> a -> Bool
< N -> Closure N
forall x. x -> Closure x
It N
k' = (u, N)
w(u, N) -> WordN u -> WordN u
forall a. a -> [a] -> [a]
:WordN u
ws -- see the note below

                        | Bool
otherwise = Closure N
-> N -> WordN u -> WordN u -> PermutationForm N -> WordN u
forall u.
Closure N
-> N -> [(u, N)] -> [(u, N)] -> PermutationForm N -> [(u, N)]
opr' Closure N
h N
k [] ((u, N)
w(u, N) -> WordN u -> WordN u
forall a. a -> [a] -> [a]
:WordN u
ws) PermutationForm N
p
    where k' :: N
k' = N
k N -> N -> N
forall a. Additive a => a -> a -> a
+ (u, N) -> N
forall a b. (a, b) -> b
snd (u, N)
w
    -- Note: the span of p is within the first word w, and as such, applying p

    -- will not alter w.


  opr' :: Closure N -> N -> [(u,I)] -> WordN u -> PermutationForm N -> WordN u
  opr' :: forall u.
Closure N
-> N -> [(u, N)] -> [(u, N)] -> PermutationForm N -> [(u, N)]
opr' Closure N
_ N
_ [(u, N)]
uis [] PermutationForm N
p            = PSequence N u -> PermutationForm N -> [(u, N)]
forall u. PSequence N u -> PermutationForm N -> WordN u
opr'' ([(u, N)] -> PSequence N u
forall i x. [(x, i)] -> PSequence i x
PSequence [(u, N)]
uis) PermutationForm N
p
  opr' Closure N
h N
k [(u, N)]
uis [(u, N)]
ws PermutationForm N
p | Closure N
h Closure N -> Closure N -> Bool
forall a. Ord a => a -> a -> Bool
< N -> Closure N
forall x. x -> Closure x
It N
k = PSequence N u -> PermutationForm N -> [(u, N)]
forall u. PSequence N u -> PermutationForm N -> WordN u
opr'' ([(u, N)] -> PSequence N u
forall i x. [(x, i)] -> PSequence i x
PSequence [(u, N)]
uis) PermutationForm N
p [(u, N)] -> [(u, N)] -> [(u, N)]
forall a. [a] -> [a] -> [a]
++ [(u, N)]
ws
  opr' Closure N
h N
k [(u, N)]
uis ((u, N)
w:[(u, N)]
ws) PermutationForm N
p        = Closure N
-> N -> [(u, N)] -> [(u, N)] -> PermutationForm N -> [(u, N)]
forall u.
Closure N
-> N -> [(u, N)] -> [(u, N)] -> PermutationForm N -> [(u, N)]
opr' Closure N
h (N
kN -> N -> N
forall a. Additive a => a -> a -> a
+(u, N) -> N
forall a b. (a, b) -> b
snd (u, N)
w) ([(u, N)]
uis [(u, N)] -> [(u, N)] -> [(u, N)]
forall a. [a] -> [a] -> [a]
++ N -> (u, N) -> [(u, N)]
forall u. N -> (u, N) -> [(u, N)]
expand N
k (u, N)
w) [(u, N)]
ws PermutationForm N
p

  opr'' :: PSequence N u -> PermutationForm N -> WordN u
  opr'' :: forall u. PSequence N u -> PermutationForm N -> WordN u
opr'' PSequence N u
uis PermutationForm N
p = ((u, N) -> (u, N)) -> [(u, N)] -> [(u, N)]
forall a b. (a -> b) -> [a] -> [b]
map (\(u
u,N
_) -> (u
u,N
1)) ([(u, N)] -> [(u, N)]) -> [(u, N)] -> [(u, N)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ PSequence N u -> [(u, N)]
forall i x. PSequence i x -> [(x, i)]
psqxs (PSequence N u -> [(u, N)]) -> PSequence N u -> [(u, N)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (PSequence N u
uis PSequence N u -> PermutationForm N -> PSequence N u
forall i x.
Ord i =>
PSequence i x -> PermutationForm i -> PSequence i x
`pmfOprPsq` PermutationForm N
p)

--------------------------------------------------------------------------------

-- pmfPsq -


-- | orders the partial sequence according to the given ordering an delivers the resulting

-- permutation form.

pmfPsq :: Ord i
  => (w -> w -> Ordering) -> (x -> w) -> PSequence i x -> (PSequence i x,PermutationForm i)
pmfPsq :: forall i w x.
Ord i =>
(w -> w -> Ordering)
-> (x -> w) -> PSequence i x -> (PSequence i x, PermutationForm i)
pmfPsq w -> w -> Ordering
wcmp x -> w
w (PSequence [(x, i)]
xjs) = ([(x, i)] -> PSequence i x
forall i x. [(x, i)] -> PSequence i x
PSequence [(x, i)]
xjs',PSequence i i -> PermutationForm i
forall i. PSequence i i -> PermutationForm i
PermutationForm ([(i, i)] -> PSequence i i
forall i x. [(x, i)] -> PSequence i x
PSequence [(i, i)]
jis)) where
  wjxs :: [((w, i), x)]
wjxs = ((w, i) -> (w, i) -> Ordering) -> [((w, i), x)] -> [((w, i), x)]
forall a b. (a -> a -> Ordering) -> [(a, b)] -> [(a, b)]
sortFstBy (w, i) -> (w, i) -> Ordering
cmp ([((w, i), x)] -> [((w, i), x)]) -> [((w, i), x)] -> [((w, i), x)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((x, i) -> ((w, i), x)) -> [(x, i)] -> [((w, i), x)]
forall a b. (a -> b) -> [a] -> [b]
map (\(x
x,i
j) -> ((x -> w
w x
x,i
j),x
x)) [(x, i)]
xjs
  js :: [i]
js   = ((x, i) -> i) -> [(x, i)] -> [i]
forall a b. (a -> b) -> [a] -> [b]
map (x, i) -> i
forall a b. (a, b) -> b
snd [(x, i)]
xjs
  xjs' :: [(x, i)]
xjs' = (((w, i), x) -> x) -> [((w, i), x)] -> [x]
forall a b. (a -> b) -> [a] -> [b]
map ((w, i), x) -> x
forall a b. (a, b) -> b
snd [((w, i), x)]
wjxs [x] -> [i] -> [(x, i)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [i]
js
  jis :: [(i, i)]
jis  = (((w, i), x) -> i) -> [((w, i), x)] -> [i]
forall a b. (a -> b) -> [a] -> [b]
map ((w, i) -> i
forall a b. (a, b) -> b
snd((w, i) -> i) -> (((w, i), x) -> (w, i)) -> ((w, i), x) -> i
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
.((w, i), x) -> (w, i)
forall a b. (a, b) -> a
fst) [((w, i), x)]
wjxs [i] -> [i] -> [(i, i)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [i]
js

  cmp :: (w, i) -> (w, i) -> Ordering
cmp = (w -> w -> Ordering)
-> (i -> i -> Ordering) -> (w, i) -> (w, i) -> Ordering
forall a b.
(a -> a -> Ordering)
-> (b -> b -> Ordering) -> (a, b) -> (a, b) -> Ordering
compare2 w -> w -> Ordering
wcmp i -> i -> Ordering
forall a. Ord a => a -> a -> Ordering
compare

--------------------------------------------------------------------------------

-- pmfLst -


-- | orders the list according to the given ordering an delivers the resulting

-- permutation form.

pmfLst :: (w -> w -> Ordering) -> (x -> w) -> [x] -> ([x],PermutationForm N)
pmfLst :: forall w x.
(w -> w -> Ordering) -> (x -> w) -> [x] -> ([x], PermutationForm N)
pmfLst w -> w -> Ordering
wcmp x -> w
w [x]
xs = (((x, N) -> x) -> [(x, N)] -> [x]
forall a b. (a -> b) -> [a] -> [b]
map (x, N) -> x
forall a b. (a, b) -> a
fst ([(x, N)] -> [x]) -> [(x, N)] -> [x]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ PSequence N x -> [(x, N)]
forall i x. PSequence i x -> [(x, i)]
psqxs (PSequence N x -> [(x, N)]) -> PSequence N x -> [(x, N)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ PSequence N x
xs',PermutationForm N
p) where
  (PSequence N x
xs',PermutationForm N
p) = (w -> w -> Ordering)
-> (x -> w) -> PSequence N x -> (PSequence N x, PermutationForm N)
forall i w x.
Ord i =>
(w -> w -> Ordering)
-> (x -> w) -> PSequence i x -> (PSequence i x, PermutationForm i)
pmfPsq w -> w -> Ordering
wcmp x -> w
w ([x] -> PSequence N x
forall a b. Embeddable a b => a -> b
inj [x]
xs)

--------------------------------------------------------------------------------

-- pmfPsy -


-- | orders the product symbol according to the given ordering an delivers the resulting

-- permutation form.

pmfPsy :: Entity x
  => (w -> w -> Ordering) -> (x -> w) -> CSequence x
  -> (CSequence x,PermutationForm N)
pmfPsy :: forall x w.
Entity x =>
(w -> w -> Ordering)
-> (x -> w) -> CSequence x -> (CSequence x, PermutationForm N)
pmfPsy w -> w -> Ordering
wcmp x -> w
w CSequence x
xs = ([x] -> CSequence x
forall x. Entity x => [x] -> ProductSymbol x
productSymbol [x]
xs',PermutationForm N
p) where
  ([x]
xs',PermutationForm N
p) = (w -> w -> Ordering) -> (x -> w) -> [x] -> ([x], PermutationForm N)
forall w x.
(w -> w -> Ordering) -> (x -> w) -> [x] -> ([x], PermutationForm N)
pmfLst w -> w -> Ordering
wcmp x -> w
w (CSequence x -> [x]
forall a. ProductSymbol a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList CSequence x
xs)

--------------------------------------------------------------------------------

-- PermuationForm - Entity -

  
instance (Entity i, Ord i) => Validable (PermutationForm i) where
  valid :: PermutationForm i -> Statement
valid p :: PermutationForm i
p@(PermutationForm PSequence i i
jis) = String -> Label
Label String
"PermutationForm" Label -> Statement -> Statement
:<=>:
    [Statement] -> Statement
And [ PSequence i i -> Statement
forall a. Validable a => a -> Statement
valid PSequence i i
jis
        , String -> Label
Label String
"1" Label -> Statement -> Statement
:<=>: (PSequence i i -> PermutationForm i -> Set i
forall (s :: * -> *) i x (p :: * -> *).
Sequence s i x =>
p i -> s x -> Set i
support PSequence i i
jis PermutationForm i
p Set i -> Set i -> Bool
forall a. Eq a => a -> a -> Bool
== PSequence i i -> PermutationForm i -> Set i
forall (s :: * -> *) i x (p :: * -> *).
(Sequence s i x, Ord x) =>
p i -> s x -> Set x
image PSequence i i
jis PermutationForm i
p)Bool -> Message -> Statement
:?>[Parameter] -> Message
Params [String
"p"String -> String -> Parameter
:=PermutationForm i -> String
forall a. Show a => a -> String
show PermutationForm i
p]
        ]

-- instance (Entity i, Ord i) => Entity (PermutationForm i)


--------------------------------------------------------------------------------

-- PermutationForm - Oriented -


type instance Point (PermutationForm i) = ()

instance ShowPoint (PermutationForm i)
instance EqPoint (PermutationForm i)
instance ValidablePoint (PermutationForm i)
instance TypeablePoint (PermutationForm i)

instance (Entity i, Ord i) => Oriented (PermutationForm i) where
  orientation :: PermutationForm i -> Orientation (Point (PermutationForm i))
orientation = Orientation () -> PermutationForm i -> Orientation ()
forall b a. b -> a -> b
const (()() -> () -> Orientation ()
forall p. p -> p -> Orientation p
:>())

--------------------------------------------------------------------------------

-- PermutationForm - Reducible -


instance Eq i => Reducible (PermutationForm i) where
  reduce :: PermutationForm i -> PermutationForm i
reduce (PermutationForm (PSequence [(i, i)]
jis)) = PSequence i i -> PermutationForm i
forall i. PSequence i i -> PermutationForm i
PermutationForm ([(i, i)] -> PSequence i i
forall i x. [(x, i)] -> PSequence i x
PSequence [(i, i)]
jis') where
    jis' :: [(i, i)]
jis' = ((i, i) -> Bool) -> [(i, i)] -> [(i, i)]
forall x. (x -> Bool) -> [x] -> [x]
forall (s :: * -> *) x. Filterable s => (x -> Bool) -> s x -> s x
filter (\(i
j,i
i) -> i
j i -> i -> Bool
forall a. Eq a => a -> a -> Bool
/= i
i) [(i, i)]
jis

--------------------------------------------------------------------------------

-- Permutation -


-- | permutation of a totally ordered index type @__i__@ which yield a /bijection/ 'pmt' on

--  @__i__@. They are constructed using

--

-- * 'make' of a 'valid' 'PermutationForm', which defines also the validity for

-- the constructed permutation.

--

-- * 'swap' and the 'Multiplicative' structure for permutations.

--

-- * 'permuteBy' for 'PermutableSequence'.

--

-- * 'xPermutation' to generate randomly permutations.

--

-- In the following the total right operation '<*' of a permutation on several types of

-- sequences will be defined to achieve the permutation of there items.

--

-- __Definitions__

--

-- [List] Let @xs@ be in @[__x__]@ with @'ConstructableSequence' [] __r__ [__x__]@ and @p@

-- a permutation in @'Permutation' __r__@, then @xs '<*' p@ is given by

-- @'sqcIndexMap' is ('pmt' p) xs@, where @is@ is the image of the support of @xs@

-- under the inverse of @p@.

--

-- [CSequence] Let @xs@ be in @'CSequence' __x__@ with

-- @'ConstructableSequence' 'CSequence' 'N' __x__@ and @p@ a permutation in

-- @'Permutation' 'N'@, then @xs '<*' p@ is given by

-- @'sqcIndexMap' is ('pmt' p) xs@, where @is@ is the image of the support of @xs@

-- under the inverse of @p@.

--

-- [PSequence] Let @xs@ be in @'PSequence' __i__ __x__@ with

-- @'ConstructableSequence' ('PSequence' __i__) __i__ __x__@ and @p@ a permutation in

-- @'Permutation' __i__@, then @xs '<*' p@ is given by

-- @'sqcIndexMap' is ('pmt' p) xs@, where @is@ is the image of the support of @xs@

-- under the inverse of @p@.

--

-- [Permutation] Let @xs@, @p@ be in @'Permutation' __i__@, then @xs '<*' p@ is given

-- by '*'.

--

-- __Note__ The given definitions are not very efficient and only terminate for finite

-- sequences (in fact, a more efficient implementation has been chosen that also

-- terminates for infinite sequences (see example below)). However, they serve on the one

-- hand to define the semantic and to \'prove\' the properties for 'TotalOpr' and on the

-- other hand to verify the chosen implementation for finite sequences (see

-- 'prpOprPermutation').

--

-- __Examples__

--

-- >>> "abcdef" <* (swap 2 5 :: Permutation N)

-- "abfdec"

--

-- the support of a sequence and the relevant image of a permutation may be disjoint which

-- will leave the sequence untouched

--

-- >>> "abcdef" <* (swap 7 10 :: Permutation N)

-- "abcdef"

--

-- the intersection of the support of a sequence with the relevant image of a permutation

-- may be a non empty proper sub set

--

-- >>> "abcdef" <* swap 2 10 :: Permutation N)

-- "abdefc"

--

-- the result can be interpreted as: first, put @c@ at position @10@ and 'Nothing'

-- (which is the item at position @10@) at position @2@. Second, strip all nothings form it.

--

-- Although the given definition of the permutation of sequences dose not terminate for

-- infinite sequences, its implementation will terminate

--

-- >>> takeN 5 $ (([0..] :: [N]) <* (swap 1 2 :: Permutation N)

-- [0,2,1,3,4]

newtype Permutation i = Permutation (PermutationForm i)
  deriving (Int -> Permutation i -> ShowS
[Permutation i] -> ShowS
Permutation i -> String
(Int -> Permutation i -> ShowS)
-> (Permutation i -> String)
-> ([Permutation i] -> ShowS)
-> Show (Permutation i)
forall i. Show i => Int -> Permutation i -> ShowS
forall i. Show i => [Permutation i] -> ShowS
forall i. Show i => Permutation i -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall i. Show i => Int -> Permutation i -> ShowS
showsPrec :: Int -> Permutation i -> ShowS
$cshow :: forall i. Show i => Permutation i -> String
show :: Permutation i -> String
$cshowList :: forall i. Show i => [Permutation i] -> ShowS
showList :: [Permutation i] -> ShowS
Show,Permutation i -> Permutation i -> Bool
(Permutation i -> Permutation i -> Bool)
-> (Permutation i -> Permutation i -> Bool) -> Eq (Permutation i)
forall i. Eq i => Permutation i -> Permutation i -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall i. Eq i => Permutation i -> Permutation i -> Bool
== :: Permutation i -> Permutation i -> Bool
$c/= :: forall i. Eq i => Permutation i -> Permutation i -> Bool
/= :: Permutation i -> Permutation i -> Bool
Eq,Permutation i -> Statement
(Permutation i -> Statement) -> Validable (Permutation i)
forall i.
(Show i, Validable i, Typeable i, Ord i) =>
Permutation i -> Statement
forall a. (a -> Statement) -> Validable a
$cvalid :: forall i.
(Show i, Validable i, Typeable i, Ord i) =>
Permutation i -> Statement
valid :: Permutation i -> Statement
Validable,Permutation i -> N
(Permutation i -> N) -> LengthN (Permutation i)
forall i. Permutation i -> N
forall x. (x -> N) -> LengthN x
$clengthN :: forall i. Permutation i -> N
lengthN :: Permutation i -> N
LengthN)

instance Exposable (Permutation i) where
  type Form (Permutation i) = PermutationForm i
  form :: Permutation i -> Form (Permutation i)
form (Permutation PermutationForm i
f) = Form (Permutation i)
PermutationForm i
f

instance Eq i => Constructable (Permutation i) where
  make :: Form (Permutation i) -> Permutation i
make Form (Permutation i)
f = PermutationForm i -> Permutation i
forall i. PermutationForm i -> Permutation i
Permutation (PermutationForm i -> Permutation i)
-> PermutationForm i -> Permutation i
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ PermutationForm i -> PermutationForm i
forall e. Reducible e => e -> e
reduce Form (Permutation i)
PermutationForm i
f

instance Ord i => Sequence Permutation i i where
  list :: forall (p :: * -> *). p i -> Permutation i -> [(i, i)]
list p i
f (Permutation PermutationForm i
p) = p i -> PermutationForm i -> [(i, i)]
forall (p :: * -> *). p i -> PermutationForm i -> [(i, i)]
forall (s :: * -> *) i x (p :: * -> *).
Sequence s i x =>
p i -> s x -> [(x, i)]
list p i
f PermutationForm i
p
  Permutation PermutationForm i
p ?? :: Permutation i -> i -> Maybe i
?? i
i = PermutationForm i
p PermutationForm i -> i -> Maybe i
forall (s :: * -> *) i x. Sequence s i x => s x -> i -> Maybe x
?? i
i

--------------------------------------------------------------------------------

-- pmt -


-- | the bijection on @__i__@ for a given permutation and is defined via

--   @'restrict' 'pmf'@.

pmt :: Ord i => Permutation i -> i -> i
pmt :: forall i. Ord i => Permutation i -> i -> i
pmt = (Form (Permutation i) -> i -> i) -> Permutation i -> i -> i
forall x y. Exposable x => (Form x -> y) -> x -> y
restrict Form (Permutation i) -> i -> i
PermutationForm i -> i -> i
forall i. Ord i => PermutationForm i -> i -> i
pmf

--------------------------------------------------------------------------------

-- Permutation - Cayleyan -


type instance Point (Permutation i) = ()

instance ShowPoint (Permutation i)
instance EqPoint (Permutation i)
instance ValidablePoint (Permutation i)
instance TypeablePoint (Permutation i)
instance SingletonPoint (Permutation i)

instance (Entity i, Ord i) => Oriented (Permutation i) where
  orientation :: Permutation i -> Orientation (Point (Permutation i))
orientation = (Form (Permutation i) -> Orientation ())
-> Permutation i -> Orientation ()
forall x y. Exposable x => (Form x -> y) -> x -> y
restrict Form (Permutation i) -> Orientation ()
PermutationForm i -> Orientation (Point (PermutationForm i))
forall q. Oriented q => q -> Orientation (Point q)
orientation

instance (Entity i, Ord i) => Multiplicative (Permutation i) where
  one :: Point (Permutation i) -> Permutation i
one Point (Permutation i)
_ = Form (Permutation i) -> Permutation i
forall x. Constructable x => Form x -> x
make (PSequence i i -> PermutationForm i
forall i. PSequence i i -> PermutationForm i
PermutationForm PSequence i i
forall i x. PSequence i x
psqEmpty)
  Permutation PermutationForm i
f * :: Permutation i -> Permutation i -> Permutation i
* Permutation PermutationForm i
g = Form (Permutation i) -> Permutation i
forall x. Constructable x => Form x -> x
make (PermutationForm i
f PermutationForm i -> PermutationForm i -> PermutationForm i
forall i.
Ord i =>
PermutationForm i -> PermutationForm i -> PermutationForm i
`pmfMlt` PermutationForm i
g)

instance (Entity i, Ord i) => Invertible (Permutation i) where
  tryToInvert :: Permutation i -> Solver (Permutation i)
tryToInvert (Permutation (PermutationForm (PSequence [(i, i)]
jis)))
    = Permutation i -> Solver (Permutation i)
forall a. a -> Solver a
forall (m :: * -> *) a. Monad m => a -> m a
return (PermutationForm i -> Permutation i
forall i. PermutationForm i -> Permutation i
Permutation (PSequence i i -> PermutationForm i
forall i. PSequence i i -> PermutationForm i
PermutationForm ([(i, i)] -> PSequence i i
forall i x. [(x, i)] -> PSequence i x
PSequence [(i, i)]
ijs)))
    where ijs :: [(i, i)]
ijs = [(i, i)] -> [(i, i)]
forall b a. Ord b => [(a, b)] -> [(a, b)]
sortSnd ([(i, i)] -> [(i, i)]) -> [(i, i)] -> [(i, i)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((i, i) -> (i, i)) -> [(i, i)] -> [(i, i)]
forall a b. (a -> b) -> [a] -> [b]
map (\(i
j,i
i) -> (i
i,i
j)) [(i, i)]
jis

instance (Entity i, Ord i) => Cayleyan (Permutation i)

instance (Entity i, Ord i) => Exponential (Permutation i) where
  type Exponent (Permutation i) = Z
  ^ :: Permutation i -> Exponent (Permutation i) -> Permutation i
(^) = Permutation i -> Z -> Permutation i
Permutation i -> Exponent (Permutation i) -> Permutation i
forall c. Invertible c => c -> Z -> c
zpower

--------------------------------------------------------------------------------

-- swap -


-- | swapping.

--

-- __Property__ Let @p = 'swap' n (i,j)@, then holds:

-- If @i,j '<' n@ then @p@ is the permutation given by swapping @i@ with @j@, otherwise a

-- exception will be thrown.

swap :: (Entity i, Ord i) => i -> i -> Permutation i
swap :: forall i. (Entity i, Ord i) => i -> i -> Permutation i
swap i
i i
j = case i
i i -> i -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` i
j of
  Ordering
LT -> Form (Permutation i) -> Permutation i
forall x. Constructable x => Form x -> x
make (PSequence i i -> PermutationForm i
forall i. PSequence i i -> PermutationForm i
PermutationForm ([(i, i)] -> PSequence i i
forall i x. [(x, i)] -> PSequence i x
PSequence [(i
j,i
i),(i
i,i
j)]))
  Ordering
EQ -> Point (Permutation i) -> Permutation i
forall c. Multiplicative c => Point c -> c
one ()
  Ordering
GT -> i -> i -> Permutation i
forall i. (Entity i, Ord i) => i -> i -> Permutation i
swap i
j i
i

--------------------------------------------------------------------------------

-- PermutableSequence -


-- | total right operations of permutations on sequences, admitting the following

--   properties:

--

--  __Property__ Let @__s__@, @__i__@, @__x__@ be an instance of

--  @'PermutableSequence'  __s__ __i__ __x__@, then holds:

--

--  (1) Let @xs@ be in @__s__ __x__@, @p@ in @'Permutation' __i__@ with

--  @'image' z p '<<=' 'support' z xs@ for some @z@ in @__z__ __i__@, then holds:

--  @(xs '<*' p) '??' i '==' ((xs '??') '.' 'pmt' p) i@ for all @i@ in @'support' z xs@.

--

--  (2) Let @xs@ be in @__s__ __x__@, @w@ in @__x__ -> __w__@,

--  @c@ in @__w__ -> __w__ -> 'Ordering'@ and @z@ in @__z__ __i__@, then holds:

--  Let @(xs',p) = 'permuteBy' z c w xs@ in

--

--      (1) @xs' '==' xs '<*' p@.

--

--      (2) @xs'@ is ordered according to @c@ by applying @w@ to its items.

--

--      (3) @'image' z p '<<=' 'support' z xs@.

--

-- __Examples__

--

-- >>> fst $ permuteBy nProxy compare isUpper "abCd1eFgH"

-- "abd1egCFH"

--

-- as @'False' '<' 'True'@

--

-- >>> fst $ permuteBy nProxy (coCompare compare) isUpper "abCd1eFgH"

-- "CFHabd1eg"

--

-- which orders it in the reverse ordering.

class (Sequence s i x, TotalOpr (Permutation i) (s x))
  => PermutableSequence s i x where
  -- | a resulting permuation.

  permuteBy :: p i -> (w -> w -> Ordering) -> (x -> w) -> s x -> (s x,Permutation i)


--------------------------------------------------------------------------------

-- permuteByN -


-- | orders the permutable sequence according to the given ordering an delivers the resulting

-- permutation form.

permuteByN :: PermutableSequence s N x
  => (w -> w -> Ordering) -> (x -> w) -> s x -> (s x,Permutation N)
permuteByN :: forall (s :: * -> *) x w.
PermutableSequence s N x =>
(w -> w -> Ordering) -> (x -> w) -> s x -> (s x, Permutation N)
permuteByN = Maybe N
-> (w -> w -> Ordering) -> (x -> w) -> s x -> (s x, Permutation N)
forall (p :: * -> *) w.
p N
-> (w -> w -> Ordering) -> (x -> w) -> s x -> (s x, Permutation N)
forall (s :: * -> *) i x (p :: * -> *) w.
PermutableSequence s i x =>
p i
-> (w -> w -> Ordering) -> (x -> w) -> s x -> (s x, Permutation i)
permuteBy (N -> Maybe N
forall a. a -> Maybe a
Just (N
0 :: N))

--------------------------------------------------------------------------------

-- PSequence N - PermutableSequence -


instance Ord i => Opr (Permutation i) (PSequence i x) where
  PSequence i x
xs <* :: PSequence i x -> Permutation i -> PSequence i x
<* Permutation i
p = PSequence i x -> PermutationForm i -> PSequence i x
forall i x.
Ord i =>
PSequence i x -> PermutationForm i -> PSequence i x
pmfOprPsq PSequence i x
xs (Permutation i -> Form (Permutation i)
forall x. Exposable x => x -> Form x
form Permutation i
p)

instance (Entity i, Ord i, Entity x) => TotalOpr (Permutation i) (PSequence i x)

instance (Entity x, Entity i, Ord i) => PermutableSequence (PSequence i) i x where
  permuteBy :: forall (p :: * -> *) w.
p i
-> (w -> w -> Ordering)
-> (x -> w)
-> PSequence i x
-> (PSequence i x, Permutation i)
permuteBy p i
_ w -> w -> Ordering
cmp x -> w
w PSequence i x
xs = (PSequence i x
xs',Form (Permutation i) -> Permutation i
forall x. Constructable x => Form x -> x
make Form (Permutation i)
PermutationForm i
p) where (PSequence i x
xs',PermutationForm i
p) = (w -> w -> Ordering)
-> (x -> w) -> PSequence i x -> (PSequence i x, PermutationForm i)
forall i w x.
Ord i =>
(w -> w -> Ordering)
-> (x -> w) -> PSequence i x -> (PSequence i x, PermutationForm i)
pmfPsq w -> w -> Ordering
cmp x -> w
w PSequence i x
xs

--------------------------------------------------------------------------------

-- [x] - PermutableSequence -


instance Opr (Permutation N) [x] where
  [x]
xs <* :: [x] -> Permutation N -> [x]
<* Permutation N
p = [x] -> PermutationForm N -> [x]
forall x. [x] -> PermutationForm N -> [x]
pmfOprLst [x]
xs (Permutation N -> Form (Permutation N)
forall x. Exposable x => x -> Form x
form Permutation N
p)

instance Entity x => TotalOpr (Permutation N) [x]

instance Entity x => PermutableSequence [] N x where
  permuteBy :: forall (p :: * -> *) w.
p N
-> (w -> w -> Ordering) -> (x -> w) -> [x] -> ([x], Permutation N)
permuteBy p N
_ w -> w -> Ordering
wcmp x -> w
w [x]
xs = ([x]
xs',Form (Permutation N) -> Permutation N
forall x. Constructable x => Form x -> x
make Form (Permutation N)
PermutationForm N
p) where ([x]
xs',PermutationForm N
p) = (w -> w -> Ordering) -> (x -> w) -> [x] -> ([x], PermutationForm N)
forall w x.
(w -> w -> Ordering) -> (x -> w) -> [x] -> ([x], PermutationForm N)
pmfLst w -> w -> Ordering
wcmp x -> w
w [x]
xs

--------------------------------------------------------------------------------

-- CSequence - PermutableSequence -


instance Entity x => Opr (Permutation N) (CSequence x) where
  CSequence x
xs <* :: CSequence x -> Permutation N -> CSequence x
<* Permutation N
p = CSequence x -> PermutationForm N -> CSequence x
forall x.
Entity x =>
CSequence x -> PermutationForm N -> CSequence x
pmfOprPsy CSequence x
xs (Permutation N -> Form (Permutation N)
forall x. Exposable x => x -> Form x
form Permutation N
p)

instance Entity x => TotalOpr (Permutation N) (CSequence x)

instance Entity x => PermutableSequence CSequence N x where
  permuteBy :: forall (p :: * -> *) w.
p N
-> (w -> w -> Ordering)
-> (x -> w)
-> CSequence x
-> (CSequence x, Permutation N)
permuteBy p N
_ w -> w -> Ordering
wcmp x -> w
w CSequence x
xs = (CSequence x
xs',Form (Permutation N) -> Permutation N
forall x. Constructable x => Form x -> x
make Form (Permutation N)
PermutationForm N
p) where (CSequence x
xs',PermutationForm N
p) = (w -> w -> Ordering)
-> (x -> w) -> CSequence x -> (CSequence x, PermutationForm N)
forall x w.
Entity x =>
(w -> w -> Ordering)
-> (x -> w) -> CSequence x -> (CSequence x, PermutationForm N)
pmfPsy w -> w -> Ordering
wcmp x -> w
w CSequence x
xs

--------------------------------------------------------------------------------

-- Permutation - PermutableSequence -


instance (Entity i, Ord i) => Opr (Permutation i) (Permutation i) where
  <* :: Permutation i -> Permutation i -> Permutation i
(<*) = Permutation i -> Permutation i -> Permutation i
forall c. Multiplicative c => c -> c -> c
(*)

instance (Entity i, Ord i) => TotalOpr (Permutation i) (Permutation i)

instance (Entity i, Ord i) => PermutableSequence Permutation i i where
  permuteBy :: forall (p :: * -> *) w.
p i
-> (w -> w -> Ordering)
-> (i -> w)
-> Permutation i
-> (Permutation i, Permutation i)
permuteBy p i
f w -> w -> Ordering
wcmp i -> w
w (Permutation (PermutationForm PSequence i i
p))
    = (Form (Permutation i) -> Permutation i
forall x. Constructable x => Form x -> x
make (PSequence i i -> PermutationForm i
forall i. PSequence i i -> PermutationForm i
PermutationForm PSequence i i
p'),Permutation i
q) where (PSequence i i
p',Permutation i
q) = p i
-> (w -> w -> Ordering)
-> (i -> w)
-> PSequence i i
-> (PSequence i i, Permutation i)
forall (p :: * -> *) w.
p i
-> (w -> w -> Ordering)
-> (i -> w)
-> PSequence i i
-> (PSequence i i, Permutation i)
forall (s :: * -> *) i x (p :: * -> *) w.
PermutableSequence s i x =>
p i
-> (w -> w -> Ordering) -> (x -> w) -> s x -> (s x, Permutation i)
permuteBy p i
f w -> w -> Ordering
wcmp i -> w
w PSequence i i
p

--------------------------------------------------------------------------------

-- Cycle -


-- | cycle over the index @__i__@, i.e. a monomorphic list @i 0, i 1 .. i j, i (j+1)..,i (n-1),i n@

--   where @1 <= n@ and represents the permutation where @i j@ maps to @i (j+1)@ for @j = 0..n.1@ and

--   @j n@ maps to @i 0@.

--

--   __Properties__ Let @'Cycle' is@ be in @'Cycle' __i__@, then holds:

--

--  (1) @'length' is '>=' 2@.

--

--  (2) @is@ is monomorph.

newtype Cycle i = Cycle [i] deriving (Int -> Cycle i -> ShowS
[Cycle i] -> ShowS
Cycle i -> String
(Int -> Cycle i -> ShowS)
-> (Cycle i -> String) -> ([Cycle i] -> ShowS) -> Show (Cycle i)
forall i. Show i => Int -> Cycle i -> ShowS
forall i. Show i => [Cycle i] -> ShowS
forall i. Show i => Cycle i -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall i. Show i => Int -> Cycle i -> ShowS
showsPrec :: Int -> Cycle i -> ShowS
$cshow :: forall i. Show i => Cycle i -> String
show :: Cycle i -> String
$cshowList :: forall i. Show i => [Cycle i] -> ShowS
showList :: [Cycle i] -> ShowS
Show,Cycle i -> Cycle i -> Bool
(Cycle i -> Cycle i -> Bool)
-> (Cycle i -> Cycle i -> Bool) -> Eq (Cycle i)
forall i. Eq i => Cycle i -> Cycle i -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall i. Eq i => Cycle i -> Cycle i -> Bool
== :: Cycle i -> Cycle i -> Bool
$c/= :: forall i. Eq i => Cycle i -> Cycle i -> Bool
/= :: Cycle i -> Cycle i -> Bool
Eq,Eq (Cycle i)
Eq (Cycle i) =>
(Cycle i -> Cycle i -> Ordering)
-> (Cycle i -> Cycle i -> Bool)
-> (Cycle i -> Cycle i -> Bool)
-> (Cycle i -> Cycle i -> Bool)
-> (Cycle i -> Cycle i -> Bool)
-> (Cycle i -> Cycle i -> Cycle i)
-> (Cycle i -> Cycle i -> Cycle i)
-> Ord (Cycle i)
Cycle i -> Cycle i -> Bool
Cycle i -> Cycle i -> Ordering
Cycle i -> Cycle i -> Cycle i
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall i. Ord i => Eq (Cycle i)
forall i. Ord i => Cycle i -> Cycle i -> Bool
forall i. Ord i => Cycle i -> Cycle i -> Ordering
forall i. Ord i => Cycle i -> Cycle i -> Cycle i
$ccompare :: forall i. Ord i => Cycle i -> Cycle i -> Ordering
compare :: Cycle i -> Cycle i -> Ordering
$c< :: forall i. Ord i => Cycle i -> Cycle i -> Bool
< :: Cycle i -> Cycle i -> Bool
$c<= :: forall i. Ord i => Cycle i -> Cycle i -> Bool
<= :: Cycle i -> Cycle i -> Bool
$c> :: forall i. Ord i => Cycle i -> Cycle i -> Bool
> :: Cycle i -> Cycle i -> Bool
$c>= :: forall i. Ord i => Cycle i -> Cycle i -> Bool
>= :: Cycle i -> Cycle i -> Bool
$cmax :: forall i. Ord i => Cycle i -> Cycle i -> Cycle i
max :: Cycle i -> Cycle i -> Cycle i
$cmin :: forall i. Ord i => Cycle i -> Cycle i -> Cycle i
min :: Cycle i -> Cycle i -> Cycle i
Ord)

instance (Show i, Ord i, Validable i) => Validable (Cycle i) where
  valid :: Cycle i -> Statement
valid (Cycle [i]
is) = String -> Label
Label String
"Cycle" Label -> Statement -> Statement
:<=>:
    [Statement] -> Statement
And [ [i] -> Statement
forall a. Validable a => a -> Statement
valid [i]
is
        , String -> Label
Label String
"length" Label -> Statement -> Statement
:<=>: ([i] -> N
forall x. LengthN x => x -> N
lengthN [i]
is N -> N -> Bool
forall a. Ord a => a -> a -> Bool
>= N
2) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"length is"String -> String -> Parameter
:= (N -> String
forall a. Show a => a -> String
show (N -> String) -> N -> String
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [i] -> N
forall x. LengthN x => x -> N
lengthN [i]
is)]
        , String -> Label
Label String
"monomorph" Label -> Statement -> Statement
:<=>: ([i] -> N
forall x. LengthN x => x -> N
lengthN [i]
is N -> N -> Bool
forall a. Eq a => a -> a -> Bool
== (Set i -> N
forall x. LengthN x => x -> N
lengthN (Set i -> N) -> Set i -> N
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [i] -> Set i
forall x. Ord x => [x] -> Set x
set [i]
is)) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"is"String -> String -> Parameter
:=[i] -> String
forall a. Show a => a -> String
show [i]
is]
        ]

--------------------------------------------------------------------------------

-- splitCycle -


-- | splits a permutation in a cycle and its residuum permutation.

splitCycle :: Eq i => Permutation i -> Maybe (Cycle i,Permutation i)
splitCycle :: forall i. Eq i => Permutation i -> Maybe (Cycle i, Permutation i)
splitCycle Permutation i
p = do
  PermutationForm PSequence i i
jis <- PermutationForm i -> Maybe (PermutationForm i)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (PermutationForm i -> Maybe (PermutationForm i))
-> PermutationForm i -> Maybe (PermutationForm i)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Permutation i -> Form (Permutation i)
forall x. Exposable x => x -> Form x
form Permutation i
p
  (Cycle i
c,PSequence i i
jis')            <- PSequence i i -> Maybe (Cycle i, PSequence i i)
forall i. Eq i => PSequence i i -> Maybe (Cycle i, PSequence i i)
splitCycle' PSequence i i
jis
  (Cycle i, Permutation i) -> Maybe (Cycle i, Permutation i)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Cycle i
c,Form (Permutation i) -> Permutation i
PermutationForm i -> Permutation i
forall x. Constructable x => Form x -> x
make (PermutationForm i -> Permutation i)
-> PermutationForm i -> Permutation i
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ PSequence i i -> PermutationForm i
forall i. PSequence i i -> PermutationForm i
PermutationForm PSequence i i
jis')

splitCycle' :: Eq i => PSequence i i -> Maybe (Cycle i,PSequence i i)
splitCycle' :: forall i. Eq i => PSequence i i -> Maybe (Cycle i, PSequence i i)
splitCycle' (PSequence [])          = Maybe (Cycle i, PSequence i i)
forall a. Maybe a
Nothing
splitCycle' (PSequence ((i
j,i
i):[(i, i)]
jis)) = (Cycle i, PSequence i i) -> Maybe (Cycle i, PSequence i i)
forall a. a -> Maybe a
Just ([i] -> Cycle i
forall i. [i] -> Cycle i
Cycle ([i] -> Cycle i) -> [i] -> Cycle i
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [i] -> [i]
forall a. [a] -> [a]
reverse [i]
cs,[(i, i)] -> PSequence i i
forall i x. [(x, i)] -> PSequence i x
PSequence [(i, i)]
jis') where
  ([i]
cs,[(i, i)]
jis') = i -> i -> ([i], [(i, i)]) -> ([i], [(i, i)])
forall {t}. Eq t => t -> t -> ([t], [(t, t)]) -> ([t], [(t, t)])
sc i
i i
j ([i
i],[(i, i)]
jis)

  sc :: t -> t -> ([t], [(t, t)]) -> ([t], [(t, t)])
sc t
i t
j ([t], [(t, t)])
res | t
i t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
j = ([t], [(t, t)])
res
  sc t
i t
j ([t]
cs,[(t, t)]
jis)     = case ((t, t) -> Bool) -> [(t, t)] -> ([(t, t)], [(t, t)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.span ((t
jt -> t -> Bool
forall a. Eq a => a -> a -> Bool
/=) (t -> Bool) -> ((t, t) -> t) -> (t, t) -> Bool
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. (t, t) -> t
forall a b. (a, b) -> b
snd) [(t, t)]
jis of
    ([(t, t)]
jis',[(t, t)]
jis'')     -> case [(t, t)]
jis'' of
      (t
j',t
_):[(t, t)]
jis'''  -> t -> t -> ([t], [(t, t)]) -> ([t], [(t, t)])
sc t
i t
j' (t
jt -> [t] -> [t]
forall a. a -> [a] -> [a]
:[t]
cs,[(t, t)]
jis' [(t, t)] -> [(t, t)] -> [(t, t)]
forall a. [a] -> [a] -> [a]
++ [(t, t)]
jis''')
      [(t, t)]
_              -> AlgebraicException -> ([t], [(t, t)])
forall a e. Exception e => e -> a
throw (AlgebraicException -> ([t], [(t, t)]))
-> AlgebraicException -> ([t], [(t, t)])
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ String -> AlgebraicException
InvalidData String
"splitCycle'"
    
--------------------------------------------------------------------------------

-- splitCycles -


-- | splits a permutation in a list of cycles.

splitCycles :: Eq i => Permutation i -> [Cycle i]
splitCycles :: forall i. Eq i => Permutation i -> [Cycle i]
splitCycles Permutation i
p = PSequence i i -> [Cycle i]
forall {i}. Eq i => PSequence i i -> [Cycle i]
cyc PSequence i i
is where
  PermutationForm PSequence i i
is = Permutation i -> Form (Permutation i)
forall x. Exposable x => x -> Form x
form Permutation i
p
  
  cyc :: PSequence i i -> [Cycle i]
cyc PSequence i i
is = case PSequence i i -> Maybe (Cycle i, PSequence i i)
forall i. Eq i => PSequence i i -> Maybe (Cycle i, PSequence i i)
splitCycle' PSequence i i
is of
    Maybe (Cycle i, PSequence i i)
Nothing      -> []
    Just (Cycle i
c,PSequence i i
is') -> Cycle i
c Cycle i -> [Cycle i] -> [Cycle i]
forall a. a -> [a] -> [a]
: PSequence i i -> [Cycle i]
cyc PSequence i i
is'
  
--------------------------------------------------------------------------------

-- pmtSign -


-- | the signum of a permutation

pmtSign :: Permutation N -> Z
pmtSign :: Permutation N -> Z
pmtSign Permutation N
p = if N -> N -> N
forall a. Integral a => a -> a -> a
mod ([Cycle N] -> N
forall x. LengthN x => x -> N
lengthN ([Cycle N] -> N) -> [Cycle N] -> N
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Permutation N -> [Cycle N]
forall i. Eq i => Permutation i -> [Cycle i]
splitCycles Permutation N
p) N
2 N -> N -> Bool
forall a. Eq a => a -> a -> Bool
== N
0 then Z
1 else -Z
1

--------------------------------------------------------------------------------

-- xPermutation -


-- | random variable of permutations.

xPermutation :: (Entity i, Ord i)
  => N -- ^ maximal number of swappings.

  -> X i -- ^ span of the swappings.

  -> X (Permutation i)
xPermutation :: forall i. (Entity i, Ord i) => N -> X i -> X (Permutation i)
xPermutation N
n X i
xi = N -> N -> X N
xNB N
0 N
n X N -> (N -> X (Permutation i)) -> X (Permutation i)
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= N -> Permutation i -> N -> X (Permutation i)
pmt N
0 (Point (Permutation i) -> Permutation i
forall c. Multiplicative c => Point c -> c
one ()) where
  pmt :: N -> Permutation i -> N -> X (Permutation i)
pmt N
k Permutation i
p N
n | N
n N -> N -> Bool
forall a. Ord a => a -> a -> Bool
<= N
k = Permutation i -> X (Permutation i)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return Permutation i
p
  pmt N
k Permutation i
p N
n = do
    (i
i,i
j) <- X i -> X i -> X (i, i)
forall a b. X a -> X b -> X (a, b)
xTupple2 X i
xi X i
xi
    N -> Permutation i -> N -> X (Permutation i)
pmt (N -> N
forall a. Enum a => a -> a
succ N
k) (Permutation i
pPermutation i -> Permutation i -> Permutation i
forall c. Multiplicative c => c -> c -> c
*i -> i -> Permutation i
forall i. (Entity i, Ord i) => i -> i -> Permutation i
swap i
i i
j) N
n

--------------------------------------------------------------------------------

-- xPermutationB -


-- | random variable of permutations within the given bounds.

xPermutationB :: (Ord i, Enum i) => i -> i -> X (Permutation i)
xPermutationB :: forall i. (Ord i, Enum i) => i -> i -> X (Permutation i)
xPermutationB i
l i
h = do
  [i]
is' <- Int -> [i] -> X [i]
forall {a}. Int -> [a] -> X [a]
xp ([i] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [i]
is) [i]
is
  Permutation i -> X (Permutation i)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Permutation i -> X (Permutation i))
-> Permutation i -> X (Permutation i)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Form (Permutation i) -> Permutation i
PermutationForm i -> Permutation i
forall x. Constructable x => Form x -> x
make (PermutationForm i -> Permutation i)
-> PermutationForm i -> Permutation i
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ PSequence i i -> PermutationForm i
forall i. PSequence i i -> PermutationForm i
PermutationForm (PSequence i i -> PermutationForm i)
-> PSequence i i -> PermutationForm i
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(i, i)] -> PSequence i i
forall i x. [(x, i)] -> PSequence i x
PSequence ([i]
is' [i] -> [i] -> [(i, i)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [i]
is)
  where
    is :: [i]
is = i -> i -> [i]
forall i. (Ord i, Enum i) => i -> i -> [i]
enum i
l i
h
    xp :: Int -> [a] -> X [a]
xp Int
l [a]
is | Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1    = [a] -> X [a]
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return [a]
is
            | Bool
otherwise = do
      Int
n <- Int -> Int -> X Int
xIntB Int
1 Int
l
      if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
l
        then [a] -> X [a]
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return [a]
is
        else let ([a]
is',[a]
is'') = Int -> [a] -> ([a], [a])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [a]
is in do
          [a]
is''' <- Int -> [a] -> X [a]
xp (Int -> Int
forall a. Enum a => a -> a
pred Int
l) ([a]
is' [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a] -> [a]
forall a. HasCallStack => [a] -> [a]
tail [a]
is'')
          [a] -> X [a]
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return ([a] -> a
forall a. HasCallStack => [a] -> a
head [a]
is''a -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
is''')

--------------------------------------------------------------------------------

-- xPermutationN -


-- | random variable of permutations of the index set @[0..prd n]@. 

xPermutationN :: N -> X (Permutation N)
xPermutationN :: N -> X (Permutation N)
xPermutationN N
0 = Permutation N -> X (Permutation N)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Point (Permutation N) -> Permutation N
forall c. Multiplicative c => Point c -> c
one ())
xPermutationN N
n = N -> N -> X (Permutation N)
forall i. (Ord i, Enum i) => i -> i -> X (Permutation i)
xPermutationB N
0 (N -> N
forall a. Enum a => a -> a
pred N
n)

dd :: Int -> X (Permutation N) -> IO ()
dd :: Int -> X (Permutation N) -> IO ()
dd Int
n X (Permutation N)
xp = IO Omega
getOmega IO Omega -> (Omega -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Int -> X N -> Omega -> IO ()
forall x. (Show x, Ord x) => Int -> X x -> Omega -> IO ()
putDistribution Int
n ((Permutation N -> N) -> X (Permutation N) -> X N
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (Permutation N -> N -> N
forall i. Ord i => Permutation i -> i -> i
`pmt`(N
0::N)) X (Permutation N)
xp)

--------------------------------------------------------------------------------

-- xMltPermutation -


-- | random variable for validating the 'Multiplicative' structure.

xMltPermutation :: (Entity i, Ord i) => N -> X i -> XMlt (Permutation i)
xMltPermutation :: forall i. (Entity i, Ord i) => N -> X i -> XMlt (Permutation i)
xMltPermutation N
n X i
xi = X N -> X (Permutation i) -> XMlt (Permutation i)
forall c. Singleton (Point c) => X N -> X c -> XMlt c
xMltTtl (N -> N -> X N
xNB N
0 N
10) (N -> X i -> X (Permutation i)
forall i. (Entity i, Ord i) => N -> X i -> X (Permutation i)
xPermutation N
n X i
xi)

--------------------------------------------------------------------------------

-- relOprPermutation -


relOprPermutation :: (TotalOpr (Permutation i) (s x), ConstructableSequence s i x)
  => p i -> s x -> Permutation i -> Statement
relOprPermutation :: forall i (s :: * -> *) x (p :: * -> *).
(TotalOpr (Permutation i) (s x), ConstructableSequence s i x) =>
p i -> s x -> Permutation i -> Statement
relOprPermutation p i
pi s x
xs Permutation i
p = (s x
xs s x -> Permutation i -> s x
forall f x. Opr f x => x -> f -> x
<* Permutation i
p s x -> s x -> Bool
forall a. Eq a => a -> a -> Bool
== Set i -> (i -> i) -> s x -> s x
forall (s :: * -> *) i x j.
(ConstructableSequence s i x, Sequence s j x) =>
Set i -> (i -> j) -> s x -> s x
sqcIndexMap Set i
is (Permutation i -> i -> i
forall i. Ord i => Permutation i -> i -> i
pmt Permutation i
p) s x
xs)
                Bool -> Message -> Statement
:?>[Parameter] -> Message
Params [String
"xs"String -> String -> Parameter
:=s x -> String
forall a. Show a => a -> String
show s x
xs,String
"p"String -> String -> Parameter
:=Permutation i -> String
forall a. Show a => a -> String
show Permutation i
p] where
  is :: Set i
is = (i -> i) -> Set i -> Set i
forall y x. Ord y => (x -> y) -> Set x -> Set y
setMap (Permutation i -> i -> i
forall i. Ord i => Permutation i -> i -> i
pmt Permutation i
p') (Set i -> Set i) -> Set i -> Set i
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ p i -> s x -> Set i
forall (s :: * -> *) i x (p :: * -> *).
Sequence s i x =>
p i -> s x -> Set i
support p i
pi s x
xs
  p' :: Permutation i
p' = Permutation i -> Permutation i
forall c. Invertible c => c -> c
invert Permutation i
p

--------------------------------------------------------------------------------

-- relOprPermutationLst -


relOprPermutationLst :: Entity x => X [x] -> X (Permutation N) -> Statement
relOprPermutationLst :: forall x. Entity x => X [x] -> X (Permutation N) -> Statement
relOprPermutationLst X [x]
xxs X (Permutation N)
xp = String -> Label
Label String
"[]"
  Label -> Statement -> Statement
:<=>: X ([x], Permutation N)
-> (([x], Permutation N) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall  X ([x], Permutation N)
xxsp (([x] -> Permutation N -> Statement)
-> ([x], Permutation N) -> Statement
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Proxy N -> [x] -> Permutation N -> Statement
forall i (s :: * -> *) x (p :: * -> *).
(TotalOpr (Permutation i) (s x), ConstructableSequence s i x) =>
p i -> s x -> Permutation i -> Statement
relOprPermutation Proxy N
nProxy)) where
  xxsp :: X ([x], Permutation N)
xxsp = X [x] -> X (Permutation N) -> X ([x], Permutation N)
forall a b. X a -> X b -> X (a, b)
xTupple2 X [x]
xxs X (Permutation N)
xp

--------------------------------------------------------------------------------

-- relOprPermutationPsq -


-- | validity of the right operation of permutations on partial sequences according

--   to its definition.

relOprPermutationPsq :: (Entity x, Entity i, Ord i)
  => X (PSequence i x) -> X (Permutation i) -> Statement
relOprPermutationPsq :: forall x i.
(Entity x, Entity i, Ord i) =>
X (PSequence i x) -> X (Permutation i) -> Statement
relOprPermutationPsq X (PSequence i x)
xxs X (Permutation i)
xp = String -> Label
Label String
"PSequence"
  Label -> Statement -> Statement
:<=>: X (PSequence i x, Permutation i)
-> ((PSequence i x, Permutation i) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall (X (PSequence i x)
-> X (Permutation i) -> X (PSequence i x, Permutation i)
forall a b. X a -> X b -> X (a, b)
xTupple2 X (PSequence i x)
xxs X (Permutation i)
xp) ((PSequence i x -> Permutation i -> Statement)
-> (PSequence i x, Permutation i) -> Statement
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Proxy i -> PSequence i x -> Permutation i -> Statement
forall i (s :: * -> *) x (p :: * -> *).
(TotalOpr (Permutation i) (s x), ConstructableSequence s i x) =>
p i -> s x -> Permutation i -> Statement
relOprPermutation (X (PSequence i x) -> Proxy i
forall i x. X (PSequence i x) -> Proxy i
p X (PSequence i x)
xxs))) where
  p :: X (PSequence i x) -> Proxy i
  p :: forall i x. X (PSequence i x) -> Proxy i
p X (PSequence i x)
_ = Proxy i
forall {k} (t :: k). Proxy t
Proxy
    
--------------------------------------------------------------------------------

-- relOprPermutationPsy -


relOprPermutationPsy :: Entity x
  => X (CSequence x) -> X (Permutation N) -> Statement
relOprPermutationPsy :: forall x.
Entity x =>
X (CSequence x) -> X (Permutation N) -> Statement
relOprPermutationPsy X (ProductSymbol x)
xxs X (Permutation N)
xp = String -> Label
Label String
"CSequence"
  Label -> Statement -> Statement
:<=>: X (ProductSymbol x, Permutation N)
-> ((ProductSymbol x, Permutation N) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall (X (ProductSymbol x)
-> X (Permutation N) -> X (ProductSymbol x, Permutation N)
forall a b. X a -> X b -> X (a, b)
xTupple2 X (ProductSymbol x)
xxs X (Permutation N)
xp) ((ProductSymbol x -> Permutation N -> Statement)
-> (ProductSymbol x, Permutation N) -> Statement
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Proxy N -> ProductSymbol x -> Permutation N -> Statement
forall i (s :: * -> *) x (p :: * -> *).
(TotalOpr (Permutation i) (s x), ConstructableSequence s i x) =>
p i -> s x -> Permutation i -> Statement
relOprPermutation Proxy N
nProxy))

--------------------------------------------------------------------------------

-- prpOprPermutaiton -


-- | validity of the total right operation '<*' of permutations on sequences.

prpOprPermutation :: Statement
prpOprPermutation :: Statement
prpOprPermutation = String -> Label
Prp String
"OprPermutation"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [Statement
prpLst,Statement
prpPsy,Statement
prpPsq] where
  xp :: N -> N -> X (Permutation N)
xp N
n N
m = N -> X N -> X (Permutation N)
forall i. (Entity i, Ord i) => N -> X i -> X (Permutation i)
xPermutation N
n (N -> N -> X N
xNB N
0 N
m)

  prpLst :: Statement
prpLst = X [Symbol] -> X (Permutation N) -> Statement
forall x. Entity x => X [x] -> X (Permutation N) -> Statement
relOprPermutationLst X [Symbol]
xxs (N -> N -> X (Permutation N)
xp N
40 N
100) where
    xxs :: X [Symbol]
xxs  = N -> N -> X N
xNB N
0 N
20 X N -> (N -> X [Symbol]) -> X [Symbol]
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \N
n -> N -> X Symbol -> X [Symbol]
forall x. N -> X x -> X [x]
xTakeN N
n (X Symbol
forall x. XStandard x => X x
xStandard :: X Symbol)

  prpPsy :: Statement
prpPsy = X (CSequence Symbol) -> X (Permutation N) -> Statement
forall x.
Entity x =>
X (CSequence x) -> X (Permutation N) -> Statement
relOprPermutationPsy X (CSequence Symbol)
xxs (N -> N -> X (Permutation N)
xp N
40 N
100) where
    xxs :: X (CSequence Symbol)
xxs = N -> X Symbol -> X (CSequence Symbol)
forall x. Entity x => N -> X x -> X (CSequence x)
xCSequence N
20 (X Symbol
forall x. XStandard x => X x
xStandard :: X Symbol)
    
  prpPsq :: Statement
prpPsq = X (PSequence N Symbol) -> X (Permutation N) -> Statement
forall x i.
(Entity x, Entity i, Ord i) =>
X (PSequence i x) -> X (Permutation i) -> Statement
relOprPermutationPsq X (PSequence N Symbol)
xxs (N -> N -> X (Permutation N)
xp N
40 N
300) where
    xxs :: X (PSequence N Symbol)
xxs = N -> N -> X Symbol -> X N -> X (PSequence N Symbol)
forall i x. Ord i => N -> N -> X x -> X i -> X (PSequence i x)
xPSequence N
20 N
40 (X Symbol
forall x. XStandard x => X x
xStandard :: X Symbol) (N -> N -> X N
xNB N
0 N
200)

--------------------------------------------------------------------------------

-- relPmtSqc1 -


relPmtSqc1 :: (PermutableSequence s i x, Entity x, Entity i)
  => N -> z i -> s x -> Statement
relPmtSqc1 :: forall (s :: * -> *) i x (z :: * -> *).
(PermutableSequence s i x, Entity x, Entity i) =>
N -> z i -> s x -> Statement
relPmtSqc1 N
n z i
z s x
xs = case [i]
is of
  [] -> Statement
SValid -- with out this match, there will be denied permisses

  [i]
_  -> X (Permutation i, i)
-> ((Permutation i, i) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (Permutation i, i)
xpi (\(Permutation i
p,i
i)
                    -> ((s x
xss x -> Permutation i -> s x
forall f x. Opr f x => x -> f -> x
<*Permutation i
p)s x -> i -> Maybe x
forall (s :: * -> *) i x. Sequence s i x => s x -> i -> Maybe x
??i
i Maybe x -> Maybe x -> Bool
forall a. Eq a => a -> a -> Bool
== ((s x
xss x -> i -> Maybe x
forall (s :: * -> *) i x. Sequence s i x => s x -> i -> Maybe x
??) (i -> Maybe x) -> (i -> i) -> i -> Maybe x
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. Permutation i -> i -> i
forall i. Ord i => Permutation i -> i -> i
pmt Permutation i
p) i
i)
                         Bool -> Message -> Statement
:?> [Parameter] -> Message
Params[String
"xs"String -> String -> Parameter
:=s x -> String
forall a. Show a => a -> String
show s x
xs,String
"p"String -> String -> Parameter
:=Permutation i -> String
forall a. Show a => a -> String
show Permutation i
p,String
"i"String -> String -> Parameter
:=i -> String
forall a. Show a => a -> String
show i
i]
                   )
  where
    Set [i]
is = z i -> s x -> Set i
forall (s :: * -> *) i x (p :: * -> *).
Sequence s i x =>
p i -> s x -> Set i
support z i
z s x
xs
    xi :: X i
xi = [i] -> X i
forall a. [a] -> X a
xOneOf [i]
is
    xp :: X (Permutation i)
xp = N -> X i -> X (Permutation i)
forall i. (Entity i, Ord i) => N -> X i -> X (Permutation i)
xPermutation N
n X i
xi
    xpi :: X (Permutation i, i)
xpi = X (Permutation i) -> X i -> X (Permutation i, i)
forall a b. X a -> X b -> X (a, b)
xTupple2 X (Permutation i)
xp X i
xi 

--------------------------------------------------------------------------------

-- relPmtSqc2 -


relPmtSqc2 :: (PermutableSequence s i x, Show w)
  => z i -> (w -> w -> Ordering) -> (x -> w) -> s x -> Statement
relPmtSqc2 :: forall (s :: * -> *) i x w (z :: * -> *).
(PermutableSequence s i x, Show w) =>
z i -> (w -> w -> Ordering) -> (x -> w) -> s x -> Statement
relPmtSqc2 z i
z w -> w -> Ordering
c x -> w
w s x
xs = let (s x
xs',Permutation i
p) = z i
-> (w -> w -> Ordering) -> (x -> w) -> s x -> (s x, Permutation i)
forall (p :: * -> *) w.
p i
-> (w -> w -> Ordering) -> (x -> w) -> s x -> (s x, Permutation i)
forall (s :: * -> *) i x (p :: * -> *) w.
PermutableSequence s i x =>
p i
-> (w -> w -> Ordering) -> (x -> w) -> s x -> (s x, Permutation i)
permuteBy z i
z w -> w -> Ordering
c x -> w
w s x
xs in
  [Statement] -> Statement
And [ String -> Label
Label String
"1" Label -> Statement -> Statement
:<=>: (s x
xs' s x -> s x -> Bool
forall a. Eq a => a -> a -> Bool
== s x
xs s x -> Permutation i -> s x
forall f x. Opr f x => x -> f -> x
<* Permutation i
p) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"xs"String -> String -> Parameter
:=s x -> String
forall a. Show a => a -> String
show s x
xs,String
"p"String -> String -> Parameter
:=Permutation i -> String
forall a. Show a => a -> String
show Permutation i
p]
      , String -> Label
Label String
"2" Label -> Statement -> Statement
:<=>: [x] -> Statement
increasing (((x, i) -> x) -> [(x, i)] -> [x]
forall a b. (a -> b) -> [a] -> [b]
map (x, i) -> x
forall a b. (a, b) -> a
fst ([(x, i)] -> [x]) -> [(x, i)] -> [x]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ z i -> s x -> [(x, i)]
forall (p :: * -> *). p i -> s x -> [(x, i)]
forall (s :: * -> *) i x (p :: * -> *).
Sequence s i x =>
p i -> s x -> [(x, i)]
list z i
z s x
xs')
      , String -> Label
Label String
"3" Label -> Statement -> Statement
:<=>: (z i -> Permutation i -> Set i
forall (s :: * -> *) i x (p :: * -> *).
(Sequence s i x, Ord x) =>
p i -> s x -> Set x
image z i
z Permutation i
p Set i -> Set i -> Bool
forall a. PartiallyOrdered a => a -> a -> Bool
<<= z i -> s x -> Set i
forall (s :: * -> *) i x (p :: * -> *).
Sequence s i x =>
p i -> s x -> Set i
support z i
z s x
xs) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"xs"String -> String -> Parameter
:=s x -> String
forall a. Show a => a -> String
show s x
xs,String
"p"String -> String -> Parameter
:=Permutation i -> String
forall a. Show a => a -> String
show Permutation i
p]
      ] where

  w
w <= :: w -> w -> Bool
<= w
w' = case w -> w -> Ordering
c w
w w
w' of
    Ordering
GT -> Bool
False
    Ordering
_  -> Bool
True
    
  increasing :: [x] -> Statement
increasing []     = Statement
SValid
  increasing (x
x:[x]
xs) = N -> w -> [x] -> Statement
inc (N
0::N) (x -> w
w x
x) [x]
xs where
    inc :: N -> w -> [x] -> Statement
inc N
_ w
_ []      = Statement
SValid
    inc N
i w
wx (x
y:[x]
xs) = let wy :: w
wy = x -> w
w x
y in
      [Statement] -> Statement
And [ (w
wx w -> w -> Bool
<= w
wy) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"i"String -> String -> Parameter
:=N -> String
forall a. Show a => a -> String
show N
i,String
"(wx,wy)"String -> String -> Parameter
:=(w, w) -> String
forall a. Show a => a -> String
show (w
wx,w
wy)]
          , N -> w -> [x] -> Statement
inc (N -> N
forall a. Enum a => a -> a
succ N
i) w
wy [x]
xs
          ]
  
--------------------------------------------------------------------------------

-- prpPermutableSequence -


-- | validity for 'PermutableSequence'.

prpPermutableSequence :: (PermutableSequence s i x, Entity x, Entity i, Show w)
  => N -> z i -> (w -> w -> Ordering) -> (x -> w) -> X (s x) -> Statement
prpPermutableSequence :: forall (s :: * -> *) i x w (z :: * -> *).
(PermutableSequence s i x, Entity x, Entity i, Show w) =>
N
-> z i -> (w -> w -> Ordering) -> (x -> w) -> X (s x) -> Statement
prpPermutableSequence N
n z i
z w -> w -> Ordering
c x -> w
w X (s x)
xxs = String -> Label
Prp String
"PermutableSequence" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ String -> Label
Label String
"1" Label -> Statement -> Statement
:<=>: X (s x) -> (s x -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (s x)
xxs (N -> z i -> s x -> Statement
forall (s :: * -> *) i x (z :: * -> *).
(PermutableSequence s i x, Entity x, Entity i) =>
N -> z i -> s x -> Statement
relPmtSqc1 N
n z i
z)
      , String -> Label
Label String
"2" Label -> Statement -> Statement
:<=>: X (s x) -> (s x -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (s x)
xxs (z i -> (w -> w -> Ordering) -> (x -> w) -> s x -> Statement
forall (s :: * -> *) i x w (z :: * -> *).
(PermutableSequence s i x, Show w) =>
z i -> (w -> w -> Ordering) -> (x -> w) -> s x -> Statement
relPmtSqc2 z i
z w -> w -> Ordering
c x -> w
w)
      ]

--------------------------------------------------------------------------------

-- prpPermutation -


-- | validity of the functionality of the module "Permutation".

prpPermutation :: Statement
prpPermutation :: Statement
prpPermutation = String -> Label
Prp String
"Permutation" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ XMlt (Permutation N) -> Statement
forall c. Multiplicative c => XMlt c -> Statement
prpMlt (N -> X N -> XMlt (Permutation N)
forall i. (Entity i, Ord i) => N -> X i -> XMlt (Permutation i)
xMltPermutation N
20 (N -> N -> X N
xNB N
0 N
50))
      , Statement
prpOprPermutation
      , N
-> Proxy N
-> (N -> N -> Ordering)
-> (N -> N)
-> X [N]
-> Statement
forall (s :: * -> *) i x w (z :: * -> *).
(PermutableSequence s i x, Entity x, Entity i, Show w) =>
N
-> z i -> (w -> w -> Ordering) -> (x -> w) -> X (s x) -> Statement
prpPermutableSequence N
10 Proxy N
nProxy N -> N -> Ordering
forall a. Ord a => a -> a -> Ordering
compare N -> N
forall x. x -> x
id X [N]
xxs
      , N
-> Proxy N
-> (Symbol -> Symbol -> Ordering)
-> (Symbol -> Symbol)
-> X (PSequence N Symbol)
-> Statement
forall (s :: * -> *) i x w (z :: * -> *).
(PermutableSequence s i x, Entity x, Entity i, Show w) =>
N
-> z i -> (w -> w -> Ordering) -> (x -> w) -> X (s x) -> Statement
prpPermutableSequence N
15 Proxy N
nProxy Symbol -> Symbol -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Symbol -> Symbol
forall x. x -> x
id X (PSequence N Symbol)
xpxs
      , N
-> Proxy N
-> (Symbol -> Symbol -> Ordering)
-> (Symbol -> Symbol)
-> X (CSequence Symbol)
-> Statement
forall (s :: * -> *) i x w (z :: * -> *).
(PermutableSequence s i x, Entity x, Entity i, Show w) =>
N
-> z i -> (w -> w -> Ordering) -> (x -> w) -> X (s x) -> Statement
prpPermutableSequence N
10 Proxy N
nProxy Symbol -> Symbol -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Symbol -> Symbol
forall x. x -> x
id X (CSequence Symbol)
xpsy
      ] where
  xxs :: X [N]
xxs = N -> N -> X N
xNB N
0 N
10 X N -> (N -> X [N]) -> X [N]
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \N
n -> N -> X N -> X [N]
forall x. N -> X x -> X [x]
xTakeN N
n (N -> N -> X N
xNB N
0 N
20)
  xpxs :: X (PSequence N Symbol)
xpxs = N -> N -> X Symbol -> X N -> X (PSequence N Symbol)
forall i x. Ord i => N -> N -> X x -> X i -> X (PSequence i x)
xPSequence N
20 N
40 (X Symbol
forall x. XStandard x => X x
xStandard :: X Symbol) (N -> N -> X N
xNB N
0 N
200)
  xpsy :: X (CSequence Symbol)
xpsy = N -> X Symbol -> X (CSequence Symbol)
forall x. Entity x => N -> X x -> X (CSequence x)
xCSequence N
20 (X Symbol
forall x. XStandard x => X x
xStandard :: X Symbol)