module UVMHS.Lib.ZerInf where

import UVMHS.Core

-- ====== --
-- AddZer --
-- ====== --

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

elimAddZer ∷ b → (a → b) → AddZer a → b
elimAddZer :: forall b a. b -> (a -> b) -> AddZer a -> b
elimAddZer b
i a -> b
f = \case
  AddZer a
Zer → b
i
  AddZer a
x → a -> b
f a
x

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

instance Zero (AddZer a) where zero :: AddZer a
zero = AddZer a
forall a. AddZer a
Zer
instance (One a) ⇒ One (AddZer a) where one :: AddZer a
one = a -> AddZer a
forall a. a -> AddZer a
AddZer a
forall a. One a => a
one
instance (Plus a) ⇒ Plus (AddZer a) where
  AddZer a
Zer + :: AddZer a -> AddZer a -> AddZer a
+ AddZer a
y = AddZer a
y
  AddZer a
x + AddZer a
Zer = AddZer a
x
  AddZer a
x + AddZer a
y = a -> AddZer a
forall a. a -> AddZer a
AddZer (a -> AddZer a) -> a -> AddZer a
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Plus a => a -> a -> a
+ a
y
instance (Times a) ⇒ Times (AddZer a) where
  AddZer a
Zer × :: AddZer a -> AddZer a -> AddZer a
× AddZer a
y = AddZer a
y
  AddZer a
x × AddZer a
Zer = AddZer a
x
  AddZer a
x × AddZer a
y = a -> AddZer a
forall a. a -> AddZer a
AddZer (a -> AddZer a) -> a -> AddZer a
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Times a => a -> a -> a
× a
y
instance (Divide a,Top a) ⇒ Divide (AddZer a) where
  AddZer a
Zer / :: AddZer a -> AddZer a -> AddZer a
/ AddZer a
Zer = 𝕊 -> AddZer a
forall a. STACK => 𝕊 -> a
error 𝕊
"0 / 0"
  AddZer a
Zer / AddZer a
_ = AddZer a
forall a. AddZer a
Zer
  AddZer a
_ / AddZer a
Zer = AddZer a
forall a. Top a => a
top
  AddZer a
x / AddZer a
y = a -> AddZer a
forall a. a -> AddZer a
AddZer (a -> AddZer a) -> a -> AddZer a
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Divide a => a -> a -> a
/ a
y
instance (DivMod a,Top a) ⇒ DivMod (AddZer a) where
  AddZer a
Zer ⌿ :: AddZer a -> AddZer a -> AddZer a
⌿ AddZer a
Zer = 𝕊 -> AddZer a
forall a. STACK => 𝕊 -> a
error 𝕊
"0 ⌿ 0"
  AddZer a
Zer ⌿ AddZer a
_ = AddZer a
forall a. AddZer a
Zer
  AddZer a
_ ⌿ AddZer a
Zer = AddZer a
forall a. Top a => a
top
  AddZer a
x ⌿ AddZer a
y = a -> AddZer a
forall a. a -> AddZer a
AddZer (a -> AddZer a) -> a -> AddZer a
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. DivMod a => a -> a -> a
⌿ a
y
  AddZer a
Zer ÷ :: AddZer a -> AddZer a -> AddZer a
÷ AddZer a
_ = AddZer a
forall a. AddZer a
Zer
  AddZer a
_ ÷ AddZer a
Zer = 𝕊 -> AddZer a
forall a. STACK => 𝕊 -> a
error 𝕊
"mod Zer"
  AddZer a
x ÷ AddZer a
y = a -> AddZer a
forall a. a -> AddZer a
AddZer (a -> AddZer a) -> a -> AddZer a
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. DivMod a => a -> a -> a
÷ a
y
instance (Pon a) ⇒ Pon (AddZer a) where
  AddZer a
Zer ^^ :: AddZer a -> ℕ -> AddZer a
^^ ℕ
_ = AddZer a
forall a. AddZer a
Zer
  AddZer a
