module UVMHS.Core.Pointed where

import UVMHS.Core.Init
import UVMHS.Core.Classes
import UVMHS.Core.Data

-- ======= --
-- AddNull --
-- ======= --

data AddNull a = Null | AddNull a
  deriving (AddNull a -> AddNull a -> Bool
(AddNull a -> AddNull a -> Bool)
-> (AddNull a -> AddNull a -> Bool) -> Eq (AddNull a)
forall a. Eq a => AddNull a -> AddNull a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => AddNull a -> AddNull a -> Bool
== :: AddNull a -> AddNull a -> Bool
$c/= :: forall a. Eq a => AddNull a -> AddNull a -> Bool
/= :: AddNull a -> AddNull a -> Bool
Eq,Eq (AddNull a)
Eq (AddNull a) =>
(AddNull a -> AddNull a -> Ordering)
-> (AddNull a -> AddNull a -> Bool)
-> (AddNull a -> AddNull a -> Bool)
-> (AddNull a -> AddNull a -> Bool)
-> (AddNull a -> AddNull a -> Bool)
-> (AddNull a -> AddNull a -> AddNull a)
-> (AddNull a -> AddNull a -> AddNull a)
-> Ord (AddNull a)
AddNull a -> AddNull a -> Bool
AddNull a -> AddNull a -> Ordering
AddNull a -> AddNull a -> AddNull a
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 a. Ord a => Eq (AddNull a)
forall a. Ord a => AddNull a -> AddNull a -> Bool
forall a. Ord a => AddNull a -> AddNull a -> Ordering
forall a. Ord a => AddNull a -> AddNull a -> AddNull a
$ccompare :: forall a. Ord a => AddNull a -> AddNull a -> Ordering
compare :: AddNull a -> AddNull a -> Ordering
$c< :: forall a. Ord a => AddNull a -> AddNull a -> Bool
< :: AddNull a -> AddNull a -> Bool
$c<= :: forall a. Ord a => AddNull a -> AddNull a -> Bool
<= :: AddNull a -> AddNull a -> Bool
$c> :: forall a. Ord a => AddNull a -> AddNull a -> Bool
> :: AddNull a -> AddNull a -> Bool
$c>= :: forall a. Ord a => AddNull a -> AddNull a -> Bool
>= :: AddNull a -> AddNull a -> Bool
$cmax :: forall a. Ord a => AddNull a -> AddNull a -> AddNull a
max :: AddNull a -> AddNull a -> AddNull a
$cmin :: forall a. Ord a => AddNull a -> AddNull a -> AddNull a
min :: AddNull a -> AddNull a -> AddNull a
Ord,Int -> AddNull a -> ShowS
[AddNull a] -> ShowS
AddNull a -> String
(Int -> AddNull a -> ShowS)
-> (AddNull a -> String)
-> ([AddNull a] -> ShowS)
-> Show (AddNull a)
forall a. Show a => Int -> AddNull a -> ShowS
forall a. Show a => [AddNull a] -> ShowS
forall a. Show a => AddNull a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> AddNull a -> ShowS
showsPrec :: Int -> AddNull a -> ShowS
$cshow :: forall a. Show a => AddNull a -> String
show :: AddNull a -> String
$cshowList :: forall a. Show a => [AddNull a] -> ShowS
showList :: [AddNull a] -> ShowS
Show)

elimAddNull ∷ b → (a → b) → AddNull a → b
elimAddNull :: forall b a. b -> (a -> b) -> AddNull a -> b
elimAddNull b
i a -> b
f = \case
  AddNull a
Null → b
i
  AddNull a
x → a -> b
f a
x

instance Null (AddNull a) where 
  null :: AddNull a
null = AddNull a
forall a. AddNull a
Null
instance (Append a) ⇒ Append (AddNull a) where
  AddNull a
Null ⧺ :: AddNull a -> AddNull a -> AddNull a
⧺ AddNull a
x = AddNull a
x
  AddNull a
x ⧺ AddNull a
Null = AddNull a
x
  AddNull a
x ⧺ AddNull a
y = a -> AddNull a
forall a. a -> AddNull a
AddNull (a -> AddNull a) -> a -> AddNull a
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Append a => a -> a -> a
⧺ a
y
instance (Append a) ⇒ Monoid (AddNull a)
instance Functor AddNull where 
  map :: forall a b. (a -> b) -> AddNull a -> AddNull b
map = (a -> b) -> AddNull a -> AddNull b
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
mmap
instance Return AddNull where 
  return :: forall a. a -> AddNull a
return = a -> AddNull a
forall a. a -> AddNull a
AddNull
instance Bind AddNull where 
  AddNull a
