{-# LANGUAGE NoImplicitPrelude #-}

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

-- |
-- Module      : OAlg.Entity.Sequence.PSequence
-- Description : partially defined sequences
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
-- 
-- partially defined sequences of items in @__x__@ with a totally ordered index type @__i__@.
module OAlg.Entity.Sequence.PSequence
  ( -- * Sequence
    PSequence(..), iProxy
  , psqSpan
  , psqEmpty, psqIsEmpty, psqxs, psequence
  , psqHead, psqTail
  , psqMap, psqMapShift
  , psqFilter
  , psqSplitWhile
  , psqInterlace
  , psqCompose
  , psqAppend
  , psqShear
  , psqSwap

    -- * X
  , xPSequence
  ) where

import Control.Monad 

import Data.Foldable
import Data.Typeable

import Data.List (map,sortBy,groupBy,filter,head,tail,(++),zip)

import OAlg.Prelude

import OAlg.Data.Canonical

import OAlg.Structure.Additive
import OAlg.Structure.Number

import OAlg.Entity.Sequence.Definition
import OAlg.Entity.Sequence.Set

--------------------------------------------------------------------------------
-- PSequence -

-- | partially defined sequences @(x0,i0),(x1,i1)..@ of index items in @__x__@ with a
-- totally ordered index type @__i__@.
--
-- __Property__ Let @'PSequence' xis@ be in @'PSequence' __i__ __x__@ then holds:
-- @i '<' j@ for all @..(_,i)':'(_,j)..@ in @xis@.
--
--  __Examples__
--
-- >>> PSequence [('a',3),('b',7),('c',12)] :: PSequence N Char
-- PSequence [('a',3),('b',7),('c',12)]
--
-- and
--
-- >>> validate (valid (PSequence [('a',3),('b',7),('c',12)] :: PSequence N Char))
-- Valid
--
-- but
--
-- >>> validate (valid (PSequence [('a',3),('b',15),('c',12)] :: PSequence N Char))
-- Invalid
--
-- as 'Char' is a totally ordered type it can serve as index type
--
-- >>> validate (valid (PSequence [(12,'c'),(3,'e'),(8,'x')] :: PSequence Char Z))
-- Valid
--
-- and they admit a total right operation 'OAlg.Structure.Operational.<*' of
-- @t'OAlg.Entity.Sequence.Permutation.Permutation' __i__@
--
-- >>> (PSequence [(12,'c'),(3,'e'),(8,'x')] :: PSequence Char Z) <* pmtSwap 'e' 'x'
-- PSequence [(12,'c'),(8,'e'),(3,'x')]
--
--
--  __Note__ As we keep the constructor public, it is crucial for there further use to
--  ensure that they are 'valid'!
newtype PSequence i x = PSequence [(x,i)] deriving (Int -> PSequence i x -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall i x. (Show x, Show i) => Int -> PSequence i x -> ShowS
forall i x. (Show x, Show i) => [PSequence i x] -> ShowS
forall i x. (Show x, Show i) => PSequence i x -> String
showList :: [PSequence i x] -> ShowS
$cshowList :: forall i x. (Show x, Show i) => [PSequence i x] -> ShowS
show :: PSequence i x -> String
$cshow :: forall i x. (Show x, Show i) => PSequence i x -> String
showsPrec :: Int -> PSequence i x -> ShowS
$cshowsPrec :: forall i x. (Show x, Show i) => Int -> PSequence i x -> ShowS
Show,PSequence i x -> PSequence i x -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall i x. (Eq x, Eq i) => PSequence i x -> PSequence i x -> Bool
/= :: PSequence i x -> PSequence i x -> Bool
$c/= :: forall i x. (Eq x, Eq i) => PSequence i x -> PSequence i x -> Bool
== :: PSequence i x -> PSequence i x -> Bool
$c== :: forall i x. (Eq x, Eq i) => PSequence i x -> PSequence i x -> Bool
Eq,PSequence i x -> PSequence i x -> Bool
PSequence i x -> PSequence i x -> Ordering
PSequence i x -> PSequence i x -> PSequence i x
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} {x}. (Ord x, Ord i) => Eq (PSequence i x)
forall i x.
(Ord x, Ord i) =>
PSequence i x -> PSequence i x -> Bool
forall i x.
(Ord x, Ord i) =>
PSequence i x -> PSequence i x -> Ordering
forall i x.
(Ord x, Ord i) =>
PSequence i x -> PSequence i x -> PSequence i x
min :: PSequence i x -> PSequence i x -> PSequence i x
$cmin :: forall i x.
(Ord x, Ord i) =>
PSequence i x -> PSequence i x -> PSequence i x
max :: PSequence i x -> PSequence i x -> PSequence i x
$cmax :: forall i x.
(Ord x, Ord i) =>
PSequence i x -> PSequence i x -> PSequence i x
>= :: PSequence i x -> PSequence i x -> Bool
$c>= :: forall i x.
(Ord x, Ord i) =>
PSequence i x -> PSequence i x -> Bool
> :: PSequence i x -> PSequence i x -> Bool
$c> :: forall i x.
(Ord x, Ord i) =>
PSequence i x -> PSequence i x -> Bool
<= :: PSequence i x -> PSequence i x -> Bool
$c<= :: forall i x.
(Ord x, Ord i) =>
PSequence i x -> PSequence i x -> Bool
< :: PSequence i x -> PSequence i x -> Bool
$c< :: forall i x.
(Ord x, Ord i) =>
PSequence i x -> PSequence i x -> Bool
compare :: PSequence i x -> PSequence i x -> Ordering
$ccompare :: forall i x.
(Ord x, Ord i) =>
PSequence i x -> PSequence i x -> Ordering
Ord,PSequence i x -> N
forall x. (x -> N) -> LengthN x
forall i x. PSequence i x -> N
lengthN :: PSequence i x -> N
$clengthN :: forall i x. PSequence i x -> N
LengthN,forall a. PSequence i a -> Bool
forall i a. Eq a => a -> PSequence i a -> Bool
forall i a. Num a => PSequence i a -> a
forall i a. Ord a => PSequence i a -> a
forall m a. Monoid m => (a -> m) -> PSequence i a -> m
forall i m. Monoid m => PSequence i m -> m
forall i a. PSequence i a -> Bool
forall i a. PSequence i a -> Int
forall i a. PSequence i a -> [a]
forall a b. (a -> b -> b) -> b -> PSequence i a -> b
forall i a. (a -> a -> a) -> PSequence i a -> a
forall i m a. Monoid m => (a -> m) -> PSequence i a -> m
forall i b a. (b -> a -> b) -> b -> PSequence i a -> b
forall i a b. (a -> b -> b) -> b -> PSequence i a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => PSequence i a -> a
$cproduct :: forall i a. Num a => PSequence i a -> a
sum :: forall a. Num a => PSequence i a -> a
$csum :: forall i a. Num a => PSequence i a -> a
minimum :: forall a. Ord a => PSequence i a -> a
$cminimum :: forall i a. Ord a => PSequence i a -> a
maximum :: forall a. Ord a => PSequence i a -> a
$cmaximum :: forall i a. Ord a => PSequence i a -> a
elem :: forall a. Eq a => a -> PSequence i a -> Bool
$celem :: forall i a. Eq a => a -> PSequence i a -> Bool
length :: forall a. PSequence i a -> Int
$clength :: forall i a. PSequence i a -> Int
null :: forall a. PSequence i a -> Bool
$cnull :: forall i a. PSequence i a -> Bool
toList :: forall a. PSequence i a -> [a]
$ctoList :: forall i a. PSequence i a -> [a]
foldl1 :: forall a. (a -> a -> a) -> PSequence i a -> a
$cfoldl1 :: forall i a. (a -> a -> a) -> PSequence i a -> a
foldr1 :: forall a. (a -> a -> a) -> PSequence i a -> a
$cfoldr1 :: forall i a. (a -> a -> a) -> PSequence i a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> PSequence i a -> b
$cfoldl' :: forall i b a. (b -> a -> b) -> b -> PSequence i a -> b
foldl :: forall b a. (b -> a -> b) -> b -> PSequence i a -> b
$cfoldl :: forall i b a. (b -> a -> b) -> b -> PSequence i a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> PSequence i a -> b
$cfoldr' :: forall i a b. (a -> b -> b) -> b -> PSequence i a -> b
foldr :: forall a b. (a -> b -> b) -> b -> PSequence i a -> b
$cfoldr :: forall i a b. (a -> b -> b) -> b -> PSequence i a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> PSequence i a -> m
$cfoldMap' :: forall i m a. Monoid m => (a -> m) -> PSequence i a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> PSequence i a -> m
$cfoldMap :: forall i m a. Monoid m => (a -> m) -> PSequence i a -> m
fold :: forall m. Monoid m => PSequence i m -> m
$cfold :: forall i m. Monoid m => PSequence i m -> m
Foldable)

