{-# OPTIONS_GHC -fno-warn-orphans #-}
module Pandora.Paradigm.Primary (module Exports, Simplification) where

import Pandora.Paradigm.Primary.Linear as Exports
import Pandora.Paradigm.Primary.Transformer as Exports
import Pandora.Paradigm.Primary.Functor as Exports
import Pandora.Paradigm.Primary.Object as Exports

import Pandora.Pattern.Morphism.Flip (Flip (Flip))
import Pandora.Core.Functor (type (:.), type (>))
import Pandora.Pattern.Semigroupoid (Semigroupoid ((.)))
import Pandora.Pattern.Category ((<---))
import Pandora.Pattern.Functor.Adjoint (Adjoint ((|-), (-|)))
import Pandora.Paradigm.Algebraic.Product ((:*:) ((:*:)))
import Pandora.Paradigm.Schemes (TU, T_U, UT, TUT)

instance Adjoint (->) (->) (Flip (:*:) s) ((->) s) where
	Flip (:*:) s a -> b
f -| :: (Flip (:*:) s a -> b) -> a -> s -> b
-| a
x = \s
s -> Flip (:*:) s a -> b
f (Flip (:*:) s a -> b)
-> ((a :*: s) -> Flip (:*:) s a) -> (a :*: s) -> b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a :*: s) -> Flip (:*:) s a
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip ((a :*: s) -> b) -> (a :*: s) -> b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- a
x a -> s -> a :*: s
forall s a. s -> a -> s :*: a
:*: s
s
	a -> s -> b
f |- :: (a -> s -> b) -> Flip (:*:) s a -> b
|- Flip (a
x :*: s
s) = a -> s -> b
f a
x s
s

type family Simplification (t :: * -> *) (a :: *) where
	Simplification Exactly a = a
	Simplification (TU _ _ t u) a = t :. u > a
	Simplification (UT _ _ t u) a = u :. t > a
	Simplification (TUT _ _ _ t t' u) a = t :. u :. t' > a
	Simplification (T_U _ _ p t u) a = p (t a) (u a)
	Simplification t a = t a