{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE UndecidableInstances #-}
module Pandora.Paradigm.Structure.Ability.Substructure where

import Pandora.Core.Functor (type (>))
import Pandora.Pattern.Semigroupoid (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.Paradigm.Controlflow.Effect.Interpreted (run, (=#-))
import Pandora.Paradigm.Inventory.Some.Store (Store (Store))
import Pandora.Paradigm.Inventory.Some.Optics (Lens, Convex, type (#=@), type (@>>>))
import Pandora.Paradigm.Primary.Algebraic.Product ((:*:) ((:*:)), type (<:*:>))
import Pandora.Paradigm.Primary.Algebraic ((>-|-<-|-))
import Pandora.Paradigm.Primary.Functor.Exactly (Exactly)
import Pandora.Paradigm.Primary.Functor.Tagged (Tagged)
import Pandora.Paradigm.Primary.Functor.Wye (Wye (Left, Right))
import Pandora.Paradigm.Schemes.TU (type (<:.>))
import Pandora.Paradigm.Schemes.T_U (T_U (T_U))
import Pandora.Paradigm.Schemes.P_Q_T (P_Q_T (P_Q_T))

data Segment a = Root a | Tail a

type Substructured segment source target = (Substructure segment source, Substance segment source ~ target)

class Substructure segment (structure :: * -> *) where
	type Substance segment structure :: * -> *
	substructure :: (Tagged segment <:.> structure) @>>> Substance segment structure

	sub :: (Covariant (->) (->) structure) => structure @>>> Substance segment structure
	sub = ((structure a -> TU Covariant Covariant (Tagged segment) structure a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (structure a
 -> TU Covariant Covariant (Tagged segment) structure a)
-> (Store
      (Substance segment structure a)
      (TU Covariant Covariant (Tagged segment) structure a)
    -> Store (Substance segment structure a) (structure a))
-> (structure a
    -> TU Covariant Covariant (Tagged segment) structure a)
   :*: (Store
          (Substance segment structure a)
          (TU Covariant Covariant (Tagged segment) structure a)
        -> Store (Substance segment structure a) (structure a))
forall s a. s -> a -> s :*: a
:*: (forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
forall (t :: (* -> *) -> * -> *) (u :: * -> *) a.
(Lowerable (->) t, Covariant (->) (->) u) =>
t u a -> u a
lower @(->) (TU Covariant Covariant (Tagged segment) structure a
 -> structure a)
-> Store
     (Substance segment structure a)
     (TU Covariant Covariant (Tagged segment) structure a)
-> Store (Substance segment structure a) (structure a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-)) ((structure a
  -> TU Covariant Covariant (Tagged segment) structure a)
 :*: (Store
        (Substance segment structure a)
        (TU Covariant Covariant (Tagged segment) structure a)
      -> Store (Substance segment structure a) (structure a)))
-> (TU Covariant Covariant (Tagged segment) structure a
    -> Store
         (Substance segment structure a)
         (TU Covariant Covariant (Tagged segment) structure a))
-> structure a
-> Store (Substance segment structure a) (structure a)
forall (m :: * -> * -> *) (p :: * -> * -> *) a b c d.
(Contravariant m m (Flip p d), Covariant m m (p b),
 Interpreted m (Flip p d)) =>
(m a b :*: m c d) -> m (p b c) (p a d)
>-|-<-|-) (Primary
   (P_Q_T
      (->)
      Store
      (Substance segment structure)
      (TU Covariant Covariant (Tagged segment) structure a))
   a
 -> Primary
      (P_Q_T (->) Store (Substance segment structure) (structure a)) a)
-> ((->)
    < P_Q_T
        (->)
        Store
        (Substance segment structure)
        (TU Covariant Covariant (Tagged segment) structure a)
        a)
   < P_Q_T (->) Store (Substance segment structure) (structure a) 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
=#- Substructure segment structure =>
(Tagged segment <:.> structure) @>>> Substance segment structure
forall k (segment :: k) (structure :: * -> *).
Substructure segment structure =>
(Tagged segment <:.> structure) @>>> Substance segment structure
substructure @segment @structure

-- TODO: generalize `available` and then rename to `singleton`
-- The main problem is that we should handle (Maybe target -> sourse)
-- For Convex Lens: we can ignore Exactly cause we can wrap/unwrap its value
-- For Obscure Lens: if we got nothing -> nothing should change
--only :: forall segment structure element . (Covariant (->) (->) structure, Substructured segment structure Exactly Exactly) => Convex Lens (structure element) element
--only = inner . ((sub @segment) :: Convex Lens (structure element) (Exactly element)) where

--	inner :: Convex Lens (Exactly element) element
--	inner = P_Q_T <-- \x -> Store <--- x :*: identity

instance (Covariant (->) (->) t, Covariant (->) (->) u) => Substructure Left (t <:*:> u) where
	type Substance Left (t <:*:> u) = t
	substructure :: Lens
  (Substance 'Left (t <:*:> u))
  ((<:.>) (Tagged 'Left) (t <:*:> u) a)
  a
substructure = ((<:.>) (Tagged 'Left) (t <:*:> u) a
 -> Store (t a) ((<:.>) (Tagged 'Left) (t <:*:> u) a))
-> P_Q_T (->) Store t ((<:.>) (Tagged 'Left) (t <:*:> u) 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 (((<:.>) (Tagged 'Left) (t <:*:> u) a
  -> Store (t a) ((<:.>) (Tagged 'Left) (t <:*:> u) a))
 -> P_Q_T (->) Store t ((<:.>) (Tagged 'Left) (t <:*:> u) a) a)
-> ((<:.>) (Tagged 'Left) (t <:*:> u) a
    -> Store (t a) ((<:.>) (Tagged 'Left) (t <:*:> u) a))
-> P_Q_T (->) Store t ((<:.>) (Tagged 'Left) (t <:*:> u) a) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(<:.>) (Tagged 'Left) (t <:*:> u) a
x -> case T_U Covariant Covariant (:*:) t u a -> t a :*: u a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (T_U Covariant Covariant (:*:) t u a -> t a :*: u a)
-> T_U Covariant Covariant (:*:) t u a -> t a :*: u a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:.>) (Tagged 'Left) (t <:*:> u) a
-> T_U Covariant Covariant (:*:) t u a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged 'Left) (t <:*:> u) a
x of
		t a
ls :*: u a
rs -> (((:*:) (t a) :. (->) (t a)) > (<:.>) (Tagged 'Left) (t <:*:> u) a)
-> Store (t a) ((<:.>) (Tagged 'Left) (t <:*:> u) a)
forall s a. (((:*:) s :. (->) s) > a) -> Store s a
Store ((((:*:) (t a) :. (->) (t a))
  > (<:.>) (Tagged 'Left) (t <:*:> u) a)
 -> Store (t a) ((<:.>) (Tagged 'Left) (t <:*:> u) a))
-> (((:*:) (t a) :. (->) (t a))
    > (<:.>) (Tagged 'Left) (t <:*:> u) a)
-> Store (t a) ((<:.>) (Tagged 'Left) (t <:*:> u) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- t a
ls t a
-> (t a -> (<:.>) (Tagged 'Left) (t <:*:> u) a)
-> ((:*:) (t a) :. (->) (t a))
   > (<:.>) (Tagged 'Left) (t <:*:> u) a
forall s a. s -> a -> s :*: a
:*: T_U Covariant Covariant (:*:) t u a
-> (<:.>) (Tagged 'Left) (t <:*:> u) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (T_U Covariant Covariant (:*:) t u a
 -> (<:.>) (Tagged 'Left) (t <:*:> u) a)
-> (t a -> T_U Covariant Covariant (:*:) t u a)
-> t a
-> (<:.>) (Tagged 'Left) (t <:*:> u) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((t a :*: u a) -> T_U Covariant Covariant (:*:) t u a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((t a :*: u a) -> T_U Covariant Covariant (:*:) t u a)
-> (t a -> t a :*: u a)
-> t a
-> T_U Covariant Covariant (:*:) t u a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (t a -> u a -> t a :*: u a
forall s a. s -> a -> s :*: a
:*: u a
rs))

instance (Covariant (->) (->) t, Covariant (->) (->) u) => Substructure Right (t <:*:> u) where
	type Substance Right (t <:*:> u) = u
	substructure :: Lens
  (Substance 'Right (t <:*:> u))
  ((<:.>) (Tagged 'Right) (t <:*:> u) a)
  a
substructure = ((<:.>) (Tagged 'Right) (t <:*:> u) a
 -> Store (u a) ((<:.>) (Tagged 'Right) (t <:*:> u) a))
-> P_Q_T (->) Store u ((<:.>) (Tagged 'Right) (t <:*:> u) 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 (((<:.>) (Tagged 'Right) (t <:*:> u) a
  -> Store (u a) ((<:.>) (Tagged 'Right) (t <:*:> u) a))
 -> P_Q_T (->) Store u ((<:.>) (Tagged 'Right) (t <:*:> u) a) a)
-> ((<:.>) (Tagged 'Right) (t <:*:> u) a
    -> Store (u a) ((<:.>) (Tagged 'Right) (t <:*:> u) a))
-> P_Q_T (->) Store u ((<:.>) (Tagged 'Right) (t <:*:> u) a) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(<:.>) (Tagged 'Right) (t <:*:> u) a
x -> case T_U Covariant Covariant (:*:) t u a -> t a :*: u a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (T_U Covariant Covariant (:*:) t u a -> t a :*: u a)
-> T_U Covariant Covariant (:*:) t u a -> t a :*: u a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:.>) (Tagged 'Right) (t <:*:> u) a
-> T_U Covariant Covariant (:*:) t u a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged 'Right) (t <:*:> u) a
x of
		t a
ls :*: u a
rs -> (((:*:) (u a) :. (->) (u a))
 > (<:.>) (Tagged 'Right) (t <:*:> u) a)
-> Store (u a) ((<:.>) (Tagged 'Right) (t <:*:> u) a)
forall s a. (((:*:) s :. (->) s) > a) -> Store s a
Store ((((:*:) (u a) :. (->) (u a))
  > (<:.>) (Tagged 'Right) (t <:*:> u) a)
 -> Store (u a) ((<:.>) (Tagged 'Right) (t <:*:> u) a))
-> (((:*:) (u a) :. (->) (u a))
    > (<:.>) (Tagged 'Right) (t <:*:> u) a)
-> Store (u a) ((<:.>) (Tagged 'Right) (t <:*:> u) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- u a
rs u a
-> (u a -> (<:.>) (Tagged 'Right) (t <:*:> u) a)
-> ((:*:) (u a) :. (->) (u a))
   > (<:.>) (Tagged 'Right) (t <:*:> u) a
forall s a. s -> a -> s :*: a
:*: T_U Covariant Covariant (:*:) t u a
-> (<:.>) (Tagged 'Right) (t <:*:> u) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (T_U Covariant Covariant (:*:) t u a
 -> (<:.>) (Tagged 'Right) (t <:*:> u) a)
-> (u a -> T_U Covariant Covariant (:*:) t u a)
-> u a
-> (<:.>) (Tagged 'Right) (t <:*:> u) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((t a :*: u a) -> T_U Covariant Covariant (:*:) t u a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((t a :*: u a) -> T_U Covariant Covariant (:*:) t u a)
-> (u a -> t a :*: u a)
-> u a
-> T_U Covariant Covariant (:*:) t u a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (t a
ls t a -> u a -> t a :*: u a
forall s a. s -> a -> s :*: a
:*:))