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