{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies, TypeOperators #-}
{-# 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(..), psqxs, iProxy
  , psqSpan
  , psqEmpty, psqIsEmpty, psequence
  , psqHead, psqTail
  , psqMap, psqMapShift, psqMapWithIndex, Monotone(..)
  , psqFilter
  , psqSplitWhile
  , psqInterlace
  , psqCompose
  , psqAppend
  , psqShear
  , psqSwap
  , psqTree
  , psqFromTree

    -- * Tree
  , PTree(..), ptrxs, ptrx
  , ptrEmpty
  , ptrMax, ptrMin, ptrSpan
  , ptrFilter, ptrFilterWithIndex
  , ptrMap, ptrMapShift, ptrMapWithIndex
  
    -- * X
  , xPSequence

    -- * Proposition
  , prpPSequence, prpPTreeFilter
  ) where

import Control.Monad as M

import Data.Monoid
import Data.Foldable
import Data.Typeable

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

import OAlg.Prelude

import OAlg.Data.Tree
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
[PSequence i x] -> ShowS
PSequence i x -> String
(Int -> PSequence i x -> ShowS)
-> (PSequence i x -> String)
-> ([PSequence i x] -> ShowS)
-> Show (PSequence i x)
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
$cshowsPrec :: forall i x. (Show x, Show i) => Int -> PSequence i x -> ShowS
showsPrec :: Int -> PSequence i x -> ShowS
$cshow :: forall i x. (Show x, Show i) => PSequence i x -> String
show :: PSequence i x -> String
$cshowList :: forall i x. (Show x, Show i) => [PSequence i x] -> ShowS
showList :: [PSequence i x] -> ShowS
Show,PSequence i x -> PSequence i x -> Bool
(PSequence i x -> PSequence i x -> Bool)
-> (PSequence i x -> PSequence i x -> Bool) -> Eq (PSequence i x)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall i x. (Eq x, Eq i) => 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
/= :: PSequence i x -> PSequence i x -> Bool
Eq,Eq (PSequence i x)
Eq (PSequence i x) =>
(PSequence i x -> PSequence i x -> Ordering)
-> (PSequence i x -> PSequence i x -> Bool)
-> (PSequence i x -> PSequence i x -> Bool)
-> (PSequence i x -> PSequence i x -> Bool)
-> (PSequence i x -> PSequence i x -> Bool)
-> (PSequence i x -> PSequence i x -> PSequence i x)
-> (PSequence i x -> PSequence i x -> PSequence i x)
-> Ord (PSequence i x)
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
$ccompare :: forall i x.
(Ord x, Ord i) =>
PSequence i x -> PSequence i x -> Ordering
compare :: PSequence i x -> PSequence i x -> Ordering
$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
>= :: PSequence i x -> PSequence i x -> Bool
$cmax :: 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
$cmin :: 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
Ord,PSequence i x -> N
(PSequence i x -> N) -> LengthN (PSequence i x)
forall x. (x -> N) -> LengthN x
forall i x. PSequence i x -> N
$clengthN :: forall i x. PSequence i x -> N
lengthN :: PSequence i x -> N
LengthN,(forall m. Monoid m => PSequence i m -> m)
-> (forall m a. Monoid m => (a -> m) -> PSequence i a -> m)
-> (forall m a. Monoid m => (a -> m) -> PSequence i a -> m)
-> (forall a b. (a -> b -> b) -> b -> PSequence i a -> b)
-> (forall a b. (a -> b -> b) -> b -> PSequence i a -> b)
-> (forall b a. (b -> a -> b) -> b -> PSequence i a -> b)
-> (forall b a. (b -> a -> b) -> b -> PSequence i a -> b)
-> (forall a. (a -> a -> a) -> PSequence i a -> a)
-> (forall a. (a -> a -> a) -> PSequence i a -> a)
-> (forall a. PSequence i a -> [a])
-> (forall a. PSequence i a -> Bool)
-> (forall a. PSequence i a -> Int)
-> (forall a. Eq a => a -> PSequence i a -> Bool)
-> (forall a. Ord a => PSequence i a -> a)
-> (forall a. Ord a => PSequence i a -> a)
-> (forall a. Num a => PSequence i a -> a)
-> (forall a. Num a => PSequence i a -> a)
-> Foldable (PSequence i)
forall a. Eq a => a -> PSequence i a -> Bool
forall a. Num a => PSequence i a -> a
forall a. Ord a => PSequence i a -> a
forall m. Monoid m => PSequence i m -> m
forall a. PSequence i a -> Bool
forall a. PSequence i a -> Int
forall a. PSequence i a -> [a]
forall a. (a -> a -> a) -> PSequence i a -> a
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 i m. Monoid m => PSequence i m -> m
forall m a. Monoid m => (a -> m) -> PSequence i a -> m
forall i a. PSequence i a -> Bool
forall i a. PSequence i a -> Int
forall i a. PSequence i a -> [a]
forall b a. (b -> a -> b) -> b -> PSequence i a -> b
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
$cfold :: forall i m. Monoid m => PSequence i m -> m
fold :: forall m. Monoid m => PSequence i m -> 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
foldMap' :: forall m a. Monoid m => (a -> m) -> PSequence i a -> m
$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
foldr' :: forall a b. (a -> b -> 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
foldl' :: forall b a. (b -> a -> b) -> b -> PSequence i a -> b
$cfoldr1 :: forall i a. (a -> a -> a) -> PSequence i a -> a
foldr1 :: forall a. (a -> a -> a) -> PSequence i a -> a
$cfoldl1 :: forall i a. (a -> a -> a) -> PSequence i a -> a
foldl1 :: forall a. (a -> a -> a) -> PSequence i a -> a
$ctoList :: forall i a. PSequence i a -> [a]
toList :: forall a. PSequence i a -> [a]
$cnull :: forall i a. PSequence i a -> Bool
null :: forall a. PSequence i a -> Bool
$clength :: forall i a. PSequence i a -> Int
length :: forall a. PSequence i a -> Int
$celem :: forall i a. Eq a => a -> PSequence i a -> Bool
elem :: forall a. Eq a => a -> PSequence i a -> Bool
$cmaximum :: forall i a. Ord a => PSequence i a -> a
maximum :: forall a. Ord a => PSequence i a -> a
$cminimum :: forall i a. Ord a => PSequence i a -> a
minimum :: forall a. Ord a => PSequence i a -> a
$csum :: forall i a. Num a => PSequence i a -> a
sum :: forall a. Num a => PSequence i a -> a
$cproduct :: forall i a. Num a => PSequence i a -> a
product :: forall a. Num a => PSequence i a -> a
Foldable)

