{-# 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)@ ('PrismRes' \/ '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 'Market' carrier;
-- 'toOpLens'\/'fromOpLens' witness the equivalence with the op-lens encoding, and 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
  ( CompactFlavor
  , ExOptic (..)
  , FLAVOR
  , Flip
  , OpConstraint
  , Optic
  , Optic_ (..)
  , Prostrong (..)
  , SubFlavor (..)
  , convert
  , ex2prof
  , opOptic
  , unOpOptic
  , (%)
  )
import Proarrow.Optic.AffineFold (AffineFoldRes)
import Proarrow.Optic.AffineTraversal (AffineTravRes (..), AffineTraversal)
import Proarrow.Optic.Fold (FoldRes)
import Proarrow.Optic.Getter (GetterRes (..))
import Proarrow.Optic.Lens (Lens, LensRes, lens, withLens)
import Proarrow.Optic.Setter (SetterRes)
import Proarrow.Optic.Traversal (MonTravRes, TravRes)
import Proarrow.Profunctor.Corepresentable (Corep (..))
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Identity (Id (..))
import Proarrow.Profunctor.Representable (Rep (..))

type PrismRes :: forall {k}. FLAVOR k k
class (AffineTravRes p q, GetterRes q p, MonTravRes p q) => PrismRes (p :: k +-> k) (q :: k +-> k) where
  -- | Like 'affineMatch', but with an honest constraint: prism witnesses only ever need binary
  -- coproducts, 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) => PrismRes (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 :: k +-> 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 :: k +-> 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) => PrismRes (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 :: k +-> 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 (PrismRes f g, PrismRes f' g') => PrismRes (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).
GetterRes p q =>
p s a -> s ~> a
forall (p :: i +-> i) (q :: i +-> i) (s :: i) (a :: i).
GetterRes 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 :: k +-> 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).
(PrismRes 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).
(PrismRes 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 :: k +-> 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).
(PrismRes 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).
(PrismRes p q, HasBinaryCoproducts i) =>
p s a -> q b t -> s ~> (t || a)
matchingP @f @g f s b
f g b t
g

instance CompactFlavor PrismRes

instance SubFlavor PrismRes AffineTravRes where subFlavor :: forall (p :: j +-> j) (q :: j +-> j) r.
PrismRes p q =>
(AffineTravRes p q => r) -> r
subFlavor AffineTravRes p q => r
r = r
AffineTravRes p q => r
r
instance SubFlavor PrismRes MonTravRes where subFlavor :: forall (p :: j +-> j) (q :: j +-> j) r.
PrismRes p q =>
(MonTravRes p q => r) -> r
subFlavor MonTravRes p q => r
r = r
MonTravRes p q => r
r
instance SubFlavor PrismRes (Flip GetterRes) where subFlavor :: forall (p :: j +-> j) (q :: j +-> j) r.
PrismRes p q =>
(Flip GetterRes p q => r) -> r
subFlavor Flip GetterRes p q => r
r = r
Flip GetterRes p q => r
r
instance SubFlavor PrismRes TravRes where subFlavor :: forall (p :: j +-> j) (q :: j +-> j) r.
PrismRes p q =>
(TravRes p q => r) -> r
subFlavor TravRes p q => r
r = r
TravRes p q => r
r
instance SubFlavor PrismRes SetterRes where subFlavor :: forall (p :: j +-> j) (q :: j +-> j) r.
PrismRes p q =>
(SetterRes p q => r) -> r
subFlavor SetterRes p q => r
r = r
SetterRes p q => r
r
instance SubFlavor PrismRes AffineFoldRes where subFlavor :: forall (p :: j +-> j) (q :: j +-> j) r.
PrismRes p q =>
(AffineFoldRes p q => r) -> r
subFlavor AffineFoldRes p q => r
r = r
AffineFoldRes p q => r
r
instance SubFlavor PrismRes FoldRes where subFlavor :: forall (p :: j +-> j) (q :: j +-> j) r.
PrismRes p q =>
(FoldRes p q => r) -> r
subFlavor FoldRes p q => r
r = r
FoldRes p q => r
r

-- | A reversed prism views its build leg (@'getP'@ on the swapped pair): @'Proarrow.Optic.re' prism@ is a getter.
instance SubFlavor (Flip PrismRes) GetterRes where subFlavor :: forall (p :: j +-> j) (q :: j +-> j) r.
Flip PrismRes p q =>
(GetterRes p q => r) -> r
subFlavor GetterRes p q => r
r = r
GetterRes p q => r
r

