{-# OPTIONS_GHC -fno-warn-orphans #-}
module Pandora.Paradigm.Structure.Stack where
import Pandora.Core.Functor (type (:.), type (:=))
import Pandora.Pattern ((.|..))
import Pandora.Pattern.Category ((.), ($), identity)
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.Avoidable (empty)
import Pandora.Pattern.Functor.Traversable (Traversable)
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.Object.Numerator (Numerator (Numerator))
import Pandora.Paradigm.Primary.Object.Denumerator (Denumerator (One))
import Pandora.Paradigm.Primary.Functor.Function ((%), (&))
import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Just, Nothing))
import Pandora.Paradigm.Primary.Functor.Predicate (Predicate (Predicate))
import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)), type (:*:))
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 (view)
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 (<:.:>))
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.Deletable (Deletable (delete))
import Pandora.Paradigm.Structure.Ability.Insertable (Insertable (insert))
import Pandora.Paradigm.Structure.Ability.Measurable (Measurable (Measural, measurement), Scale (Length), measure)
import Pandora.Paradigm.Structure.Ability.Monotonic (Monotonic (reduce))
import Pandora.Paradigm.Structure.Ability.Morphable (Morphable (Morphing, morphing), Morph (Rotate), morph)
import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Substructural, substructure), Segment (Tail), sub, subview)
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 = Stack a
forall (t :: * -> *) a. Avoidable t => t a
empty
instance Focusable Head Stack where
type Focusing Head Stack a = Maybe a
focusing :: Tagged 'Head (Stack a) :-. Focusing 'Head Stack a
focusing (Stack a <:= Tagged 'Head
forall (t :: * -> *) a. Extractable t => a <:= t
extract -> 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
& forall k (f :: k) (t :: * -> *).
Substructure f t =>
t ~> Substructural f t
forall (t :: * -> *).
Substructure 'Tail t =>
t ~> Substructural 'Tail t
subview @Tail 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
stack Stack a -> (Stack a -> Stack a) -> Stack a
forall a b. a -> (a -> b) -> b
& forall k (f :: k) (t :: * -> *).
Substructure f t =>
t ~> Substructural f t
forall (t :: * -> *).
Substructure 'Tail t =>
t ~> Substructural 'Tail t
subview @Tail 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
instance Insertable Stack where
insert :: a -> Stack a -> Stack a
insert a
x (Stack a -> Primary Stack a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Primary Stack 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
<$> Primary Stack a
(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 Measurable Length Stack where
type Measural Length Stack a = Numerator
measurement :: Tagged 'Length (Stack a) -> Measural 'Length Stack a
measurement (Stack a -> Maybe (Construction Maybe a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Stack a -> Maybe (Construction Maybe a))
-> (Tagged 'Length (Stack a) -> Stack a)
-> Tagged 'Length (Stack a)
-> Maybe (Construction Maybe a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged 'Length (Stack a) -> Stack a
forall (t :: * -> *) a. Extractable t => a <:= t
extract -> Maybe (Construction Maybe a)
Nothing) = Measural 'Length Stack a
forall a. Monoid a => a
zero
measurement (Stack a -> Maybe (Construction Maybe a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Stack a -> Maybe (Construction Maybe a))
-> (Tagged 'Length (Stack a) -> Stack a)
-> Tagged 'Length (Stack a)
-> Maybe (Construction Maybe a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged 'Length (Stack a) -> Stack a
forall (t :: * -> *) a. Extractable t => a <:= t
extract -> Just Construction Maybe a
xs) = Denumerator -> Numerator
Numerator (Denumerator -> Numerator) -> Denumerator -> Numerator
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Construction Maybe a -> Measural 'Length (Construction Maybe) a
forall k (f :: k) (t :: * -> *) a.
Measurable f t =>
t a -> Measural f t a
measure @Length Construction Maybe a
xs
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 }
instance Substructure Tail Stack where
type Substructural Tail Stack = Stack
substructure :: Lens ((<:.>) (Tagged 'Tail) Stack a) (Substructural 'Tail Stack a)
substructure (TU Covariant Covariant Maybe (Construction Maybe) a
-> Maybe (Construction Maybe a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (TU Covariant Covariant Maybe (Construction Maybe) a
-> Maybe (Construction Maybe a))
-> ((<:.>) (Tagged 'Tail) Stack a
-> TU Covariant Covariant Maybe (Construction Maybe) a)
-> (<:.>) (Tagged 'Tail) Stack a
-> Maybe (Construction Maybe a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction Maybe) a
<:= Tagged 'Tail
forall (t :: * -> *) a. Extractable t => a <:= t
extract (TU Covariant Covariant Maybe (Construction Maybe) a
<:= Tagged 'Tail)
-> ((<:.>) (Tagged 'Tail) Stack a
-> Tagged
'Tail (TU Covariant Covariant Maybe (Construction Maybe) a))
-> (<:.>) (Tagged 'Tail) Stack a
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Tail) Stack a
-> Tagged
'Tail (TU Covariant Covariant Maybe (Construction Maybe) a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Just Construction Maybe a
ns) = TU Covariant Covariant Maybe (Construction Maybe) a
-> (<:.>) (Tagged 'Tail) Stack a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (TU Covariant Covariant Maybe (Construction Maybe) a
-> (<:.>) (Tagged 'Tail) Stack a)
-> (Construction Maybe a
-> TU Covariant Covariant Maybe (Construction Maybe) a)
-> Construction Maybe a
-> (<:.>) (Tagged 'Tail) Stack a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Maybe a
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Maybe a -> (<:.>) (Tagged 'Tail) Stack a)
-> Store
(TU Covariant Covariant Maybe (Construction Maybe) a)
(Construction Maybe a)
-> Store
(TU Covariant Covariant Maybe (Construction Maybe) a)
((<:.>) (Tagged 'Tail) Stack a)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> Lens
(Construction Maybe a) (Substructural 'Tail (Construction Maybe) a)
forall k (f :: k) (t :: * -> *).
Substructure f t =>
t :~. Substructural f t
sub @Tail Construction Maybe a
ns
substructure (TU Covariant Covariant Maybe (Construction Maybe) a
-> Maybe (Construction Maybe a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (TU Covariant Covariant Maybe (Construction Maybe) a
-> Maybe (Construction Maybe a))
-> ((<:.>) (Tagged 'Tail) Stack a
-> TU Covariant Covariant Maybe (Construction Maybe) a)
-> (<:.>) (Tagged 'Tail) Stack a
-> Maybe (Construction Maybe a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction Maybe) a
<:= Tagged 'Tail
forall (t :: * -> *) a. Extractable t => a <:= t
extract (TU Covariant Covariant Maybe (Construction Maybe) a
<:= Tagged 'Tail)
-> ((<:.>) (Tagged 'Tail) Stack a
-> Tagged
'Tail (TU Covariant Covariant Maybe (Construction Maybe) a))
-> (<:.>) (Tagged 'Tail) Stack a
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Tail) Stack a
-> Tagged
'Tail (TU Covariant Covariant Maybe (Construction Maybe) a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Maybe (Construction Maybe a)
Nothing) = (((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
:. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
:= (<:.>) (Tagged 'Tail) Stack a)
-> Store
(TU Covariant Covariant Maybe (Construction Maybe) a)
((<:.>) (Tagged 'Tail) Stack a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
:. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
:= (<:.>) (Tagged 'Tail) Stack a)
-> Store
(TU Covariant Covariant Maybe (Construction Maybe) a)
((<:.>) (Tagged 'Tail) Stack a))
-> (((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
:. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
:= (<:.>) (Tagged 'Tail) Stack a)
-> Store
(TU Covariant Covariant Maybe (Construction Maybe) a)
((<:.>) (Tagged 'Tail) Stack a)
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ TU Covariant Covariant Maybe (Construction Maybe) a
forall (t :: * -> *) a. Avoidable t => t a
empty TU Covariant Covariant Maybe (Construction Maybe) a
-> (TU Covariant Covariant Maybe (Construction Maybe) a
-> (<:.>) (Tagged 'Tail) Stack a)
-> ((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
:. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
:= (<:.>) (Tagged 'Tail) Stack a
forall s a. s -> a -> Product s a
:*: TU Covariant Covariant Maybe (Construction Maybe) a
-> (<:.>) (Tagged 'Tail) Stack a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (TU Covariant Covariant Maybe (Construction Maybe) a
-> (<:.>) (Tagged 'Tail) Stack a)
-> (TU Covariant Covariant Maybe (Construction Maybe) a
-> TU Covariant Covariant Maybe (Construction Maybe) a)
-> TU Covariant Covariant Maybe (Construction Maybe) a
-> (<:.>) (Tagged 'Tail) Stack a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction Maybe) a
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) a. Category m => m a a
identity
instance Deletable Stack where
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 (t :: * -> *) a. (Deletable t, Setoid a) => a -> t a -> t a
delete @Stack 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 {-# OVERLAPS #-} Semigroup (Construction Maybe a) where
Construct a
x Maybe (Construction Maybe a)
Nothing + :: Construction Maybe a
-> Construction Maybe a -> Construction Maybe a
+ Construction Maybe a
ys = 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)
-> Maybe (Construction Maybe a) -> Construction Maybe a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Construction Maybe a -> Maybe (Construction Maybe a)
forall a. a -> Maybe a
Just Construction Maybe a
ys
Construct a
x (Just Construction Maybe a
xs) + Construction Maybe a
ys = 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)
-> Construction Maybe a -> Construction Maybe a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Construction Maybe a
xs Construction Maybe a
-> Construction Maybe a -> Construction Maybe a
forall a. Semigroup a => a -> a -> a
+ Construction Maybe a
ys
instance Morphable Stack (Construction Maybe) where
type Morphing Stack (Construction Maybe) = Stack
morphing :: (<:.>) (Tagged Stack) (Construction Maybe) a
-> Morphing Stack (Construction Maybe) a
morphing = Construction Maybe a
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Maybe a
-> TU Covariant Covariant Maybe (Construction Maybe) a)
-> ((<:.>) (Tagged Stack) (Construction Maybe) a
-> Construction Maybe a)
-> (<:.>) (Tagged Stack) (Construction Maybe) a
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Maybe a <:= Tagged Stack
forall (t :: * -> *) a. Extractable t => a <:= t
extract (Construction Maybe a <:= Tagged Stack)
-> ((<:.>) (Tagged Stack) (Construction Maybe) a
-> Tagged Stack (Construction Maybe a))
-> (<:.>) (Tagged Stack) (Construction Maybe) a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged Stack) (Construction Maybe) a
-> Tagged Stack (Construction Maybe a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run
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 (Construction Maybe a <:= Tagged 'Head
forall (t :: * -> *) a. Extractable t => a <:= t
extract -> 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 Measurable Length (Construction Maybe) where
type Measural Length (Construction Maybe) a = Denumerator
measurement :: Tagged 'Length (Construction Maybe a)
-> Measural 'Length (Construction Maybe) a
measurement (Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct (Construction Maybe a -> (Maybe :. Construction Maybe) := a)
-> (Tagged 'Length (Construction Maybe a) -> Construction Maybe a)
-> Tagged 'Length (Construction Maybe a)
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged 'Length (Construction Maybe a) -> Construction Maybe a
forall (t :: * -> *) a. Extractable t => a <:= t
extract -> (Maybe :. Construction Maybe) := a
Nothing) = Denumerator
Measural 'Length (Construction Maybe) a
One
measurement (Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct (Construction Maybe a -> (Maybe :. Construction Maybe) := a)
-> (Tagged 'Length (Construction Maybe a) -> Construction Maybe a)
-> Tagged 'Length (Construction Maybe a)
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged 'Length (Construction Maybe a) -> Construction Maybe a
forall (t :: * -> *) a. Extractable t => a <:= t
extract -> Just Construction Maybe a
xs) = Denumerator
One Denumerator -> Denumerator -> Denumerator
forall a. Semigroup a => a -> a -> a
+ Construction Maybe a -> Measural 'Length (Construction Maybe) a
forall k (f :: k) (t :: * -> *) a.
Measurable f t =>
t a -> Measural f t a
measure @Length Construction Maybe a
xs
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
instance Substructure Tail (Construction Maybe) where
type Substructural Tail (Construction Maybe) = Stack
substructure :: Lens
((<:.>) (Tagged 'Tail) (Construction Maybe) a)
(Substructural 'Tail (Construction Maybe) a)
substructure (Construction Maybe a <:= Tagged 'Tail
forall (t :: * -> *) a. Extractable t => a <:= t
extract (Construction Maybe a <:= Tagged 'Tail)
-> ((<:.>) (Tagged 'Tail) (Construction Maybe) a
-> Tagged 'Tail (Construction Maybe a))
-> (<:.>) (Tagged 'Tail) (Construction Maybe) a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Tail) (Construction Maybe) a
-> Tagged 'Tail (Construction Maybe a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Construct a
x (Maybe :. Construction Maybe) := a
xs) =
(((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
:. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
:= (<:.>) (Tagged 'Tail) (Construction Maybe) a)
-> Store
(TU Covariant Covariant Maybe (Construction Maybe) a)
((<:.>) (Tagged 'Tail) (Construction Maybe) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
:. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
:= (<:.>) (Tagged 'Tail) (Construction Maybe) a)
-> Store
(TU Covariant Covariant Maybe (Construction Maybe) a)
((<:.>) (Tagged 'Tail) (Construction Maybe) a))
-> (((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
:. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
:= (<:.>) (Tagged 'Tail) (Construction Maybe) a)
-> Store
(TU Covariant Covariant Maybe (Construction Maybe) a)
((<:.>) (Tagged 'Tail) (Construction Maybe) a)
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ ((Maybe :. Construction Maybe) := a)
-> TU Covariant Covariant Maybe (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 (Maybe :. Construction Maybe) := a
xs TU Covariant Covariant Maybe (Construction Maybe) a
-> (TU Covariant Covariant Maybe (Construction Maybe) a
-> (<:.>) (Tagged 'Tail) (Construction Maybe) a)
-> ((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
:. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
:= (<:.>) (Tagged 'Tail) (Construction Maybe) a
forall s a. s -> a -> Product s a
:*: Construction Maybe a
-> (<:.>) (Tagged 'Tail) (Construction Maybe) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Maybe a
-> (<:.>) (Tagged 'Tail) (Construction Maybe) a)
-> (TU Covariant Covariant Maybe (Construction Maybe) a
-> Construction Maybe a)
-> TU Covariant Covariant Maybe (Construction Maybe) a
-> (<:.>) (Tagged 'Tail) (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
x (((Maybe :. Construction Maybe) := a) -> Construction Maybe a)
-> (TU Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a)
-> TU Covariant Covariant Maybe (Construction Maybe) a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run
type instance Zipper Stack = Tap ((:*:) <:.:> Stack)
instance {-# OVERLAPS #-} Extendable (Tap ((:*:) <:.:> Stack)) where
Tap ((:*:) <:.:> Stack) a
z =>> :: Tap ((:*:) <:.:> Stack) a
-> (Tap ((:*:) <:.:> Stack) a -> b) -> Tap ((:*:) <:.:> Stack) b
=>> Tap ((:*:) <:.:> Stack) a -> b
f = let move :: (Tap ((:*:) <:.:> Stack) a :=> Maybe)
-> TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap ((:*:) <:.:> Stack) a)
move Tap ((:*:) <:.:> Stack) a :=> Maybe
rtt = ((Maybe :. Construction Maybe) := Tap ((:*:) <:.:> Stack) a)
-> TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap ((:*:) <:.:> 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 ((:*:) <:.:> Stack) a)
-> TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap ((:*:) <:.:> Stack) a))
-> (Construction Maybe (Tap ((:*:) <:.:> Stack) a)
-> (Maybe :. Construction Maybe) := Tap ((:*:) <:.:> Stack) a)
-> Construction Maybe (Tap ((:*:) <:.:> Stack) a)
-> TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap ((:*:) <:.:> Stack) a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Maybe (Tap ((:*:) <:.:> Stack) a)
-> (Maybe :. Construction Maybe) := Tap ((:*:) <:.:> Stack) a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct (Construction Maybe (Tap ((:*:) <:.:> Stack) a)
-> TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap ((:*:) <:.:> Stack) a))
-> Construction Maybe (Tap ((:*:) <:.:> Stack) a)
-> TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap ((:*:) <:.:> Stack) a)
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Tap ((:*:) <:.:> Stack) a :=> Maybe
rtt (Tap ((:*:) <:.:> Stack) a :=> Maybe)
-> Tap ((:*:) <:.:> Stack) a :=> Construction Maybe
forall (t :: * -> *) a.
Covariant t =>
(a :=> t) -> a :=> Construction t
.-+ Tap ((:*:) <:.:> Stack) a
z
in Tap ((:*:) <:.:> Stack) a -> b
f (Tap ((:*:) <:.:> Stack) a -> b)
-> Tap ((:*:) <:.:> Stack) (Tap ((:*:) <:.:> Stack) a)
-> Tap ((:*:) <:.:> Stack) b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> Tap ((:*:) <:.:> Stack) a
-> (<:.:>) (:*:) Stack (Tap ((:*:) <:.:> Stack) a)
-> Tap ((:*:) <:.:> Stack) (Tap ((:*:) <:.:> Stack) a)
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap Tap ((:*:) <:.:> Stack) a
z (Product
(TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap ((:*:) <:.:> Stack) a))
(TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap ((:*:) <:.:> Stack) a))
-> (<:.:>) (:*:) Stack (Tap ((:*:) <:.:> Stack) a)
forall k k k k k (ct :: k) (cu :: k) (t :: k -> k)
(p :: k -> k -> *) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu t p u a
T_U (Product
(TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap ((:*:) <:.:> Stack) a))
(TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap ((:*:) <:.:> Stack) a))
-> (<:.:>) (:*:) Stack (Tap ((:*:) <:.:> Stack) a))
-> Product
(TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap ((:*:) <:.:> Stack) a))
(TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap ((:*:) <:.:> Stack) a))
-> (<:.:>) (:*:) Stack (Tap ((:*:) <:.:> Stack) a)
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ (Tap ((:*:) <:.:> Stack) a :=> Maybe)
-> TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap ((:*:) <:.:> Stack) a)
move ((<:.>) Maybe (Tap ((:*:) <:.:> Stack)) a
-> (Maybe :. Tap ((:*:) <:.:> Stack)) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run ((<:.>) Maybe (Tap ((:*:) <:.:> Stack)) a
-> (Maybe :. Tap ((:*:) <:.:> Stack)) := a)
-> (Tap ((:*:) <:.:> Stack) a
-> (<:.>) Maybe (Tap ((:*:) <:.:> Stack)) a)
-> Tap ((:*:) <:.:> Stack) a :=> Maybe
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. forall k (f :: k) (t :: * -> *). Morphable f t => t ~> Morphing f t
forall (t :: * -> *).
Morphable ('Rotate 'Left) t =>
t ~> Morphing ('Rotate 'Left) t
morph @(Rotate Left)) TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap ((:*:) <:.:> Stack) a)
-> TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap ((:*:) <:.:> Stack) a)
-> Product
(TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap ((:*:) <:.:> Stack) a))
(TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap ((:*:) <:.:> Stack) a))
forall s a. s -> a -> Product s a
:*: (Tap ((:*:) <:.:> Stack) a :=> Maybe)
-> TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap ((:*:) <:.:> Stack) a)
move ((<:.>) Maybe (Tap ((:*:) <:.:> Stack)) a
-> (Maybe :. Tap ((:*:) <:.:> Stack)) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run ((<:.>) Maybe (Tap ((:*:) <:.:> Stack)) a
-> (Maybe :. Tap ((:*:) <:.:> Stack)) := a)
-> (Tap ((:*:) <:.:> Stack) a
-> (<:.>) Maybe (Tap ((:*:) <:.:> Stack)) a)
-> Tap ((:*:) <:.:> Stack) a :=> Maybe
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. forall k (f :: k) (t :: * -> *). Morphable f t => t ~> Morphing f t
forall (t :: * -> *).
Morphable ('Rotate 'Right) t =>
t ~> Morphing ('Rotate 'Right) t
morph @(Rotate Right)))
instance Morphable (Rotate Left) (Tap ((:*:) <:.:> Stack)) where
type Morphing (Rotate Left) (Tap ((:*:) <:.:> Stack)) = Maybe <:.> Zipper Stack
morphing :: (<:.>) (Tagged ('Rotate 'Left)) (Tap ((:*:) <:.:> Stack)) a
-> Morphing ('Rotate 'Left) (Tap ((:*:) <:.:> Stack)) a
morphing (Tap ((:*:) <:.:> Stack) a <:= Tagged ('Rotate 'Left)
forall (t :: * -> *) a. Extractable t => a <:= t
extract (Tap ((:*:) <:.:> Stack) a <:= Tagged ('Rotate 'Left))
-> ((<:.>) (Tagged ('Rotate 'Left)) (Tap ((:*:) <:.:> Stack)) a
-> Tagged ('Rotate 'Left) (Tap ((:*:) <:.:> Stack) a))
-> (<:.>) (Tagged ('Rotate 'Left)) (Tap ((:*:) <:.:> Stack)) a
-> Tap ((:*:) <:.:> Stack) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged ('Rotate 'Left)) (Tap ((:*:) <:.:> Stack)) a
-> Tagged ('Rotate 'Left) (Tap ((:*:) <:.:> Stack) a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Tap a
x (T_U (Stack a
bs :*: Stack a
fs))) = ((Maybe :. Tap ((:*:) <:.:> Stack)) := a)
-> TU Covariant Covariant Maybe (Tap ((:*:) <:.:> 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 :. Tap ((:*:) <:.:> Stack)) := a)
-> TU Covariant Covariant Maybe (Tap ((:*:) <:.:> Stack)) a)
-> ((Maybe :. Tap ((:*:) <:.:> Stack)) := a)
-> TU Covariant Covariant Maybe (Tap ((:*:) <:.:> Stack)) a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ a
-> T_U Covariant Covariant Stack (:*:) Stack a
-> Tap ((:*:) <:.:> Stack) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (a
-> T_U Covariant Covariant Stack (:*:) Stack a
-> Tap ((:*:) <:.:> Stack) a)
-> T_U Covariant Covariant Stack (:*:) Stack a
-> a
-> Tap ((:*:) <:.:> Stack) a
forall a b c. (a -> b -> c) -> b -> a -> c
% (Product (Stack a) (Stack a)
-> T_U Covariant Covariant Stack (:*:) Stack a
forall k k k k k (ct :: k) (cu :: k) (t :: k -> k)
(p :: k -> k -> *) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu t p u a
T_U (Product (Stack a) (Stack a)
-> T_U Covariant Covariant Stack (:*:) Stack a)
-> Product (Stack a) (Stack a)
-> T_U Covariant Covariant Stack (:*:) Stack a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Stack a -> Substructural 'Tail Stack a
forall k (f :: k) (t :: * -> *).
Substructure f t =>
t ~> Substructural f t
subview @Tail Stack a
bs Stack a -> Stack a -> Product (Stack a) (Stack a)
forall s a. s -> a -> Product s a
:*: a -> Stack a -> Stack a
forall (t :: * -> *) a. Insertable t => a -> t a -> t a
insert a
x Stack a
fs) (a -> Tap ((:*:) <:.:> Stack) a)
-> Maybe a -> (Maybe :. Tap ((:*:) <:.:> Stack)) := a
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> Lens (Stack a) (Maybe a) -> Stack a -> Maybe a
forall src tgt. Lens src tgt -> src -> tgt
view (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
bs
instance Morphable (Rotate Right) (Tap ((:*:) <:.:> Stack)) where
type Morphing (Rotate Right) (Tap ((:*:) <:.:> Stack)) = Maybe <:.> Zipper Stack
morphing :: (<:.>) (Tagged ('Rotate 'Right)) (Tap ((:*:) <:.:> Stack)) a
-> Morphing ('Rotate 'Right) (Tap ((:*:) <:.:> Stack)) a
morphing (Tap ((:*:) <:.:> Stack) a <:= Tagged ('Rotate 'Right)
forall (t :: * -> *) a. Extractable t => a <:= t
extract (Tap ((:*:) <:.:> Stack) a <:= Tagged ('Rotate 'Right))
-> ((<:.>) (Tagged ('Rotate 'Right)) (Tap ((:*:) <:.:> Stack)) a
-> Tagged ('Rotate 'Right) (Tap ((:*:) <:.:> Stack) a))
-> (<:.>) (Tagged ('Rotate 'Right)) (Tap ((:*:) <:.:> Stack)) a
-> Tap ((:*:) <:.:> Stack) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged ('Rotate 'Right)) (Tap ((:*:) <:.:> Stack)) a
-> Tagged ('Rotate 'Right) (Tap ((:*:) <:.:> Stack) a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Tap a
x (T_U (Stack a
bs :*: Stack a
fs))) = ((Maybe :. Tap ((:*:) <:.:> Stack)) := a)
-> TU Covariant Covariant Maybe (Tap ((:*:) <:.:> 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 :. Tap ((:*:) <:.:> Stack)) := a)
-> TU Covariant Covariant Maybe (Tap ((:*:) <:.:> Stack)) a)
-> ((Maybe :. Tap ((:*:) <:.:> Stack)) := a)
-> TU Covariant Covariant Maybe (Tap ((:*:) <:.:> Stack)) a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ a
-> T_U Covariant Covariant Stack (:*:) Stack a
-> Tap ((:*:) <:.:> Stack) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (a
-> T_U Covariant Covariant Stack (:*:) Stack a
-> Tap ((:*:) <:.:> Stack) a)
-> T_U Covariant Covariant Stack (:*:) Stack a
-> a
-> Tap ((:*:) <:.:> Stack) a
forall a b c. (a -> b -> c) -> b -> a -> c
% (Product (Stack a) (Stack a)
-> T_U Covariant Covariant Stack (:*:) Stack a
forall k k k k k (ct :: k) (cu :: k) (t :: k -> k)
(p :: k -> k -> *) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu t p u a
T_U (Product (Stack a) (Stack a)
-> T_U Covariant Covariant Stack (:*:) Stack a)
-> Product (Stack a) (Stack a)
-> T_U Covariant Covariant Stack (:*:) 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 -> Product (Stack a) (Stack a)
forall s a. s -> a -> Product s a
:*: Stack a -> Substructural 'Tail Stack a
forall k (f :: k) (t :: * -> *).
Substructure f t =>
t ~> Substructural f t
subview @Tail Stack a
fs) (a -> Tap ((:*:) <:.:> Stack) a)
-> Maybe a -> (Maybe :. Tap ((:*:) <:.:> Stack)) := a
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> Lens (Stack a) (Maybe a) -> Stack a -> Maybe a
forall src tgt. Lens src tgt -> src -> tgt
view (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
fs
type instance Zipper (Construction Maybe) = Tap ((:*:) <:.:> Construction Maybe)
instance Morphable (Rotate Left) (Tap ((:*:) <:.:> Construction Maybe)) where
type Morphing (Rotate Left) (Tap ((:*:) <:.:> Construction Maybe)) = Maybe <:.> Zipper (Construction Maybe)
morphing :: (<:.>)
(Tagged ('Rotate 'Left)) (Tap ((:*:) <:.:> Construction Maybe)) a
-> Morphing
('Rotate 'Left) (Tap ((:*:) <:.:> Construction Maybe)) a
morphing (Tap ((:*:) <:.:> Construction Maybe) a <:= Tagged ('Rotate 'Left)
forall (t :: * -> *) a. Extractable t => a <:= t
extract (Tap ((:*:) <:.:> Construction Maybe) a <:= Tagged ('Rotate 'Left))
-> ((<:.>)
(Tagged ('Rotate 'Left)) (Tap ((:*:) <:.:> Construction Maybe)) a
-> Tagged ('Rotate 'Left) (Tap ((:*:) <:.:> Construction Maybe) a))
-> (<:.>)
(Tagged ('Rotate 'Left)) (Tap ((:*:) <:.:> Construction Maybe)) a
-> Tap ((:*:) <:.:> Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>)
(Tagged ('Rotate 'Left)) (Tap ((:*:) <:.:> Construction Maybe)) a
-> Tagged ('Rotate 'Left) (Tap ((:*:) <:.:> Construction Maybe) a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Tap a
x (T_U (Construction Maybe a
bs :*: Construction Maybe a
fs))) = ((Maybe :. Tap ((:*:) <:.:> Construction Maybe)) := a)
-> TU
Covariant Covariant Maybe (Tap ((:*:) <:.:> 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
(((Maybe :. Tap ((:*:) <:.:> Construction Maybe)) := a)
-> TU
Covariant Covariant Maybe (Tap ((:*:) <:.:> Construction Maybe)) a)
-> ((Maybe :. Tap ((:*:) <:.:> Construction Maybe)) := a)
-> TU
Covariant Covariant Maybe (Tap ((:*:) <:.:> Construction Maybe)) a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ a
-> T_U
Covariant
Covariant
(Construction Maybe)
(:*:)
(Construction Maybe)
a
-> Tap ((:*:) <:.:> 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) (T_U
Covariant
Covariant
(Construction Maybe)
(:*:)
(Construction Maybe)
a
-> Tap ((:*:) <:.:> Construction Maybe) a)
-> (Construction Maybe a
-> T_U
Covariant
Covariant
(Construction Maybe)
(:*:)
(Construction Maybe)
a)
-> Construction Maybe a
-> Tap ((:*:) <:.:> Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Product (Construction Maybe a) (Construction Maybe a)
-> T_U
Covariant
Covariant
(Construction Maybe)
(:*:)
(Construction Maybe)
a
forall k k k k k (ct :: k) (cu :: k) (t :: k -> k)
(p :: k -> k -> *) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu t p u a
T_U (Product (Construction Maybe a) (Construction Maybe a)
-> T_U
Covariant
Covariant
(Construction Maybe)
(:*:)
(Construction Maybe)
a)
-> (Construction Maybe a
-> Product (Construction Maybe a) (Construction Maybe a))
-> Construction Maybe a
-> T_U
Covariant
Covariant
(Construction Maybe)
(:*:)
(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
-> Product (Construction Maybe a) (Construction Maybe a)
forall s a. s -> a -> Product s 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 ((:*:) <:.:> Construction Maybe) a)
-> Maybe (Construction Maybe a)
-> (Maybe :. Tap ((:*:) <:.:> 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 Morphable (Rotate Right) (Tap ((:*:) <:.:> Construction Maybe)) where
type Morphing (Rotate Right) (Tap ((:*:) <:.:> Construction Maybe)) = Maybe <:.> Zipper (Construction Maybe)
morphing :: (<:.>)
(Tagged ('Rotate 'Right)) (Tap ((:*:) <:.:> Construction Maybe)) a
-> Morphing
('Rotate 'Right) (Tap ((:*:) <:.:> Construction Maybe)) a
morphing (Tap ((:*:) <:.:> Construction Maybe) a <:= Tagged ('Rotate 'Right)
forall (t :: * -> *) a. Extractable t => a <:= t
extract (Tap ((:*:) <:.:> Construction Maybe) a
<:= Tagged ('Rotate 'Right))
-> ((<:.>)
(Tagged ('Rotate 'Right)) (Tap ((:*:) <:.:> Construction Maybe)) a
-> Tagged
('Rotate 'Right) (Tap ((:*:) <:.:> Construction Maybe) a))
-> (<:.>)
(Tagged ('Rotate 'Right)) (Tap ((:*:) <:.:> Construction Maybe)) a
-> Tap ((:*:) <:.:> Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>)
(Tagged ('Rotate 'Right)) (Tap ((:*:) <:.:> Construction Maybe)) a
-> Tagged ('Rotate 'Right) (Tap ((:*:) <:.:> Construction Maybe) a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Tap a
x (T_U (Construction Maybe a
bs :*: Construction Maybe a
fs))) = ((Maybe :. Tap ((:*:) <:.:> Construction Maybe)) := a)
-> TU
Covariant Covariant Maybe (Tap ((:*:) <:.:> 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
(((Maybe :. Tap ((:*:) <:.:> Construction Maybe)) := a)
-> TU
Covariant Covariant Maybe (Tap ((:*:) <:.:> Construction Maybe)) a)
-> ((Maybe :. Tap ((:*:) <:.:> Construction Maybe)) := a)
-> TU
Covariant Covariant Maybe (Tap ((:*:) <:.:> Construction Maybe)) a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ a
-> T_U
Covariant
Covariant
(Construction Maybe)
(:*:)
(Construction Maybe)
a
-> Tap ((:*:) <:.:> 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) (T_U
Covariant
Covariant
(Construction Maybe)
(:*:)
(Construction Maybe)
a
-> Tap ((:*:) <:.:> Construction Maybe) a)
-> (Construction Maybe a
-> T_U
Covariant
Covariant
(Construction Maybe)
(:*:)
(Construction Maybe)
a)
-> Construction Maybe a
-> Tap ((:*:) <:.:> Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Product (Construction Maybe a) (Construction Maybe a)
-> T_U
Covariant
Covariant
(Construction Maybe)
(:*:)
(Construction Maybe)
a
forall k k k k k (ct :: k) (cu :: k) (t :: k -> k)
(p :: k -> k -> *) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu t p u a
T_U (Product (Construction Maybe a) (Construction Maybe a)
-> T_U
Covariant
Covariant
(Construction Maybe)
(:*:)
(Construction Maybe)
a)
-> (Construction Maybe a
-> Product (Construction Maybe a) (Construction Maybe a))
-> Construction Maybe a
-> T_U
Covariant
Covariant
(Construction Maybe)
(:*:)
(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
-> Product (Construction Maybe a) (Construction Maybe a)
forall s a. s -> a -> Product s a
:*:) (Construction Maybe a -> Tap ((:*:) <:.:> Construction Maybe) a)
-> Maybe (Construction Maybe a)
-> (Maybe :. Tap ((:*:) <:.:> 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