xM ≫= :: forall a b. AddNull a -> (a -> AddNull b) -> AddNull b
≫= a -> AddNull b
f = case AddNull a
xM of {AddNull a
Null → AddNull b
forall a. AddNull a
Null;AddNull a
x → a -> AddNull b
f a
x}
instance Monad AddNull
instance FunctorM AddNull where 
  mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> AddNull a -> m (AddNull b)
mapM a -> m b
f AddNull a
xM = case AddNull a
xM of {AddNull a
Null → AddNull b -> m (AddNull b)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return AddNull b
forall a. AddNull a
Null;AddNull a
x → (b -> AddNull b) -> m b -> m (AddNull b)
forall a b. (a -> b) -> m a -> m b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map b -> AddNull b
forall a. a -> AddNull a
AddNull (m b -> m (AddNull b)) -> m b -> m (AddNull b)
forall a b. (a -> b) -> a -> b
$ a -> m b
f a
x}

-- === --
-- ZOM --
-- === --

data ZOM a = NullZOM | OneZOM a | MoreZOM
  deriving (ZOM a -> ZOM a -> Bool
(ZOM a -> ZOM a -> Bool) -> (ZOM a -> ZOM a -> Bool) -> Eq (ZOM a)
forall a. Eq a => ZOM a -> ZOM a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => ZOM a -> ZOM a -> Bool
== :: ZOM a -> ZOM a -> Bool
$c/= :: forall a. Eq a => ZOM a -> ZOM a -> Bool
/= :: ZOM a -> ZOM a -> Bool
Eq,Eq (ZOM a)
Eq (ZOM a) =>
(ZOM a -> ZOM a -> Ordering)
-> (ZOM a -> ZOM a -> Bool)
-> (ZOM a -> ZOM a -> Bool)
-> (ZOM a -> ZOM a -> Bool)
-> (ZOM a -> ZOM a -> Bool)
-> (ZOM a -> ZOM a -> ZOM a)
-> (ZOM a -> ZOM a -> ZOM a)
-> Ord (ZOM a)
ZOM a -> ZOM a -> Bool
ZOM a -> ZOM a -> Ordering
ZOM a -> ZOM a -> ZOM a
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 a. Ord a => Eq (ZOM a)
forall a. Ord a => ZOM a -> ZOM a -> Bool
forall a. Ord a => ZOM a -> ZOM a -> Ordering
forall a. Ord a => ZOM a -> ZOM a -> ZOM a
$ccompare :: forall a. Ord a => ZOM a -> ZOM a -> Ordering
compare :: ZOM a -> ZOM a -> Ordering
$c< :: forall a. Ord a => ZOM a -> ZOM a -> Bool
< :: ZOM a -> ZOM a -> Bool
$c<= :: forall a. Ord a => ZOM a -> ZOM a -> Bool
<= :: ZOM a -> ZOM a -> Bool
$c> :: forall a. Ord a => ZOM a -> ZOM a -> Bool
> :: ZOM a -> ZOM a -> Bool
$c>= :: forall a. Ord a => ZOM a -> ZOM a -> Bool
>= :: ZOM a -> ZOM a -> Bool
$cmax :: forall a. Ord a => ZOM a -> ZOM a -> ZOM a
max :: ZOM a -> ZOM a -> ZOM a
$cmin :: forall a. Ord a => ZOM a -> ZOM a -> ZOM a
min :: ZOM a -> ZOM a -> ZOM a
Ord,Int -> ZOM a -> ShowS
[ZOM a] -> ShowS
ZOM a -> String
(Int -> ZOM a -> ShowS)
-> (ZOM a -> String) -> ([ZOM a] -> ShowS) -> Show (ZOM a)
forall a. Show a => Int -> ZOM a -> ShowS
forall a. Show a => [ZOM a] -> ShowS
forall a. Show a => ZOM a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> ZOM a -> ShowS
showsPrec :: Int -> ZOM a -> ShowS
$cshow :: forall a. Show a => ZOM a -> String
show :: ZOM a -> String
$cshowList :: forall a. Show a => [ZOM a] -> ShowS
showList :: [ZOM a] -> ShowS
Show)

elimZOM ∷ b → (a → b) → b → ZOM a → b
elimZOM :: forall b a. b -> (a -> b) -> b -> ZOM a -> b
elimZOM b
i₁ a -> b
f b
i₂= \case
  ZOM a
NullZOM → b
i₁
  OneZOM a
x → a -> b
f a
x
  ZOM a
MoreZOM → b
i₂

instance Null (ZOM a) where 
  null :: ZOM a
null = ZOM a
forall a. ZOM a
NullZOM
instance Append (ZOM a) where
  ZOM a
NullZOM ⧺ :: ZOM a -> ZOM a -> ZOM a
⧺ ZOM a
x = ZOM a
x
  ZOM a
x ⧺ ZOM a
NullZOM = ZOM a
x
  ZOM a