x ^^ ℕ
n = a -> AddZer a
forall a. a -> AddZer a
AddZer (a -> AddZer a) -> a -> AddZer a
forall a b. (a -> b) -> a -> b
$ a
x a -> ℕ -> a
forall a. Pon a => a -> ℕ -> a
^^ ℕ
n
instance (Pow a,One a) ⇒ Pow (AddZer a) where
  AddZer a
_ ^ :: AddZer a -> AddZer a -> AddZer a
^ AddZer a
Zer = a -> AddZer a
forall a. a -> AddZer a
AddZer a
forall a. One a => a
one
  AddZer a
Zer ^ AddZer a
_ = AddZer a
forall a. AddZer a
Zer
  AddZer a
x ^ AddZer a
y = a -> AddZer a
forall a. a -> AddZer a
AddZer (a -> AddZer a) -> a -> AddZer a
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Pow a => a -> a -> a
^ a
y
instance (Root a) ⇒ Root (AddZer a) where
  root :: AddZer a -> AddZer a
root AddZer a
Zer = AddZer a
forall a. AddZer a
Zer
  root (AddZer a
x) = a -> AddZer a
forall a. a -> AddZer a
AddZer (a -> AddZer a) -> a -> AddZer a
forall a b. (a -> b) -> a -> b
$ a -> a
forall a. Root a => a -> a
root a
x
instance (Log a,Top a,Minus a) ⇒ Log (AddZer a) where
  log :: AddZer a -> AddZer a
log AddZer a
Zer = 𝕊 -> AddZer a
forall a. STACK => 𝕊 -> a
error 𝕊
"log of Zer"
  log (AddZer a
x) = a -> AddZer a
forall a. a -> AddZer a
AddZer (a -> AddZer a) -> a -> AddZer a
forall a b. (a -> b) -> a -> b
$ a -> a
forall a. Log a => a -> a
log a
x
instance (Efn a,One a) ⇒ Efn (AddZer a) where
  efn :: AddZer a -> AddZer a
efn AddZer a
Zer = a -> AddZer a
forall a. a -> AddZer a
AddZer a
forall a. One a => a
one
  efn (AddZer a
x) = a -> AddZer a
forall a. a -> AddZer a
AddZer (a -> AddZer a) -> a -> AddZer a
forall a b. (a -> b) -> a -> b
$ a -> a
forall a. Efn a => a -> a
efn a
x

-- ====== --
-- AddInf --
-- ====== --

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

elimAddInf ∷ b → (a → b) → AddInf a → b
elimAddInf :: forall b a. b -> (a -> b) -> AddInf a -> b
elimAddInf b
i a -> b
f = \case
  AddInf a
Inf → b
i
  AddInf a
x → a -> b
f a
x

instance (Null a) ⇒ Null (AddInf a) where null :: AddInf a
null = a -> AddInf a
forall a. a -> AddInf a
AddInf a
forall a. Null a => a
null
instance (Append a) ⇒ Append (AddInf a) where
  AddInf a
Inf ⧺ :: AddInf a -> AddInf a -> AddInf a
⧺ AddInf a
_ = AddInf a
forall a. AddInf a
Inf
  AddInf a
_ ⧺ AddInf a
Inf = AddInf a
forall a. AddInf a
Inf
  AddInf a
x ⧺ AddInf a
y = a -> AddInf a
forall a. a -> AddInf a
AddInf (a
x a -> a -> a
forall a. Append a => a -> a -> a
⧺ a
y)
instance (Monoid a) ⇒ Monoid (AddInf a)

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

instance (Zero a) ⇒ Zero (AddInf a) where zero :: AddInf a
zero = a -> AddInf a
forall a. a -> AddInf a
AddInf a
forall a. Zero a => a
zero
instance (One a) ⇒ One (AddInf a) where one :: AddInf a
one = a -> AddInf a
forall a. a -> AddInf a
AddInf a
forall a. One a => a
one
instance (Plus a) ⇒ Plus (AddInf a) where
  AddInf a
