module UVMHS.Core.Data.Option where

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

import qualified Prelude as HS

instance Functor 𝑂 where 
  map :: forall a b. (a -> b) -> 𝑂 a -> 𝑂 b
map = (a -> b) -> 𝑂 a -> 𝑂 b
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
mmap
instance Return 𝑂 where 
  return :: forall a. a -> 𝑂 a
return = a -> 𝑂 a
forall a. a -> 𝑂 a
Some
instance Bind 𝑂 where 
  𝑂 a
xO ≫= :: forall a b. 𝑂 a -> (a -> 𝑂 b) -> 𝑂 b
≫= a -> 𝑂 b
k = case 𝑂 a
xO of {𝑂 a
None → 𝑂 b
forall a. 𝑂 a
None;Some a
x → a -> 𝑂 b
k a
x}
instance Monad 𝑂
instance FunctorM 𝑂 where 
  mapM :: forall (m :: * -> *) a b. Monad m => (a -> m b) -> 𝑂 a -> m (𝑂 b)
mapM a -> m b
f = \case
    𝑂 a
None → 𝑂 b -> m (𝑂 b)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return 𝑂 b
forall a. 𝑂 a
None
    Some a
x → b -> 𝑂 b
forall a. a -> 𝑂 a
Some (b -> 𝑂 b) -> m b -> m (𝑂 b)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ a -> m b
f a
x
instance (Null a) ⇒ Null (𝑂 a) where 
  null :: 𝑂 a
null = a -> 𝑂 a
forall a. a -> 𝑂 a
Some a
forall a. Null a => a
null
instance (Append a) ⇒ Append (𝑂 a) where
  𝑂 a
None ⧺ :: 𝑂 a -> 𝑂 a -> 𝑂 a
⧺ 𝑂 a
_ = 𝑂 a
forall a. 𝑂 a
None
  𝑂 a
_ ⧺ 𝑂 a
None = 𝑂 a
forall a. 𝑂 a
None
  Some a
x ⧺ Some a
y = a -> 𝑂 a
forall a. a -> 𝑂 a
Some (a -> 𝑂 a) -> a -> 𝑂 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 (𝑂 a)

instance ToIter a (𝑂 a) where iter :: 𝑂 a -> 𝐼 a
iter = 𝑂 a -> 𝐼 a
forall a. 𝑂 a -> 𝐼 a
iter𝑂

iter𝑂 ∷ 𝑂 a → 𝐼 a
iter𝑂 :: forall a. 𝑂 a -> 𝐼 a
iter𝑂 𝑂 a
xO = (forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b) -> 𝐼 a
forall a.
(forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b) -> 𝐼 a
𝐼 ((forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
 -> 𝐼 a)
-> (forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
-> 𝐼 a
forall a b. (a -> b) -> a -> b
HS.$ \ a -> b -> (b -> b) -> b
f b
i b -> b
𝓀 → case 𝑂 a
xO of
    𝑂 a
None → b -> b
𝓀 b
i
    Some a
x → a -> b -> (b -> b) -> b
f a
x b
i b -> b
𝓀

instance 𝑂 a ⇄ (() ∨ a) where
  isoto :: 𝑂 a -> () ∨ a
isoto = \case
    𝑂 a
None → () -> () ∨ a
forall a b. a -> a ∨ b
Inl ()
    Some a
x → a -> () ∨ a
forall a b. b -> a ∨ b
Inr a
x
  isofr :: (() ∨ a) -> 𝑂 a
isofr = \case
    Inl () → 𝑂 a
forall a. 𝑂 a
None
    Inr a
x → a -> 𝑂 a
forall a. a -> 𝑂 a
Some a
x

elim𝑂 ∷ (() → b) → (a → b) → 𝑂 a → b
elim𝑂 :: forall b a. (() -> b) -> (a -> b) -> 𝑂 a -> b
elim𝑂 () -> b
f a -> b
g = \case
  𝑂 a
None → () -> b
f ()
  Some a
x → a -> b
g a
x

isNone ∷ 𝑂 a → 𝔹
isNone :: forall a. 𝑂 a -> 𝔹
isNone = \case
  𝑂 a
None → 𝔹
True
  Some a
_ → 𝔹
False

isSome ∷ 𝑂 a → 𝔹
isSome :: forall a. 𝑂 a -> 𝔹
isSome = \case
  𝑂 a
None → 𝔹
False
  Some a
_ → 𝔹
True

ifNone ∷ a → 𝑂 a → a
ifNone :: forall a. a -> 𝑂 a -> a
ifNone a
i = \case
  𝑂 a
None → a
i
  Some a
x → a
x

ifNoneZ ∷ a → 𝑂 a → a
ifNoneZ :: forall a. a -> 𝑂 a -> a
ifNoneZ ~a
i = \case
  𝑂 a
None → a
i
  Some a
x → a
x

ifNoneM ∷ (Return m) ⇒ m a → 𝑂 a → m a
ifNoneM :: forall (m :: * -> *) a. Return m => m a -> 𝑂 a -> m a
ifNoneM m a
xM = \case
  𝑂 a
None → m a
xM
  Some a
x → a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return (a -> m a) -> a -> m a
forall a b. (a -> b) -> a -> b
$ a
x

ifNoneMZ ∷ (Return m) ⇒ m a → 𝑂 a → m a
ifNoneMZ :: forall (m :: * -> *) a. Return m => m a -> 𝑂 a -> m a
ifNoneMZ ~m a
xM = \case
  𝑂 a
None → m a
xM
  Some a
x → a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return (a -> m a) -> a -> m a
forall a b. (a -> b) -> a -> b
$ a
x

first ∷ 𝑂 a → 𝑂 a → 𝑂 a
first :: forall a. 𝑂 a -> 𝑂 a -> 𝑂 a
first = \case
  𝑂 a
None → 𝑂 a -> 𝑂 a
forall a. a -> a
id
  Some a
x → 𝑂 a -> 𝑂 a -> 𝑂 a
forall a b. a -> b -> a
const (𝑂 a -> 𝑂 a -> 𝑂 a) -> 𝑂 a -> 𝑂 a -> 𝑂 a
forall a b. (a -> b) -> a -> b
$ a -> 𝑂 a
forall a. a -> 𝑂 a
Some a
x

last ∷ 𝑂 a → 𝑂 a → 𝑂 a
last :: forall a. 𝑂 a -> 𝑂 a -> 𝑂 a
last = (𝑂 a -> 𝑂 a -> 𝑂 a) -> 𝑂 a -> 𝑂 a -> 𝑂 a
forall a b c. (a -> b -> c) -> b -> a -> c
flip 𝑂 a -> 𝑂 a -> 𝑂 a
forall a. 𝑂 a -> 𝑂 a -> 𝑂 a
first