_ ⧺ ZOM a
_ = ZOM a
forall a. ZOM a
MoreZOM
instance Monoid (ZOM a)
instance Functor ZOM where 
  map :: forall a b. (a -> b) -> ZOM a -> ZOM b
map = (a -> b) -> ZOM a -> ZOM b
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
mmap
instance Return ZOM where 
  return :: forall a. a -> ZOM a
return = a -> ZOM a
forall a. a -> ZOM a
OneZOM
instance Bind ZOM where 
  ZOM a
xM ≫= :: forall a b. ZOM a -> (a -> ZOM b) -> ZOM b
≫= a -> ZOM b
f = case ZOM a
xM of {ZOM a
NullZOM → ZOM b
forall a. ZOM a
NullZOM;OneZOM a
x → a -> ZOM b
f a
x;ZOM a
MoreZOM → ZOM b
forall a. ZOM a
MoreZOM}
instance Monad ZOM
instance FunctorM ZOM where 
  mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> ZOM a -> m (ZOM b)
mapM a -> m b
f ZOM a
xM = case ZOM a
xM of {ZOM a
NullZOM → ZOM b -> m (ZOM b)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return ZOM b
forall a. ZOM a
NullZOM;OneZOM a
x → (b -> ZOM b) -> m b -> m (ZOM b)
forall a b. (a -> b) -> m a -> m b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map b -> ZOM b
forall a. a -> ZOM a
OneZOM (m b -> m (ZOM b)) -> m b -> m (ZOM b)
forall a b. (a -> b) -> a -> b
$ a -> m b
f a
x;ZOM a
MoreZOM → ZOM b -> m (ZOM b)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return ZOM b
forall a. ZOM a
MoreZOM}

instance Single a (ZOM a) where single :: a -> ZOM a
single = a -> ZOM a
forall a. a -> ZOM a
OneZOM

-- ====== --
-- AddBot --
-- ====== --

data AddBot a = Bot | AddBot a
  deriving (AddBot a -> AddBot a -> Bool
(AddBot a -> AddBot a -> Bool)
-> (AddBot a -> AddBot a -> Bool) -> Eq (AddBot a)
forall a. Eq a => AddBot a -> AddBot a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => AddBot a -> AddBot a -> Bool
== :: AddBot a -> AddBot a -> Bool
$c/= :: forall a. Eq a => AddBot a -> AddBot a -> Bool
/= :: AddBot a -> AddBot a -> Bool
Eq,Eq (AddBot a)
Eq (AddBot a) =>
(AddBot a -> AddBot a -> Ordering)
-> (AddBot a -> AddBot a -> Bool)
-> (AddBot a -> AddBot a -> Bool)
-> (AddBot a -> AddBot a -> Bool)
-> (AddBot a -> AddBot a -> Bool)
-> (AddBot a -> AddBot a -> AddBot a)
-> (AddBot a -> AddBot a -> AddBot a)
-> Ord (AddBot a)
AddBot a -> AddBot a -> Bool
AddBot a -> AddBot a -> Ordering
AddBot a -> AddBot a -> AddBot a
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 a. Ord a => Eq (AddBot a)
forall a. Ord a => AddBot a -> AddBot a -> Bool
forall a. Ord a => AddBot a -> AddBot a -> Ordering
forall a. Ord a => AddBot a -> AddBot a -> AddBot a
$ccompare :: forall a. Ord a => AddBot a -> AddBot a -> Ordering
compare :: AddBot a -> AddBot a -> Ordering
$c< :: forall a. Ord a => AddBot a -> AddBot a -> Bool
< :: AddBot a -> AddBot a -> Bool
$c<= :: forall a. Ord a => AddBot a -> AddBot a -> Bool
<= :: AddBot a -> AddBot a -> Bool
$c> :: forall a. Ord a => AddBot a -> AddBot a -> Bool
> :: AddBot a -> AddBot a -> Bool
$c>= :: forall a. Ord a => AddBot a -> AddBot a -> Bool
>= :: AddBot a -> AddBot a -> Bool
$cmax :: forall a. Ord a => AddBot a -> AddBot a -> AddBot a
max :: AddBot a -> AddBot a -> AddBot a
$cmin :: forall a. Ord a => AddBot a -> AddBot a -> AddBot a
min :: AddBot a -> AddBot a -> AddBot a
Ord,Int -> AddBot a -> ShowS
[AddBot a] -> ShowS
AddBot a -> String
(Int -> AddBot a -> ShowS)
-> (AddBot a -> String) -> ([AddBot a] -> ShowS) -> Show (AddBot a)
forall a. Show a => Int -> AddBot a -> ShowS
forall a. Show a => [AddBot a] -> ShowS
forall a. Show a => AddBot a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> AddBot a -> ShowS
showsPrec :: Int -> AddBot a -> ShowS
$cshow :: forall a. Show a => AddBot a -> String
show :: AddBot a -> String
$cshowList :: forall a. Show a => [AddBot a] -> ShowS
showList :: [AddBot a] -> ShowS
Show)

