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

module Pandora.Paradigm.Structure.Stack where

import Pandora.Core.Functor (type (:.), 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.Traversable (Traversable)
import Pandora.Pattern.Functor.Extendable (Extendable ((=>>)))
import Pandora.Pattern.Functor.Bindable (Bindable (join))
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.Delta (Delta ((:^:)))
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 ((:*:)))
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, unite)
import Pandora.Paradigm.Schemes.TU (TU (TU), type (<:.>))
import Pandora.Paradigm.Structure.Ability.Nonempty (Nonempty)
import Pandora.Paradigm.Structure.Ability.Nullable (Nullable (null))
import Pandora.Paradigm.Structure.Ability.Zipper (Zipper)
import Pandora.Paradigm.Structure.Ability.Focusable (Focusable (Focusing, focusing), Location (Head), focus)
import Pandora.Paradigm.Structure.Ability.Insertable (Insertable (insert))
import Pandora.Paradigm.Structure.Ability.Measurable (Measurable (Measural, measurement), Scale (Length), measure)
import Pandora.Paradigm.Structure.Ability.Monotonic (Monotonic (reduce))
import Pandora.Paradigm.Structure.Ability.Rotatable (Rotatable (Rotational, rotation), rotate)
import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Substructural, substructure), Command (Delete), Segment (All, First, Tail), sub)

-- | 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 :: * -> * -> *) a b. Category m => m a b -> m a b
$ Maybe (Construction Maybe a) -> Stack a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU @Covariant @Covariant Maybe (Construction Maybe a)
xs Stack a -> Stack a -> Stack a
forall a. Semigroup a => a -> a -> a
+ Maybe (Construction Maybe a) -> Stack a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU @Covariant @Covariant Maybe (Construction Maybe a)
ys

instance Monoid (Stack a) where
	zero :: Stack a
zero = ((Maybe :. Construction Maybe) := a) -> Stack a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (Maybe :. Construction Maybe) := a
forall a. Maybe a
Nothing

instance Focusable Head Stack where
	type Focusing Head Stack a = Maybe a
	focusing :: Tagged 'Head (Stack a) :-. Focusing 'Head Stack a
