module Pandora.Paradigm.Primary.Functor.Predicate where

import Pandora.Core.Functor (type (~>), type (:=>))
import Pandora.Core.Interpreted (Interpreted (Primary, run, unite))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category ((<--))
import Pandora.Pattern.Morphism.Straight (Straight (Straight))
import Pandora.Pattern.Functor.Contravariant (Contravariant ((>-|-)))
import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (mult))
import Pandora.Pattern.Functor.Monoidal (Monoidal (unit))
import Pandora.Pattern.Object.Setoid (Setoid ((==)))
import Pandora.Pattern.Object.Ringoid (Ringoid ((*)))
import Pandora.Paradigm.Primary.Object.Boolean (Boolean (True, False), bool)
import Pandora.Paradigm.Algebraic.Product ((:*:)((:*:)))
import Pandora.Paradigm.Algebraic.Sum ((:+:)(Option, Adoption))
import Pandora.Paradigm.Algebraic.Exponential (type (-->), type (<--))

newtype Predicate a = Predicate (a -> Boolean)

instance Interpreted (->) Predicate where
	type Primary Predicate a = a -> Boolean
	run :: ((->) < Predicate a) < Primary Predicate a
run ~(Predicate a -> Boolean
f) = Primary Predicate a
a -> Boolean
f
	unite :: ((->) < Primary Predicate a) < Predicate a
unite = ((->) < Primary Predicate a) < Predicate a
forall a. (a -> Boolean) -> Predicate a
Predicate

instance Contravariant (->) (->) Predicate where
	a -> b
f >-|- :: (a -> b) -> Predicate b -> Predicate a
>-|- Predicate b -> Boolean
g = (a -> Boolean) -> Predicate a
forall a. (a -> Boolean) -> Predicate a
Predicate ((a -> Boolean) -> Predicate a) -> (a -> Boolean) -> Predicate a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- b -> Boolean
g (b -> Boolean) -> (a -> b) -> a -> Boolean
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> b
f

instance Semimonoidal (-->) (:*:) (:*:) Predicate where
	mult :: (Predicate a :*: Predicate b) --> Predicate (a :*: b)
mult = ((Predicate a :*: Predicate b) -> Predicate (a :*: b))
-> (Predicate a :*: Predicate b) --> Predicate (a :*: b)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((Predicate a :*: Predicate b) -> Predicate (a :*: b))
 -> (Predicate a :*: Predicate b) --> Predicate (a :*: b))
-> ((Predicate a :*: Predicate b) -> Predicate (a :*: b))
-> (Predicate a :*: Predicate b) --> Predicate (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(Predicate a -> Boolean
f :*: Predicate b -> Boolean
g) -> ((a :*: b) -> Boolean) -> Predicate (a :*: b)
forall a. (a -> Boolean) -> Predicate a
Predicate (((a :*: b) -> Boolean) -> Predicate (a :*: b))
-> ((a :*: b) -> Boolean) -> Predicate (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(a
x :*: b
y) -> a -> Boolean
f a
x Boolean -> Boolean -> Boolean
forall a. Ringoid a => a -> a -> a
* b -> Boolean
g b
y

instance Monoidal (-->) (<--) (:*:) (:*:) Predicate where
	unit :: Proxy (:*:) -> (Unit (:*:) <-- a) --> Predicate a
unit Proxy (:*:)
_ = ((Unit (:*:) <-- a) -> Predicate a)
-> (Unit (:*:) <-- a) --> Predicate a
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((Unit (:*:) <-- a) -> Predicate a)
 -> (Unit (:*:) <-- a) --> Predicate a)
-> ((Unit (:*:) <-- a) -> Predicate a)
-> (Unit (:*:) <-- a) --> Predicate a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \Unit (:*:) <-- a
_ -> (a -> Boolean) -> Predicate a
forall a. (a -> Boolean) -> Predicate a
Predicate ((a -> Boolean) -> Predicate a) -> (a -> Boolean) -> Predicate a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \a
_ -> Boolean
True

instance Semimonoidal (-->) (:*:) (:+:) Predicate where
	mult :: (Predicate a :*: Predicate b) --> Predicate (a :+: b)
mult = ((Predicate a :*: Predicate b) -> Predicate (a :+: b))
-> (Predicate a :*: Predicate b) --> Predicate (a :+: b)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((Predicate a :*: Predicate b) -> Predicate (a :+: b))
 -> (Predicate a :*: Predicate b) --> Predicate (a :+: b))
-> ((Predicate a :*: Predicate b) -> Predicate (a :+: b))
-> (Predicate a :*: Predicate b) --> Predicate (a :+: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(Predicate a -> Boolean
f :*: Predicate b -> Boolean
g) -> ((a :+: b) -> Boolean) -> Predicate (a :+: b)
forall a. (a -> Boolean) -> Predicate a
Predicate (((a :+: b) -> Boolean) -> Predicate (a :+: b))
-> ((a :+: b) -> Boolean) -> Predicate (a :+: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \case
		Option a
x -> a -> Boolean
f a
x
		Adoption b
y -> b -> Boolean
g b
y

equate :: Setoid a => a :=> Predicate
equate :: a :=> Predicate
equate a
x = (a -> Boolean) -> Predicate a
forall a. (a -> Boolean) -> Predicate a
Predicate (a -> a -> Boolean
forall a. Setoid a => a -> a -> Boolean
== a
x)

not :: Predicate ~> Predicate
not :: Predicate a -> Predicate a
not (Predicate a -> Boolean
p) = (a -> Boolean) -> Predicate a
forall a. (a -> Boolean) -> Predicate a
Predicate ((a -> Boolean) -> Predicate a) -> (a -> Boolean) -> Predicate a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Boolean -> Boolean -> Boolean -> Boolean
forall a. a -> a -> Boolean -> a
bool Boolean
True Boolean
False (Boolean -> Boolean) -> (a -> Boolean) -> a -> Boolean
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> Boolean
p