{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# 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
  , setPower, setFilter, setTakeN

    -- * Operations

  , setEmpty, setIsEmpty, setUnion, setIntersection, setDifference

    -- * Lookup

  , setIndex 

    -- * X

  , xSet

    -- * Propositions

  , prpSetUnion

  ) where

import Control.Monad

import Data.Foldable
import Data.List as L (head,sort,group,map,zip,(++))

import OAlg.Prelude

import OAlg.Category.Map

import OAlg.Data.Tree
import OAlg.Data.Filterable

import OAlg.Structure.Number
import OAlg.Structure.PartiallyOrdered as P
import OAlg.Structure.Lattice.Definition

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

-- 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@.

--

--  __Note__ The canonical ordering 'Ord' and the subset ordering 'PartiallyOrdered' are not equivalent.

newtype Set x = Set [x] deriving (Int -> Set x -> ShowS
[Set x] -> ShowS
Set x -> String
(Int -> Set x -> ShowS)
-> (Set x -> String) -> ([Set x] -> ShowS) -> Show (Set x)
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
$cshowsPrec :: forall x. Show x => Int -> Set x -> ShowS
showsPrec :: Int -> Set x -> ShowS
$cshow :: forall x. Show x => Set x -> String
show :: Set x -> String
$cshowList :: forall x. Show x => [Set x] -> ShowS
showList :: [Set x] -> ShowS
Show,Set x -> Set x -> Bool
(Set x -> Set x -> Bool) -> (Set x -> Set x -> Bool) -> Eq (Set x)
forall x. Eq x => Set x -> Set x -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: Set x -> Set x -> Bool
Eq,Eq (Set x)
Eq (Set x) =>
(Set x -> Set x -> Ordering)
-> (Set x -> Set x -> Bool)
-> (Set x -> Set x -> Bool)
-> (Set x -> Set x -> Bool)
-> (Set x -> Set x -> Bool)
-> (Set x -> Set x -> Set x)
-> (Set x -> Set x -> Set x)
-> Ord (Set x)
Set x -> Set x -> Bool
Set x -> Set x -> Ordering
Set x -> Set x -> Set 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 x. Ord x => Eq (Set x)
forall x. Ord x => Set x -> Set x -> Bool
forall x. Ord x => Set x -> Set x -> Ordering
forall x. Ord x => Set x -> Set x -> Set x
$ccompare :: forall x. Ord x => Set x -> Set x -> Ordering
compare :: Set x -> Set x -> Ordering
$c< :: forall x. Ord x => Set x -> Set x -> Bool
< :: Set x -> Set x -> Bool
$c<= :: forall x. Ord x => Set x -> Set x -> Bool
<= :: Set x -> Set x -> Bool
$c> :: forall x. Ord x => Set x -> Set x -> Bool
> :: Set x -> Set x -> Bool
$c>= :: forall x. Ord x => Set x -> Set x -> Bool
>= :: Set x -> Set x -> Bool
$cmax :: forall x. Ord x => Set x -> Set x -> Set x
max :: Set x -> Set x -> Set x
$cmin :: forall x. Ord x => Set x -> Set x -> Set x
min :: Set x -> Set x -> Set x
Ord,Set x -> N
(Set x -> N) -> LengthN (Set x)
forall x. Set x -> N
forall x. (x -> N) -> LengthN x
$clengthN :: forall x. Set x -> N
lengthN :: Set x -> N
LengthN,(forall m. Monoid m => Set m -> m)
-> (forall m a. Monoid m => (a -> m) -> Set a -> m)
-> (forall m a. Monoid m => (a -> m) -> Set a -> m)
-> (forall a b. (a -> b -> b) -> b -> Set a -> b)
-> (forall a b. (a -> b -> b) -> b -> Set a -> b)
-> (forall b a. (b -> a -> b) -> b -> Set a -> b)
-> (forall b a. (b -> a -> b) -> b -> Set a -> b)
-> (forall a. (a -> a -> a) -> Set a -> a)
-> (forall a. (a -> a -> a) -> Set a -> a)
-> (forall a. Set a -> [a])
-> (forall a. Set a -> Bool)
-> (forall a. Set a -> Int)
-> (forall a. Eq a => a -> Set a -> Bool)
-> (forall a. Ord a => Set a -> a)
-> (forall a. Ord a => Set a -> a)
-> (forall a. Num a => Set a -> a)
-> (forall a. Num a => Set a -> a)
-> Foldable Set
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
$cfold :: forall m. Monoid m => Set m -> m
fold :: forall m. Monoid m => Set m -> 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
foldMap' :: forall m a. Monoid m => (a -> m) -> Set a -> m
$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
foldr' :: forall a b. (a -> b -> 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
foldl' :: forall b a. (b -> a -> b) -> b -> Set a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Set a -> a
foldr1 :: forall a. (a -> a -> a) -> Set a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Set a -> a
foldl1 :: forall a. (a -> a -> a) -> Set a -> a
$ctoList :: forall a. Set a -> [a]
toList :: forall a. Set a -> [a]
$cnull :: forall a. Set a -> Bool
null :: forall a. Set a -> Bool
$clength :: forall a. Set a -> Int
length :: forall a. Set a -> Int
$celem :: forall a. Eq a => a -> Set a -> Bool
elem :: forall a. Eq a => a -> Set a -> Bool
$cmaximum :: forall a. Ord a => Set a -> a
maximum :: forall a. Ord a => Set a -> a
$cminimum :: forall a. Ord a => Set a -> a
minimum :: forall a. Ord a => Set a -> a
$csum :: forall a. Num a => Set a -> a
sum :: forall a. Num a => Set a -> a
$cproduct :: forall a. Num a => Set a -> a
product :: forall a. Num a => Set a -> a
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)) = x -> Statement
forall a. Validable a => a -> Statement
valid x
x Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& N -> x -> [x] -> Statement
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 [ t -> Statement
forall a. Validable a => a -> Statement
valid t
y
                       , (t
xt -> t -> Bool
forall a. Ord a => a -> a -> Bool
<t
y) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"i"String -> String -> Parameter
:=t -> String
forall a. Show a => a -> String
show t
i,String
"(x,y)"String -> String -> Parameter
:=(t, t) -> String
forall a. Show a => a -> String
show (t
x,t
y)]
                       , t -> t -> [t] -> Statement
