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

    -- * Form
  , PermutationForm(..), pmf

    -- * X
  , xPermutation, xPermutationB, xPermutationN
  , xMltPermutation

    -- * Propositions
  , prpPermutation
  , prpPermutableSequence
  , prpOprPermutation
  ) where

import Control.Monad hiding (sequence)

import Data.List (map,filter,zip,repeat,(++),head,tail,splitAt)
import Data.Foldable
import Data.Proxy

import OAlg.Prelude

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
import OAlg.Entity.Sequence.PSequence
import OAlg.Entity.Sequence.CSequence
import OAlg.Entity.Sequence.Set

import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative
import OAlg.Structure.Additive
import OAlg.Structure.Exponential
import OAlg.Structure.Operational

--------------------------------------------------------------------------------
-- 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
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
showList :: [PermutationForm i] -> ShowS
$cshowList :: forall i. Show i => [PermutationForm i] -> ShowS
show :: PermutationForm i -> String
$cshow :: forall i. Show i => PermutationForm i -> String
showsPrec :: Int -> PermutationForm i -> ShowS
$cshowsPrec :: forall i. Show i => Int -> PermutationForm i -> ShowS
Show,PermutationForm i -> PermutationForm i -> Bool
forall i. Eq i => PermutationForm i -> PermutationForm i -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PermutationForm i -> PermutationForm i -> Bool
$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
Eq,PermutationForm i -> N
forall i. PermutationForm i -> N
forall x. (x -> N) -> LengthN x
lengthN :: PermutationForm i -> N
$clengthN :: forall i. 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) = 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 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) = forall i. PSequence i i -> PermutationForm i
PermutationForm PSequence i i
kis where
  kis :: PSequence i i
