{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}

module Pandora.Paradigm.Structure (module Exports) where

import Pandora.Paradigm.Structure.Ability as Exports
import Pandora.Paradigm.Structure.Interface as Exports
import Pandora.Paradigm.Structure.Modification as Exports
import Pandora.Paradigm.Structure.Some as Exports

import Pandora.Core.Functor (type (:=))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category ((#), identity)
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-)))
import Pandora.Pattern.Transformer.Liftable (lift)
import Pandora.Pattern.Transformer.Lowerable (lower)
import Pandora.Pattern.Object.Semigroup ((+))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run, (=#-), (!))
import Pandora.Paradigm.Inventory.Some.Optics ()
import Pandora.Paradigm.Inventory.Some.Store (Store (Store))
import Pandora.Paradigm.Primary.Algebraic.Product ((:*:) ((:*:)), attached)
import Pandora.Paradigm.Primary.Algebraic.Sum ((:+:) (Option, Adoption))
import Pandora.Paradigm.Primary.Algebraic.Exponential ((%))
import Pandora.Paradigm.Primary.Algebraic (extract)
import Pandora.Paradigm.Primary.Functor.Exactly (Exactly (Exactly))
import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Just, Nothing))
import Pandora.Paradigm.Primary.Functor.Wye (Wye (Both, Left, Right, End))
import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct))
import Pandora.Paradigm.Primary.Linear.Vector (Vector (Scalar, Vector))
import Pandora.Paradigm.Primary (twosome)
import Pandora.Pattern.Morphism.Flip (Flip (Flip))
import Pandora.Paradigm.Primary.Transformer.Tap (Tap (Tap))
import Pandora.Paradigm.Schemes.TU (type (<:.>))
import Pandora.Paradigm.Schemes.TT (TT (TT))
import Pandora.Paradigm.Schemes.T_U ( type (<:.:>))
import Pandora.Paradigm.Schemes.P_Q_T (P_Q_T (P_Q_T))

instance Monotonic s a => Monotonic s (s :*: a) where
	reduce :: (s -> r -> r) -> r -> (s :*: a) -> r
reduce s -> r -> r
f r
r s :*: a
x = (s -> r -> r) -> r -> a -> r
forall a e r. Monotonic a e => (a -> r -> r) -> r -> e -> r
reduce s -> r -> r
f (r -> a -> r) -> r -> a -> r
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# s -> r -> r
f ((s :*: a) -> s
forall a b. (a :*: b) -> a
attached s :*: a
x) r
r (a -> r) -> a -> r
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (s :*: a) -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract s :*: a
x

