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

import Pandora.Core.Functor (type (:.), type (<), type (>))
import Pandora.Core.Impliable (imply)
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category ((<--), (<---), (<----), (<-----), (<------), (-->), (--->), (---->), identity)
import Pandora.Pattern.Kernel (constant)
import Pandora.Pattern.Functor.Covariant (Covariant, Covariant ((<-|-), (<-|--), (<-|-|-)))
import Pandora.Pattern.Functor.Traversable (Traversable ((<<-)))
import Pandora.Pattern.Functor.Extendable (Extendable ((<<=)))
import Pandora.Pattern.Functor.Bindable (Bindable ((=<<), (==<<), (===<<), (====<<)))
import Pandora.Pattern.Functor.Adjoint (Adjoint ((|-)))
import Pandora.Pattern.Transformer.Liftable (lift)
import Pandora.Pattern.Transformer.Lowerable (lower)
import Pandora.Pattern.Object.Setoid (Setoid ((==), (?=)))
import Pandora.Pattern.Object.Semigroup (Semigroup ((+)))
import Pandora.Pattern.Object.Monoid (Monoid (zero))
import Pandora.Paradigm.Algebraic ((<-*-), (<-*--), (.-*-), (.-+-), (.:..), extract, point, empty, void)
import Pandora.Paradigm.Algebraic.Product ((:*:) ((:*:)), type (<:*:>), (<:*:>), attached)
import Pandora.Paradigm.Algebraic.Exponential ((%))
import Pandora.Paradigm.Algebraic ((<-|-<-|-))
import Pandora.Paradigm.Primary.Object.Boolean (Boolean (True))
import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Just, Nothing))
import Pandora.Paradigm.Primary.Functor.Exactly (Exactly (Exactly))
import Pandora.Paradigm.Primary.Functor.Predicate (Predicate (Predicate))
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.Reverse (Reverse (Reverse))
import Pandora.Paradigm.Primary ()
import Pandora.Paradigm.Inventory.Ability.Gettable (get)
import Pandora.Paradigm.Inventory.Ability.Settable (set)
import Pandora.Paradigm.Inventory.Ability.Modifiable (modify)
import Pandora.Paradigm.Inventory.Some.State (State, fold)
import Pandora.Paradigm.Inventory.Some.Store (Store (Store))
import Pandora.Paradigm.Inventory.Some.Optics (Convex, Obscure, Lens)
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run, (<~), (<~~~), (=#-))
import Pandora.Paradigm.Schemes.TT (TT (TT), type (<::>))
import Pandora.Paradigm.Schemes.TU (TU (TU))
import Pandora.Paradigm.Schemes.T_U (T_U (T_U), type (<:.:>))
import Pandora.Paradigm.Schemes.P_Q_T (P_Q_T (P_Q_T))
import Pandora.Paradigm.Structure.Ability.Nonempty (Nonempty)
import Pandora.Paradigm.Structure.Interface.Zipper (Zippable (Breadcrumbs), Zipper)
import Pandora.Paradigm.Structure.Ability.Monotonic (resolve)
import Pandora.Paradigm.Structure.Ability.Morphable (Morphable (Morphing, morphing)
	, Morph (Rotate, Into, Push, Pop, Delete, Find, Lookup, Element, Key)
	, Occurrence (All, First), premorph, rotate, item, filter, find, lookup, into)
import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Substance, substructure, sub), Segment (Root, Rest))
import Pandora.Paradigm.Structure.Interface.Stack (Stack (Popping, Pushing, Topping, push, pop, top))
import Pandora.Paradigm.Structure.Modification.Combinative (Combinative)
import Pandora.Paradigm.Structure.Modification.Comprehension (Comprehension (Comprehension))
import Pandora.Paradigm.Structure.Modification.Prefixed (Prefixed (Prefixed))
import Pandora.Paradigm.Structure.Modification.Tape (Tape)
import Pandora.Paradigm.Structure.Modification.Turnover (Turnover (Turnover))

-- | Linear data structure that serves as a collection of elements
type List = Maybe <::> Construction Maybe

instance Setoid a => Setoid (List a) where
	TT (Maybe :. Construction Maybe) > a
ls == :: List a -> List a -> Boolean
== TT (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 (List a) where
	TT Maybe (Construction Maybe a)
Nothing + :: List a -> List a -> List a
+ TT Maybe (Construction Maybe a)
ys = Maybe (Construction Maybe a) -> List a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT Maybe (Construction Maybe a)
ys
	TT (Just (Construct a
x Maybe (Construction Maybe a)
xs)) + TT Maybe (Construction Maybe a)
ys = Construction Maybe a -> List a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Maybe a -> List a)
-> (List a -> Construction Maybe a) -> List a -> List a
forall (m :: * -> * -> *) b c a.
Semigroupoid 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)
-> (List a -> Maybe (Construction Maybe a))
-> List a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. List a -> Maybe (Construction Maybe a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run
		(List a -> List a) -> List a -> List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Maybe (Construction Maybe a) -> List a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT @Covariant @Covariant Maybe (Construction Maybe a)
xs List a -> List a -> List a
forall a. Semigroup a => a -> a -> a
+ Maybe (Construction Maybe a) -> List a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT @Covariant @Covariant Maybe (Construction Maybe a)
ys

instance Monoid (List a) where
	zero :: List a
zero = List a
forall (t :: * -> *) a. Emptiable t => t a
empty

instance Morphable Push List where
	type Morphing Push List = Exactly <:.:> List > (->)
	morphing :: (<::>) (Tagged 'Push) List a -> Morphing 'Push List a
morphing ((<::>) (Tagged 'Push) List a -> List a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> List a
xs) = (Exactly a -> List a)
-> T_U Covariant Covariant (->) Exactly List a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((Exactly a -> List a)
 -> T_U Covariant Covariant (->) Exactly List a)
-> (Exactly a -> List a)
-> T_U Covariant Covariant (->) Exactly List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction Maybe a -> List a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Maybe a -> List a)
-> (Exactly a -> Construction Maybe a) -> Exactly a -> List a
forall (m :: * -> * -> *) b c a.
Semigroupoid 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
% List a -> (Maybe :. Construction Maybe) > a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run List a
xs) (a -> Construction Maybe a)
-> (Exactly a -> a) -> Exactly a -> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Exactly a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract

instance Morphable Pop List where
	type Morphing Pop List = List
	morphing :: (<::>) (Tagged 'Pop) List a -> Morphing 'Pop List a
morphing ((<::>) (Tagged 'Pop) List a -> List a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> List a
xs) = (Construction Maybe a -> (Maybe :. Construction Maybe) > a)
-> ((Maybe :. Construction Maybe) > a)
-> ((Maybe :. Construction Maybe) > a)
-> (Maybe :. Construction Maybe) > a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve Construction Maybe a -> (Maybe :. Construction Maybe) > a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) > a
deconstruct (Maybe :. Construction Maybe) > a
forall a. Maybe a
Nothing (Primary List a -> Primary List a) -> ((->) < List a) < List a
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < Primary t a) < Primary u b) -> (m < t a) < u b
=#- List a
xs

instance Morphable (Find Element) List where
	type Morphing (Find Element) List = Predicate <:.:> Maybe > (->)
	morphing :: (<::>) (Tagged ('Find 'Element)) List a
-> Morphing ('Find 'Element) List a
morphing (<::>) (Tagged ('Find 'Element)) List a
list = case TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) > a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (TT Covariant Covariant Maybe (Construction Maybe) a
 -> (Maybe :. Construction Maybe) > a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) > a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
--> (<::>) (Tagged ('Find 'Element)) List a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph (<::>) (Tagged ('Find 'Element)) List a
list of
		(Maybe :. Construction Maybe) > a
Nothing -> (Predicate a -> Maybe a)
-> T_U Covariant Covariant (->) Predicate Maybe a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((Predicate a -> Maybe a)
 -> T_U Covariant Covariant (->) Predicate Maybe a)
-> (Predicate a -> Maybe a)
-> T_U Covariant Covariant (->) Predicate Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \Predicate a
_ -> Maybe a
forall a. Maybe a
Nothing
		Just (Construct a
x (Maybe :. Construction Maybe) > a
xs) -> (Predicate a -> Maybe a)
-> T_U Covariant Covariant (->) Predicate Maybe a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((Predicate a -> Maybe a)
 -> T_U Covariant Covariant (->) Predicate Maybe a)
-> (Predicate a -> Maybe a)
-> T_U Covariant Covariant (->) Predicate Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \Predicate a
p ->
			(Predicate a
p Predicate a -> a -> Boolean
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~ a
x) Boolean -> Boolean -> Maybe a -> Maybe a -> Maybe a
forall a r. Setoid a => a -> a -> r -> r -> r
?= Boolean
True (Maybe a -> Maybe a -> Maybe a) -> Maybe a -> Maybe a -> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- a -> Maybe a
forall a. a -> Maybe a
Just a
x
				(Maybe a -> Maybe a) -> Maybe a -> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- forall a2.
