{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE UndecidableInstances #-}

module Pandora.Paradigm.Structure.Ability.Substructure where

import Pandora.Pattern.Category ((.), ($))
import Pandora.Pattern.Functor.Covariant (Covariant ((<$>)))
import Pandora.Pattern.Functor.Extractable (extract)
import Pandora.Pattern.Functor.Pointable (point)
import Pandora.Pattern.Functor.Divariant ((>->))
import Pandora.Pattern.Transformer.Liftable (lift)
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run, unite)
import Pandora.Paradigm.Inventory.Optics (type (:~.), (|>))
import Pandora.Paradigm.Primary.Functor.Tagged (Tagged)
import Pandora.Paradigm.Schemes.TU (type (<:.>))

class Substructure f t where
	type Substructural (f :: k) (t :: * -> *) :: * -> *
	substructure :: Tagged f <:.> t :~. Substructural f t

	sub :: Covariant t => t :~. Substructural f t
	sub t a
x = t a <:= Tagged f
forall (t :: * -> *) a. Extractable t => a <:= t
extract (t a <:= Tagged f)
-> (TU Covariant Covariant (Tagged f) t a -> Tagged f (t a))
-> TU Covariant Covariant (Tagged f) t a
-> t a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant (Tagged f) t a -> Tagged f (t a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (TU Covariant Covariant (Tagged f) t a -> t a)
-> Store
     (Substructural f t a) (TU Covariant Covariant (Tagged f) t a)
-> Store (Substructural f t a) (t a)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> Lens (TU Covariant Covariant (Tagged f) t a) (Substructural f t a)
forall k (f :: k) (t :: * -> *).
Substructure f t =>
(Tagged f <:.> t) :~. Substructural f t
substructure @f (t a -> TU Covariant Covariant (Tagged f) t a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift t a
x)

data Segment a = Tail a

data (|>) (i :: * -> k) (j :: * -> k') a

instance (Covariant t, Covariant (Substructural i t), Substructure i t, Substructure j (Substructural i t)) => Substructure (i |> j) t where
	type Substructural (i |> j) t = Substructural j (Substructural i t)
	substructure :: Lens ((<:.>) (Tagged (i |> j)) t a) (Substructural (i |> j) t a)
substructure = t a <:= Tagged (i |> j)
forall (t :: * -> *) a. Extractable t => a <:= t
extract (t a <:= Tagged (i |> j))
-> ((<:.>) (Tagged (i |> j)) t a -> Tagged (i |> j) (t a))
-> (<:.>) (Tagged (i |> j)) t a
-> t a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged (i |> j)) t a -> Tagged (i |> j) (t a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run ((<:.>) (Tagged (i |> j)) t a -> t a)
-> (Store (Substructural j (Substructural i t) a) (t a)
    -> Store
         (Substructural j (Substructural i t) a)
         ((<:.>) (Tagged (i |> j)) t a))
-> (t a -> Store (Substructural j (Substructural i t) a) (t a))
-> (<:.>) (Tagged (i |> j)) t a
-> Store
     (Substructural j (Substructural i t) a)
     ((<:.>) (Tagged (i |> j)) t a)
forall (v :: * -> * -> *) a b c d.
Divariant v =>
(a -> b) -> (c -> d) -> v b c -> v a d
>-> (Tagged (i |> j) (t a) -> (<:.>) (Tagged (i |> j)) t a
forall (t :: * -> *) a. Interpreted t => Primary t a -> t a
unite (Tagged (i |> j) (t a) -> (<:.>) (Tagged (i |> j)) t a)
-> (t a -> Tagged (i |> j) (t a))
-> t a
-> (<:.>) (Tagged (i |> j)) t a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. t a -> Tagged (i |> j) (t a)
forall (t :: * -> *) a. Pointable t => a :=> t
point (t a -> (<:.>) (Tagged (i |> j)) t a)
-> Store (Substructural j (Substructural i t) a) (t a)
-> Store
     (Substructural j (Substructural i t) a)
     ((<:.>) (Tagged (i |> j)) t a)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$>) ((t a -> Store (Substructural j (Substructural i t) a) (t a))
 -> (<:.>) (Tagged (i |> j)) t a
 -> Store
      (Substructural j (Substructural i t) a)
      ((<:.>) (Tagged (i |> j)) t a))
-> (t a -> Store (Substructural j (Substructural i t) a) (t a))
-> (<:.>) (Tagged (i |> j)) t a
-> Store
     (Substructural j (Substructural i t) a)
     ((<:.>) (Tagged (i |> j)) t a)
forall (m :: * -> * -> *). Category m => m ~~> m
$ forall k (f :: k) (t :: * -> *).
(Substructure f t, Covariant t) =>
t :~. Substructural f t
forall (t :: * -> *).
(Substructure i t, Covariant t) =>
t :~. Substructural i t
sub @i (t a -> Store (Substructural i t a) (t a))
-> Lens
     (Substructural i t a) (Substructural j (Substructural i t) a)
-> t a
-> Store (Substructural j (Substructural i t) a) (t a)
forall src tgt new. Lens src tgt -> Lens tgt new -> Lens src new
|> forall k (f :: k) (t :: * -> *).
(Substructure f t, Covariant t) =>
t :~. Substructural f t
forall (t :: * -> *).
(Substructure j t, Covariant t) =>
t :~. Substructural j t
sub @j

type Substructured i source target = (Substructure i source, Substructural i source ~ target)