module Pandora.Paradigm.Primary.Functor.Conclusion where

import Pandora.Core.Functor (type (~>))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Morphism.Straight (Straight (Straight))
import Pandora.Pattern.Category (identity, ($), (#))
import Pandora.Pattern.Functor.Covariant (Covariant ((<$>)))
import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (mult))
import Pandora.Pattern.Functor.Monoidal (Monoidal (unit))
import Pandora.Pattern.Functor.Traversable (Traversable ((<<-)))
import Pandora.Pattern.Functor.Bindable (Bindable ((=<<)))
import Pandora.Pattern.Functor.Monad (Monad)
import Pandora.Pattern.Functor.Bivariant (Bivariant ((<->)))
import Pandora.Pattern.Object.Setoid (Setoid ((==)))
import Pandora.Pattern.Object.Chain (Chain ((<=>)))
import Pandora.Pattern.Object.Semigroup (Semigroup ((+)))
import Pandora.Paradigm.Primary.Object.Boolean (Boolean (False))
import Pandora.Paradigm.Primary.Object.Ordering (Ordering (Less, Greater))
import Pandora.Paradigm.Primary.Algebraic.Product ((:*:) ((:*:)))
import Pandora.Paradigm.Primary.Algebraic.Sum ((:+:) (Option, Adoption))
import Pandora.Pattern.Morphism.Flip (Flip (Flip))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (Schematic, Interpreted (Primary, run, unite))
import Pandora.Paradigm.Controlflow.Effect.Transformer.Monadic (Monadic (wrap), (:>) (TM))
import Pandora.Paradigm.Controlflow.Effect.Adaptable (Adaptable (adapt))
import Pandora.Paradigm.Schemes.UT (UT (UT), type (<.:>))
import Pandora.Paradigm.Primary.Algebraic.Exponential (type (-->))
import Pandora.Paradigm.Primary.Algebraic.One (One (One))
import Pandora.Paradigm.Primary.Algebraic (point)

data Conclusion e a = Failure e | Success a

instance Covariant (->) (->) (Conclusion e) where
	a -> b
f <$> :: (a -> b) -> Conclusion e a -> Conclusion e b
<$> Success a
x = b -> Conclusion e b
forall e a. a -> Conclusion e a
Success (b -> Conclusion e b) -> b -> Conclusion e b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a -> b
f a
x
	a -> b
_ <$> Failure e
y = e -> Conclusion e b
forall e a. e -> Conclusion e a
Failure e
y

instance Covariant (->) (->) (Flip Conclusion e) where
	a -> b
_ <$> :: (a -> b) -> Flip Conclusion e a -> Flip Conclusion e b
<$> Flip (Success e
x) = Conclusion b e -> Flip Conclusion e b
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (Conclusion b e -> Flip Conclusion e b)
-> Conclusion b e -> Flip Conclusion e b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ e -> Conclusion b e
forall e a. a -> Conclusion e a
Success e
x
	a -> b
f <$> Flip (Failure a
y) = Conclusion b e -> Flip Conclusion e b
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (Conclusion b e -> Flip Conclusion e b)
-> (b -> Conclusion b e) -> b -> Flip Conclusion e b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. b -> Conclusion b e
forall e a. e -> Conclusion e a
Failure (b -> Flip Conclusion e b) -> b -> Flip Conclusion e b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a -> b
f a
y

instance Semimonoidal (-->) (:*:) (:*:) (Conclusion e) where
	mult :: (Conclusion e a :*: Conclusion e b) --> Conclusion e (a :*: b)
mult = ((Conclusion e a :*: Conclusion e b) -> Conclusion e (a :*: b))
-> (Conclusion e a :*: Conclusion e b) --> Conclusion e (a :*: b)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((Conclusion e a :*: Conclusion e b) -> Conclusion e (a :*: b))
 -> (Conclusion e a :*: Conclusion e b) --> Conclusion e (a :*: b))