instance (Covariant (->) (->) t) => Substructure Tail (Tap t) where
	type Available Tail (Tap t) = Exactly
	type Substance Tail (Tap t) = t
	substructure :: Lens
  (Available 'Tail (Tap t))
  ((<:.>) (Tagged 'Tail) (Tap t) a)
  (Substance 'Tail (Tap t) a)
substructure = ((<:.>) (Tagged 'Tail) (Tap t) a
 -> Store (Exactly (t a)) ((<:.>) (Tagged 'Tail) (Tap t) a))
-> P_Q_T (->) Store Exactly ((<:.>) (Tagged 'Tail) (Tap t) a) (t a)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Tail) (Tap t) a
  -> Store (Exactly (t a)) ((<:.>) (Tagged 'Tail) (Tap t) a))
 -> P_Q_T
      (->) Store Exactly ((<:.>) (Tagged 'Tail) (Tap t) a) (t a))
-> ((<:.>) (Tagged 'Tail) (Tap t) a
    -> Store (Exactly (t a)) ((<:.>) (Tagged 'Tail) (Tap t) a))
-> P_Q_T (->) Store Exactly ((<:.>) (Tagged 'Tail) (Tap t) a) (t a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(<:.>) (Tagged 'Tail) (Tap t) a
tap -> case Tagged 'Tail (Tap t a) -> Tap t a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Tagged 'Tail (Tap t a) -> Tap t a)
-> Tagged 'Tail (Tap t a) -> Tap t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<:.>) (Tagged 'Tail) (Tap t) a -> Tagged 'Tail (Tap t a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (<:.>) (Tagged 'Tail) (Tap t) a
tap of
		Tap a
x t a
xs -> (((:*:) (Exactly (t a)) :. (->) (Exactly (t a)))
 := (<:.>) (Tagged 'Tail) (Tap t) a)
-> Store (Exactly (t a)) ((<:.>) (Tagged 'Tail) (Tap t) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Exactly (t a)) :. (->) (Exactly (t a)))
  := (<:.>) (Tagged 'Tail) (Tap t) a)
 -> Store (Exactly (t a)) ((<:.>) (Tagged 'Tail) (Tap t) a))
-> (((:*:) (Exactly (t a)) :. (->) (Exactly (t a)))
    := (<:.>) (Tagged 'Tail) (Tap t) a)
-> Store (Exactly (t a)) ((<:.>) (Tagged 'Tail) (Tap t) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! t a -> Exactly (t a)
forall a. a -> Exactly a
Exactly t a
xs Exactly (t a)
-> (Exactly (t a) -> (<:.>) (Tagged 'Tail) (Tap t) a)
-> ((:*:) (Exactly (t a)) :. (->) (Exactly (t a)))
   := (<:.>) (Tagged 'Tail) (Tap t) a
forall s a. s -> a -> s :*: a
:*: Tap t a -> (<:.>) (Tagged 'Tail) (Tap t) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Tap t a -> (<:.>) (Tagged 'Tail) (Tap t) a)
-> (Exactly (t a) -> Tap t a)
-> Exactly (t a)
-> (<:.>) (Tagged 'Tail) (Tap t) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> t a -> Tap t a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap a
x (t a -> Tap t a)
-> (Exactly (t a) -> t a) -> Exactly (t a) -> Tap t a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Exactly (t a) -> t a
forall (t :: * -> *) a. Extractable t => t a -> a
extract

instance Morphable (Into (Preorder (Construction Maybe))) (Construction Wye) where
	type Morphing (Into (Preorder (Construction Maybe))) (Construction Wye) = Construction Maybe
	morphing :: (<::>)
  (Tagged ('Into ('Preorder (Construction Maybe))))
  (Construction Wye)
  a
-> Morphing
     ('Into ('Preorder (Construction Maybe))) (Construction Wye) a
morphing (<::>)
  (Tagged ('Into ('Preorder (Construction Maybe))))
  (Construction Wye)
  a
nonempty_binary = case (<::>)
  (Tagged ('Into ('Preorder (Construction Maybe))))
  (Construction Wye)
  a
-> Construction Wye a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph (<::>)
  (Tagged ('Into ('Preorder (Construction Maybe))))
  (Construction Wye)
  a
nonempty_binary of
		Construct a
x Wye (Construction Wye a)
End -> a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Maybe :. Construction Maybe) := a
forall a. Maybe a
Nothing
		Construct a
x (Left Construction Wye a
lst) -> a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (((Maybe :. Construction Maybe) := a) -> Construction Maybe a)
-> (Construction Maybe a -> (Maybe :. Construction Maybe) := a)
-> Construction Maybe a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall a. a -> Maybe a
Just (Construction Maybe a -> Construction Maybe a)
-> Construction Maybe a -> Construction Maybe a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Construction Wye a
-> Morphing
     ('Into ('Preorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Preorder (Nonempty List)) Construction Wye a
lst
		Construct a
x (Right Construction Wye a
rst) -> a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (((Maybe :. Construction Maybe) := a) -> Construction Maybe a)
-> (Construction Maybe a -> (Maybe :. Construction Maybe) := a)
-> Construction Maybe a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall a. a -> Maybe a
Just (Construction Maybe a -> Construction Maybe a)
-> Construction Maybe a -> Construction Maybe a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Construction Wye a
-> Morphing
     ('Into ('Preorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Preorder (Nonempty List)) Construction Wye a
rst
		Construct a
x (Both Construction Wye a
lst Construction Wye a
rst) -> a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (((Maybe :. Construction Maybe) := a) -> Construction Maybe a)
-> (Construction Maybe a -> (Maybe :. Construction Maybe) := a)
-> Construction Maybe a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall a. a -> Maybe a
Just (Construction Maybe a -> Construction Maybe a)
-> Construction Maybe a -> Construction Maybe a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Construction Wye a
-> Morphing
     ('Into ('Preorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Preorder (Nonempty List)) Construction Wye a
lst Construction Maybe a
-> Construction Maybe a -> Construction Maybe a
forall a. Semigroup a => a -> a -> a
+ Construction Wye a
-> Morphing
     ('Into ('Preorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Preorder (Nonempty List)) Construction Wye a
rst

instance Morphable (Into (Inorder (Construction Maybe))) (Construction Wye) where
	type Morphing (Into (Inorder (Construction Maybe))) (Construction Wye) = Construction Maybe
	morphing :: (<::>)
  (Tagged ('Into ('Inorder (Construction Maybe))))
  (Construction Wye)
  a
-> Morphing
     ('Into ('Inorder (Construction Maybe))) (Construction Wye) a
morphing (<::>)
  (Tagged ('Into ('Inorder (Construction Maybe))))
  (Construction Wye)
  a
nonempty_binary = case (<::>)
  (Tagged ('Into ('Inorder (Construction Maybe))))
  (Construction Wye)
  a
-> Construction Wye a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph (<::>)
  (Tagged ('Into ('Inorder (Construction Maybe))))
  (Construction Wye)
  a
nonempty_binary of
		Construct a
x Wye (Construction Wye a)
End -> a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Maybe :. Construction Maybe) := a
forall a. Maybe a
Nothing
		Construct a
x (Left Construction Wye a
lst) -> Construction Wye a
-> Morphing ('Into ('Inorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Inorder (Nonempty List)) Construction Wye a
lst Construction Maybe a
-> Construction Maybe a -> Construction Maybe a
forall a. Semigroup a => a -> a -> a
+ a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Maybe :. Construction Maybe) := a
forall a. Maybe a
Nothing
		Construct a
x (Right Construction Wye a
rst) -> a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Maybe :. Construction Maybe) := a
forall a. Maybe a
Nothing Construction Maybe a
-> Construction Maybe a -> Construction Maybe a
forall a. Semigroup a => a -> a -> a
+ Construction Wye a
-> Morphing ('Into ('Inorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Inorder (Nonempty List)) Construction Wye a
rst
		Construct a
x (Both Construction Wye a
lst Construction Wye a
rst) -> Construction Wye a
-> Morphing ('Into ('Inorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Inorder (Nonempty List)) Construction Wye a
lst Construction Maybe a
-> Construction Maybe a -> Construction Maybe a
forall a. Semigroup a => a -> a -> a
+ a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Maybe :. Construction Maybe) := a
forall a. Maybe a
Nothing Construction Maybe a
-> Construction Maybe a -> Construction Maybe a
forall a. Semigroup a => a -> a -> a
+ Construction Wye a
-> Morphing ('Into ('Inorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Inorder (Nonempty List)) Construction Wye a
rst

instance Morphable (Into (Postorder (Construction Maybe))) (Construction Wye) where
	type Morphing (Into (Postorder (Construction Maybe))) (Construction Wye) = Construction Maybe
	morphing :: (<::>)
  (Tagged ('Into ('Postorder (Construction Maybe))))
  (Construction Wye)
  a
-> Morphing
     ('Into ('Postorder (Construction Maybe))) (Construction Wye) a
morphing (<::>)
  (Tagged ('Into ('Postorder (Construction Maybe))))
  (Construction Wye)
  a
nonempty_binary = case (<::>)
  (Tagged ('Into ('Postorder (Construction Maybe))))
  (Construction Wye)
  a
-> Construction Wye a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph (<::>)
  (Tagged ('Into ('Postorder (Construction Maybe))))
  (Construction Wye)
  a
nonempty_binary of
		Construct a
x Wye (Construction Wye a)
End -> a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Maybe :. Construction Maybe) := a
forall a. Maybe a
Nothing
		Construct a
x (Left Construction Wye a
lst) -> Construction Wye a
-> Morphing
     ('Into ('Postorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Postorder (Nonempty List)) Construction Wye a
lst Construction Maybe a
-> Construction Maybe a -> Construction Maybe a
forall a. Semigroup a => a -> a -> a
+ a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Maybe :. Construction Maybe) := a
forall a. Maybe a
Nothing
		Construct a
x (Right Construction Wye a
rst) -> Construction Wye a
-> Morphing
     ('Into ('Postorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Postorder (Nonempty List)) Construction Wye a
rst Construction Maybe a
-> Construction Maybe a -> Construction Maybe a
forall a. Semigroup a => a -> a -> a
+ a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Maybe :. Construction Maybe) := a
forall a. Maybe a
Nothing
		Construct a
x (Both Construction Wye a
lst Construction Wye a
rst) -> Construction Wye a
-> Morphing
     ('Into ('Postorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Postorder (Nonempty List)) Construction Wye a
lst Construction Maybe a
-> Construction Maybe a -> Construction Maybe a
forall a. Semigroup a => a -> a -> a
+ Construction Wye a
-> Morphing
     ('Into ('Postorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Postorder (Nonempty List)) Construction Wye a
rst Construction Maybe a
-> Construction Maybe a -> Construction Maybe a
forall a. Semigroup a => a -> a -> a
+ a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Maybe :. Construction Maybe) := a
forall a. Maybe a
Nothing

instance Morphable (Into (o ds)) (Construction Wye) => Morphable (Into (o ds)) Binary where
	type Morphing (Into (o ds)) Binary = Maybe <:.> Morphing (Into (o ds)) (Construction Wye)
	morphing :: (<::>) (Tagged ('Into (o ds))) Binary a
-> Morphing ('Into (o ds)) Binary a
morphing ((<::>) (Tagged ('Into (o ds))) Binary a -> Binary a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Binary a
xs) = (forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
forall (struct :: * -> *).
Morphable ('Into (o ds)) struct =>
struct ~> Morphing ('Into (o ds)) struct
into @(o ds) (Construction Wye a
 -> Morphing ('Into (o ds)) (Construction Wye) a)
-> Maybe (Construction Wye a)
-> Maybe (Morphing ('Into (o ds)) (Construction Wye) a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-) (Primary Binary a
 -> Primary
      (TU
         Covariant
         Covariant
         Maybe
         (Morphing ('Into (o ds)) (Construction Wye)))
      a)
-> Binary a
-> TU
     Covariant
     Covariant
     Maybe
     (Morphing ('Into (o ds)) (Construction Wye))
     a
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
m (Primary t a) (Primary u b) -> m (t a) (u b)
=#- Binary a
xs

instance Substructure Left (Flip (:*:) a) where
	type Available Left (Flip (:*:) a) = Exactly
	type Substance Left (Flip (:*:) a) = Exactly
	substructure :: Lens
  (Available 'Left (Flip (:*:) a))
  ((<:.>) (Tagged 'Left) (Flip (:*:) a) a)
  (Substance 'Left (Flip (:*:) a) a)
substructure = ((<:.>) (Tagged 'Left) (Flip (:*:) a) a
 -> Store
      (Exactly (Exactly a)) ((<:.>) (Tagged 'Left) (Flip (:*:) a) a))
-> P_Q_T
     (->)
     Store
     Exactly
     ((<:.>) (Tagged 'Left) (Flip (:*:) a) a)
     (Exactly a)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Left) (Flip (:*:) a) a
  -> Store
       (Exactly (Exactly a)) ((<:.>) (Tagged 'Left) (Flip (:*:) a) a))
 -> P_Q_T
      (->)
      Store
      Exactly
      ((<:.>) (Tagged 'Left) (Flip (:*:) a) a)
      (Exactly a))
-> ((<:.>) (Tagged 'Left) (Flip (:*:) a) a
    -> Store
         (Exactly (Exactly a)) ((<:.>) (Tagged 'Left) (Flip (:*:) a) a))
-> P_Q_T
     (->)
     Store
     Exactly
     ((<:.>) (Tagged 'Left) (Flip (:*:) a) a)
     (Exactly a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(<:.>) (Tagged 'Left) (Flip (:*:) a) a
product -> case Flip (:*:) a a -> a :*: a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Flip (:*:) a a -> a :*: a) -> Flip (:*:) a a -> a :*: a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<:.>) (Tagged 'Left) (Flip (:*:) a) a -> Flip (:*:) a a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged 'Left) (Flip (:*:) a) a
product of
		a
s :*: a
x -> (((:*:) (Exactly (Exactly a)) :. (->) (Exactly (Exactly a)))
 := (<:.>) (Tagged 'Left) (Flip (:*:) a) a)
-> Store
     (Exactly (Exactly a)) ((<:.>) (Tagged 'Left) (Flip (:*:) a) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Exactly (Exactly a)) :. (->) (Exactly (Exactly a)))
  := (<:.>) (Tagged 'Left) (Flip (:*:) a) a)
 -> Store
      (Exactly (Exactly a)) ((<:.>) (Tagged 'Left) (Flip (:*:) a) a))
-> (((:*:) (Exactly (Exactly a)) :. (->) (Exactly (Exactly a)))
    := (<:.>) (Tagged 'Left) (Flip (:*:) a) a)
-> Store
     (Exactly (Exactly a)) ((<:.>) (Tagged 'Left) (Flip (:*:) a) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Exactly a -> Exactly (Exactly a)
forall a. a -> Exactly a
Exactly (a -> Exactly a
forall a. a -> Exactly a
Exactly a
s) Exactly (Exactly a)
-> (Exactly (Exactly a) -> (<:.>) (Tagged 'Left) (Flip (:*:) a) a)
-> ((:*:) (Exactly (Exactly a)) :. (->) (Exactly (Exactly a)))
   := (<:.>) (Tagged 'Left) (Flip (:*:) a) a
forall s a. s -> a -> s :*: a
:*: Flip (:*:) a a -> (<:.>) (Tagged 'Left) (Flip (:*:) a) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Flip (:*:) a a -> (<:.>) (Tagged 'Left) (Flip (:*:) a) a)
-> (Exactly (Exactly a) -> Flip (:*:) a a)
-> Exactly (Exactly a)
-> (<:.>) (Tagged 'Left) (Flip (:*:) a) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a :*: a) -> Flip (:*:) a a
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip ((a :*: a) -> Flip (:*:) a a)
-> (Exactly (Exactly a) -> a :*: a)
-> Exactly (Exactly a)
-> Flip (:*:) a a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a -> a -> a :*: a
forall s a. s -> a -> s :*: a
:*: a
x) (a -> a :*: a)
-> (Exactly (Exactly a) -> a) -> Exactly (Exactly a) -> a :*: a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Exactly a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Exactly a -> a)
-> (Exactly (Exactly a) -> Exactly a) -> Exactly (Exactly a) -> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Exactly (Exactly a) -> Exactly a
forall (t :: * -> *) a. Extractable t => t a -> a
extract

instance Substructure Right ((:*:) s) where
	type Available Right ((:*:) s) = Exactly
	type Substance Right ((:*:) s) = Exactly
	substructure :: Lens
  (Available 'Right ((:*:) s))
  ((<:.>) (Tagged 'Right) ((:*:) s) a)
  (Substance 'Right ((:*:) s) a)
substructure = ((<:.>) (Tagged 'Right) ((:*:) s) a
 -> Store
      (Exactly (Exactly a)) ((<:.>) (Tagged 'Right) ((:*:) s) a))
-> P_Q_T
     (->) Store Exactly ((<:.>) (Tagged 'Right) ((:*:) s) a) (Exactly a)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Right) ((:*:) s) a
  -> Store
       (Exactly (Exactly a)) ((<:.>) (Tagged 'Right) ((:*:) s) a))
 -> P_Q_T
      (->)
      Store
      Exactly
      ((<:.>) (Tagged 'Right) ((:*:) s) a)
      (Exactly a))
-> ((<:.>) (Tagged 'Right) ((:*:) s) a
    -> Store
         (Exactly (Exactly a)) ((<:.>) (Tagged 'Right) ((:*:) s) a))
-> P_Q_T
     (->) Store Exactly ((<:.>) (Tagged 'Right) ((:*:) s) a) (Exactly a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(<:.>) (Tagged 'Right) ((:*:) s) a
product -> case (<:.>) (Tagged 'Right) ((:*:) s) a -> s :*: a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged 'Right) ((:*:) s) a
product of
		s
s :*: a
x -> (((:*:) (Exactly (Exactly a)) :. (->) (Exactly (Exactly a)))
 := (<:.>) (Tagged 'Right) ((:*:) s) a)
-> Store (Exactly (Exactly a)) ((<:.>) (Tagged 'Right) ((:*:) s) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Exactly (Exactly a)) :. (->) (Exactly (Exactly a)))
  := (<:.>) (Tagged 'Right) ((:*:) s) a)
 -> Store
      (Exactly (Exactly a)) ((<:.>) (Tagged 'Right) ((:*:) s) a))
-> (((:*:) (Exactly (Exactly a)) :. (->) (Exactly (Exactly a)))
    := (<:.>) (Tagged 'Right) ((:*:) s) a)
-> Store (Exactly (Exactly a)) ((<:.>) (Tagged 'Right) ((:*:) s) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Exactly a -> Exactly (Exactly a)
forall a. a -> Exactly a
Exactly (a -> Exactly a
forall a. a -> Exactly a
Exactly a
x) Exactly (Exactly a)
-> (Exactly (Exactly a) -> (<:.>) (Tagged 'Right) ((:*:) s) a)
-> ((:*:) (Exactly (Exactly a)) :. (->) (Exactly (Exactly a)))
   := (<:.>) (Tagged 'Right) ((:*:) s) a
forall s a. s -> a -> s :*: a
:*: (s :*: a) -> (<:.>) (Tagged 'Right) ((:*:) s) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift ((s :*: a) -> (<:.>) (Tagged 'Right) ((:*:) s) a)
-> (Exactly (Exactly a) -> s :*: a)
-> Exactly (Exactly a)
-> (<:.>) (Tagged 'Right) ((:*:) s) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (s
s s -> a -> s :*: a
forall s a. s -> a -> s :*: a
:*:) (a -> s :*: a)
-> (Exactly (Exactly a) -> a) -> Exactly (Exactly a) -> s :*: a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Exactly a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Exactly a -> a)
-> (Exactly (Exactly a) -> Exactly a) -> Exactly (Exactly a) -> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Exactly (Exactly a) -> Exactly a
forall (t :: * -> *) a. Extractable t => t a -> a
extract

instance Accessible s (s :*: a) where
	access :: Lens Exactly (s :*: a) s
access = ((s :*: a) -> Store (Exactly s) (s :*: a))
-> Lens Exactly (s :*: a) s
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((s :*: a) -> Store (Exactly s) (s :*: a))
 -> Lens Exactly (s :*: a) s)
-> ((s :*: a) -> Store (Exactly s) (s :*: a))
-> Lens Exactly (s :*: a) s
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(s
s :*: a
x) -> (((:*:) (Exactly s) :. (->) (Exactly s)) := (s :*: a))
-> Store (Exactly s) (s :*: a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Exactly s) :. (->) (Exactly s)) := (s :*: a))
 -> Store (Exactly s) (s :*: a))
-> (((:*:) (Exactly s) :. (->) (Exactly s)) := (s :*: a))
-> Store (Exactly s) (s :*: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! s -> Exactly s
forall a. a -> Exactly a
Exactly s
s Exactly s
-> (Exactly s -> s :*: a)
-> ((:*:) (Exactly s) :. (->) (Exactly s)) := (s :*: a)
forall s a. s -> a -> s :*: a
:*: (s -> a -> s :*: a
forall s a. s -> a -> s :*: a
:*: a
x) (s -> s :*: a) -> (Exactly s -> s) -> Exactly s -> s :*: a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Exactly s -> s
forall (t :: * -> *) a. Extractable t => t a -> a
extract

instance Accessible a (s :*: a) where
	access :: Lens Exactly (s :*: a) a
access = ((s :*: a) -> Store (Exactly a) (s :*: a))
-> Lens Exactly (s :*: a) a
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((s :*: a) -> Store (Exactly a) (s :*: a))
 -> Lens Exactly (s :*: a) a)
-> ((s :*: a) -> Store (Exactly a) (s :*: a))
-> Lens Exactly (s :*: a) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(s
s :*: a
x) -> (((:*:) (Exactly a) :. (->) (Exactly a)) := (s :*: a))
-> Store (Exactly a) (s :*: a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Exactly a) :. (->) (Exactly a)) := (s :*: a))
 -> Store (Exactly a) (s :*: a))
-> (((:*:) (Exactly a) :. (->) (Exactly a)) := (s :*: a))
-> Store (Exactly a) (s :*: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! a -> Exactly a
forall a. a -> Exactly a
Exactly a
x Exactly a
-> (Exactly a -> s :*: a)
-> ((:*:) (Exactly a) :. (->) (Exactly a)) := (s :*: a)
forall s a. s -> a -> s :*: a
:*: (s
s s -> a -> s :*: a
forall s a. s -> a -> s :*: a
:*:) (a -> s :*: a) -> (Exactly a -> a) -> Exactly a -> s :*: a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Exactly a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract

instance {-# OVERLAPS #-} Accessible b a => Accessible b (s :*: a) where
	access :: Lens Exactly (s :*: a) b
access = forall source. Accessible b source => Lens Exactly source b
forall target source.
Accessible target source =>
Lens Exactly source target
access @b Lens Exactly a b
-> P_Q_T (->) Store Exactly (s :*: a) a -> Lens Exactly (s :*: a) b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall source. Accessible a source => Lens Exactly source a
forall target source.
Accessible target source =>
Lens Exactly source target
access @a

-- TODO: Causes overlapping instances error when target is (a :*: b), it's better to use some wrapper instead
-- instance {-# OVERLAPS #-} (Accessible a s, Accessible b s) => Accessible (a :*: b) s where
	-- access = mult @(-->) @(:*:) @(:*:) ! (access @a :*: access @b)

instance Accessible a (Exactly a) where
	access :: Lens Exactly (Exactly a) a
access = (Exactly a -> Store (Exactly a) (Exactly a))
-> Lens Exactly (Exactly a) a
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T ((Exactly a -> Store (Exactly a) (Exactly a))
 -> Lens Exactly (Exactly a) a)
-> (Exactly a -> Store (Exactly a) (Exactly a))
-> Lens Exactly (Exactly a) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(Exactly a
x) -> (((:*:) (Exactly a) :. (->) (Exactly a)) := Exactly a)
-> Store (Exactly a) (Exactly a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Exactly a) :. (->) (Exactly a)) := Exactly a)
 -> Store (Exactly a) (Exactly a))
-> (((:*:) (Exactly a) :. (->) (Exactly a)) := Exactly a)
-> Store (Exactly a) (Exactly a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! a -> Exactly a
forall a. a -> Exactly a
Exactly a
x Exactly a
-> (Exactly a -> Exactly a)
-> ((:*:) (Exactly a) :. (->) (Exactly a)) := Exactly a
forall s a. s -> a -> s :*: a
:*: Exactly a -> Exactly a
forall (m :: * -> * -> *) a. Category m => m a a
identity

instance Possible a (Maybe a) where
	perhaps :: Lens Maybe (Maybe a) a
perhaps = (Maybe a -> Store (Maybe a) (Maybe a)) -> Lens Maybe (Maybe a) a
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T ((Maybe a -> Store (Maybe a) (Maybe a)) -> Lens Maybe (Maybe a) a)
-> (Maybe a -> Store (Maybe a) (Maybe a)) -> Lens Maybe (Maybe a) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \Maybe a
x -> (((:*:) (Maybe a) :. (->) (Maybe a)) := Maybe a)
-> Store (Maybe a) (Maybe a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe a) :. (->) (Maybe a)) := Maybe a)
 -> Store (Maybe a) (Maybe a))
-> (((:*:) (Maybe a) :. (->) (Maybe a)) := Maybe a)
-> Store (Maybe a) (Maybe a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Maybe a
x Maybe a
-> (Maybe a -> Maybe a)
-> ((:*:) (Maybe a) :. (->) (Maybe a)) := Maybe a
forall s a. s -> a -> s :*: a
:*: Maybe a -> Maybe a
forall (m :: * -> * -> *) a. Category m => m a a
identity

instance {-# OVERLAPS #-} Possible a (o :+: a) where
	perhaps :: Lens Maybe (o :+: a) a
perhaps = ((o :+: a) -> Store (Maybe a) (o :+: a)) -> Lens Maybe (o :+: a) a
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((o :+: a) -> Store (Maybe a) (o :+: a))
 -> Lens Maybe (o :+: a) a)
-> ((o :+: a) -> Store (Maybe a) (o :+: a))
-> Lens Maybe (o :+: a) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \case
		Option o
s -> (((:*:) (Maybe a) :. (->) (Maybe a)) := (o :+: a))
-> Store (Maybe a) (o :+: a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe a) :. (->) (Maybe a)) := (o :+: a))
 -> Store (Maybe a) (o :+: a))
-> (((:*:) (Maybe a) :. (->) (Maybe a)) := (o :+: a))
-> Store (Maybe a) (o :+: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Maybe a
forall a. Maybe a
Nothing Maybe a
-> (Maybe a -> o :+: a)
-> ((:*:) (Maybe a) :. (->) (Maybe a)) := (o :+: a)
forall s a. s -> a -> s :*: a
:*: (a -> o :+: a) -> (o :+: a) -> Maybe a -> o :+: a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve @a @(Maybe a) a -> o :+: a
forall o a. a -> o :+: a
Adoption (o -> o :+: a
forall o a. o -> o :+: a
Option o
s)
		Adoption a
x -> (((:*:) (Maybe a) :. (->) (Maybe a)) := (o :+: a))
-> Store (Maybe a) (o :+: a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe a) :. (->) (Maybe a)) := (o :+: a))
 -> Store (Maybe a) (o :+: a))
-> (((:*:) (Maybe a) :. (->) (Maybe a)) := (o :+: a))
-> Store (Maybe a) (o :+: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! a -> Maybe a
forall a. a -> Maybe a
Just a
x Maybe a
-> (Maybe a -> o :+: a)
-> ((:*:) (Maybe a) :. (->) (Maybe a)) := (o :+: a)
forall s a. s -> a -> s :*: a
:*: (a -> o :+: a) -> (o :+: a) -> Maybe a -> o :+: a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve @a @(Maybe a) a -> o :+: a
forall o a. a -> o :+: a
Adoption (a -> o :+: a
forall o a. a -> o :+: a
Adoption a
x)

instance {-# OVERLAPS #-} Possible o (o :+: a) where
	perhaps :: Lens Maybe (o :+: a) o
perhaps = ((o :+: a) -> Store (Maybe o) (o :+: a)) -> Lens Maybe (o :+: a) o
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((o :+: a) -> Store (Maybe o) (o :+: a))
 -> Lens Maybe (o :+: a) o)
-> ((o :+: a) -> Store (Maybe o) (o :+: a))
-> Lens Maybe (o :+: a) o
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \case
		Option o
s -> (((:*:) (Maybe o) :. (->) (Maybe o)) := (o :+: a))
-> Store (Maybe o) (o :+: a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe o) :. (->) (Maybe o)) := (o :+: a))
 -> Store (Maybe o) (o :+: a))
-> (((:*:) (Maybe o) :. (->) (Maybe o)) := (o :+: a))
-> Store (Maybe o) (o :+: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! o -> Maybe o
forall a. a -> Maybe a
Just o
s Maybe o
-> (Maybe o -> o :+: a)
-> ((:*:) (Maybe o) :. (->) (Maybe o)) := (o :+: a)
forall s a. s -> a -> s :*: a
:*: (o -> o :+: a) -> (o :+: a) -> Maybe o -> o :+: a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve @o @(Maybe o) o -> o :+: a
forall o a. o -> o :+: a
Option (o -> o :+: a
forall o a. o -> o :+: a
Option o
s)
		Adoption a
x -> (((:*:) (Maybe o) :. (->) (Maybe o)) := (o :+: a))
-> Store (Maybe o) (o :+: a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe o) :. (->) (Maybe o)) := (o :+: a))
 -> Store (Maybe o) (o :+: a))
-> (((:*:) (Maybe o) :. (->) (Maybe o)) := (o :+: a))
-> Store (Maybe o) (o :+: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Maybe o
forall a. Maybe a
Nothing Maybe o
-> (Maybe o -> o :+: a)
-> ((:*:) (Maybe o) :. (->) (Maybe o)) := (o :+: a)
forall s a. s -> a -> s :*: a
:*: (o -> o :+: a) -> (o :+: a) -> Maybe o -> o :+: a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve @o @(Maybe o) o -> o :+: a
forall o a. o -> o :+: a
Option (a -> o :+: a
forall o a. a -> o :+: a
Adoption a
x)

instance Accessible target source => Possible target (Maybe source) where
	perhaps :: Lens Maybe (Maybe source) target
perhaps = let lst :: Lens Exactly source target
lst = Accessible target source => Lens Exactly source target
forall target source.
Accessible target source =>
Lens Exactly source target
access @target @source in (Maybe source -> Store (Maybe target) (Maybe source))
-> Lens Maybe (Maybe source) target
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T ((Maybe source -> Store (Maybe target) (Maybe source))
 -> Lens Maybe (Maybe source) target)
-> (Maybe source -> Store (Maybe target) (Maybe source))
-> Lens Maybe (Maybe source) target
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \case
		Just source
source -> let (Exactly target
target :*: Exactly target -> source
its) = Store (Exactly target) source
-> Exactly target :*: (Exactly target -> source)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Lens Exactly source target
lst Lens Exactly source target
-> source -> Store (Exactly target) source
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! source
source) in
			(((:*:) (Maybe target) :. (->) (Maybe target)) := Maybe source)
-> Store (Maybe target) (Maybe source)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe target) :. (->) (Maybe target)) := Maybe source)
 -> Store (Maybe target) (Maybe source))
-> (((:*:) (Maybe target) :. (->) (Maybe target)) := Maybe source)
-> Store (Maybe target) (Maybe source)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! target -> Maybe target
forall a. a -> Maybe a
Just target
target Maybe target
-> (Maybe target -> Maybe source)
-> ((:*:) (Maybe target) :. (->) (Maybe target)) := Maybe source
forall s a. s -> a -> s :*: a
:*: (Exactly target -> source
its (Exactly target -> source)
-> (target -> Exactly target) -> target -> source
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. target -> Exactly target
forall a. a -> Exactly a
Exactly (target -> source) -> Maybe target -> Maybe source
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-)
		Maybe source
Nothing -> (((:*:) (Maybe target) :. (->) (Maybe target)) := Maybe source)
-> Store (Maybe target) (Maybe source)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe target) :. (->) (Maybe target)) := Maybe source)
 -> Store (Maybe target) (Maybe source))
-> (((:*:) (Maybe target) :. (->) (Maybe target)) := Maybe source)
-> Store (Maybe target) (Maybe source)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Maybe target
forall a. Maybe a
Nothing Maybe target
-> (Maybe target -> Maybe source)
-> ((:*:) (Maybe target) :. (->) (Maybe target)) := Maybe source
forall s a. s -> a -> s :*: a
:*: \Maybe target
_ -> Maybe source
forall a. Maybe a
Nothing

instance Accessible (Maybe target) source => Possible target source where
	perhaps :: Lens Maybe source target
perhaps = let lst :: Lens Exactly source (Maybe target)
lst = Accessible (Maybe target) source =>
Lens Exactly source (Maybe target)
forall target source.
Accessible target source =>
Lens Exactly source target
access @(Maybe target) @source in (source -> Store (Maybe target) source) -> Lens Maybe source target
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T ((source -> Store (Maybe target) source)
 -> Lens Maybe source target)
-> (source -> Store (Maybe target) source)
-> Lens Maybe source target
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \source
source ->
		let Exactly (Maybe target)
target :*: Exactly (Maybe target) -> source
imts = Store (Exactly (Maybe target)) source
-> Exactly (Maybe target) :*: (Exactly (Maybe target) -> source)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Lens Exactly source (Maybe target)
lst Lens Exactly source (Maybe target)
-> source -> Store (Exactly (Maybe target)) source
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! source
source) in
			(((:*:) (Maybe target) :. (->) (Maybe target)) := source)
-> Store (Maybe target) source
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe target) :. (->) (Maybe target)) := source)
 -> Store (Maybe target) source)
-> (((:*:) (Maybe target) :. (->) (Maybe target)) := source)
-> Store (Maybe target) source
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Exactly (Maybe target) -> Maybe target
forall (t :: * -> *) a. Extractable t => t a -> a
extract Exactly (Maybe target)
target Maybe target
-> (Maybe target -> source)
-> ((:*:) (Maybe target) :. (->) (Maybe target)) := source
forall s a. s -> a -> s :*: a
:*: Exactly (Maybe target) -> source
imts (Exactly (Maybe target) -> source)
-> (Maybe target -> Exactly (Maybe target))
-> Maybe target
-> source
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Maybe target -> Exactly (Maybe target)
forall a. a -> Exactly a
Exactly

instance (Covariant (->) (->) t) => Substructure Left (t <:.:> t := (:*:)) where
	type Available Left (t <:.:> t := (:*:)) = Exactly
	type Substance Left (t <:.:> t := (:*:)) = t
	substructure :: Lens
  (Available 'Left ((t <:.:> t) := (:*:)))
  ((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a)
  (Substance 'Left ((t <:.:> t) := (:*:)) a)
substructure = ((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a
 -> Store
      (Exactly (t a)) ((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a))
-> P_Q_T
     (->)
     Store
     Exactly
     ((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a)
     (t a)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a
  -> Store
       (Exactly (t a)) ((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a))
 -> P_Q_T
      (->)
      Store
      Exactly
      ((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a)
      (t a))
-> ((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a
    -> Store
         (Exactly (t a)) ((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a))
-> P_Q_T
     (->)
     Store
     Exactly
     ((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a)
     (t a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a
x -> case (:=) (t <:.:> t) (:*:) a -> t a :*: t a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run ((:=) (t <:.:> t) (:*:) a -> t a :*: t a)
-> (:=) (t <:.:> t) (:*:) a -> t a :*: t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a
-> (:=) (t <:.:> t) (:*:) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a
x of
		t a
ls :*: t a
rs -> (((:*:) (Exactly (t a)) :. (->) (Exactly (t a)))
 := (<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a)
-> Store
     (Exactly (t a)) ((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Exactly (t a)) :. (->) (Exactly (t a)))
  := (<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a)
 -> Store
      (Exactly (t a)) ((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a))
-> (((:*:) (Exactly (t a)) :. (->) (Exactly (t a)))
    := (<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a)
-> Store
     (Exactly (t a)) ((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! t a -> Exactly (t a)
forall a. a -> Exactly a
Exactly t a
ls Exactly (t a)
-> (Exactly (t a)
    -> (<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a)
-> ((:*:) (Exactly (t a)) :. (->) (Exactly (t a)))
   := (<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a
forall s a. s -> a -> s :*: a
:*: (:=) (t <:.:> t) (:*:) a
-> (<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift ((:=) (t <:.:> t) (:*:) a
 -> (<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a)
-> (Exactly (t a) -> (:=) (t <:.:> t) (:*:) a)
-> Exactly (t a)
-> (<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (t a -> t a -> (:=) (t <:.:> t) (:*:) a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (t a -> t a -> (:=) (t <:.:> t) (:*:) a)
-> t a -> t a -> (:=) (t <:.:> t) (:*:) a
forall a b c. (a -> b -> c) -> b -> a -> c
% t a
rs) (t a -> (:=) (t <:.:> t) (:*:) a)
-> (Exactly (t a) -> t a)
-> Exactly (t a)
-> (:=) (t <:.:> t) (:*:) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Exactly (t a) -> t a
forall (t :: * -> *) a. Extractable t => t a -> a
extract

instance (Covariant (->) (->) t) => Substructure Right (t <:.:> t := (:*:)) where
	type Available Right (t <:.:> t := (:*:)) = Exactly
	type Substance Right (t <:.:> t := (:*:)) = t
	substructure :: Lens
  (Available 'Right ((t <:.:> t) := (:*:)))
  ((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a)
  (Substance 'Right ((t <:.:> t) := (:*:)) a)
substructure = ((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a
 -> Store
      (Exactly (t a)) ((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a))
-> P_Q_T
     (->)
     Store
     Exactly
     ((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a)
     (t a)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a
  -> Store
       (Exactly (t a)) ((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a))
 -> P_Q_T
      (->)
      Store
      Exactly
      ((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a)
      (t a))
-> ((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a
    -> Store
         (Exactly (t a)) ((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a))
-> P_Q_T
     (->)
     Store
     Exactly
     ((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a)
     (t a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a
x -> case (:=) (t <:.:> t) (:*:) a -> t a :*: t a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run ((:=) (t <:.:> t) (:*:) a -> t a :*: t a)
-> (:=) (t <:.:> t) (:*:) a -> t a :*: t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a
-> (:=) (t <:.:> t) (:*:) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a
x of
		t a
ls :*: t a
rs -> (((:*:) (Exactly (t a)) :. (->) (Exactly (t a)))
 := (<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a)
-> Store
     (Exactly (t a)) ((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Exactly (t a)) :. (->) (Exactly (t a)))
  := (<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a)
 -> Store
      (Exactly (t a)) ((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a))
-> (((:*:) (Exactly (t a)) :. (->) (Exactly (t a)))
    := (<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a)
-> Store
     (Exactly (t a)) ((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! t a -> Exactly (t a)
forall a. a -> Exactly a
Exactly t a
rs Exactly (t a)
-> (Exactly (t a)
    -> (<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a)
-> ((:*:) (Exactly (t a)) :. (->) (Exactly (t a)))
   := (<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a
forall s a. s -> a -> s :*: a
:*: (:=) (t <:.:> t) (:*:) a
-> (<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift ((:=) (t <:.:> t) (:*:) a
 -> (<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a)
-> (Exactly (t a) -> (:=) (t <:.:> t) (:*:) a)
-> Exactly (t a)
-> (<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (t a -> t a -> (:=) (t <:.:> t) (:*:) a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome t a
ls) (t a -> (:=) (t <:.:> t) (:*:) a)
-> (Exactly (t a) -> t a)
-> Exactly (t a)
-> (:=) (t <:.:> t) (:*:) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Exactly (t a) -> t a
forall (t :: * -> *) a. Extractable t => t a -> a
extract

instance Morphable (Into List) (Vector r) where
	type Morphing (Into List) (Vector r) = List
	morphing :: (<::>) (Tagged ('Into List)) (Vector r) a
-> Morphing ('Into List) (Vector r) a
morphing ((<::>) (Tagged ('Into List)) (Vector r) a -> Vector r a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Scalar r
x) = ((Maybe :. Construction Maybe) := r)
-> TT Covariant Covariant Maybe (Construction Maybe) r
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (((Maybe :. Construction Maybe) := r)
 -> TT Covariant Covariant Maybe (Construction Maybe) r)
-> (Construction Maybe r -> (Maybe :. Construction Maybe) := r)
-> Construction Maybe r
-> TT Covariant Covariant Maybe (Construction Maybe) r
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Maybe r -> (Maybe :. Construction Maybe) := r
forall a. a -> Maybe a
Just (Construction Maybe r
 -> TT Covariant Covariant Maybe (Construction Maybe) r)
-> Construction Maybe r
-> TT Covariant Covariant Maybe (Construction Maybe) r
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! r -> ((Maybe :. Construction Maybe) := r) -> Construction Maybe r
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct r
x (Maybe :. Construction Maybe) := r
forall a. Maybe a
Nothing
	morphing ((<::>) (Tagged ('Into List)) (Vector r) a -> Vector r a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Vector a
x Vector r a
xs) = a :=:=> List
forall k (mod :: k) (struct :: * -> *) a.
Morphed mod struct ((Exactly <:.:> struct) := (->)) =>
a :=:=> struct
item @Push a
x (TT Covariant Covariant Maybe (Construction Maybe) a
 -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Vector r a -> Morphing ('Into List) (Vector r) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @List Vector r a
xs

instance Morphable (Into (Construction Maybe)) (Vector r) where
	type Morphing (Into (Construction Maybe)) (Vector r) = Construction Maybe
	morphing :: (<::>) (Tagged ('Into (Construction Maybe))) (Vector r) a
-> Morphing ('Into (Construction Maybe)) (Vector r) a
morphing ((<::>) (Tagged ('Into (Construction Maybe))) (Vector r) a
-> Vector r a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Scalar r
x) = r -> ((Maybe :. Construction Maybe) := r) -> Construction Maybe r
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct r
x (Maybe :. Construction Maybe) := r
forall a. Maybe a
Nothing
	morphing ((<::>) (Tagged ('Into (Construction Maybe))) (Vector r) a
-> Vector r a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Vector a
x Vector r a
xs) = a :=:=> Construction Maybe
forall k (mod :: k) (struct :: * -> *) a.
Morphed mod struct ((Exactly <:.:> struct) := (->)) =>
a :=:=> struct
item @Push a
x (Construction Maybe a -> Construction Maybe a)
-> Construction Maybe a -> Construction Maybe a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Vector r a -> Morphing ('Into (Nonempty List)) (Vector r) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Nonempty List) Vector r a
xs