{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeSynonymInstances #-}
module Pandora.Paradigm.Structure.Interface.Zipper where

import Pandora.Core.Functor (type (>), type (<), type (:.), type (:::))
import Pandora.Core.Impliable (Impliable (Arguments, imply))
import Pandora.Pattern.Morphism.Flip (Flip (Flip))
import Pandora.Pattern.Morphism.Straight (Straight (Straight))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category ((<--), (<---), (<----), (<------))
import Pandora.Pattern.Kernel (constant)
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-), (<-|--), (<-|---)))
import Pandora.Pattern.Functor.Traversable (Traversable ((<<-), (<<---)))
import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (mult))
import Pandora.Pattern.Functor.Monoidal (Monoidal (unit))
import Pandora.Pattern.Transformer.Liftable (lift)
import Pandora.Pattern.Transformer.Lowerable (lower)
import Pandora.Paradigm.Algebraic.Exponential (type (<--), type (-->), (%))
import Pandora.Paradigm.Algebraic.Product ((:*:) ((:*:)), type (<:*:>), (<:*:>))
import Pandora.Paradigm.Algebraic ((<-*-), (<-*--), (<-*---), (.-*-), extract, point)
import Pandora.Paradigm.Primary.Functor.Exactly (Exactly (Exactly))
import Pandora.Paradigm.Primary.Functor.Tagged (Tagged)
import Pandora.Paradigm.Schemes.TU (TU (TU), type (<:.>))
import Pandora.Paradigm.Schemes.T_U (T_U (T_U), type (<:.:>))
import Pandora.Paradigm.Schemes.P_Q_T (P_Q_T (P_Q_T))
import Pandora.Paradigm.Inventory.Some.Store (Store (Store))
import Pandora.Paradigm.Structure.Ability.Morphable (Morphable, Morph (Rotate))
import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Substance, substructure, sub), Segment (Root, Rest))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run, unite, (<~), (=#-))

class Zippable (structure :: * -> *) where
	type Breadcrumbs structure :: * -> *

type Zipper (structure :: * -> *) = Tagged (Zippable structure) <:.> (Exactly <:*:> Breadcrumbs structure)

type Breadcrumbed structure t = (Zippable structure, Breadcrumbs structure ~ t)

instance {-# OVERLAPS #-} Semimonoidal (<--) (:*:) (:*:) t
	=> Semimonoidal (<--) (:*:) (:*:) (Exactly <:*:> t) where
	mult :: ((<:*:>) Exactly t a :*: (<:*:>) Exactly t b)
<-- (<:*:>) Exactly t (a :*: b)
mult = ((<:*:>) Exactly t (a :*: b)
 -> (<:*:>) Exactly t a :*: (<:*:>) Exactly t b)
-> ((<:*:>) Exactly t a :*: (<:*:>) Exactly t b)
   <-- (<:*:>) Exactly t (a :*: b)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (((<:*:>) Exactly t (a :*: b)
  -> (<:*:>) Exactly t a :*: (<:*:>) Exactly t b)
 -> ((<:*:>) Exactly t a :*: (<:*:>) Exactly t b)
    <-- (<:*:>) Exactly t (a :*: b))
-> ((<:*:>) Exactly t (a :*: b)
    -> (<:*:>) Exactly t a :*: (<:*:>) Exactly t b)
-> ((<:*:>) Exactly t a :*: (<:*:>) Exactly t b)
   <-- (<:*:>) Exactly t (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(T_U (Exactly (a
x :*: b
y) :*: t (a :*: b)
xys)) ->
		let t a
xs :*: t b
ys = forall k (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k).
Semimonoidal p source target t =>
p (source (t a) (t b)) (t (target a b))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Semimonoidal (<--) source target t =>
source (t a) (t b) <-- t (target a b)
mult @(<--) ((t a :*: t b) <-- t (a :*: b)) -> t (a :*: b) -> t a :*: t b
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~ t (a :*: b)
xys in
			(a -> Exactly a
forall a. a -> Exactly a
Exactly a
x Exactly a -> t a -> (<:*:>) Exactly t a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) > a
<:*:> t a
xs) (<:*:>) Exactly t a
-> (<:*:>) Exactly t b
-> (<:*:>) Exactly t a :*: (<:*:>) Exactly t b
forall s a. s -> a -> s :*: a
:*: (b -> Exactly b
forall a. a -> Exactly a
Exactly b
y Exactly b -> t b -> (<:*:>) Exactly t b
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) > a
<:*:> t b
ys)

instance {-# OVERLAPS #-} Semimonoidal (<--) (:*:) (:*:) t => Monoidal (<--) (-->) (:*:) (:*:) (Exactly <:*:> t) where
	unit :: Proxy (:*:) -> (Unit (:*:) --> a) <-- (<:*:>) Exactly t a
unit Proxy (:*:)
_ = ((<:*:>) Exactly t a -> Straight (->) One a)
-> Flip (->) (Straight (->) One a) ((<:*:>) Exactly t a)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (((<:*:>) Exactly t a -> Straight (->) One a)
 -> Flip (->) (Straight (->) One a) ((<:*:>) Exactly t a))
-> ((<:*:>) Exactly t a -> Straight (->) One a)
-> Flip (->) (Straight (->) One a) ((<:*:>) Exactly t a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(T_U (Exactly a
x :*: t a
_)) -> (One -> a) -> Straight (->) One a
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (\One
_ -> a
x)

instance Covariant (->) (->) t => Substructure Root (Tagged (Zippable structure) <:.> (Exactly <:*:> t)) where
	type Substance Root (Tagged (Zippable structure) <:.> (Exactly <:*:> t)) = Exactly
	substructure :: Lens
  (Substance
     'Root (Tagged (Zippable structure) <:.> (Exactly <:*:> t)))
  ((<:.>)
     (Tagged 'Root)
     (Tagged (Zippable structure) <:.> (Exactly <:*:> t))
     a)
  a
substructure = ((<:.>)
   (Tagged 'Root)
   (Tagged (Zippable structure) <:.> (Exactly <:*:> t))
   a
 -> Store
      (Exactly a)
      ((<:.>)
         (Tagged 'Root)
         (Tagged (Zippable structure) <:.> (Exactly <:*:> t))
         a))
-> P_Q_T
     (->)
     Store
     Exactly
     ((<:.>)
        (Tagged 'Root)
        (Tagged (Zippable structure) <:.> (Exactly <:*:> t))
        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 'Root)
    (Tagged (Zippable structure) <:.> (Exactly <:*:> t))
    a
  -> Store
       (Exactly a)
       ((<:.>)
          (Tagged 'Root)
          (Tagged (Zippable structure) <:.> (Exactly <:*:> t))
          a))
 -> P_Q_T
      (->)
      Store
      Exactly
      ((<:.>)
         (Tagged 'Root)
         (Tagged (Zippable structure) <:.> (Exactly <:*:> t))
         a)
      a)
-> ((<:.>)
      (Tagged 'Root)
      (Tagged (Zippable structure) <:.> (Exactly <:*:> t))
      a
    -> Store
         (Exactly a)
         ((<:.>)
            (Tagged 'Root)
            (Tagged (Zippable structure) <:.> (Exactly <:*:> t))
            a))
-> P_Q_T
     (->)
     Store
     Exactly
     ((<:.>)
        (Tagged 'Root)
        (Tagged (Zippable structure) <:.> (Exactly <:*:> t))
        a)
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(<:.>)
  (Tagged 'Root)
  (Tagged (Zippable structure) <:.> (Exactly <:*:> t))
  a
source -> case TU
  Covariant
  Covariant
  (Tagged (Zippable structure))
  (Exactly <:*:> t)
  a
-> T_U Covariant Covariant (:*:) Exactly t a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (TU
   Covariant
   Covariant
   (Tagged (Zippable structure))
   (Exactly <:*:> t)
   a
 -> T_U Covariant Covariant (:*:) Exactly t a)
-> ((<:.>)
      (Tagged 'Root)
      (Tagged (Zippable structure) <:.> (Exactly <:*:> t))
      a
    -> TU
         Covariant
         Covariant
         (Tagged (Zippable structure))
         (Exactly <:*:> t)
         a)
-> (<:.>)
     (Tagged 'Root)
     (Tagged (Zippable structure) <:.> (Exactly <:*:> t))
     a
-> T_U Covariant Covariant (:*:) Exactly t a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<:.>)
  (Tagged 'Root)
  (Tagged (Zippable structure) <:.> (Exactly <:*:> t))
  a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable structure))
     (Exactly <:*:> t)
     a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower ((<:.>)
   (Tagged 'Root)
   (Tagged (Zippable structure) <:.> (Exactly <:*:> t))
   a
 -> T_U Covariant Covariant (:*:) Exactly t a)
-> (<:.>)
     (Tagged 'Root)
     (Tagged (Zippable structure) <:.> (Exactly <:*:> t))
     a
-> T_U Covariant Covariant (:*:) Exactly t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:.>)
  (Tagged 'Root)
  (Tagged (Zippable structure) <:.> (Exactly <:*:> t))
  a
source of
		T_U (Exactly a
x :*: t a
xs) -> (((:*:) (Exactly a) :. (->) (Exactly a))
 > (<:.>)
     (Tagged 'Root)
     (Tagged (Zippable structure) <:.> (Exactly <:*:> t))
     a)
-> Store
     (Exactly a)
     ((<:.>)
        (Tagged 'Root)
        (Tagged (Zippable structure) <:.> (Exactly <:*:> t))
        a)
forall s a. (((:*:) s :. (->) s) > a) -> Store s a
Store ((((:*:) (Exactly a) :. (->) (Exactly a))
  > (<:.>)
      (Tagged 'Root)
      (Tagged (Zippable structure) <:.> (Exactly <:*:> t))
      a)
 -> Store
      (Exactly a)
      ((<:.>)
         (Tagged 'Root)
         (Tagged (Zippable structure) <:.> (Exactly <:*:> t))
         a))
-> (((:*:) (Exactly a) :. (->) (Exactly a))
    > (<:.>)
        (Tagged 'Root)
        (Tagged (Zippable structure) <:.> (Exactly <:*:> t))
        a)
-> Store
     (Exactly a)
     ((<:.>)
        (Tagged 'Root)
        (Tagged (Zippable structure) <:.> (Exactly <:*:> t))
        a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- a -> Exactly a
forall a. a -> Exactly a
Exactly a
x Exactly a
-> (Exactly a
    -> (<:.>)
         (Tagged 'Root)
         (Tagged (Zippable structure) <:.> (Exactly <:*:> t))
         a)
-> ((:*:) (Exactly a) :. (->) (Exactly a))
   > (<:.>)
       (Tagged 'Root)
       (Tagged (Zippable structure) <:.> (Exactly <:*:> t))
       a
forall s a. s -> a -> s :*: a
:*: TU
  Covariant
  Covariant
  (Tagged (Zippable structure))
  (Exactly <:*:> t)
  a
-> (<:.>)
     (Tagged 'Root)
     (Tagged (Zippable structure) <:.> (Exactly <:*:> t))
     a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (TU
   Covariant
   Covariant
   (Tagged (Zippable structure))
   (Exactly <:*:> t)
   a
 -> (<:.>)
      (Tagged 'Root)
      (Tagged (Zippable structure) <:.> (Exactly <:*:> t))
      a)
-> (Exactly a
    -> TU
         Covariant
         Covariant
         (Tagged (Zippable structure))
         (Exactly <:*:> t)
         a)
-> Exactly a
-> (<:.>)
     (Tagged 'Root)
     (Tagged (Zippable structure) <:.> (Exactly <:*:> t))
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. T_U Covariant Covariant (:*:) Exactly t a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable structure))
     (Exactly <:*:> t)
     a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (T_U Covariant Covariant (:*:) Exactly t a
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable structure))
      (Exactly <:*:> t)
      a)
-> (Exactly a -> T_U Covariant Covariant (:*:) Exactly t a)
-> Exactly a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable structure))
     (Exactly <:*:> t)
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Exactly a -> t a -> T_U Covariant Covariant (:*:) Exactly t a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) > a
<:*:> t a
xs)

type family Fastenable structure rs where
	Fastenable structure (r ::: rs) = (Morphable < Rotate r < structure, Fastenable structure rs)
	Fastenable structure r = Morphable < Rotate r < structure