instance Embeddable [x] (PSequence N x) where
  inj :: [x] -> PSequence N x
inj [x]
xs = forall i x. [(x, i)] -> PSequence i x
PSequence ([x]
xs forall a b. [a] -> [b] -> [(a, b)]
`zip` [N
0..])

instance Projectible [x] (PSequence N x) where
  prj :: PSequence N x -> [x]
prj (PSequence [(x, N)]
xis) = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(x, N)]
xis
  
--------------------------------------------------------------------------------
-- psqxs -

-- | the underlying list of indexed values.
psqxs :: PSequence i x -> [(x,i)]
psqxs :: forall i x. PSequence i x -> [(x, i)]
psqxs (PSequence [(x, i)]
xs) = [(x, i)]
xs

--------------------------------------------------------------------------------
-- psqSqc -

-- | @'psqSqc' f is@ maps the index set @is@ according to @f@ and strips out all 'Nothing'
--   items.
psqSqc :: (i -> Maybe x) -> Set i -> PSequence i x
psqSqc :: forall i x. (i -> Maybe x) -> Set i -> PSequence i x
psqSqc i -> Maybe x
mx (Set [i]
is)
  = forall i x. [(x, i)] -> PSequence i x
PSequence
  forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\(Maybe x
mx,i
i) -> (forall a. HasCallStack => Maybe a -> a
fromJust Maybe x
mx,i
i))
  forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Maybe a -> Bool
