{-# LANGUAGE AllowAmbiguousTypes #-}

-- | The __affine traversal__: the 0-or-1 focus optic that can also reconstruct, the meet of
-- 'Proarrow.Optic.Lens.Lens' and 'Proarrow.Optic.Prism.Prism' in the subtyping lattice. Its two
-- legs are 'affineMatch' @:: s ~> (t || a)@ and 'affineSet' @:: (s && b) ~> t@ ('AffineTravRes').
-- Its witnesses only ever arise by composing lens and prism witnesses, so it is built with
-- 'Proarrow.Optic.Prism.affineTraversal' (a 'Proarrow.Optic.Lens.Lens' followed by a
-- 'Proarrow.Optic.Prism.Prism') and eliminated with 'matching', via the 'MatchP' carrier.
module Proarrow.Optic.AffineTraversal where

import Prelude (($))

import Proarrow.Category.Monoidal.CopyDiscard (CopyDiscard (..))
import Proarrow.Category.Monoidal.Distributive (Bicartesian, Distributive (..))
import Proarrow.Colimit.BinaryCoproduct (Coproduct, HasBinaryCoproducts (..), HasCoproducts, left)
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), (\\), type (+->))
import Proarrow.Limit.BinaryProduct (HasBinaryProducts (..), Product, TensorIsProduct, first, second)
import Proarrow.Object (pattern Objs)
import Proarrow.Optic (CompactFlavor, FLAVOR, Optic, Optic_ (..), Prostrong (..), SubFlavor (..))
import Proarrow.Optic.AffineFold (AffineFoldRes)
import Proarrow.Optic.Fold (FoldRes)
import Proarrow.Optic.Setter (SetterRes)
import Proarrow.Optic.Traversal (TravRes)
import Proarrow.Profunctor.Corepresentable (Corep (..))
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Identity (Id (..))
import Proarrow.Profunctor.Representable (Rep (..))

-- | 'distL'/'distR' are stated in terms of @**@, which is only /equal/ to '&&' under
-- 'Proarrow.Limit.BinaryProduct.Cartesian' rather than reducing to it, and that equality doesn't propagate through the
-- non-injective '||' automatically. Forcing 'TensorIsProduct' to be solved at each component
-- (rather than relying on the quantified constraint 'Proarrow.Limit.BinaryProduct.Cartesian' provides to fire implicitly)
-- materializes the equalities as givens so they rewrite inside '||' too.
distLP
  :: forall k (a :: k) b c
   . (Distributive k, Ob a, Ob b, Ob c, TensorIsProduct a (b || c), TensorIsProduct a b, TensorIsProduct a c)
  => (a && (b || c)) ~> (a && b || a && c)
distLP :: forall k (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c, TensorIsProduct a (b || c),
 TensorIsProduct a b, TensorIsProduct a c) =>