instance SubFlavor (Flip PrismRes) AffineFoldRes where subFlavor :: forall (p :: j +-> j) (q :: j +-> j) r.
Flip PrismRes p q =>
(AffineFoldRes p q => r) -> r
subFlavor AffineFoldRes p q => r
r = r
AffineFoldRes p q => r
r
instance SubFlavor (Flip PrismRes) FoldRes where subFlavor :: forall (p :: j +-> j) (q :: j +-> j) r.
Flip PrismRes p q =>
(FoldRes p q => r) -> r
subFlavor FoldRes p q => r
r = r
FoldRes p q => r
r

type Prism (s :: k) t a b = Optic (Prostrong PrismRes) 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 =
  ExOptic PrismRes a b s t -> Optic (Prostrong PrismRes) s t a b
forall {j} {k} {w :: FLAVOR j k} (a :: k) (b :: j) (s :: k)
       (t :: j).
(CategoryOf j, CategoryOf k) =>
ExOptic w a b s t -> Optic (Prostrong w) s t a b
ex2prof (forall {j} {k} {w :: FLAVOR j k} (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(w p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: ExOptic w a b) q s t -> ExOptic w a b s t
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (t :: k) (a :: k)
       (b :: k).
(PrismRes p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: ExOptic PrismRes a b) q s t
-> ExOptic PrismRes a b s t
ExProstrong @(Rep (Coproduct t)) @(Corep (Coproduct t)) ((s ~> (Coproduct t @ a)) -> Rep (Coproduct t) s a
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep s ~> (Coproduct t @ a)
s ~> (t || a)
sta Rep (Coproduct t) s a
-> ExOptic PrismRes a b a b
-> (:.:) (Rep (Coproduct t)) (ExOptic PrismRes a b) s b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (a ~> a) -> (b ~> b) -> ExOptic PrismRes a b a b
forall {j} {k} {w :: FLAVOR j k} (s :: k) (t :: j) (a :: k)
       (b :: j).
(s ~> a) -> (b ~> t) -> ExOptic w a b s t
ExIso a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id b ~> b
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (:.:) (Rep (Coproduct t)) (ExOptic PrismRes a b) s b
-> Corep (Coproduct t) b t
-> (:.:)
     (Rep (Coproduct t) :.: ExOptic PrismRes a b)
     (Corep (Coproduct t))
     s
     t
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: ((Coproduct t @ b) ~> t) -> Corep (Coproduct t) b t
forall {j} {k} (a :: j) (f :: j +-> k) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
Corep (t ~> t
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> 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 PrismRes) s t a b)
-> (b ~> t) -> Optic (Prostrong PrismRes) 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 design-aligned way to
-- make one -- the same @'convert' (l '%' p)@ idiom the test suite uses.
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 LensRes :&&: Prostrong PrismRes) s t a b
-> Optic (Prostrong AffineTravRes) 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, (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 LensRes :&&: Prostrong PrismRes) 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)

-- | The eliminating carrier for prisms: a prism's two legs, as a profunctor in @s@\/@t@.
type Market :: forall {k}. k -> k -> k +-> k
data Market a b s t where
  Market :: (Ob a, Ob b) => (b ~> t) -> (s ~> (t || a)) -> Market a b s t