isJust forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall a b. (a, b) -> a
fst)
  forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\i
i -> (i -> Maybe x
mx i
i,i
i)) [i]
is

--------------------------------------------------------------------------------
-- PSequence - Sequence -

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

instance (Entity x, Entity i, Ord i) => ConstructableSequence (PSequence i) i x where
  sequence :: (i -> Maybe x) -> Set i -> PSequence i x
sequence = forall i x. (i -> Maybe x) -> Set i -> PSequence i x
psqSqc
  
--------------------------------------------------------------------------------
-- psqFromMap -

-- | constructs a partially defined sequence according to the given map and the bounds.
psqFromMap :: (Enum i, Ord i) => i -> Closer i -> (i -> Maybe x) -> PSequence i x
psqFromMap :: forall i x.
(Enum i, Ord i) =>
i -> Closer i -> (i -> Maybe x) -> PSequence i x
psqFromMap i
i0 Closer i
h i -> Maybe x
f
  = forall i x. [(x, i)] -> PSequence i x
PSequence
  forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\(Maybe x
mx,i
i) -> (forall a. HasCallStack => Maybe a -> a
fromJust Maybe x
mx,i
i)) 
  forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Maybe a -> Bool
isJust forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall a b. (a, b) -> a
fst)
  forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\i
i -> (i -> Maybe x
f i
i,i
i))
  forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall i. (Enum i, Ord i) => i -> Closer i -> [i]
enumSpan i
i0 Closer i
h


--------------------------------------------------------------------------------
-- iProxy -

-- | proxy of the second type valiable @__i__@.
iProxy :: s i x -> Proxy i
iProxy :: forall (s :: * -> * -> *) i x. s i x -> Proxy i
iProxy s i x
_ = forall {k} (t :: k). Proxy t
Proxy
  
--------------------------------------------------------------------------------
-- psqSpan -

-- | the span.
psqSpan :: Ord i => PSequence i x -> Span i
psqSpan :: forall i x. Ord i => PSequence i x -> Span i
psqSpan (PSequence [(x, i)]
xs) = forall x. Ord x => [x] -> Span x
cspan forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(x, i)]
xs

