{-# LANGUAGE AllowAmbiguousTypes #-} module Pandora.Paradigm.Structure.Ability.Morphable where import Pandora.Core.Functor (type (:=), type (~>), type (:=:=>)) import Pandora.Pattern.Category ((.), (/)) import Pandora.Pattern.Functor.Extractable (extract) import Pandora.Pattern.Object.Chain (Chain ((<=>))) import Pandora.Pattern.Object.Setoid (Setoid) import Pandora.Paradigm.Primary.Functor (Comparison) import Pandora.Paradigm.Primary.Functor.Convergence (Convergence (Convergence)) import Pandora.Paradigm.Primary.Functor.Identity (Identity (Identity)) import Pandora.Paradigm.Primary.Functor.Predicate (Predicate, equate) import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)), type (:*:)) import Pandora.Paradigm.Primary.Functor.Tagged (Tagged (Tag)) import Pandora.Paradigm.Controlflow.Effect.Interpreted (run) import Pandora.Paradigm.Schemes.TU (TU (TU), type (<:.>)) import Pandora.Paradigm.Schemes.T_U (T_U (T_U), type (<:.:>)) class Morphable f t | f t -> t where type Morphing (f :: k) (t :: * -> *) :: * -> * morphing :: Tagged f <:.> t ~> Morphing f t morph :: forall f t . Morphable f t => t ~> Morphing f t morph :: t ~> Morphing f t morph = (<:.>) (Tagged f) t a -> Morphing f t a forall k (f :: k) (t :: * -> *). Morphable f t => (Tagged f <:.> t) ~> Morphing f t morphing ((<:.>) (Tagged f) t a -> Morphing f t a) -> (t a -> (<:.>) (Tagged f) t a) -> t a -> Morphing f t a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . ((Tagged f :. t) := a) -> (<:.>) (Tagged f) t a forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (((Tagged f :. t) := a) -> (<:.>) (Tagged f) t a) -> (t a -> (Tagged f :. t) := a) -> t a -> (<:.>) (Tagged f) t a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . forall a. a -> Tagged f a forall k (tag :: k) a. a -> Tagged tag a Tag @f premorph :: Morphable f t => Tagged f <:.> t ~> t premorph :: (Tagged f <:.> t) ~> t premorph = t a <:= Tagged f forall (t :: * -> *) a. Extractable t => a <:= t extract (t a <:= Tagged f) -> (TU Covariant Covariant (Tagged f) t a -> Tagged f (t a)) -> TU Covariant Covariant (Tagged f) t a -> t a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . TU Covariant Covariant (Tagged f) t a -> Tagged f (t a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run data Walk a = Preorder a | Inorder a | Postorder a | Levelorder a data Morph a = Rotate a | Into a | Insert a | Push a | Pop a | Delete a | Find a | Lookup a | Element a data Occurrence a = All a | First a rotate :: forall f t . Morphable (Rotate f) t => t ~> Morphing (Rotate f) t rotate :: t ~> Morphing ('Rotate f) t rotate = (<:.>) (Tagged ('Rotate f)) t a -> Morphing ('Rotate f) t a forall k (f :: k) (t :: * -> *). Morphable f t => (Tagged f <:.> t) ~> Morphing f t morphing ((<:.>) (Tagged ('Rotate f)) t a -> Morphing ('Rotate f) t a) -> (t a -> (<:.>) (Tagged ('Rotate f)) t a) -> t a -> Morphing ('Rotate f) t a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . ((Tagged ('Rotate f) :. t) := a) -> (<:.>) (Tagged ('Rotate f)) t a forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (((Tagged ('Rotate f) :. t) := a) -> (<:.>) (Tagged ('Rotate f)) t a) -> (t a -> (Tagged ('Rotate f) :. t) := a) -> t a -> (<:.>) (Tagged ('Rotate f)) t a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . forall a. a -> Tagged ('Rotate f) a forall k (tag :: k) a. a -> Tagged tag a Tag @(Rotate f) into :: forall f t . Morphable (Into f) t => t ~> Morphing (Into f) t into :: t ~> Morphing ('Into f) t into = (<:.>) (Tagged ('Into f)) t a -> Morphing ('Into f) t a forall k (f :: k) (t :: * -> *). Morphable f t => (Tagged f <:.> t) ~> Morphing f t morphing ((<:.>) (Tagged ('Into f)) t a -> Morphing ('Into f) t a) -> (t a -> (<:.>) (Tagged ('Into f)) t a) -> t a -> Morphing ('Into f) t a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . ((Tagged ('Into f) :. t) := a) -> (<:.>) (Tagged ('Into f)) t a forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (((Tagged ('Into f) :. t) := a) -> (<:.>) (Tagged ('Into f)) t a) -> (t a -> (Tagged ('Into f) :. t) := a) -> t a -> (<:.>) (Tagged ('Into f)) t a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . forall a. a -> Tagged ('Into f) a forall k (tag :: k) a. a -> Tagged tag a Tag @(Into f) insert :: forall f t a . (Morphable (Insert f) t, Morphing (Insert f) t ~ (Identity <:.:> t := (->))) => a :=:=> t insert :: a :=:=> t insert a new t a xs = T_U Covariant Covariant (->) Identity t a -> Identity a -> t a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (T_U Covariant Covariant (->) Identity t a -> Identity a -> t a) -> T_U Covariant Covariant (->) Identity t a -> Identity a -> t a forall (m :: * -> * -> *). Category m => m ~~> m / t a -> Morphing ('Insert f) t a forall k (f :: k) (t :: * -> *). Morphable f t => t ~> Morphing f t morph @(Insert f) t a xs (Identity a -> t a) -> Identity a -> t a forall (m :: * -> * -> *). Category m => m ~~> m / a -> Identity a forall a. a -> Identity a Identity a new item :: forall f t a . (Morphable f t, Morphing f t ~ (Identity <:.:> t := (->))) => a :=:=> t item :: a :=:=> t item a new t a xs = T_U Covariant Covariant (->) Identity t a -> Identity a -> t a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (T_U Covariant Covariant (->) Identity t a -> Identity a -> t a) -> T_U Covariant Covariant (->) Identity t a -> Identity a -> t a forall (m :: * -> * -> *). Category m => m ~~> m / t a -> Morphing f t a forall k (f :: k) (t :: * -> *). Morphable f t => t ~> Morphing f t morph @f t a xs (Identity a -> t a) -> Identity a -> t a forall (m :: * -> * -> *). Category m => m ~~> m / a -> Identity a forall a. a -> Identity a Identity a new collate :: forall f t a . (Chain a, Morphable f t, Morphing f t ~ ((Identity <:.:> Comparison := (:*:)) <:.:> t := (->))) => a :=:=> t collate :: a :=:=> t collate a new t a xs = T_U Covariant Covariant (->) ((Identity <:.:> Comparison) := (:*:)) t a -> T_U Covariant Covariant (:*:) Identity Comparison a -> t a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (T_U Covariant Covariant (->) ((Identity <:.:> Comparison) := (:*:)) t a -> T_U Covariant Covariant (:*:) Identity Comparison a -> t a) -> T_U Covariant Covariant (->) ((Identity <:.:> Comparison) := (:*:)) t a -> T_U Covariant Covariant (:*:) Identity Comparison a -> t a forall (m :: * -> * -> *). Category m => m ~~> m / t a -> Morphing f t a forall k (f :: k) (t :: * -> *). Morphable f t => t ~> Morphing f t morph @f t a xs (T_U Covariant Covariant (:*:) Identity Comparison a -> t a) -> T_U Covariant Covariant (:*:) Identity Comparison a -> t a forall (m :: * -> * -> *). Category m => m ~~> m / Product (Identity a) (Convergence Ordering a) -> T_U Covariant Covariant (:*:) Identity Comparison a forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *) (t :: k -> k) (u :: k -> k) (a :: k). p (t a) (u a) -> T_U ct cu p t u a T_U (a -> Identity a forall a. a -> Identity a Identity a new Identity a -> Convergence Ordering a -> Product (Identity a) (Convergence Ordering a) forall s a. s -> a -> Product s a :*: (a -> a -> Ordering) -> Convergence Ordering a forall r a. (a -> a -> r) -> Convergence r a Convergence a -> a -> Ordering forall a. Chain a => a -> a -> Ordering (<=>)) delete :: forall f t a . (Setoid a, Morphable (Delete f) t, Morphing (Delete f) t ~ (Predicate <:.:> t := (->))) => a :=:=> t delete :: a :=:=> t delete a x t a xs = T_U Covariant Covariant (->) Predicate t a -> Predicate a -> t a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (T_U Covariant Covariant (->) Predicate t a -> Predicate a -> t a) -> T_U Covariant Covariant (->) Predicate t a -> Predicate a -> t a forall (m :: * -> * -> *). Category m => m ~~> m / t a -> Morphing ('Delete f) t a forall k (f :: k) (t :: * -> *). Morphable f t => t ~> Morphing f t morph @(Delete f) t a xs (Predicate a -> t a) -> Predicate a -> t a forall (m :: * -> * -> *). Category m => m ~~> m / a :=> Predicate forall a. Setoid a => a :=> Predicate equate a x filter :: forall f t a . (Morphable (Delete f) t, Morphing (Delete f) t ~ (Predicate <:.:> t := (->))) => Predicate a -> t a -> t a filter :: Predicate a -> t a -> t a filter Predicate a p t a xs = T_U Covariant Covariant (->) Predicate t a -> Predicate a -> t a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (T_U Covariant Covariant (->) Predicate t a -> Predicate a -> t a) -> T_U Covariant Covariant (->) Predicate t a -> Predicate a -> t a forall (m :: * -> * -> *). Category m => m ~~> m / t a -> Morphing ('Delete f) t a forall k (f :: k) (t :: * -> *). Morphable f t => t ~> Morphing f t morph @(Delete f) t a xs (Predicate a -> t a) -> Predicate a -> t a forall (m :: * -> * -> *). Category m => m ~~> m / Predicate a p find :: forall f t u a . (Morphable (Find f) t, Morphing (Find f) t ~ (Predicate <:.:> u := (->))) => Predicate a -> t a -> u a find :: Predicate a -> t a -> u a find Predicate a p t a xs = T_U Covariant Covariant (->) Predicate u a -> Predicate a -> u a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (T_U Covariant Covariant (->) Predicate u a -> Predicate a -> u a) -> T_U Covariant Covariant (->) Predicate u a -> Predicate a -> u a forall (m :: * -> * -> *). Category m => m ~~> m / t a -> Morphing ('Find f) t a forall k (f :: k) (t :: * -> *). Morphable f t => t ~> Morphing f t morph @(Find f) t a xs (Predicate a -> u a) -> Predicate a -> u a forall (m :: * -> * -> *). Category m => m ~~> m / Predicate a p