{-# 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.Pattern.Category (($), (.), (/))
import Pandora.Pattern.Functor.Covariant (Covariant (comap))
import Pandora.Pattern.Functor.Extractable (extract)
import Pandora.Pattern.Functor.Pointable (point)
import Pandora.Pattern.Transformer.Liftable (lift)
import Pandora.Pattern.Object.Semigroup ((+))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run, (||=))
import Pandora.Paradigm.Inventory.Optics ((|>))
import Pandora.Paradigm.Inventory.Store (Store (Store))
import Pandora.Paradigm.Primary.Object.Boolean (Boolean (True, False))
import Pandora.Paradigm.Primary.Functor.Identity (Identity (Identity))
import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Just, Nothing))
import Pandora.Paradigm.Primary.Functor.Tagged (Tagged (Tag))
import Pandora.Paradigm.Primary.Functor.Predicate (Predicate (Predicate))
import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)), type (:*:), attached)
import Pandora.Paradigm.Primary.Functor.Wye (Wye (Both, Left, Right, End))
import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct))
import Pandora.Paradigm.Primary.Transformer.Tap (Tap (Tap))
import Pandora.Paradigm.Schemes.TU (type (<:.>))

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 :: * -> * -> *). Category m => m ~~> m
/ 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 :: * -> * -> *). Category m => m ~~> m
/ a <:= Product s
forall (t :: * -> *) a. Extractable t => a <:= t
extract s :*: a
x

instance Nullable Maybe where
	null :: (Predicate :. Maybe) := a
null = (Maybe a -> Boolean) -> (Predicate :. Maybe) := a
forall a. (a -> Boolean) -> Predicate a
Predicate ((Maybe a -> Boolean) -> (Predicate :. Maybe) := a)
-> (Maybe a -> Boolean) -> (Predicate :. Maybe) := a
forall (m :: * -> * -> *). Category m => m ~~> m
$ \case { Just a
_ -> Boolean
True ; Maybe a
_ -> Boolean
False }

