{-# OPTIONS_GHC -fno-warn-orphans #-}

module Pandora.Paradigm.Structure.Some.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 ((-=)))
import Pandora.Paradigm.Structure.Ability.Insertable (Insertable ((+=)))
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, Into), rotate)
import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Substructural, substructure), Segment (Tail), sub, subview)

-- | Linear data structure that serves as a collection of elements
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 :: * -> * -> *). Category m => m ~~> m
$ 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 :: * -> * -> *). Category m => m ~~> m
$ 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
x a -> Stack a -> Stack a
forall (t :: * -> *) a. Insertable t => a -> t a -> t a
+=) 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
	a
x += :: a -> Stack a -> Stack a
+= (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 :: * -> * -> *). Category m => m ~~> m
$ (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 :: * -> * -> *). Category m => m ~~> m
$ 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 :: * -> * -> *). Category m => m ~~> m
$ \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 :: * -> * -> *). Category m => m ~~> m
$ 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
	a
_ -= :: a -> Stack a -> Stack 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
	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 :: * -> * -> *). Category m => m ~~> m
$ 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
(-=) @Stack a
x (Stack a -> Stack a) -> Stack a -> Stack a
forall (m :: * -> * -> *). Category m => m ~~> m
$ 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 :: * -> * -> *). Category m => m ~~> m
$ (Maybe :. Construction Maybe) := a
new)

-- | Transform any traversable structure into a stack
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 :: * -> * -> *). Category m => m ~~> m
$ 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 :: * -> * -> *). Category m => m ~~> m
$ 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 (Into Stack) (Construction Maybe) where
	type Morphing (Into Stack) (Construction Maybe) = Stack
	morphing :: (<:.>) (Tagged ('Into Stack)) (Construction Maybe) a
-> Morphing ('Into 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 ('Into Stack)) (Construction Maybe) a
    -> Construction Maybe a)
-> (<:.>) (Tagged ('Into 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 ('Into Stack)
forall (t :: * -> *) a. Extractable t => a <:= t
extract (Construction Maybe a <:= Tagged ('Into Stack))
-> ((<:.>) (Tagged ('Into Stack)) (Construction Maybe) a
    -> Tagged ('Into Stack) (Construction Maybe a))
-> (<:.>) (Tagged ('Into Stack)) (Construction Maybe) a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged ('Into Stack)) (Construction Maybe) a
-> Tagged ('Into 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 :: * -> * -> *). Category m => m ~~> m
$ 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
	+= :: a -> Construction Maybe a -> Construction Maybe a
(+=) 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 :: * -> * -> *). Category m => m ~~> m
$ (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 :: * -> * -> *). Category m => m ~~> m
$ ((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 :: * -> * -> *). Category m => m ~~> m
$ 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 :: * -> * -> *). Category m => m ~~> m
$ (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 a (f :: a) (t :: * -> *).
Morphable ('Rotate f) t =>
t ~> Morphing ('Rotate f) t
forall (t :: * -> *).
Morphable ('Rotate 'Left) t =>
t ~> Morphing ('Rotate 'Left) t
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 a (f :: a) (t :: * -> *).
Morphable ('Rotate f) t =>
t ~> Morphing ('Rotate f) t
forall (t :: * -> *).
Morphable ('Rotate 'Right) t =>
t ~> Morphing ('Rotate 'Right) t
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 :: * -> * -> *). Category m => m ~~> m
$ 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 :: * -> * -> *). Category m => m ~~> m
$ 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
x a -> Stack a -> Stack a
forall (t :: * -> *) a. Insertable t => a -> t a -> t a
+= 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 :: * -> * -> *). Category m => m ~~> m
$ 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 :: * -> * -> *). Category m => m ~~> m
$ a
x a -> Stack a -> Stack a
forall (t :: * -> *) a. Insertable t => a -> t a -> t a
+= 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 :: * -> * -> *). Category m => m ~~> m
$ 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
x a -> Construction Maybe a -> Construction Maybe a
forall (t :: * -> *) a. Insertable t => a -> t a -> t a
+= 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 :: * -> * -> *). Category m => m ~~> m
$ 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
x a -> Construction Maybe a -> Construction Maybe a
forall (t :: * -> *) a. Insertable t => a -> t a -> t a
+= 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