--------------------------------------------------------------------------------
-- psqEmpty -

-- | the empty partially defined sequence.
psqEmpty :: PSequence i x
psqEmpty :: forall i x. PSequence i x
psqEmpty = forall i x. [(x, i)] -> PSequence i x
PSequence []

--------------------------------------------------------------------------------
-- psqIsEmpty -

-- | checks of being empty.
psqIsEmpty :: PSequence i x -> Bool
psqIsEmpty :: forall i a. PSequence i a -> Bool
psqIsEmpty (PSequence []) = Bool
True
psqIsEmpty PSequence i x
_              = Bool
False

--------------------------------------------------------------------------------
-- psqMap -

-- | maps the entries, where the indices are preserved.
psqMap :: (x -> y) -> PSequence i x -> PSequence i y
psqMap :: forall x y i. (x -> y) -> PSequence i x -> PSequence i y
psqMap x -> y
f (PSequence [(x, i)]
xis) = forall i x. [(x, i)] -> PSequence i x
PSequence forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\(x
x,i
i) -> (x -> y
f x
x,i
i)) [(x, i)]
xis

instance Functor (PSequence i) where fmap :: forall a b. (a -> b) -> PSequence i a -> PSequence i b
fmap = forall x y i. (x -> y) -> PSequence i x -> PSequence i y
psqMap
  
--------------------------------------------------------------------------------
-- psqMapShift -

-- | maps and shifts a partial sequence.
psqMapShift :: Number i => i -> ((x,i) -> y) -> PSequence i x -> PSequence i y
psqMapShift :: forall i x y.
Number i =>
i -> ((x, i) -> y) -> PSequence i x -> PSequence i y
psqMapShift i
o (x, i) -> y
f (PSequence [(x, i)]
xs) = forall i x. [(x, i)] -> PSequence i x
PSequence forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (x, i) -> (y, i)
f' [(x, i)]
xs where f' :: (x, i) -> (y, i)
f' (x, i)
xi = ((x, i) -> y
f (x, i)
xi,forall a b. (a, b) -> b
snd (x, i)
xi forall a. Additive a => a -> a -> a
+ i
o)

--------------------------------------------------------------------------------
-- PSequence - Entity -

relPSequence :: (Entity x, Entity i, Ord i) => PSequence i x -> Statement
relPSequence :: forall x i.
(Entity x, Entity i, Ord i) =>
PSequence i x -> Statement
relPSequence (PSequence [])       = Statement
SValid
relPSequence (PSequence ((x, i)
xi:[(x, i)]
xis)) = forall {a} {b} {t}.
(Validable a, Validable b, Ord b, Show t, Show b, Enum t) =>
t -> (a, b) -> [(a, b)] -> Statement
vld (N
0::N) (x, i)
xi [(x, i)]
xis where
    vld :: t -> (a, b) -> [(a, b)] -> Statement
vld t
_ (a, b)
xi [] = forall a. Validable a => a -> Statement
valid (a, b)
xi
    vld t
l xi :: (a, b)
xi@(a
_,b
i) (xj :: (a, b)
xj@(a
_,b
j):[(a, b)]
xis) = [Statement] -> Statement
And [ (b
iforall a. Ord a => a -> a -> Bool
<b
j)Bool -> Message -> Statement
:?>[Parameter] -> Message
Params [String
"l"String -> String -> Parameter
:=forall a. Show a => a -> String
show t
l,String
"(i,j)"String -> String -> Parameter
:=forall a. Show a => a -> String
show (b
i,b
j)]
                                        , forall a. Validable a => a -> Statement
valid (a, b)
xi
                                        , t -> (a, b) -> [(a, b)] -> Statement
vld (forall a. Enum a => a -> a
succ t
l) (a, b)
xj [(a, b)]
xis
                                        ]

instance (Entity x, Entity i, Ord i) => Validable (PSequence i x) where
  valid :: PSequence i x -> Statement
valid PSequence i x
xs = String -> Label
Label String
"PSequence" Label -> Statement -> Statement
:<=>: forall a. Validable a => a -> Statement
valid (forall (s :: * -> *) i x (p :: * -> *).
Sequence s i x =>
p i -> s x -> Graph i x
graph (forall (s :: * -> * -> *) i x. s i x -> Proxy i
iProxy PSequence i x
xs) PSequence i x
xs)

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