(a && (b || c)) ~> ((a && b) || (a && c))
distLP = forall k (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL @k @a @b @c

distRP
  :: forall k (a :: k) b c
   . (Distributive k, Ob a, Ob b, Ob c, TensorIsProduct (a || b) c, TensorIsProduct a c, TensorIsProduct b c)
  => ((a || b) && c) ~> (a && c || b && c)
distRP :: forall k (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c, TensorIsProduct (a || b) c,
 TensorIsProduct a c, TensorIsProduct b c) =>
((a || b) && c) ~> ((a && c) || (b && c))
distRP = forall k (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR @k @a @b @c

type AffineTravRes :: forall {k}. FLAVOR k k
class (TravRes p q, AffineFoldRes p q) => AffineTravRes (p :: k +-> k) (q :: k +-> k) where
  affineMatch :: (Bicartesian k) => p (s :: k) a -> q b t -> s ~> (t || a)
  affineSet :: (Bicartesian k) => p (s :: k) a -> q b t -> (s && b) ~> t
instance (HasBinaryProducts k, Ob (s :: k)) => AffineTravRes (Rep (Product s)) (Corep (Product s)) where
  -- a lens always matches
  affineMatch :: forall (s :: k) (a :: k) (b :: k) (t :: k).
Bicartesian k =>
Rep (Product s) s a -> Corep (Product s) b t -> s ~> (t || a)
affineMatch @_ @a @_ @t (Rep s ~> (Product s @ a)
p) Corep (Product s) b t
q = 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
. forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @k @s @a ((s && a) ~> a) -> (s ~> (s && a)) -> s ~> 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 ~> (Product s @ a)
s ~> (s && a)
p ((Ob s, Ob (s && a)) => s ~> (t || a))
-> (s ~> (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 ~> (Product s @ a)
s ~> (s && a)
p ((Ob b, Ob t) => s ~> (t || a))
-> Corep (Product s) b t -> s ~> (t || a)
forall (a :: k) (b :: k) r.
((Ob a, Ob b) => r) -> Corep (Product s) 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
\\ Corep (Product s) b t
q
  affineSet :: forall (s :: k) (a :: k) (b :: k) (t :: k).
Bicartesian k =>
Rep (Product s) s a -> Corep (Product s) b t -> (s && b) ~> t
affineSet @_ @a @b (Rep s ~> (Product s @ a)
p) (Corep (Product s @ b) ~> t
q) = (Product s @ b) ~> t
(s && b) ~> t
q ((s && b) ~> t) -> ((s && b) ~> (s && b)) -> (s && b) ~> 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 (c :: k) (a :: k) (b :: k).
(HasBinaryProducts k, Ob c) =>
(a ~> b) -> (a && c) ~> (b && c)
forall {k} (c :: k) (a :: k) (b :: k).
(HasBinaryProducts k, Ob c) =>
(a ~> b) -> (a && c) ~> (b && c)
first @b (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @k @s @a ((s && a) ~> s) -> (s ~> (s && a)) -> s ~> s
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 ~> (Product s @ a)
s ~> (s && a)
p)
instance (CopyDiscard k, HasCoproducts k, Ob t) => AffineTravRes (Rep (Coproduct t) :: k +-> k) (Corep (Coproduct t)) where
  affineMatch :: forall (s :: k) (a :: k) (b :: k) (t :: k).
Bicartesian k =>
Rep (Coproduct t) s a -> Corep (Coproduct t) b t -> s ~> (t || a)
affineMatch @_ @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

  -- a prism's set never needs the original value, it just reviews
  affineSet :: forall (s :: k) (a :: k) (b :: k) (t :: k).
Bicartesian k =>
Rep (Coproduct t) s a -> Corep (Coproduct t) b t -> (s && b) ~> t
affineSet @s @_ @b (Rep s ~> (Coproduct t @ a)
p) (Corep (Coproduct t @ b) ~> t
q) = (Coproduct t @ b) ~> t
(t || b) ~> t
q ((t || b) ~> t) -> ((s && b) ~> (t || b)) -> (s && b) ~> 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) =>
b ~> (a || b)
rgt @k @t @b (b ~> (t || b)) -> ((s && b) ~> b) -> (s && b) ~> (t || 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
. forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @k @s @b ((Ob s, Ob (t || a)) => (s && b) ~> t)
-> (s ~> (t || a)) -> (s && b) ~> t
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 ~> (Coproduct t @ a)
s ~> (t || a)
p
instance (CategoryOf k) => AffineTravRes (Id :: k +-> k) (Id :: k +-> k) where
  affineMatch :: forall (s :: k) (a :: k) (b :: k) (t :: k).
Bicartesian k =>
Id s a -> Id b t -> s ~> (t || a)
affineMatch @_ @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
  affineSet :: forall (s :: k) (a :: k) (b :: k) (t :: k).
Bicartesian k =>
Id s a -> Id b t -> (s && b) ~> t
affineSet @s @_ @b Id s a
sa (Id b ~> t
bt) = b ~> t
bt (b ~> t) -> ((s && b) ~> b) -> (s && b) ~> 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).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @k @s @b ((Ob s, Ob a) => (s && b) ~> t) -> Id s a -> (s && b) ~> t
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 s a
sa ((Ob b, Ob t) => (s && b) ~> t) -> (b ~> t) -> (s && b) ~> t
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
instance (AffineTravRes f g, AffineTravRes f' g') => AffineTravRes (f :.: f') (g' :.: g) where
  -- match the outer; on failure of the inner, reconstruct via the outer's own setter, reusing s
  affineMatch :: forall (s :: i) (a :: i) (b :: i) (t :: i).
Bicartesian i =>
(:.:) f f' s a -> (:.:) g' g b t -> s ~> (t || a)
affineMatch @s @a @_ @t ((:.:) @m f :: f s b
f@f s b
Objs f' :: f' b a
f'@f' b a
Objs) ((:.:) @n g' :: g' b b
g'@g' b b
Objs 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)) -> ((s && t) ~> t) -> (s && t) ~> (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 (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @_ @s @t)
        ((s && t) ~> (t || a))
-> ((s && b) ~> (t || a)) -> ((s && t) || (s && 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 k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @_ @t @a (t ~> (t || a)) -> ((s && b) ~> t) -> (s && 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).
(AffineTravRes p q, Bicartesian k) =>
p s a -> q b t -> (s && b) ~> t
forall (p :: i +-> i) (q :: i +-> i) (s :: i) (a :: i) (b :: i)
       (t :: i).
(AffineTravRes p q, Bicartesian i) =>
p s a -> q b t -> (s && b) ~> t
affineSet @f @g f s b
f g b t
g) ((s && b) ~> (t || a))
-> ((s && a) ~> (t || a)) -> ((s && b) || (s && a)) ~> (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 k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @_ @t @a (a ~> (t || a)) -> ((s && a) ~> a) -> (s && a) ~> (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 (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @_ @s @a))
                (((s && b) || (s && a)) ~> (t || a))
-> ((s && b) ~> ((s && b) || (s && a))) -> (s && 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 (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c, TensorIsProduct a (b || c),
 TensorIsProduct a b, TensorIsProduct a c) =>
(a && (b || c)) ~> ((a && b) || (a && c))
distLP @_ @s @n @a
                ((s && (b || a)) ~> ((s && b) || (s && a)))
-> ((s && b) ~> (s && (b || a)))
-> (s && b) ~> ((s && b) || (s && 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 (c :: i) (a :: i) (b :: i).
(HasBinaryProducts i, Ob c) =>
(a ~> b) -> (c && a) ~> (c && b)
forall {k} (c :: k) (a :: k) (b :: k).
(HasBinaryProducts k, Ob c) =>
(a ~> b) -> (c && a) ~> (c && b)
second @s (forall {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
(AffineTravRes p q, Bicartesian 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).
(AffineTravRes p q, Bicartesian i) =>
p s a -> q b t -> s ~> (t || a)
affineMatch @f' @g' f' b a
f' g' b b
g')
            )
    )
      (((s && t) || (s && b)) ~> (t || a))
-> (s ~> ((s && t) || (s && 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 (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c, TensorIsProduct a (b || c),
 TensorIsProduct a b, TensorIsProduct a c) =>
(a && (b || c)) ~> ((a && b) || (a && c))
distLP @_ @s @t @m
      ((s && (t || b)) ~> ((s && t) || (s && b)))
-> (s ~> (s && (t || b))) -> s ~> ((s && t) || (s && b))
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
. (s ~> s
forall (a :: i). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (s ~> s) -> (s ~> (t || b)) -> s ~> (s && (t || b))
forall (a :: i) (x :: i) (y :: i).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& forall {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
(AffineTravRes p q, Bicartesian 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).
(AffineTravRes p q, Bicartesian i) =>
p s a -> q b t -> s ~> (t || a)
affineMatch @f @g f s b
f g b t
g)

  -- if the outer already fails, the new b is irrelevant; otherwise set inner-then-outer, reusing s
  affineSet :: forall (s :: i) (a :: i) (b :: i) (t :: i).
Bicartesian i =>
(:.:) f f' s a -> (:.:) g' g b t -> (s && b) ~> t
affineSet @s @_ @b @t ((:.:) @m f :: f s b
f@f s b
Objs f' :: f' b a
f'@f' b a
Objs) ((:.:) g' :: g' b b
g'@g' b b
Objs g :: g b t
g@g b t
Objs) =
    forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @_ @t @b ((Ob (t && b) => (s && b) ~> t) -> (s && b) ~> t)
-> (Ob (t && b) => (s && b) ~> t) -> (s && b) ~> t
forall a b. (a -> b) -> a -> b
$
      forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @_ @m @b ((Ob (b && b) => (s && b) ~> t) -> (s && b) ~> t)
-> (Ob (b && b) => (s && b) ~> t) -> (s && b) ~> t
forall a b. (a -> b) -> a -> b
$
        ( (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @_ @t @b ((t && b) ~> t)
-> ((s && (t && b)) ~> (t && b)) -> (s && (t && b)) ~> t
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 (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @_ @s @(t && b))
            ((s && (t && b)) ~> t)
-> ((s && (b && b)) ~> t)
-> ((s && (t && b)) || (s && (b && b))) ~> t
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 {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
(AffineTravRes p q, Bicartesian k) =>
p s a -> q b t -> (s && b) ~> t
forall (p :: i +-> i) (q :: i +-> i) (s :: i) (a :: i) (b :: i)
       (t :: i).
(AffineTravRes p q, Bicartesian i) =>
p s a -> q b t -> (s && b) ~> t
affineSet @f @g f s b
f g b t
g ((s && b) ~> t)
-> ((s && (b && b)) ~> (s && b)) -> (s && (b && b)) ~> t
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 (c :: i) (a :: i) (b :: i).
(HasBinaryProducts i, Ob c) =>
(a ~> b) -> (c && a) ~> (c && b)
forall {k} (c :: k) (a :: k) (b :: k).
(HasBinaryProducts k, Ob c) =>
(a ~> b) -> (c && a) ~> (c && b)
second @s (forall {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
(AffineTravRes p q, Bicartesian k) =>
p s a -> q b t -> (s && b) ~> t
forall (p :: i +-> i) (q :: i +-> i) (s :: i) (a :: i) (b :: i)
       (t :: i).
(AffineTravRes p q, Bicartesian i) =>
p s a -> q b t -> (s && b) ~> t
affineSet @f' @g' f' b a
f' g' b b
g'))
        )
          (((s && (t && b)) || (s && (b && b))) ~> t)
-> ((s && b) ~> ((s && (t && b)) || (s && (b && b))))
-> (s && b) ~> t
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 (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c, TensorIsProduct a (b || c),
 TensorIsProduct a b, TensorIsProduct a c) =>
(a && (b || c)) ~> ((a && b) || (a && c))
distLP @_ @s @(t && b) @(m && b)
          ((s && ((t && b) || (b && b)))
 ~> ((s && (t && b)) || (s && (b && b))))
-> ((s && b) ~> (s && ((t && b) || (b && b))))
-> (s && b) ~> ((s && (t && b)) || (s && (b && b)))
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 (c :: i) (a :: i) (b :: i).
(HasBinaryProducts i, Ob c) =>
(a ~> b) -> (c && a) ~> (c && b)
forall {k} (c :: k) (a :: k) (b :: k).
(HasBinaryProducts k, Ob c) =>
(a ~> b) -> (c && a) ~> (c && b)
second @s (forall k (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c, TensorIsProduct (a || b) c,
 TensorIsProduct a c, TensorIsProduct b c) =>
((a || b) && c) ~> ((a && c) || (b && c))
distRP @_ @t @m @b)
          ((s && ((t || b) && b)) ~> (s && ((t && b) || (b && b))))
-> ((s && b) ~> (s && ((t || b) && b)))
-> (s && b) ~> (s && ((t && b) || (b && b)))
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 (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @_ @s @b ((s && b) ~> s)
-> ((s && b) ~> ((t || b) && b))
-> (s && b) ~> (s && ((t || b) && b))
forall (a :: i) (x :: i) (y :: i).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& forall (c :: i) (a :: i) (b :: i).
(HasBinaryProducts i, Ob c) =>
(a ~> b) -> (a && c) ~> (b && c)
forall {k} (c :: k) (a :: k) (b :: k).
(HasBinaryProducts k, Ob c) =>
(a ~> b) -> (a && c) ~> (b && c)
first @b (forall {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
(AffineTravRes p q, Bicartesian 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).
(AffineTravRes p q, Bicartesian i) =>
p s a -> q b t -> s ~> (t || a)
affineMatch @f @g f s b
f g b t
g))

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

instance CompactFlavor AffineTravRes

type AffineTraversal (s :: k) (t :: k) a b = Optic (Prostrong AffineTravRes) s t a b
type AffineTraversal' s a = AffineTraversal s s a a

-- | The eliminating carrier for 'matching': an affine traversal's match leg @s '~>' (t '||' a)@,
-- as a profunctor in @s@\/@t@.
type MatchP :: forall {k}. k -> k +-> k
data MatchP (a :: k) (s :: k) (t :: k) where
  MatchP :: (Ob t) => {forall {k} (t :: k) (s :: k) (a :: k).
MatchP a s t -> s ~> (t || a)
unMatchP :: s ~> (t || a)} -> MatchP a s t

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

-- | Any flavor whose optics can match has strength for the 'MatchP' carrier. Combining an outer
-- witness pair with the stored match leg is exactly the affine-traversal composition's match rule:
-- match the outer, and on the inner's failure reconstruct a @t@ via the outer's own 'affineSet'.
instance
  (Bicartesian k, Ob (a :: k), SubFlavor w AffineTravRes)
  => Prostrong (w :: FLAVOR k k) (MatchP a :: k +-> k)
  where
  proact :: forall (f :: k +-> k) (g :: k +-> k).
(w f g, Profunctor f, Profunctor g) =>
((f :.: MatchP a) :.: g) :~> MatchP a
proact @f @g @s @t ((:.:) @n ((:.:) @m fw :: f a b
fw@f a b
Objs (MatchP b ~> (b || a)
mm)) gw :: g b b
gw@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 @AffineTravRes @f @g
      ( (a ~> (b || a)) -> MatchP a a b
forall {k} (t :: k) (s :: k) (a :: k).
Ob t =>
(s ~> (t || a)) -> MatchP a s t
MatchP
          ( ( (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @_ @t @a (b ~> (b || a)) -> ((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
. forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @_ @s @t)
                ((a && b) ~> (b || a))
-> ((a && b) ~> (b || a)) -> ((a && b) || (a && 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 k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @_ @t @a (b ~> (b || a)) -> ((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
. forall {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
(AffineTravRes p q, Bicartesian k) =>
p s a -> q b t -> (s && b) ~> t
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
(AffineTravRes p q, Bicartesian k) =>
p s a -> q b t -> (s && b) ~> t
affineSet @f @g f a b
fw g b b
gw) ((a && b) ~> (b || a))
-> ((a && a) ~> (b || a)) -> ((a && b) || (a && a)) ~> (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 k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @_ @t @a (a ~> (b || a)) -> ((a && a) ~> a) -> (a && 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 (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @_ @s @a))
                        (((a && b) || (a && a)) ~> (b || a))
-> ((a && b) ~> ((a && b) || (a && a))) -> (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
. forall k (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c, TensorIsProduct a (b || c),
 TensorIsProduct a b, TensorIsProduct a c) =>
(a && (b || c)) ~> ((a && b) || (a && c))
distLP @_ @s @n @a
                        ((a && (b || a)) ~> ((a && b) || (a && a)))
-> ((a && b) ~> (a && (b || a)))
-> (a && b) ~> ((a && b) || (a && 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 (c :: k) (a :: k) (b :: k).
(HasBinaryProducts k, Ob c) =>
(a ~> b) -> (c && a) ~> (c && b)
forall {k} (c :: k) (a :: k) (b :: k).
(HasBinaryProducts k, Ob c) =>
(a ~> b) -> (c && a) ~> (c && b)
second @s b ~> (b || a)
mm
                    )
            )
              (((a && b) || (a && b)) ~> (b || a))
-> (a ~> ((a && b) || (a && 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 (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c, TensorIsProduct a (b || c),
 TensorIsProduct a b, TensorIsProduct a c) =>
(a && (b || c)) ~> ((a && b) || (a && c))
distLP @_ @s @t @m
              ((a && (b || b)) ~> ((a && b) || (a && b)))
-> (a ~> (a && (b || b))) -> a ~> ((a && b) || (a && 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
. (a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (a ~> a) -> (a ~> (b || b)) -> a ~> (a && (b || b))
forall (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& forall {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
(AffineTravRes p q, Bicartesian 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).
(AffineTravRes p q, Bicartesian k) =>
p s a -> q b t -> s ~> (t || a)
affineMatch @f @g f a b
fw g b b
gw)
          )
      )

-- | Match through any optic that can act as an affine traversal, in either encoding: returns the
-- focus (@'rgt'@) when it matches, or a reconstructed @t@ (@'lft'@) when it does not. This is the
-- 'AffineTraversal' eliminator, refining 'Proarrow.Optic.AffineFold.preview' (which forgets @t@).
matching
  :: forall {k} c (s :: k) (t :: k) a b
   . (Bicartesian k, c (MatchP a))
  => Optic c s t a b -> s ~> (t || a)
matching :: forall {k} (c :: (k -> k -> Type) -> Constraint) (s :: k) (t :: k)
       (a :: k) (b :: k).
(Bicartesian k, c (MatchP a)) =>
Optic c s t a b -> s ~> (t || a)
matching (Optic forall (p :: k +-> k). c p => p a b -> p s t
l) = MatchP a s t -> s ~> (t || a)
forall {k} (t :: k) (s :: k) (a :: k).
MatchP a s t -> s ~> (t || a)
unMatchP (forall (p :: k +-> k). c p => p a b -> p s t
l @(MatchP a) ((a ~> (b || a)) -> MatchP a a b
forall {k} (t :: k) (s :: k) (a :: k).
Ob t =>
(s ~> (t || a)) -> MatchP a s t
MatchP (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @b @a)))