elimAddBot ∷ b → (a → b) → AddBot a → b
elimAddBot :: forall b a. b -> (a -> b) -> AddBot a -> b
elimAddBot b
i a -> b
f = \case
  AddBot a
Bot → b
i
  AddBot a
x → a -> b
f a
x

instance (POrd a) ⇒ POrd (AddBot a) where
  AddBot a
xT ⊑ :: AddBot a -> AddBot a -> Bool
⊑ AddBot a
yT = case (AddBot a
xT,AddBot a
yT) of
    (AddBot a
Bot,AddBot a
Bot) → Bool
True
    (AddBot a
Bot,AddBot a
_) → Bool
True
    (AddBot a
_,AddBot a
Bot) → Bool
False
    (AddBot a
x,AddBot a
y) → a
x a -> a -> Bool
forall a. POrd a => a -> a -> Bool
⊑ a
y
instance Bot (AddBot a) where 
  bot :: AddBot a
bot = AddBot a
forall a. AddBot a
Bot
instance (Join a) ⇒ Join (AddBot a) where
  AddBot a
Bot ⊔ :: AddBot a -> AddBot a -> AddBot a
⊔ AddBot a
x = AddBot a
x
  AddBot a
x ⊔ AddBot a
Bot = AddBot a
x
  AddBot a
x ⊔ AddBot a
y = a -> AddBot a
forall a. a -> AddBot a
AddBot (a -> AddBot a) -> a -> AddBot a
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Join a => a -> a -> a
⊔ a
y
instance (Top a) ⇒ Top (AddBot a) where 
  top :: AddBot a
top = a -> AddBot a
forall a. a -> AddBot a
AddBot a
forall a. Top a => a
top
instance (Meet a) ⇒ Meet (AddBot a) where
  AddBot a
Bot ⊓ :: AddBot a -> AddBot a -> AddBot a
⊓ AddBot a
_ = AddBot a
forall a. AddBot a
Bot
  AddBot a
_ ⊓ AddBot a
Bot = AddBot a
forall a. AddBot a
Bot
  AddBot a
x ⊓ AddBot a
y = a -> AddBot a
forall a. a -> AddBot a
AddBot (a -> AddBot a) -> a -> AddBot a
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Meet a => a -> a -> a
⊓ a
y
instance (Join a) ⇒ JoinLattice (AddBot a)
instance (MeetLattice a) ⇒ MeetLattice (AddBot a)
instance (Join a,MeetLattice a) ⇒ Lattice (AddBot a)
instance Functor AddBot where 
  map :: forall a b. (a -> b) -> AddBot a -> AddBot b
map = (a -> b) -> AddBot a -> AddBot b
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
mmap
instance Return AddBot where 
  return :: forall a. a -> AddBot a
return = a -> AddBot a
forall a. a -> AddBot a
AddBot
instance Bind AddBot where 
  AddBot a
xM ≫= :: forall a b. AddBot a -> (a -> AddBot b) -> AddBot b
≫= a -> AddBot b
f = case AddBot a
xM of {AddBot a
Bot → AddBot b
forall a. AddBot a
Bot;AddBot a
x → a -> AddBot b
f a
x}
instance Monad AddBot
instance FunctorM AddBot where 
  mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> AddBot a -> m (AddBot b)
mapM a -> m b
f AddBot a
xM = case AddBot a
xM of {AddBot a
Bot → AddBot b -> m (AddBot b)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return AddBot b
forall a. AddBot a
Bot;AddBot a
x → (b -> AddBot b) -> m b -> m (AddBot b)
forall a b. (a -> b) -> m a -> m b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map b -> AddBot b
forall a. a -> AddBot a
AddBot (m b -> m (AddBot b)) -> m b -> m (AddBot b)
forall a b. (a -> b) -> a -> b
$ a -> m b
f a
x}

-- ====== --
-- AddTop --
-- ====== --

