module UVMHS.Core.Data.Choice where

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

instance Functor ((∨) a) where 
  map :: forall a b. (a -> b) -> (a ∨ a) -> a ∨ b
map a -> b
f = \case
    Inl a
x → a -> a ∨ b
forall a b. a -> a ∨ b
Inl a
x
    Inr a
y → b -> a ∨ b
forall a b. b -> a ∨ b
Inr (b -> a ∨ b) -> b -> a ∨ b
forall a b. (a -> b) -> a -> b
$ a -> b
f a
y
instance Return ((∨) a) where 
  return :: forall a. a -> a ∨ a
return = a -> a ∨ a
forall a b. b -> a ∨ b
Inr
instance Bind ((∨) a) where
  Inl a
x ≫= :: forall a b. (a ∨ a) -> (a -> a ∨ b) -> a ∨ b
≫= a -> a ∨ b
_ = a -> a ∨ b
forall a b. a -> a ∨ b
Inl a
x
  Inr a
y ≫= a -> a ∨ b
k = a -> a ∨ b
k a
y
instance Monad ((∨) a)
instance FunctorM ((∨) a) where
  mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> (a ∨ a) -> m (a ∨ b)
mapM a -> m b
f = \case
    Inl a
x → (a ∨ b) -> m (a ∨ b)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return ((a ∨ b) -> m (a ∨ b)) -> (a ∨ b) -> m (a ∨ b)
forall a b. (a -> b) -> a -> b
$ a -> a ∨ b
forall a b. a -> a ∨ b
Inl a
x
    Inr a
y → do
      b
y' ← a -> m b
f a
y
      (a ∨ b) -> m (a ∨ b)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return ((a ∨ b) -> m (a ∨ b)) -> (a ∨ b) -> m (a ∨ b)
forall a b. (a -> b) -> a -> b
$ b -> a ∨ b
forall a b. b -> a ∨ b
Inr b
y'

instance (Null b) ⇒ Null (a ∨ b) where 
  null :: a ∨ b
null = b -> a ∨ b
forall a b. b -> a ∨ b
Inr b
forall a. Null a => a
null
instance (Append a,Append b) ⇒ Append (a ∨ b) where 
  Inl a
x ⧺ :: (a ∨ b) -> (a ∨ b) -> a ∨ b
⧺ Inl a
y = a -> a ∨ b
forall a b. a -> a ∨ b
Inl (a
x a -> a -> a
forall a. Append a => a -> a -> a
⧺ a
y)
  Inl a
x ⧺ Inr b
_ = a -> a ∨ b
forall a b. a -> a ∨ b
Inl a
x
  Inr b
_ ⧺ Inl a
y = a -> a ∨ b
forall a b. a -> a ∨ b
Inl a
y
  Inr b
x ⧺ Inr b
y = b -> a ∨ b
forall a b. b -> a ∨ b
Inr (b
x b -> b -> b
forall a. Append a => a -> a -> a
⧺ b
y)
instance (Append a,Monoid b) ⇒ Monoid (a ∨ b) 

elimChoice ∷ (a → c) → (b → c) → a ∨ b → c
elimChoice :: forall a c b. (a -> c) -> (b -> c) -> (a ∨ b) -> c
elimChoice a -> c
f₁ b -> c
f₂ = \case
  Inl a
x → a -> c
f₁ a
x
  Inr b
y → b -> c
f₂ b
y

mapChoice ∷ (a₁ → a₂) → (b₁ → b₂) → a₁ ∨ b₁ → a₂ ∨ b₂
mapChoice :: forall a₁ a₂ b₁ b₂.
(a₁ -> a₂) -> (b₁ -> b₂) -> (a₁ ∨ b₁) -> a₂ ∨ b₂
mapChoice a₁ -> a₂
f b₁ -> b₂
g = (a₁ -> a₂ ∨ b₂) -> (b₁ -> a₂ ∨ b₂) -> (a₁ ∨ b₁) -> a₂ ∨ b₂
forall a c b. (a -> c) -> (b -> c) -> (a ∨ b) -> c
elimChoice (a₂ -> a₂ ∨ b₂
forall a b. a -> a ∨ b
Inl (a₂ -> a₂ ∨ b₂) -> (a₁ -> a₂) -> a₁ -> a₂ ∨ b₂
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ a₁ -> a₂
f) (b₂ -> a₂ ∨ b₂
forall a b. b -> a ∨ b
Inr (b₂ -> a₂ ∨ b₂) -> (b₁ -> b₂) -> b₁ -> a₂ ∨ b₂
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ b₁ -> b₂
g)