focusing (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
& Lens (Stack a) (Stack a) -> Stack a -> Stack a
forall src tgt. Lens src tgt -> src -> tgt
view (forall k (f :: k) (t :: * -> *) a.
Substructure f t a =>
t a :-. Substructural f t a
forall (t :: * -> *) a.
Substructure 'Tail t a =>
t a :-. Substructural 'Tail t a
sub @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 -> Tagged 'Head (Stack a)
forall k (tag :: k) a. a -> Tagged tag a
Tag (Stack a -> Tagged 'Head (Stack a))
-> Stack a -> Tagged 'Head (Stack a)
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ forall k (f :: k) (t :: * -> *) a.
Substructure f t a =>
t a :-. Substructural f t a
forall (t :: * -> *) a.
Substructure 'Tail t a =>
t a :-. Substructural 'Tail t a
sub @Tail Lens (Stack a) (Stack a) -> Stack a -> Stack a
forall src tgt. Lens src tgt -> src -> tgt
^. Stack a
stack

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 (t :: * -> *) a. Interpreted t => Primary t a -> t a
unite (((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 a where
	type Substructural Tail Stack a = Stack a
	substructure :: Tagged 'Tail (Stack a) :-. Substructural 'Tail Stack a
substructure (Stack a -> Maybe (Construction Maybe a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Stack a -> Maybe (Construction Maybe a))
-> (Tagged 'Tail (Stack a) -> Stack 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
. Tagged 'Tail (Stack a) -> Stack a
forall (t :: * -> *) a. Extractable t => a <-| t
extract -> Just Construction Maybe a
ns) = Stack a |-> Tagged 'Tail
forall (t :: * -> *) a. Pointable t => a |-> t
point (Stack a |-> Tagged 'Tail)
-> (Construction Maybe a -> Stack a)
-> Construction Maybe a
-> Tagged 'Tail (Stack a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Maybe (Construction Maybe a) -> Stack a
forall (t :: * -> *) a. Interpreted t => Primary t a -> t a
unite (Maybe (Construction Maybe a) -> Stack a)
-> (Construction Maybe a -> Maybe (Construction Maybe a))
-> Construction Maybe a
-> Stack 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 -> Tagged 'Tail (Stack a))
-> Store (Stack a) (Construction Maybe a)
-> Store (Stack a) (Tagged 'Tail (Stack a))
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> Construction Maybe a :-. Substructural 'Tail (Construction Maybe) a
forall k (f :: k) (t :: * -> *) a.
Substructure f t a =>
t a :-. Substructural f t a
sub @Tail Construction Maybe a
ns
	substructure (Stack a -> Maybe (Construction Maybe a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Stack a -> Maybe (Construction Maybe a))
-> (Tagged 'Tail (Stack a) -> Stack 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
. Tagged 'Tail (Stack a) -> Stack a
forall (t :: * -> *) a. Extractable t => a <-| t
extract -> Maybe (Construction Maybe a)
Nothing) = (((:*:) (Stack a) :. (->) (Stack a)) := Tagged 'Tail (Stack a))
-> Store (Stack a) (Tagged 'Tail (Stack a))
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Stack a) :. (->) (Stack a)) := Tagged 'Tail (Stack a))
 -> Store (Stack a) (Tagged 'Tail (Stack a)))
-> (((:*:) (Stack a) :. (->) (Stack a)) := Tagged 'Tail (Stack a))
-> Store (Stack a) (Tagged 'Tail (Stack a))
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Primary Stack a -> Stack a
forall (t :: * -> *) a. Interpreted t => Primary t a -> t a
unite Primary Stack a
forall a. Maybe a
Nothing Stack a
-> (Stack a |-> Tagged 'Tail)
-> ((:*:) (Stack a) :. (->) (Stack a)) := Tagged 'Tail (Stack a)
forall s a. s -> a -> Product s a
:*: Stack a |-> Tagged 'Tail
forall (t :: * -> *) a. Pointable t => a |-> t
point (Stack a |-> Tagged 'Tail)
-> (Stack a -> Stack a) -> Stack a |-> Tagged 'Tail
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Stack a -> Stack a
forall (m :: * -> * -> *) a. Category m => m a a
identity

instance Setoid a => Substructure (Delete First) Stack a where
	type Substructural (Delete First) Stack a = a |-> Stack
	substructure :: Tagged ('Delete 'First) (Stack a)
:-. Substructural ('Delete 'First) Stack a
substructure (Stack a <-| Tagged ('Delete 'First)
forall (t :: * -> *) a. Extractable t => a <-| t
extract -> Stack a
xs) = (((:*:) (a -> Stack a) :. (->) (a -> Stack a))
 := Tagged ('Delete 'First) (Stack a))
-> Store (a -> Stack a) (Tagged ('Delete 'First) (Stack a))
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (a -> Stack a) :. (->) (a -> Stack a))
  := Tagged ('Delete 'First) (Stack a))
 -> Store (a -> Stack a) (Tagged ('Delete 'First) (Stack a)))
-> (((:*:) (a -> Stack a) :. (->) (a -> Stack a))
    := Tagged ('Delete 'First) (Stack a))
-> Store (a -> Stack a) (Tagged ('Delete 'First) (Stack a))
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ a -> Stack a -> Stack a
Setoid a => a -> Stack a -> Stack a
delete (a -> Stack a -> Stack a) -> Stack a -> a -> Stack a
forall a b c. (a -> b -> c) -> b -> a -> c
% Stack a
xs (a -> Stack a)
-> ((a -> Stack a) -> Tagged ('Delete 'First) (Stack a))
-> ((:*:) (a -> Stack a) :. (->) (a -> Stack a))
   := Tagged ('Delete 'First) (Stack a)
forall s a. s -> a -> Product s a
:*: (Stack a |-> Tagged ('Delete 'First)
forall (t :: * -> *) a. Pointable t => a |-> t
point Stack a
xs Tagged ('Delete 'First) (Stack a)
-> (a -> Stack a) -> Tagged ('Delete 'First) (Stack a)
forall a b. a -> b -> a
!) where

		delete :: Setoid a => a -> Stack a -> Stack a
		delete :: a -> Stack a -> Stack a
delete a
_ (TU Maybe (Construction Maybe a)
Nothing) = Maybe (Construction Maybe a) -> Stack a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU Maybe (Construction Maybe a)
forall a. Maybe a
Nothing
		delete a
x (TU (Just (Construct a
y Maybe (Construction Maybe a)
ys))) = a
x a -> a -> Boolean
forall a. Setoid a => a -> a -> Boolean
== a
y Boolean -> Stack a -> Stack a -> Stack a
forall a. Boolean -> a -> a -> a
? Maybe (Construction Maybe a) -> Stack a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU Maybe (Construction Maybe a)
ys
			(Stack a -> Stack a) -> Stack a -> Stack a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Construction Maybe a -> Stack a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Maybe a -> Stack a)
-> (Stack a -> Construction Maybe a) -> Stack a -> Stack a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Maybe (Construction Maybe a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
y (Maybe (Construction Maybe a) -> Construction Maybe a)
-> (Stack a -> Maybe (Construction Maybe a))
-> Stack a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Stack a -> Maybe (Construction Maybe a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Stack a -> Maybe (Construction Maybe a))
-> (Stack a -> Stack a) -> Stack a -> Maybe (Construction Maybe a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Stack a -> Stack a
Setoid a => a -> Stack a -> Stack a
delete a
x (Stack a -> Stack a) -> Stack a -> Stack a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Maybe (Construction Maybe a) -> Stack a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU Maybe (Construction Maybe a)
ys

filter :: forall a . Predicate a -> Stack a -> Stack a
filter :: Predicate a -> Stack a -> Stack a
filter (Predicate a -> Boolean
p) = ((Maybe :. Construction Maybe) := a) -> Stack a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (((Maybe :. Construction Maybe) := a) -> Stack a)
-> (Stack a -> (Maybe :. Construction Maybe) := a)
-> Stack a
-> Stack a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. ((Maybe :. Construction Maybe) := a)
<-| Product ((Maybe :. Construction Maybe) := a)
forall (t :: * -> *) a. Extractable t => a <-| t
extract
	(((Maybe :. Construction Maybe) := a)
 <-| Product ((Maybe :. Construction Maybe) := a))
-> (Stack a
    -> Product
         ((Maybe :. Construction Maybe) := a)
         ((Maybe :. Construction Maybe) := a))
-> Stack a
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. forall a.
Interpreted (State ((Maybe :. Nonempty Stack) := a)) =>
State ((Maybe :. Nonempty Stack) := a) a
-> Primary (State ((Maybe :. Nonempty Stack) := a)) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run @(State (Maybe :. Nonempty Stack := a)) (State
   ((Maybe :. Construction Maybe) := a)
   ((Maybe :. Construction Maybe) := a)
 -> ((Maybe :. Construction Maybe) := a)
 -> Product
      ((Maybe :. Construction Maybe) := a)
      ((Maybe :. Construction Maybe) := a))
-> ((Maybe :. Construction Maybe) := a)
-> State
     ((Maybe :. Construction Maybe) := a)
     ((Maybe :. Construction Maybe) := a)
-> Product
     ((Maybe :. Construction Maybe) := a)
     ((Maybe :. Construction Maybe) := a)
forall a b c. (a -> b -> c) -> b -> a -> c
% (Maybe :. Construction Maybe) := a
forall a. Maybe a
Nothing
	(State
   ((Maybe :. Construction Maybe) := a)
   ((Maybe :. Construction Maybe) := a)
 -> Product
      ((Maybe :. Construction Maybe) := a)
      ((Maybe :. Construction Maybe) := a))
-> (Stack a
    -> State
         ((Maybe :. Construction Maybe) := a)
         ((Maybe :. Construction Maybe) := a))
-> Stack a
-> Product
     ((Maybe :. Construction Maybe) := a)
     ((Maybe :. Construction Maybe) := a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (a
 -> ((Maybe :. Construction Maybe) := a)
 -> (Maybe :. Construction Maybe) := a)
-> Stack a
-> State
     ((Maybe :. Construction Maybe) := a)
     ((Maybe :. Construction Maybe) := a)
forall (t :: * -> *) s (u :: * -> *) a.
(Traversable t, Memorable s u) =>
(a -> s -> s) -> t a -> u s
fold (\a
now (Maybe :. Construction Maybe) := a
new -> a -> Boolean
p a
now Boolean
-> ((Maybe :. Construction Maybe) := a)
-> ((Maybe :. Construction Maybe) := a)
-> (Maybe :. Construction Maybe) := a
forall a. Boolean -> a -> a -> a
? Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall a. a -> Maybe a
Just (a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
now (Maybe :. Construction Maybe) := a
new) (((Maybe :. Construction Maybe) := a)
 -> (Maybe :. Construction Maybe) := a)
-> ((Maybe :. Construction Maybe) := a)
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ (Maybe :. Construction Maybe) := a
new)

-- | 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 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) a where
	type Substructural Tail (Construction Maybe) a = Stack a
	substructure :: Tagged 'Tail (Construction Maybe a)
:-. Substructural 'Tail (Construction Maybe) a
substructure (Construction Maybe a <-| Tagged 'Tail
forall (t :: * -> *) a. Extractable t => a <-| t
extract -> 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
$ Primary Stack a
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall (t :: * -> *) a. Interpreted t => Primary t a -> t a
unite Primary Stack a
(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
forall (t :: * -> *) a. Pointable t => a |-> t
point (Construction Maybe a |-> Tagged 'Tail)
-> (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

instance Setoid a => Substructure (Delete First) (Construction Maybe) a where
	type Substructural (Delete First) (Construction Maybe) a = a |-> Stack
	substructure :: Tagged ('Delete 'First) (Construction Maybe a)
:-. Substructural ('Delete 'First) (Construction Maybe) a
substructure (Construction Maybe a <-| Tagged ('Delete 'First)
forall (t :: * -> *) a. Extractable t => a <-| t
extract -> Construction Maybe a
xs) = (((:*:) (a -> Stack a) :. (->) (a -> Stack a))
 := Tagged ('Delete 'First) (Construction Maybe a))
-> Store
     (a -> Stack a) (Tagged ('Delete 'First) (Construction Maybe a))
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (a -> Stack a) :. (->) (a -> Stack a))
  := Tagged ('Delete 'First) (Construction Maybe a))
 -> Store
      (a -> Stack a) (Tagged ('Delete 'First) (Construction Maybe a)))
-> (((:*:) (a -> Stack a) :. (->) (a -> Stack a))
    := Tagged ('Delete 'First) (Construction Maybe a))
-> Store
     (a -> Stack a) (Tagged ('Delete 'First) (Construction Maybe a))
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ a -> Construction Maybe a -> Stack a
Setoid a => a -> Nonempty Stack a -> Stack a
delete (a -> Construction Maybe a -> Stack a)
-> Construction Maybe a -> a -> Stack a
forall a b c. (a -> b -> c) -> b -> a -> c
% Construction Maybe a
xs (a -> Stack a)
-> ((a -> Stack a)
    -> Tagged ('Delete 'First) (Construction Maybe a))
-> ((:*:) (a -> Stack a) :. (->) (a -> Stack a))
   := Tagged ('Delete 'First) (Construction Maybe a)
forall s a. s -> a -> Product s a
:*: (Construction Maybe a |-> Tagged ('Delete 'First)
forall (t :: * -> *) a. Pointable t => a |-> t
point Construction Maybe a
xs Tagged ('Delete 'First) (Construction Maybe a)
-> (a -> Stack a) -> Tagged ('Delete 'First) (Construction Maybe a)
forall a b. a -> b -> a
!) where

		delete :: Setoid a => a -> Nonempty Stack a -> Stack a
		delete :: a -> Nonempty Stack a -> Stack a
delete a
x (Construct y 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
? Primary Stack a -> Stack a
forall (t :: * -> *) a. Interpreted t => Primary t a -> t a
unite Primary Stack a
(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
$ ((Maybe :. Construction Maybe) := a) -> Stack a
forall (t :: * -> *) a. Interpreted t => Primary t a -> t a
unite (((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
y (((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
. Stack a -> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Stack a -> (Maybe :. Construction Maybe) := a)
-> (Construction Maybe a -> Stack a)
-> Construction Maybe a
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Nonempty Stack a -> Stack a
Setoid a => a -> Nonempty Stack a -> Stack a
delete a
x (Construction Maybe a -> Construction Maybe a)
-> ((Maybe :. Construction Maybe) := a)
-> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> (Maybe :. Construction Maybe) := a
ys

instance Setoid a => Substructure (Delete All) (Construction Maybe) a where
	type Substructural (Delete All) (Construction Maybe) a = a |-> Stack
	substructure :: Tagged ('Delete 'All) (Construction Maybe a)
:-. Substructural ('Delete 'All) (Construction Maybe) a
substructure (Construction Maybe a <-| Tagged ('Delete 'All)
forall (t :: * -> *) a. Extractable t => a <-| t
extract -> Construction Maybe a
xs) = (((:*:) (a -> Stack a) :. (->) (a -> Stack a))
 := Tagged ('Delete 'All) (Construction Maybe a))
-> Store
     (a -> Stack a) (Tagged ('Delete 'All) (Construction Maybe a))
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (a -> Stack a) :. (->) (a -> Stack a))
  := Tagged ('Delete 'All) (Construction Maybe a))
 -> Store
      (a -> Stack a) (Tagged ('Delete 'All) (Construction Maybe a)))
-> (((:*:) (a -> Stack a) :. (->) (a -> Stack a))
    := Tagged ('Delete 'All) (Construction Maybe a))
-> Store
     (a -> Stack a) (Tagged ('Delete 'All) (Construction Maybe a))
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ a -> Construction Maybe a -> Stack a
Setoid a => a -> Nonempty Stack a -> Stack a
delete (a -> Construction Maybe a -> Stack a)
-> Construction Maybe a -> a -> Stack a
forall a b c. (a -> b -> c) -> b -> a -> c
% Construction Maybe a
xs (a -> Stack a)
-> ((a -> Stack a) -> Tagged ('Delete 'All) (Construction Maybe a))
-> ((:*:) (a -> Stack a) :. (->) (a -> Stack a))
   := Tagged ('Delete 'All) (Construction Maybe a)
forall s a. s -> a -> Product s a
:*: (Construction Maybe a |-> Tagged ('Delete 'All)
forall (t :: * -> *) a. Pointable t => a |-> t
point Construction Maybe a
xs Tagged ('Delete 'All) (Construction Maybe a)
-> (a -> Stack a) -> Tagged ('Delete 'All) (Construction Maybe a)
forall a b. a -> b -> a
!) where

		delete :: Setoid a => a -> Nonempty Stack a -> Stack a
		delete :: a -> Nonempty Stack a -> Stack a
delete a
x (Construct y 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 (t :: * -> *) a. Interpreted t => Primary t a -> t a
unite (((Maybe :. Construction Maybe) := a) -> Stack a)
-> (((Maybe :. Maybe) := Construction Maybe a)
    -> (Maybe :. Construction Maybe) := a)
-> ((Maybe :. Maybe) := Construction Maybe a)
-> Stack a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. ((Maybe :. Maybe) := Construction Maybe a)
-> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a. Bindable t => ((t :. t) := a) -> t a
join (((Maybe :. Maybe) := Construction Maybe a) -> Stack a)
-> ((Maybe :. Maybe) := Construction Maybe a) -> Stack a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Stack a -> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Stack a -> (Maybe :. Construction Maybe) := a)
-> (Construction Maybe a -> Stack a)
-> Construction Maybe a
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Nonempty Stack a -> Stack a
Setoid a => a -> Nonempty Stack a -> Stack a
delete a
x (Construction Maybe a -> (Maybe :. Construction Maybe) := a)
-> ((Maybe :. Construction Maybe) := a)
-> (Maybe :. Maybe) := Construction Maybe a
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> (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
$ (((Maybe :. Construction Maybe) := a) -> Stack a
forall (t :: * -> *) a. Interpreted t => Primary t a -> t a
unite (((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
y (((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
. Stack a -> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Stack a -> (Maybe :. Construction Maybe) := a)
-> (Construction Maybe a -> Stack a)
-> Construction Maybe a
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Nonempty Stack a -> Stack a
Setoid a => a -> Nonempty Stack a -> Stack a
delete a
x (Construction Maybe a -> Construction Maybe a)
-> ((Maybe :. Construction Maybe) := a)
-> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> (Maybe :. Construction Maybe) := a
ys)

type instance Zipper Stack = Tap (Delta <:.> Stack)

instance {-# OVERLAPS #-} Extendable (Tap (Delta <:.> Stack)) where
	Tap (Delta <:.> Stack) a
z =>> :: Tap (Delta <:.> Stack) a
-> (Tap (Delta <:.> Stack) a -> b) -> Tap (Delta <:.> Stack) b
=>> Tap (Delta <:.> Stack) a -> b
f = let move :: (Tap (Delta <:.> Stack) a |-> Maybe)
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Tap (Delta <:.> Stack) a)
move Tap (Delta <:.> Stack) a |-> Maybe
rtt = ((Maybe :. Construction Maybe) := Tap (Delta <:.> Stack) a)
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Tap (Delta <:.> Stack) a)
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (((Maybe :. Construction Maybe) := Tap (Delta <:.> Stack) a)
 -> TU
      Covariant
      Covariant
      Maybe
      (Construction Maybe)
      (Tap (Delta <:.> Stack) a))
-> (Construction Maybe (Tap (Delta <:.> Stack) a)
    -> (Maybe :. Construction Maybe) := Tap (Delta <:.> Stack) a)
-> Construction Maybe (Tap (Delta <:.> Stack) a)
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Tap (Delta <:.> Stack) a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Maybe (Tap (Delta <:.> Stack) a)
-> (Maybe :. Construction Maybe) := Tap (Delta <:.> Stack) a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct (Construction Maybe (Tap (Delta <:.> Stack) a)
 -> TU
      Covariant
      Covariant
      Maybe
      (Construction Maybe)
      (Tap (Delta <:.> Stack) a))
-> Construction Maybe (Tap (Delta <:.> Stack) a)
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Tap (Delta <:.> Stack) a)
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Tap (Delta <:.> Stack) a |-> Maybe
rtt (Tap (Delta <:.> Stack) a |-> Maybe)
-> Tap (Delta <:.> Stack) a |-> Construction Maybe
forall (t :: * -> *) a.
Covariant t =>
(a |-> t) -> a |-> Construction t
.-+ Tap (Delta <:.> Stack) a
z
		in Tap (Delta <:.> Stack) a -> b
f (Tap (Delta <:.> Stack) a -> b)
-> Tap (Delta <:.> Stack) (Tap (Delta <:.> Stack) a)
-> Tap (Delta <:.> Stack) b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> Tap (Delta <:.> Stack) a
-> (<:.>) Delta Stack (Tap (Delta <:.> Stack) a)
-> Tap (Delta <:.> Stack) (Tap (Delta <:.> Stack) a)
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap Tap (Delta <:.> Stack) a
z (((Delta :. Stack) := Tap (Delta <:.> Stack) a)
-> (<:.>) Delta Stack (Tap (Delta <:.> Stack) a)
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (((Delta :. Stack) := Tap (Delta <:.> Stack) a)
 -> (<:.>) Delta Stack (Tap (Delta <:.> Stack) a))
-> ((Delta :. Stack) := Tap (Delta <:.> Stack) a)
-> (<:.>) Delta Stack (Tap (Delta <:.> Stack) a)
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ (Tap (Delta <:.> Stack) a |-> Maybe)
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Tap (Delta <:.> Stack) a)
move (forall k (f :: k) (t :: * -> *) a.
Rotatable f t =>
t a -> Rotational f t a
forall (t :: * -> *) a.
Rotatable 'Left t =>
t a -> Rotational 'Left t a
rotate @Left) TU
  Covariant
  Covariant
  Maybe
  (Construction Maybe)
  (Tap (Delta <:.> Stack) a)
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Tap (Delta <:.> Stack) a)
-> (Delta :. Stack) := Tap (Delta <:.> Stack) a
forall a. a -> a -> Delta a
:^: (Tap (Delta <:.> Stack) a |-> Maybe)
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Tap (Delta <:.> Stack) a)
move (forall k (f :: k) (t :: * -> *) a.
Rotatable f t =>
t a -> Rotational f t a
forall (t :: * -> *) a.
Rotatable 'Right t =>
t a -> Rotational 'Right t a
rotate @Right))

instance Rotatable Left (Tap (Delta <:.> Stack)) where
	type Rotational Left (Tap (Delta <:.> Stack)) a = Maybe :. Zipper Stack := a
	rotation :: Tagged 'Left (Tap (Delta <:.> Stack) a)
-> Rotational 'Left (Tap (Delta <:.> Stack)) a
rotation (Tap (Delta <:.> Stack) a <-| Tagged 'Left
forall (t :: * -> *) a. Extractable t => a <-| t
extract -> Tap a
x (TU (Stack a
bs :^: Stack a
fs))) = a
-> TU Covariant Covariant Delta Stack a -> Tap (Delta <:.> Stack) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (a
 -> TU Covariant Covariant Delta Stack a
 -> Tap (Delta <:.> Stack) a)
-> TU Covariant Covariant Delta Stack a
-> a
-> Tap (Delta <:.> Stack) a
forall a b c. (a -> b -> c) -> b -> a -> c
% (Delta (Stack a) -> TU Covariant Covariant Delta Stack a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (Delta (Stack a) -> TU Covariant Covariant Delta Stack a)
-> Delta (Stack a) -> TU Covariant Covariant Delta Stack a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ forall k (f :: k) (t :: * -> *) a.
Substructure f t a =>
t a :-. Substructural f t a
forall (t :: * -> *) a.
Substructure 'Tail t a =>
t a :-. Substructural 'Tail t a
sub @Tail (Stack a -> Store (Stack a) (Stack a)) -> Stack a -> Stack a
forall src tgt. Lens src tgt -> src -> tgt
^. Stack a
bs Stack a -> Stack a -> Delta (Stack a)
forall a. a -> a -> Delta a
:^: a -> Stack a -> Stack a
forall (t :: * -> *) a. Insertable t => a -> t a -> t a
insert a
x Stack a
fs) (a -> Tap (Delta <:.> Stack) a)
-> Maybe a -> Maybe (Tap (Delta <:.> Stack) a)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> forall k (f :: * -> k) (t :: * -> *) a.
Focusable f t =>
t a :-. Focusing f t a
forall (t :: * -> *) a.
Focusable 'Head t =>
t a :-. Focusing 'Head t a
focus @Head (Stack a -> Store (Maybe a) (Stack a)) -> Stack a -> Maybe a
forall src tgt. Lens src tgt -> src -> tgt
^. Stack a
bs

instance Rotatable Right (Tap (Delta <:.> Stack)) where
	type Rotational Right (Tap (Delta <:.> Stack)) a = Maybe :. Zipper Stack := a
	rotation :: Tagged 'Right (Tap (Delta <:.> Stack) a)
-> Rotational 'Right (Tap (Delta <:.> Stack)) a
rotation (Tap (Delta <:.> Stack) a <-| Tagged 'Right
forall (t :: * -> *) a. Extractable t => a <-| t
extract -> Tap a
x (TU (Stack a
bs :^: Stack a
fs))) = a
-> TU Covariant Covariant Delta Stack a -> Tap (Delta <:.> Stack) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (a
 -> TU Covariant Covariant Delta Stack a
 -> Tap (Delta <:.> Stack) a)
-> TU Covariant Covariant Delta Stack a
-> a
-> Tap (Delta <:.> Stack) a
forall a b c. (a -> b -> c) -> b -> a -> c
% (Delta (Stack a) -> TU Covariant Covariant Delta Stack a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (Delta (Stack a) -> TU Covariant Covariant Delta Stack a)
-> Delta (Stack a) -> TU Covariant Covariant Delta Stack a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ a -> Stack a -> Stack a
forall (t :: * -> *) a. Insertable t => a -> t a -> t a
insert a
x Stack a
bs Stack a -> Stack a -> Delta (Stack a)
forall a. a -> a -> Delta a
:^: forall k (f :: k) (t :: * -> *) a.
Substructure f t a =>
t a :-. Substructural f t a
forall (t :: * -> *) a.
Substructure 'Tail t a =>
t a :-. Substructural 'Tail t a
sub @Tail (Stack a -> Store (Stack a) (Stack a)) -> Stack a -> Stack a
forall src tgt. Lens src tgt -> src -> tgt
^. Stack a
fs) (a -> Tap (Delta <:.> Stack) a)
-> Maybe a -> Maybe (Tap (Delta <:.> Stack) a)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> forall k (f :: * -> k) (t :: * -> *) a.
Focusable f t =>
t a :-. Focusing f t a
forall (t :: * -> *) a.
Focusable 'Head t =>
t a :-. Focusing 'Head t a
focus @Head (Stack a -> Store (Maybe a) (Stack a)) -> Stack a -> Maybe a
forall src tgt. Lens src tgt -> src -> tgt
^. Stack a
fs

type instance Zipper (Construction Maybe) = Tap (Delta <:.> Construction Maybe)

instance Rotatable Left (Tap (Delta <:.> Construction Maybe)) where
	type Rotational Left (Tap (Delta <:.> Construction Maybe)) a = Maybe :. Zipper (Construction Maybe) := a
	rotation :: Tagged 'Left (Tap (Delta <:.> Construction Maybe) a)
-> Rotational 'Left (Tap (Delta <:.> Construction Maybe)) a
rotation (Tap (Delta <:.> Construction Maybe) a <-| Tagged 'Left
forall (t :: * -> *) a. Extractable t => a <-| t
extract -> Tap a
x (TU (Construction Maybe a
bs :^: Construction Maybe a
fs))) = a
-> TU Covariant Covariant Delta (Construction Maybe) a
-> Tap (Delta <:.> Construction Maybe) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (a <-| Construction Maybe
forall (t :: * -> *) a. Extractable t => a <-| t
extract Construction Maybe a
bs) (TU Covariant Covariant Delta (Construction Maybe) a
 -> Tap (Delta <:.> Construction Maybe) a)
-> (Construction Maybe a
    -> TU Covariant Covariant Delta (Construction Maybe) a)
-> Construction Maybe a
-> Tap (Delta <:.> Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Delta (Construction Maybe a)
-> TU Covariant Covariant Delta (Construction Maybe) a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (Delta (Construction Maybe a)
 -> TU Covariant Covariant Delta (Construction Maybe) a)
-> (Construction Maybe a -> Delta (Construction Maybe a))
-> Construction Maybe a
-> TU Covariant Covariant Delta (Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (Construction Maybe a
-> Construction Maybe a -> Delta (Construction Maybe a)
forall a. a -> a -> Delta a
:^: a -> Construction Maybe a -> Construction Maybe a
forall (t :: * -> *) a. Insertable t => a -> t a -> t a
insert a
x Construction Maybe a
fs) (Construction Maybe a -> Tap (Delta <:.> Construction Maybe) a)
-> Maybe (Construction Maybe a)
-> Maybe (Tap (Delta <:.> Construction Maybe) a)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> Construction Maybe a -> Maybe (Construction Maybe a)
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct Construction Maybe a
bs

instance Rotatable Right (Tap (Delta <:.> Construction Maybe)) where
	type Rotational Right (Tap (Delta <:.> Construction Maybe)) a = Maybe :. Zipper (Construction Maybe) := a
	rotation :: Tagged 'Right (Tap (Delta <:.> Construction Maybe) a)
-> Rotational 'Right (Tap (Delta <:.> Construction Maybe)) a
rotation (Tap (Delta <:.> Construction Maybe) a <-| Tagged 'Right
forall (t :: * -> *) a. Extractable t => a <-| t
extract -> Tap a
x (TU (Construction Maybe a
bs :^: Construction Maybe a
fs))) = a
-> TU Covariant Covariant Delta (Construction Maybe) a
-> Tap (Delta <:.> Construction Maybe) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (a <-| Construction Maybe
forall (t :: * -> *) a. Extractable t => a <-| t
extract Construction Maybe a
fs) (TU Covariant Covariant Delta (Construction Maybe) a
 -> Tap (Delta <:.> Construction Maybe) a)
-> (Construction Maybe a
    -> TU Covariant Covariant Delta (Construction Maybe) a)
-> Construction Maybe a
-> Tap (Delta <:.> Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Delta (Construction Maybe a)
-> TU Covariant Covariant Delta (Construction Maybe) a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (Delta (Construction Maybe a)
 -> TU Covariant Covariant Delta (Construction Maybe) a)
-> (Construction Maybe a -> Delta (Construction Maybe a))
-> Construction Maybe a
-> TU Covariant Covariant Delta (Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (a -> Construction Maybe a -> Construction Maybe a
forall (t :: * -> *) a. Insertable t => a -> t a -> t a
insert a
x Construction Maybe a
bs Construction Maybe a
-> Construction Maybe a -> Delta (Construction Maybe a)
forall a. a -> a -> Delta a
:^:) (Construction Maybe a -> Tap (Delta <:.> Construction Maybe) a)
-> Maybe (Construction Maybe a)
-> Maybe (Tap (Delta <:.> Construction Maybe) a)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> Construction Maybe a -> Maybe (Construction Maybe a)
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct Construction Maybe a
fs

instance Monotonic a (Maybe <:.> Construction Maybe := a) where
	reduce :: (a -> r -> r) -> r -> (Stack := a) -> r
reduce a -> r -> r
f r
r = (a -> r -> r) -> r -> ((Maybe :. Construction Maybe) := a) -> r
forall a e r. Monotonic a e => (a -> r -> r) -> r -> e -> r
reduce a -> r -> r
f r
r (((Maybe :. Construction Maybe) := a) -> r)
-> ((Stack := a) -> (Maybe :. Construction Maybe) := a)
-> (Stack := a)
-> r
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (Stack := a) -> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run