data AddTop a = AddTop a | Top
  deriving (AddTop a -> AddTop a -> Bool
(AddTop a -> AddTop a -> Bool)
-> (AddTop a -> AddTop a -> Bool) -> Eq (AddTop a)
forall a. Eq a => AddTop a -> AddTop a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => AddTop a -> AddTop a -> Bool
== :: AddTop a -> AddTop a -> Bool
$c/= :: forall a. Eq a => AddTop a -> AddTop a -> Bool
/= :: AddTop a -> AddTop a -> Bool
Eq,Eq (AddTop a)
Eq (AddTop a) =>
(AddTop a -> AddTop a -> Ordering)
-> (AddTop a -> AddTop a -> Bool)
-> (AddTop a -> AddTop a -> Bool)
-> (AddTop a -> AddTop a -> Bool)
-> (AddTop a -> AddTop a -> Bool)
-> (AddTop a -> AddTop a -> AddTop a)
-> (AddTop a -> AddTop a -> AddTop a)
-> Ord (AddTop a)
AddTop a -> AddTop a -> Bool
AddTop a -> AddTop a -> Ordering
AddTop a -> AddTop a -> AddTop a
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 a. Ord a => Eq (AddTop a)
forall a. Ord a => AddTop a -> AddTop a -> Bool
forall a. Ord a => AddTop a -> AddTop a -> Ordering
forall a. Ord a => AddTop a -> AddTop a -> AddTop a
$ccompare :: forall a. Ord a => AddTop a -> AddTop a -> Ordering
compare :: AddTop a -> AddTop a -> Ordering
$c< :: forall a. Ord a => AddTop a -> AddTop a -> Bool
< :: AddTop a -> AddTop a -> Bool
$c<= :: forall a. Ord a => AddTop a -> AddTop a -> Bool
<= :: AddTop a -> AddTop a -> Bool
$c> :: forall a. Ord a => AddTop a -> AddTop a -> Bool
> :: AddTop a -> AddTop a -> Bool
$c>= :: forall a. Ord a => AddTop a -> AddTop a -> Bool
>= :: AddTop a -> AddTop a -> Bool
$cmax :: forall a. Ord a => AddTop a -> AddTop a -> AddTop a
max :: AddTop a -> AddTop a -> AddTop a
$cmin :: forall a. Ord a => AddTop a -> AddTop a -> AddTop a
min :: AddTop a -> AddTop a -> AddTop a
Ord,Int -> AddTop a -> ShowS
[AddTop a] -> ShowS
AddTop a -> String
(Int -> AddTop a -> ShowS)
-> (AddTop a -> String) -> ([AddTop a] -> ShowS) -> Show (AddTop a)
forall a. Show a => Int -> AddTop a -> ShowS
forall a. Show a => [AddTop a] -> ShowS
forall a. Show a => AddTop a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> AddTop a -> ShowS
showsPrec :: Int -> AddTop a -> ShowS
$cshow :: forall a. Show a => AddTop a -> String
show :: AddTop a -> String
$cshowList :: forall a. Show a => [AddTop a] -> ShowS
showList :: [AddTop a] -> ShowS
Show)

elimAddTop ∷ b → (a → b) → AddTop a → b
elimAddTop :: forall b a. b -> (a -> b) -> AddTop a -> b
elimAddTop b
i a -> b
f = \case
  AddTop a
Top → b
i
  AddTop a
x → a -> b
f a
x

instance (POrd a) ⇒ POrd (AddTop a) where
  AddTop a
xT ⊑ :: AddTop a -> AddTop a -> Bool
⊑ AddTop a
yT = case (AddTop a
xT,AddTop a
yT) of
    (AddTop a
Top,AddTop a
Top) → Bool
True
    (AddTop a
Top,AddTop a
_) → Bool
False
    (AddTop a
_,AddTop a
Top) → Bool
True
    (AddTop a
x,AddTop a
y) → a
x a -> a -> Bool
forall a. POrd a => a -> a -> Bool
⊑ a
y
instance (Bot a) ⇒ Bot (AddTop a) where 
  bot :: AddTop a
bot = a -> AddTop a
forall a. a -> AddTop a
AddTop a
forall a. Bot a => a
bot
instance (Join a) ⇒ Join (AddTop a) where
  AddTop a
Top ⊔ :: AddTop a -> AddTop a -> AddTop a
⊔ AddTop a
_ = AddTop a
forall a. AddTop a
Top
  AddTop a
_ ⊔ AddTop a
Top = AddTop a
forall a. AddTop a
Top
  AddTop a
x ⊔ AddTop a
y = a -> AddTop a
forall a. a -> AddTop a
AddTop (a -> AddTop a) -> a -> AddTop a
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Join a => a -> a -> a
⊔ a
y
instance Top (AddTop a) where 
  top :: AddTop a
top = AddTop a
forall a. AddTop a
Top
instance (Meet a) ⇒ Meet (AddTop a) where
  AddTop a
Top ⊓ :: AddTop a -> AddTop a -> AddTop a
⊓ AddTop a
x = AddTop a
x
  AddTop a
x ⊓ AddTop a
Top = AddTop a
x
  AddTop a
