module Data.Interval.Borel (
Borel,
borel,
intervalSet,
Data.Interval.Borel.empty,
singleton,
Data.Interval.Borel.null,
insert,
whole,
remove,
(\-),
truncate,
(\=),
member,
notMember,
union,
unions,
difference,
symmetricDifference,
complement,
intersection,
intersections,
hull,
isSubsetOf,
) where
import Algebra.Heyting (Heyting ((==>)))
import Algebra.Lattice
import Control.Arrow ((>>>))
import Data.Data
import Data.Foldable (fold)
import Data.Functor ((<&>))
import Data.Interval (Interval)
import Data.Interval qualified as I
import Data.List.NonEmpty (NonEmpty ((:|)))
import Data.OneOrTwo (OneOrTwo (..))
import Data.Semiring (Ring, Semiring)
import Data.Semiring qualified as Semiring
import Data.Set (Set)
import Data.Set qualified as Set
import GHC.Generics (Generic)
import Prelude hiding (null, truncate)
newtype Borel x = Borel (Set (Interval x))
deriving (Borel x -> Borel x -> Bool
forall x. Ord x => Borel x -> Borel x -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Borel x -> Borel x -> Bool
$c/= :: forall x. Ord x => Borel x -> Borel x -> Bool
== :: Borel x -> Borel x -> Bool
$c== :: forall x. Ord x => Borel x -> Borel x -> Bool
Eq, Borel x -> Borel x -> Bool
Borel x -> Borel x -> Ordering
Borel x -> Borel x -> Borel 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 (Borel x)
forall x. Ord x => Borel x -> Borel x -> Bool
forall x. Ord x => Borel x -> Borel x -> Ordering
forall x. Ord x => Borel x -> Borel x -> Borel x
min :: Borel x -> Borel x -> Borel x
$cmin :: forall x. Ord x => Borel x -> Borel x -> Borel x
max :: Borel x -> Borel x -> Borel x
$cmax :: forall x. Ord x => Borel x -> Borel x -> Borel x
>= :: Borel x -> Borel x -> Bool
$c>= :: forall x. Ord x => Borel x -> Borel x -> Bool
> :: Borel x -> Borel x -> Bool
$c> :: forall x. Ord x => Borel x -> Borel x -> Bool
<= :: Borel x -> Borel x -> Bool
$c<= :: forall x. Ord x => Borel x -> Borel x -> Bool
< :: Borel x -> Borel x -> Bool
$c< :: forall x. Ord x => Borel x -> Borel x -> Bool
compare :: Borel x -> Borel x -> Ordering
$ccompare :: forall x. Ord x => Borel x -> Borel x -> Ordering
Ord, Int -> Borel x -> ShowS
forall x. (Ord x, Show x) => Int -> Borel x -> ShowS
forall x. (Ord x, Show x) => [Borel x] -> ShowS
forall x. (Ord x, Show x) => Borel x -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Borel x] -> ShowS
$cshowList :: forall x. (Ord x, Show x) => [Borel x] -> ShowS
show :: Borel x -> String
$cshow :: forall x. (Ord x, Show x) => Borel x -> String
showsPrec :: Int -> Borel x -> ShowS
$cshowsPrec :: forall x. (Ord x, Show x) => Int -> Borel x -> ShowS
Show, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall x x. Rep (Borel x) x -> Borel x
forall x x. Borel x -> Rep (Borel x) x
$cto :: forall x x. Rep (Borel x) x -> Borel x
$cfrom :: forall x x. Borel x -> Rep (Borel x) x
Generic, Typeable, Borel x -> DataType
Borel x -> Constr
forall {x}. (Data x, Ord x) => Typeable (Borel x)
forall x. (Data x, Ord x) => Borel x -> DataType
forall x. (Data x, Ord x) => Borel x -> Constr
forall x.
(Data x, Ord x) =>
(forall b. Data b => b -> b) -> Borel x -> Borel x
forall x u.
(Data x, Ord x) =>
Int -> (forall d. Data d => d -> u) -> Borel x -> u
forall x u.
(Data x, Ord x) =>
(forall d. Data d => d -> u) -> Borel x -> [u]
forall x r r'.
(Data x, Ord x) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Borel x -> r
forall x r r'.
(Data x, Ord x) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Borel x -> r
forall x (m :: * -> *).
(Data x, Ord x, Monad m) =>
(forall d. Data d => d -> m d) -> Borel x -> m (Borel x)
forall x (m :: * -> *).
(Data x, Ord x, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Borel x -> m (Borel x)
forall x (c :: * -> *).
(Data x, Ord x) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Borel x)
forall x (c :: * -> *).
(Data x, Ord x) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Borel x -> c (Borel x)
forall x (t :: * -> *) (c :: * -> *).
(Data x, Ord x, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Borel x))
forall x (t :: * -> * -> *) (c :: * -> *).
(Data x, Ord x, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Borel x))
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Borel x)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Borel x -> c (Borel x)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Borel x))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Borel x -> m (Borel x)
$cgmapMo :: forall x (m :: * -> *).
(Data x, Ord x, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Borel x -> m (Borel x)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Borel x -> m (Borel x)
$cgmapMp :: forall x (m :: * -> *).
(Data x, Ord x, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Borel x -> m (Borel x)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Borel x -> m (Borel x)
$cgmapM :: forall x (m :: * -> *).
(Data x, Ord x, Monad m) =>
(forall d. Data d => d -> m d) -> Borel x -> m (Borel x)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Borel x -> u
$cgmapQi :: forall x u.
(Data x, Ord x) =>
Int -> (forall d. Data d => d -> u) -> Borel x -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Borel x -> [u]
$cgmapQ :: forall x u.
(Data x, Ord x) =>
(forall d. Data d => d -> u) -> Borel x -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Borel x -> r
$cgmapQr :: forall x r r'.
(Data x, Ord x) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Borel x -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Borel x -> r
$cgmapQl :: forall x r r'.
(Data x, Ord x) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Borel x -> r
gmapT :: (forall b. Data b => b -> b) -> Borel x -> Borel x
$cgmapT :: forall x.
(Data x, Ord x) =>
(forall b. Data b => b -> b) -> Borel x -> Borel x
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Borel x))
$cdataCast2 :: forall x (t :: * -> * -> *) (c :: * -> *).
(Data x, Ord x, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Borel x))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Borel x))
$cdataCast1 :: forall x (t :: * -> *) (c :: * -> *).
(Data x, Ord x, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Borel x))
dataTypeOf :: Borel x -> DataType
$cdataTypeOf :: forall x. (Data x, Ord x) => Borel x -> DataType
toConstr :: Borel x -> Constr
$ctoConstr :: forall x. (Data x, Ord x) => Borel x -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Borel x)
$cgunfold :: forall x (c :: * -> *).
(Data x, Ord x) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Borel x)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Borel x -> c (Borel x)
$cgfoldl :: forall x (c :: * -> *).
(Data x, Ord x) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Borel x -> c (Borel x)
Data)
instance (Ord x) => Semigroup (Borel x) where
Borel Set (Interval x)
is <> :: Borel x -> Borel x -> Borel x
<> Borel Set (Interval x)
js = forall x. Set (Interval x) -> Borel x
Borel (forall x. Ord x => Set (Interval x) -> Set (Interval x)
unionsSet (Set (Interval x)
is forall a. Semigroup a => a -> a -> a
<> Set (Interval x)
js))
instance (Ord x) => Monoid (Borel x) where
mempty :: Borel x
mempty = forall x. Set (Interval x) -> Borel x
Borel forall a. Monoid a => a
mempty
instance (Ord x, Lattice x) => Lattice (Borel x) where
\/ :: Borel x -> Borel x -> Borel x
(\/) = forall x. Ord x => Borel x -> Borel x -> Borel x
union
/\ :: Borel x -> Borel x -> Borel x
(/\) = forall x. Ord x => Borel x -> Borel x -> Borel x
intersection
instance (Ord x, Lattice x) => BoundedMeetSemiLattice (Borel x) where
top :: Borel x
top = forall x. Ord x => Borel x
whole
instance (Ord x, Lattice x) => BoundedJoinSemiLattice (Borel x) where
bottom :: Borel x
bottom = forall a. Monoid a => a
mempty
instance (Ord x, Lattice x) => Heyting (Borel x) where
Borel x
x ==> :: Borel x -> Borel x -> Borel x
==> Borel x
y = forall x. Ord x => Borel x -> Borel x
complement Borel x
x forall a. Lattice a => a -> a -> a
\/ Borel x
y
instance (Ord x, Lattice x) => Semiring (Borel x) where
plus :: Borel x -> Borel x -> Borel x
plus = forall x. Ord x => Borel x -> Borel x -> Borel x
symmetricDifference
times :: Borel x -> Borel x -> Borel x
times = forall x. Ord x => Borel x -> Borel x -> Borel x
intersection
zero :: Borel x
zero = forall a. Monoid a => a
mempty
one :: Borel x
one = forall x. Ord x => Borel x
whole
instance (Ord x, Lattice x) => Ring (Borel x) where
negate :: Borel x -> Borel x
negate = forall x. Ord x => Borel x -> Borel x
complement
borel :: (Ord x) => [Interval x] -> Borel x
borel :: forall x. Ord x => [Interval x] -> Borel x
borel = forall x. Set (Interval x) -> Borel x
Borel forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> Set a
Set.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x. Ord x => [Interval x] -> [Interval x]
I.unions
intervalSet :: (Ord x) => Borel x -> Set (Interval x)
intervalSet :: forall x. Ord x => Borel x -> Set (Interval x)
intervalSet (Borel Set (Interval x)
is) = forall x. Ord x => Set (Interval x) -> Set (Interval x)
unionsSet Set (Interval x)
is
unionsSet :: (Ord x) => Set (Interval x) -> Set (Interval x)
unionsSet :: forall x. Ord x => Set (Interval x) -> Set (Interval x)
unionsSet = forall a. Eq a => [a] -> Set a
Set.fromAscList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x. Ord x => [Interval x] -> [Interval x]
I.unionsAsc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
Set.toAscList
empty :: (Ord x) => Borel x
empty :: forall x. Ord x => Borel x
empty = forall x. Set (Interval x) -> Borel x
Borel forall a. Set a
Set.empty
singleton :: (Ord x) => Interval x -> Borel x
singleton :: forall x. Ord x => Interval x -> Borel x
singleton Interval x
x = forall x. Set (Interval x) -> Borel x
Borel (forall a. a -> Set a
Set.singleton Interval x
x)
null :: Borel x -> Bool
null :: forall x. Borel x -> Bool
null (Borel Set (Interval x)
is) = forall a. Set a -> Bool
Set.null Set (Interval x)
is
insert :: (Ord x) => Interval x -> Borel x -> Borel x
insert :: forall x. Ord x => Interval x -> Borel x -> Borel x
insert Interval x
i (Borel Set (Interval x)
is) = forall x. Set (Interval x) -> Borel x
Borel (forall x. Ord x => Set (Interval x) -> Set (Interval x)
unionsSet (forall a. Ord a => a -> Set a -> Set a
Set.insert Interval x
i Set (Interval x)
is))
whole :: (Ord x) => Borel x
whole :: forall x. Ord x => Borel x
whole = forall x. Ord x => Interval x -> Borel x
singleton forall x. Ord x => Interval x
I.Whole
remove :: (Ord x) => Interval x -> Borel x -> Borel x
remove :: forall x. Ord x => Interval x -> Borel x -> Borel x
remove Interval x
i (Borel Set (Interval x)
is) =
forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Set (Interval x)
is forall a b. (a -> b) -> a -> b
$
(forall x.
Ord x =>
Interval x -> Interval x -> Maybe (OneOrTwo (Interval x))
I.\\ Interval x
i) forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> \case
Maybe (OneOrTwo (Interval x))
Nothing -> forall a. Monoid a => a
mempty
Just (One Interval x
j) -> forall x. Ord x => [Interval x] -> Borel x
borel [Interval x
j]
Just (Two Interval x
j Interval x
k) -> forall x. Ord x => [Interval x] -> Borel x
borel [Interval x
j, Interval x
k]
(\-) :: (Ord x) => Borel x -> Interval x -> Borel x
\- :: forall x. Ord x => Borel x -> Interval x -> Borel x
(\-) = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall x. Ord x => Interval x -> Borel x -> Borel x
remove
member :: (Ord x) => x -> Borel x -> Bool
member :: forall x. Ord x => x -> Borel x -> Bool
member x
x (Borel Set (Interval x)
is) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall x. Ord x => x -> Interval x -> Bool
I.within x
x) Set (Interval x)
is
notMember :: (Ord x) => x -> Borel x -> Bool
notMember :: forall x. Ord x => x -> Borel x -> Bool
notMember x
x = Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x. Ord x => x -> Borel x -> Bool
member x
x
union :: (Ord x) => Borel x -> Borel x -> Borel x
union :: forall x. Ord x => Borel x -> Borel x -> Borel x
union = forall a. Semigroup a => a -> a -> a
(<>)
unions :: (Ord x) => [Borel x] -> Borel x
unions :: forall x. Ord x => [Borel x] -> Borel x
unions = forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold
difference :: (Ord x) => Borel x -> Borel x -> Borel x
difference :: forall x. Ord x => Borel x -> Borel x -> Borel x
difference Borel x
is (Borel Set (Interval x)
js) = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall x. Ord x => Interval x -> Borel x -> Borel x
remove Borel x
is Set (Interval x)
js
symmetricDifference :: (Ord x) => Borel x -> Borel x -> Borel x
symmetricDifference :: forall x. Ord x => Borel x -> Borel x -> Borel x
symmetricDifference Borel x
is Borel x
js = forall x. Ord x => Borel x -> Borel x -> Borel x
difference Borel x
is Borel x
js forall a. Semigroup a => a -> a -> a
<> forall x. Ord x => Borel x -> Borel x -> Borel x
difference Borel x
js Borel x
is
complement :: (Ord x) => Borel x -> Borel x
complement :: forall x. Ord x => Borel x -> Borel x
complement = forall x. Ord x => Borel x -> Borel x -> Borel x
difference forall x. Ord x => Borel x
whole
truncate :: (Ord x) => Interval x -> Borel x -> Borel x
truncate :: forall x. Ord x => Interval x -> Borel x -> Borel x
truncate Interval x
i (Borel Set (Interval x)
js) =
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall a. Semigroup a => a -> a -> a
(<>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Monoid a => a
mempty forall x. Ord x => Interval x -> Borel x
singleton forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x. Ord x => Interval x -> Interval x -> Maybe (Interval x)
I.intersect Interval x
i) forall a. Monoid a => a
mempty Set (Interval x)
js
(\=) :: (Ord x) => Borel x -> Interval x -> Borel x
\= :: forall x. Ord x => Borel x -> Interval x -> Borel x
(\=) = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall x. Ord x => Interval x -> Borel x -> Borel x
truncate
intersection :: (Ord x) => Borel x -> Borel x -> Borel x
intersection :: forall x. Ord x => Borel x -> Borel x -> Borel x
intersection Borel x
is (Borel Set (Interval x)
js) = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall x. Ord x => Interval x -> Borel x -> Borel x
`truncate` Borel x
is) Set (Interval x)
js
intersections :: (Ord x) => [Borel x] -> Borel x
intersections :: forall x. Ord x => [Borel x] -> Borel x
intersections [] = forall a. Monoid a => a
mempty
intersections [Borel x
i] = Borel x
i
intersections (Borel x
i : Borel x
j : [Borel x]
js) = forall x. Ord x => Borel x -> Borel x -> Borel x
intersection (forall x. Ord x => Borel x -> Borel x -> Borel x
intersection Borel x
i Borel x
j) (forall x. Ord x => [Borel x] -> Borel x
intersections [Borel x]
js)
hull :: (Ord x) => Borel x -> Maybe (Interval x)
hull :: forall x. Ord x => Borel x -> Maybe (Interval x)
hull (Borel Set (Interval x)
js) = forall a. Set a -> Maybe (a, Set a)
Set.minView Set (Interval x)
js forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \(Interval x
i, Set (Interval x)
is) -> forall x. Ord x => NonEmpty (Interval x) -> Interval x
I.hulls (Interval x
i forall a. a -> [a] -> NonEmpty a
:| forall a. Set a -> [a]
Set.toAscList Set (Interval x)
is)
isSubsetOf :: (Ord x) => Borel x -> Borel x -> Bool
isSubsetOf :: forall x. Ord x => Borel x -> Borel x -> Bool
isSubsetOf Borel x
is Borel x
js = forall x. Borel x -> Bool
null forall a b. (a -> b) -> a -> b
$ forall x. Ord x => Borel x -> Borel x -> Borel x
difference Borel x
is Borel x
js