{-# LANGUAGE NoImplicitPrelude #-}

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

-- |
-- Module      : OAlg.Entity.Sequence.Set
-- Description : sets of ordered entities
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- sets of ordered entities.
module OAlg.Entity.Sequence.Set
  ( 
    -- * Set
    Set(..), set, setSpan, setxs, setSqc, setMap, isSubSet

    -- * Operations
  , setEmpty, setUnion

    -- * Lookup
  , setIndex 

    -- * X
  , xSet

    -- * Propositions
  , prpSetUnion

  ) where

import Control.Monad

import Data.Foldable
import Data.List (head,sort,group,map,filter,zip)

import OAlg.Prelude

import OAlg.Data.Tree

import OAlg.Structure.Number

--------------------------------------------------------------------------------
-- Set -

-- | set of ordered entities in @__x__@.
--
--  __Property__ Let @s = 'Set' xs@ be in @'Set' __x__@ for a ordered 'Entity' type @__x__@,
--  then holds:
--
--  (1) For all @..x':'y..@ in @xs@ holds: @x '<' y@.
--
--  (2) @'lengthN' s '==' 'lengthN' xs@.
newtype Set x = Set [x] deriving (Int -> Set x -> ShowS
forall x. Show x => Int -> Set x -> ShowS
forall x. Show x => [Set x] -> ShowS
forall x. Show x => Set x -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Set x] -> ShowS
$cshowList :: forall x. Show x => [Set x] -> ShowS
show :: Set x -> String
$cshow :: forall x. Show x => Set x -> String
showsPrec :: Int -> Set x -> ShowS
$cshowsPrec :: forall x. Show x => Int -> Set x -> ShowS
Show,Set x -> Set x -> Bool
forall x. Eq x => Set x -> Set x -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Set x -> Set x -> Bool
$c/= :: forall x. Eq x => Set x -> Set x -> Bool
== :: Set x -> Set x -> Bool
$c== :: forall x. Eq x => Set x -> Set x -> Bool
Eq,Set x -> N
forall x. Set x -> N
forall x. (x -> N) -> LengthN x
lengthN :: Set x -> N
$clengthN :: forall x. Set x -> N
LengthN,forall a. Eq a => a -> Set a -> Bool
forall a. Num a => Set a -> a
forall a. Ord a => Set a -> a
forall m. Monoid m => Set m -> m
forall a. Set a -> Bool
forall a. Set a -> Int
forall a. Set a -> [a]
forall a. (a -> a -> a) -> Set a -> a
forall m a. Monoid m => (a -> m) -> Set a -> m
forall b a. (b -> a -> b) -> b -> Set a -> b
forall a b. (a -> b -> b) -> b -> Set 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 => Set a -> a
$cproduct :: forall a. Num a => Set a -> a
sum :: forall a. Num a => Set a -> a
$csum :: forall a. Num a => Set a -> a
minimum :: forall a. Ord a => Set a -> a
$cminimum :: forall a. Ord a => Set a -> a
maximum :: forall a. Ord a => Set a -> a
$cmaximum :: forall a. Ord a => Set a -> a
elem :: forall a. Eq a => a -> Set a -> Bool
$celem :: forall a. Eq a => a -> Set a -> Bool
length :: forall a. Set a -> Int
$clength :: forall a. Set a -> Int
null :: forall a. Set a -> Bool
$cnull :: forall a. Set a -> Bool
toList :: forall a. Set a -> [a]
$ctoList :: forall a. Set a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Set a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Set a -> a
foldr1 :: forall a. (a -> a -> a) -> Set a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Set a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Set a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Set a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Set a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Set a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Set a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Set a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Set a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Set a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Set a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Set a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Set a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Set a -> m
fold :: forall m. Monoid m => Set m -> m
$cfold :: forall m. Monoid m => Set m -> m
Foldable)

relSet :: (Validable x, Ord x, Show x) => Set x -> Statement
relSet :: forall x. (Validable x, Ord x, Show x) => Set x -> Statement
relSet (Set [])     = Statement
SValid
relSet (Set (x
x:[x]
xs)) = forall a. Validable a => a -> Statement
valid x
x forall b. Boolean b => b -> b -> b
&& forall {t} {t}.
(Validable t, Ord t, Show t, Show t, Enum t) =>
t -> t -> [t] -> Statement
vld (N
0::N) x
x [x]
xs where
  vld :: t -> t -> [t] -> Statement
vld t
_ t
_ []     = Statement
SValid
  vld t
i t
x (t
y:[t]
xs) = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid t
y
                       , (t
xforall a. Ord a => a -> a -> Bool
<t
y) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"i"String -> String -> Parameter
:=forall a. Show a => a -> String
show t
i,String
"(x,y)"String -> String -> Parameter
:=forall a. Show a => a -> String
show (t
x,t
y)]
                       , t -> t -> [t] -> Statement
