{-# OPTIONS_GHC -fno-warn-orphans #-}
module Pandora.Paradigm.Structure.Stack where
import Pandora.Core.Functor (type (~>), type (:.), type (:=))
import Pandora.Core.Morphism ((&), (%))
import Pandora.Pattern ((.|..))
import Pandora.Pattern.Category ((.), ($))
import Pandora.Pattern.Functor.Covariant (Covariant ((<$>)))
import Pandora.Pattern.Functor.Alternative ((<+>))
import Pandora.Pattern.Functor.Pointable (point)
import Pandora.Pattern.Functor.Extractable (extract)
import Pandora.Pattern.Functor.Traversable (Traversable)
import Pandora.Pattern.Functor.Bindable ((>>=))
import Pandora.Pattern.Functor.Extendable (Extendable ((=>>)))
import Pandora.Pattern.Transformer.Liftable (lift)
import Pandora.Pattern.Object.Setoid (Setoid ((==)))
import Pandora.Pattern.Object.Semigroup (Semigroup ((+)))
import Pandora.Pattern.Object.Monoid (Monoid (zero))
import Pandora.Paradigm.Primary.Object.Boolean (Boolean (True, False), (?))
import Pandora.Paradigm.Primary.Functor.Delta (Delta ((:^:)))
import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Just, Nothing))
import Pandora.Paradigm.Primary.Functor.Predicate (Predicate (Predicate))
import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)))
import Pandora.Paradigm.Primary.Functor.Tagged (Tagged (Tag))
import Pandora.Paradigm.Primary.Functor.Wye (Wye (Left, Right))
import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct), deconstruct, (.-+))
import Pandora.Paradigm.Primary.Transformer.Tap (Tap (Tap))
import Pandora.Paradigm.Inventory.State (State, fold)
import Pandora.Paradigm.Inventory.Store (Store (Store))
import Pandora.Paradigm.Inventory.Optics ((^.))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run)
import Pandora.Paradigm.Schemes.TU (TU (TU), type (<:.>))
import Pandora.Paradigm.Structure.Ability.Nonempty (Nonempty)
import Pandora.Paradigm.Structure.Ability.Nullable (Nullable (null))
import Pandora.Paradigm.Structure.Ability.Zipper (Zipper)
import Pandora.Paradigm.Structure.Ability.Focusable (Focusable (Focusing, focusing), Location (Head), focus)
import Pandora.Paradigm.Structure.Ability.Insertable (Insertable (insert))
import Pandora.Paradigm.Structure.Ability.Monotonic (Monotonic (reduce))
import Pandora.Paradigm.Structure.Ability.Rotatable (Rotatable (Rotational, rotation), rotate)
type Stack = Maybe <:.> Construction Maybe
instance Setoid a => Setoid (Stack a) where
TU (Maybe :. Construction Maybe) := a
ls == :: Stack a -> Stack a -> Boolean
== TU (Maybe :. Construction Maybe) := a
rs = (Maybe :. Construction Maybe) := a
ls ((Maybe :. Construction Maybe) := a)
-> ((Maybe :. Construction Maybe) := a) -> Boolean
forall a. Setoid a => a -> a -> Boolean
== (Maybe :. Construction Maybe) := a
rs
instance Semigroup (Stack a) where
TU Maybe (Construction Maybe a)
Nothing + :: Stack a -> Stack a -> Stack a
+ TU Maybe (Construction Maybe a)
ys = Maybe (Construction Maybe a) -> Stack 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 Maybe (Construction Maybe a)
ys
TU (Just (Construct a
x Maybe (Construction Maybe a)
xs)) + TU Maybe (Construction Maybe a)
ys = Construction Maybe a -> Stack a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Maybe a -> Stack a)
-> (Stack a -> Construction Maybe a) -> Stack a -> Stack a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Maybe (Construction Maybe a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Maybe (Construction Maybe a) -> Construction Maybe a)
-> (Stack a -> Maybe (Construction Maybe a))
-> Stack a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Stack a -> Maybe (Construction Maybe a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run
(Stack a -> Stack a) -> Stack a -> Stack a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Maybe (Construction Maybe a) -> Stack 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 @Covariant @Covariant Maybe (Construction Maybe a)
xs Stack a -> Stack a -> Stack a
forall a. Semigroup a => a -> a -> a
+ Maybe (Construction Maybe a) -> Stack 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 @Covariant @Covariant Maybe (Construction Maybe a)
ys
instance Monoid (Stack a) where
zero :: Stack a
zero = ((Maybe :. Construction Maybe) := a) -> Stack 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 (Maybe :. Construction Maybe) := a
forall a. Maybe a
Nothing
instance Focusable Head Stack where
type Focusing Head Stack a = Maybe a
focusing :: Tagged 'Head (Stack a) :-. Focusing 'Head Stack a
focusing (Tag Stack a
stack) = (((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Head (Stack a))
-> Store (Maybe a) (Tagged 'Head (Stack a))
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Head (Stack a))
-> Store (Maybe a) (Tagged 'Head (Stack a)))
-> (((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Head (Stack a))
-> Store (Maybe a) (Tagged 'Head (Stack a))
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ a <-| Construction Maybe
forall (t :: * -> *) a. Extractable t => a <-| t
extract (a <-| Construction Maybe)
-> Maybe (Construction Maybe a) -> Maybe a
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> Stack a -> Primary Stack a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run Stack a
stack Maybe a
-> (Maybe a -> Tagged 'Head (Stack a))
-> ((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Head (Stack a)
forall s a. s -> a -> Product s a
:*: \case
Just a
x -> Stack a
stack Stack a -> (Stack a -> Stack a) -> Stack a
forall a b. a -> (a -> b) -> b
& Stack a -> Stack a
Stack ~> Stack
pop Stack a -> (Stack a -> Stack a) -> Stack a
forall a b. a -> (a -> b) -> b
& a -> Stack a -> Stack a
forall (t :: * -> *) a. Insertable t => a -> t a -> t a
insert a
x Stack a
-> (Stack a -> Tagged 'Head (Stack a)) -> Tagged 'Head (Stack a)
forall a b. a -> (a -> b) -> b
& Stack a -> Tagged 'Head (Stack a)
forall k (tag :: k) a. a -> Tagged tag a
Tag
Maybe a
Nothing -> Stack a -> Tagged 'Head (Stack a)
forall k (tag :: k) a. a -> Tagged tag a
Tag (Stack a -> Tagged 'Head (Stack a))
-> Stack a -> Tagged 'Head (Stack a)
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Stack a -> Stack a
Stack ~> Stack
pop Stack a
stack
instance Insertable Stack where
insert :: a -> Stack a -> Stack a
insert a
x (TU (Maybe :. Construction Maybe) := a
stack) = ((Maybe :. Construction Maybe) := a) -> Stack 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 (((Maybe :. Construction Maybe) := a) -> Stack a)
-> ((Maybe :. Construction Maybe) := a) -> Stack a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ (a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (((Maybe :. Construction Maybe) := a) -> Construction Maybe a)
-> (Construction Maybe a -> (Maybe :. Construction Maybe) := a)
-> Construction Maybe a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall a. a -> Maybe a
Just (Construction Maybe a -> Construction Maybe a)
-> ((Maybe :. Construction Maybe) := a)
-> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> (Maybe :. Construction Maybe) := a
stack) ((Maybe :. Construction Maybe) := a)
-> ((Maybe :. Construction Maybe) := a)
-> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a. Alternative t => t a -> t a -> t a
<+> (Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a. Pointable t => a |-> t
point (Construction Maybe a -> (Maybe :. Construction Maybe) := a)
-> (a -> Construction Maybe a)
-> a
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Construction Maybe a
forall (t :: * -> *) a. Pointable t => a |-> t
point) a
x
instance Nullable Stack where
null :: (Predicate :. Stack) := a
null = (Stack a -> Boolean) -> (Predicate :. Stack) := a
forall a. (a -> Boolean) -> Predicate a
Predicate ((Stack a -> Boolean) -> (Predicate :. Stack) := a)
-> (Stack a -> Boolean) -> (Predicate :. Stack) := a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ \case { TU Maybe (Construction Maybe a)
Nothing -> Boolean
True ; Stack a
_ -> Boolean
False }
pop :: Stack ~> Stack
pop :: Stack a -> Stack a
pop (TU (Maybe :. Construction Maybe) := a
stack) = ((Maybe :. Construction Maybe) := a) -> Stack 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 (((Maybe :. Construction Maybe) := a) -> Stack a)
-> ((Maybe :. Construction Maybe) := a) -> Stack a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ (Maybe :. Construction Maybe) := a
stack ((Maybe :. Construction Maybe) := a)
-> (Construction Maybe a -> (Maybe :. Construction Maybe) := a)
-> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a b. Bindable t => t a -> (a -> t b) -> t b
>>= Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct
delete :: Setoid a => a -> Stack a -> Stack a
delete :: a -> Stack a -> Stack a
delete a
_ (TU Maybe (Construction Maybe a)
Nothing) = Maybe (Construction Maybe a) -> Stack 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 Maybe (Construction Maybe a)
forall a. Maybe a
Nothing
delete a
x (TU (Just (Construct a
y Maybe (Construction Maybe a)
ys))) = a
x a -> a -> Boolean
forall a. Setoid a => a -> a -> Boolean
== a
y Boolean -> Stack a -> Stack a -> Stack a
forall a. Boolean -> a -> a -> a
? Maybe (Construction Maybe a) -> Stack 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 Maybe (Construction Maybe a)
ys
(Stack a -> Stack a) -> Stack a -> Stack a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Construction Maybe a -> Stack a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Maybe a -> Stack a)
-> (Stack a -> Construction Maybe a) -> Stack a -> Stack a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Maybe (Construction Maybe a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
y (Maybe (Construction Maybe a) -> Construction Maybe a)
-> (Stack a -> Maybe (Construction Maybe a))
-> Stack a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Stack a -> Maybe (Construction Maybe a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Stack a -> Maybe (Construction Maybe a))
-> (Stack a -> Stack a) -> Stack a -> Maybe (Construction Maybe a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Stack a -> Stack a
forall a. Setoid a => a -> Stack a -> Stack a
delete a
x (Stack a -> Stack a) -> Stack a -> Stack a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Maybe (Construction Maybe a) -> Stack 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 Maybe (Construction Maybe a)
ys
filter :: forall a . Predicate a -> Stack a -> Stack a
filter :: Predicate a -> Stack a -> Stack a
filter (Predicate a -> Boolean
p) = ((Maybe :. Construction Maybe) := a) -> Stack 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 (((Maybe :. Construction Maybe) := a) -> Stack a)
-> (Stack a -> (Maybe :. Construction Maybe) := a)
-> Stack a
-> Stack a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. ((Maybe :. Construction Maybe) := a)
<-| Product ((Maybe :. Construction Maybe) := a)
forall (t :: * -> *) a. Extractable t => a <-| t
extract
(((Maybe :. Construction Maybe) := a)
<-| Product ((Maybe :. Construction Maybe) := a))
-> (Stack a
-> Product
((Maybe :. Construction Maybe) := a)
((Maybe :. Construction Maybe) := a))
-> Stack a
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. forall a.
Interpreted (State ((Maybe :. Nonempty Stack) := a)) =>
State ((Maybe :. Nonempty Stack) := a) a
-> Primary (State ((Maybe :. Nonempty Stack) := a)) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run @(State (Maybe :. Nonempty Stack := a)) (State
((Maybe :. Construction Maybe) := a)
((Maybe :. Construction Maybe) := a)
-> ((Maybe :. Construction Maybe) := a)
-> Product
((Maybe :. Construction Maybe) := a)
((Maybe :. Construction Maybe) := a))
-> ((Maybe :. Construction Maybe) := a)
-> State
((Maybe :. Construction Maybe) := a)
((Maybe :. Construction Maybe) := a)
-> Product
((Maybe :. Construction Maybe) := a)
((Maybe :. Construction Maybe) := a)
forall a b c. (a -> b -> c) -> b -> a -> c
% (Maybe :. Construction Maybe) := a
forall a. Maybe a
Nothing
(State
((Maybe :. Construction Maybe) := a)
((Maybe :. Construction Maybe) := a)
-> Product
((Maybe :. Construction Maybe) := a)
((Maybe :. Construction Maybe) := a))
-> (Stack a
-> State
((Maybe :. Construction Maybe) := a)
((Maybe :. Construction Maybe) := a))
-> Stack a
-> Product
((Maybe :. Construction Maybe) := a)
((Maybe :. Construction Maybe) := a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (a
-> ((Maybe :. Construction Maybe) := a)
-> (Maybe :. Construction Maybe) := a)
-> Stack a
-> State
((Maybe :. Construction Maybe) := a)
((Maybe :. Construction Maybe) := a)
forall (t :: * -> *) s (u :: * -> *) a.
(Traversable t, Memorable s u) =>
(a -> s -> s) -> t a -> u s
fold (\a
now (Maybe :. Construction Maybe) := a
new -> a -> Boolean
p a
now Boolean
-> ((Maybe :. Construction Maybe) := a)
-> ((Maybe :. Construction Maybe) := a)
-> (Maybe :. Construction Maybe) := a
forall a. Boolean -> a -> a -> a
? Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall a. a -> Maybe a
Just (a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
now (Maybe :. Construction Maybe) := a
new) (((Maybe :. Construction Maybe) := a)
-> (Maybe :. Construction Maybe) := a)
-> ((Maybe :. Construction Maybe) := a)
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ (Maybe :. Construction Maybe) := a
new)
linearize :: forall t a . Traversable t => t a -> Stack a
linearize :: t a -> Stack a
linearize = ((Maybe :. Construction Maybe) := a) -> Stack 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 (((Maybe :. Construction Maybe) := a) -> Stack a)
-> (t a -> (Maybe :. Construction Maybe) := a) -> t a -> Stack a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. ((Maybe :. Construction Maybe) := a)
<-| Product ((Maybe :. Construction Maybe) := a)
forall (t :: * -> *) a. Extractable t => a <-| t
extract (((Maybe :. Construction Maybe) := a)
<-| Product ((Maybe :. Construction Maybe) := a))
-> (t a
-> Product
((Maybe :. Construction Maybe) := a)
((Maybe :. Construction Maybe) := a))
-> t a
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. forall a.
Interpreted (State ((Maybe :. Nonempty Stack) := a)) =>
State ((Maybe :. Nonempty Stack) := a) a
-> Primary (State ((Maybe :. Nonempty Stack) := a)) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run @(State (Maybe :. Nonempty Stack := a)) (State
((Maybe :. Construction Maybe) := a)
((Maybe :. Construction Maybe) := a)
-> ((Maybe :. Construction Maybe) := a)
-> Product
((Maybe :. Construction Maybe) := a)
((Maybe :. Construction Maybe) := a))
-> ((Maybe :. Construction Maybe) := a)
-> State
((Maybe :. Construction Maybe) := a)
((Maybe :. Construction Maybe) := a)
-> Product
((Maybe :. Construction Maybe) := a)
((Maybe :. Construction Maybe) := a)
forall a b c. (a -> b -> c) -> b -> a -> c
% (Maybe :. Construction Maybe) := a
forall a. Maybe a
Nothing (State
((Maybe :. Construction Maybe) := a)
((Maybe :. Construction Maybe) := a)
-> Product
((Maybe :. Construction Maybe) := a)
((Maybe :. Construction Maybe) := a))
-> (t a
-> State
((Maybe :. Construction Maybe) := a)
((Maybe :. Construction Maybe) := a))
-> t a
-> Product
((Maybe :. Construction Maybe) := a)
((Maybe :. Construction Maybe) := a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (a
-> ((Maybe :. Construction Maybe) := a)
-> (Maybe :. Construction Maybe) := a)
-> t a
-> State
((Maybe :. Construction Maybe) := a)
((Maybe :. Construction Maybe) := a)
forall (t :: * -> *) s (u :: * -> *) a.
(Traversable t, Memorable s u) =>
(a -> s -> s) -> t a -> u s
fold (Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall a. a -> Maybe a
Just (Construction Maybe a -> (Maybe :. Construction Maybe) := a)
-> (((->) a :. (->) ((Maybe :. Construction Maybe) := a))
:= Construction Maybe a)
-> a
-> ((Maybe :. Construction Maybe) := a)
-> (Maybe :. Construction Maybe) := a
forall (v :: * -> * -> *) a c d b.
(Category v, Covariant (v a)) =>
v c d -> ((v a :. v b) := c) -> (v a :. v b) := d
.|.. ((->) a :. (->) ((Maybe :. Construction Maybe) := a))
:= Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct)
type instance Nonempty Stack = Construction Maybe
instance Focusable Head (Construction Maybe) where
type Focusing Head (Construction Maybe) a = a
focusing :: Tagged 'Head (Construction Maybe a)
:-. Focusing 'Head (Construction Maybe) a
focusing (Tag Construction Maybe a
stack) = (((:*:) a :. (->) a) := Tagged 'Head (Construction Maybe a))
-> Store a (Tagged 'Head (Construction Maybe a))
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) a :. (->) a) := Tagged 'Head (Construction Maybe a))
-> Store a (Tagged 'Head (Construction Maybe a)))
-> (((:*:) a :. (->) a) := Tagged 'Head (Construction Maybe a))
-> Store a (Tagged 'Head (Construction Maybe a))
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ a <-| Construction Maybe
forall (t :: * -> *) a. Extractable t => a <-| t
extract Construction Maybe a
stack a
-> (a -> Tagged 'Head (Construction Maybe a))
-> ((:*:) a :. (->) a) := Tagged 'Head (Construction Maybe a)
forall s a. s -> a -> Product s a
:*: Construction Maybe a -> Tagged 'Head (Construction Maybe a)
forall k (tag :: k) a. a -> Tagged tag a
Tag (Construction Maybe a -> Tagged 'Head (Construction Maybe a))
-> (a -> Construction Maybe a)
-> a
-> Tagged 'Head (Construction Maybe a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a)
-> ((Maybe :. Construction Maybe) := a)
-> a
-> Construction Maybe a
forall a b c. (a -> b -> c) -> b -> a -> c
% Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct Construction Maybe a
stack
instance Insertable (Construction Maybe) where
insert :: a -> Construction Maybe a -> Construction Maybe a
insert a
x = a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (((Maybe :. Construction Maybe) := a) -> Construction Maybe a)
-> (Construction Maybe a -> (Maybe :. Construction Maybe) := a)
-> Construction Maybe a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall a. a -> Maybe a
Just
instance Monotonic a (Construction Maybe a) where
reduce :: (a -> r -> r) -> r -> Construction Maybe a -> r
reduce a -> r -> r
f r
r ~(Construct a
x (Maybe :. Construction Maybe) := a
xs) = a -> r -> r
f a
x (r -> r) -> r -> r
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ (a -> r -> r) -> r -> ((Maybe :. Construction Maybe) := a) -> r
forall a e r. Monotonic a e => (a -> r -> r) -> r -> e -> r
reduce a -> r -> r
f r
r (Maybe :. Construction Maybe) := a
xs
type instance Zipper Stack = Tap (Delta <:.> Stack)
instance {-# OVERLAPS #-} Extendable (Tap (Delta <:.> Stack)) where
Tap (Delta <:.> Stack) a
z =>> :: Tap (Delta <:.> Stack) a
-> (Tap (Delta <:.> Stack) a -> b) -> Tap (Delta <:.> Stack) b
=>> Tap (Delta <:.> Stack) a -> b
f = let move :: (Tap (Delta <:.> Stack) a |-> Maybe)
-> TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap (Delta <:.> Stack) a)
move Tap (Delta <:.> Stack) a |-> Maybe
rtt = ((Maybe :. Construction Maybe) := Tap (Delta <:.> Stack) a)
-> TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap (Delta <:.> Stack) 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 (((Maybe :. Construction Maybe) := Tap (Delta <:.> Stack) a)
-> TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap (Delta <:.> Stack) a))
-> (Construction Maybe (Tap (Delta <:.> Stack) a)
-> (Maybe :. Construction Maybe) := Tap (Delta <:.> Stack) a)
-> Construction Maybe (Tap (Delta <:.> Stack) a)
-> TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap (Delta <:.> Stack) a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Maybe (Tap (Delta <:.> Stack) a)
-> (Maybe :. Construction Maybe) := Tap (Delta <:.> Stack) a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct (Construction Maybe (Tap (Delta <:.> Stack) a)
-> TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap (Delta <:.> Stack) a))
-> Construction Maybe (Tap (Delta <:.> Stack) a)
-> TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap (Delta <:.> Stack) a)
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Tap (Delta <:.> Stack) a |-> Maybe
rtt (Tap (Delta <:.> Stack) a |-> Maybe)
-> Tap (Delta <:.> Stack) a |-> Construction Maybe
forall (t :: * -> *) a.
Covariant t =>
(a |-> t) -> a |-> Construction t
.-+ Tap (Delta <:.> Stack) a
z
in Tap (Delta <:.> Stack) a -> b
f (Tap (Delta <:.> Stack) a -> b)
-> Tap (Delta <:.> Stack) (Tap (Delta <:.> Stack) a)
-> Tap (Delta <:.> Stack) b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> Tap (Delta <:.> Stack) a
-> (<:.>) Delta Stack (Tap (Delta <:.> Stack) a)
-> Tap (Delta <:.> Stack) (Tap (Delta <:.> Stack) a)
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap Tap (Delta <:.> Stack) a
z (((Delta :. Stack) := Tap (Delta <:.> Stack) a)
-> (<:.>) Delta Stack (Tap (Delta <:.> Stack) 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 (((Delta :. Stack) := Tap (Delta <:.> Stack) a)
-> (<:.>) Delta Stack (Tap (Delta <:.> Stack) a))
-> ((Delta :. Stack) := Tap (Delta <:.> Stack) a)
-> (<:.>) Delta Stack (Tap (Delta <:.> Stack) a)
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ (Tap (Delta <:.> Stack) a |-> Maybe)
-> TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap (Delta <:.> Stack) a)
move (forall k (f :: k) (t :: * -> *) a.
Rotatable f t =>
t a -> Rotational f t a
forall (t :: * -> *) a.
Rotatable 'Left t =>
t a -> Rotational 'Left t a
rotate @Left) TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap (Delta <:.> Stack) a)
-> TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap (Delta <:.> Stack) a)
-> (Delta :. Stack) := Tap (Delta <:.> Stack) a
forall a. a -> a -> Delta a
:^: (Tap (Delta <:.> Stack) a |-> Maybe)
-> TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap (Delta <:.> Stack) a)
move (forall k (f :: k) (t :: * -> *) a.
Rotatable f t =>
t a -> Rotational f t a
forall (t :: * -> *) a.
Rotatable 'Right t =>
t a -> Rotational 'Right t a
rotate @Right))
instance Rotatable Left (Tap (Delta <:.> Stack)) where
type Rotational Left (Tap (Delta <:.> Stack)) a = Maybe :. Zipper Stack := a
rotation :: Tagged 'Left (Tap (Delta <:.> Stack) a)
-> Rotational 'Left (Tap (Delta <:.> Stack)) a
rotation (Tap (Delta <:.> Stack) a <-| Tagged 'Left
forall (t :: * -> *) a. Extractable t => a <-| t
extract -> Tap a
x (TU (Stack a
bs :^: Stack a
fs))) = a
-> TU Covariant Covariant Delta Stack a -> Tap (Delta <:.> Stack) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (a
-> TU Covariant Covariant Delta Stack a
-> Tap (Delta <:.> Stack) a)
-> TU Covariant Covariant Delta Stack a
-> a
-> Tap (Delta <:.> Stack) a
forall a b c. (a -> b -> c) -> b -> a -> c
% (Delta (Stack a) -> TU Covariant Covariant Delta Stack 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 (Delta (Stack a) -> TU Covariant Covariant Delta Stack a)
-> Delta (Stack a) -> TU Covariant Covariant Delta Stack a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Stack a -> Stack a
Stack ~> Stack
pop Stack a
bs Stack a -> Stack a -> Delta (Stack a)
forall a. a -> a -> Delta a
:^: a -> Stack a -> Stack a
forall (t :: * -> *) a. Insertable t => a -> t a -> t a
insert a
x Stack a
fs) (a -> Tap (Delta <:.> Stack) a)
-> Maybe a -> Maybe (Tap (Delta <:.> Stack) a)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> forall k (f :: * -> k) (t :: * -> *) a.
Focusable f t =>
t a :-. Focusing f t a
forall (t :: * -> *) a.
Focusable 'Head t =>
t a :-. Focusing 'Head t a
focus @Head (Stack a -> Store (Maybe a) (Stack a)) -> Stack a -> Maybe a
forall src tgt. Lens src tgt -> src -> tgt
^. Stack a
bs
instance Rotatable Right (Tap (Delta <:.> Stack)) where
type Rotational Right (Tap (Delta <:.> Stack)) a = Maybe :. Zipper Stack := a
rotation :: Tagged 'Right (Tap (Delta <:.> Stack) a)
-> Rotational 'Right (Tap (Delta <:.> Stack)) a
rotation (Tap (Delta <:.> Stack) a <-| Tagged 'Right
forall (t :: * -> *) a. Extractable t => a <-| t
extract -> Tap a
x (TU (Stack a
bs :^: Stack a
fs))) = a
-> TU Covariant Covariant Delta Stack a -> Tap (Delta <:.> Stack) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (a
-> TU Covariant Covariant Delta Stack a
-> Tap (Delta <:.> Stack) a)
-> TU Covariant Covariant Delta Stack a
-> a
-> Tap (Delta <:.> Stack) a
forall a b c. (a -> b -> c) -> b -> a -> c
% (Delta (Stack a) -> TU Covariant Covariant Delta Stack 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 (Delta (Stack a) -> TU Covariant Covariant Delta Stack a)
-> Delta (Stack a) -> TU Covariant Covariant Delta Stack a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ a -> Stack a -> Stack a
forall (t :: * -> *) a. Insertable t => a -> t a -> t a
insert a
x Stack a
bs Stack a -> Stack a -> Delta (Stack a)
forall a. a -> a -> Delta a
:^: Stack a -> Stack a
Stack ~> Stack
pop Stack a
fs) (a -> Tap (Delta <:.> Stack) a)
-> Maybe a -> Maybe (Tap (Delta <:.> Stack) a)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> forall k (f :: * -> k) (t :: * -> *) a.
Focusable f t =>
t a :-. Focusing f t a
forall (t :: * -> *) a.
Focusable 'Head t =>
t a :-. Focusing 'Head t a
focus @Head (Stack a -> Store (Maybe a) (Stack a)) -> Stack a -> Maybe a
forall src tgt. Lens src tgt -> src -> tgt
^. Stack a
fs
type instance Zipper (Construction Maybe) = Tap (Delta <:.> Construction Maybe)
instance Rotatable Left (Tap (Delta <:.> Construction Maybe)) where
type Rotational Left (Tap (Delta <:.> Construction Maybe)) a = Maybe :. Zipper (Construction Maybe) := a
rotation :: Tagged 'Left (Tap (Delta <:.> Construction Maybe) a)
-> Rotational 'Left (Tap (Delta <:.> Construction Maybe)) a
rotation (Tap (Delta <:.> Construction Maybe) a <-| Tagged 'Left
forall (t :: * -> *) a. Extractable t => a <-| t
extract -> Tap a
x (TU (Construction Maybe a
bs :^: Construction Maybe a
fs))) = a
-> TU Covariant Covariant Delta (Construction Maybe) a
-> Tap (Delta <:.> Construction Maybe) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (a <-| Construction Maybe
forall (t :: * -> *) a. Extractable t => a <-| t
extract Construction Maybe a
bs) (TU Covariant Covariant Delta (Construction Maybe) a
-> Tap (Delta <:.> Construction Maybe) a)
-> (Construction Maybe a
-> TU Covariant Covariant Delta (Construction Maybe) a)
-> Construction Maybe a
-> Tap (Delta <:.> Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Delta (Construction Maybe a)
-> TU Covariant Covariant Delta (Construction 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 (Delta (Construction Maybe a)
-> TU Covariant Covariant Delta (Construction Maybe) a)
-> (Construction Maybe a -> Delta (Construction Maybe a))
-> Construction Maybe a
-> TU Covariant Covariant Delta (Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (Construction Maybe a
-> Construction Maybe a -> Delta (Construction Maybe a)
forall a. a -> a -> Delta a
:^: a -> Construction Maybe a -> Construction Maybe a
forall (t :: * -> *) a. Insertable t => a -> t a -> t a
insert a
x Construction Maybe a
fs) (Construction Maybe a -> Tap (Delta <:.> Construction Maybe) a)
-> Maybe (Construction Maybe a)
-> Maybe (Tap (Delta <:.> Construction Maybe) a)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> Construction Maybe a -> Maybe (Construction Maybe a)
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct Construction Maybe a
bs
instance Rotatable Right (Tap (Delta <:.> Construction Maybe)) where
type Rotational Right (Tap (Delta <:.> Construction Maybe)) a = Maybe :. Zipper (Construction Maybe) := a
rotation :: Tagged 'Right (Tap (Delta <:.> Construction Maybe) a)
-> Rotational 'Right (Tap (Delta <:.> Construction Maybe)) a
rotation (Tap (Delta <:.> Construction Maybe) a <-| Tagged 'Right
forall (t :: * -> *) a. Extractable t => a <-| t
extract -> Tap a
x (TU (Construction Maybe a
bs :^: Construction Maybe a
fs))) = a
-> TU Covariant Covariant Delta (Construction Maybe) a
-> Tap (Delta <:.> Construction Maybe) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (a <-| Construction Maybe
forall (t :: * -> *) a. Extractable t => a <-| t
extract Construction Maybe a
fs) (TU Covariant Covariant Delta (Construction Maybe) a
-> Tap (Delta <:.> Construction Maybe) a)
-> (Construction Maybe a
-> TU Covariant Covariant Delta (Construction Maybe) a)
-> Construction Maybe a
-> Tap (Delta <:.> Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Delta (Construction Maybe a)
-> TU Covariant Covariant Delta (Construction 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 (Delta (Construction Maybe a)
-> TU Covariant Covariant Delta (Construction Maybe) a)
-> (Construction Maybe a -> Delta (Construction Maybe a))
-> Construction Maybe a
-> TU Covariant Covariant Delta (Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (a -> Construction Maybe a -> Construction Maybe a
forall (t :: * -> *) a. Insertable t => a -> t a -> t a
insert a
x Construction Maybe a
bs Construction Maybe a
-> Construction Maybe a -> Delta (Construction Maybe a)
forall a. a -> a -> Delta a
:^:) (Construction Maybe a -> Tap (Delta <:.> Construction Maybe) a)
-> Maybe (Construction Maybe a)
-> Maybe (Tap (Delta <:.> Construction Maybe) a)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> Construction Maybe a -> Maybe (Construction Maybe a)
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct Construction Maybe a
fs
instance Monotonic a (Maybe <:.> Construction Maybe := a) where
reduce :: (a -> r -> r) -> r -> (Stack := a) -> r
reduce a -> r -> r
f r
r = (a -> r -> r) -> r -> ((Maybe :. Construction Maybe) := a) -> r
forall a e r. Monotonic a e => (a -> r -> r) -> r -> e -> r
reduce a -> r -> r
f r
r (((Maybe :. Construction Maybe) := a) -> r)
-> ((Stack := a) -> (Maybe :. Construction Maybe) := a)
-> (Stack := a)
-> r
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (Stack := a) -> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run