x ⊓ AddTop a
y = a -> AddTop a
forall a. a -> AddTop a
AddTop (a -> AddTop a) -> a -> AddTop a
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Meet a => a -> a -> a
⊓ a
y
instance (JoinLattice a) ⇒ JoinLattice (AddTop a)
instance (Meet a) ⇒ MeetLattice (AddTop a)
instance (JoinLattice a,Meet a) ⇒ Lattice (AddTop a)
instance (Bot a,Difference a) ⇒ Difference (AddTop a) where
  AddTop a
_ ⊟ :: AddTop a -> AddTop a -> AddTop a
⊟ AddTop a
Top = AddTop a
forall a. Bot a => a
bot
  AddTop a
Top ⊟ AddTop a
_ = AddTop a
forall a. Top a => a
top
  AddTop a
x ⊟ AddTop a
y = a -> AddTop a
forall a. a -> AddTop a
AddTop (a -> AddTop a) -> a -> AddTop a
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Difference a => a -> a -> a
⊟ a
y

instance (Null a) ⇒ Null (AddTop a) where
  null :: AddTop a
null = a -> AddTop a
forall a. a -> AddTop a
AddTop a
forall a. Null a => a
null
instance (Append a) ⇒ Append (AddTop a) where
  AddTop a
Top ⧺ :: AddTop a -> AddTop a -> AddTop a
⧺ AddTop a
_ = AddTop a
forall a. AddTop a
Top
  AddTop a
_ ⧺ AddTop a
Top = AddTop a
forall a. AddTop a
Top
  AddTop a
x ⧺ AddTop a
y = a -> AddTop a
forall a. a -> AddTop a
AddTop (a -> AddTop a) -> a -> AddTop a
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Append a => a -> a -> a
⧺ a
y
instance (Monoid a) ⇒ Monoid (AddTop a)

instance (Zero a) ⇒ Zero (AddTop a) where
  zero :: AddTop a
zero = a -> AddTop a
forall a. a -> AddTop a
AddTop a
forall a. Zero a => a
zero
instance (Plus a) ⇒ Plus (AddTop a) where
  AddTop a
Top + :: AddTop a -> AddTop a -> AddTop a
+ AddTop a
_ = AddTop a
forall a. AddTop a
Top
  AddTop a
_ + AddTop a
Top = AddTop a
forall a. AddTop a
Top
  AddTop a
x + AddTop a
y = a -> AddTop a
forall a. a -> AddTop a
AddTop (a -> AddTop a) -> a -> AddTop a
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Plus a => a -> a -> a
+ a
y
instance (Additive a) ⇒ Additive (AddTop a)

instance (Times a) ⇒ Times (AddTop a) where
  AddTop a
Top × :: AddTop a -> AddTop a -> AddTop a
× AddTop a
_ = AddTop a
forall a. AddTop a
Top
  AddTop a
_ × AddTop a
Top = AddTop a
forall a. AddTop a
Top
  AddTop a
x × AddTop a
y = a -> AddTop a
forall a. a -> AddTop a
AddTop (a -> AddTop a) -> a -> AddTop a
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Times a => a -> a -> a
× a
y

instance Functor AddTop where 
  map :: forall a b. (a -> b) -> AddTop a -> AddTop b
map = (a -> b) -> AddTop a -> AddTop b
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
mmap
instance Return AddTop where 
  return :: forall a. a -> AddTop a
return = a -> AddTop a
forall a. a -> AddTop a
AddTop
instance Bind AddTop where 
  AddTop a
xM ≫= :: forall a b. AddTop a -> (a -> AddTop b) -> AddTop b
≫= a -> AddTop b
f = case AddTop a
xM of {AddTop a
Top → AddTop b
forall a. AddTop a
Top;AddTop a
x → a -> AddTop b
f a
x}
instance Monad AddTop
instance FunctorM AddTop where 
  mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> AddTop a -> m (AddTop b)
mapM a -> m b
f AddTop a
xM = case AddTop a
xM of {AddTop a
Top → AddTop b -> m (AddTop b)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return AddTop b
forall a. AddTop a
Top;AddTop a
x → (b -> AddTop b) -> m b -> m (AddTop b)
forall a b. (a -> b) -> m a -> m b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map b -> AddTop b
forall a. a -> AddTop a
AddTop (m b -> m (AddTop b)) -> m b -> m (AddTop b)
forall a b. (a -> b) -> a -> b
$ a -> m b
f a
x}

-- ===== --
-- AddBT --
-- ===== --