vld (forall a. Enum a => a -> a
succ t
i) t
y [t]
xs
                       ]

instance (Validable x, Ord x, Show x) => Validable (Set x) where
  valid :: Set x -> Statement
valid Set x
xs = String -> Label
Label String
"Set" Label -> Statement -> Statement
:<=>: forall x. (Validable x, Ord x, Show x) => Set x -> Statement
relSet Set x
xs

instance (Entity x, Ord x) => Entity (Set x)

--------------------------------------------------------------------------------
-- set -

-- | makes a set from the given list.
set :: Ord x => [x] -> Set x
set :: forall x. Ord x => [x] -> Set x
set = forall x. [x] -> Set x
Set forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall a. [a] -> a
head forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall a. Eq a => [a] -> [[a]]
group forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall a. Ord a => [a] -> [a]
sort

--------------------------------------------------------------------------------
-- setxs -

-- | the elements of a set.
setxs :: Set x -> [x]
setxs :: forall a. Set a -> [a]
setxs (Set [x]
xs) = [x]
xs

--------------------------------------------------------------------------------
-- setSpan -

-- | the span of a set.
setSpan :: Set x -> Span x
setSpan :: forall x. Set x -> Span x
setSpan (Set [])     = (forall x. Closer x
PosInf,forall x. Closer x
NegInf)
setSpan (Set (x
x:[x]
xs)) = (forall x. x -> Closer x
It x
x,forall {t}. t -> [t] -> Closer t
last x
x [x]
xs) where
  last :: t -> [t] -> Closer t
last t
x []     = forall x. x -> Closer x
It t
x
  last t
_ (t
x:[t]
xs) = t -> [t] -> Closer t
last t
x [t]
xs

--------------------------------------------------------------------------------
-- setMap -

-- | mapping of sets.
--
--  __Note__ This works only for finite sets!
setMap :: Ord y => (x -> y) -> Set x -> Set y
setMap :: forall y x. Ord y => (x -> y) -> Set x -> Set y
setMap x -> y
f (Set [x]
xs) = forall x. [x] -> Set x
Set forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. Ord a => [a] -> [a]
sort forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map x -> y
f [x]
xs

--------------------------------------------------------------------------------
-- setSqc -

-- | mapping a set.
setSqc :: Ord x => (i -> Maybe x) -> Set i -> Set x
setSqc :: forall x i. Ord x => (i -> Maybe x) -> Set i -> Set x
setSqc i -> Maybe x
mx (Set [i]
is)
  = forall x. [x] -> Set x
Set
  forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. Ord a => [a] -> [a]
sort
  forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. HasCallStack => Maybe a -> a