vld (t -> t
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
:<=>: Set x -> 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 = [x] -> Set x
forall x. [x] -> Set x
Set ([x] -> Set x) -> ([x] -> [x]) -> [x] -> Set x
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. ([x] -> x) -> [[x]] -> [x]
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 [x] -> x
forall a. HasCallStack => [a] -> a
head ([[x]] -> [x]) -> ([x] -> [[x]]) -> [x] -> [x]
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. [x] -> [[x]]
forall a. Eq a => [a] -> [[a]]
group ([x] -> [[x]]) -> ([x] -> [x]) -> [x] -> [[x]]
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. [x] -> [x]
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

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

-- setTakeN -


-- | takes the first @n@ elements.

setTakeN :: N -> Set x -> Set x
setTakeN :: forall x. N -> Set x -> Set x
setTakeN N
n (Set [x]
xs) = [x] -> Set x
forall x. [x] -> Set x
Set ([x] -> Set x) -> [x] -> Set x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ N -> [x] -> [x]
forall a. N -> [a] -> [a]
takeN N
n [x]
xs

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

-- setSpan -


-- | the span of a set.

setSpan :: Set x -> Span x
setSpan :: forall x. Set x -> Span x
setSpan (Set [])     = (Closure x
forall x. Closure x
PosInf,Closure x
forall x. Closure x
NegInf)
setSpan (Set (x
x:[x]
xs)) = (x -> Closure x
forall x. x -> Closure x
It x
x,x -> [x] -> Closure x
forall {t}. t -> [t] -> Closure t
last x
x [x]
xs) where
  last :: t -> [t] -> Closure t
last t
x []     = t -> Closure t
forall x. x -> Closure x
It t
x
  last t
_ (t
x:[t]
xs) = t -> [t] -> Closure 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) = [y] -> Set y
forall x. [x] -> Set x
Set ([y] -> Set y) -> [y] -> Set y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [y] -> [y]
forall a. Ord a => [a] -> [a]
sort ([y] -> [y]) -> [y] -> [y]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (x -> y) -> [x] -> [y]
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)
  = [x] -> Set x
