module Pandora.Paradigm.Primary.Functor.Predicate where

import Pandora.Core.Functor (type (~>), type (:=>))
import Pandora.Pattern.Category ((.), ($))
import Pandora.Pattern.Functor.Contravariant (Contravariant ((>$<)))
import Pandora.Pattern.Functor.Divisible (Divisible ((>*<)))
import Pandora.Pattern.Functor.Determinable (Determinable (determine))
import Pandora.Pattern.Functor.Pointable (Pointable (point))
import Pandora.Pattern.Functor.Avoidable (Avoidable (empty))
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.Primary.Functor.Function ((!))
import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (Primary, run, unite))

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 :: * -> * -> *). Category m => m ~~> m
$ b -> Boolean
g (b -> Boolean) -> (a -> b) -> a -> Boolean
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> b
f

instance Divisible Predicate where
	Predicate b -> Boolean
g >*< :: Predicate b -> Predicate c -> Predicate (b :*: c)
>*< Predicate c -> Boolean
h = ((b :*: c) -> Boolean) -> Predicate (b :*: c)
forall a. (a -> Boolean) -> Predicate a
Predicate (((b :*: c) -> Boolean) -> Predicate (b :*: c))
-> ((b :*: c) -> Boolean) -> Predicate (b :*: c)
forall (m :: * -> * -> *). Category m => m ~~> m
$ \(b
b :*: c
c) -> b -> Boolean
g b
b Boolean -> Boolean -> Boolean
forall a. Ringoid a => a -> a -> a
* c -> Boolean
h c
c

instance Determinable Predicate where
	determine :: Predicate a
determine = (a -> Boolean) -> Predicate a
forall a. (a -> Boolean) -> Predicate a
Predicate (Boolean
True Boolean -> a -> Boolean
forall a b. a -> b -> a
!)

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)

satisfy :: (Pointable t, Avoidable t) => Predicate a -> a -> t a
satisfy :: Predicate a -> a -> t a
satisfy Predicate a
p a
x = Predicate a -> a -> Boolean
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run Predicate a
p a
x Boolean -> t a -> t a -> t a
forall a. Boolean -> a -> a -> a
? a -> t a
forall (t :: * -> *) a. Pointable t => a :=> t
point a
x (t a -> t a) -> t a -> t a
forall (m :: * -> * -> *). Category m => m ~~> m
$ t a
forall (t :: * -> *) a. Avoidable t => t a
empty

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 :: * -> * -> *). Category m => m ~~> m
$ 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.
Category m =>
m b c -> m a b -> m a c
. a -> Boolean
p