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

module Pandora.Paradigm.Structure.Ability.Substructure where

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 (<:.>))

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 -> TU Covariant Covariant (Tagged f) t a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (t a -> TU Covariant Covariant (Tagged f) t a)
-> (Store
      (Substructural f t a) (TU Covariant Covariant (Tagged f) t a)
    -> Store (Substructural f t a) (t a))
-> (TU Covariant Covariant (Tagged f) t a
    -> Store
         (Substructural f t a) (TU Covariant Covariant (Tagged f) t a))
-> t a
-> Store (Substructural f t a) (t a)
forall (v :: * -> * -> *) a b c d.
Divariant v =>
(a -> b) -> (c -> d) -> v b c -> v a d
>-> (TU Covariant Covariant (Tagged f) t a -> t a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Lowerable t, Covariant u) =>
t u ~> u
lower (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
<$>) (Primary
   (PQ_ (->) Store (TU Covariant Covariant (Tagged f) t a))
   (Substructural f t a)
 -> Primary (PQ_ (->) Store (t a)) (Substructural f t a))
-> PQ_
     (->)
     Store
     (TU Covariant Covariant (Tagged f) t a)
     (Substructural f t a)
-> PQ_ (->) Store (t a) (Substructural f t a)
forall (t :: * -> *) (u :: * -> *) a b.
(Interpreted t, Interpreted u) =>
(Primary t a -> Primary u b) -> t a -> u b
||= Substructure f t => (Tagged f <:.> t) :~. Substructural f t
forall k (f :: k) (t :: * -> *).
Substructure f t =>
(Tagged f <:.> t) :~. Substructural f t
substructure @f @t

data Segment a = Root a | Tail a

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