data AddBT a = BotBT | AddBT a | TopBT
  deriving (AddBT a -> AddBT a -> Bool
(AddBT a -> AddBT a -> Bool)
-> (AddBT a -> AddBT a -> Bool) -> Eq (AddBT a)
forall a. Eq a => AddBT a -> AddBT a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => AddBT a -> AddBT a -> Bool
== :: AddBT a -> AddBT a -> Bool
$c/= :: forall a. Eq a => AddBT a -> AddBT a -> Bool
/= :: AddBT a -> AddBT a -> Bool
Eq,Eq (AddBT a)
Eq (AddBT a) =>
(AddBT a -> AddBT a -> Ordering)
-> (AddBT a -> AddBT a -> Bool)
-> (AddBT a -> AddBT a -> Bool)
-> (AddBT a -> AddBT a -> Bool)
-> (AddBT a -> AddBT a -> Bool)
-> (AddBT a -> AddBT a -> AddBT a)
-> (AddBT a -> AddBT a -> AddBT a)
-> Ord (AddBT a)
AddBT a -> AddBT a -> Bool
AddBT a -> AddBT a -> Ordering
AddBT a -> AddBT a -> AddBT a
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 a. Ord a => Eq (AddBT a)
forall a. Ord a => AddBT a -> AddBT a -> Bool
forall a. Ord a => AddBT a -> AddBT a -> Ordering
forall a. Ord a => AddBT a -> AddBT a -> AddBT a
$ccompare :: forall a. Ord a => AddBT a -> AddBT a -> Ordering
compare :: AddBT a -> AddBT a -> Ordering
$c< :: forall a. Ord a => AddBT a -> AddBT a -> Bool
< :: AddBT a -> AddBT a -> Bool
$c<= :: forall a. Ord a => AddBT a -> AddBT a -> Bool
<= :: AddBT a -> AddBT a -> Bool
$c> :: forall a. Ord a => AddBT a -> AddBT a -> Bool
> :: AddBT a -> AddBT a -> Bool
$c>= :: forall a. Ord a => AddBT a -> AddBT a -> Bool
>= :: AddBT a -> AddBT a -> Bool
$cmax :: forall a. Ord a => AddBT a -> AddBT a -> AddBT a
max :: AddBT a -> AddBT a -> AddBT a
$cmin :: forall a. Ord a => AddBT a -> AddBT a -> AddBT a
min :: AddBT a -> AddBT a -> AddBT a
Ord,Int -> AddBT a -> ShowS
[AddBT a] -> ShowS
AddBT a -> String
(Int -> AddBT a -> ShowS)
-> (AddBT a -> String) -> ([AddBT a] -> ShowS) -> Show (AddBT a)
forall a. Show a => Int -> AddBT a -> ShowS
forall a. Show a => [AddBT a] -> ShowS
forall a. Show a => AddBT a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> AddBT a -> ShowS
showsPrec :: Int -> AddBT a -> ShowS
$cshow :: forall a. Show a => AddBT a -> String
show :: AddBT a -> String
$cshowList :: forall a. Show a => [AddBT a] -> ShowS
showList :: [AddBT a] -> ShowS
Show)

instance Bot (AddBT a) where 
  bot :: AddBT a
bot = AddBT a
forall a. AddBT a
BotBT
instance (Join a) ⇒ Join (AddBT a) where
  AddBT a
BotBT ⊔ :: AddBT a -> AddBT a -> AddBT a
⊔ AddBT a
x = AddBT a
x
  AddBT a
x ⊔ AddBT a
BotBT = AddBT a
x
  AddBT a
TopBT ⊔ AddBT a
_ = AddBT a
forall a. AddBT a
TopBT
  AddBT a
_ ⊔ AddBT a
TopBT = AddBT a
forall a. AddBT a
TopBT
  AddBT a
x ⊔ AddBT a
y = a -> AddBT a
forall a. a -> AddBT a
AddBT (a -> AddBT a) -> a -> AddBT a
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Join a => a -> a -> a
⊔ a
y
instance Top (AddBT a) where 
  top :: AddBT a
top = AddBT a
forall a. AddBT a
TopBT
instance (Meet a) ⇒ Meet (AddBT a) where
  AddBT a
BotBT ⊓ :: AddBT a -> AddBT a -> AddBT a
⊓ AddBT a
_ = AddBT a
forall a. AddBT a
BotBT
  AddBT a
_ ⊓ AddBT a
BotBT = AddBT a
forall a. AddBT a
BotBT
  AddBT a
TopBT ⊓ AddBT a
x = AddBT a
x
  AddBT a
x ⊓ AddBT a
TopBT = AddBT a
x
  AddBT a
x ⊓ AddBT a
y = a -> AddBT a
forall a. a -> AddBT a
AddBT (a -> AddBT a) -> a -> AddBT a
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Meet a => a -> a -> a
⊓ a
y
instance (Join a) ⇒ JoinLattice (AddBT a)
instance (Meet a) ⇒ MeetLattice (AddBT a)
instance (Join a,Meet a) ⇒ Lattice (AddBT a)
instance Functor AddBT where 
  map :: forall a b. (a -> b) -> AddBT a -> AddBT b