Inf + :: AddInf a -> AddInf a -> AddInf a
+ AddInf a
_ = AddInf a
forall a. AddInf a
Inf
  AddInf a
_ + AddInf a
Inf = AddInf a
forall a. AddInf a
Inf
  AddInf a
x + AddInf a
y = a -> AddInf a
forall a. a -> AddInf a
AddInf (a -> AddInf a) -> a -> AddInf a
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Plus a => a -> a -> a
+ a
y
instance (Times a) ⇒ Times (AddInf a) where
  AddInf a
Inf × :: AddInf a -> AddInf a -> AddInf a
× AddInf a
_ = AddInf a
forall a. AddInf a
Inf
  AddInf a
_ × AddInf a
Inf = AddInf a
forall a. AddInf a
Inf
  AddInf a
x × AddInf a
y = a -> AddInf a
forall a. a -> AddInf a
AddInf (a -> AddInf a) -> a -> AddInf a
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Times a => a -> a -> a
× a
y
instance (Divide a,Zero a,Eq a) ⇒ Divide (AddInf a) where
  AddInf a
Inf / :: AddInf a -> AddInf a -> AddInf a
/ AddInf a
Inf = 𝕊 -> AddInf a
forall a. STACK => 𝕊 -> a
error 𝕊
"∞ / ∞"
  AddInf a
Inf / AddInf a
y 
    | AddInf a
y AddInf a -> AddInf a -> Bool
forall a. Eq a => a -> a -> Bool
≡ AddInf a
forall a. Zero a => a
zero = 𝕊 -> AddInf a
forall a. STACK => 𝕊 -> a
error 𝕊
"∞ / 0"
    | Bool
otherwise = AddInf a
forall a. AddInf a
Inf
  AddInf a
_ / AddInf a
Inf = AddInf a
forall a. Zero a => a
zero
  AddInf a
x / AddInf a
y = a -> AddInf a
forall a. a -> AddInf a
AddInf (a -> AddInf a) -> a -> AddInf a
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Divide a => a -> a -> a
/ a
y
instance (DivMod a,Zero a) ⇒ DivMod (AddInf a) where
  AddInf a
Inf ⌿ :: AddInf a -> AddInf a -> AddInf a
⌿ AddInf a
_ = AddInf a
forall a. AddInf a
Inf
  AddInf a
_ ⌿ AddInf a
Inf = AddInf a
forall a. Zero a => a
zero
  AddInf a
x ⌿ AddInf a
y = a -> AddInf a
forall a. a -> AddInf a
AddInf (a -> AddInf a) -> a -> AddInf a
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. DivMod a => a -> a -> a
⌿ a
y
  AddInf a
Inf ÷ :: AddInf a -> AddInf a -> AddInf a
÷ AddInf a
x = AddInf a
x
  AddInf a
x ÷ AddInf a
Inf = AddInf a
x
  AddInf a
x ÷ AddInf a
y = a -> AddInf a
forall a. a -> AddInf a
AddInf (a -> AddInf a) -> a -> AddInf a
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. DivMod a => a -> a -> a
÷ a
y
instance (Pon a,One a) ⇒ Pon (AddInf a) where
  AddInf a
Inf ^^ :: AddInf a -> ℕ -> AddInf a
^^ ℕ
n 
    | ℕ
n ℕ -> ℕ -> Bool
forall a. Eq a => a -> a -> Bool
≡ ℕ
forall a. Zero a => a
zero = AddInf a
forall a. One a => a
one
    | Bool
otherwise = AddInf a
forall a. AddInf a
Inf
  AddInf a
x ^^ ℕ
n = a -> AddInf a
forall a. a -> AddInf a
AddInf (a -> AddInf a) -> a -> AddInf a
forall a b. (a -> b) -> a -> b
$ a
x a -> ℕ -> a
forall a. Pon a => a -> ℕ -> a
^^ ℕ
n
instance (Pow a,One a) ⇒ Pow (AddInf a) where
  AddInf a
