{-# 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