fromJust
  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 (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map i -> Maybe x
mx [i]
is

--------------------------------------------------------------------------------
-- setEmpty -

-- | the empty set.
setEmpty :: Set x
setEmpty :: forall x. Set x
setEmpty = forall x. [x] -> Set x
Set []

--------------------------------------------------------------------------------
-- setUnion -

-- | the union of two sets.
setUnion :: Ord x => Set x -> Set x -> Set x
setUnion :: forall x. Ord x => Set x -> Set x -> Set x
setUnion (Set [x]
xs) (Set [x]
ys) = forall x. [x] -> Set x
Set forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall {a}. Ord a => [a] -> [a] -> [a]
un [x]
xs [x]
ys where
  un :: [a] -> [a] -> [a]
un [] [a]
ys = [a]
ys
  un [a]
xs [] = [a]
xs
  un xs :: [a]
xs@(a
x:[a]
xs') ys :: [a]
ys@(a
y:[a]
ys') = case a
x forall a. Ord a => a -> a -> Ordering
`compare` a
y of
    Ordering
LT -> a
xforall a. a -> [a] -> [a]
:[a] -> [a] -> [a]
un [a]
xs' [a]
ys
    Ordering
EQ -> a
xforall a. a -> [a] -> [a]
:[a] -> [a] -> [a]
un [a]
xs' [a]
ys'
    Ordering
GT -> a
yforall a. a -> [a] -> [a]
:[a] -> [a] -> [a]
un [a]
xs  [a]
ys'

--------------------------------------------------------------------------------
-- isSubSet -

-- | checks for being a sub set.
isSubSet :: Ord x => Set x -> Set x -> Bool
isSubSet :: forall x. Ord x => Set x -> Set x -> Bool
isSubSet (Set [x]
xs) (Set [x]
ys) = forall {a}. Ord a => [a] -> [a] -> Bool
sbs [x]
xs [x]
ys where
  sbs :: [a] -> [a] -> Bool
sbs [] [a]
_             = Bool
True
  sbs [a]
_ []             = Bool
False
  sbs xs :: [a]
xs@(a
x:[a]
xs') (a
y:[a]
ys') = case a
x forall a. Ord a => a -> a -> Ordering
`compare` a
y of
    Ordering
LT -> Bool
False
    Ordering
EQ -> [a] -> [a] -> Bool
sbs [a]
xs' [a]
ys'
    Ordering
GT -> [a] -> [a] -> Bool
sbs [a]
xs [a]
ys'

--------------------------------------------------------------------------------
-- setIndex -

-- | the index of an element, where the elements of the given set are indexed from @0@.
--
--  __Examples__
--
-- >>> setIndex (Set ['a'..'x']) 'c'
-- Just 2
setIndex :: Ord x => Set x -> x -> Maybe N
setIndex :: forall x. Ord x => Set x -> x -> Maybe N
setIndex (Set []) = forall b a. b -> a -> b
const forall a. Maybe a
Nothing
setIndex (Set [x]
xs) = \x
x -> let (x
x',N
i) = forall i x. Ord i => Tree i x -> i -> x
lookup Tree x (x, N)
xs' x
x in if x
x' forall a. Eq a => a -> a -> Bool
== x
x then forall a. a -> Maybe a
Just N
i else forall a. Maybe a
Nothing
  where
    xs' :: Tree x (x, N)
xs' = forall x. Ord x => [(x, N)] -> Tree x (x, N)
lt ([x]
xs forall a b. [a] -> [b] -> [(a, b)]
`zip` [N
0..])

    lt :: Ord x => [(x,N)] -> Tree x (x,N)
    lt :: forall x. Ord x => [(x, N)] -> Tree x (x, N)
lt [(x, N)
xi] = forall i x. x -> Tree i x
Leaf (x, N)
xi
    lt [(x, N)]
xis  = forall i x. i -> Tree i x -> Tree i x -> Tree i x
Node (forall a b. (a, b) -> a
fst forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. [a] -> a
head [(x, N)]
xisR) (forall x. Ord x => [(x, N)] -> Tree x (x, N)
lt [(x, N)]
xisL) (forall x. Ord x => [(x, N)] -> Tree x (x, N)
lt [(x, N)]
xisR) where
      ([(x, N)]
xisL,[(x, N)]
xisR) = forall x. N -> [x] -> ([x], [x])
splitAtN (forall x. LengthN x => x -> N
lengthN [(x, N)]
xis forall a. Integral a => a -> a -> a
`div` N
2) [(x, N)]
xis

--------------------------------------------------------------------------------
-- Set - POrd -

instance Ord x => POrd (Set x) where
  <<= :: Set x -> Set x -> Bool
(<<=) = forall x. Ord x => Set x -> Set x -> Bool
isSubSet  

--------------------------------------------------------------------------------
-- xSet -

-- | random variable of sets with maximal the given length.
xSet :: Ord x => N -> X x -> X (Set x)
xSet :: forall x. Ord x => N -> X x -> X (Set x)
xSet N
n X x
xx = do
  [x]
xs <- forall x. N -> X x -> X [x]
xTakeN N
n X x
xx
  forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x. [x] -> Set x
Set forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. [a] -> a
head forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. Eq a => [a] -> [[a]]
group forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. Ord a => [a] -> [a]
sort [x]
xs


--------------------------------------------------------------------------------
-- prpSetUnion -

-- | validity for the union operator of sets.
prpSetUnion :: (Ord x, Show x) => X (Set x) -> Statement
prpSetUnion :: forall x. (Ord x, Show x) => X (Set x) -> Statement
prpSetUnion X (Set x)
x = String -> Label
Prp String
"SetUnion" Label -> Statement -> Statement
:<=>:
  forall x. X x -> (x -> Statement) -> Statement
Forall X (Set x, Set x)
xy (\(Set x
x,Set x
y)
             -> let xy :: Set x
xy = Set x
x forall x. Ord x => Set x -> Set x -> Set x
`setUnion` Set x
y in
                  [Statement] -> Statement
And [ String -> Label
Label String
"x"
                        Label -> Statement -> Statement
:<=>: (Set x
x forall x. Ord x => Set x -> Set x -> Bool
`isSubSet` Set x
xy) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"x"String -> String -> Parameter
:=forall a. Show a => a -> String
show Set x
x, String
"xy"String -> String -> Parameter
:=forall a. Show a => a -> String
show Set x
xy]
                      , String -> Label
Label String
"y"
                        Label -> Statement -> Statement
:<=>: (Set x
y forall x. Ord x => Set x -> Set x -> Bool
`isSubSet` Set x
xy) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"y"String -> String -> Parameter
:=forall a. Show a => a -> String
show Set x
y, String
"xy"String -> String -> Parameter
:=forall a. Show a => a -> String
show Set x
xy]
                      ]
            ) 
  where xy :: X (Set x, Set x)
xy = forall a b. X a -> X b -> X (a, b)
xTupple2 X (Set x)
x X (Set x)
x