module Plutarch.Extra.Profunctor (
  PProfunctor (..),
) where

import Data.Kind (Constraint)
import Plutarch.Extra.Function (pidentity)
import Plutarch.Extra.Functor (Plut)

-- | @since 1.0.0
class PProfunctor (p :: (S -> Type) -> (S -> Type) -> S -> Type) where
  {-# MINIMAL pdimap | plmap, prmap #-}
  type PContraSubcategory p :: (S -> Type) -> Constraint
  type PCoSubcategory p :: (S -> Type) -> Constraint
  pdimap ::
    forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (d :: S -> Type) (s :: S).
    ( PContraSubcategory p a
    , PContraSubcategory p b
    , PCoSubcategory p c
    , PCoSubcategory p d
    ) =>
    Term s ((a :--> b) :--> (c :--> d) :--> p b c :--> p a d)
  pdimap = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (a :--> b)
f Term s (c :--> d)
g Term s (p b c)
p -> forall (p :: (S -> Type) -> (S -> Type) -> S -> Type)
       (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (s :: S).
(PProfunctor p, PContraSubcategory p a, PContraSubcategory p b,
 PCoSubcategory p c) =>
Term s ((a :--> b) :--> (p b c :--> p a c))
plmap forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (a :--> b)
f forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (p :: (S -> Type) -> (S -> Type) -> S -> Type)
       (a :: S -> Type) (c :: S -> Type) (d :: S -> Type) (s :: S).
(PProfunctor p, PContraSubcategory p a, PCoSubcategory p c,
 PCoSubcategory p d) =>
Term s ((c :--> d) :--> (p a c :--> p a d))
prmap forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (c :--> d)
g forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (p b c)
p)
  plmap ::
    forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (s :: S).
    ( PContraSubcategory p a
    , PContraSubcategory p b
    , PCoSubcategory p c
    ) =>
    Term s ((a :--> b) :--> p b c :--> p a c)
  plmap = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (a :--> b)
f Term s (p b c)
p -> forall (p :: (S -> Type) -> (S -> Type) -> S -> Type)
       (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (d :: S -> Type)
       (s :: S).
(PProfunctor p, PContraSubcategory p a, PContraSubcategory p b,
 PCoSubcategory p c, PCoSubcategory p d) =>
Term s ((a :--> b) :--> ((c :--> d) :--> (p b c :--> p a d)))
pdimap forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (a :--> b)
f forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S). Term s (a :--> a)
pidentity forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (p b c)
p
  prmap ::
    forall (a :: S -> Type) (c :: S -> Type) (d :: S -> Type) (s :: S).
    ( PContraSubcategory p a
    , PCoSubcategory p c
    , PCoSubcategory p d
    ) =>
    Term s ((c :--> d) :--> p a c :--> p a d)
  prmap = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (c :--> d)
g Term s (p a c)
p -> forall (p :: (S -> Type) -> (S -> Type) -> S -> Type)
       (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (d :: S -> Type)
       (s :: S).
(PProfunctor p, PContraSubcategory p a, PContraSubcategory p b,
 PCoSubcategory p c, PCoSubcategory p d) =>
Term s ((a :--> b) :--> ((c :--> d) :--> (p b c :--> p a d)))
pdimap forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S). Term s (a :--> a)
pidentity forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (c :--> d)
g forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (p a c)
p

-- | @since 3.1.0
instance PProfunctor (:-->) where
  type PContraSubcategory (:-->) = Plut
  type PCoSubcategory (:-->) = Plut
  pdimap :: forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type)
       (d :: S -> Type) (s :: S).
(PContraSubcategory (:-->) a, PContraSubcategory (:-->) b,
 PCoSubcategory (:-->) c, PCoSubcategory (:-->) d) =>
Term
  s ((a :--> b) :--> ((c :--> d) :--> ((b :--> c) :--> (a :--> d))))
pdimap = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (a :--> b)
ab Term s (c :--> d)
cd Term s (b :--> c)
bc -> forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s a
x -> Term s (c :--> d)
cd forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (b :--> c)
bc forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (a :--> b)
ab forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x))