kis = forall i x. [(x, i)] -> PSequence i x
PSequence forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall b a. Ord b => [(a, b)] -> [(a, b)]
sortSnd forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ (forall i x. PSequence i x -> [(x, i)]
psqxs PSequence i i
kjs forall {a}. Ord a => [(a, a)] -> [(a, a)] -> [(a, a)]
* forall a b. Ord a => [(a, b)] -> [(a, b)]
sortFst (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 forall a. Ord a => a -> a -> Ordering
`compare` a
j' of
    Ordering
LT -> (a
k,a
j)forall a. a -> [a] -> [a]
:([(a, a)]
kjs' [(a, a)] -> [(a, a)] -> [(a, a)]
* [(a, a)]
jis)
    Ordering
EQ -> (a
k,a
i)forall a. a -> [a] -> [a]
:([(a, a)]
kjs' [(a, a)] -> [(a, a)] -> [(a, a)]
* [(a, a)]
jis')
    Ordering
GT -> (a
j',a
i)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) = forall i x. [(x, i)] -> PSequence i x
PSequence (forall b a. Ord b => [(a, b)] -> [(a, b)]
sortSnd [(x, i)]
xis forall a. [a] -> [a] -> [a]
++ [(x, i)]
xis') where
  ([(x, i)]
xis,[(x, i)]
xis') = forall i x. PSequence i x -> [(x, i)]
psqxs PSequence i x
xjs forall {b} {a}.
Ord b =>
[(a, b)] -> [(b, b)] -> ([(a, b)], [(a, b)])
* forall a b. Ord a => [(a, b)] -> [(a, b)]
sortFst (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 forall a. Ord a => a -> a -> Ordering
`compare` b
j' of
    Ordering
LT -> ((a
x,b
j)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)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') '<=' u@ - where @(_,u) = '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 = forall a b. Projectible a b => b -> a
prj (PSequence N x
xs' forall i x.
Ord i =>
PSequence i x -> PermutationForm i -> PSequence i x
`pmfOprPsq` PermutationForm N
p) where
  xs' :: PSequence N x
xs' = (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 = forall x. Constructable x => Form x -> x
make forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall r a. Semiring r => Point a -> Word r a -> ProductForm r a
wrdprf () forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall r a. [(a, r)] -> Word r a
Word forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall u. Span N -> N -> WordN u -> PermutationForm N -> WordN u
opr (forall (s :: * -> *) i x (p :: * -> *).
Sequence s i x =>
p i -> s x -> Span i
span (forall a. a -> Maybe a
Just (N
0::N)) PermutationForm N
p) N
0 (forall r a. Word r a -> [(a, r)]
fromWord forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ 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) = (forall a. N -> [a] -> [a]
takeN N
l forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. a -> [a]
repeat u
u) 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 (Closer N
l,Closer N
h) N
_ WordN u
w PermutationForm N
_ | Closer N
h forall a. Ord a => a -> a -> Bool
<= Closer N
l         = WordN u
w -- empty span
  opr Span N
_ N
_ [] PermutationForm N
_                     = []
  opr (Closer N
l,Closer N
h) N
k ((u, N)
w:WordN u
ws) PermutationForm N
p | forall x. x -> Closer x
It N
k' forall a. Ord a => a -> a -> Bool
< Closer N
l = (u, N)
w forall a. a -> [a] -> [a]
: forall u. Span N -> N -> WordN u -> PermutationForm N -> WordN u
opr (Closer N
l,Closer N
h) N
k' WordN u
ws PermutationForm N
p
                        | Closer N
h forall a. Ord a => a -> a -> Bool
< forall x. x -> Closer x
It N
k' = (u, N)
wforall a. a -> [a] -> [a]
:WordN u
ws -- see the note below
                        | Bool
otherwise = forall u.
Closer N
-> N -> [(u, N)] -> [(u, N)] -> PermutationForm N -> [(u, N)]
opr' Closer N
h N
k [] ((u, N)
wforall a. a -> [a] -> [a]
:WordN u
ws) PermutationForm N
p
    where k' :: N
k' = N
k forall a. Additive a => a -> a -> a
+ 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' :: Closer N -> N -> [(u,I)] -> WordN u -> PermutationForm N -> WordN u
  opr' :: forall u.
Closer N
-> N -> [(u, N)] -> [(u, N)] -> PermutationForm N -> [(u, N)]
opr' Closer N
_ N
_ [(u, N)]
uis [] PermutationForm N
p            = forall u. PSequence N u -> PermutationForm N -> WordN u
opr'' (forall i x. [(x, i)] -> PSequence i x
PSequence [(u, N)]
uis) PermutationForm N
p
  opr' Closer N
h N
k [(u, N)]
uis [(u, N)]
ws PermutationForm N
p | Closer N
h forall a. Ord a => a -> a -> Bool
< forall x. x -> Closer x
It N
k = forall u. PSequence N u -> PermutationForm N -> WordN u
opr'' (forall i x. [(x, i)] -> PSequence i x
PSequence [(u, N)]
uis) PermutationForm N
p forall a. [a] -> [a] -> [a]
++ [(u, N)]
ws
  opr' Closer N
h N
k [(u, N)]
uis ((u, N)
w:[(u, N)]
ws) PermutationForm N
p        = forall u.
Closer N
-> N -> [(u, N)] -> [(u, N)] -> PermutationForm N -> [(u, N)]
opr' Closer N
h (N
kforall a. Additive a => a -> a -> a
+forall a b. (a, b) -> b
snd (u, N)
w) ([(u, N)]
uis forall a. [a] -> [a] -> [a]
++ 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 = forall a b. (a -> b) -> [a] -> [b]
map (\(u
u,N
_) -> (u
u,N
1)) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall i x. PSequence i x -> [(x, i)]
psqxs forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ (PSequence N u
uis 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) = (forall i x. [(x, i)] -> PSequence i x
PSequence [(x, i)]
xjs',forall i. PSequence i i -> PermutationForm i
PermutationForm (forall i x. [(x, i)] -> PSequence i x
PSequence [(i, i)]
jis)) where
  wjxs :: [((w, i), x)]
wjxs = forall a b. (a -> a -> Ordering) -> [(a, b)] -> [(a, b)]
sortFstBy (w, i) -> (w, i) -> Ordering
cmp forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ 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   = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(x, i)]
xjs
  xjs' :: [(x, i)]
xjs' = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [((w, i), x)]
wjxs forall a b. [a] -> [b] -> [(a, b)]
`zip` [i]
js
  jis :: [(i, i)]
jis  = forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> b
sndforall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
.forall a b. (a, b) -> a
fst) [((w, i), x)]
wjxs forall a b. [a] -> [b] -> [(a, b)]
`zip` [i]
js

  cmp :: (w, i) -> (w, i) -> Ordering
cmp = forall a b.
(a -> a -> Ordering)
-> (b -> b -> Ordering) -> (a, b) -> (a, b) -> Ordering
compare2 w -> w -> Ordering
wcmp 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 = (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall i x. PSequence i x -> [(x, i)]
psqxs forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ PSequence N x
xs',PermutationForm N
p) where
  (PSequence N x
xs',PermutationForm N
p) = 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 (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 = (forall x. Entity x => [x] -> ProductSymbol x
productSymbol [x]
xs',PermutationForm N
p) where
  ([x]
xs',PermutationForm N
p) = forall w x.
(w -> w -> Ordering) -> (x -> w) -> [x] -> ([x], PermutationForm N)
pmfLst w -> w -> Ordering
wcmp x -> w
w (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 [ forall a. Validable a => a -> Statement
valid PSequence i i
jis
        , String -> Label
Label String
"1" Label -> Statement -> Statement
:<=>: (forall (s :: * -> *) i x (p :: * -> *).
Sequence s i x =>
p i -> s x -> Set i
support PSequence i i
jis PermutationForm i
p forall a. Eq a => a -> a -> Bool
== 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
:=forall a. Show a => a -> String
show PermutationForm i
p]
        ]

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

--------------------------------------------------------------------------------
-- PermutationForm - Oriented -

instance (Entity i, Ord i) => Oriented (PermutationForm i) where
  type Point (PermutationForm i) = ()
  orientation :: PermutationForm i -> Orientation (Point (PermutationForm i))
orientation = forall b a. b -> a -> b
const (()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)) = forall i. PSequence i i -> PermutationForm i
PermutationForm (forall i x. [(x, i)] -> PSequence i x
PSequence [(i, i)]
jis') where
    jis' :: [(i, i)]
jis' = forall a. (a -> Bool) -> [a] -> [a]
filter (\(i
j,i
i) -> i
j 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
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
showList :: [Permutation i] -> ShowS
$cshowList :: forall i. Show i => [Permutation i] -> ShowS
show :: Permutation i -> String
$cshow :: forall i. Show i => Permutation i -> String
showsPrec :: Int -> Permutation i -> ShowS
$cshowsPrec :: forall i. Show i => Int -> Permutation i -> ShowS
Show,Permutation i -> Permutation i -> Bool
forall i. Eq i => Permutation i -> Permutation i -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Permutation i -> Permutation i -> Bool
$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
Eq,Permutation i -> Statement
forall i. (Entity i, Ord i) => Permutation i -> Statement
forall a. (a -> Statement) -> Validable a
valid :: Permutation i -> Statement
$cvalid :: forall i. (Entity i, Ord i) => Permutation i -> Statement
Validable,forall a. Show a -> Eq a -> Validable a -> Typeable a -> Entity a
forall {i}. (Entity i, Ord i) => Eq (Permutation i)
forall {i}. (Entity i, Ord i) => Show (Permutation i)
forall {i}. (Entity i, Ord i) => Typeable (Permutation i)
forall i. (Entity i, Ord i) => Validable (Permutation i)
Entity,Permutation i -> N
forall i. Permutation i -> N
forall x. (x -> N) -> LengthN x
lengthN :: Permutation i -> N
$clengthN :: forall i. 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) = PermutationForm i
f

instance Eq i => Constructable (Permutation i) where
  make :: Form (Permutation i) -> Permutation i
make Form (Permutation i)
f = forall i. PermutationForm i -> Permutation i
Permutation forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall e. Reducible e => e -> e
reduce Form (Permutation 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) = 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 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 = forall x y. Exposable x => (Form x -> y) -> x -> y
restrict forall i. Ord i => PermutationForm i -> i -> i
pmf

--------------------------------------------------------------------------------
-- Permutation - Cayleyan -

instance (Entity i, Ord i) => Oriented (Permutation i) where
  type Point (Permutation i) = ()
  orientation :: Permutation i -> Orientation (Point (Permutation i))
orientation = forall x y. Exposable x => (Form x -> y) -> x -> y
restrict 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)
_ = forall x. Constructable x => Form x -> x
make (forall i. PSequence i i -> PermutationForm i
PermutationForm forall i x. PSequence i x
psqEmpty)
  Permutation PermutationForm i
f * :: Permutation i -> Permutation i -> Permutation i
* Permutation PermutationForm i
g = forall x. Constructable x => Form x -> x
make (PermutationForm i
f forall i.
Ord i =>
PermutationForm i -> PermutationForm i -> PermutationForm i
`pmfMlt` PermutationForm i
g)

instance Total (Permutation i)

instance (Entity i, Ord i) => Invertible (Permutation i) where
  tryToInvert :: Permutation i -> Solver (Permutation i)
tryToInvert (Permutation (PermutationForm (PSequence [(i, i)]
jis)))
    = forall (m :: * -> *) a. Monad m => a -> m a
return (forall i. PermutationForm i -> Permutation i
Permutation (forall i. PSequence i i -> PermutationForm i
PermutationForm (forall i x. [(x, i)] -> PSequence i x
PSequence [(i, i)]
ijs)))
    where ijs :: [(i, i)]
ijs = forall b a. Ord b => [(a, b)] -> [(a, b)]
sortSnd forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ 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
(^) = 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 forall a. Ord a => a -> a -> Ordering
`compare` i
j of
  Ordering
LT -> forall x. Constructable x => Form x -> x
make (forall i. PSequence i i -> PermutationForm i
PermutationForm (forall i x. [(x, i)] -> PSequence i x
PSequence [(i
j,i
i),(i
i,i
j)]))
  Ordering
EQ -> forall c. Multiplicative c => Point c -> c
one ()
  Ordering
GT -> 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 = forall (s :: * -> *) i x (p :: * -> *) w.
PermutableSequence s i x =>
p i
-> (w -> w -> Ordering) -> (x -> w) -> s x -> (s x, Permutation i)
permuteBy (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 = forall i x.
Ord i =>
PSequence i x -> PermutationForm i -> PSequence i x
pmfOprPsq PSequence i x
xs (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',forall x. Constructable x => Form x -> x
make PermutationForm i
p) where (PSequence i x
xs',PermutationForm i
p) = 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 = forall x. [x] -> PermutationForm N -> [x]
pmfOprLst [x]
xs (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',forall x. Constructable x => Form x -> x
make PermutationForm N
p) where ([x]
xs',PermutationForm N
p) = 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 = forall x.
Entity x =>
CSequence x -> PermutationForm N -> CSequence x
pmfOprPsy CSequence x
xs (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',forall x. Constructable x => Form x -> x
make PermutationForm N
p) where (CSequence x
xs',PermutationForm N
p) = 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
(<*) = 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))
    = (forall x. Constructable x => Form x -> x
make (forall i. PSequence i i -> PermutationForm i
PermutationForm PSequence i i
p'),Permutation i
q) where (PSequence i i
p',Permutation i
q) = 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

--------------------------------------------------------------------------------
-- 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= N -> Permutation i -> N -> X (Permutation i)
pmt N
0 (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 forall a. Ord a => a -> a -> Bool
<= N
k = 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) <- 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 (forall a. Enum a => a -> a
succ N
k) (Permutation i
pforall c. Multiplicative c => c -> c -> c
*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' <- forall {a}. Int -> [a] -> X [a]
xp (forall (t :: * -> *) a. Foldable t => t a -> Int
length [i]
is) [i]
is
  forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x. Constructable x => Form x -> x
make forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall i. PSequence i i -> PermutationForm i
PermutationForm forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall i x. [(x, i)] -> PSequence i x
PSequence ([i]
is' forall a b. [a] -> [b] -> [(a, b)]
`zip` [i]
is)
  where
    is :: [i]
is = 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 forall a. Ord a => a -> a -> Bool
<= Int
1    = 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 forall a. Eq a => a -> a -> Bool
== Int
l
        then forall (m :: * -> *) a. Monad m => a -> m a
return [a]
is
        else let ([a]
is',[a]
is'') = forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [a]
is in do
          [a]
is''' <- Int -> [a] -> X [a]
xp (forall a. Enum a => a -> a
pred Int
l) ([a]
is' forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [a]
tail [a]
is'')
          forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. [a] -> a
head [a]
is''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 = forall (m :: * -> *) a. Monad m => a -> m a
return (forall c. Multiplicative c => Point c -> c
one ())
xPermutationN N
n = forall i. (Ord i, Enum i) => i -> i -> X (Permutation i)
xPermutationB N
0 (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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall x. (Show x, Ord x) => Int -> X x -> Omega -> IO ()
putDistribution Int
n (forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (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 = forall c. Singleton (Point c) => X N -> X c -> XMlt c
xMltTtl (N -> N -> X N
xNB N
0 N
10) (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 forall f x. Opr f x => x -> f -> x
<* Permutation i
p forall a. Eq a => a -> a -> Bool
== 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 (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
:=forall a. Show a => a -> String
show s x
xs,String
"p"String -> String -> Parameter
:=forall a. Show a => a -> String
show Permutation i
p] where
  is :: Set i
is = forall y x. Ord y => (x -> y) -> Set x -> Set y
setMap (forall i. Ord i => Permutation i -> i -> i
pmt Permutation i
p') forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ 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' = 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
:<=>: forall x. X x -> (x -> Statement) -> Statement
Forall  X ([x], Permutation N)
xxsp (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (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 = 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
:<=>: forall x. X x -> (x -> Statement) -> Statement
Forall (forall a b. X a -> X b -> X (a, b)
xTupple2 X (PSequence i x)
xxs X (Permutation i)
xp) (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (forall i (s :: * -> *) x (p :: * -> *).
(TotalOpr (Permutation i) (s x), ConstructableSequence s i x) =>
p i -> s x -> Permutation i -> Statement
relOprPermutation (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)
_ = 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
:<=>: forall x. X x -> (x -> Statement) -> Statement
Forall (forall a b. X a -> X b -> X (a, b)
xTupple2 X (ProductSymbol x)
xxs X (Permutation N)
xp) (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (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 = 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 = 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \N
n -> forall x. N -> X x -> X [x]
xTakeN N
n (forall x. XStandard x => X x
xStandard :: X Symbol)

  prpPsy :: Statement
prpPsy = 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 = forall x. Entity x => N -> X x -> X (CSequence x)
xCSequence N
20 (forall x. XStandard x => X x
xStandard :: X Symbol)
    
  prpPsq :: Statement
prpPsq = 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 = forall i x. Ord i => N -> N -> X x -> X i -> X (PSequence i x)
xPSequence N
20 N
40 (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]
_  -> forall x. X x -> (x -> Statement) -> Statement
Forall X (Permutation i, i)
xpi (\(Permutation i
p,i
i)
                    -> ((s x
xsforall f x. Opr f x => x -> f -> x
<*Permutation i
p)forall (s :: * -> *) i x. Sequence s i x => s x -> i -> Maybe x
??i
i forall a. Eq a => a -> a -> Bool
== ((s x
xsforall (s :: * -> *) i x. Sequence s i x => s x -> i -> Maybe x
??) forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. 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
:=forall a. Show a => a -> String
show s x
xs,String
"p"String -> String -> Parameter
:=forall a. Show a => a -> String
show Permutation i
p,String
"i"String -> String -> Parameter
:=forall a. Show a => a -> String
show i
i]
                   )
  where
    Set [i]
is = 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 = forall a. [a] -> X a
xOneOf [i]
is
    xp :: X (Permutation i)
xp = forall i. (Entity i, Ord i) => N -> X i -> X (Permutation i)
xPermutation N
n X i
xi
    xpi :: X (Permutation i, i)
xpi = 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) = 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' forall a. Eq a => a -> a -> Bool
== s x
xs forall f x. Opr f x => x -> f -> x
<* Permutation i
p) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"xs"String -> String -> Parameter
:=forall a. Show a => a -> String
show s x
xs,String
"p"String -> String -> Parameter
:=forall a. Show a => a -> String
show Permutation i
p]
      , String -> Label
Label String
"2" Label -> Statement -> Statement
:<=>: [x] -> Statement
increasing (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ 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
:<=>: (forall (s :: * -> *) i x (p :: * -> *).
(Sequence s i x, Ord x) =>
p i -> s x -> Set x
image z i
z Permutation i
p forall a. POrd a => a -> a -> Bool
<<= 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
:=forall a. Show a => a -> String
show s x
xs,String
"p"String -> String -> Parameter
:=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
:=forall a. Show a => a -> String
show N
i,String
"(wx,wy)"String -> String -> Parameter
:=forall a. Show a => a -> String
show (w
wx,w
wy)]
          , N -> w -> [x] -> Statement
inc (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
:<=>: forall x. X x -> (x -> Statement) -> Statement
Forall X (s x)
xxs (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
:<=>: forall x. X x -> (x -> Statement) -> Statement
Forall X (s x)
xxs (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 [ forall c. Multiplicative c => XMlt c -> Statement
prpMlt (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
      , 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 forall a. Ord a => a -> a -> Ordering
compare forall x. x -> x
id X [N]
xxs
      , 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 forall a. Ord a => a -> a -> Ordering
compare forall x. x -> x
id X (PSequence N Symbol)
xpxs
      , 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 forall a. Ord a => a -> a -> Ordering
compare forall x. x -> x
id X (CSequence Symbol)
xpsy
      ] where
  xxs :: X [N]
xxs = N -> N -> X N
xNB N
0 N
10 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \N
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 = forall i x. Ord i => N -> N -> X x -> X i -> X (PSequence i x)
xPSequence N
20 N
40 (forall x. XStandard x => X x
xStandard :: X Symbol) (N -> N -> X N
xNB N
0 N
200)
  xpsy :: X (CSequence Symbol)
xpsy = forall x. Entity x => N -> X x -> X (CSequence x)
xCSequence N
20 (forall x. XStandard x => X x
xStandard :: X Symbol)