forall x. [x] -> Set x
Set
  ([x] -> Set x) -> [x] -> Set x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [x] -> [x]
forall a. Ord a => [a] -> [a]
sort
  ([x] -> [x]) -> [x] -> [x]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (Maybe x -> x) -> [Maybe x] -> [x]
forall a b. (a -> b) -> [a] -> [b]
map Maybe x -> x
forall a. HasCallStack => Maybe a -> a
fromJust
  ([Maybe x] -> [x]) -> [Maybe x] -> [x]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (Maybe x -> Bool) -> [Maybe x] -> [Maybe x]
forall x. (x -> Bool) -> [x] -> [x]
forall (s :: * -> *) x. Filterable s => (x -> Bool) -> s x -> s x
filter Maybe x -> Bool
forall a. Maybe a -> Bool
isJust
  ([Maybe x] -> [Maybe x]) -> [Maybe x] -> [Maybe x]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (i -> Maybe x) -> [i] -> [Maybe x]
forall a b. (a -> b) -> [a] -> [b]
map i -> Maybe x
mx [i]
is

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

-- setFilter -


-- | filtering a set according to a given predicate.

setFilter :: (x -> Bool) -> Set x -> Set x
setFilter :: forall x. (x -> Bool) -> Set x -> Set x
setFilter x -> Bool
p (Set [x]
xs) = [x] -> Set x
forall x. [x] -> Set x
Set ([x] -> Set x) -> [x] -> Set x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (x -> Bool) -> [x] -> [x]
forall x. (x -> Bool) -> [x] -> [x]
forall (s :: * -> *) x. Filterable s => (x -> Bool) -> s x -> s x
filter x -> Bool
p [x]
xs

instance Filterable Set where
  filter :: forall x. (x -> Bool) -> Set x -> Set x
filter = (x -> Bool) -> Set x -> Set x
forall x. (x -> Bool) -> Set x -> Set x
setFilter

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

-- setIsEmpty -


-- | checking for the empty set.

setIsEmpty :: Set x -> Bool
setIsEmpty :: forall a. Set a -> Bool
setIsEmpty (Set [x]
xs) = case [x]
xs of
  [] -> Bool
True
  [x]
_  -> Bool
False
  
--------------------------------------------------------------------------------

-- setEmpty -


-- | the empty set.

setEmpty :: Set x
setEmpty :: forall x. Set x
setEmpty = [x] -> Set x
forall x. [x] -> Set x
Set []

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

-- setPower -


-- | the power set of a given set, grouped by there length.

setPower :: Set x -> Set (N,Set (Set x))
setPower :: forall x. Set x -> Set (N, Set (Set x))
setPower = [(N, Set (Set x))] -> Set (N, Set (Set x))
forall x. [x] -> Set x
Set ([(N, Set (Set x))] -> Set (N, Set (Set x)))
-> (Set x -> [(N, Set (Set x))]) -> Set x -> Set (N, Set (Set x))
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. Set x -> [(N, Set (Set x))]
forall {x}. Set x -> [(N, Set (Set x))]
spwr where
  spwr :: Set x -> [(N, Set (Set x))]
spwr (Set [])     = [(N
0,[Set x] -> Set (Set x)
forall x. [x] -> Set x
Set [[x] -> Set x
forall x. [x] -> Set x
Set []])]
  spwr (Set (x
x:[x]
xs)) = (N
0,[Set x] -> Set (Set x)
forall x. [x] -> Set x
Set [[x] -> Set x
forall x. [x] -> Set x
Set []]) (N, Set (Set x)) -> [(N, Set (Set x))] -> [(N, Set (Set x))]
forall a. a -> [a] -> [a]
: (x
x x -> [(N, Set (Set x))] -> [(N, Set (Set x))]
forall x. x -> [(N, Set (Set x))] -> [(N, Set (Set x))]
<<: Set x -> [(N, Set (Set x))]
spwr ([x] -> Set x
forall x. [x] -> Set x
Set [x]
xs))
  
  (<<:) :: x -> [(N,Set (Set x))] -> [(N,Set (Set x))]
  x