instance (HasBinaryCoproducts k, Ob (a :: k), Ob b) => Profunctor (Market a b :: k +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> Market a b a b -> Market a b c d
dimap c ~> a
l b ~> d
r (Market b ~> b
bt a ~> (b || a)
sta) = (b ~> d) -> (c ~> (d || a)) -> Market a b c d
forall {k} (a :: k) (b :: k) (t :: k) (s :: k).
(Ob a, Ob b) =>
(b ~> t) -> (s ~> (t || a)) -> Market a b s t
Market (b ~> d
r (b ~> d) -> (b ~> b) -> b ~> d
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. b ~> b
bt) (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 b ~> d
r ((b || a) ~> (d || a)) -> (c ~> (b || a)) -> c ~> (d || a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> (b || a)
sta (a ~> (b || a)) -> (c ~> a) -> c ~> (b || a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. c ~> a
l) ((Ob c, Ob a) => Market a b c d) -> (c ~> a) -> Market a b c d
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
\\ c ~> a
l ((Ob b, Ob d) => Market a b c d) -> (b ~> d) -> Market a b c d
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 ~> d
r
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: k) r.
((Ob a, Ob b) => r) -> Market a b a b -> r
\\ Market b ~> b
bt a ~> (b || a)
sta = r
(Ob b, Ob b) => r
(Ob a, Ob b) => r
r ((Ob b, Ob b) => r) -> (b ~> b) -> r
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 ~> b
bt ((Ob a, Ob (b || a)) => r) -> (a ~> (b || a)) -> r
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
\\ a ~> (b || a)
sta

-- | Any flavor whose optics have prism legs has strength for the 'Market' carrier.
instance (HasBinaryCoproducts k, Ob (a :: k), Ob b, SubFlavor w PrismRes) => Prostrong (w :: FLAVOR k k) (Market a b :: k +-> k) where
  proact :: forall (f :: k +-> k) (g :: k +-> k).
(w f g, Profunctor f, Profunctor g) =>
((f :.: Market a b) :.: g) :~> Market a b
proact @f @g @_ @t (f :: f a b
f@f a b
Objs :.: Market b ~> b
bt b ~> (b || a)
sta :.: g :: g b b
g@g b b
Objs) =
    forall {j} {k} (w1 :: FLAVOR j k) (w2 :: FLAVOR j k) (p :: k +-> k)
       (q :: j +-> j) r.
(SubFlavor w1 w2, w1 p q) =>
(w2 p q => r) -> r
forall (w1 :: FLAVOR k k) (w2 :: FLAVOR k k) (p :: k +-> k)
       (q :: k +-> k) r.
(SubFlavor w1 w2, w1 p q) =>
(w2 p q => r) -> r
subFlavor @w @PrismRes @f @g
      ((b ~> b) -> (a ~> (b || a)) -> Market a b a b
forall {k} (a :: k) (b :: k) (t :: k) (s :: k).
(Ob a, Ob b) =>
(b ~> t) -> (s ~> (t || a)) -> Market a b s t
Market (forall {j} {k} (p :: k +-> k) (q :: j +-> j) (s :: k) (a :: k).
GetterRes p q =>
p s a -> s ~> a
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k).
GetterRes p q =>
p s a -> s ~> a
getP @g @f g b b
g (b ~> b) -> (b ~> b) -> b ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. b ~> b
bt) ((forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @_ @t @a (b ~> (b || a)) -> (b ~> (b || a)) -> (b || b) ~> (b || a)
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
||| (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 (forall {j} {k} (p :: k +-> k) (q :: j +-> j) (s :: k) (a :: k).
GetterRes p q =>
p s a -> s ~> a
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k).
GetterRes p q =>
p s a -> s ~> a
getP @g @f g b b
g) ((b || a) ~> (b || a)) -> (b ~> (b || a)) -> b ~> (b || a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. b ~> (b || a)
sta)) ((b || b) ~> (b || a)) -> (a ~> (b || b)) -> a ~> (b || a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> 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).
(PrismRes 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).
(PrismRes p q, HasBinaryCoproducts k) =>
p s a -> q b t -> s ~> (t || a)
matchingP @f @g f a b
f g b b
g))

-- | Eliminate any optic that is at least an iso and at most a prism to its two legs, in either
-- encoding.
withPrism
  :: forall {k} c (s :: k) (t :: k) a b r
   . (HasBinaryCoproducts k, (Ob a, Ob b) => c (Market 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 (Market a b)) =>
Optic c s t a b -> ((b ~> t) -> (s ~> (t || a)) -> r) -> r
withPrism (Optic forall (p :: k +-> k). c p => p a b -> p s t
l) (b ~> t) -> (s ~> (t || a)) -> r
k = case forall (p :: k +-> k). c p => p a b -> p s t
l @(Market a b) ((b ~> b) -> (a ~> (b || a)) -> Market a b a b
forall {k} (a :: k) (b :: k) (t :: k) (s :: k).
(Ob a, Ob b) =>
(b ~> t) -> (s ~> (t || a)) -> Market a b s t
Market b ~> b
b ~> b
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @b @a)) of Market b ~> t
bt s ~> (t || a)
sta -> (b ~> t) -> (s ~> (t || a)) -> r
k b ~> t
b ~> t
bt s ~> (t || a)
s ~> (t || a)
sta

-- | 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 'PrismRes' prism to its legs (via 'Market') 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 'PrismRes' 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 LensRes)) 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 (Market 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 LensRes) ('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 LensRes) ('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 LensRes) ('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 (Shop a b)) =>
Optic c s t a b -> ((s ~> a) -> ((s && b) ~> t) -> r) -> r
withLens (OpLens s t a b
-> Optic (Prostrong LensRes) ('OP t) ('OP s) ('OP b) ('OP a)
forall {k1} {k2}
       (c :: (OPPOSITE k1 -> OPPOSITE k2 -> Type) -> Constraint) (s :: k2)
       (t :: k1) (a :: k2) (b :: k1).
(forall (p :: OPPOSITE k1 -> OPPOSITE k2 -> Type).
 c p =>
 c (Op (UnOp p))) =>
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))