--------------------------------------------------------------------------------
-- psequence -

-- | the partial sequenc given by a aggregation function an a list of value index pairs,
--   which will be sorted and accordingly aggregated by thegiven aggregation function.
psequence :: Ord i => (x -> x -> x) -> [(x,i)] -> PSequence i x
psequence :: forall i x. Ord i => (x -> x -> x) -> [(x, i)] -> PSequence i x
psequence x -> x -> x
(+) [(x, i)]
xis = forall i x. [(x, i)] -> PSequence i x
PSequence
             forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall x i. (x -> x -> x) -> [(x, i)] -> (x, i)
aggrBy x -> x -> x
(+))
             forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (forall a. (a -> a -> Ordering) -> a -> a -> Bool
eql (forall i a. Ord i => (a -> i) -> a -> a -> Ordering
fcompare forall a b. (a, b) -> b
snd))
             forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (forall i a. Ord i => (a -> i) -> a -> a -> Ordering
fcompare forall a b. (a, b) -> b
snd)
             forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ [(x, i)]
xis where

  aggrBy :: (x -> x -> x) -> [(x,i)] -> (x,i)
  aggrBy :: forall x i. (x -> x -> x) -> [(x, i)] -> (x, i)
aggrBy x -> x -> x
(+) ((x
x,i
i):[(x, i)]
xis) = (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl x -> x -> x
(+) x
x (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(x, i)]
xis),i
i)

--------------------------------------------------------------------------------
-- psqHead -

-- | the head of a partial sequence.
psqHead :: PSequence i x -> (x,i)
psqHead :: forall i x. PSequence i x -> (x, i)
psqHead (PSequence [(x, i)]
xs) = forall a. [a] -> a
head [(x, i)]
xs

--------------------------------------------------------------------------------
-- psqTail -

-- | the tail.
psqTail :: PSequence i x -> PSequence i x
psqTail :: forall i x. PSequence i x -> PSequence i x
psqTail (PSequence [(x, i)]
xs) = forall i x. [(x, i)] -> PSequence i x
PSequence (forall a. [a] -> [a]
tail [(x, i)]
xs)

--------------------------------------------------------------------------------
-- psqFilter -

-- | filters the partially defiend sequence accordingly the given predicate.
psqFilter :: (x -> Bool) -> PSequence i x -> PSequence i x
psqFilter :: forall x i. (x -> Bool) -> PSequence i x -> PSequence i x
psqFilter x -> Bool
p (PSequence [(x, i)]
xis) = forall i x. [(x, i)] -> PSequence i x
PSequence forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (x, i) -> Bool
p' [(x, i)]
xis where
  p' :: (x, i) -> Bool
p' (x
x,i
_) = x -> Bool
p x
x

--------------------------------------------------------------------------------
-- psqInterlace -

-- | interlaces the tow partially defined sequences according to the given mappings.
psqInterlace :: Ord i
  => (x -> y -> z) -> (x -> z) -> (y -> z)
  -> PSequence i x -> PSequence i y -> PSequence i z
psqInterlace :: forall i x y z.
Ord i =>
(x -> y -> z)
-> (x -> z)
-> (y -> z)
-> PSequence i x
-> PSequence i y
-> PSequence i z
psqInterlace x -> y -> z
(+) x -> z
xz y -> z
yz (PSequence [(x, i)]
xis) (PSequence [(y, i)]
yjs) = forall i x. [(x, i)] -> PSequence i x
PSequence ([(x, i)] -> [(y, i)] -> [(z, i)]
zks [(x, i)]
xis [(y, i)]
yjs) where
  zks :: [(x, i)] -> [(y, i)] -> [(z, i)]
zks [] [(y, i)]
yjs                  = forall a b. (a -> b) -> [a] -> [b]
map (\(y
y,i
j) -> (y -> z
yz y
y,i
j)) [(y, i)]
yjs
  zks [(x, i)]