map = (a -> b) -> AddBT a -> AddBT b
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
mmap
instance Return AddBT where 
  return :: forall a. a -> AddBT a
return = a -> AddBT a
forall a. a -> AddBT a
AddBT
instance Bind AddBT where 
  AddBT a
xM ≫= :: forall a b. AddBT a -> (a -> AddBT b) -> AddBT b
≫= a -> AddBT b
f = case AddBT a
xM of {AddBT a
TopBT → AddBT b
forall a. AddBT a
TopBT;AddBT a
BotBT → AddBT b
forall a. AddBT a
BotBT;AddBT a
x → a -> AddBT b
f a
x}
instance Monad AddBT
instance FunctorM AddBT where 
  mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> AddBT a -> m (AddBT b)
mapM a -> m b
f AddBT a
xM = case AddBT a
xM of {AddBT a
TopBT → AddBT b -> m (AddBT b)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return AddBT b
forall a. AddBT a
TopBT;AddBT a
BotBT → AddBT b -> m (AddBT b)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return AddBT b
forall a. AddBT a
BotBT;AddBT a
x → (b -> AddBT b) -> m b -> m (AddBT b)
forall a b. (a -> b) -> m a -> m b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map b -> AddBT b
forall a. a -> AddBT a
AddBT (m b -> m (AddBT b)) -> m b -> m (AddBT b)
forall a b. (a -> b) -> a -> b
$ a -> m b
f a
x}

-- LENSES --

addTopL ∷ AddTop a ⌲ a
addTopL :: forall a. AddTop a ⌲ a
addTopL = (a -> AddTop a) -> (AddTop a -> 𝑂 a) -> AddTop a ⌲ a
forall b a. (b -> a) -> (a -> 𝑂 b) -> a ⌲ b
prism a -> AddTop a
forall a. a -> AddTop a
AddTop ((AddTop a -> 𝑂 a) -> AddTop a ⌲ a)
-> (AddTop a -> 𝑂 a) -> AddTop a ⌲ a
forall a b. (a -> b) -> a -> b
$ \case
  AddTop a
x → a -> 𝑂 a
forall a. a -> 𝑂 a
Some a
x
  AddTop a
_ → 𝑂 a
forall a. 𝑂 a
None

nullZOML ∷ ZOM a ⌲ ()
nullZOML :: forall a. ZOM a ⌲ ()
nullZOML = (() -> ZOM a) -> (ZOM a -> 𝑂 ()) -> ZOM a ⌲ ()
forall b a. (b -> a) -> (a -> 𝑂 b) -> a ⌲ b
prism (ZOM a -> () -> ZOM a
forall a b. a -> b -> a
const ZOM a
forall a. ZOM a
NullZOM) ((ZOM a -> 𝑂 ()) -> ZOM a ⌲ ()) -> (ZOM a -> 𝑂 ()) -> ZOM a ⌲ ()
forall a b. (a -> b) -> a -> b
$ \case
  ZOM a
NullZOM → () -> 𝑂 ()
forall a. a -> 𝑂 a
Some ()
  ZOM a
_ → 𝑂 ()
forall a. 𝑂 a
None

oneZOML ∷ ZOM a ⌲ a
oneZOML :: forall a. ZOM a ⌲ a
oneZOML = (a -> ZOM a) -> (ZOM a -> 𝑂 a) -> ZOM a ⌲ a
forall b a. (b -> a) -> (a -> 𝑂 b) -> a ⌲ b
prism a -> ZOM a
forall a. a -> ZOM a
OneZOM ((ZOM a -> 𝑂 a) -> ZOM a ⌲ a) -> (ZOM a -> 𝑂 a) -> ZOM a ⌲ a
forall a b. (a -> b) -> a -> b
$ \case
  OneZOM a
x → a -> 𝑂 a
forall a. a -> 𝑂 a
Some a
x
  ZOM a
_ → 𝑂 a
forall a. 𝑂 a
None

moreZOML ∷ ZOM a ⌲ ()
moreZOML :: forall a. ZOM a ⌲ ()
moreZOML = (() -> ZOM a) -> (ZOM a -> 𝑂 ()) -> ZOM a ⌲ ()
forall b a. (b -> a) -> (a -> 𝑂 b) -> a ⌲ b
prism (ZOM a -> () -> ZOM a
forall a b. a -> b -> a
const ZOM a
forall a. ZOM a
MoreZOM) ((ZOM a -> 𝑂 ()) -> ZOM a ⌲ ()) -> (ZOM a -> 𝑂 ()) -> ZOM a ⌲ ()
forall a b. (a -> b) -> a -> b
$ \case
  ZOM a
MoreZOM → () -> 𝑂 ()
forall a. a -> 𝑂 a
Some ()
  ZOM a
_ → 𝑂 ()
forall a. 𝑂 a
None