{-# LANGUAGE AllowAmbiguousTypes #-}

-- | The __prism__: the optic for the coproduct, with legs
--
-- > Prism s t a b = (b ~> t, s ~> (t || a))
--
-- witnessed by @'Rep'@\/@'Corep'@ @('Coproduct' t)@ ('PrismFl' \/ 'matchingP'). A prism reviews
-- and matches, sitting below 'Proarrow.Optic.Getter.Review',
-- 'Proarrow.Optic.AffineTraversal.AffineTraversal' and
-- 'Proarrow.Optic.MonoidalTraversal.MonoidalTraversal' in the lattice. Build with 'prism',
-- eliminate to the two legs with 'withPrism' via the generic 'ExOptic' carrier.
-- 'toOpLens'\/'fromOpLens' witness the equivalence with the op-lens encoding. This module also
-- hosts 'affineTraversal', the lens-then-prism builder for affine traversals.
module Proarrow.Optic.Prism where

import Proarrow.Category.Instance.Opposite (Op (..))
import Proarrow.Category.Monoidal.CopyDiscard (CopyDiscard (..))
import Proarrow.Colimit.BinaryCoproduct (Coproduct, HasBinaryCoproducts (..), HasCoproducts, left)
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), (\\), type (+->))
import Proarrow.Object (pattern Objs)
import Proarrow.Optic
  ( ExOptic
  , FLAVOR
  , OpConstraint
  , Optic
  , Prostrong (..)
  , convert
  , legs2prof
  , opOptic
  , unOpOptic
  , withLegs
  , (%)
  )
import Proarrow.Optic.AffineTraversal (AffineTravFl (..), AffineTraversal)
import Proarrow.Optic.Getter (GetterFl (..))
import Proarrow.Optic.Lens (Lens, LensFl, lens, withLens)
import Proarrow.Optic.Traversal (MonTravFl)
import Proarrow.Profunctor.Corepresentable (Corep (..))
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Identity (Id (..))
import Proarrow.Profunctor.Representable (Rep (..))

-- | The prism flavor. The @'GetterFl' q p@ superclass says a reversed prism views its build leg
-- ('getP' on the swapped pair): @'Proarrow.Optic.re' prism@ is a getter.
type PrismFl :: forall {k}. FLAVOR k k
class (AffineTravFl p q, GetterFl q p, MonTravFl p q) => PrismFl (p :: k +-> k) (q :: k +-> k) where
  -- | Like 'affineMatch', but asking only for binary coproducts. Prism witnesses never need more,
  -- so prisms stay usable in categories without products.
  matchingP :: (HasBinaryCoproducts k) => p (s :: k) a -> q (b :: k) t -> s ~> (t || a)

instance (CopyDiscard k, HasCoproducts k, Ob t) => PrismFl (Rep (Coproduct t) :: k +-> k) (Corep (Coproduct t)) where
  matchingP :: forall (s :: k) (a :: k) (b :: k) (t :: k).