Morphed ('Find 'Element) List ((Predicate <:.:> Maybe) > (->)) =>
Predicate a2 -> List a2 -> Maybe a2
forall a1 (mod :: a1) (struct :: * -> *) (result :: * -> *) a2.
Morphed ('Find mod) struct ((Predicate <:.:> result) > (->)) =>
Predicate a2 -> struct a2 -> result a2
find @Element @List @Maybe (Predicate a
 -> TT Covariant Covariant Maybe (Construction Maybe) a -> Maybe a)
-> Predicate a
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Predicate a
p (TT Covariant Covariant Maybe (Construction Maybe) a -> Maybe a)
-> TT Covariant Covariant Maybe (Construction Maybe) a -> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- ((Maybe :. Construction Maybe) > a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT (Maybe :. Construction Maybe) > a
xs

instance Morphable (Delete First) List where
	type Morphing (Delete First) List = Predicate <:.:> List > (->)
	morphing :: (<::>) (Tagged ('Delete 'First)) List a
-> Morphing ('Delete 'First) List a
morphing (<::>) (Tagged ('Delete 'First)) List a
list = case TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) > a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (TT Covariant Covariant Maybe (Construction Maybe) a
 -> (Maybe :. Construction Maybe) > a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) > a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
--> (<::>) (Tagged ('Delete 'First)) List a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph (<::>) (Tagged ('Delete 'First)) List a
list of
		(Maybe :. Construction Maybe) > a
Nothing -> (Predicate a
 -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> T_U Covariant Covariant (->) Predicate List a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((Predicate a
  -> TT Covariant Covariant Maybe (Construction Maybe) a)
 -> T_U Covariant Covariant (->) Predicate List a)
-> (Predicate a
    -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> T_U Covariant Covariant (->) Predicate List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- TT Covariant Covariant Maybe (Construction Maybe) a
-> Predicate a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant TT Covariant Covariant Maybe (Construction Maybe) a
forall (t :: * -> *) a. Emptiable t => t a
empty
		Just (Construct a
x (Maybe :. Construction Maybe) > a
xs) -> (Predicate a
 -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> T_U Covariant Covariant (->) Predicate List a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((Predicate a
  -> TT Covariant Covariant Maybe (Construction Maybe) a)
 -> T_U Covariant Covariant (->) Predicate List a)
-> (Predicate a
    -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> T_U Covariant Covariant (->) Predicate List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \Predicate a
p ->
			(Predicate a
p Predicate a -> a -> Boolean
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~ a
x) Boolean
-> Boolean
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall a r. Setoid a => a -> a -> r -> r -> r
?= Boolean
True (TT Covariant Covariant Maybe (Construction Maybe) a
 -> TT Covariant Covariant Maybe (Construction Maybe) a
 -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- ((Maybe :. Construction Maybe) > a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT (Maybe :. Construction Maybe) > a
xs
				(TT Covariant Covariant Maybe (Construction Maybe) a
 -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Construction Maybe a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Maybe a
 -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> (TT Covariant Covariant Maybe (Construction Maybe) a
    -> Construction Maybe a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Semigroupoid 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)
-> (TT Covariant Covariant Maybe (Construction Maybe) a
    -> (Maybe :. Construction Maybe) > a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) > a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (TT Covariant Covariant Maybe (Construction Maybe) a
 -> (Maybe :. Construction Maybe) > a)
-> (TT Covariant Covariant Maybe (Construction Maybe) a
    -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) > a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Predicate a
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall a1 (mod :: a1) (struct :: * -> *) a2.
Morphed ('Delete mod) struct ((Predicate <:.:> struct) > (->)) =>
Predicate a2 -> struct a2 -> struct a2
filter @First @List Predicate a
p (TT Covariant Covariant Maybe (Construction Maybe) a
 -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- ((Maybe :. Construction Maybe) > a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT (Maybe :. Construction Maybe) > a
xs

instance Morphable (Delete All) List where
	type Morphing (Delete All) List = Predicate <:.:> List > (->)
	morphing :: (<::>) (Tagged ('Delete 'All)) List a
-> Morphing ('Delete 'All) List a
morphing (<::>) (Tagged ('Delete 'All)) List a
list = case TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) > a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (TT Covariant Covariant Maybe (Construction Maybe) a
 -> (Maybe :. Construction Maybe) > a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) > a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- (<::>) (Tagged ('Delete 'All)) List a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph (<::>) (Tagged ('Delete 'All)) List a
list of
		(Maybe :. Construction Maybe) > a
Nothing -> (Predicate a
 -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> T_U Covariant Covariant (->) Predicate List a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((Predicate a
  -> TT Covariant Covariant Maybe (Construction Maybe) a)
 -> T_U Covariant Covariant (->) Predicate List a)
-> (Predicate a
    -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> T_U Covariant Covariant (->) Predicate List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- TT Covariant Covariant Maybe (Construction Maybe) a
-> Predicate a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant TT Covariant Covariant Maybe (Construction Maybe) a
forall (t :: * -> *) a. Emptiable t => t a
empty
		Just (Construct a
x (Maybe :. Construction Maybe) > a
xs) -> (Predicate a
 -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> T_U Covariant Covariant (->) Predicate List a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((Predicate a
  -> TT Covariant Covariant Maybe (Construction Maybe) a)
 -> T_U Covariant Covariant (->) Predicate List a)
-> (Predicate a
    -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> T_U Covariant Covariant (->) Predicate List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \Predicate a
p -> (Predicate a
p Predicate a -> a -> Boolean
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~ a
x) Boolean
-> Boolean
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall a r. Setoid a => a -> a -> r -> r -> r
?= Boolean
True
				(TT Covariant Covariant Maybe (Construction Maybe) a
 -> TT Covariant Covariant Maybe (Construction Maybe) a
 -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Predicate a
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall a1 (mod :: a1) (struct :: * -> *) a2.
Morphed ('Delete mod) struct ((Predicate <:.:> struct) > (->)) =>
Predicate a2 -> struct a2 -> struct a2
filter @All @List Predicate a
p (TT Covariant Covariant Maybe (Construction Maybe) a
 -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- ((Maybe :. Construction Maybe) > a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT (Maybe :. Construction Maybe) > a
xs
				(TT Covariant Covariant Maybe (Construction Maybe) a
 -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Construction Maybe a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Maybe a
 -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> (TT Covariant Covariant Maybe (Construction Maybe) a
    -> Construction Maybe a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Semigroupoid 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)
-> (TT Covariant Covariant Maybe (Construction Maybe) a
    -> (Maybe :. Construction Maybe) > a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) > a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (TT Covariant Covariant Maybe (Construction Maybe) a
 -> (Maybe :. Construction Maybe) > a)
-> (TT Covariant Covariant Maybe (Construction Maybe) a
    -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) > a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Predicate a
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall a1 (mod :: a1) (struct :: * -> *) a2.
Morphed ('Delete mod) struct ((Predicate <:.:> struct) > (->)) =>
Predicate a2 -> struct a2 -> struct a2
filter @All @List Predicate a
p (TT Covariant Covariant Maybe (Construction Maybe) a
 -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- ((Maybe :. Construction Maybe) > a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT (Maybe :. Construction Maybe) > a
xs

instance Stack List where
	type Topping List = Maybe
	type Popping List = List
	type Pushing List = List
	top :: Lens (Topping List) (List e) e
top = (List e -> Store (Maybe e) (List e))
-> P_Q_T (->) Store Maybe (List e) e
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T ((List e -> Store (Maybe e) (List e))
 -> P_Q_T (->) Store Maybe (List e) e)
-> (List e -> Store (Maybe e) (List e))
-> P_Q_T (->) Store Maybe (List e) e
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \List e
list -> case List e
list of
		TT Maybe (Construction Maybe e)
Nothing -> (((:*:) (Maybe e) :. (->) (Maybe e)) > List e)
-> Store (Maybe e) (List e)
forall s a. (((:*:) s :. (->) s) > a) -> Store s a
Store ((((:*:) (Maybe e) :. (->) (Maybe e)) > List e)
 -> Store (Maybe e) (List e))
-> (((:*:) (Maybe e) :. (->) (Maybe e)) > List e)
-> Store (Maybe e) (List e)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Maybe e
forall a. Maybe a
Nothing Maybe e
-> (Maybe e -> List e)
-> ((:*:) (Maybe e) :. (->) (Maybe e)) > List e
forall s a. s -> a -> s :*: a
:*: List e -> Maybe e -> List e
forall (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant List e
forall (t :: * -> *) a. Emptiable t => t a
empty
		TT (Just Construction Maybe e
xs) -> (((:*:) (Maybe e) :. (->) (Maybe e)) > List e)
-> Store (Maybe e) (List e)
forall s a. (((:*:) s :. (->) s) > a) -> Store s a
Store ((((:*:) (Maybe e) :. (->) (Maybe e)) > List e)
 -> Store (Maybe e) (List e))
-> (((:*:) (Maybe e) :. (->) (Maybe e)) > List e)
-> Store (Maybe e) (List e)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- e -> Maybe e
forall a. a -> Maybe a
Just (Construction Maybe e -> e
forall (t :: * -> *) a. Extractable t => t a -> a
extract Construction Maybe e
xs) Maybe e
-> (Maybe e -> List e)
-> ((:*:) (Maybe e) :. (->) (Maybe e)) > List e
forall s a. s -> a -> s :*: a
:*: \Maybe e
new -> case Maybe e
new of
			Maybe e
Nothing -> Maybe (Construction Maybe e) -> List e
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT (Maybe (Construction Maybe e) -> List e)
-> Maybe (Construction Maybe e) -> List e
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction Maybe e -> Maybe (Construction Maybe e)
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) > a
deconstruct Construction Maybe e
xs
			Just e
x -> Maybe (Construction Maybe e) -> List e
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT (Maybe (Construction Maybe e) -> List e)
-> Maybe (Construction Maybe e) -> List e
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- e -> Maybe (Construction Maybe e) -> Construction Maybe e
forall (t :: * -> *) a.
a -> ((t :. Construction t) > a) -> Construction t a
Construct e
x (Maybe (Construction Maybe e) -> Construction Maybe e)
-> (Construction Maybe e -> Maybe (Construction Maybe e))
-> Construction Maybe e
-> Construction Maybe e
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Maybe e -> Maybe (Construction Maybe e)
forall a. a -> Maybe a
Just (Construction Maybe e -> Construction Maybe e)
-> Maybe (Construction Maybe e) -> Maybe (Construction Maybe e)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- Construction Maybe e -> Maybe (Construction Maybe e)
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) > a
deconstruct Construction Maybe e
xs
	pop :: State (Popping List e) (Maybe e)
pop = (Nonempty List e
 -> State
      (TT Covariant Covariant Maybe (Construction Maybe) e) (Maybe e))
-> State
     (TT Covariant Covariant Maybe (Construction Maybe) e) (Maybe e)
-> ((Maybe :. Construction Maybe) > e)
-> State
     (TT Covariant Covariant Maybe (Construction Maybe) e) (Maybe e)
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve @(Nonempty List _) (\(Construct x xs) -> Maybe e
-> TT Covariant Covariant Maybe (Construction Maybe) e -> Maybe e
forall (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant (e -> Maybe e
forall a. a -> Maybe a
Just e
x) (TT Covariant Covariant Maybe (Construction Maybe) e -> Maybe e)
-> State
     (TT Covariant Covariant Maybe (Construction Maybe) e)
     (TT Covariant Covariant Maybe (Construction Maybe) e)
-> State
     (TT Covariant Covariant Maybe (Construction Maybe) e) (Maybe e)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- TT Covariant Covariant Maybe (Construction Maybe) e
-> State
     (TT Covariant Covariant Maybe (Construction Maybe) e)
     (TT Covariant Covariant Maybe (Construction Maybe) e)
forall k (i :: k) e r. Settable i => Setting i e r
set @State (((Maybe :. Construction Maybe) > e)
-> TT Covariant Covariant Maybe (Construction Maybe) e
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT (Maybe :. Construction Maybe) > e
xs)) (Maybe e
-> State
     (TT Covariant Covariant Maybe (Construction Maybe) e) (Maybe e)
forall (t :: * -> *) a. Pointable t => a -> t a
point Maybe e
forall a. Maybe a
Nothing) (((Maybe :. Construction Maybe) > e)
 -> State
      (TT Covariant Covariant Maybe (Construction Maybe) e) (Maybe e))
-> (TT Covariant Covariant Maybe (Construction Maybe) e
    -> (Maybe :. Construction Maybe) > e)
-> TT Covariant Covariant Maybe (Construction Maybe) e
-> State
     (TT Covariant Covariant Maybe (Construction Maybe) e) (Maybe e)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TT Covariant Covariant Maybe (Construction Maybe) e
-> (Maybe :. Construction Maybe) > e
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (TT Covariant Covariant Maybe (Construction Maybe) e
 -> State
      (TT Covariant Covariant Maybe (Construction Maybe) e) (Maybe e))
-> State
     (TT Covariant Covariant Maybe (Construction Maybe) e)
     (TT Covariant Covariant Maybe (Construction Maybe) e)
-> State
     (TT Covariant Covariant Maybe (Construction Maybe) e) (Maybe e)
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
==<< forall e r. Gettable State => Getting State e r
forall k (i :: k) e r. Gettable i => Getting i e r
get @State
	push :: e -> State (Pushing List e) e
push e
x = e -> State (TT Covariant Covariant Maybe (Construction Maybe) e) e
forall (t :: * -> *) a. Pointable t => a -> t a
point e
x State (TT Covariant Covariant Maybe (Construction Maybe) e) e
-> State
     (TT Covariant Covariant Maybe (Construction Maybe) e)
     (TT Covariant Covariant Maybe (Construction Maybe) e)
-> State (TT Covariant Covariant Maybe (Construction Maybe) e) e
forall (t :: * -> *) b a.
(Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) =>
t b -> t a -> t b
.-*- (TT Covariant Covariant Maybe (Construction Maybe) e
 -> TT Covariant Covariant Maybe (Construction Maybe) e)
-> State
     (TT Covariant Covariant Maybe (Construction Maybe) e)
     (TT Covariant Covariant Maybe (Construction Maybe) e)
forall k (i :: k) e r. Modifiable i => Modification i e r
modify @State (e :=:=> List
forall k (mod :: k) (struct :: * -> *) a.
Morphed mod struct ((Exactly <:.:> struct) > (->)) =>
a :=:=> struct
item @Push e
x)

instance Substructure Root List where
	type Substance Root List = Maybe
	substructure :: Lens (Substance 'Root List) ((<:.>) (Tagged 'Root) List a) a
substructure = ((<:.>) (Tagged 'Root) List a
 -> Store (Maybe a) ((<:.>) (Tagged 'Root) List a))
-> P_Q_T (->) Store Maybe ((<:.>) (Tagged 'Root) List a) a
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Root) List a
  -> Store (Maybe a) ((<:.>) (Tagged 'Root) List a))
 -> P_Q_T (->) Store Maybe ((<:.>) (Tagged 'Root) List a) a)
-> ((<:.>) (Tagged 'Root) List a
    -> Store (Maybe a) ((<:.>) (Tagged 'Root) List a))
-> P_Q_T (->) Store Maybe ((<:.>) (Tagged 'Root) List a) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(<:.>) (Tagged 'Root) List a
zipper -> case TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) > a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (TT Covariant Covariant Maybe (Construction Maybe) a
 -> (Maybe :. Construction Maybe) > a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) > a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
--> (<:.>) (Tagged 'Root) List a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged 'Root) List a
zipper of
		Just (Construct a
x (Maybe :. Construction Maybe) > a
xs) -> (((:*:) (Maybe a) :. (->) (Maybe a))
 > (<:.>) (Tagged 'Root) List a)
-> Store (Maybe a) ((<:.>) (Tagged 'Root) List a)
forall s a. (((:*:) s :. (->) s) > a) -> Store s a
Store ((((:*:) (Maybe a) :. (->) (Maybe a))
  > (<:.>) (Tagged 'Root) List a)
 -> Store (Maybe a) ((<:.>) (Tagged 'Root) List a))
-> (((:*:) (Maybe a) :. (->) (Maybe a))
    > (<:.>) (Tagged 'Root) List a)
-> Store (Maybe a) ((<:.>) (Tagged 'Root) List a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- a -> Maybe a
forall a. a -> Maybe a
Just a
x Maybe a
-> (Maybe a -> (<:.>) (Tagged 'Root) List a)
-> ((:*:) (Maybe a) :. (->) (Maybe a))
   > (<:.>) (Tagged 'Root) List a
forall s a. s -> a -> s :*: a
:*: TT Covariant Covariant Maybe (Construction Maybe) a
-> (<:.>) (Tagged 'Root) List a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (TT Covariant Covariant Maybe (Construction Maybe) a
 -> (<:.>) (Tagged 'Root) List a)
-> (Maybe a -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> Maybe a
-> (<:.>) (Tagged 'Root) List a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> Maybe a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve (Construction Maybe a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Maybe a
 -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> (a -> Construction Maybe a)
-> a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Semigroupoid 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
% (Maybe :. Construction Maybe) > a
xs)) TT Covariant Covariant Maybe (Construction Maybe) a
forall a. Monoid a => a
zero
		(Maybe :. Construction Maybe) > a
Nothing -> (((:*:) (Maybe a) :. (->) (Maybe a))
 > (<:.>) (Tagged 'Root) List a)
-> Store (Maybe a) ((<:.>) (Tagged 'Root) List a)
forall s a. (((:*:) s :. (->) s) > a) -> Store s a
Store ((((:*:) (Maybe a) :. (->) (Maybe a))
  > (<:.>) (Tagged 'Root) List a)
 -> Store (Maybe a) ((<:.>) (Tagged 'Root) List a))
-> (((:*:) (Maybe a) :. (->) (Maybe a))
    > (<:.>) (Tagged 'Root) List a)
-> Store (Maybe a) ((<:.>) (Tagged 'Root) List a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Maybe a
forall a. Maybe a
Nothing Maybe a
-> (Maybe a -> (<:.>) (Tagged 'Root) List a)
-> ((:*:) (Maybe a) :. (->) (Maybe a))
   > (<:.>) (Tagged 'Root) List a
forall s a. s -> a -> s :*: a
:*: TT Covariant Covariant Maybe (Construction Maybe) a
-> (<:.>) (Tagged 'Root) List a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (TT Covariant Covariant Maybe (Construction Maybe) a
 -> (<:.>) (Tagged 'Root) List a)
-> (Maybe a -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> Maybe a
-> (<:.>) (Tagged 'Root) List a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> Maybe a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve (Construction Maybe a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Maybe a
 -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> (a -> Construction Maybe a)
-> a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> Construction Maybe a
forall (t :: * -> *) a. Pointable t => a -> t a
point) TT Covariant Covariant Maybe (Construction Maybe) a
forall a. Monoid a => a
zero

instance Substructure Rest List where
	type Substance Rest List = List
	substructure :: Lens (Substance 'Rest List) ((<:.>) (Tagged 'Rest) List a) a
substructure = ((<:.>) (Tagged 'Rest) List a
 -> Store
      (TT Covariant Covariant Maybe (Construction Maybe) a)
      ((<:.>) (Tagged 'Rest) List a))
-> P_Q_T (->) Store List ((<:.>) (Tagged 'Rest) List a) a
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Rest) List a
  -> Store
       (TT Covariant Covariant Maybe (Construction Maybe) a)
       ((<:.>) (Tagged 'Rest) List a))
 -> P_Q_T (->) Store List ((<:.>) (Tagged 'Rest) List a) a)
-> ((<:.>) (Tagged 'Rest) List a
    -> Store
         (TT Covariant Covariant Maybe (Construction Maybe) a)
         ((<:.>) (Tagged 'Rest) List a))
-> P_Q_T (->) Store List ((<:.>) (Tagged 'Rest) List a) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(<:.>) (Tagged 'Rest) List a
source -> case TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) > a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (TT Covariant Covariant Maybe (Construction Maybe) a
 -> (Maybe :. Construction Maybe) > a)
-> ((<:.>) (Tagged 'Rest) List a
    -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> (<:.>) (Tagged 'Rest) List a
-> (Maybe :. Construction Maybe) > a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Rest) List a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower ((<:.>) (Tagged 'Rest) List a -> (Maybe :. Construction Maybe) > a)
-> (<:.>) (Tagged 'Rest) List a
-> (Maybe :. Construction Maybe) > a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:.>) (Tagged 'Rest) List a
source of
		Just Construction Maybe a
ns -> TT Covariant Covariant Maybe (Construction Maybe) a
-> (<:.>) (Tagged 'Rest) List a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (TT Covariant Covariant Maybe (Construction Maybe) a
 -> (<:.>) (Tagged 'Rest) List a)
-> (Construction Maybe a
    -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> Construction Maybe a
-> (<:.>) (Tagged 'Rest) List a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
forall (t :: (* -> *) -> * -> *) (u :: * -> *) a.
(Liftable (->) t, Covariant (->) (->) u) =>
u a -> t u a
lift @(->) (Construction Maybe a -> (<:.>) (Tagged 'Rest) List a)
-> Store
     (TT Covariant Covariant Maybe (Construction Maybe) a)
     (Construction Maybe a)
-> Store
     (TT Covariant Covariant Maybe (Construction Maybe) a)
     ((<:.>) (Tagged 'Rest) List a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- P_Q_T (->) Store List (Construction Maybe a) a
-> Construction Maybe a
-> Store
     (TT Covariant Covariant Maybe (Construction Maybe) a)
     (Construction Maybe a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Rest structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Rest structure
sub @Rest) Construction Maybe a
ns
		(Maybe :. Construction Maybe) > a
Nothing -> (((:*:) (TT Covariant Covariant Maybe (Construction Maybe) a)
  :. (->) (TT Covariant Covariant Maybe (Construction Maybe) a))
 > (<:.>) (Tagged 'Rest) List a)
-> Store
     (TT Covariant Covariant Maybe (Construction Maybe) a)
     ((<:.>) (Tagged 'Rest) List a)
forall s a. (((:*:) s :. (->) s) > a) -> Store s a
Store ((((:*:) (TT Covariant Covariant Maybe (Construction Maybe) a)
   :. (->) (TT Covariant Covariant Maybe (Construction Maybe) a))
  > (<:.>) (Tagged 'Rest) List a)
 -> Store
      (TT Covariant Covariant Maybe (Construction Maybe) a)
      ((<:.>) (Tagged 'Rest) List a))
-> (((:*:) (TT Covariant Covariant Maybe (Construction Maybe) a)
     :. (->) (TT Covariant Covariant Maybe (Construction Maybe) a))
    > (<:.>) (Tagged 'Rest) List a)
-> Store
     (TT Covariant Covariant Maybe (Construction Maybe) a)
     ((<:.>) (Tagged 'Rest) List a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- TT Covariant Covariant Maybe (Construction Maybe) a
forall a. Monoid a => a
zero TT Covariant Covariant Maybe (Construction Maybe) a
-> (TT Covariant Covariant Maybe (Construction Maybe) a
    -> (<:.>) (Tagged 'Rest) List a)
-> ((:*:) (TT Covariant Covariant Maybe (Construction Maybe) a)
    :. (->) (TT Covariant Covariant Maybe (Construction Maybe) a))
   > (<:.>) (Tagged 'Rest) List a
forall s a. s -> a -> s :*: a
:*: TT Covariant Covariant Maybe (Construction Maybe) a
-> (<:.>) (Tagged 'Rest) List a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (TT Covariant Covariant Maybe (Construction Maybe) a
 -> (<:.>) (Tagged 'Rest) List a)
-> (TT Covariant Covariant Maybe (Construction Maybe) a
    -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> (<:.>) (Tagged 'Rest) List a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) a. Category m => m a a
identity

-- | Transform any traversable structure into a list
linearize :: forall t a . Traversable (->) (->) t => t a -> List a
linearize :: t a -> List a
linearize = ((Maybe :. Construction Maybe) > a) -> List a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT (((Maybe :. Construction Maybe) > a) -> List a)
-> (t a -> (Maybe :. Construction Maybe) > a) -> t a -> List a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (((Maybe :. Construction Maybe) > a)
 :*: ((Maybe :. Construction Maybe) > a))
-> (Maybe :. Construction Maybe) > a
forall (t :: * -> *) a. Extractable t => t a -> a
extract ((((Maybe :. Construction Maybe) > a)
  :*: ((Maybe :. Construction Maybe) > a))
 -> (Maybe :. Construction Maybe) > a)
-> (t a
    -> ((Maybe :. Construction Maybe) > a)
       :*: ((Maybe :. Construction Maybe) > a))
-> t a
-> (Maybe :. Construction Maybe) > a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (forall a.
Interpreted (->) (State ((Maybe :. Nonempty List) > a)) =>
((->) < State ((Maybe :. Nonempty List) > a) a)
< Primary (State ((Maybe :. Nonempty List) > a)) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run @(->) @(State (Maybe :. Nonempty List > a)) (State
   ((Maybe :. Construction Maybe) > a)
   ((Maybe :. Construction Maybe) > a)
 -> ((Maybe :. Construction Maybe) > a)
 -> ((Maybe :. Construction Maybe) > a)
    :*: ((Maybe :. Construction Maybe) > a))
-> ((Maybe :. Construction Maybe) > a)
-> State
     ((Maybe :. Construction Maybe) > a)
     ((Maybe :. Construction Maybe) > a)
-> ((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)
 -> ((Maybe :. Construction Maybe) > a)
    :*: ((Maybe :. Construction Maybe) > a))
-> (t a
    -> State
         ((Maybe :. Construction Maybe) > a)
         ((Maybe :. Construction Maybe) > a))
-> t a
-> ((Maybe :. Construction Maybe) > a)
   :*: ((Maybe :. Construction Maybe) > a)
forall (m :: * -> * -> *) b c a.
Semigroupoid 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 (target :: * -> * -> *) (v :: * -> * -> *) a c d b.
(Covariant (->) target (v a), Semigroupoid v) =>
v c d -> target (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)

----------------------------------------- Non-empty list -------------------------------------------

type instance Nonempty List = Construction Maybe

instance {-# OVERLAPS #-} Semigroup (Construction Maybe a) where
	Construct a
x Maybe (Construction Maybe a)
Nothing + :: Construction Maybe a
-> Construction Maybe a -> Construction Maybe a
+ Construction Maybe a
ys = a -> Maybe (Construction Maybe a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) > a) -> Construction t a
Construct a
x (Maybe (Construction Maybe a) -> Construction Maybe a)
-> Maybe (Construction Maybe a) -> Construction Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction Maybe a -> Maybe (Construction Maybe a)
forall a. a -> Maybe a
Just Construction Maybe a
ys
	Construct a
x (Just Construction Maybe a
xs) + Construction Maybe a
ys = a -> Maybe (Construction Maybe a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) > a) -> Construction t a
Construct a
x (Maybe (Construction Maybe a) -> Construction Maybe a)
-> (Construction Maybe a -> Maybe (Construction Maybe a))
-> Construction Maybe a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Maybe a -> Maybe (Construction Maybe a)
forall a. a -> Maybe a
Just (Construction Maybe a -> Construction Maybe a)
-> Construction Maybe a -> Construction Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction Maybe a
xs Construction Maybe a
-> Construction Maybe a -> Construction Maybe a
forall a. Semigroup a => a -> a -> a
+ Construction Maybe a
ys

instance Morphable (Find Element) (Construction Maybe) where
	type Morphing (Find Element) (Construction Maybe) = Predicate <:.:> Maybe > (->)
	morphing :: (<::>) (Tagged ('Find 'Element)) (Construction Maybe) a
-> Morphing ('Find 'Element) (Construction Maybe) a
morphing ((<::>) (Tagged ('Find 'Element)) (Construction Maybe) a
-> Construction Maybe a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Construct a
x (Maybe :. Construction Maybe) > a
xs) = (Predicate a -> Maybe a)
-> T_U Covariant Covariant (->) Predicate Maybe a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((Predicate a -> Maybe a)
 -> T_U Covariant Covariant (->) Predicate Maybe a)
-> (Predicate a -> Maybe a)
-> T_U Covariant Covariant (->) Predicate Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \Predicate a
p -> (Predicate a
p Predicate a -> a -> Boolean
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~ a
x) Boolean -> Boolean -> Maybe a -> Maybe a -> Maybe a
forall a r. Setoid a => a -> a -> r -> r -> r
?= Boolean
True (Maybe a -> Maybe a -> Maybe a) -> Maybe a -> Maybe a -> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<----- a -> Maybe a
forall a. a -> Maybe a
Just a
x
		(Maybe a -> Maybe a) -> Maybe a -> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<----- forall a2.
Morphed
  ('Find 'Element)
  (Nonempty List)
  ((Predicate <:.:> Maybe) > (->)) =>
Predicate a2 -> Nonempty List a2 -> Maybe a2
forall a1 (mod :: a1) (struct :: * -> *) (result :: * -> *) a2.
Morphed ('Find mod) struct ((Predicate <:.:> result) > (->)) =>
Predicate a2 -> struct a2 -> result a2
find @Element @(Nonempty List) @Maybe (Predicate a -> Construction Maybe a -> Maybe a)
-> Predicate a -> Construction Maybe a -> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Predicate a
p (Construction Maybe a -> Maybe a)
-> ((Maybe :. Construction Maybe) > a) -> Maybe a
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
===<< (Maybe :. Construction Maybe) > a
xs

instance Morphable (Into List) (Construction Maybe) where
	type Morphing (Into List) (Construction Maybe) = List
	morphing :: (<::>) (Tagged ('Into List)) (Construction Maybe) a
-> Morphing ('Into List) (Construction Maybe) a
morphing = Construction Maybe a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Maybe a
 -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> ((<::>) (Tagged ('Into List)) (Construction Maybe) a
    -> Construction Maybe a)
-> (<::>) (Tagged ('Into List)) (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>) (Tagged ('Into List)) (Construction Maybe) a
-> Construction Maybe a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph

instance Morphable (Into List) (Construction Maybe <::> Maybe) where
	type Morphing (Into List) (Construction Maybe <::> Maybe) = List
	morphing :: (<::>) (Tagged ('Into List)) (Construction Maybe <::> Maybe) a
-> Morphing ('Into List) (Construction Maybe <::> Maybe) a
morphing (<::>) (Tagged ('Into List)) (Construction Maybe <::> Maybe) a
nonempty_list_with_maybe_elements = case (<::>) (Construction Maybe) Maybe a
-> (Construction Maybe :. Maybe) > a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run ((<::>) (Construction Maybe) Maybe a
 -> (Construction Maybe :. Maybe) > a)
-> ((<::>) (Tagged ('Into List)) (Construction Maybe <::> Maybe) a
    -> (<::>) (Construction Maybe) Maybe a)
-> (<::>) (Tagged ('Into List)) (Construction Maybe <::> Maybe) a
-> (Construction Maybe :. Maybe) > a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>) (Tagged ('Into List)) (Construction Maybe <::> Maybe) a
-> (<::>) (Construction Maybe) Maybe a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph ((<::>) (Tagged ('Into List)) (Construction Maybe <::> Maybe) a
 -> (Construction Maybe :. Maybe) > a)
-> (<::>) (Tagged ('Into List)) (Construction Maybe <::> Maybe) a
-> (Construction Maybe :. Maybe) > a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
---> (<::>) (Tagged ('Into List)) (Construction Maybe <::> Maybe) a
nonempty_list_with_maybe_elements of
		Construct (Just a
x) (Just (Construction Maybe :. Maybe) > a
xs) -> a :=:=> List
forall k (mod :: k) (struct :: * -> *) a.
Morphed mod struct ((Exactly <:.:> struct) > (->)) =>
a :=:=> struct
item @Push a
x (TT Covariant Covariant Maybe (Construction Maybe) a
 -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
--> forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
forall (struct :: * -> *).
Morphable ('Into List) struct =>
struct ~> Morphing ('Into List) struct
into @List ((<::>) (Construction Maybe) Maybe a
 -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> (<::>) (Construction Maybe) Maybe a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
--> ((Construction Maybe :. Maybe) > a)
-> (<::>) (Construction Maybe) Maybe a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT @Covariant @Covariant (Construction Maybe :. Maybe) > a
xs
		Construct (Just a
x) Maybe ((Construction Maybe :. Maybe) > a)
Nothing -> a -> TT Covariant Covariant Maybe (Construction Maybe) a
forall (t :: * -> *) a. Pointable t => a -> t a
point a
x
		Construct Maybe a
Nothing (Just (Construction Maybe :. Maybe) > a
xs) -> forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
forall (struct :: * -> *).
Morphable ('Into List) struct =>
struct ~> Morphing ('Into List) struct
into @List ((<::>) (Construction Maybe) Maybe a
 -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> (<::>) (Construction Maybe) Maybe a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
--> ((Construction Maybe :. Maybe) > a)
-> (<::>) (Construction Maybe) Maybe a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT @Covariant @Covariant (Construction Maybe :. Maybe) > a
xs
		Construct Maybe a
Nothing Maybe ((Construction Maybe :. Maybe) > a)
Nothing -> Morphing ('Into List) (Construction Maybe <::> Maybe) a
forall (t :: * -> *) a. Emptiable t => t a
empty

instance Morphable Push (Construction Maybe) where
	type Morphing Push (Construction Maybe) = Exactly <:.:> Construction Maybe > (->)
	morphing :: (<::>) (Tagged 'Push) (Construction Maybe) a
-> Morphing 'Push (Construction Maybe) a
morphing ((<::>) (Tagged 'Push) (Construction Maybe) a
-> Construction Maybe a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Construction Maybe a
xs) = (Exactly a -> Construction Maybe a)
-> T_U Covariant Covariant (->) Exactly (Construction Maybe) a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((Exactly a -> Construction Maybe a)
 -> T_U Covariant Covariant (->) Exactly (Construction Maybe) a)
-> (Exactly a -> Construction Maybe a)
-> T_U Covariant Covariant (->) Exactly (Construction Maybe) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(Exactly 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)
-> ((Maybe :. Construction Maybe) > a) -> Construction Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction Maybe a -> (Maybe :. Construction Maybe) > a
forall a. a -> Maybe a
Just Construction Maybe a
xs

instance Stack (Construction Maybe) where
	type Topping (Construction Maybe) = Exactly
	type Popping (Construction Maybe) = Construction Maybe
	type Pushing (Construction Maybe) = Construction Maybe
	top :: Lens (Topping (Construction Maybe)) (Construction Maybe e) e
top = (Construction Maybe e -> Store (Exactly e) (Construction Maybe e))
-> P_Q_T (->) Store Exactly (Construction Maybe e) e
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T ((Construction Maybe e -> Store (Exactly e) (Construction Maybe e))
 -> P_Q_T (->) Store Exactly (Construction Maybe e) e)
-> (Construction Maybe e
    -> Store (Exactly e) (Construction Maybe e))
-> P_Q_T (->) Store Exactly (Construction Maybe e) e
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \Construction Maybe e
xs -> (((:*:) (Exactly e) :. (->) (Exactly e)) > Construction Maybe e)
-> Store (Exactly e) (Construction Maybe e)
forall s a. (((:*:) s :. (->) s) > a) -> Store s a
Store ((((:*:) (Exactly e) :. (->) (Exactly e)) > Construction Maybe e)
 -> Store (Exactly e) (Construction Maybe e))
-> (((:*:) (Exactly e) :. (->) (Exactly e)) > Construction Maybe e)
-> Store (Exactly e) (Construction Maybe e)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- e -> Exactly e
forall a. a -> Exactly a
Exactly (Construction Maybe e -> e
forall (t :: * -> *) a. Extractable t => t a -> a
extract Construction Maybe e
xs) Exactly e
-> (Exactly e -> Construction Maybe e)
-> ((:*:) (Exactly e) :. (->) (Exactly e)) > Construction Maybe e
forall s a. s -> a -> s :*: a
:*: \(Exactly e
new) -> e -> ((Maybe :. Construction Maybe) > e) -> Construction Maybe e
forall (t :: * -> *) a.
a -> ((t :. Construction t) > a) -> Construction t a
Construct e
new (((Maybe :. Construction Maybe) > e) -> Construction Maybe e)
-> ((Maybe :. Construction Maybe) > e) -> Construction Maybe e
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Construction Maybe e -> (Maybe :. Construction Maybe) > e
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) > a
deconstruct Construction Maybe e
xs
	-- It will never return you the last element
	pop :: State (Popping (Construction Maybe) e) (Maybe e)
pop = (\(Construct e
x (Maybe :. Construction Maybe) > e
xs) -> e -> Construction Maybe e -> e
forall (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant e
x (Construction Maybe e -> e)
-> State (Construction Maybe e) ((Maybe :. Construction Maybe) > e)
-> State (Construction Maybe e) (Maybe e)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Covariant source target t,
 Covariant source (Betwixt source target) u,
 Covariant (Betwixt source target) target t) =>
source a b -> target (t (u a)) (t (u b))
<-|-|- forall e r. Settable State => Setting State e r
forall k (i :: k) e r. Settable i => Setting i e r
set @State (Construction Maybe e
 -> State (Construction Maybe e) (Construction Maybe e))
-> ((Maybe :. Construction Maybe) > e)
-> State (Construction Maybe e) ((Maybe :. Construction Maybe) > e)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
 Monoidal (Straight source) (Straight target) (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<<- (Maybe :. Construction Maybe) > e
xs) (Construction Maybe e -> State (Construction Maybe e) (Maybe e))
-> State (Construction Maybe e) (Construction Maybe e)
-> State (Construction Maybe e) (Maybe e)
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
=<< forall e r. Gettable State => Getting State e r
forall k (i :: k) e r. Gettable i => Getting i e r
get @State
	push :: e -> State (Pushing (Construction Maybe) e) e
push e
x = e -> State (Construction Maybe e) e
forall (t :: * -> *) a. Pointable t => a -> t a
point e
x State (Construction Maybe e) e
-> State (Construction Maybe e) (Construction Maybe e)
-> State (Construction Maybe e) e
forall (t :: * -> *) b a.
(Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) =>
t b -> t a -> t b
.-*- (forall e r. Modifiable State => Modification State e r
forall k (i :: k) e r. Modifiable i => Modification i e r
modify @State ((Construction Maybe e -> Construction Maybe e)
 -> State (Construction Maybe e) (Construction Maybe e))
-> (Construction Maybe e -> Construction Maybe e)
-> State (Construction Maybe e) (Construction Maybe e)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- e -> ((Maybe :. Construction Maybe) > e) -> Construction Maybe e
forall (t :: * -> *) a.
a -> ((t :. Construction t) > a) -> Construction t a
Construct e
x (((Maybe :. Construction Maybe) > e) -> Construction Maybe e)
-> (Construction Maybe e -> (Maybe :. Construction Maybe) > e)
-> Construction Maybe e
-> Construction Maybe e
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Maybe e -> (Maybe :. Construction Maybe) > e
forall a. a -> Maybe a
Just)

---------------------------------------- Combinative list ------------------------------------------

type instance Combinative List = Comprehension Maybe

----------------------------------------- Zipper of list -------------------------------------------

instance Zippable List where
	type Breadcrumbs List = Reverse List <:*:> List

instance {-# OVERLAPS #-} Traversable (->) (->) (Tape List) where
	a -> u b
f <<- :: (a -> u b) -> Tape List a -> u (Tape List b)
<<- TU (Tag (T_U (Exactly a
x :*: T_U (Reverse List a
left :*: List a
right)))) =
		(\Reverse List b
past' b
x' Reverse List b
left' -> T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List) b
-> Tape List b
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List) b
 -> Tape List b)
-> T_U
     Covariant Covariant (:*:) Exactly (Reverse List <:*:> List) b
-> Tape List b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<------ b -> Exactly b
forall a. a -> Exactly a
Exactly b
x' Exactly b
-> T_U Covariant Covariant (:*:) (Reverse List) List b
-> T_U
     Covariant Covariant (:*:) Exactly (Reverse List <:*:> List) b
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) > a
<:*:> Reverse List b
left' Reverse List b
-> List b -> T_U Covariant Covariant (:*:) (Reverse List) List b
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) > a
<:*:> Reverse List b -> List b
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run Reverse List b
past')
			(Reverse List b -> b -> Reverse List b -> Tape List b)
-> u (Reverse List b) -> u (b -> Reverse List b -> Tape List b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- a -> u b
f (a -> u b) -> Reverse List a -> u (Reverse List b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
 Monoidal (Straight source) (Straight target) (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<<- List a -> Reverse List a
forall k (t :: k -> *) (a :: k). t a -> Reverse t a
Reverse List a
right u (b -> Reverse List b -> Tape List b)
-> u b -> u (Reverse List b -> Tape List b)
forall (t :: * -> *) a b.
(Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*- a -> u b
f a
x u (Reverse List b -> Tape List b)
-> u (Reverse List b) -> u (Tape List b)
forall (t :: * -> *) a b.
(Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*- a -> u b
f (a -> u b) -> Reverse List a -> u (Reverse List b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
 Monoidal (Straight source) (Straight target) (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<<- Reverse List a
left

-- instance {-# OVERLAPS #-} Extendable (->) (Tape List) where
	-- f <<= z = let move rtt = TT . deconstruct <----- run . rtt .-+ z in
		-- imply @(Tape List _)
			-- <---- f z
			-- <---- f <-|-- move <-- rotate @Left
			-- <---- f <-|-- move <-- rotate @Right

instance Morphable (Rotate Left) (Turnover < Tape List) where
	type Morphing (Rotate Left) (Turnover < Tape List) = Turnover < Tape List
	morphing :: (<::>) (Tagged ('Rotate 'Left)) (Turnover < Tape List) a
-> Morphing ('Rotate 'Left) (Turnover < Tape List) a
morphing s :: (<::>) (Tagged ('Rotate 'Left)) (Turnover < Tape List) a
s@(TU
  Covariant
  Covariant
  (Tagged (Zippable List))
  (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
  a
-> T_U
     Covariant Covariant (:*:) Exactly (Reverse List <:*:> List) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (TU
   Covariant
   Covariant
   (Tagged (Zippable List))
   (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
   a
 -> T_U
      Covariant Covariant (:*:) Exactly (Reverse List <:*:> List) a)
-> ((<::>) (Tagged ('Rotate 'Left)) (Turnover < Tape List) a
    -> TU
         Covariant
         Covariant
         (Tagged (Zippable List))
         (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
         a)
-> (<::>) (Tagged ('Rotate 'Left)) (Turnover < Tape List) a
-> T_U
     Covariant Covariant (:*:) Exactly (Reverse List <:*:> List) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<) Turnover (Tape List) a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable List))
     (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
     a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run ((<) Turnover (Tape List) a
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable List))
      (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
      a)
-> ((<::>) (Tagged ('Rotate 'Left)) (Turnover < Tape List) a
    -> (<) Turnover (Tape List) a)
-> (<::>) (Tagged ('Rotate 'Left)) (Turnover < Tape List) a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable List))
     (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>) (Tagged ('Rotate 'Left)) (Turnover < Tape List) a
-> (<) Turnover (Tape List) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> T_U (Exactly a
x :*: T_U (Reverse TT Covariant Covariant Maybe (Construction Maybe) a
left :*: TT Covariant Covariant Maybe (Construction Maybe) a
right))) =
		forall e r.
Monotonic
  (TU
     Covariant
     Covariant
     (Tagged (Zippable List))
     (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
     a)
  e =>
(TU
   Covariant
   Covariant
   (Tagged (Zippable List))
   (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
   a
 -> r)
-> r -> e -> r
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve @(Tape List _) ((TU
    Covariant
    Covariant
    (Tagged (Zippable List))
    (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
    a
  -> (<) Turnover (Tape List) a)
 -> (<) Turnover (Tape List) a
 -> Maybe
      (TU
         Covariant
         Covariant
         (Tagged (Zippable List))
         (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
         a)
 -> (<) Turnover (Tape List) a)
-> (TU
      Covariant
      Covariant
      (Tagged (Zippable List))
      (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
      a
    -> (<) Turnover (Tape List) a)
-> (<) Turnover (Tape List) a
-> Maybe
     (TU
        Covariant
        Covariant
        (Tagged (Zippable List))
        (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
        a)
-> (<) Turnover (Tape List) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- TU
  Covariant
  Covariant
  (Tagged (Zippable List))
  (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
  a
-> (<) Turnover (Tape List) a
forall k (t :: k -> *) (a :: k). t a -> Turnover t a
Turnover ((<) Turnover (Tape List) a
 -> Maybe
      (TU
         Covariant
         Covariant
         (Tagged (Zippable List))
         (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
         a)
 -> (<) Turnover (Tape List) a)
-> (<) Turnover (Tape List) a
-> Maybe
     (TU
        Covariant
        Covariant
        (Tagged (Zippable List))
        (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
        a)
-> (<) Turnover (Tape List) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- (<::>) (Tagged ('Rotate 'Left)) (Turnover < Tape List) a
-> (<) Turnover (Tape List) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph (<::>) (Tagged ('Rotate 'Left)) (Turnover < Tape List) a
s (Maybe
   (TU
      Covariant
      Covariant
      (Tagged (Zippable List))
      (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
      a)
 -> (<) Turnover (Tape List) a)
-> Maybe
     (TU
        Covariant
        Covariant
        (Tagged (Zippable List))
        (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
        a)
-> (<) Turnover (Tape List) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<----
			(a
-> Nonempty List a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable List))
     (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
     a
forall a. a -> Nonempty List a -> Tape List a
rotate_over a
x (Construction Maybe a
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable List))
      (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
      a)
-> Maybe (Construction Maybe a)
-> Maybe
     (TU
        Covariant
        Covariant
        (Tagged (Zippable List))
        (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
        a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- TT Covariant Covariant Maybe (Construction Maybe) a
-> Maybe (Construction Maybe a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run TT Covariant Covariant Maybe (Construction Maybe) a
right) Maybe
  (TU
     Covariant
     Covariant
     (Tagged (Zippable List))
     (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
     a)
-> Maybe
     (TU
        Covariant
        Covariant
        (Tagged (Zippable List))
        (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
        a)
-> Maybe
     (TU
        Covariant
        Covariant
        (Tagged (Zippable List))
        (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
        a)
forall (t :: * -> *) a.
(Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:+:) t) =>
t a -> t a -> t a
.-+- (a
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> Nonempty List a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable List))
     (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
     a
forall a. a -> List a -> Nonempty List a -> Tape List a
rotate_left a
x TT Covariant Covariant Maybe (Construction Maybe) a
right (Construction Maybe a
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable List))
      (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
      a)
-> Maybe (Construction Maybe a)
-> Maybe
     (TU
        Covariant
        Covariant
        (Tagged (Zippable List))
        (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
        a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- TT Covariant Covariant Maybe (Construction Maybe) a
-> Maybe (Construction Maybe a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run TT Covariant Covariant Maybe (Construction Maybe) a
left) where

		rotate_left :: a -> List a -> Nonempty List a -> Tape List a
		rotate_left :: a -> List a -> Nonempty List a -> Tape List a
rotate_left a
focused List a
rs (Construct lx lxs) = Impliable (Tape List a) => Arguments (Tape List a)
forall k (result :: k). Impliable result => Arguments result
imply @(Tape List _) (a -> List a -> List a -> Tape List a)
-> a -> List a -> List a -> Tape List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- a
lx (List a -> List a -> Tape List a)
-> List a -> List a -> Tape List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- ((Maybe :. Construction Maybe) > a) -> List a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT (Maybe :. Construction Maybe) > a
lxs (List a -> Tape List a) -> List a -> Tape List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- a :=:=> List
forall k (mod :: k) (struct :: * -> *) a.
Morphed mod struct ((Exactly <:.:> struct) > (->)) =>
a :=:=> struct
item @Push a
focused List a
rs

		rotate_over :: a -> Nonempty List a -> Tape List a
		rotate_over :: a -> Nonempty List a -> Tape List a
rotate_over a
focused Nonempty List a
rs = let new_left :: Construction Maybe a
new_left = (Construction Maybe a :*: Construction Maybe ())
-> Construction Maybe a
forall a b. (a :*: b) -> a
attached ((Construction Maybe a :*: Construction Maybe ())
 -> Construction Maybe a)
-> (Construction Maybe a :*: Construction Maybe ())
-> Construction Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- (a -> State (Construction Maybe a) ()
forall a. a -> State (Nonempty List a) ()
put_over (a -> State (Construction Maybe a) ())
-> Construction Maybe a
-> State (Construction Maybe a) (Construction Maybe ())
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
 Monoidal (Straight source) (Straight target) (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<<- Nonempty List a
Construction Maybe a
rs State (Construction Maybe a) (Construction Maybe ())
-> ((->) (Construction Maybe a) :. (:*:) (Construction Maybe a))
   > Construction Maybe ()
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~~~ a -> Construction Maybe a
forall (t :: * -> *) a. Pointable t => a -> t a
point a
focused) in
			Impliable (Tape List a) => Arguments (Tape List a)
forall k (result :: k). Impliable result => Arguments result
imply @(Tape List _) (a
 -> TT Covariant Covariant Maybe (Construction Maybe) a
 -> TT Covariant Covariant Maybe (Construction Maybe) a
 -> Tape List a)
-> a
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> Tape List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Construction Maybe a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Construction Maybe a
new_left (TT Covariant Covariant Maybe (Construction Maybe) a
 -> TT Covariant Covariant Maybe (Construction Maybe) a
 -> Tape List a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> Tape List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- ((Maybe :. Construction Maybe) > a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT (((Maybe :. Construction Maybe) > a)
 -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> ((Maybe :. Construction Maybe) > a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction Maybe a -> (Maybe :. Construction Maybe) > a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) > a
deconstruct Construction Maybe a
new_left (TT Covariant Covariant Maybe (Construction Maybe) a
 -> Tape List a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> Tape List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- TT Covariant Covariant Maybe (Construction Maybe) a
forall (t :: * -> *) a. Emptiable t => t a
empty

		put_over :: a -> State (Nonempty List a) ()
		put_over :: a -> State (Nonempty List a) ()
put_over = State (Construction Maybe a) (Construction Maybe a)
-> State (Construction Maybe a) ()
forall (t :: * -> *) a. Covariant (->) (->) t => t a -> t ()
void (State (Construction Maybe a) (Construction Maybe a)
 -> State (Construction Maybe a) ())
-> (a -> State (Construction Maybe a) (Construction Maybe a))
-> a
-> State (Construction Maybe a) ()
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall e r. Modifiable State => Modification State e r
forall k (i :: k) e r. Modifiable i => Modification i e r
modify @State ((Construction Maybe a -> Construction Maybe a)
 -> State (Construction Maybe a) (Construction Maybe a))
-> (a -> Construction Maybe a -> Construction Maybe a)
-> a
-> State (Construction Maybe a) (Construction Maybe a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall k (mod :: k) (struct :: * -> *) a.
Morphed mod struct ((Exactly <:.:> struct) > (->)) =>
a :=:=> struct
forall (struct :: * -> *) a.
Morphed 'Push struct ((Exactly <:.:> struct) > (->)) =>
a :=:=> struct
item @Push

instance Morphable (Rotate Right) (Turnover < Tape List) where
	type Morphing (Rotate Right) (Turnover < Tape List) = Turnover < Tape List
	morphing :: (<::>) (Tagged ('Rotate 'Right)) (Turnover < Tape List) a
-> Morphing ('Rotate 'Right) (Turnover < Tape List) a
morphing s :: (<::>) (Tagged ('Rotate 'Right)) (Turnover < Tape List) a
s@(TU
  Covariant
  Covariant
  (Tagged (Zippable List))
  (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
  a
-> T_U
     Covariant Covariant (:*:) Exactly (Reverse List <:*:> List) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (TU
   Covariant
   Covariant
   (Tagged (Zippable List))
   (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
   a
 -> T_U
      Covariant Covariant (:*:) Exactly (Reverse List <:*:> List) a)
-> ((<::>) (Tagged ('Rotate 'Right)) (Turnover < Tape List) a
    -> TU
         Covariant
         Covariant
         (Tagged (Zippable List))
         (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
         a)
-> (<::>) (Tagged ('Rotate 'Right)) (Turnover < Tape List) a
-> T_U
     Covariant Covariant (:*:) Exactly (Reverse List <:*:> List) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<) Turnover (Tape List) a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable List))
     (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
     a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run ((<) Turnover (Tape List) a
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable List))
      (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
      a)
-> ((<::>) (Tagged ('Rotate 'Right)) (Turnover < Tape List) a
    -> (<) Turnover (Tape List) a)
-> (<::>) (Tagged ('Rotate 'Right)) (Turnover < Tape List) a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable List))
     (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>) (Tagged ('Rotate 'Right)) (Turnover < Tape List) a
-> (<) Turnover (Tape List) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> T_U (Exactly a
x :*: T_U (Reverse List a
left :*: List a
right))) =
		forall e r.
Monotonic
  (TU
     Covariant
     Covariant
     (Tagged (Zippable List))
     (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
     a)
  e =>
(TU
   Covariant
   Covariant
   (Tagged (Zippable List))
   (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
   a
 -> r)
-> r -> e -> r
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve @(Tape List _) ((TU
    Covariant
    Covariant
    (Tagged (Zippable List))
    (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
    a
  -> (<) Turnover (Tape List) a)
 -> (<) Turnover (Tape List) a
 -> Maybe
      (TU
         Covariant
         Covariant
         (Tagged (Zippable List))
         (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
         a)
 -> (<) Turnover (Tape List) a)
-> (TU
      Covariant
      Covariant
      (Tagged (Zippable List))
      (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
      a
    -> (<) Turnover (Tape List) a)
-> (<) Turnover (Tape List) a
-> Maybe
     (TU
        Covariant
        Covariant
        (Tagged (Zippable List))
        (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
        a)
-> (<) Turnover (Tape List) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- TU
  Covariant
  Covariant
  (Tagged (Zippable List))
  (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
  a
-> (<) Turnover (Tape List) a
forall k (t :: k -> *) (a :: k). t a -> Turnover t a
Turnover ((<) Turnover (Tape List) a
 -> Maybe
      (TU
         Covariant
         Covariant
         (Tagged (Zippable List))
         (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
         a)
 -> (<) Turnover (Tape List) a)
-> (<) Turnover (Tape List) a
-> Maybe
     (TU
        Covariant
        Covariant
        (Tagged (Zippable List))
        (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
        a)
-> (<) Turnover (Tape List) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- (<::>) (Tagged ('Rotate 'Right)) (Turnover < Tape List) a
-> (<) Turnover (Tape List) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph (<::>) (Tagged ('Rotate 'Right)) (Turnover < Tape List) a
s
			(Maybe
   (TU
      Covariant
      Covariant
      (Tagged (Zippable List))
      (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
      a)
 -> (<) Turnover (Tape List) a)
-> Maybe
     (TU
        Covariant
        Covariant
        (Tagged (Zippable List))
        (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
        a)
-> (<) Turnover (Tape List) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- (a
-> Nonempty List a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable List))
     (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
     a
forall a. a -> Nonempty List a -> Tape List a
rotate_over a
x (Construction Maybe a
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable List))
      (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
      a)
-> Maybe (Construction Maybe a)
-> Maybe
     (TU
        Covariant
        Covariant
        (Tagged (Zippable List))
        (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
        a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- List a -> Maybe (Construction Maybe a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run List a
left) Maybe
  (TU
     Covariant
     Covariant
     (Tagged (Zippable List))
     (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
     a)
-> Maybe
     (TU
        Covariant
        Covariant
        (Tagged (Zippable List))
        (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
        a)
-> Maybe
     (TU
        Covariant
        Covariant
        (Tagged (Zippable List))
        (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
        a)
forall (t :: * -> *) a.
(Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:+:) t) =>
t a -> t a -> t a
.-+- (a
-> List a
-> Nonempty List a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable List))
     (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
     a
forall a. a -> List a -> Nonempty List a -> Tape List a
rotate_right a
x List a
left (Construction Maybe a
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable List))
      (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
      a)
-> Maybe (Construction Maybe a)
-> Maybe
     (TU
        Covariant
        Covariant
        (Tagged (Zippable List))
        (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
        a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- List a -> Maybe (Construction Maybe a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run List a
right) where

		rotate_right :: a -> List a -> Nonempty List a -> Tape List a
		rotate_right :: a -> List a -> Nonempty List a -> Tape List a
rotate_right a
focused List a
ls (Construct rx rxs) = Impliable (Tape List a) => Arguments (Tape List a)
forall k (result :: k). Impliable result => Arguments result
imply @(Tape List _) (a -> List a -> List a -> Tape List a)
-> a -> List a -> List a -> Tape List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- a
rx (List a -> List a -> Tape List a)
-> List a -> List a -> Tape List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- a :=:=> List
forall k (mod :: k) (struct :: * -> *) a.
Morphed mod struct ((Exactly <:.:> struct) > (->)) =>
a :=:=> struct
item @Push a
focused List a
ls (List a -> Tape List a) -> List a -> Tape List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- ((Maybe :. Construction Maybe) > a) -> List a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT (Maybe :. Construction Maybe) > a
rxs

		rotate_over :: a -> Nonempty List a -> Tape List a
		rotate_over :: a -> Nonempty List a -> Tape List a
rotate_over a
focused Nonempty List a
ls = let new_right :: Construction Maybe a
new_right = (Construction Maybe a :*: Construction Maybe ())
-> Construction Maybe a
forall a b. (a :*: b) -> a
attached (a -> State (Construction Maybe a) ()
forall a. a -> State (Nonempty List a) ()
put_over (a -> State (Construction Maybe a) ())
-> Construction Maybe a
-> State (Construction Maybe a) (Construction Maybe ())
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
 Monoidal (Straight source) (Straight target) (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<<- Nonempty List a
Construction Maybe a
ls State (Construction Maybe a) (Construction Maybe ())
-> ((->) (Construction Maybe a) :. (:*:) (Construction Maybe a))
   > Construction Maybe ()
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~~~ a -> Construction Maybe a
forall (t :: * -> *) a. Pointable t => a -> t a
point a
focused) in
			Impliable (Tape List a) => Arguments (Tape List a)
forall k (result :: k). Impliable result => Arguments result
imply @(Tape List _) (a
 -> TT Covariant Covariant Maybe (Construction Maybe) a
 -> TT Covariant Covariant Maybe (Construction Maybe) a
 -> Tape List a)
-> a
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> Tape List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Construction Maybe a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Construction Maybe a
new_right (TT Covariant Covariant Maybe (Construction Maybe) a
 -> TT Covariant Covariant Maybe (Construction Maybe) a
 -> Tape List a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> Tape List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- TT Covariant Covariant Maybe (Construction Maybe) a
forall (t :: * -> *) a. Emptiable t => t a
empty (TT Covariant Covariant Maybe (Construction Maybe) a
 -> Tape List a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> Tape List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- ((Maybe :. Construction Maybe) > a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT (((Maybe :. Construction Maybe) > a)
 -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> ((Maybe :. Construction Maybe) > a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction Maybe a -> (Maybe :. Construction Maybe) > a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) > a
deconstruct Construction Maybe a
new_right

		put_over :: a -> State (Nonempty List a) ()
		put_over :: a -> State (Nonempty List a) ()
put_over = State (Construction Maybe a) (Construction Maybe a)
-> State (Construction Maybe a) ()
forall (t :: * -> *) a. Covariant (->) (->) t => t a -> t ()
void (State (Construction Maybe a) (Construction Maybe a)
 -> State (Construction Maybe a) ())
-> (a -> State (Construction Maybe a) (Construction Maybe a))
-> a
-> State (Construction Maybe a) ()
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall e r. Modifiable State => Modification State e r
forall k (i :: k) e r. Modifiable i => Modification i e r
modify @State ((Construction Maybe a -> Construction Maybe a)
 -> State (Construction Maybe a) (Construction Maybe a))
-> (a -> Construction Maybe a -> Construction Maybe a)
-> a
-> State (Construction Maybe a) (Construction Maybe a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall k (mod :: k) (struct :: * -> *) a.
Morphed mod struct ((Exactly <:.:> struct) > (->)) =>
a :=:=> struct
forall (struct :: * -> *) a.
Morphed 'Push struct ((Exactly <:.:> struct) > (->)) =>
a :=:=> struct
item @Push

instance Morphable (Into > Tape List) List where
	type Morphing (Into > Tape List) List = Maybe <::> Tape List
	morphing :: (<::>) (Tagged ('Into > Tape List)) List a
-> Morphing ('Into > Tape List) List a
morphing ((<::>) (Tagged ('Into > Tape List)) List a -> List a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> List a
list) = (forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
forall (struct :: * -> *).
Morphable ('Into (Zipper List)) struct =>
struct ~> Morphing ('Into (Zipper List)) struct
into @(Zipper List) (Construction Maybe a -> Tape List a)
-> Maybe (Construction Maybe a) -> Maybe (Tape List a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-) (Primary List a
 -> Primary (TT Covariant Covariant Maybe (Tape List)) a)
-> ((->) < List a) < TT Covariant Covariant Maybe (Tape List) a
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < Primary t a) < Primary u b) -> (m < t a) < u b
=#- List a
list

instance Morphable (Into List) (Tape List) where
	type Morphing (Into List) (Tape List) = List
	morphing :: (<::>) (Tagged ('Into List)) (Tape List) a
-> Morphing ('Into List) (Tape List) a
morphing (TU
  Covariant
  Covariant
  (Tagged (Zippable List))
  (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
  a
-> T_U
     Covariant Covariant (:*:) Exactly (Reverse List <:*:> List) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (TU
   Covariant
   Covariant
   (Tagged (Zippable List))
   (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
   a
 -> T_U
      Covariant Covariant (:*:) Exactly (Reverse List <:*:> List) a)
-> ((<::>) (Tagged ('Into List)) (Tape List) a
    -> TU
         Covariant
         Covariant
         (Tagged (Zippable List))
         (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
         a)
-> (<::>) (Tagged ('Into List)) (Tape List) a
-> T_U
     Covariant Covariant (:*:) Exactly (Reverse List <:*:> List) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>) (Tagged ('Into List)) (Tape List) a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable List))
     (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
     a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> T_U (Exactly a
x :*: T_U (Reverse List a
left :*: List a
right))) = (List a
 :*: TT Covariant Covariant Maybe (Construction Maybe) (List a))
-> List a
forall a b. (a :*: b) -> a
attached ((List a
  :*: TT Covariant Covariant Maybe (Construction Maybe) (List a))
 -> List a)
-> (List a
    :*: TT Covariant Covariant Maybe (Construction Maybe) (List a))
-> List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- forall a.
Interpreted (->) (State (List a)) =>
((->) < State (List a) a) < Primary (State (List a)) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run @(->) @(State _)
		(State
   (List a)
   (TT Covariant Covariant Maybe (Construction Maybe) (List a))
 -> ((->) (List a) :. (:*:) (List a))
    > TT Covariant Covariant Maybe (Construction Maybe) (List a))
-> State
     (List a)
     (TT Covariant Covariant Maybe (Construction Maybe) (List a))
-> ((->) (List a) :. (:*:) (List a))
   > TT Covariant Covariant Maybe (Construction Maybe) (List a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- forall e r. Modifiable State => Modification State e r
forall k (i :: k) e r. Modifiable i => Modification i e r
modify @State ((List a -> List a) -> State (List a) (List a))
-> (a -> List a -> List a) -> a -> State (List a) (List a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall a.
Morphed 'Push List ((Exactly <:.:> List) > (->)) =>
a :=:=> List
forall k (mod :: k) (struct :: * -> *) a.
Morphed mod struct ((Exactly <:.:> struct) > (->)) =>
a :=:=> struct
item @Push @List (a -> State (List a) (List a))
-> List a
-> State
     (List a)
     (TT Covariant Covariant Maybe (Construction Maybe) (List a))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
 Monoidal (Straight source) (Straight target) (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<<- List a
right
		(((->) (List a) :. (:*:) (List a))
 > TT Covariant Covariant Maybe (Construction Maybe) (List a))
-> ((->) (List a) :. (:*:) (List a))
   > TT Covariant Covariant Maybe (Construction Maybe) (List a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- a -> List a -> List a
forall k (mod :: k) (struct :: * -> *) a.
Morphed mod struct ((Exactly <:.:> struct) > (->)) =>
a :=:=> struct
item @Push a
x List a
left

instance Morphable (Into > Comprehension Maybe) (Tape List) where
	type Morphing (Into > Comprehension Maybe) (Tape List) = Comprehension Maybe
	morphing :: (<::>) (Tagged ('Into > Comprehension Maybe)) (Tape List) a
-> Morphing ('Into > Comprehension Maybe) (Tape List) a
morphing (TU
  Covariant
  Covariant
  (Tagged (Zippable List))
  (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
  a
-> T_U
     Covariant Covariant (:*:) Exactly (Reverse List <:*:> List) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (TU
   Covariant
   Covariant
   (Tagged (Zippable List))
   (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
   a
 -> T_U
      Covariant Covariant (:*:) Exactly (Reverse List <:*:> List) a)
-> ((<::>) (Tagged ('Into > Comprehension Maybe)) (Tape List) a
    -> TU
         Covariant
         Covariant
         (Tagged (Zippable List))
         (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
         a)
-> (<::>) (Tagged ('Into > Comprehension Maybe)) (Tape List) a
-> T_U
     Covariant Covariant (:*:) Exactly (Reverse List <:*:> List) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>) (Tagged ('Into > Comprehension Maybe)) (Tape List) a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable List))
     (T_U Covariant Covariant (:*:) Exactly (Reverse List <:*:> List))
     a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> T_U (Exactly a
x :*: T_U (Reverse List a
left :*: List a
right))) = (Comprehension Maybe a
 :*: TT
       Covariant
       Covariant
       Maybe
       (Construction Maybe)
       (Comprehension Maybe a))
-> Comprehension Maybe a
forall a b. (a :*: b) -> a
attached ((Comprehension Maybe a
  :*: TT
        Covariant
        Covariant
        Maybe
        (Construction Maybe)
        (Comprehension Maybe a))
 -> Comprehension Maybe a)
-> (Comprehension Maybe a
    :*: TT
          Covariant
          Covariant
          Maybe
          (Construction Maybe)
          (Comprehension Maybe a))
-> Comprehension Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- forall a.
Interpreted (->) (State (Comprehension Maybe a)) =>
((->) < State (Comprehension Maybe a) a)
< Primary (State (Comprehension Maybe a)) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run @(->) @(State _)
		(State
   (Comprehension Maybe a)
   (TT
      Covariant
      Covariant
      Maybe
      (Construction Maybe)
      (Comprehension Maybe a))
 -> ((->) (Comprehension Maybe a) :. (:*:) (Comprehension Maybe a))
    > TT
        Covariant
        Covariant
        Maybe
        (Construction Maybe)
        (Comprehension Maybe a))
-> State
     (Comprehension Maybe a)
     (TT
        Covariant
        Covariant
        Maybe
        (Construction Maybe)
        (Comprehension Maybe a))
-> ((->) (Comprehension Maybe a) :. (:*:) (Comprehension Maybe a))
   > TT
       Covariant
       Covariant
       Maybe
       (Construction Maybe)
       (Comprehension Maybe a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- forall e r. Modifiable State => Modification State e r
forall k (i :: k) e r. Modifiable i => Modification i e r
modify @State ((Comprehension Maybe a -> Comprehension Maybe a)
 -> State (Comprehension Maybe a) (Comprehension Maybe a))
-> (a -> Comprehension Maybe a -> Comprehension Maybe a)
-> a
-> State (Comprehension Maybe a) (Comprehension Maybe a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall a.
Morphed
  'Push
  (Comprehension Maybe)
  ((Exactly <:.:> Comprehension Maybe) > (->)) =>
a :=:=> Comprehension Maybe
forall k (mod :: k) (struct :: * -> *) a.
Morphed mod struct ((Exactly <:.:> struct) > (->)) =>
a :=:=> struct
item @Push @(Comprehension Maybe) (a -> State (Comprehension Maybe a) (Comprehension Maybe a))
-> List a
-> State
     (Comprehension Maybe a)
     (TT
        Covariant
        Covariant
        Maybe
        (Construction Maybe)
        (Comprehension Maybe a))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
 Monoidal (Straight source) (Straight target) (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<<- List a
right
		(((->) (Comprehension Maybe a) :. (:*:) (Comprehension Maybe a))
 > TT
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Comprehension Maybe a))
-> ((->) (Comprehension Maybe a) :. (:*:) (Comprehension Maybe a))
   > TT
       Covariant
       Covariant
       Maybe
       (Construction Maybe)
       (Comprehension Maybe a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- a -> Comprehension Maybe a -> Comprehension Maybe a
forall k (mod :: k) (struct :: * -> *) a.
Morphed mod struct ((Exactly <:.:> struct) > (->)) =>
a :=:=> struct
item @Push a
x (Comprehension Maybe a -> Comprehension Maybe a)
-> Comprehension Maybe a -> Comprehension Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- List a -> Comprehension Maybe a
forall (t :: * -> *) a.
((t <::> Construction t) > a) -> Comprehension t a
Comprehension List a
left

------------------------------------- Zipper of non-empty list -------------------------------------

instance Zippable (Construction Maybe) where
	type Breadcrumbs (Construction Maybe) = Reverse > Construction Maybe <:*:> Construction Maybe

instance Morphable (Rotate Left) (Tape > Construction Maybe) where
	type Morphing (Rotate Left) (Tape > Construction Maybe) = Maybe <::> (Tape > Construction Maybe)
	morphing :: (<::>) (Tagged ('Rotate 'Left)) (Tape > Construction Maybe) a
-> Morphing ('Rotate 'Left) (Tape > Construction Maybe) a
morphing (TU
  Covariant
  Covariant
  (Tagged (Zippable (Construction Maybe)))
  (T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (T_U
        Covariant
        Covariant
        (:*:)
        (Reverse (Construction Maybe))
        (Construction Maybe)))
  a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (T_U
        Covariant
        Covariant
        (:*:)
        (Reverse (Construction Maybe))
        (Construction Maybe))
     a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (TU
   Covariant
   Covariant
   (Tagged (Zippable (Construction Maybe)))
   (T_U
      Covariant
      Covariant
      (:*:)
      Exactly
      (T_U
         Covariant
         Covariant
         (:*:)
         (Reverse (Construction Maybe))
         (Construction Maybe)))
   a
 -> T_U
      Covariant
      Covariant
      (:*:)
      Exactly
      (T_U
         Covariant
         Covariant
         (:*:)
         (Reverse (Construction Maybe))
         (Construction Maybe))
      a)
-> ((<::>) (Tagged ('Rotate 'Left)) (Tape > Construction Maybe) a
    -> TU
         Covariant
         Covariant
         (Tagged (Zippable (Construction Maybe)))
         (T_U
            Covariant
            Covariant
            (:*:)
            Exactly
            (T_U
               Covariant
               Covariant
               (:*:)
               (Reverse (Construction Maybe))
               (Construction Maybe)))
         a)
-> (<::>) (Tagged ('Rotate 'Left)) (Tape > Construction Maybe) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (T_U
        Covariant
        Covariant
        (:*:)
        (Reverse (Construction Maybe))
        (Construction Maybe))
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>) (Tagged ('Rotate 'Left)) (Tape > Construction Maybe) a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable (Construction Maybe)))
     (T_U
        Covariant
        Covariant
        (:*:)
        Exactly
        (T_U
           Covariant
           Covariant
           (:*:)
           (Reverse (Construction Maybe))
           (Construction Maybe)))
     a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> T_U (Exactly a
x :*: T_U (Reverse Construction Maybe a
left :*: Construction Maybe a
right))) =
		((Maybe :. (Tape > Construction Maybe)) > a)
-> TT Covariant Covariant Maybe (Tape > Construction Maybe) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT (((Maybe :. (Tape > Construction Maybe)) > a)
 -> TT Covariant Covariant Maybe (Tape > Construction Maybe) a)
-> ((Maybe :. (Tape > Construction Maybe)) > a)
-> TT Covariant Covariant Maybe (Tape > Construction Maybe) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<----- Impliable (Tape (Nonempty List) a) =>
Arguments (Tape (Nonempty List) a)
forall k (result :: k). Impliable result => Arguments result
imply @(Tape (Nonempty List) _)
			(a
 -> Construction Maybe a
 -> Construction Maybe a
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable (Construction Maybe)))
      (T_U
         Covariant
         Covariant
         (:*:)
         Exactly
         (T_U
            Covariant
            Covariant
            (:*:)
            (Reverse (Construction Maybe))
            (Construction Maybe)))
      a)
-> Maybe a
-> Maybe
     (Construction Maybe a
      -> Construction Maybe a
      -> TU
           Covariant
           Covariant
           (Tagged (Zippable (Construction Maybe)))
           (T_U
              Covariant
              Covariant
              (:*:)
              Exactly
              (T_U
                 Covariant
                 Covariant
                 (:*:)
                 (Reverse (Construction Maybe))
                 (Construction Maybe)))
           a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-- a -> Maybe a
forall (t :: * -> *) a. Pointable t => a -> t a
point (a -> Maybe a) -> a -> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction Maybe a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Construction Maybe a
left
			Maybe
  (Construction Maybe a
   -> Construction Maybe a
   -> TU
        Covariant
        Covariant
        (Tagged (Zippable (Construction Maybe)))
        (T_U
           Covariant
           Covariant
           (:*:)
           Exactly
           (T_U
              Covariant
              Covariant
              (:*:)
              (Reverse (Construction Maybe))
              (Construction Maybe)))
        a)
-> Maybe (Construction Maybe a)
-> Maybe
     (Construction Maybe a
      -> TU
           Covariant
           Covariant
           (Tagged (Zippable (Construction Maybe)))
           (T_U
              Covariant
              Covariant
              (:*:)
              Exactly
              (T_U
                 Covariant
                 Covariant
                 (:*:)
                 (Reverse (Construction Maybe))
                 (Construction Maybe)))
           a)
forall (t :: * -> *) a b.
(Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) =>
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
left
			Maybe
  (Construction Maybe a
   -> TU
        Covariant
        Covariant
        (Tagged (Zippable (Construction Maybe)))
        (T_U
           Covariant
           Covariant
           (:*:)
           Exactly
           (T_U
              Covariant
              Covariant
              (:*:)
              (Reverse (Construction Maybe))
              (Construction Maybe)))
        a)
-> Maybe (Construction Maybe a)
-> (Maybe :. (Tape > Construction Maybe)) > a
forall (t :: * -> *) a b.
(Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*-- Construction Maybe a -> Maybe (Construction Maybe a)
forall (t :: * -> *) a. Pointable t => a -> t a
point (Construction Maybe a -> Maybe (Construction Maybe a))
-> Construction Maybe a -> Maybe (Construction Maybe a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- a :=:=> Construction Maybe
forall k (mod :: k) (struct :: * -> *) a.
Morphed mod struct ((Exactly <:.:> struct) > (->)) =>
a :=:=> struct
item @Push a
x Construction Maybe a
right

instance Morphable (Rotate Right) (Tape > Construction Maybe) where
	type Morphing (Rotate Right) (Tape > Construction Maybe) = Maybe <::> Tape (Construction Maybe)
	morphing :: (<::>) (Tagged ('Rotate 'Right)) (Tape > Construction Maybe) a
-> Morphing ('Rotate 'Right) (Tape > Construction Maybe) a
morphing (TU
  Covariant
  Covariant
  (Tagged (Zippable (Construction Maybe)))
  (T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (T_U
        Covariant
        Covariant
        (:*:)
        (Reverse (Construction Maybe))
        (Construction Maybe)))
  a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (T_U
        Covariant
        Covariant
        (:*:)
        (Reverse (Construction Maybe))
        (Construction Maybe))
     a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (TU
   Covariant
   Covariant
   (Tagged (Zippable (Construction Maybe)))
   (T_U
      Covariant
      Covariant
      (:*:)
      Exactly
      (T_U
         Covariant
         Covariant
         (:*:)
         (Reverse (Construction Maybe))
         (Construction Maybe)))
   a
 -> T_U
      Covariant
      Covariant
      (:*:)
      Exactly
      (T_U
         Covariant
         Covariant
         (:*:)
         (Reverse (Construction Maybe))
         (Construction Maybe))
      a)
-> ((<::>) (Tagged ('Rotate 'Right)) (Tape > Construction Maybe) a
    -> TU
         Covariant
         Covariant
         (Tagged (Zippable (Construction Maybe)))
         (T_U
            Covariant
            Covariant
            (:*:)
            Exactly
            (T_U
               Covariant
               Covariant
               (:*:)
               (Reverse (Construction Maybe))
               (Construction Maybe)))
         a)
-> (<::>) (Tagged ('Rotate 'Right)) (Tape > Construction Maybe) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (T_U
        Covariant
        Covariant
        (:*:)
        (Reverse (Construction Maybe))
        (Construction Maybe))
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>) (Tagged ('Rotate 'Right)) (Tape > Construction Maybe) a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable (Construction Maybe)))
     (T_U
        Covariant
        Covariant
        (:*:)
        Exactly
        (T_U
           Covariant
           Covariant
           (:*:)
           (Reverse (Construction Maybe))
           (Construction Maybe)))
     a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> T_U (Exactly a
x :*: T_U (Reverse Construction Maybe a
left :*: Construction Maybe a
right))) =
		((Maybe :. (Tape > Construction Maybe)) > a)
-> TT Covariant Covariant Maybe (Tape > Construction Maybe) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT (((Maybe :. (Tape > Construction Maybe)) > a)
 -> TT Covariant Covariant Maybe (Tape > Construction Maybe) a)
-> ((Maybe :. (Tape > Construction Maybe)) > a)
-> TT Covariant Covariant Maybe (Tape > Construction Maybe) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<----- Impliable (Tape (Nonempty List) a) =>
Arguments (Tape (Nonempty List) a)
forall k (result :: k). Impliable result => Arguments result
imply @(Tape (Nonempty List) _)
			(a
 -> Construction Maybe a
 -> Construction Maybe a
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable (Construction Maybe)))
      (T_U
         Covariant
         Covariant
         (:*:)
         Exactly
         (T_U
            Covariant
            Covariant
            (:*:)
            (Reverse (Construction Maybe))
            (Construction Maybe)))
      a)
-> Maybe a
-> Maybe
     (Construction Maybe a
      -> Construction Maybe a
      -> TU
           Covariant
           Covariant
           (Tagged (Zippable (Construction Maybe)))
           (T_U
              Covariant
              Covariant
              (:*:)
              Exactly
              (T_U
                 Covariant
                 Covariant
                 (:*:)
                 (Reverse (Construction Maybe))
                 (Construction Maybe)))
           a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-- a -> Maybe a
forall (t :: * -> *) a. Pointable t => a -> t a
point (a -> Maybe a) -> a -> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction Maybe a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Construction Maybe a
right
			Maybe
  (Construction Maybe a
   -> Construction Maybe a
   -> TU
        Covariant
        Covariant
        (Tagged (Zippable (Construction Maybe)))
        (T_U
           Covariant
           Covariant
           (:*:)
           Exactly
           (T_U
              Covariant
              Covariant
              (:*:)
              (Reverse (Construction Maybe))
              (Construction Maybe)))
        a)
-> Maybe (Construction Maybe a)
-> Maybe
     (Construction Maybe a
      -> TU
           Covariant
           Covariant
           (Tagged (Zippable (Construction Maybe)))
           (T_U
              Covariant
              Covariant
              (:*:)
              Exactly
              (T_U
                 Covariant
                 Covariant
                 (:*:)
                 (Reverse (Construction Maybe))
                 (Construction Maybe)))
           a)
forall (t :: * -> *) a b.
(Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*-- Construction Maybe a -> Maybe (Construction Maybe a)
forall (t :: * -> *) a. Pointable t => a -> t a
point (Construction Maybe a -> Maybe (Construction Maybe a))
-> Construction Maybe a -> Maybe (Construction Maybe a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- a :=:=> Construction Maybe
forall k (mod :: k) (struct :: * -> *) a.
Morphed mod struct ((Exactly <:.:> struct) > (->)) =>
a :=:=> struct
item @Push a
x Construction Maybe a
left
			Maybe
  (Construction Maybe a
   -> TU
        Covariant
        Covariant
        (Tagged (Zippable (Construction Maybe)))
        (T_U
           Covariant
           Covariant
           (:*:)
           Exactly
           (T_U
              Covariant
              Covariant
              (:*:)
              (Reverse (Construction Maybe))
              (Construction Maybe)))
        a)
-> Maybe (Construction Maybe a)
-> (Maybe :. (Tape > Construction Maybe)) > a
forall (t :: * -> *) a b.
(Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) =>
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
right

instance Morphable (Into > Tape List) (Construction Maybe) where
	type Morphing (Into > Tape List) (Construction Maybe) = Tape List
	morphing :: (<::>) (Tagged ('Into > Tape List)) (Construction Maybe) a
-> Morphing ('Into > Tape List) (Construction Maybe) a
morphing ((<::>) (Tagged ('Into > Tape List)) (Construction Maybe) a
-> Construction Maybe a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Construction Maybe a
ne) = Impliable (Tape List a) => Arguments (Tape List a)
forall k (result :: k). Impliable result => Arguments result
imply @(Tape List _) (a
 -> TT Covariant Covariant Maybe (Construction Maybe) a
 -> TT Covariant Covariant Maybe (Construction Maybe) a
 -> Tape List a)
-> a
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> Tape List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Construction Maybe a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Construction Maybe a
ne (TT Covariant Covariant Maybe (Construction Maybe) a
 -> TT Covariant Covariant Maybe (Construction Maybe) a
 -> Tape List a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> Tape List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- TT Covariant Covariant Maybe (Construction Maybe) a
forall (t :: * -> *) a. Emptiable t => t a
empty (TT Covariant Covariant Maybe (Construction Maybe) a
 -> Tape List a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> Tape List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- ((Maybe :. Construction Maybe) > a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT (((Maybe :. Construction Maybe) > a)
 -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> ((Maybe :. Construction Maybe) > a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction Maybe a -> (Maybe :. Construction Maybe) > a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) > a
deconstruct Construction Maybe a
ne

--instance Morphable (Into > Tape List) (Tape > Construction Maybe) where
	--type Morphing (Into > Tape List) (Tape > Construction Maybe) = Tape List
	--morphing (premorph -> zipper) = (((((((lift =#-) :*: lift) <-|-<-|-) =#-) <-|-) =#-) =#-) zipper

--instance Morphable (Into > Tape > Construction Maybe) (Tape List) where
	--type Morphing (Into > Tape > Construction Maybe) (Tape List) =
		--Maybe <::> Tape (Construction Maybe)
	--morphing (lower . premorph -> zipper) = let spread x y = (\x' y' -> Reverse x' :*: y') <-|- x <-*- y in
		--lift . TT <--- T_U . (Exactly <-- extract zipper :*:) . T_U <-|- ((spread |-) . ((run . run :*: run) <-|-<-|-) . run . extract <-- run zipper)

instance Morphable (Into > Construction Maybe) (Tape > Construction Maybe) where
	type Morphing (Into > Construction Maybe) (Tape > Construction Maybe) = Construction Maybe
	morphing :: (<::>)
  (Tagged ('Into > Construction Maybe)) (Tape > Construction Maybe) a
-> Morphing
     ('Into > Construction Maybe) (Tape > Construction Maybe) a
morphing (TU
  Covariant
  Covariant
  (Tagged (Zippable (Construction Maybe)))
  (T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (T_U
        Covariant
        Covariant
        (:*:)
        (Reverse (Construction Maybe))
        (Construction Maybe)))
  a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (T_U
        Covariant
        Covariant
        (:*:)
        (Reverse (Construction Maybe))
        (Construction Maybe))
     a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (TU
   Covariant
   Covariant
   (Tagged (Zippable (Construction Maybe)))
   (T_U
      Covariant
      Covariant
      (:*:)
      Exactly
      (T_U
         Covariant
         Covariant
         (:*:)
         (Reverse (Construction Maybe))
         (Construction Maybe)))
   a
 -> T_U
      Covariant
      Covariant
      (:*:)
      Exactly
      (T_U
         Covariant
         Covariant
         (:*:)
         (Reverse (Construction Maybe))
         (Construction Maybe))
      a)
-> ((<::>)
      (Tagged ('Into > Construction Maybe)) (Tape > Construction Maybe) a
    -> TU
         Covariant
         Covariant
         (Tagged (Zippable (Construction Maybe)))
         (T_U
            Covariant
            Covariant
            (:*:)
            Exactly
            (T_U
               Covariant
               Covariant
               (:*:)
               (Reverse (Construction Maybe))
               (Construction Maybe)))
         a)
-> (<::>)
     (Tagged ('Into > Construction Maybe)) (Tape > Construction Maybe) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (T_U
        Covariant
        Covariant
        (:*:)
        (Reverse (Construction Maybe))
        (Construction Maybe))
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>)
  (Tagged ('Into > Construction Maybe)) (Tape > Construction Maybe) a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable (Construction Maybe)))
     (T_U
        Covariant
        Covariant
        (:*:)
        Exactly
        (T_U
           Covariant
           Covariant
           (:*:)
           (Reverse (Construction Maybe))
           (Construction Maybe)))
     a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> T_U (Exactly a
x :*: T_U (Reverse Construction Maybe a
left :*: Construction Maybe a
right))) = (Construction Maybe a
 :*: Construction Maybe (Construction Maybe a))
-> Construction Maybe a
forall a b. (a :*: b) -> a
attached ((Construction Maybe a
  :*: Construction Maybe (Construction Maybe a))
 -> Construction Maybe a)
-> (Construction Maybe a
    :*: Construction Maybe (Construction Maybe a))
-> Construction Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- forall a.
Interpreted (->) (State (Construction Maybe a)) =>
((->) < State (Construction Maybe a) a)
< Primary (State (Construction Maybe a)) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run @(->) @(State _)
		(State
   (Construction Maybe a) (Construction Maybe (Construction Maybe a))
 -> ((->) (Construction Maybe a) :. (:*:) (Construction Maybe a))
    > Construction Maybe (Construction Maybe a))
-> State
     (Construction Maybe a) (Construction Maybe (Construction Maybe a))
-> ((->) (Construction Maybe a) :. (:*:) (Construction Maybe a))
   > Construction Maybe (Construction Maybe a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- forall e r. Modifiable State => Modification State e r
forall k (i :: k) e r. Modifiable i => Modification i e r
modify @State ((Construction Maybe a -> Construction Maybe a)
 -> State (Construction Maybe a) (Construction Maybe a))
-> (a -> Construction Maybe a -> Construction Maybe a)
-> a
-> State (Construction Maybe a) (Construction Maybe a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall a.
Morphed
  'Push (Nonempty List) ((Exactly <:.:> Nonempty List) > (->)) =>
a :=:=> Nonempty List
forall k (mod :: k) (struct :: * -> *) a.
Morphed mod struct ((Exactly <:.:> struct) > (->)) =>
a :=:=> struct
item @Push @(Nonempty List) (a -> State (Construction Maybe a) (Construction Maybe a))
-> Construction Maybe a
-> State
     (Construction Maybe a) (Construction Maybe (Construction Maybe a))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
 Monoidal (Straight source) (Straight target) (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<<- Construction Maybe a
right
		(((->) (Construction Maybe a) :. (:*:) (Construction Maybe a))
 > Construction Maybe (Construction Maybe a))
-> ((->) (Construction Maybe a) :. (:*:) (Construction Maybe a))
   > Construction Maybe (Construction Maybe a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- a -> Construction Maybe a -> Construction Maybe a
forall k (mod :: k) (struct :: * -> *) a.
Morphed mod struct ((Exactly <:.:> struct) > (->)) =>
a :=:=> struct
item @Push a
x Construction Maybe a
left

instance Morphable (Into List) (Tape > Construction Maybe) where
	type Morphing (Into List) (Tape > Construction Maybe) = List
	morphing :: (<::>) (Tagged ('Into List)) (Tape > Construction Maybe) a
-> Morphing ('Into List) (Tape > Construction Maybe) a
morphing (TU
  Covariant
  Covariant
  (Tagged (Zippable (Construction Maybe)))
  (T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (T_U
        Covariant
        Covariant
        (:*:)
        (Reverse (Construction Maybe))
        (Construction Maybe)))
  a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (T_U
        Covariant
        Covariant
        (:*:)
        (Reverse (Construction Maybe))
        (Construction Maybe))
     a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (TU
   Covariant
   Covariant
   (Tagged (Zippable (Construction Maybe)))
   (T_U
      Covariant
      Covariant
      (:*:)
      Exactly
      (T_U
         Covariant
         Covariant
         (:*:)
         (Reverse (Construction Maybe))
         (Construction Maybe)))
   a
 -> T_U
      Covariant
      Covariant
      (:*:)
      Exactly
      (T_U
         Covariant
         Covariant
         (:*:)
         (Reverse (Construction Maybe))
         (Construction Maybe))
      a)
-> ((<::>) (Tagged ('Into List)) (Tape > Construction Maybe) a
    -> TU
         Covariant
         Covariant
         (Tagged (Zippable (Construction Maybe)))
         (T_U
            Covariant
            Covariant
            (:*:)
            Exactly
            (T_U
               Covariant
               Covariant
               (:*:)
               (Reverse (Construction Maybe))
               (Construction Maybe)))
         a)
-> (<::>) (Tagged ('Into List)) (Tape > Construction Maybe) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (T_U
        Covariant
        Covariant
        (:*:)
        (Reverse (Construction Maybe))
        (Construction Maybe))
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>) (Tagged ('Into List)) (Tape > Construction Maybe) a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable (Construction Maybe)))
     (T_U
        Covariant
        Covariant
        (:*:)
        Exactly
        (T_U
           Covariant
           Covariant
           (:*:)
           (Reverse (Construction Maybe))
           (Construction Maybe)))
     a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> T_U (Exactly a
x :*: T_U (Reverse Construction Maybe a
left :*: Construction Maybe a
right))) = (TT Covariant Covariant Maybe (Construction Maybe) a
 :*: Construction
       Maybe (TT Covariant Covariant Maybe (Construction Maybe) a))
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall a b. (a :*: b) -> a
attached ((TT Covariant Covariant Maybe (Construction Maybe) a
  :*: Construction
        Maybe (TT Covariant Covariant Maybe (Construction Maybe) a))
 -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> (TT Covariant Covariant Maybe (Construction Maybe) a
    :*: Construction
          Maybe (TT Covariant Covariant Maybe (Construction Maybe) a))
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- forall a.
Interpreted
  (->)
  (State (TT Covariant Covariant Maybe (Construction Maybe) a)) =>
((->)
 < State (TT Covariant Covariant Maybe (Construction Maybe) a) a)
< Primary
    (State (TT Covariant Covariant Maybe (Construction Maybe) a)) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run @(->) @(State _)
		(State
   (TT Covariant Covariant Maybe (Construction Maybe) a)
   (Construction
      Maybe (TT Covariant Covariant Maybe (Construction Maybe) a))
 -> ((->) (TT Covariant Covariant Maybe (Construction Maybe) a)
     :. (:*:) (TT Covariant Covariant Maybe (Construction Maybe) a))
    > Construction
        Maybe (TT Covariant Covariant Maybe (Construction Maybe) a))
-> State
     (TT Covariant Covariant Maybe (Construction Maybe) a)
     (Construction
        Maybe (TT Covariant Covariant Maybe (Construction Maybe) a))
-> ((->) (TT Covariant Covariant Maybe (Construction Maybe) a)
    :. (:*:) (TT Covariant Covariant Maybe (Construction Maybe) a))
   > Construction
       Maybe (TT Covariant Covariant Maybe (Construction Maybe) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- forall e r. Modifiable State => Modification State e r
forall k (i :: k) e r. Modifiable i => Modification i e r
modify @State ((TT Covariant Covariant Maybe (Construction Maybe) a
  -> TT Covariant Covariant Maybe (Construction Maybe) a)
 -> State
      (TT Covariant Covariant Maybe (Construction Maybe) a)
      (TT Covariant Covariant Maybe (Construction Maybe) a))
-> (a
    -> TT Covariant Covariant Maybe (Construction Maybe) a
    -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> a
-> State
     (TT Covariant Covariant Maybe (Construction Maybe) a)
     (TT Covariant Covariant Maybe (Construction Maybe) a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall a.
Morphed 'Push List ((Exactly <:.:> List) > (->)) =>
a :=:=> List
forall k (mod :: k) (struct :: * -> *) a.
Morphed mod struct ((Exactly <:.:> struct) > (->)) =>
a :=:=> struct
item @Push @List (a
 -> State
      (TT Covariant Covariant Maybe (Construction Maybe) a)
      (TT Covariant Covariant Maybe (Construction Maybe) a))
-> Construction Maybe a
-> State
     (TT Covariant Covariant Maybe (Construction Maybe) a)
     (Construction
        Maybe (TT Covariant Covariant Maybe (Construction Maybe) a))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
 Monoidal (Straight source) (Straight target) (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<<- Construction Maybe a
right
		(((->) (TT Covariant Covariant Maybe (Construction Maybe) a)
  :. (:*:) (TT Covariant Covariant Maybe (Construction Maybe) a))
 > Construction
     Maybe (TT Covariant Covariant Maybe (Construction Maybe) a))
-> ((->) (TT Covariant Covariant Maybe (Construction Maybe) a)
    :. (:*:) (TT Covariant Covariant Maybe (Construction Maybe) a))
   > Construction
       Maybe (TT Covariant Covariant Maybe (Construction Maybe) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- a
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall k (mod :: k) (struct :: * -> *) a.
Morphed mod struct ((Exactly <:.:> struct) > (->)) =>
a :=:=> struct
item @Push a
x (TT Covariant Covariant Maybe (Construction Maybe) a
 -> TT Covariant Covariant Maybe (Construction Maybe) a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction Maybe a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift Construction Maybe a
left

------------------------------------ Zipper of combinative list ------------------------------------

instance Zippable (Comprehension Maybe) where
	type Breadcrumbs (Comprehension Maybe) = Comprehension Maybe <:*:> Comprehension Maybe

----------------------------------------- Prefixed list --------------------------------------------

instance Setoid key => Morphable (Lookup Key) (Prefixed List key) where
	type Morphing (Lookup Key) (Prefixed List key) = (->) key <::> Maybe
	morphing :: (<::>) (Tagged ('Lookup 'Key)) (Prefixed List key) a
-> Morphing ('Lookup 'Key) (Prefixed List key) a
morphing (Prefixed List key a
-> TT Covariant Covariant Maybe (Construction Maybe) (key :*: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Prefixed List key a
 -> TT Covariant Covariant Maybe (Construction Maybe) (key :*: a))
-> ((<::>) (Tagged ('Lookup 'Key)) (Prefixed List key) a
    -> Prefixed List key a)
-> (<::>) (Tagged ('Lookup 'Key)) (Prefixed List key) a
-> TT Covariant Covariant Maybe (Construction Maybe) (key :*: a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>) (Tagged ('Lookup 'Key)) (Prefixed List key) a
-> Prefixed List key a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> TT Covariant Covariant Maybe (Construction Maybe) (key :*: a)
list) = (((->) key :. Maybe) > a)
-> TT Covariant Covariant ((->) key) Maybe a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT ((((->) key :. Maybe) > a)
 -> TT Covariant Covariant ((->) key) Maybe a)
-> (((->) key :. Maybe) > a)
-> TT Covariant Covariant ((->) key) Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \key
key -> key -> Prefixed (Construction Maybe) key a -> Maybe a
forall a1 (mod :: a1) key (struct :: * -> *) a2.
Morphed ('Lookup mod) struct ((->) key <::> Maybe) =>
key -> struct a2 -> Maybe a2
lookup @Key key
key (Prefixed (Construction Maybe) key a -> Maybe a)
-> Maybe (Prefixed (Construction Maybe) key a) -> Maybe a
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
===<< ((Construction Maybe :. (:*:) key) > a)
-> Prefixed (Construction Maybe) key a
forall (t :: * -> *) k a. ((t :. (:*:) k) > a) -> Prefixed t k a
Prefixed (((Construction Maybe :. (:*:) key) > a)
 -> Prefixed (Construction Maybe) key a)
-> Maybe ((Construction Maybe :. (:*:) key) > a)
-> Maybe (Prefixed (Construction Maybe) key a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- TT Covariant Covariant Maybe (Construction Maybe) (key :*: a)
-> Maybe ((Construction Maybe :. (:*:) key) > a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run TT Covariant Covariant Maybe (Construction Maybe) (key :*: a)
list

------------------------------------ Prefixed non-empty list ---------------------------------------

instance Setoid key => Morphable (Lookup Key) (Prefixed < Construction Maybe < key) where
	type Morphing (Lookup Key) (Prefixed < Construction Maybe < key) = (->) key <::> Maybe
	morphing :: (<::>)
  (Tagged ('Lookup 'Key)) ((Prefixed < Construction Maybe) < key) a
-> Morphing
     ('Lookup 'Key) ((Prefixed < Construction Maybe) < key) a
morphing ((<) (Prefixed < Construction Maybe) key a
-> Construction Maybe (key :*: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run ((<) (Prefixed < Construction Maybe) key a
 -> Construction Maybe (key :*: a))
-> ((<::>)
      (Tagged ('Lookup 'Key)) ((Prefixed < Construction Maybe) < key) a
    -> (<) (Prefixed < Construction Maybe) key a)
-> (<::>)
     (Tagged ('Lookup 'Key)) ((Prefixed < Construction Maybe) < key) a
-> Construction Maybe (key :*: a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>)
  (Tagged ('Lookup 'Key)) ((Prefixed < Construction Maybe) < key) a
-> (<) (Prefixed < Construction Maybe) key a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Construct key :*: a
x (Maybe :. Construction Maybe) > (key :*: a)
xs) = (((->) key :. Maybe) > a)
-> TT Covariant Covariant ((->) key) Maybe a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT ((((->) key :. Maybe) > a)
 -> TT Covariant Covariant ((->) key) Maybe a)
-> (((->) key :. Maybe) > a)
-> TT Covariant Covariant ((->) key) Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \key
key -> (key :*: a) -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract ((key :*: a) -> a) -> Maybe (key :*: a) -> Maybe a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- key -> Maybe (key :*: a)
search key
key where
		search :: key -> Maybe (key :*: a)
search key
key = key
key key
-> key
-> Maybe (key :*: a)
-> Maybe (key :*: a)
-> Maybe (key :*: a)
forall a r. Setoid a => a -> a -> r -> r -> r
?= (key :*: a) -> key
forall a b. (a :*: b) -> a
attached key :*: a
x
			(Maybe (key :*: a) -> Maybe (key :*: a) -> Maybe (key :*: a))
-> Maybe (key :*: a) -> Maybe (key :*: a) -> Maybe (key :*: a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<----- (key :*: a) -> Maybe (key :*: a)
forall a. a -> Maybe a
Just key :*: a
x
			(Maybe (key :*: a) -> Maybe (key :*: a))
-> Maybe (key :*: a) -> Maybe (key :*: a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<----- forall a1 (mod :: a1) (struct :: * -> *) (result :: * -> *) a2.
Morphed ('Find mod) struct ((Predicate <:.:> result) > (->)) =>
Predicate a2 -> struct a2 -> result a2
forall (struct :: * -> *) (result :: * -> *) a2.
Morphed
  ('Find 'Element) struct ((Predicate <:.:> result) > (->)) =>
Predicate a2 -> struct a2 -> result a2
find @Element (Predicate (key :*: a)
 -> Construction Maybe (key :*: a) -> Maybe (key :*: a))
-> Predicate (key :*: a)
-> Construction Maybe (key :*: a)
-> Maybe (key :*: a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- ((key :*: a) -> Boolean) -> Predicate (key :*: a)
forall a. (a -> Boolean) -> Predicate a
Predicate (((key :*: a) -> Boolean) -> Predicate (key :*: a))
-> ((key :*: a) -> Boolean) -> Predicate (key :*: a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (key
key key -> key -> Boolean
forall a. Setoid a => a -> a -> Boolean
==) (key -> Boolean) -> ((key :*: a) -> key) -> (key :*: a) -> Boolean
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (key :*: a) -> key
forall a b. (a :*: b) -> a
attached (Construction Maybe (key :*: a) -> Maybe (key :*: a))
-> ((Maybe :. Construction Maybe) > (key :*: a))
-> Maybe (key :*: a)
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
===<< (Maybe :. Construction Maybe) > (key :*: a)
xs