mapInl ∷ (a₁ → a₂) → a₁ ∨ b → a₂ ∨ b
mapInl :: forall a₁ a₂ b. (a₁ -> a₂) -> (a₁ ∨ b) -> a₂ ∨ b
mapInl a₁ -> a₂
f = (a₁ -> a₂) -> (b -> b) -> (a₁ ∨ b) -> a₂ ∨ b
forall a₁ a₂ b₁ b₂.
(a₁ -> a₂) -> (b₁ -> b₂) -> (a₁ ∨ b₁) -> a₂ ∨ b₂
mapChoice a₁ -> a₂
f b -> b
forall a. a -> a
id

mapInr ∷ (b₁ → b₂) → a ∨ b₁ → a ∨ b₂
mapInr :: forall b₁ b₂ a. (b₁ -> b₂) -> (a ∨ b₁) -> a ∨ b₂
mapInr b₁ -> b₂
f = (a -> a) -> (b₁ -> b₂) -> (a ∨ b₁) -> a ∨ b₂
forall a₁ a₂ b₁ b₂.
(a₁ -> a₂) -> (b₁ -> b₂) -> (a₁ ∨ b₁) -> a₂ ∨ b₂
mapChoice a -> a
forall a. a -> a
id b₁ -> b₂
f

mapMChoice ∷ (Monad m) ⇒ (a → m a') → (b → m b') → a ∨ b → m (a' ∨ b')
mapMChoice :: forall (m :: * -> *) a a' b b'.
Monad m =>
(a -> m a') -> (b -> m b') -> (a ∨ b) -> m (a' ∨ b')
mapMChoice a -> m a'
f b -> m b'
g = \case
  Inl a
x → do
    a'
x' ← a -> m a'
f a
x
    (a' ∨ b') -> m (a' ∨ b')
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return ((a' ∨ b') -> m (a' ∨ b')) -> (a' ∨ b') -> m (a' ∨ b')
forall a b. (a -> b) -> a -> b
$ a' -> a' ∨ b'
forall a b. a -> a ∨ b
Inl a'
x'
  Inr b
y → do
    b'
y' ← b -> m b'
g b
y
    (a' ∨ b') -> m (a' ∨ b')
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return ((a' ∨ b') -> m (a' ∨ b')) -> (a' ∨ b') -> m (a' ∨ b')
forall a b. (a -> b) -> a -> b
$ b' -> a' ∨ b'
forall a b. b -> a ∨ b
Inr b'
y'

mapMInl ∷ (Monad m) ⇒ (a → m a') → a ∨ b → m (a' ∨ b)
mapMInl :: forall (m :: * -> *) a a' b.
Monad m =>
(a -> m a') -> (a ∨ b) -> m (a' ∨ b)
mapMInl = ((a -> m a') -> (b -> m b) -> (a ∨ b) -> m (a' ∨ b))
-> (b -> m b) -> (a -> m a') -> (a ∨ b) -> m (a' ∨ b)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> m a') -> (b -> m b) -> (a ∨ b) -> m (a' ∨ b)
forall (m :: * -> *) a a' b b'.
Monad m =>
(a -> m a') -> (b -> m b') -> (a ∨ b) -> m (a' ∨ b')
mapMChoice b -> m b
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return

mapMInr ∷ (Monad m) ⇒ (b → m b') → a ∨ b → m (a ∨ b')
mapMInr :: forall (m :: * -> *) b b' a.
Monad m =>
(b -> m b') -> (a ∨ b) -> m (a ∨ b')
mapMInr = (a -> m a) -> (b -> m b') -> (a ∨ b) -> m (a ∨ b')
forall (m :: * -> *) a a' b b'.
Monad m =>
(a -> m a') -> (b -> m b') -> (a ∨ b) -> m (a' ∨ b')
mapMChoice a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return