{-# OPTIONS_GHC -fno-warn-orphans #-}
module Pandora.Paradigm.Structure.Some.Rose where

import Pandora.Core.Functor (type (:.), type (>))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category ((<--), (<---), (<----), (<-----))
import Pandora.Pattern.Kernel (constant)
import Pandora.Pattern.Functor.Contravariant ((>-|--))
import Pandora.Pattern.Functor.Bindable (Bindable ((=<<)))
import Pandora.Pattern.Transformer.Liftable (lift)
import Pandora.Pattern.Transformer.Lowerable (lower)
import Pandora.Pattern.Object.Setoid (Setoid ((==), (!=), (?==)))
import Pandora.Paradigm.Primary.Algebraic.Product ((:*:) ((:*:)), attached)
import Pandora.Paradigm.Primary.Algebraic.Exponential ((%))
import Pandora.Paradigm.Primary.Algebraic (extract)
import Pandora.Paradigm.Primary.Object.Boolean (Boolean (True))
import Pandora.Paradigm.Primary.Algebraic.Product ((:*:) ((:*:)), attached)
import Pandora.Paradigm.Primary.Algebraic.Exponential ((%))
import Pandora.Paradigm.Primary.Algebraic (extract)
import Pandora.Paradigm.Primary.Object.Boolean (Boolean (True))
import Pandora.Paradigm.Primary.Functor.Exactly (Exactly (Exactly))
import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Just, Nothing))
import Pandora.Paradigm.Primary.Functor.Predicate (equate)
import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct), deconstruct)
import Pandora.Paradigm.Schemes (TU (TU), P_Q_T (P_Q_T), type (<:.>))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run)
import Pandora.Paradigm.Inventory.Some.Store (Store (Store))
import Pandora.Paradigm.Structure.Ability.Morphable (Morphable (Morphing, morphing), Morph (Lookup, Element, Key), premorph, find)
import Pandora.Paradigm.Structure.Ability.Nonempty (Nonempty)
import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Substance, substructure), Segment (Root, Tail))
import Pandora.Paradigm.Structure.Modification.Prefixed (Prefixed)
import Pandora.Paradigm.Structure.Some.List (List)

type Rose = Maybe <:.> Construction List

-- FIXME: If we want to remove root node, we ruin the whole tree
--instance Substructure Root Rose where
--	type Available Root Rose = Maybe
--	type Substance Root Rose = Exactly
--	substructure = P_Q_T <-- \rose -> case run # lower rose of
--		Nothing -> Store <--- Nothing :*: TU . Tag . TU . ((Construct % empty) . extract <-|-)
--		Just nonempty_rose -> Store <--- Just (Exactly # extract nonempty_rose) :*: \case
--			Just (Exactly new) -> lift . TU . Just . Construct new <-- deconstruct nonempty_rose
--			Nothing -> lift empty

--instance Substructure Just Rose where
--	type Available Just Rose = Exactly
--	type Substance Just Rose = List <:.> Construction List
--	substructure = P_Q_T <-- \rose -> case run . extract . run # rose of
--		Nothing -> Store <--- Exactly empty :*: constant (lift empty)
--		Just (Construct x xs) -> Store <--- Exactly (TU xs) :*: lift . lift . Construct x . run . extract

--------------------------------------- Non-empty rose tree ----------------------------------------

type instance Nonempty Rose = Construction List

instance Substructure Root (Construction List) where
	type Substance Root (Construction List) = Exactly
	--substructure = P_Q_T <-- \rose -> Store <--- Exactly (Exactly <-- extract (lower rose)) :*: lift . (Construct % deconstruct (lower rose)) . extract . extract

instance Substructure Tail (Construction List) where
	type Substance Tail (Construction List) = List <:.> Construction List
	--substructure = P_Q_T <-- \rose -> case extract <-- run rose of
	--	Construct x xs -> Store <--- Exactly (TU xs) :*: lift . Construct x . run . extract

--------------------------------------- Prefixed rose tree -----------------------------------------

instance Setoid k => Morphable (Lookup Key) (Prefixed Rose k) where
	type Morphing (Lookup Key) (Prefixed Rose k) = (->) (Nonempty List k) <:.> Maybe
	morphing :: (<::>) (Tagged ('Lookup 'Key)) (Prefixed Rose k) a
-> Morphing ('Lookup 'Key) (Prefixed Rose k) a
morphing (<::>) (Tagged ('Lookup 'Key)) (Prefixed Rose k) a
prefixed_rose_tree = case Prefixed Rose k a -> (Rose :. (:*:) k) > a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Prefixed Rose k a -> (Rose :. (:*:) k) > a)
-> Prefixed Rose k a -> (Rose :. (:*:) k) > a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<::>) (Tagged ('Lookup 'Key)) (Prefixed Rose k) a
-> Prefixed Rose k a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph (<::>) (Tagged ('Lookup 'Key)) (Prefixed Rose k) a
prefixed_rose_tree of
		TU Maybe (Construction List (k :*: a))
