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

module Pandora.Paradigm.Structure.Ability.Substructure where

import Pandora.Core.Functor (type (:=))
import Pandora.Pattern.Functor.Covariant (Covariant ((-<$>-)))
import Pandora.Pattern.Functor.Divariant ((>->))
import Pandora.Pattern.Transformer.Liftable (lift)
import Pandora.Pattern.Transformer.Lowerable (lower)
import Pandora.Paradigm.Controlflow.Effect.Interpreted ((||=))
import Pandora.Paradigm.Inventory.Optics (type (#=@))
import Pandora.Paradigm.Primary.Functor.Tagged (Tagged)
import Pandora.Paradigm.Schemes.TU (type (<:.>))

data Segment a = Root a | Tail a

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

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

	sub :: (Covariant structure (->) (->)) => structure #=@ Substance segment structure := Available segment structure
	sub = structure a -> TU Covariant Covariant (Tagged segment) structure a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u (->) (->)) =>
u ~> t u
lift (structure a
 -> TU Covariant Covariant (Tagged segment) structure a)
-> (Store
      (Available segment structure (Substance segment structure a))
      (TU Covariant Covariant (Tagged segment) structure a)
    -> Store
         (Available segment structure (Substance segment structure a))
         (structure a))
-> (TU Covariant Covariant (Tagged segment) structure a
    -> Store
         (Available segment structure (Substance segment structure a))
         (TU Covariant Covariant (Tagged segment) structure a))
-> structure a
-> Store
     (Available segment structure (Substance segment structure a))
     (structure a)
forall (v :: * -> * -> *) (left :: * -> * -> *)
       (right :: * -> * -> *) (target :: * -> * -> *) a b c d.
Divariant v left right target =>
left a b -> right c d -> target (v b c) (v a d)
>-> (TU Covariant Covariant (Tagged segment) structure a -> structure a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Lowerable t, Covariant u (->) (->)) =>
t u ~> u
lower (TU Covariant Covariant (Tagged segment) structure a
 -> structure a)
-> Store
     (Available segment structure (Substance segment structure a))
     (TU Covariant Covariant (Tagged segment) structure a)
-> Store
     (Available segment structure (Substance segment structure a))
     (structure a)
forall (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant t source target =>
source a b -> target (t a) (t b)
-<$>-) (Primary
   (P_Q_T
      (->)
      Store
      (Available segment structure)
      (TU Covariant Covariant (Tagged segment) structure a))
   (Substance segment structure a)
 -> Primary
      (P_Q_T (->) Store (Available segment structure) (structure a))
      (Substance segment structure a))
-> P_Q_T
     (->)
     Store
     (Available segment structure)
     (TU Covariant Covariant (Tagged segment) structure a)
     (Substance segment structure a)
-> P_Q_T
     (->)
     Store
     (Available segment structure)
     (structure a)
     (Substance segment structure a)
forall (t :: * -> *) (u :: * -> *) a b.
(Interpreted t, Interpreted u) =>
(Primary t a -> Primary u b) -> t a -> u b
||= Substructure segment structure =>
((Tagged segment <:.> structure) #=@ Substance segment structure)
:= Available segment structure
forall k (segment :: k) (structure :: * -> *).
Substructure segment structure =>
((Tagged segment <:.> structure) #=@ Substance segment structure)
:= Available segment structure
substructure @segment @structure