instance Substructure Right (Product s) where
	type Substructural Right (Product s) = Identity
	substructure :: Lens
  ((<:.>) (Tagged 'Right) (Product s) a)
  (Substructural 'Right (Product s) a)
substructure (Product s a <:= Tagged 'Right
forall (t :: * -> *) a. Extractable t => a <:= t
extract (Product s a <:= Tagged 'Right)
-> ((<:.>) (Tagged 'Right) (Product s) a
    -> Tagged 'Right (Product s a))
-> (<:.>) (Tagged 'Right) (Product s) a
-> Product s a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Right) (Product s) a -> Tagged 'Right (Product s a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> s
s :*: a
x) =
		(((:*:) (Identity a) :. (->) (Identity a))
 := (<:.>) (Tagged 'Right) (Product s) a)
-> Store (Identity a) ((<:.>) (Tagged 'Right) (Product s) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity a) :. (->) (Identity a))
  := (<:.>) (Tagged 'Right) (Product s) a)
 -> Store (Identity a) ((<:.>) (Tagged 'Right) (Product s) a))
-> (((:*:) (Identity a) :. (->) (Identity a))
    := (<:.>) (Tagged 'Right) (Product s) a)
-> Store (Identity a) ((<:.>) (Tagged 'Right) (Product s) a)
forall (m :: * -> * -> *). Category m => m ~~> m
$ a -> Identity a
forall a. a -> Identity a
Identity a
x Identity a
-> (Identity a -> (<:.>) (Tagged 'Right) (Product s) a)
-> ((:*:) (Identity a) :. (->) (Identity a))
   := (<:.>) (Tagged 'Right) (Product s) a
forall s a. s -> a -> Product s a
:*: Product s a -> (<:.>) (Tagged 'Right) (Product s) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Product s a -> (<:.>) (Tagged 'Right) (Product s) a)
-> (Identity a -> Product s a)
-> Identity a
-> (<:.>) (Tagged 'Right) (Product s) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (s
s s -> a -> Product s a
forall s a. s -> a -> Product s a
:*:) (a -> Product s a)
-> (Identity a -> a) -> Identity a -> Product s a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Identity a -> a
forall (t :: * -> *) a. Extractable t => a <:= t
extract

instance Covariant t => Substructure Tail (Tap t) where
	type Substructural Tail (Tap t) = t
	substructure :: Lens
  ((<:.>) (Tagged 'Tail) (Tap t) a) (Substructural 'Tail (Tap t) a)
substructure (Tap t a <:= Tagged 'Tail
forall (t :: * -> *) a. Extractable t => a <:= t
extract (Tap t a <:= Tagged 'Tail)
-> ((<:.>) (Tagged 'Tail) (Tap t) a -> Tagged 'Tail (Tap t a))
-> (<:.>) (Tagged 'Tail) (Tap t) a
-> Tap t a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Tail) (Tap t) a -> Tagged 'Tail (Tap t a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Tap a
x t a
xs) =
		(((:*:) (t a) :. (->) (t a)) := (<:.>) (Tagged 'Tail) (Tap t) a)
-> Store (t a) ((<:.>) (Tagged 'Tail) (Tap t) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (t a) :. (->) (t a)) := (<:.>) (Tagged 'Tail) (Tap t) a)
 -> Store (t a) ((<:.>) (Tagged 'Tail) (Tap t) a))
-> (((:*:) (t a) :. (->) (t a)) := (<:.>) (Tagged 'Tail) (Tap t) a)
-> Store (t a) ((<:.>) (Tagged 'Tail) (Tap t) a)
forall (m :: * -> * -> *). Category m => m ~~> m
$ t a
xs t a
-> (t a -> (<:.>) (Tagged 'Tail) (Tap t) a)
-> ((:*:) (t a) :. (->) (t a)) := (<:.>) (Tagged 'Tail) (Tap t) a
forall s a. s -> a -> Product s a
:*: Tap t a -> (<:.>) (Tagged 'Tail) (Tap t) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Tap t a -> (<:.>) (Tagged 'Tail) (Tap t) a)
-> (t a -> Tap t a) -> t a -> (<:.>) (Tagged 'Tail) (Tap t) a
forall (m :: * -> * -> *) b c a.
Category 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

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
-> Construction Wye a
forall k (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> 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
	morphing ((<:.>)
  (Tagged ('Into ('Preorder (Construction Maybe))))
  (Construction Wye)
  a
-> Construction Wye a
forall k (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> 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.
Category 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 :: * -> * -> *). Category m => m ~~> m
$ Construction Wye a
-> Morphing
     ('Into ('Preorder (Nonempty List))) (Construction Wye) a
forall a (f :: a) (t :: * -> *).
Morphable ('Into f) t =>
t ~> Morphing ('Into f) t
into @(Preorder (Nonempty List)) Construction Wye a
lst
	morphing ((<:.>)
  (Tagged ('Into ('Preorder (Construction Maybe))))
  (Construction Wye)
  a
-> Construction Wye a
forall k (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> 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.
Category 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 :: * -> * -> *). Category m => m ~~> m
$ Construction Wye a
-> Morphing
     ('Into ('Preorder (Nonempty List))) (Construction Wye) a
forall a (f :: a) (t :: * -> *).
Morphable ('Into f) t =>
t ~> Morphing ('Into f) t
into @(Preorder (Nonempty List)) Construction Wye a
rst
	morphing ((<:.>)
  (Tagged ('Into ('Preorder (Construction Maybe))))
  (Construction Wye)
  a
-> Construction Wye a
forall k (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> 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.
Category 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 :: * -> * -> *). Category m => m ~~> m
$ Construction Wye a
-> Morphing
     ('Into ('Preorder (Nonempty List))) (Construction Wye) a
forall a (f :: a) (t :: * -> *).
Morphable ('Into f) t =>
t ~> Morphing ('Into f) t
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 (f :: a) (t :: * -> *).
Morphable ('Into f) t =>
t ~> Morphing ('Into f) t
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
-> Construction Wye a
forall k (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> Construct a
x Wye (Construction Wye a)
End) = a :=> Construction Maybe
forall (t :: * -> *) a. Pointable t => a :=> t
point a
x
	morphing ((<:.>)
  (Tagged ('Into ('Inorder (Construction Maybe))))
  (Construction Wye)
  a
-> Construction Wye a
forall k (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> Construct a
x (Left Construction Wye a
lst)) = Construction Wye a
-> Morphing ('Into ('Inorder (Nonempty List))) (Construction Wye) a
forall a (f :: a) (t :: * -> *).
Morphable ('Into f) t =>
t ~> Morphing ('Into f) t
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 :=> Construction Maybe
forall (t :: * -> *) a. Pointable t => a :=> t
point a
x
	morphing ((<:.>)
  (Tagged ('Into ('Inorder (Construction Maybe))))
  (Construction Wye)
  a
-> Construction Wye a
forall k (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> Construct a
x (Right Construction Wye a
rst)) = a :=> Construction Maybe
forall (t :: * -> *) a. Pointable t => a :=> t
point a
x 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 (f :: a) (t :: * -> *).
Morphable ('Into f) t =>
t ~> Morphing ('Into f) t
into @(Inorder (Nonempty List)) Construction Wye a
rst
	morphing ((<:.>)
  (Tagged ('Into ('Inorder (Construction Maybe))))
  (Construction Wye)
  a
-> Construction Wye a
forall k (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> 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 (f :: a) (t :: * -> *).
Morphable ('Into f) t =>
t ~> Morphing ('Into f) t
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 :=> Construction Maybe
forall (t :: * -> *) a. Pointable t => a :=> t
point a
x 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 (f :: a) (t :: * -> *).
Morphable ('Into f) t =>
t ~> Morphing ('Into f) t
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
-> Construction Wye a
forall k (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> Construct a
x Wye (Construction Wye a)
End) = a :=> Construction Maybe
forall (t :: * -> *) a. Pointable t => a :=> t
point a
x
	morphing ((<:.>)
  (Tagged ('Into ('Postorder (Construction Maybe))))
  (Construction Wye)
  a
-> Construction Wye a
forall k (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> Construct a
x (Left Construction Wye a
lst)) = Construction Wye a
-> Morphing
     ('Into ('Postorder (Nonempty List))) (Construction Wye) a
forall a (f :: a) (t :: * -> *).
Morphable ('Into f) t =>
t ~> Morphing ('Into f) t
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 :=> Construction Maybe
forall (t :: * -> *) a. Pointable t => a :=> t
point a
x
	morphing ((<:.>)
  (Tagged ('Into ('Postorder (Construction Maybe))))
  (Construction Wye)
  a
-> Construction Wye a
forall k (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> Construct a
x (Right Construction Wye a
rst)) = Construction Wye a
-> Morphing
     ('Into ('Postorder (Nonempty List))) (Construction Wye) a
forall a (f :: a) (t :: * -> *).
Morphable ('Into f) t =>
t ~> Morphing ('Into f) t
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 :=> Construction Maybe
forall (t :: * -> *) a. Pointable t => a :=> t
point a
x
	morphing ((<:.>)
  (Tagged ('Into ('Postorder (Construction Maybe))))
  (Construction Wye)
  a
-> Construction Wye a
forall k (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> 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 (f :: a) (t :: * -> *).
Morphable ('Into f) t =>
t ~> Morphing ('Into f) t
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 (f :: a) (t :: * -> *).
Morphable ('Into f) t =>
t ~> Morphing ('Into f) t
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 :=> Construction Maybe
forall (t :: * -> *) a. Pointable t => a :=> t
point a
x

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 (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> Binary a
xs) = (Construction Wye a
 -> Morphing ('Into (o ds)) (Construction Wye) a)
-> Maybe (Construction Wye a)
-> Maybe (Morphing ('Into (o ds)) (Construction Wye) a)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
comap (forall a (f :: a) (t :: * -> *).
Morphable ('Into f) t =>
t ~> Morphing ('Into f) t
forall (t :: * -> *).
Morphable ('Into (o ds)) t =>
t ~> Morphing ('Into (o ds)) t
into @(o ds)) (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 (t :: * -> *) (u :: * -> *) a b.
(Interpreted t, Interpreted u) =>
(Primary t a -> Primary u b) -> t a -> u b
||= Binary a
xs

instance Focusable Left (Product s) where
	type Focusing Left (Product s) a = s
	focusing :: Tagged 'Left (Product s a) :-. Focusing 'Left (Product s) a
focusing (Product s a <:= Tagged 'Left
forall (t :: * -> *) a. Extractable t => a <:= t
extract -> s
s :*: a
x) = ((Product s :. (->) s) := Tagged 'Left (Product s a))
-> Store s (Tagged 'Left (Product s a))
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store (((Product s :. (->) s) := Tagged 'Left (Product s a))
 -> Store s (Tagged 'Left (Product s a)))
-> ((Product s :. (->) s) := Tagged 'Left (Product s a))
-> Store s (Tagged 'Left (Product s a))
forall (m :: * -> * -> *). Category m => m ~~> m
$ s
s s
-> (s -> Tagged 'Left (Product s a))
-> (Product s :. (->) s) := Tagged 'Left (Product s a)
forall s a. s -> a -> Product s a
:*: Product s a -> Tagged 'Left (Product s a)
forall k (tag :: k) a. a -> Tagged tag a
Tag (Product s a -> Tagged 'Left (Product s a))
-> (s -> Product s a) -> s -> Tagged 'Left (Product s a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (s -> a -> Product s a
forall s a. s -> a -> Product s a
:*: a
x)

instance Focusable Right (Product s) where
	type Focusing Right (Product s) a = a
	focusing :: Tagged 'Right (Product s a) :-. Focusing 'Right (Product s) a
focusing (Product s a <:= Tagged 'Right
forall (t :: * -> *) a. Extractable t => a <:= t
extract -> s
s :*: a
x) = (((:*:) a :. (->) a) := Tagged 'Right (Product s a))
-> Store a (Tagged 'Right (Product s a))
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) a :. (->) a) := Tagged 'Right (Product s a))
 -> Store a (Tagged 'Right (Product s a)))
-> (((:*:) a :. (->) a) := Tagged 'Right (Product s a))
-> Store a (Tagged 'Right (Product s a))
forall (m :: * -> * -> *). Category m => m ~~> m
$ a
x a
-> (a -> Tagged 'Right (Product s a))
-> ((:*:) a :. (->) a) := Tagged 'Right (Product s a)
forall s a. s -> a -> Product s a
:*: Product s a -> Tagged 'Right (Product s a)
forall k (tag :: k) a. a -> Tagged tag a
Tag (Product s a -> Tagged 'Right (Product s a))
-> (a -> Product s a) -> a -> Tagged 'Right (Product s a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (s
s s -> a -> Product s a
forall s a. s -> a -> Product s a
:*:)

instance Accessible s (s :*: a) where
	access :: (s :*: a) :-. s
access ~(s
s :*: a
x) = (((:*:) s :. (->) s) := (s :*: a)) -> Store s (s :*: a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) s :. (->) s) := (s :*: a)) -> Store s (s :*: a))
-> (((:*:) s :. (->) s) := (s :*: a)) -> Store s (s :*: a)
forall (m :: * -> * -> *). Category m => m ~~> m
$ s
s s -> (s -> s :*: a) -> ((:*:) s :. (->) s) := (s :*: a)
forall s a. s -> a -> Product s a
:*: (s -> a -> s :*: a
forall s a. s -> a -> Product s a
:*: a
x)

instance Accessible a (s :*: a) where
	access :: (s :*: a) :-. a
access ~(s
s :*: a
x) = (((:*:) a :. (->) a) := (s :*: a)) -> Store a (s :*: a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) a :. (->) a) := (s :*: a)) -> Store a (s :*: a))
-> (((:*:) a :. (->) a) := (s :*: a)) -> Store a (s :*: a)
forall (m :: * -> * -> *). Category m => m ~~> m
$ a
x a -> (a -> s :*: a) -> ((:*:) a :. (->) a) := (s :*: a)
forall s a. s -> a -> Product s a
:*: (s
s s -> a -> s :*: a
forall s a. s -> a -> Product s a
:*:)

instance {-# OVERLAPS #-} Accessible b a => Accessible b (s :*: a) where
	access :: (s :*: a) :-. b
access = forall src. Accessible a src => src :-. a
forall tgt src. Accessible tgt src => src :-. tgt
access @a ((s :*: a) :-. a) -> Lens a b -> (s :*: a) :-. b
forall src tgt new. Lens src tgt -> Lens tgt new -> Lens src new
|> forall src. Accessible b src => src :-. b
forall tgt src. Accessible tgt src => src :-. tgt
access @b