Nothing -> (((->) (Construction Maybe k) :. Maybe) > a)
-> TU Covariant Covariant ((->) (Construction Maybe k)) Maybe 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 ((((->) (Construction Maybe k) :. Maybe) > a)
 -> TU Covariant Covariant ((->) (Construction Maybe k)) Maybe a)
-> (((->) (Construction Maybe k) :. Maybe) > a)
-> TU Covariant Covariant ((->) (Construction Maybe k)) Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Maybe a -> ((->) (Construction Maybe k) :. Maybe) > a
forall (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant Maybe a
forall a. Maybe a
Nothing
		TU (Just Construction List (k :*: a)
tree) -> (((->) (Construction Maybe k) :. Maybe) > a)
-> TU Covariant Covariant ((->) (Construction Maybe k)) Maybe 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 ((((->) (Construction Maybe k) :. Maybe) > a)
 -> TU Covariant Covariant ((->) (Construction Maybe k)) Maybe a)
-> (((->) (Construction Maybe k) :. Maybe) > a)
-> TU Covariant Covariant ((->) (Construction Maybe k)) Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction Maybe k -> Construction List (k :*: a) -> Maybe a
forall k a.
Setoid k =>
Nonempty List k -> (Nonempty Rose > (k :*: a)) -> Maybe a
find_rose_sub_tree (Construction Maybe k -> Construction List (k :*: a) -> Maybe a)
-> Construction List (k :*: a)
-> ((->) (Construction Maybe k) :. Maybe) > a
forall a b c. (a -> b -> c) -> b -> a -> c
% Construction List (k :*: a)
tree

-- TODO: Ineffiecient - we iterate over all branches in subtree, but we need to short-circuit on the first matching part of
--instance Setoid k => Morphable (Vary Element) (Prefixed Rose k) where
--	type Morphing (Vary Element) (Prefixed Rose k) = ((:*:) (Nonempty List k) <:.> Exactly) <:.:> Prefixed Rose k > (->)
--	morphing (run . run . premorph -> Nothing) = T_U ! \(TU (Construct key _ :*: Exactly value)) -> Prefixed . lift ! Construct (key :*: value) empty
--	morphing (run . run . premorph -> Just (Construct focused subtree)) = T_U ! \(TU (breadcrumbs :*: Exactly value)) -> case breadcrumbs of
--		Construct key Nothing -> Prefixed . lift ! attached focused == key ? Construct (key :*: value) subtree ! Construct focused subtree
--		Construct key (Just keys) -> Prefixed . lift ! attached focused != key ? Construct focused subtree
--			! Construct focused ! vary @Element @_ @_ @(Nonempty (Prefixed Rose k)) keys value -#=!> subtree

---------------------------------- Non-empty prefixed rose tree ------------------------------------

-- TODO: Ineffiecient - we iterate over all branches in subtree, but we need to short-circuit on the first matching part of
--instance Setoid k => Morphable (Vary Element) (Prefixed (Construction List) k) where
--	type Morphing (Vary Element) (Prefixed (Construction List) k) =
--		((:*:) (Nonempty List k) <:.> Exactly) <:.:> Prefixed (Construction List) k > (->)
--	morphing (run . premorph -> Construct x (TU Nothing)) = T_U ! \(TU (breadcrumbs :*: Exactly value)) -> case breadcrumbs of
--		Construct key Nothing -> Prefixed ! attached x == key ? Construct (key :*: value) empty ! Construct x empty
--		Construct _ (Just _) -> Prefixed ! Construct x (TU Nothing)
--	morphing (run . premorph -> Construct x (TU (Just subtree))) = T_U ! \(TU (breadcrumbs :*: Exactly value)) -> case breadcrumbs of
--		Construct key Nothing -> Prefixed ! attached x != key ? Construct x # lift subtree
--			! Construct (key :*: value) (lift subtree)
--		Construct key (Just keys) -> Prefixed ! attached x != key ? Construct x # lift subtree
--			! Construct (key :*: value) . lift ! vary @Element @_ @_ @(Nonempty (Prefixed Rose k)) keys value -#=!> subtree

find_rose_sub_tree :: forall k a . Setoid k => Nonempty List k -> Nonempty Rose > k :*: a -> Maybe a
find_rose_sub_tree :: Nonempty List k -> (Nonempty Rose > (k :*: a)) -> Maybe a
find_rose_sub_tree (Construct k Nothing) Nonempty Rose > (k :*: a)
tree = k
k k -> k -> Maybe a -> Maybe a -> Maybe a
forall a r. Setoid a => a -> a -> r -> r -> r
?== (k :*: a) -> k
forall a b. (a :*: b) -> a
attached ((k :*: a) -> k) -> (k :*: a) -> k
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction List (k :*: a) -> k :*: a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Nonempty Rose > (k :*: a)
Construction List (k :*: a)
tree (Maybe a -> Maybe a -> Maybe a) -> Maybe a -> Maybe a -> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<----- a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- (k :*: a) -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract ((k :*: a) -> a) -> (k :*: a) -> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction List (k :*: a) -> k :*: a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Nonempty Rose > (k :*: a)
Construction List (k :*: a)
tree (Maybe a -> Maybe a) -> Maybe a -> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<----- Maybe a
forall a. Maybe a
Nothing
find_rose_sub_tree (Construct k (Just ks)) Nonempty Rose > (k :*: a)
tree = k
k k -> k -> Maybe a -> Maybe a -> Maybe a
forall a r. Setoid a => a -> a -> r -> r -> r
?== (k :*: a) -> k
forall a b. (a :*: b) -> a
attached ((k :*: a) -> k) -> (k :*: a) -> k
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction List (k :*: a) -> k :*: a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Nonempty Rose > (k :*: a)
Construction List (k :*: a)
tree (Maybe a -> Maybe a -> Maybe a) -> Maybe a -> Maybe a -> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<----- Nonempty List k -> (Nonempty Rose > (k :*: a)) -> Maybe a
forall k a.
Setoid k =>
Nonempty List k -> (Nonempty Rose > (k :*: a)) -> Maybe a
find_rose_sub_tree Nonempty List k
Construction Maybe k
ks (Construction List (k :*: a) -> Maybe a)
-> Maybe (Construction List (k :*: a)) -> Maybe a
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
=<< (Maybe :. Nonempty Rose) > (k :*: a)
Maybe (Construction List (k :*: a))
subtree (Maybe a -> Maybe a) -> Maybe a -> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<----- Maybe a
forall a. Maybe a
Nothing where 

	subtree :: Maybe :. Nonempty Rose > k :*: a
	subtree :: (Maybe :. Nonempty Rose) > (k :*: a)
subtree = forall a1 (mod :: a1) (struct :: * -> *) (result :: * -> *) a2.
Morphed ('Find mod) struct ((Predicate <:.:> result) > (->)) =>
Predicate a2 -> struct a2 -> result a2
forall (struct :: * -> *) (result :: * -> *) a2.
Morphed
  ('Find 'Element) struct ((Predicate <:.:> result) > (->)) =>
Predicate a2 -> struct a2 -> result a2
find @Element (Predicate (Construction List (k :*: a))
 -> List (Construction List (k :*: a))
 -> Maybe (Construction List (k :*: a)))
-> Predicate (Construction List (k :*: a))
-> List (Construction List (k :*: a))
-> Maybe (Construction List (k :*: a))
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- (k :*: a) -> k
forall a b. (a :*: b) -> a
attached ((k :*: a) -> k)
-> (Construction List (k :*: a) -> k :*: a)
-> Construction List (k :*: a)
-> k
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction List (k :*: a) -> k :*: a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Construction List (k :*: a) -> k)
-> Predicate k -> Predicate (Construction List (k :*: a))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Contravariant source target t =>
source a b -> target (t b) (t a)
>-|-- k :=> Predicate
forall a. Setoid a => a :=> Predicate
equate (k :=> Predicate) -> k :=> Predicate
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction Maybe k -> k
forall (t :: * -> *) a. Extractable t => t a -> a
extract Construction Maybe k
ks (List (Construction List (k :*: a))
 -> Maybe (Construction List (k :*: a)))
-> List (Construction List (k :*: a))
-> Maybe (Construction List (k :*: a))
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- Construction List (k :*: a) -> List (Construction List (k :*: a))
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) > a
deconstruct Nonempty Rose > (k :*: a)
Construction List (k :*: a)
tree