x <<: :: forall x. x -> [(N, Set (Set x))] -> [(N, Set (Set x))]
<<: ((N
_,Set [Set x]
ss):(N
n,Set [Set x]
ss'):[(N, Set (Set x))]
nss) = (N
n,[Set x] -> Set (Set x)
forall x. [x] -> Set x
Set ((Set x -> Set x) -> [Set x] -> [Set x]
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (x
xx -> Set x -> Set x
forall {x}. x -> Set x -> Set x
<:) [Set x]
ss [Set x] -> [Set x] -> [Set x]
forall a. [a] -> [a] -> [a]
++ [Set x]
ss')) (N, Set (Set x)) -> [(N, Set (Set x))] -> [(N, Set (Set x))]
forall a. a -> [a] -> [a]
: (x
x x -> [(N, Set (Set x))] -> [(N, Set (Set x))]
forall x. x -> [(N, Set (Set x))] -> [(N, Set (Set x))]
<<: ((N
n,[Set x] -> Set (Set x)
forall x. [x] -> Set x
Set [Set x]
ss')(N, Set (Set x)) -> [(N, Set (Set x))] -> [(N, Set (Set x))]
forall a. a -> [a] -> [a]
:[(N, Set (Set x))]
nss))
  x
x <<: [(N
n,Set [Set x]
ss)]                 = [(N -> N
forall a. Enum a => a -> a
succ N
n,[Set x] -> Set (Set x)
forall x. [x] -> Set x
Set ([Set x] -> Set (Set x)) -> [Set x] -> Set (Set x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (Set x -> Set x) -> [Set x] -> [Set x]
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (x
xx -> Set x -> Set x
forall {x}. x -> Set x -> Set x
<:) [Set x]
ss)]
  x
_ <<: []                           = AlgebraicException -> [(N, Set (Set x))]
forall a e. Exception e => e -> a
throw (AlgebraicException -> [(N, Set (Set x))])
-> AlgebraicException -> [(N, Set (Set x))]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ String -> AlgebraicException
ImplementationError String
"spwr"

  x
x <: :: x -> Set x -> Set x
<: Set [x]
xs = [x] -> Set x
forall x. [x] -> Set x
Set (x
xx -> [x] -> [x]
forall a. a -> [a] -> [a]
:[x]
xs)

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

-- 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) = [x] -> Set x
forall x. [x] -> Set x
Set ([x] -> Set x) -> [x] -> Set x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [x] -> [x] -> [x]
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 a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` a
y of
    Ordering
LT -> a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a] -> [a] -> [a]
un [a]
xs' [a]
ys
    Ordering
EQ -> a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a] -> [a] -> [a]
un [a]
xs' [a]
ys'
    Ordering
GT -> a
ya -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a] -> [a] -> [a]
un [a]
xs  [a]
ys'

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

-- setDifference -


-- | difference of two sets.

setDifference :: Ord x => Set x -> Set x -> Set x
setDifference :: forall x. Ord x => Set x -> Set x -> Set x
setDifference (Set [x]
xs) (Set [x]
ys) = [x] -> Set x
forall x. [x] -> Set x
Set ([x] -> Set x) -> [x] -> Set x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [x] -> [x] -> [x]
forall {a}. Ord a => [a] -> [a] -> [a]
diff [x]
xs [x]
ys where
  diff :: [a] -> [a] -> [a]
diff [] [a]
_          = []
  diff [a]
xs []         = [a]
xs
  diff (a
x:[a]
xs) (a
y:[a]
ys) = case a
x a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` a
y of
    Ordering
LT -> a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a] -> [a] -> [a]
diff [a]
xs (a
ya -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
ys)
    Ordering
EQ -> [a] -> [a] -> [a]
diff [a]
xs [a]
ys
    Ordering
GT -> [a] -> [a] -> [a]
diff (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
xs) [a]
ys

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

-- setIntersection -


-- | intersection of two sets.

setIntersection :: Ord x => Set x -> Set x -> Set x
setIntersection :: forall x. Ord x => Set x -> Set x -> Set x
setIntersection (Set [x]
xs) (Set [x]
ys) = [x] -> Set x
forall x. [x] -> Set x
Set ([x] -> Set x) -> [x] -> Set x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [x] -> [x] -> [x]
forall {a}. Ord a => [a] -> [a] -> [a]
intr [x]
xs [x]
ys where
  intr :: [a] -> [a] -> [a]
intr (a
x:[a]
xs) (a
y:[a]
ys) = case a
x a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` a
y of
    Ordering
LT -> [a] -> [a] -> [a]
intr [a]
xs (a
ya -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
ys)
    Ordering
EQ -> a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a] -> [a] -> [a]
intr [a]
xs [a]
ys
    Ordering
GT -> [a] -> [a] -> [a]
intr (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
xs) [a]
ys
  intr [a]
_ [a]
_ = []

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

-- 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) = [x] -> [x] -> Bool
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 a -> a -> Ordering
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'

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

-- Set - ErasableLattice -


instance Ord x => PartiallyOrdered (Set x) where <<= :: Set x -> Set x -> Bool
(<<=) = Set x -> Set x -> Bool
forall x. Ord x => Set x -> Set x -> Bool
isSubSet
instance Ord x => Empty (Set x) where
  empty :: Set x
empty = Set x
forall x. Set x
setEmpty
  isEmpty :: Set x -> Bool
isEmpty (Set []) = Bool
True
  isEmpty (Set [x]
_)  = Bool
False

instance Ord x => Logical (Set x) where
  || :: Set x -> Set x -> Set x
(||) = Set x -> Set x -> Set x
forall x. Ord x => Set x -> Set x -> Set x
setUnion
  && :: Set x -> Set x -> Set x
(&&) = Set x -> Set x -> Set x
forall x. Ord x => Set x -> Set x -> Set x
setIntersection

instance Ord x => Lattice (Set x)

instance Ord x => Erasable (Set x) where // :: Set x -> Set x -> Set x
(//) = Set x -> Set x -> Set x
forall x. Ord x => Set x -> Set x -> Set x
setDifference

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

-- 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 []) = Maybe N -> x -> Maybe N
forall b a. b -> a -> b
const Maybe N
forall a. Maybe a
Nothing
-- setIndex (Set xs) = \x -> let (x',i) = trLookup xs' x in if x' == x then Just i else Nothing

setIndex (Set [x]
xs) = Tree x (x, N) -> x -> Maybe N
forall x y. Ord x => Tree x (x, y) -> x -> Maybe y
lp ([(x, N)] -> Tree x (x, N)
forall x. Ord x => [(x, N)] -> Tree x (x, N)
lt ([x]
xs [x] -> [N] -> [(x, N)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [N
0..]))
  where
    -- xs' = lt (xs `zip` [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] = (x, N) -> Tree x (x, N)
forall i x. x -> Tree i x
Leaf (x, N)
xi
    lt [(x, N)]
xis  = x -> Tree x (x, N) -> Tree x (x, N) -> Tree x (x, N)
forall i x. i -> Tree i x -> Tree i x -> Tree i x
Node ((x, N) -> x
forall a b. (a, b) -> a
fst ((x, N) -> x) -> (x, N) -> x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(x, N)] -> (x, N)
forall a. HasCallStack => [a] -> a
head [(x, N)]
xisR) ([(x, N)] -> Tree x (x, N)
forall x. Ord x => [(x, N)] -> Tree x (x, N)
lt [(x, N)]
xisL) ([(x, N)] -> Tree x (x, N)
forall x. Ord x => [(x, N)] -> Tree x (x, N)
lt [(x, N)]
xisR) where
      ([(x, N)]
xisL,[(x, N)]
xisR) = N -> [(x, N)] -> ([(x, N)], [(x, N)])
forall x. N -> [x] -> ([x], [x])
splitAtN ([(x, N)] -> N
forall x. LengthN x => x -> N
lengthN [(x, N)]
xis N -> N -> N
forall a. Integral a => a -> a -> a
`div` N
2) [(x, N)]
xis

lp :: Ord x => Tree x (x,y) -> x -> Maybe y
lp :: forall x y. Ord x => Tree x (x, y) -> x -> Maybe y
lp Tree x (x, y)
t x
x = let (x
x',y
y) = Tree x (x, y) -> x -> (x, y)
forall i x. Ord i => Tree i x -> i -> x
trLookup Tree x (x, y)
t x
x in if x
x' x -> x -> Bool
forall a. Eq a => a -> a -> Bool
== x
x then y -> Maybe y
forall a. a -> Maybe a
Just y
y else Maybe y
forall a. Maybe a
Nothing

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

-- Map -


instance ApplicativeG Set (Map Ord') (->) where
  amapG :: forall x y. Map Ord' x y -> Set x -> Set y
amapG (Map x -> y
f) (Set [x]
xs) = [y] -> Set y
forall x. Ord x => [x] -> Set x
set ([y] -> Set y) -> [y] -> Set y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (x -> y) -> [x] -> [y]
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 x -> y
f [x]
xs

instance FunctorialG Set (Map Ord') (->)

instance ApplicativeG Set (Map EntOrd) (->) where
  amapG :: forall x y. Map EntOrd x y -> Set x -> Set y
amapG Map EntOrd x y
f = Map Ord' x y -> Set x -> Set y
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (Map EntOrd x y -> Map Ord' x y
forall x y. Map EntOrd x y -> Map Ord' x y
ordMap Map EntOrd x y
f) where
    ordMap :: Map EntOrd x y -> Map Ord' x y
    ordMap :: forall x y. Map EntOrd x y -> Map Ord' x y
ordMap (Map x -> y
f) = (x -> y) -> Map Ord' x y
forall s x y.
(Structure s x, Structure s y) =>
(x -> y) -> Map s x y
Map x -> y
f

instance FunctorialG Set (Map EntOrd) (->)

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

-- xSet -


-- | random variable of sets with a maximal length of 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 <- N -> X x -> X [x]
forall x. N -> X x -> X [x]
xTakeN N
n X x
xx
  Set x -> X (Set x)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set x -> X (Set x)) -> Set x -> X (Set x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [x] -> Set x
forall x. [x] -> Set x
Set ([x] -> Set x) -> [x] -> Set x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ([x] -> x) -> [[x]] -> [x]
forall a b. (a -> b) -> [a] -> [b]
map [x] -> x
forall a. HasCallStack => [a] -> a
head ([[x]] -> [x]) -> [[x]] -> [x]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [x] -> [[x]]
forall a. Eq a => [a] -> [[a]]
group ([x] -> [[x]]) -> [x] -> [[x]]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [x] -> [x]
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
:<=>:
  X (Set x, Set x) -> ((Set x, Set x) -> 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 Set x -> Set x -> Set 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 Set x -> Set x -> Bool
forall x. Ord x => Set x -> Set x -> Bool
`isSubSet` Set x
xy) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"x"String -> String -> Parameter
:=Set x -> String
forall a. Show a => a -> String
show Set x
x, String
"xy"String -> String -> Parameter
:=Set x -> String
forall a. Show a => a -> String
show Set x
xy]
                      , String -> Label
Label String
"y"
                        Label -> Statement -> Statement
:<=>: (Set x
y Set x -> Set x -> Bool
forall x. Ord x => Set x -> Set x -> Bool
`isSubSet` Set x
xy) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"y"String -> String -> Parameter
:=Set x -> String
forall a. Show a => a -> String
show Set x
y, String
"xy"String -> String -> Parameter
:=Set x -> String
forall a. Show a => a -> String
show Set x
xy]
                      ]
            ) 
  where xy :: X (Set x, Set x)
xy = X (Set x) -> X (Set x) -> X (Set x, Set x)
forall a b. X a -> X b -> X (a, b)
xTupple2 X (Set x)
x X (Set x)
x