instance Embeddable [x] (PSequence N x) where
  inj :: [x] -> PSequence N x
inj [x]
xs = [(x, N)] -> PSequence N x
forall i x. [(x, i)] -> PSequence i x
PSequence ([x]
xs [x] -> [N] -> [(x, N)]
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) = ((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)]
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)
  = [(x, i)] -> PSequence i x
forall i x. [(x, i)] -> PSequence i x
PSequence
  ([(x, i)] -> PSequence i x) -> [(x, i)] -> PSequence i x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((Maybe x, i) -> (x, i)) -> [(Maybe x, i)] -> [(x, i)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Maybe x
mx,i
i) -> (Maybe x -> x
forall a. HasCallStack => Maybe a -> a
fromJust Maybe x
mx,i
i))
  ([(Maybe x, i)] -> [(x, i)]) -> [(Maybe x, i)] -> [(x, i)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((Maybe x, i) -> Bool) -> [(Maybe x, i)] -> [(Maybe x, i)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Maybe x -> Bool
forall a. Maybe a -> Bool
isJust (Maybe x -> Bool)
-> ((Maybe x, i) -> Maybe x) -> (Maybe x, i) -> 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
. (Maybe x, i) -> Maybe x
forall a b. (a, b) -> a
fst)
  ([(Maybe x, i)] -> [(Maybe x, i)])
-> [(Maybe x, i)] -> [(Maybe x, i)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (i -> (Maybe x, i)) -> [i] -> [(Maybe x, i)]
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
_ = PSequence i x -> [(x, 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 = (i -> Maybe x) -> Set i -> PSequence i x
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 -> Closure i -> (i -> Maybe x) -> PSequence i x
psqFromMap :: forall i x.
(Enum i, Ord i) =>
i -> Closure i -> (i -> Maybe x) -> PSequence i x
psqFromMap i
i0 Closure i
h i -> Maybe x
f
  = [(x, i)] -> PSequence i x
forall i x. [(x, i)] -> PSequence i x
PSequence
  ([(x, i)] -> PSequence i x) -> [(x, i)] -> PSequence i x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((Maybe x, i) -> (x, i)) -> [(Maybe x, i)] -> [(x, i)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Maybe x
mx,i
i) -> (Maybe x -> x
forall a. HasCallStack => Maybe a -> a
fromJust Maybe x
mx,i
i)) 
  ([(Maybe x, i)] -> [(x, i)]) -> [(Maybe x, i)] -> [(x, i)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((Maybe x, i) -> Bool) -> [(Maybe x, i)] -> [(Maybe x, i)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Maybe x -> Bool
forall a. Maybe a -> Bool
isJust (Maybe x -> Bool)
-> ((Maybe x, i) -> Maybe x) -> (Maybe x, i) -> 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
. (Maybe x, i) -> Maybe x
forall a b. (a, b) -> a
fst)
  ([(Maybe x, i)] -> [(Maybe x, i)])
-> [(Maybe x, i)] -> [(Maybe x, i)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (i -> (Maybe x, i)) -> [i] -> [(Maybe x, i)]
forall a b. (a -> b) -> [a] -> [b]
map (\i
i -> (i -> Maybe x
f i
i,i
i))
  ([i] -> [(Maybe x, i)]) -> [i] -> [(Maybe x, i)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ i -> Closure i -> [i]
forall i. (Enum i, Ord i) => i -> Closure i -> [i]
enumSpan i
i0 Closure 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
_ = Proxy i
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) = [i] -> Span i
forall x. Ord x => [x] -> Span x
cspan ([i] -> Span i) -> [i] -> Span i
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((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)]
xs

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

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

--------------------------------------------------------------------------------
-- Monotone -


-- | predicate for strict monoton mappings.
--
-- __Property__ Let @_i__@, @__j__@ two 'Ord'-types, and @'Monotone' f@ in @'Monotone' __i__ __j__@, then
-- holds: For all @x@, @y@ in @__i__@ holds: @'compare' (f x) (f y) '==' 'compare' x y@. 
newtype Monotone i j = Monotone (i -> j)

instance (Ord i, Ord j, XStandard i, Show i) => Validable (Monotone i j) where
  valid :: Monotone i j -> Statement
valid (Monotone i -> j
f) = String -> Label
Label String
"Monotone"
    Label -> Statement -> Statement
:<=>: X (i, i) -> ((i, i) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (i, i)
xy (\(i
x,i
y)
                     -> ((j -> j -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (i -> j
f i
x) (i -> j
f i
y) Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== i -> i -> Ordering
forall a. Ord a => a -> a -> Ordering
compare i
x i
y) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"x"String -> String -> Parameter
:=i -> String
forall a. Show a => a -> String
show i
x,String
"y"String -> String -> Parameter
:=i -> String
forall a. Show a => a -> String
show i
y])
                    )
    where xy :: X (i, i)
xy = X i -> X i -> X (i, i)
forall a b. X a -> X b -> X (a, b)
xTupple2 X i
forall x. XStandard x => X x
xStandard X i
forall x. XStandard x => X x
xStandard

--------------------------------------------------------------------------------
-- psqMapWithIndex -

-- | maps of a 'PSequence' according to the given strict monotone mapping and the given indexed
-- mapping.  
psqMapWithIndex :: Monotone i j -> ((x,i) -> y) -> PSequence i x -> PSequence j y
psqMapWithIndex :: forall i j x y.
Monotone i j -> ((x, i) -> y) -> PSequence i x -> PSequence j y
psqMapWithIndex (Monotone i -> j
j) (x, i) -> y
y (PSequence [(x, i)]
xis) = [(y, j)] -> PSequence j y
forall i x. [(x, i)] -> PSequence i x
PSequence ([(y, j)] -> PSequence j y) -> [(y, j)] -> PSequence j y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((x, i) -> (y, j)) -> [(x, i)] -> [(y, j)]
forall a b. (a -> b) -> [a] -> [b]
map (x, i) -> (y, j)
yj [(x, i)]
xis where yj :: (x, i) -> (y, j)
yj (x, i)
xi = ((x, i) -> y
y (x, i)
xi,i -> j
j (i -> j) -> i -> j
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (x, i) -> i
forall a b. (a, b) -> b
snd (x, i)
xi)
  
--------------------------------------------------------------------------------
-- psqMapShift -

-- | shifts the indices of 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
t = Monotone i i -> ((x, i) -> y) -> PSequence i x -> PSequence i y
forall i j x y.
Monotone i j -> ((x, i) -> y) -> PSequence i x -> PSequence j y
psqMapWithIndex ((i -> i) -> Monotone i i
forall i j. (i -> j) -> Monotone i j
Monotone (i -> i -> i
forall a. Additive a => a -> a -> a
+i
t))

--------------------------------------------------------------------------------
-- 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 = Monotone i i -> ((x, i) -> y) -> PSequence i x -> PSequence i y
forall i j x y.
Monotone i j -> ((x, i) -> y) -> PSequence i x -> PSequence j y
psqMapWithIndex ((i -> i) -> Monotone i i
forall i j. (i -> j) -> Monotone i j
Monotone i -> i
forall x. x -> x
id) (x -> y
f (x -> y) -> ((x, i) -> x) -> (x, i) -> y
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
. (x, i) -> x
forall a b. (a, b) -> a
fst)

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

instance ApplicativeG (PSequence i) (->) (->) where amapG :: forall x y. (x -> y) -> PSequence i x -> PSequence i y
amapG = (x -> y) -> PSequence i x -> PSequence i y
forall x y i. (x -> y) -> PSequence i x -> PSequence i y
psqMap

--------------------------------------------------------------------------------
-- 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)) = N -> (x, i) -> [(x, i)] -> Statement
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 [] = (a, b) -> Statement
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
ib -> b -> Bool
forall a. Ord a => a -> a -> Bool
<b
j)Bool -> Message -> Statement
:?>[Parameter] -> Message
Params [String
"l"String -> String -> Parameter
:=t -> String
forall a. Show a => a -> String
show t
l,String
"(i,j)"String -> String -> Parameter
:=(b, b) -> String
forall a. Show a => a -> String
show (b
i,b
j)]
                                        , (a, b) -> Statement
forall a. Validable a => a -> Statement
valid (a, b)
xi
                                        , t -> (a, b) -> [(a, b)] -> Statement
vld (t -> t
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
:<=>: Graph i x -> Statement
forall a. Validable a => a -> Statement
valid (Proxy i -> PSequence i x -> Graph i x
forall (p :: * -> *). p i -> PSequence i x -> Graph i x
forall (s :: * -> *) i x (p :: * -> *).
Sequence s i x =>
p i -> s x -> Graph i x
graph (PSequence i x -> Proxy i
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 = [(x, i)] -> PSequence i x
forall i x. [(x, i)] -> PSequence i x
PSequence
             ([(x, i)] -> PSequence i x) -> [(x, i)] -> PSequence i x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ([(x, i)] -> (x, i)) -> [[(x, i)]] -> [(x, i)]
forall a b. (a -> b) -> [a] -> [b]
map ((x -> x -> x) -> [(x, i)] -> (x, i)
forall x i. (x -> x -> x) -> [(x, i)] -> (x, i)
aggrBy x -> x -> x
(+))
             ([[(x, i)]] -> [(x, i)]) -> [[(x, i)]] -> [(x, i)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((x, i) -> (x, i) -> Bool) -> [(x, i)] -> [[(x, i)]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (((x, i) -> (x, i) -> Ordering) -> (x, i) -> (x, i) -> Bool
forall a. (a -> a -> Ordering) -> a -> a -> Bool
eql (((x, i) -> i) -> (x, i) -> (x, i) -> Ordering
forall i a. Ord i => (a -> i) -> a -> a -> Ordering
fcompare (x, i) -> i
forall a b. (a, b) -> b
snd))
             ([(x, i)] -> [[(x, i)]]) -> [(x, i)] -> [[(x, i)]]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((x, i) -> (x, i) -> Ordering) -> [(x, i)] -> [(x, i)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (((x, i) -> i) -> (x, i) -> (x, i) -> Ordering
forall i a. Ord i => (a -> i) -> a -> a -> Ordering
fcompare (x, i) -> i
forall a b. (a, b) -> b
snd)
             ([(x, i)] -> [(x, i)]) -> [(x, i)] -> [(x, i)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(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) = ((x -> x -> x) -> x -> [x] -> x
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl x -> x -> x
(+) x
x (((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)]
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) = [(x, i)] -> (x, i)
forall a. HasCallStack => [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) = [(x, i)] -> PSequence i x
forall i x. [(x, i)] -> PSequence i x
PSequence ([(x, i)] -> [(x, i)]
forall a. HasCallStack => [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) = [(x, i)] -> PSequence i x
forall i x. [(x, i)] -> PSequence i x
PSequence ([(x, i)] -> PSequence i x) -> [(x, i)] -> PSequence i x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((x, i) -> Bool) -> [(x, i)] -> [(x, i)]
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) = [(z, i)] -> PSequence i z
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                  = ((y, i) -> (z, i)) -> [(y, i)] -> [(z, i)]
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 []                  = ((x, i) -> (z, i)) -> [(x, i)] -> [(z, i)]
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 i -> i -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` i
j of
    Ordering
LT -> (x -> z
xz x
x,i
i) (z, i) -> [(z, i)] -> [(z, i)]
forall a. a -> [a] -> [a]
: [(x, i)] -> [(y, i)] -> [(z, i)]
zks [(x, i)]
xis ((y
y,i
j)(y, i) -> [(y, i)] -> [(y, i)]
forall a. a -> [a] -> [a]
:[(y, i)]
yjs)
    Ordering
EQ -> (x
x x -> y -> z
+ y
y,i
i) (z, i) -> [(z, i)] -> [(z, 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) (z, i) -> [(z, i)] -> [(z, i)]
forall a. a -> [a] -> [a]
: [(x, i)] -> [(y, i)] -> [(z, i)]
zks ((x
x,i
i)(x, i) -> [(x, i)] -> [(x, 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)
  = (Maybe x -> x) -> PSequence j (Maybe x) -> PSequence j x
forall x y i. (x -> y) -> PSequence i x -> PSequence i y
psqMap Maybe x -> x
forall a. HasCallStack => Maybe a -> a
fromJust (PSequence j (Maybe x) -> PSequence j x)
-> PSequence j (Maybe x) -> PSequence j x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(Maybe x, j)] -> PSequence j (Maybe x)
forall i x. [(x, i)] -> PSequence i x
PSequence ([(Maybe x, j)] -> PSequence j (Maybe x))
-> [(Maybe x, j)] -> PSequence j (Maybe x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(Maybe x, j)] -> [(Maybe x, j)]
forall b a. Ord b => [(a, b)] -> [(a, b)]
sortSnd ([(Maybe x, j)] -> [(Maybe x, j)])
-> [(Maybe x, j)] -> [(Maybe x, j)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(x, i)] -> [(i, j)] -> [(Maybe x, j)]
forall {a} {a} {b}. Ord a => [(a, a)] -> [(a, b)] -> [(Maybe a, b)]
cmp [(x, i)]
xis ([(i, j)] -> [(i, j)]
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 a -> a -> Ordering
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 -> (a -> Maybe a
forall a. a -> Maybe a
Just a
x,b
j)(Maybe a, b) -> [(Maybe a, b)] -> [(Maybe a, b)]
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) = ([(x, i)] -> PSequence i x
forall i x. [(x, i)] -> PSequence i x
PSequence [(x, i)]
l,[(x, i)] -> PSequence i x
forall i x. [(x, i)] -> PSequence i x
PSequence [(x, i)]
r) where
  ([(x, i)]
l,[(x, i)]
r) = ((x, i) -> Bool) -> [(x, i)] -> ([(x, i)], [(x, i)])
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
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
l,[a]
r) else ([],a
xa -> [a] -> [a]
forall 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) = [(x, i)] -> PSequence i x
forall i x. [(x, i)] -> PSequence i x
PSequence ([(x, i)]
xs [(x, i)] -> [(x, i)] -> [(x, i)]
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)(a, i) -> [(a, i)] -> [(a, 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) = [(a, i)] -> PSequence i a
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 i -> i -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` i
k of
    Ordering
LT -> (a
x,i
i) (a, i) -> [(a, i)] -> [(a, 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) (Maybe a, i) -> [(a, i)] -> [(a, i)]
forall a i. (Maybe a, i) -> [(a, i)] -> [(a, i)]
//: [(a, i)]
xis' where
      xk :: Maybe a
xk = a -> Maybe a
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 Maybe a
forall {a}. Maybe a
xk Maybe a
xl,i
k) (Maybe a, i) -> [(a, i)] -> [(a, i)]
forall a i. (Maybe a, i) -> [(a, i)] -> [(a, i)]
//: [(a, i)]
xis' where
      xk :: Maybe a
xk        = Maybe a
forall {a}. Maybe a
Nothing
      (Maybe a
xl,[(a, i)]
xis') = Maybe a -> [(a, i)] -> (Maybe a, [(a, i)])
shr' Maybe a
forall {a}. Maybe a
xk ((a
x,i
i)(a, i) -> [(a, i)] -> [(a, 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 Maybe a
forall {a}. Maybe a
Nothing []
  shr' Maybe a
xk (xi :: (a, i)
xi@(a
x,i
i):[(a, i)]
xis) = case i
i i -> i -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` i
l of
    Ordering
LT -> (Maybe a
sl,(a, i)
xi(a, i) -> [(a, i)] -> [(a, i)]
forall 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 (a -> Maybe a
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 Maybe a
forall {a}. Maybe a
Nothing ((a, i)
xi(a, i) -> [(a, i)] -> [(a, i)]
forall 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) (Maybe a, i) -> [(a, i)] -> [(a, i)]
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 = (Maybe a -> Maybe a -> Maybe a, i)
-> (Maybe a -> Maybe a -> Maybe a, i)
-> PSequence i a
-> PSequence i a
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
forall {p} {p}. p -> p -> p
sk,i
k) (Maybe a -> Maybe a -> Maybe a
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 of
--   @'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 <- N -> X x -> X [x]
forall x. N -> X x -> X [x]
xTakeN N
n X x
xx
  Set i
is <- N -> X i -> X (Set i)
forall x. Ord x => N -> X x -> X (Set x)
xSet N
m X i
xi
  PSequence i x -> X (PSequence i x)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (PSequence i x -> X (PSequence i x))
-> PSequence i x -> X (PSequence i x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(x, i)] -> PSequence i x
forall i x. [(x, i)] -> PSequence i x
PSequence ([(x, i)] -> PSequence i x) -> [(x, i)] -> PSequence i x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ([x]
xs [x] -> [i] -> [(x, i)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` Set i -> [i]
forall x. Set x -> [x]
setxs Set i
is)

--------------------------------------------------------------------------------
-- PTree -

-- | binary tree for efficient retrieving elements of a partially defined sequence.
newtype PTree i x = PTree (Maybe (Tree i (x,i))) deriving (Int -> PTree i x -> ShowS
[PTree i x] -> ShowS
PTree i x -> String
(Int -> PTree i x -> ShowS)
-> (PTree i x -> String)
-> ([PTree i x] -> ShowS)
-> Show (PTree i x)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall i x. (Show i, Show x) => Int -> PTree i x -> ShowS
forall i x. (Show i, Show x) => [PTree i x] -> ShowS
forall i x. (Show i, Show x) => PTree i x -> String
$cshowsPrec :: forall i x. (Show i, Show x) => Int -> PTree i x -> ShowS
showsPrec :: Int -> PTree i x -> ShowS
$cshow :: forall i x. (Show i, Show x) => PTree i x -> String
show :: PTree i x -> String
$cshowList :: forall i x. (Show i, Show x) => [PTree i x] -> ShowS
showList :: [PTree i x] -> ShowS
Show,PTree i x -> PTree i x -> Bool
(PTree i x -> PTree i x -> Bool)
-> (PTree i x -> PTree i x -> Bool) -> Eq (PTree i x)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall i x. (Eq i, Eq x) => PTree i x -> PTree i x -> Bool
$c== :: forall i x. (Eq i, Eq x) => PTree i x -> PTree i x -> Bool
== :: PTree i x -> PTree i x -> Bool
$c/= :: forall i x. (Eq i, Eq x) => PTree i x -> PTree i x -> Bool
/= :: PTree i x -> PTree i x -> Bool
Eq,Eq (PTree i x)
Eq (PTree i x) =>
(PTree i x -> PTree i x -> Ordering)
-> (PTree i x -> PTree i x -> Bool)
-> (PTree i x -> PTree i x -> Bool)
-> (PTree i x -> PTree i x -> Bool)
-> (PTree i x -> PTree i x -> Bool)
-> (PTree i x -> PTree i x -> PTree i x)
-> (PTree i x -> PTree i x -> PTree i x)
-> Ord (PTree i x)
PTree i x -> PTree i x -> Bool
PTree i x -> PTree i x -> Ordering
PTree i x -> PTree i x -> PTree 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 i, Ord x) => Eq (PTree i x)
forall i x. (Ord i, Ord x) => PTree i x -> PTree i x -> Bool
forall i x. (Ord i, Ord x) => PTree i x -> PTree i x -> Ordering
forall i x. (Ord i, Ord x) => PTree i x -> PTree i x -> PTree i x
$ccompare :: forall i x. (Ord i, Ord x) => PTree i x -> PTree i x -> Ordering
compare :: PTree i x -> PTree i x -> Ordering
$c< :: forall i x. (Ord i, Ord x) => PTree i x -> PTree i x -> Bool
< :: PTree i x -> PTree i x -> Bool
$c<= :: forall i x. (Ord i, Ord x) => PTree i x -> PTree i x -> Bool
<= :: PTree i x -> PTree i x -> Bool
$c> :: forall i x. (Ord i, Ord x) => PTree i x -> PTree i x -> Bool
> :: PTree i x -> PTree i x -> Bool
$c>= :: forall i x. (Ord i, Ord x) => PTree i x -> PTree i x -> Bool
>= :: PTree i x -> PTree i x -> Bool
$cmax :: forall i x. (Ord i, Ord x) => PTree i x -> PTree i x -> PTree i x
max :: PTree i x -> PTree i x -> PTree i x
$cmin :: forall i x. (Ord i, Ord x) => PTree i x -> PTree i x -> PTree i x
min :: PTree i x -> PTree i x -> PTree i x
Ord)

instance Foldable (PTree i) where
  foldMap :: forall m a. Monoid m => (a -> m) -> PTree i a -> m
foldMap a -> m
_ (PTree Maybe (Tree i (a, i))
Nothing)  = m
forall a. Monoid a => a
mempty
  foldMap a -> m
f (PTree (Just Tree i (a, i)
t)) = (a -> m) -> Tree i (a, i) -> m
forall {t} {t} {i} {b}.
Semigroup t =>
(t -> t) -> Tree i (t, b) -> t
fm a -> m
f Tree i (a, i)
t where
    fm :: (t -> t) -> Tree i (t, b) -> t
fm t -> t
f (Leaf (t
x,b
_)) = t -> t
f t
x
    fm t -> t
f (Node i
_ Tree i (t, b)
l Tree i (t, b)
r) = (t -> t) -> Tree i (t, b) -> t
fm t -> t
f Tree i (t, b)
l t -> t -> t
forall a. Semigroup a => a -> a -> a
<> (t -> t) -> Tree i (t, b) -> t
fm t -> t
f Tree i (t, b)
r
  

instance (Entity x, Entity i, Ord i) => Validable (PTree i x) where
  valid :: PTree i x -> Statement
valid (PTree Maybe (Tree i (x, i))
mt) = String -> Label
Label String
"PTree" Label -> Statement -> Statement
:<=>: case Maybe (Tree i (x, i))
mt of
    Maybe (Tree i (x, i))
Nothing -> Statement
SValid
    Just Tree i (x, i)
t  -> Tree i (x, i) -> Statement
forall {a} {a}.
(Validable a, Validable a, Ord a, Show a) =>
Tree a (a, a) -> Statement
vld Tree i (x, i)
t where
      vld :: Tree a (a, a) -> Statement
vld (Node a
i Tree a (a, a)
l Tree a (a, a)
r)  = a -> Statement
forall a. Validable a => a -> Statement
valid a
i Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& a -> Tree a (a, a) -> Statement
vldl a
i Tree a (a, a)
l Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& a -> Tree a (a, a) -> Statement
vldr a
i Tree a (a, a)
r
      vld (Leaf (a
x,a
i))  = a -> Statement
forall a. Validable a => a -> Statement
valid a
i Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& a -> Statement
forall a. Validable a => a -> Statement
valid a
x
  
      vldl :: a -> Tree a (a, a) -> Statement
vldl a
i Tree a (a, a)
t = String -> Label
Label String
"l" Label -> Statement -> Statement
:<=>: case Tree a (a, a)
t of
        Leaf (a
_,a
i') -> [Statement] -> Statement
And [ Tree a (a, a) -> Statement
vld Tree a (a, a)
t
                           , (a
i' a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
i) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"i"String -> String -> Parameter
:=a -> String
forall a. Show a => a -> String
show a
i,String
"i'"String -> String -> Parameter
:=a -> String
forall a. Show a => a -> String
show a
i']
                           ]
        Node a
i' Tree a (a, a)
l Tree a (a, a)
r -> a -> Statement
forall a. Validable a => a -> Statement
valid a
i' Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& a -> Tree a (a, a) -> Statement
vldl a
i' Tree a (a, a)
l Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& a -> Tree a (a, a) -> Statement
vldr a
i' Tree a (a, a)
r
        
      vldr :: a -> Tree a (a, a) -> Statement
vldr a
i Tree a (a, a)
t = String -> Label
Label String
"r" Label -> Statement -> Statement
:<=>: case Tree a (a, a)
t of
        Leaf (a
_,a
i') -> [Statement] -> Statement
And [ Tree a (a, a) -> Statement
vld Tree a (a, a)
t
                           , (a
i a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
i') Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"i"String -> String -> Parameter
:=a -> String
forall a. Show a => a -> String
show a
i,String
"i'"String -> String -> Parameter
:=a -> String
forall a. Show a => a -> String
show a
i']
                           ]
        Node a
i' Tree a (a, a)
l Tree a (a, a)
r -> a -> Statement
forall a. Validable a => a -> Statement
valid a
i' Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& a -> Tree a (a, a) -> Statement
vldl a
i' Tree a (a, a)
l Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& a -> Tree a (a, a) -> Statement
vldr a
i' Tree a (a, a)
r
    
-- instance (Entity x, Entity i, Ord i) => Entity (PTree i x)

--------------------------------------------------------------------------------
-- ptrEmpty -

-- | the empty 'PTree'.
ptrEmpty :: PTree i x
ptrEmpty :: forall i x. PTree i x
ptrEmpty = Maybe (Tree i (x, i)) -> PTree i x
forall i x. Maybe (Tree i (x, i)) -> PTree i x
PTree Maybe (Tree i (x, i))
forall {a}. Maybe a
Nothing

--------------------------------------------------------------------------------
-- psqTree -

-- | the induced tree.
psqTree :: PSequence i x -> PTree i x
psqTree :: forall i x. PSequence i x -> PTree i x
psqTree (PSequence [])  = Maybe (Tree i (x, i)) -> PTree i x
forall i x. Maybe (Tree i (x, i)) -> PTree i x
PTree Maybe (Tree i (x, i))
forall {a}. Maybe a
Nothing
psqTree (PSequence [(x, i)]
xis) = Maybe (Tree i (x, i)) -> PTree i x
forall i x. Maybe (Tree i (x, i)) -> PTree i x
PTree (Maybe (Tree i (x, i)) -> PTree i x)
-> Maybe (Tree i (x, i)) -> PTree i x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Tree i (x, i) -> Maybe (Tree i (x, i))
forall a. a -> Maybe a
Just (Tree i (x, i) -> Maybe (Tree i (x, i)))
-> Tree i (x, i) -> Maybe (Tree i (x, i))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(x, i)] -> Tree i (x, i)
forall {a} {i}. [(a, i)] -> Tree i (a, i)
toTree [(x, i)]
xis where
  toTree :: [(a, i)] -> Tree i (a, i)
toTree [(a, i)
xi] = (a, i) -> Tree i (a, i)
forall i x. x -> Tree i x
Leaf (a, i)
xi
  toTree [(a, i)]
xis  = i -> Tree i (a, i) -> Tree i (a, i) -> Tree i (a, i)
forall i x. i -> Tree i x -> Tree i x -> Tree i x
Node ((a, i) -> i
forall a b. (a, b) -> b
snd ((a, i) -> i) -> (a, i) -> i
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(a, i)] -> (a, i)
forall a. HasCallStack => [a] -> a
head [(a, i)]
r) ([(a, i)] -> Tree i (a, i)
toTree [(a, i)]
l) ([(a, i)] -> Tree i (a, i)
toTree [(a, i)]
r) where
    ([(a, i)]
l,[(a, i)]
r) = Int -> [(a, i)] -> ([(a, i)], [(a, i)])
forall a. Int -> [a] -> ([a], [a])
splitAt ([(a, i)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(a, i)]
xis Int -> Int -> Int
`divInt` Int
2) [(a, i)]
xis

--------------------------------------------------------------------------------
-- psqFromTree -

-- | the induced partially sequence.
psqFromTree :: PTree i x -> PSequence i x
psqFromTree :: forall i x. PTree i x -> PSequence i x
psqFromTree (PTree Maybe (Tree i (x, i))
Nothing)  = PSequence i x
forall i x. PSequence i x
psqEmpty
psqFromTree (PTree (Just Tree i (x, i)
t)) = [(x, i)] -> PSequence i x
forall i x. [(x, i)] -> PSequence i x
PSequence ([(x, i)] -> PSequence i x) -> [(x, i)] -> PSequence i x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Tree i (x, i) -> [(x, i)]
forall a. Tree i a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Tree i (x, i)
t

--------------------------------------------------------------------------------
-- ptrxs -

-- | the underlying list of indexed values.
ptrxs :: PTree i x -> [(x,i)]
ptrxs :: forall i x. PTree i x -> [(x, i)]
ptrxs = PSequence i x -> [(x, i)]
forall i x. PSequence i x -> [(x, i)]
psqxs (PSequence i x -> [(x, i)])
-> (PTree i x -> PSequence i x) -> PTree i x -> [(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
. PTree i x -> PSequence i x
forall i x. PTree i x -> PSequence i x
psqFromTree

--------------------------------------------------------------------------------
-- ptrx -

-- | retrieving a value from the tree.
ptrx :: Ord i => PTree i x -> i -> Maybe x
ptrx :: forall i x. Ord i => PTree i x -> i -> Maybe x
ptrx (PTree Maybe (Tree i (x, i))
Nothing)  i
_ = Maybe x
forall {a}. Maybe a
Nothing
ptrx (PTree (Just Tree i (x, i)
t)) i
i = if i
i' i -> i -> Bool
forall a. Eq a => a -> a -> Bool
== i
i then x -> Maybe x
forall a. a -> Maybe a
Just x
x else Maybe x
forall {a}. Maybe a
Nothing where (x
x,i
i') = Tree i (x, i) -> i -> (x, i)
forall i x. Ord i => Tree i x -> i -> x
trLookup Tree i (x, i)
t i
i

--------------------------------------------------------------------------------
-- ptrMin -

-- | the minimal index.
ptrMin :: PTree i x -> Closure i
ptrMin :: forall i x. PTree i x -> Closure i
ptrMin (PTree Maybe (Tree i (x, i))
Nothing)  = Closure i
forall x. Closure x
PosInf
ptrMin (PTree (Just Tree i (x, i)
t)) = Tree i (x, i) -> Closure i
forall {i} {a} {x}. Tree i (a, x) -> Closure x
pmin Tree i (x, i)
t where
  pmin :: Tree i (a, x) -> Closure x
pmin (Leaf (a
_,x
i)) = x -> Closure x
forall x. x -> Closure x
It x
i
  pmin (Node i
_ Tree i (a, x)
l Tree i (a, x)
_) = Tree i (a, x) -> Closure x
pmin Tree i (a, x)
l

--------------------------------------------------------------------------------
-- ptrMax -

-- | the maximal index.
ptrMax :: PTree i x -> Closure i
ptrMax :: forall i x. PTree i x -> Closure i
ptrMax (PTree Maybe (Tree i (x, i))
Nothing)  = Closure i
forall x. Closure x
NegInf
ptrMax (PTree (Just Tree i (x, i)
t)) = Tree i (x, i) -> Closure i
forall {i} {a} {x}. Tree i (a, x) -> Closure x
pmax Tree i (x, i)
t where
  pmax :: Tree i (a, x) -> Closure x
pmax (Leaf (a
_,x
i)) = x -> Closure x
forall x. x -> Closure x
It x
i
  pmax (Node i
_ Tree i (a, x)
_ Tree i (a, x)
r) = Tree i (a, x) -> Closure x
pmax Tree i (a, x)
r

--------------------------------------------------------------------------------
-- ptrSpan -

-- | the span, i.e the minimal and the maximal index of the tree.
ptrSpan :: PTree i x -> Span i
ptrSpan :: forall i x. PTree i x -> Span i
ptrSpan PTree i x
t = (PTree i x -> Closure i
forall i x. PTree i x -> Closure i
ptrMin PTree i x
t,PTree i x -> Closure i
forall i x. PTree i x -> Closure i
ptrMax PTree i x
t)

--------------------------------------------------------------------------------
-- ptrFilter -

-- | the sub tree containing all leafs satisfying the given predicate.
ptrFilter :: (x -> Bool) -> PTree i x -> PTree i x
ptrFilter :: forall x i. (x -> Bool) -> PTree i x -> PTree i x
ptrFilter x -> Bool
p (PTree Maybe (Tree i (x, i))
t) = Maybe (Tree i (x, i)) -> PTree i x
forall i x. Maybe (Tree i (x, i)) -> PTree i x
PTree (Maybe (Tree i (x, i))
t Maybe (Tree i (x, i))
-> (Tree i (x, i) -> Maybe (Tree i (x, i)))
-> Maybe (Tree i (x, i))
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ((x, i) -> Bool) -> Tree i (x, i) -> Maybe (Tree i (x, i))
forall x i. (x -> Bool) -> Tree i x -> Maybe (Tree i x)
trFilter (x -> Bool
p (x -> Bool) -> ((x, i) -> x) -> (x, i) -> 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
. (x, i) -> x
forall a b. (a, b) -> a
fst))

--------------------------------------------------------------------------------
-- ptrFilterWithIndex -

-- | the sub tree containing all leafs satisfying the given indexed predicate.
ptrFilterWithIndex :: ((x,i) -> Bool) -> PTree i x -> PTree i x
ptrFilterWithIndex :: forall x i. ((x, i) -> Bool) -> PTree i x -> PTree i x
ptrFilterWithIndex (x, i) -> Bool
p (PTree Maybe (Tree i (x, i))
t) = Maybe (Tree i (x, i)) -> PTree i x
forall i x. Maybe (Tree i (x, i)) -> PTree i x
PTree (Maybe (Tree i (x, i))
t Maybe (Tree i (x, i))
-> (Tree i (x, i) -> Maybe (Tree i (x, i)))
-> Maybe (Tree i (x, i))
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ((x, i) -> Bool) -> Tree i (x, i) -> Maybe (Tree i (x, i))
forall x i. (x -> Bool) -> Tree i x -> Maybe (Tree i x)
trFilter (x, i) -> Bool
p)

--------------------------------------------------------------------------------
-- ptrMapWithIndex -

-- | maps a 'PTree' according to the given strict monotone mapping and the given indexed
-- mapping.
ptrMapWithIndex :: Monotone i j -> ((x,i) -> y) -> PTree i x -> PTree j y
ptrMapWithIndex :: forall i j x y.
Monotone i j -> ((x, i) -> y) -> PTree i x -> PTree j y
ptrMapWithIndex Monotone i j
_ (x, i) -> y
_ (PTree Maybe (Tree i (x, i))
Nothing)           = Maybe (Tree j (y, j)) -> PTree j y
forall i x. Maybe (Tree i (x, i)) -> PTree i x
PTree Maybe (Tree j (y, j))
forall {a}. Maybe a
Nothing
ptrMapWithIndex (Monotone i -> j
j) (x, i) -> y
y (PTree (Just Tree i (x, i)
t)) = Maybe (Tree j (y, j)) -> PTree j y
forall i x. Maybe (Tree i (x, i)) -> PTree i x
PTree (Maybe (Tree j (y, j)) -> PTree j y)
-> Maybe (Tree j (y, j)) -> PTree j y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Tree j (y, j) -> Maybe (Tree j (y, j))
forall a. a -> Maybe a
Just (Tree j (y, j) -> Maybe (Tree j (y, j)))
-> Tree j (y, j) -> Maybe (Tree j (y, j))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Tree i (x, i) -> Tree j (y, j)
mapwi Tree i (x, i)
t where
  mapwi :: Tree i (x, i) -> Tree j (y, j)
mapwi (Leaf (x, i)
xi)    = (y, j) -> Tree j (y, j)
forall i x. x -> Tree i x
Leaf ((x, i) -> y
y (x, i)
xi,i -> j
j (i -> j) -> i -> j
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (x, i) -> i
forall a b. (a, b) -> b
snd (x, i)
xi)
  mapwi (Node i
i Tree i (x, i)
l Tree i (x, i)
r) = j -> Tree j (y, j) -> Tree j (y, j) -> Tree j (y, j)
forall i x. i -> Tree i x -> Tree i x -> Tree i x
Node (i -> j
j i
i) (Tree i (x, i) -> Tree j (y, j)
mapwi Tree i (x, i)
l) (Tree i (x, i) -> Tree j (y, j)
mapwi Tree i (x, i)
r)

--------------------------------------------------------------------------------
-- ptrMapShift -

-- | shifts the indices of a 'PTree'.
ptrMapShift :: Number i => i -> ((x,i) -> y) -> PTree i x -> PTree i y
ptrMapShift :: forall i x y.
Number i =>
i -> ((x, i) -> y) -> PTree i x -> PTree i y
ptrMapShift i
t = Monotone i i -> ((x, i) -> y) -> PTree i x -> PTree i y
forall i j x y.
Monotone i j -> ((x, i) -> y) -> PTree i x -> PTree j y
ptrMapWithIndex ((i -> i) -> Monotone i i
forall i j. (i -> j) -> Monotone i j
Monotone (i -> i -> i
forall a. Additive a => a -> a -> a
+i
t))

--------------------------------------------------------------------------------
-- ptrMap -

-- | maps a 'PTree' according to the given mapping.
ptrMap :: (x -> y) -> PTree i x -> PTree i y
ptrMap :: forall x y i. (x -> y) -> PTree i x -> PTree i y
ptrMap x -> y
f = Monotone i i -> ((x, i) -> y) -> PTree i x -> PTree i y
forall i j x y.
Monotone i j -> ((x, i) -> y) -> PTree i x -> PTree j y
ptrMapWithIndex ((i -> i) -> Monotone i i
forall i j. (i -> j) -> Monotone i j
Monotone i -> i
forall x. x -> x
id) (x -> y
f (x -> y) -> ((x, i) -> x) -> (x, i) -> y
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
. (x, i) -> x
forall a b. (a, b) -> a
fst)

instance M.Functor (PTree i) where fmap :: forall a b. (a -> b) -> PTree i a -> PTree i b
fmap = (a -> b) -> PTree i a -> PTree i b
forall x y i. (x -> y) -> PTree i x -> PTree i y
ptrMap

--------------------------------------------------------------------------------
-- prpTreeFilter -

-- | validates the function 'ptrFilter'.
prpPTreeFilter :: N -> Statement
prpPTreeFilter :: N -> Statement
prpPTreeFilter N
n = String -> Label
Prp (String
"PTreeFilter " String -> ShowS
forall a. [a] -> [a] -> [a]
++ N -> String
forall a. Show a => a -> String
show N
n) Label -> Statement -> Statement
:<=>:
  X (PSequence N Z) -> (PSequence N Z -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (PSequence N Z)
xps (\PSequence N Z
pxs -> (  (((Z, N) -> Bool) -> [(Z, N)] -> [(Z, N)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Z -> Bool
forall {a}. (Integral a, Num a) => a -> Bool
p (Z -> Bool) -> ((Z, N) -> Z) -> (Z, N) -> 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
. (Z, N) -> Z
forall a b. (a, b) -> a
fst) ([(Z, N)] -> [(Z, N)]) -> [(Z, N)] -> [(Z, N)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ PSequence N Z -> [(Z, N)]
forall i x. PSequence i x -> [(x, i)]
psqxs PSequence N Z
pxs)
                      [(Z, N)] -> [(Z, N)] -> Bool
forall a. Eq a => a -> a -> Bool
== (PSequence N Z -> [(Z, N)]
forall i x. PSequence i x -> [(x, i)]
psqxs (PSequence N Z -> [(Z, N)]) -> PSequence N Z -> [(Z, N)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ PTree N Z -> PSequence N Z
forall i x. PTree i x -> PSequence i x
psqFromTree (PTree N Z -> PSequence N Z) -> PTree N Z -> PSequence N Z
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (Z -> Bool) -> PTree N Z -> PTree N Z
forall x i. (x -> Bool) -> PTree i x -> PTree i x
ptrFilter Z -> Bool
forall {a}. (Integral a, Num a) => a -> Bool
p (PTree N Z -> PTree N Z) -> PTree N Z -> PTree N Z
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ PSequence N Z -> PTree N Z
forall i x. PSequence i x -> PTree i x
psqTree PSequence N Z
pxs)
                      ) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"pxs"String -> String -> Parameter
:=PSequence N Z -> String
forall a. Show a => a -> String
show PSequence N Z
pxs]
             ) where

  xps :: X (PSequence N Z)
xps = [(Q, X (PSequence N Z))] -> X (PSequence N Z)
forall a. [(Q, X a)] -> X a
xOneOfXW [(Q
1,PSequence N Z -> X (PSequence N Z)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return PSequence N Z
forall i x. PSequence i x
psqEmpty),(Q
100,N -> N -> X Z -> X N -> X (PSequence N Z)
forall i x. Ord i => N -> N -> X x -> X i -> X (PSequence i x)
xPSequence N
n N
n (Z -> Z -> X Z
xZB (-Z
100) Z
100) X N
xN)]
  p :: a -> Bool
p a
x = a
x a -> a -> a
forall a. Integral a => a -> a -> a
`mod` a
2 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
0

--------------------------------------------------------------------------------
-- prpMapShiftPSequence -

-- | validates the shifting of a 'PSequence' and 'PTree'.
prpMapShiftPSequence :: N -> Statement
prpMapShiftPSequence :: N -> Statement
prpMapShiftPSequence N
n = String -> Label
Prp String
"ShiftPSequencePTree" Label -> Statement -> Statement
:<=>:
  X (PSequence Z Z, Z, (Z, Z) -> Z)
-> ((PSequence Z Z, Z, (Z, Z) -> Z) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (PSequence Z Z, Z, (Z, Z) -> Z)
xxitf (\  (PSequence Z Z
xis,Z
t,(Z, Z) -> Z
f)
               ->  let xis' :: PTree Z Z
xis' = Z -> ((Z, Z) -> Z) -> PTree Z Z -> PTree Z Z
forall i x y.
Number i =>
i -> ((x, i) -> y) -> PTree i x -> PTree i y
ptrMapShift Z
t (Z, Z) -> Z
f (PTree Z Z -> PTree Z Z) -> PTree Z Z -> PTree Z Z
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ PSequence Z Z -> PTree Z Z
forall i x. PSequence i x -> PTree i x
psqTree PSequence Z Z
xis in
                     [Statement] -> Statement
And [ Z -> Statement
forall a. Validable a => a -> Statement
valid Z
t
                         , (Z -> ((Z, Z) -> Z) -> PSequence Z Z -> PSequence Z Z
forall i x y.
Number i =>
i -> ((x, i) -> y) -> PSequence i x -> PSequence i y
psqMapShift Z
t (Z, Z) -> Z
f PSequence Z Z
xis PSequence Z Z -> PSequence Z Z -> Bool
forall a. Eq a => a -> a -> Bool
== PTree Z Z -> PSequence Z Z
forall i x. PTree i x -> PSequence i x
psqFromTree PTree Z Z
xis')
                             Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"xis"String -> String -> Parameter
:=PSequence Z Z -> String
forall a. Show a => a -> String
show PSequence Z Z
xis,String
"t"String -> String -> Parameter
:=Z -> String
forall a. Show a => a -> String
show Z
t]
                         ]
               )

  where xxitf :: X (PSequence Z Z,Z,(Z,Z) -> Z)
        xxitf :: X (PSequence Z Z, Z, (Z, Z) -> Z)
xxitf = X (PSequence Z Z)
-> X Z -> X ((Z, Z) -> Z) -> X (PSequence Z Z, Z, (Z, Z) -> Z)
forall a b c. X a -> X b -> X c -> X (a, b, c)
xTupple3 (N -> N -> X Z -> X Z -> X (PSequence Z Z)
forall i x. Ord i => N -> N -> X x -> X i -> X (PSequence i x)
xPSequence N
n N
n X Z
xZ X Z
xZ) X Z
xZ X ((Z, Z) -> Z)
xf
        xf :: X ((Z, Z) -> Z)
xf = [(Z, Z) -> Z] -> X ((Z, Z) -> Z)
forall a. [a] -> X a
xOneOf [(Z -> Z -> Z) -> (Z, Z) -> Z
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Z -> Z -> Z
forall a. Additive a => a -> a -> a
(+),(Z -> Z -> Z) -> (Z, Z) -> Z
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (-)]
  
--------------------------------------------------------------------------------
-- prpPSequence -

-- | validity of 'PSequence'.
prpPSequence :: Statement
prpPSequence :: Statement
prpPSequence = String -> Label
Prp String
"PSequence"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ N -> Statement
prpPTreeFilter N
60
            , N -> Statement
prpMapShiftPSequence N
76
            ]