xis []                  = forall a b. (a -> b) -> [a] -> [b]
map (\(x
x,i
i) -> (x -> z
xz x
x,i
i)) [(x, i)]
xis
  zks ((x
x,i
i):[(x, i)]
xis) ((y
y,i
j):[(y, i)]
yjs) = case i
i forall a. Ord a => a -> a -> Ordering
`compare` i
j of
    Ordering
LT -> (x -> z
xz x
x,i
i) forall a. a -> [a] -> [a]
: [(x, i)] -> [(y, i)] -> [(z, i)]
zks [(x, i)]
xis ((y
y,i
j)forall a. a -> [a] -> [a]
:[(y, i)]
yjs)
    Ordering
EQ -> (x
x x -> y -> z
+ y
y,i
i) forall a. a -> [a] -> [a]
: [(x, i)] -> [(y, i)] -> [(z, i)]
zks [(x, i)]
xis [(y, i)]
yjs
    Ordering
GT -> (y -> z
yz y
y,i
j) forall a. a -> [a] -> [a]
: [(x, i)] -> [(y, i)] -> [(z, i)]
zks ((x
x,i
i)forall a. a -> [a] -> [a]
:[(x, i)]
xis) [(y, i)]
yjs

--------------------------------------------------------------------------------
-- psqCompose -

-- | composition of the two partially defined sequences.
--
-- __Property__ Let @f@ be in @'PSequence' __i__ __x__@ and @g@ be in @'PSequence' __j__ __i__@ then
-- @f '`psqCompose`' g@ is given by @'join' '.' 'fmap' (('??') f) '.' ('??') g@.
psqCompose :: (Ord i, Ord j) => PSequence i x -> PSequence j i -> PSequence j x
psqCompose :: forall i j x.
(Ord i, Ord j) =>
PSequence i x -> PSequence j i -> PSequence j x
psqCompose (PSequence [(x, i)]
xis) (PSequence [(i, j)]
ijs)
  = forall x y i. (x -> y) -> PSequence i x -> PSequence i y
psqMap forall a. HasCallStack => Maybe a -> a
fromJust forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ 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 {a} {a} {b}. Ord a => [(a, a)] -> [(a, b)] -> [(Maybe a, b)]
cmp [(x, i)]
xis (forall a b. Ord a => [(a, b)] -> [(a, b)]
sortFst [(i, j)]
ijs) where
  
  cmp :: [(a, a)] -> [(a, b)] -> [(Maybe a, b)]
cmp [] [(a, b)]
_  = []
  cmp [(a, a)]
_ []  = []
  cmp xis :: [(a, a)]