-> ((Conclusion e a :*: Conclusion e b) -> Conclusion e (a :*: b))
-> (Conclusion e a :*: Conclusion e b) --> Conclusion e (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \case
		Success a
x :*: Success b
y -> (a :*: b) -> Conclusion e (a :*: b)
forall e a. a -> Conclusion e a
Success ((a :*: b) -> Conclusion e (a :*: b))
-> (a :*: b) -> Conclusion e (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a
x a -> b -> a :*: b
forall s a. s -> a -> s :*: a
:*: b
y
		Failure e
x :*: Conclusion e b
_ -> e -> Conclusion e (a :*: b)
forall e a. e -> Conclusion e a
Failure e
x
		Conclusion e a
_ :*: Failure e
x -> e -> Conclusion e (a :*: b)
forall e a. e -> Conclusion e a
Failure e
x

instance Monoidal (-->) (->) (:*:) (:*:) (Conclusion e) where
	unit :: Proxy (:*:) -> (Unit (:*:) -> a) --> Conclusion e a
unit Proxy (:*:)
_ = ((One -> a) -> Conclusion e a)
-> Straight (->) (One -> a) (Conclusion e a)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((One -> a) -> Conclusion e a)
 -> Straight (->) (One -> a) (Conclusion e a))
-> ((One -> a) -> Conclusion e a)
-> Straight (->) (One -> a) (Conclusion e a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a -> Conclusion e a
forall e a. a -> Conclusion e a
Success (a -> Conclusion e a)
-> ((One -> a) -> a) -> (One -> a) -> Conclusion e a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((One -> a) -> One -> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ One
One)

instance Semigroup e => Semimonoidal (-->) (:*:) (:+:) (Conclusion e) where
	mult :: (Conclusion e a :*: Conclusion e b) --> Conclusion e (a :+: b)
mult = ((Conclusion e a :*: Conclusion e b) -> Conclusion e (a :+: b))
-> (Conclusion e a :*: Conclusion e b) --> Conclusion e (a :+: b)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((Conclusion e a :*: Conclusion e b) -> Conclusion e (a :+: b))
 -> (Conclusion e a :*: Conclusion e b) --> Conclusion e (a :+: b))
-> ((Conclusion e a :*: Conclusion e b) -> Conclusion e (a :+: b))
-> (Conclusion e a :*: Conclusion e b) --> Conclusion e (a :+: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \case
		Failure e
_ :*: Conclusion e b
x -> b -> a :+: b
forall s a. a -> s :+: a
Adoption (b -> a :+: b) -> Conclusion e b -> Conclusion e (a :+: b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<$> Conclusion e b
x
		Success a
x :*: Conclusion e b
_ -> a -> a :+: b
forall s a. s -> s :+: a
Option (a -> a :+: b) -> Conclusion e a -> Conclusion e (a :+: b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<$> a -> Conclusion e a
forall e a. a -> Conclusion e a
Success a
x

instance Traversable (->) (->) (Conclusion e) where
	(<<-) :: (Covariant (->) (->) u, Monoidal (-->) (->) (:*:) (:*:) u, Semimonoidal (-->) (:*:) (:*:) u)
		 => (a -> u b) -> Conclusion e a -> u (Conclusion e b)
	a -> u b
_ <<- :: (a -> u b) -> Conclusion e a -> u (Conclusion e b)
<<- Failure e
y = Conclusion e b -> u (Conclusion e b)
forall (t :: * -> *) a. Pointable t => a -> t a
point (Conclusion e b -> u (Conclusion e b))
-> Conclusion e b -> u (Conclusion e b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ e -> Conclusion e b
forall e a. e -> Conclusion e a
Failure e
y
	a -> u b
f <<- Success a
x = b -> Conclusion e b
forall e a. a -> Conclusion e a
Success (b -> Conclusion e b) -> u b -> u (Conclusion e b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<$> a -> u b
f a
x

instance Bindable (->) (Conclusion e) where
	a -> Conclusion e b
f =<< :: (a -> Conclusion e b) -> Conclusion e a -> Conclusion e b
=<< Success a
x = a -> Conclusion e b
f a
x
	a -> Conclusion e b
_ =<< Failure e
y = e -> Conclusion e b
forall e a. e -> Conclusion e a
Failure e
y

--instance Monad (Conclusion e) where

instance Bivariant (->) (->) (->) Conclusion where
	a -> b
f <-> :: (a -> b) -> (c -> d) -> Conclusion a c -> Conclusion b d
<-> c -> d
g = (a -> Conclusion b d)
-> (c -> Conclusion b d) -> Conclusion a c -> Conclusion b d
forall e r a. (e -> r) -> (a -> r) -> Conclusion e a -> r
conclusion ((a -> Conclusion b d)
 -> (c -> Conclusion b d) -> Conclusion a c -> Conclusion b d)
-> (a -> Conclusion b d)
-> (c -> Conclusion b d)
-> Conclusion a c
-> Conclusion b d
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# b -> Conclusion b d
forall e a. e -> Conclusion e a
Failure (b -> Conclusion b d) -> (a -> b) -> a -> Conclusion b d
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> b
f ((c -> Conclusion b d) -> Conclusion a c -> Conclusion b d)
-> (c -> Conclusion b d) -> Conclusion a c -> Conclusion b d
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# d -> Conclusion b d
forall e a. a -> Conclusion e a
Success (d -> Conclusion b d) -> (c -> d) -> c -> Conclusion b d
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. c -> d
g

instance (Setoid e, Setoid a) => Setoid (Conclusion e a) where
	Success a
x == :: Conclusion e a -> Conclusion e a -> Boolean
== Success a
y = a
x a -> a -> Boolean
forall a. Setoid a => a -> a -> Boolean
== a
y
	Failure e
x == Failure e
y = e
x e -> e -> Boolean
forall a. Setoid a => a -> a -> Boolean
== e
y
	Conclusion e a
_ == Conclusion e a
_ = Boolean
False

instance (Chain e, Chain a) => Chain (Conclusion e a) where
	Success a
x <=> :: Conclusion e a -> Conclusion e a -> Ordering
<=> Success a
y = a
x a -> a -> Ordering
forall a. Chain a => a -> a -> Ordering
<=> a
y
	Failure e
x <=> Failure e
y = e
x e -> e -> Ordering
forall a. Chain a => a -> a -> Ordering
<=> e
y
	Failure e
_ <=> Success a
_ = Ordering
Less
	Success a
_ <=> Failure e
_ = Ordering
Greater

instance (Semigroup e, Semigroup a) => Semigroup (Conclusion e a) where
	Success a
x + :: Conclusion e a -> Conclusion e a -> Conclusion e a
+ Success a
y = a -> Conclusion e a
forall e a. a -> Conclusion e a
Success (a -> Conclusion e a) -> a -> Conclusion e a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a
x a -> a -> a
forall a. Semigroup a => a -> a -> a
+ a
y
	Failure e
x + Failure e
y = e -> Conclusion e a
forall e a. e -> Conclusion e a
Failure (e -> Conclusion e a) -> e -> Conclusion e a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ e
x e -> e -> e
forall a. Semigroup a => a -> a -> a
+ e
y
	Failure e
_ + Success a
y = a -> Conclusion e a
forall e a. a -> Conclusion e a
Success a
y
	Success a
x + Failure e
_ = a -> Conclusion e a
forall e a. a -> Conclusion e a
Success a
x

conclusion :: (e -> r) -> (a -> r) -> Conclusion e a -> r
conclusion :: (e -> r) -> (a -> r) -> Conclusion e a -> r
conclusion e -> r
f a -> r
_ (Failure e
x) = e -> r
f e
x
conclusion e -> r
_ a -> r
s (Success a
x) = a -> r
s a
x

fail :: (e -> r) -> Conclusion e ~> Conclusion r
fail :: (e -> r) -> Conclusion e ~> Conclusion r
fail e -> r
f (Failure e
x) = r -> Conclusion r a
forall e a. e -> Conclusion e a
Failure (r -> Conclusion r a) -> r -> Conclusion r a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ e -> r
f e
x
fail e -> r
_ (Success a
y) = a -> Conclusion r a
forall e a. a -> Conclusion e a
Success a
y

instance Interpreted (->) (Conclusion e) where
	type Primary (Conclusion e) a = Conclusion e a
	run :: Conclusion e a -> Primary (Conclusion e) a
run = Conclusion e a -> Primary (Conclusion e) a
forall (m :: * -> * -> *) a. Category m => m a a
identity
	unite :: Primary (Conclusion e) a -> Conclusion e a
unite = Primary (Conclusion e) a -> Conclusion e a
forall (m :: * -> * -> *) a. Category m => m a a
identity

type instance Schematic Monad (Conclusion e) = (<.:>) (Conclusion e)

instance Monadic (Conclusion e) where
	wrap :: Conclusion e ~> (Conclusion e :> u)
wrap = (<.:>) (Conclusion e) u a -> (:>) (Conclusion e) u a
forall (t :: * -> *) (u :: * -> *) a.
Schematic Monad t u a -> (:>) t u a
TM ((<.:>) (Conclusion e) u a -> (:>) (Conclusion e) u a)
-> (Conclusion e a -> (<.:>) (Conclusion e) u a)
-> Conclusion e a
-> (:>) (Conclusion e) u a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((u :. Conclusion e) := a) -> (<.:>) (Conclusion e) u a
forall k k k k (ct :: k) (cu :: k) (t :: k -> k) (u :: k -> *)
       (a :: k).
((u :. t) := a) -> UT ct cu t u a
UT (((u :. Conclusion e) := a) -> (<.:>) (Conclusion e) u a)
-> (Conclusion e a -> (u :. Conclusion e) := a)
-> Conclusion e a
-> (<.:>) (Conclusion e) u a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Conclusion e a -> (u :. Conclusion e) := a
forall (t :: * -> *) a. Pointable t => a -> t a
point

type Failable e = Adaptable (Conclusion e)

failure :: Failable e t => e -> t a
failure :: e -> t a
failure = Conclusion e a -> t a
forall k (t :: k -> *) (u :: k -> *). Adaptable t u => t ~> u
adapt (Conclusion e a -> t a) -> (e -> Conclusion e a) -> e -> t a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. e -> Conclusion e a
forall e a. e -> Conclusion e a
Failure

class Catchable e t where
	catch :: t a -> (e -> t a) -> t a

instance Catchable e (Conclusion e) where
	catch :: Conclusion e a -> (e -> Conclusion e a) -> Conclusion e a
catch (Failure e
e) e -> Conclusion e a
handle = e -> Conclusion e a
handle e
e
	catch (Success a
x) e -> Conclusion e a
_ = a -> Conclusion e a
forall e a. a -> Conclusion e a
Success a
x

instance (Monoidal (-->) (->) (:*:) (:*:) u, Bindable (->) u) => Catchable e (Conclusion e <.:> u) where
	catch :: (<.:>) (Conclusion e) u a
-> (e -> (<.:>) (Conclusion e) u a) -> (<.:>) (Conclusion e) u a
catch (UT (u :. Conclusion e) := a
x) e -> (<.:>) (Conclusion e) u a
handle = let conclude :: Conclusion e a -> (u :. Conclusion e) := a
conclude = (e -> (u :. Conclusion e) := a)
-> (a -> (u :. Conclusion e) := a)
-> Conclusion e a
-> (u :. Conclusion e) := a
forall e r a. (e -> r) -> (a -> r) -> Conclusion e a -> r
conclusion ((e -> (u :. Conclusion e) := a)
 -> (a -> (u :. Conclusion e) := a)
 -> Conclusion e a
 -> (u :. Conclusion e) := a)
-> (e -> (u :. Conclusion e) := a)
-> (a -> (u :. Conclusion e) := a)
-> Conclusion e a
-> (u :. Conclusion e) := a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<.:>) (Conclusion e) u a -> (u :. Conclusion e) := a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run ((<.:>) (Conclusion e) u a -> (u :. Conclusion e) := a)
-> (e -> (<.:>) (Conclusion e) u a)
-> e
-> (u :. Conclusion e) := a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. e -> (<.:>) (Conclusion e) u a
handle ((a -> (u :. Conclusion e) := a)
 -> Conclusion e a -> (u :. Conclusion e) := a)
-> (a -> (u :. Conclusion e) := a)
-> Conclusion e a
-> (u :. Conclusion e) := a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Conclusion e a -> (u :. Conclusion e) := a
forall (t :: * -> *) a. Pointable t => a -> t a
point (Conclusion e a -> (u :. Conclusion e) := a)
-> (a -> Conclusion e a) -> a -> (u :. Conclusion e) := a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> Conclusion e a
forall e a. a -> Conclusion e a
Success
		in ((u :. Conclusion e) := a) -> (<.:>) (Conclusion e) u a
forall k k k k (ct :: k) (cu :: k) (t :: k -> k) (u :: k -> *)
       (a :: k).
((u :. t) := a) -> UT ct cu t u a
UT (((u :. Conclusion e) := a) -> (<.:>) (Conclusion e) u a)
-> ((u :. Conclusion e) := a) -> (<.:>) (Conclusion e) u a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Conclusion e a -> (u :. Conclusion e) := a
conclude (Conclusion e a -> (u :. Conclusion e) := a)
-> ((u :. Conclusion e) := a) -> (u :. Conclusion e) := a
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
=<< (u :. Conclusion e) := a
x