_ ^ :: AddInf a -> AddInf a -> AddInf a
^ AddInf a
_ = AddInf a
forall a. STACK => a
undefined
instance (Root a) ⇒ Root (AddInf a) where
  root :: AddInf a -> AddInf a
root AddInf a
_ = AddInf a
forall a. STACK => a
undefined
instance (Log a,Top a,Minus a) ⇒ Log (AddInf a) where
  log :: AddInf a -> AddInf a
log AddInf a
_ = AddInf a
forall a. STACK => a
undefined
instance (Efn a,One a) ⇒ Efn (AddInf a) where
  efn :: AddInf a -> AddInf a
efn AddInf a
_ = AddInf a
forall a. STACK => a
undefined

-- ===== --
-- AddZI --
-- ===== --

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

instance Bot (AddZI a) where bot :: AddZI a
bot = AddZI a
forall a. AddZI a
ZerZI
instance (Join a) ⇒ Join (AddZI a) where
  AddZI a
ZerZI ⊔ :: AddZI a -> AddZI a -> AddZI a
⊔ AddZI a
x = AddZI a
x
  AddZI a
x ⊔ AddZI a
ZerZI = AddZI a
x
  AddZI a
InfZI ⊔ AddZI a
_ = AddZI a
forall a. AddZI a
InfZI
  AddZI a
_ ⊔ AddZI a
InfZI = AddZI a
forall a. AddZI a
InfZI
  AddZI a
x ⊔ AddZI a
y = a -> AddZI a
forall a. a -> AddZI a
AddZI (a -> AddZI a) -> a -> AddZI a
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Join a => a -> a -> a
⊔ a
y
instance Top (AddZI a) where top :: AddZI a
top = AddZI a
forall a. AddZI a
InfZI
instance (Meet a) ⇒ Meet (AddZI a) where
  AddZI a
ZerZI ⊓ :: AddZI a -> AddZI a -> AddZI a
⊓ AddZI a
_ = AddZI a
forall a. AddZI a
ZerZI
  AddZI a
_ ⊓ AddZI a
ZerZI = AddZI a
forall a. AddZI a
ZerZI
  AddZI a
InfZI ⊓ AddZI a
x = AddZI a
x
  AddZI a
x ⊓ AddZI a
InfZI = AddZI a
x
  AddZI a
x ⊓ AddZI a
y = a -> AddZI a
forall a. a -> AddZI a
AddZI (a -> AddZI a) -> a -> AddZI 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 (AddZI a)
instance (Meet a) ⇒ MeetLattice (AddZI a)
instance (Join a,Meet a) ⇒ Lattice (AddZI a)
instance Functor AddZI where map :: forall a b. (a -> b) -> AddZI a -> AddZI b
map = (a -> b) -> AddZI a -> AddZI b
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
mmap
instance Return AddZI where return :: forall a. a -> AddZI a
return = a -> AddZI a
forall a. a -> AddZI a
AddZI
instance Bind AddZI where AddZI a
xM ≫= :: forall a b. AddZI a -> (a -> AddZI b) -> AddZI b
≫= a -> AddZI b
f = case AddZI a
xM of {AddZI a
InfZI → AddZI b
forall a. AddZI a
InfZI;AddZI a
ZerZI → AddZI b
forall a. AddZI a
ZerZI;AddZI a
x → a -> AddZI b
f a
x}
instance Monad AddZI
instance FunctorM AddZI where mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> AddZI a -> m (AddZI b)
mapM a -> m b
f AddZI a
xM = case AddZI a
xM of {AddZI a
InfZI → AddZI b -> m (AddZI b)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return AddZI b
forall a. AddZI a
InfZI;AddZI a
ZerZI → AddZI b -> m (AddZI b)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return AddZI b
forall a. AddZI a
ZerZI;AddZI a
x → (b -> AddZI b) -> m b -> m (AddZI b)
forall a b. (a -> b) -> m a -> m b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map b -> AddZI b
forall a. a -> AddZI a
AddZI (m b -> m (AddZI b)) -> m b -> m (AddZI b)
forall a b. (a -> b) -> a -> b
$ a -> m b
f a
x}