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

import Pandora.Core.Functor (type (>), type (<), type (:.), type (:::))
import Pandora.Core.Interpreted (run, unite, (<~), (=#-))
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.Maybe (Maybe)
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.Modification.Nonempty (Nonempty)
import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Substance, substructure, sub), Segment (Root, Rest))

-- TODO: Use Slidable superclass with Slides associated type family
class Zippable (structure :: * -> *) where
	type Breadcrumbs structure :: * -> *
	fasten :: structure e -> Maybe > Zipper structure e
	unfasten :: Zipper structure e -> Nonempty structure e

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

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)