xis@((a
x,a
i):[(a, a)]
xis') ijs :: [(a, b)]
ijs@((a
i',b
j):[(a, b)]
ijs') = case a
i forall a. Ord a => a -> a -> Ordering
`compare` a
i' of
    Ordering
LT -> [(a, a)] -> [(a, b)] -> [(Maybe a, b)]
cmp [(a, a)]
xis' [(a, b)]
ijs
    Ordering
EQ -> (forall a. a -> Maybe a
Just a
x,b
j)forall a. a -> [a] -> [a]
:[(a, a)] -> [(a, b)] -> [(Maybe a, b)]
cmp [(a, a)]
xis' [(a, b)]
ijs'
    Ordering
GT -> [(a, a)] -> [(a, b)] -> [(Maybe a, b)]
cmp [(a, a)]
xis [(a, b)]
ijs'

-- cmp :: (i -> Maybe x)  (j -> Maybe i) -> i -> Maybe x

--------------------------------------------------------------------------------
-- psqSplitWhile -

-- | splits the sequence as long as the given predicate holds.
psqSplitWhile :: ((x,i) -> Bool) -> PSequence i x -> (PSequence i x,PSequence i x)
psqSplitWhile :: forall x i.
((x, i) -> Bool) -> PSequence i x -> (PSequence i x, PSequence i x)
psqSplitWhile (x, i) -> Bool
p (PSequence [(x, i)]
xs) = (forall i x. [(x, i)] -> PSequence i x
PSequence [(x, i)]
l,forall i x. [(x, i)] -> PSequence i x
PSequence [(x, i)]
r) where
  ([(x, i)]
l,[(x, i)]
r) = forall {a}. (a -> Bool) -> [a] -> ([a], [a])
spw (x, i) -> Bool
p [(x, i)]
xs

  spw :: (a -> Bool) -> [a] -> ([a], [a])
spw a -> Bool
_ []     = ([],[])
  spw a -> Bool
p (a
x:[a]
xs) = if a -> Bool
p a
x then (a
xforall a. a -> [a] -> [a]
:[a]
l,[a]
r) else ([],a
xforall a. a -> [a] -> [a]
:[a]
xs) where ([a]
l,[a]
r) = (a -> Bool) -> [a] -> ([a], [a])
spw a -> Bool
p [a]
xs

--------------------------------------------------------------------------------
-- psqAppend -

-- | appends the second partially defined sequence to the first.
--
--  __Property__ Let @zs = 'psqAppend' xs ys@ where @..(x,l) = xs@ and
-- @(y,f).. = ys@ then holds:
--
-- [If] @l '<' f@
--
-- [Then] @zs@ is 'valid'.
psqAppend ::PSequence i x -> PSequence i x -> PSequence i x
psqAppend :: forall i x. PSequence i x -> PSequence i x -> PSequence i x
psqAppend (PSequence [(x, i)]
xs) (PSequence [(x, i)]
ys) = forall i x. [(x, i)] -> PSequence i x
PSequence ([(x, i)]
xs forall a. [a] -> [a] -> [a]
++ [(x, i)]
ys)

--------------------------------------------------------------------------------
-- //: -

-- | cone.
(//:) :: (Maybe a,i) -> [(a,i)] -> [(a,i)]
(Just a
a,i
i) //: :: forall a i. (Maybe a, i) -> [(a, i)] -> [(a, i)]
//: [(a, i)]
ais  = (a
a,i
i)forall a. a -> [a] -> [a]
:[(a, i)]
ais
(Maybe a
Nothing,i
_) //: [(a, i)]
ais = [(a, i)]
ais

--------------------------------------------------------------------------------
-- psqShear -


-- | shears the two entries at the given position and leafs the others untouched.
--
-- __Property__ Let @x' = psqShear (sk,k) (sl,l) x@, then holds
--
-- [If] @k '<' l@
--
-- [Then]
--
-- (1) @x' k '==' sk (x k) (x l)@ and @x' l '==' sl (x k) (x l)@.
--
-- (2) @x' i '==' x i@ for all @i '/=' k, l@. 
psqShear :: Ord i
         => (Maybe a -> Maybe a -> Maybe a,i) -> (Maybe a -> Maybe a -> Maybe a,i)
         -> PSequence i a -> PSequence i a
psqShear :: forall i a.
Ord i =>
(Maybe a -> Maybe a -> Maybe a, i)
-> (Maybe a -> Maybe a -> Maybe a, i)
-> PSequence i a
-> PSequence i a
psqShear (Maybe a -> Maybe a -> Maybe a
sk,i
k) (Maybe a -> Maybe a -> Maybe a
sl,i
l) (PSequence [(a, i)]
xis) = forall i x. [(x, i)] -> PSequence i x
PSequence ([(a, i)] -> [(a, i)]
shr [(a, i)]
xis) where
  shr :: [(a, i)] -> [(a, i)]
shr []          = []
  shr ((a
x,i
i):[(a, i)]
xis) = case i
i forall a. Ord a => a -> a -> Ordering
`compare` i
k of
    Ordering
LT -> (a
x,i
i) forall a. a -> [a] -> [a]
: [(a, i)] -> [(a, i)]
shr [(a, i)]
xis
    Ordering
EQ -> (Maybe a -> Maybe a -> Maybe a
sk Maybe a
xk Maybe a
xl,i
k) forall a i. (Maybe a, i) -> [(a, i)] -> [(a, i)]
//: [(a, i)]
xis' where
      xk :: Maybe a
xk = forall a. a -> Maybe a
Just a
x
      (Maybe a
xl,[(a, i)]
xis') = Maybe a -> [(a, i)] -> (Maybe a, [(a, i)])
shr' Maybe a
xk [(a, i)]
xis
    Ordering
GT -> (Maybe a -> Maybe a -> Maybe a
sk forall {a}. Maybe a
xk Maybe a
xl,i
k) forall a i. (Maybe a, i) -> [(a, i)] -> [(a, i)]
//: [(a, i)]
xis' where
      xk :: Maybe a
xk        = forall {a}. Maybe a
Nothing
      (Maybe a
xl,[(a, i)]
xis') = Maybe a -> [(a, i)] -> (Maybe a, [(a, i)])
shr' forall {a}. Maybe a
xk ((a
x,i
i)forall a. a -> [a] -> [a]
:[(a, i)]
xis)

  shr' :: Maybe a -> [(a, i)] -> (Maybe a, [(a, i)])
shr' Maybe a
xk []             = Maybe a -> Maybe a -> [(a, i)] -> (Maybe a, [(a, i)])
shr'' Maybe a
xk forall {a}. Maybe a
Nothing []
  shr' Maybe a
xk (xi :: (a, i)
xi@(a
x,i
i):[(a, i)]
xis) = case i
i forall a. Ord a => a -> a -> Ordering
`compare` i
l of
    Ordering
LT -> (Maybe a
sl,(a, i)
xiforall a. a -> [a] -> [a]
:[(a, i)]
xis') where (Maybe a
sl,[(a, i)]
xis') = Maybe a -> [(a, i)] -> (Maybe a, [(a, i)])
shr' Maybe a
xk [(a, i)]
xis
    Ordering
EQ -> Maybe a -> Maybe a -> [(a, i)] -> (Maybe a, [(a, i)])
shr'' Maybe a
xk (forall a. a -> Maybe a
Just a
x) [(a, i)]
xis
    Ordering
GT -> Maybe a -> Maybe a -> [(a, i)] -> (Maybe a, [(a, i)])
shr'' Maybe a
xk forall {a}. Maybe a
Nothing ((a, i)
xiforall a. a -> [a] -> [a]
:[(a, i)]
xis)

  shr'' :: Maybe a -> Maybe a -> [(a, i)] -> (Maybe a, [(a, i)])
shr'' Maybe a
xk Maybe a
xl [(a, i)]
xis = (Maybe a
xl,(Maybe a -> Maybe a -> Maybe a
sl Maybe a
xk Maybe a
xl,i
l) forall a i. (Maybe a, i) -> [(a, i)] -> [(a, i)]
//: [(a, i)]
xis)

--------------------------------------------------------------------------------
-- psqSwap -

-- | swaps the the @k@-th and the @l@-th entry.
--
-- __Property__ Let @x' = psqSwap k l x@, then holds:
--
-- [If] @k < l@
--
-- [Then]
--
-- (1) @x' k '==' x l@ and @x' l '==' x k@.
-- 
-- (2) @x' i '==' x i@ for all @i '/=' k, l@.
psqSwap :: Ord i => i -> i -> PSequence i a -> PSequence i a
psqSwap :: forall i a. Ord i => i -> i -> PSequence i a -> PSequence i a
psqSwap i
k i
l = forall i a.
Ord i =>
(Maybe a -> Maybe a -> Maybe a, i)
-> (Maybe a -> Maybe a -> Maybe a, i)
-> PSequence i a
-> PSequence i a
psqShear (forall {p} {p}. p -> p -> p
sk,i
k) (forall {p} {p}. p -> p -> p
sl,i
l) where
  sk :: p -> p -> p
sk p
_ p
x = p
x
  sl :: p -> p -> p
sl p
x p
_ = p
x

--------------------------------------------------------------------------------
-- xPSequence -

-- | @'xPSequence' n m@ random variable of partially defined sequences with maximal length
--   @'min' n m@.
xPSequence :: Ord i => N -> N -> X x -> X i -> X (PSequence i x)
xPSequence :: forall i x. Ord i => N -> N -> X x -> X i -> X (PSequence i x)
xPSequence N
n N
m X x
xx X i
xi = do
  [x]
xs <- forall x. N -> X x -> X [x]
xTakeN N
n X x
xx
  Set i
is <- forall x. Ord x => N -> X x -> X (Set x)
xSet N
m X i
xi
  forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall i x. [(x, i)] -> PSequence i x
PSequence forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ ([x]
xs forall a b. [a] -> [b] -> [(a, b)]
`zip` forall x. Set x -> [x]
setxs Set i
is)