HasBinaryCoproducts k =>
Rep (Coproduct t) s a -> Corep (Coproduct t) b t -> s ~> (t || a)
matchingP @_ @a @b (Rep s ~> (Coproduct t @ a)
p) (Corep (Coproduct t @ b) ~> t
q) = forall (c :: k) (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob c) =>
(a ~> b) -> (a || c) ~> (b || c)
forall {k} (c :: k) (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob c) =>
(a ~> b) -> (a || c) ~> (b || c)
left @a ((Coproduct t @ b) ~> t
(t || b) ~> t
q ((t || b) ~> t) -> (t ~> (t || b)) -> t ~> t
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @t @b) ((t || a) ~> (t || a)) -> (s ~> (t || a)) -> s ~> (t || a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> (Coproduct t @ a)
s ~> (t || a)
p
instance (CategoryOf k) => PrismFl (Id :: k +-> k) Id where
  matchingP :: forall (s :: k) (a :: k) (b :: k) (t :: k).
HasBinaryCoproducts k =>
Id s a -> Id b t -> s ~> (t || a)
matchingP @_ @a @_ @t (Id s ~> a
sa) Id b t
bt = forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @t @a (a ~> (t || a)) -> (s ~> a) -> s ~> (t || a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> a
sa ((Ob s, Ob a) => s ~> (t || a)) -> (s ~> a) -> s ~> (t || a)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ s ~> a
sa ((Ob b, Ob t) => s ~> (t || a)) -> Id b t -> s ~> (t || a)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> Id a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Id b t
bt
instance (PrismFl f g, PrismFl f' g') => PrismFl (f :.: f') (g' :.: g) where
  matchingP :: forall (s :: i) (a :: i) (b :: i) (t :: i).
HasBinaryCoproducts i =>
(:.:) f f' s a -> (:.:) g' g b t -> s ~> (t || a)
matchingP @_ @a @_ @t (f s b
f :.: f' :: f' b a
f'@f' b a
Objs) (g' b b
g' :.: g :: g b t
g@g b t
Objs) =
    (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @_ @t @a (t ~> (t || a)) -> (b ~> (t || a)) -> (t || b) ~> (t || a)
forall (x :: i) (a :: i) (y :: i).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| (forall (c :: i) (a :: i) (b :: i).
(HasBinaryCoproducts i, Ob c) =>
(a ~> b) -> (a || c) ~> (b || c)
forall {k} (c :: k) (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob c) =>
(a ~> b) -> (a || c) ~> (b || c)
left @a (forall {j} {k} (p :: k +-> k) (q :: j +-> j) (s :: k) (a :: k).
GetterFl p q =>
p s a -> s ~> a
forall (p :: i +-> i) (q :: i +-> i) (s :: i) (a :: i).
GetterFl p q =>
p s a -> s ~> a
getP @g @f g b t
g) ((b || a) ~> (t || a)) -> (b ~> (b || a)) -> b ~> (t || a)
forall (b :: i) (c :: i) (a :: i). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
(PrismFl p q, HasBinaryCoproducts k) =>
p s a -> q b t -> s ~> (t || a)
forall (p :: i +-> i) (q :: i +-> i) (s :: i) (a :: i) (b :: i)
       (t :: i).
(PrismFl p q, HasBinaryCoproducts i) =>
p s a -> q b t -> s ~> (t || a)
matchingP @f' @g' f' b a
f' g' b b
g')) ((t || b) ~> (t || a)) -> (s ~> (t || b)) -> s ~> (t || a)
forall (b :: i) (c :: i) (a :: i). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
(PrismFl p q, HasBinaryCoproducts k) =>
p s a -> q b t -> s ~> (t || a)
forall (p :: i +-> i) (q :: i +-> i) (s :: i) (a :: i) (b :: i)
       (t :: i).
(PrismFl p q, HasBinaryCoproducts i) =>
p s a -> q b t -> s ~> (t || a)
matchingP @f @g f s b
f g b t
g

type Prism (s :: k) t a b = Optic (Prostrong PrismFl) s t a b
type Prism' s a = Prism s s a a
prism
  :: forall {k} (s :: k) (t :: k) a b
   . (CopyDiscard k, HasCoproducts k, Ob a) => (b ~> t) -> (s ~> (t || a)) -> Prism s t a b
prism :: forall {k} (s :: k) (t :: k) (a :: k) (b :: k).
(CopyDiscard k, HasCoproducts k, Ob a) =>
(b ~> t) -> (s ~> (t || a)) -> Prism s t a b
prism b ~> t
bt s ~> (t || a)
sta =
  forall {j} {k} (w :: FLAVOR j k) (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
forall (w :: FLAVOR k k) (p :: k +-> k) (q :: k +-> k) (s :: k)
       (t :: k) (a :: k) (b :: k).
(CategoryOf k, CategoryOf k, w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
legs2prof @PrismFl (forall (b :: k) (f :: k +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep @a @(Coproduct t) s ~> (Coproduct t @ a)
s ~> (t || a)
sta) (forall (a :: k) (f :: k +-> k) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
forall {j} {k} (a :: j) (f :: j +-> k) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
Corep @b @(Coproduct t) (t ~> t
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id (t ~> t) -> (b ~> t) -> (t || b) ~> t
forall (x :: k) (a :: k) (y :: k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| b ~> t
bt)) ((Ob b, Ob t) => Optic (Prostrong PrismFl) s t a b)
-> (b ~> t) -> Optic (Prostrong PrismFl) s t a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ b ~> t
bt

-- | Build an 'AffineTraversal' by composing a 'Lens' with a 'Prism': focus a field with the lens,
-- then match a case of that field with the prism. There is no from-legs builder for a bare affine
-- traversal (its witness only ever arises by composition), so this is the way to make one. It is
-- @'convert' (l '%' p)@.
affineTraversal
  :: forall {k} (s :: k) t x y a b. (CategoryOf k) => Lens s t x y -> Prism x y a b -> AffineTraversal s t a b
affineTraversal :: forall {k} (s :: k) (t :: k) (x :: k) (y :: k) (a :: k) (b :: k).
CategoryOf k =>
Lens s t x y -> Prism x y a b -> AffineTraversal s t a b
affineTraversal Lens s t x y
l Prism x y a b
p = Optic (Prostrong LensFl :&&: Prostrong PrismFl) s t a b
-> Optic (Prostrong AffineTravFl) s t a b
forall {j} {k} (c :: (k -> j -> Type) -> Constraint)
       (w :: FLAVOR j k) (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b -> Optic (Prostrong w) s t a b
convert (Lens s t x y
l Lens s t x y
-> Prism x y a b
-> Optic (Prostrong LensFl :&&: Prostrong PrismFl) s t a b
forall {j} {k} (c1 :: (j +-> k) -> Constraint) (s :: k) (t :: j)
       (a :: k) (b :: j) (c2 :: (j +-> k) -> Constraint) (c :: k)
       (d :: j).
Optic c1 s t a b -> Optic c2 a b c d -> Optic (c1 :&&: c2) s t c d
% Prism x y a b
p)

-- | Eliminate any optic that is at least an iso and at most a prism to its two legs, in either
-- encoding: run it at its witness pair ('ExOptic' 'PrismFl', via 'withLegs') and read the legs off
-- with 'matchingP' and 'getP' on the flipped pair (a prism's build leg is a getter read backwards).
withPrism
  :: forall {k} c (s :: k) (t :: k) a b r
   . (HasBinaryCoproducts k, (Ob a, Ob b) => c (ExOptic PrismFl a b))
  => Optic c s t a b -> ((b ~> t) -> (s ~> (t || a)) -> r) -> r
withPrism :: forall {k} (c :: (k -> k -> Type) -> Constraint) (s :: k) (t :: k)
       (a :: k) (b :: k) r.
(HasBinaryCoproducts k, (Ob a, Ob b) => c (ExOptic PrismFl a b)) =>
Optic c s t a b -> ((b ~> t) -> (s ~> (t || a)) -> r) -> r
withPrism Optic c s t a b
o (b ~> t) -> (s ~> (t || a)) -> r
k = forall {j} {k} (w :: FLAVOR j k)
       (c :: (k -> j -> Type) -> Constraint) (s :: k) (t :: j) (a :: k)
       (b :: j) r.
(CategoryOf j, CategoryOf k, Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b
-> (forall (p :: k +-> k) (q :: j +-> j).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
forall (w :: FLAVOR k k) (c :: (k +-> k) -> Constraint) (s :: k)
       (t :: k) (a :: k) (b :: k) r.
(CategoryOf k, CategoryOf k, Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b
-> (forall (p :: k +-> k) (q :: k +-> k).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
withLegs @PrismFl Optic c s t a b
o \ @p @q p s a
p q b t
q -> (b ~> t) -> (s ~> (t || a)) -> r
k (forall {j} {k} (p :: k +-> k) (q :: j +-> j) (s :: k) (a :: k).
GetterFl p q =>
p s a -> s ~> a
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k).
GetterFl p q =>
p s a -> s ~> a
getP @q @p q b t
q) (forall {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
(PrismFl p q, HasBinaryCoproducts k) =>
p s a -> q b t -> s ~> (t || a)
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
(PrismFl p q, HasBinaryCoproducts k) =>
p s a -> q b t -> s ~> (t || a)
matchingP @p @q p s a
p q b t
q)

-- | A 'Prism' and its op-lens encoding ('Proarrow.Optic.Lens.Prism', a 'Proarrow.Optic.Lens.Lens'
-- over the opposite category) carry the same data, the two legs @(b '~>' t, s '~>' t '||' a)@,
-- so they are equivalent. 'toOpLens' eliminates a 'PrismFl' prism to its legs (via 'withPrism') and
-- rebuilds the op-lens; 'fromOpLens' eliminates the op-lens (via 'Proarrow.Optic.Lens.withLens' on
-- 'opOptic', i.e. as a lens over 'Proarrow.Category.Instance.Opposite.OPPOSITE') and rebuilds the 'PrismFl' prism.

-- | The __op-lens__ encoding of a prism: a 'Proarrow.Optic.Lens.Lens' over the opposite category.
type OpLens (s :: k) t a b = Optic (OpConstraint (Prostrong LensFl)) s t a b

toOpLens :: forall {k} (s :: k) t a b. (HasCoproducts k, Ob a, Ob b) => Prism s t a b -> OpLens s t a b
toOpLens :: forall {k} (s :: k) (t :: k) (a :: k) (b :: k).
(HasCoproducts k, Ob a, Ob b) =>
Prism s t a b -> OpLens s t a b
toOpLens Prism s t a b
o = Prism s t a b
-> ((b ~> t) -> (s ~> (t || a)) -> OpLens s t a b)
-> OpLens s t a b
forall {k} (c :: (k -> k -> Type) -> Constraint) (s :: k) (t :: k)
       (a :: k) (b :: k) r.
(HasBinaryCoproducts k, (Ob a, Ob b) => c (ExOptic PrismFl a b)) =>
Optic c s t a b -> ((b ~> t) -> (s ~> (t || a)) -> r) -> r
withPrism Prism s t a b
o (\b ~> t
bt s ~> (t || a)
sta -> Optic (Prostrong LensFl) (OP t) (OP s) (OP b) (OP a)
-> OpLens s t a b
forall {j} {k} (c :: (OPPOSITE k +-> OPPOSITE j) -> Constraint)
       (s :: k) (t :: j) (a :: k) (b :: j).
Optic c (OP t) (OP s) (OP b) (OP a)
-> Optic (OpConstraint c) s t a b
unOpOptic ((OP t ~> OP b)
-> ((OP t && OP a) ~> OP s)
-> Optic (Prostrong LensFl) (OP t) (OP s) (OP b) (OP a)
forall {k} (s :: k) (t :: k) (a :: k) (b :: k).
(HasBinaryProducts k, Ob b) =>
(s ~> a) -> ((s && b) ~> t) -> Lens s t a b
lens ((b ~> t) -> Op (~>) (OP t) (OP b)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p (OP a1) (OP b1)
Op b ~> t
bt) ((s ~> (t || a)) -> Op (~>) (OP (t || a)) (OP s)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p (OP a1) (OP b1)
Op s ~> (t || a)
sta)))

fromOpLens :: forall {k} (s :: k) t a b. (CopyDiscard k, HasCoproducts k, Ob a) => OpLens s t a b -> Prism s t a b
fromOpLens :: forall {k} (s :: k) (t :: k) (a :: k) (b :: k).
(CopyDiscard k, HasCoproducts k, Ob a) =>
OpLens s t a b -> Prism s t a b
fromOpLens OpLens s t a b
o = Optic (Prostrong LensFl) (OP t) (OP s) (OP b) (OP a)
-> ((OP t ~> OP b) -> ((OP t && OP a) ~> OP s) -> Prism s t a b)
-> Prism s t a b
forall {k} (c :: (k -> k -> Type) -> Constraint) (s :: k) (t :: k)
       (a :: k) (b :: k) r.
(HasBinaryProducts k, (Ob a, Ob b) => c (ExOptic LensFl a b)) =>
Optic c s t a b -> ((s ~> a) -> ((s && b) ~> t) -> r) -> r
withLens (OpLens s t a b
-> Optic (Prostrong LensFl) (OP t) (OP s) (OP b) (OP a)
forall {j} {k}
       (c :: (OPPOSITE k -> OPPOSITE j -> Type) -> Constraint) (s :: j)
       (t :: k) (a :: j) (b :: k).
(forall (p :: OPPOSITE k -> OPPOSITE j -> Type).
 c p =>
 c (Op (UnOp p)),
 CategoryOf j, CategoryOf k) =>
Optic (OpConstraint c) s t a b
-> Optic c (OP t) (OP s) (OP b) (OP a)
opOptic OpLens s t a b
o) (\OP t ~> OP b
rev (OP t && OP a) ~> OP s
match -> (b ~> t) -> (s ~> (t || a)) -> Prism s t a b
forall {k} (s :: k) (t :: k) (a :: k) (b :: k).
(CopyDiscard k, HasCoproducts k, Ob a) =>
(b ~> t) -> (s ~> (t || a)) -> Prism s t a b
prism (Op (~>) (OP t) (OP b) -> b ~> t
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
Op p (OP a) (OP b) -> p b a
unOp OP t ~> OP b
Op (~>) (OP t) (OP b)
rev) (Op (~>) (OP (t || a)) (OP s) -> s ~> (t || a)
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
Op p (OP a) (OP b) -> p b a
unOp (OP t && OP a) ~> OP s
Op (~>) (OP (t || a)) (OP s)
match))