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

module Pandora.Paradigm.Structure.Some.List where

import Pandora.Core.Functor (type (:.), type (:=))
import Pandora.Pattern.Category ((.), ($), (#), identity)
import Pandora.Pattern.Functor.Covariant (Covariant ((<$>), (.#..)))
import Pandora.Pattern.Functor.Applicative (Applicative ((<*>)))
import Pandora.Pattern.Functor.Extractable (extract)
import Pandora.Pattern.Functor.Avoidable (empty)
import Pandora.Pattern.Functor.Traversable (Traversable ((->>)))
import Pandora.Pattern.Functor.Extendable (Extendable ((=>>)))
import Pandora.Pattern.Functor.Bindable ((>>=))
import Pandora.Pattern.Functor.Bivariant ((<->))
import Pandora.Pattern.Functor.Adjoint ((|-))
import Pandora.Pattern.Functor ()
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.Primary.Object.Boolean (Boolean (True, False), (?))
import Pandora.Paradigm.Primary.Object.Numerator (Numerator (Numerator))
import Pandora.Paradigm.Primary.Object.Denumerator (Denumerator (One))
import Pandora.Paradigm.Primary.Functor.Function ((%))
import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Just, Nothing))
import Pandora.Paradigm.Primary.Functor.Identity (Identity (Identity))
import Pandora.Paradigm.Primary.Functor.Predicate (Predicate (Predicate))
import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)), type (:*:), attached, twosome)
import Pandora.Paradigm.Primary.Functor.Wye (Wye (Left, Right))
import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct), deconstruct, (.-+))
import Pandora.Paradigm.Primary.Transformer.Tap (Tap (Tap))
import Pandora.Paradigm.Primary.Transformer.Reverse (Reverse (Reverse))
import Pandora.Paradigm.Inventory.State (State, fold, modify)
import Pandora.Paradigm.Inventory.Store (Store (Store))
import Pandora.Paradigm.Inventory.Optics (view)
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run, (||=))
import Pandora.Paradigm.Schemes.TU (TU (TU), type (<:.>))
import Pandora.Paradigm.Schemes.T_U (T_U (T_U), type (<:.:>))
import Pandora.Paradigm.Schemes.PQ_ (PQ_ (PQ_))
import Pandora.Paradigm.Structure.Ability.Nonempty (Nonempty)
import Pandora.Paradigm.Structure.Ability.Nullable (Nullable (null))
import Pandora.Paradigm.Structure.Ability.Zipper (Zipper)
-- import Pandora.Paradigm.Structure.Ability.Focusable ()
import Pandora.Paradigm.Structure.Ability.Measurable (Measurable (Measural, measurement), Scale (Length), measure)
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 (Substructural, substructure, sub), Segment (Root, Tail))
import Pandora.Paradigm.Structure.Interface.Stack (Stack)
import Pandora.Paradigm.Structure.Modification.Combinative (Combinative)
import Pandora.Paradigm.Structure.Modification.Comprehension (Comprehension (Comprehension))
import Pandora.Paradigm.Structure.Modification.Prefixed (Prefixed (Prefixed))

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

instance Setoid a => Setoid (List a) where
	TU (Maybe :. Construction Maybe) := a
ls == :: List a -> List a -> Boolean
== TU (Maybe :. Construction Maybe) := a
rs = (Maybe :. Construction Maybe) := a
ls ((Maybe :. Construction Maybe) := a)
-> ((Maybe :. Construction Maybe) := a) -> Boolean
forall a. Setoid a => a -> a -> Boolean
== (Maybe :. Construction Maybe) := a
rs

instance Semigroup (List a) where
	TU Maybe (Construction Maybe a)
Nothing + :: List a -> List a -> List a
+ TU Maybe (Construction Maybe a)
ys = Maybe (Construction Maybe a) -> List a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU Maybe (Construction Maybe a)
ys
	TU (Just (Construct a
x Maybe (Construction Maybe a)
xs)) + TU Maybe (Construction Maybe a)
ys = Construction Maybe a -> List a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Maybe a -> List a)
-> (List a -> Construction Maybe a) -> List a -> List a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Maybe (Construction Maybe a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Maybe (Construction Maybe a) -> Construction Maybe a)
-> (List a -> Maybe (Construction Maybe a))
-> List a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. List a -> Maybe (Construction Maybe a)
forall (t :: * -> *) a. Interpreted t => 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) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU @Covariant @Covariant Maybe (Construction Maybe a)
xs 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) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU @Covariant @Covariant Maybe (Construction Maybe a)
ys

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

instance Morphable Push List where
	type Morphing Push List = Identity <:.:> 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) = (Identity a -> List a)
-> T_U Covariant Covariant (->) Identity 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 ((Identity a -> List a)
 -> T_U Covariant Covariant (->) Identity List a)
-> (Identity a -> List a)
-> T_U Covariant Covariant (->) Identity List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Construction Maybe a -> List a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Maybe a -> List a)
-> (Identity a -> Construction Maybe a) -> Identity a -> List a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a)
-> ((Maybe :. Construction Maybe) := a)
-> a
-> Construction Maybe a
forall a b c. (a -> b -> c) -> b -> a -> c
% List a -> Primary List a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run List a
xs) (a -> Construction Maybe a)
-> (Identity a -> a) -> Identity a -> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Identity a -> a
forall (t :: * -> *) a. Extractable t => a <:= t
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 (t :: * -> *) (u :: * -> *) a b.
(Interpreted t, Interpreted u) =>
(Primary t a -> Primary u b) -> 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 a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> TU 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
	morphing ((<:.>) (Tagged ('Find 'Element)) List a -> List a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> TU (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 -> a -> Boolean
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run Predicate a
p a
x Boolean -> Maybe a -> Maybe a -> Maybe a
forall a. Boolean -> a -> a -> a
? 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 -> List a -> Maybe a)
-> Predicate a -> List a -> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Predicate a
p (List a -> Maybe a) -> List a -> Maybe 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) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU 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 a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> TU Maybe (Construction Maybe a)
Nothing) = (Predicate a -> List 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 -> List a)
 -> T_U Covariant Covariant (->) Predicate List a)
-> (Predicate a -> List a)
-> T_U Covariant Covariant (->) Predicate List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \Predicate a
_ -> Maybe (Construction Maybe a) -> List a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU Maybe (Construction Maybe a)
forall a. Maybe a
Nothing
	morphing ((<:.>) (Tagged ('Delete 'First)) List a -> List a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> TU (Just (Construct a
x Maybe (Construction Maybe a)
xs))) = (Predicate a -> List 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 -> List a)
 -> T_U Covariant Covariant (->) Predicate List a)
-> (Predicate a -> List 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 -> a -> Boolean
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run Predicate a
p a
x Boolean -> List a -> List a -> List a
forall a. Boolean -> a -> a -> a
? Maybe (Construction Maybe a) -> List a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU Maybe (Construction Maybe a)
xs (List a -> List a) -> List a -> List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Construction Maybe a -> List a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Maybe a -> List a)
-> (List a -> Construction Maybe a) -> List a -> List a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Maybe (Construction Maybe a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Maybe (Construction Maybe a) -> Construction Maybe a)
-> (List a -> Maybe (Construction Maybe a))
-> List a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. List a -> Maybe (Construction Maybe a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (List a -> Maybe (Construction Maybe a))
-> (List a -> List a) -> List a -> Maybe (Construction Maybe a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Predicate a -> List a -> List 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 (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) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU 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 a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> TU Maybe (Construction Maybe a)
Nothing) = (Predicate a -> List 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 -> List a)
 -> T_U Covariant Covariant (->) Predicate List a)
-> (Predicate a -> List a)
-> T_U Covariant Covariant (->) Predicate List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \Predicate a
_ -> Maybe (Construction Maybe a) -> List a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU Maybe (Construction Maybe a)
forall a. Maybe a
Nothing
	morphing ((<:.>) (Tagged ('Delete 'All)) List a -> List a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> TU (Just (Construct a
x Maybe (Construction Maybe a)
xs))) = (Predicate a -> List 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 -> List a)
 -> T_U Covariant Covariant (->) Predicate List a)
-> (Predicate a -> List 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 -> a -> Boolean
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run Predicate a
p a
x Boolean -> List a -> List a -> List a
forall a. Boolean -> a -> a -> a
? Predicate a -> List a -> List 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 (Maybe (Construction Maybe a) -> List a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU Maybe (Construction Maybe a)
xs) (List a -> List a) -> List a -> List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Construction Maybe a -> List a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Maybe a -> List a)
-> (List a -> Construction Maybe a) -> List a -> List a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Maybe (Construction Maybe a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Maybe (Construction Maybe a) -> Construction Maybe a)
-> (List a -> Maybe (Construction Maybe a))
-> List a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. List a -> Maybe (Construction Maybe a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (List a -> Maybe (Construction Maybe a))
-> (List a -> List a) -> List a -> Maybe (Construction Maybe a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Predicate a -> List a -> List 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 (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) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU Maybe (Construction Maybe a)
xs

instance Stack List where

instance Measurable Length List where
	type Measural Length List a = Numerator
	measurement :: Tagged 'Length (List a) -> Measural 'Length List a
measurement (List a -> Maybe (Construction Maybe a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (List a -> Maybe (Construction Maybe a))
-> (Tagged 'Length (List a) -> List a)
-> Tagged 'Length (List a)
-> Maybe (Construction Maybe a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged 'Length (List a) -> List a
forall (t :: * -> *) a. Extractable t => a <:= t
extract -> Maybe (Construction Maybe a)
Nothing) = Measural 'Length List a
forall a. Monoid a => a
zero
	measurement (List a -> Maybe (Construction Maybe a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (List a -> Maybe (Construction Maybe a))
-> (Tagged 'Length (List a) -> List a)
-> Tagged 'Length (List a)
-> Maybe (Construction Maybe a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged 'Length (List a) -> List a
forall (t :: * -> *) a. Extractable t => a <:= t
extract -> Just Construction Maybe a
xs) = Denumerator -> Numerator
Numerator (Denumerator -> Numerator) -> Denumerator -> Numerator
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Construction Maybe a -> Measural 'Length (Construction Maybe) a
forall k (f :: k) (t :: * -> *) a.
Measurable f t =>
t a -> Measural f t a
measure @Length Construction Maybe a
xs

instance Nullable List where
	null :: (Predicate :. List) := a
null = (List a -> Boolean) -> (Predicate :. List) := a
forall a. (a -> Boolean) -> Predicate a
Predicate ((List a -> Boolean) -> (Predicate :. List) := a)
-> (List a -> Boolean) -> (Predicate :. List) := a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \case { TU Maybe (Construction Maybe a)
Nothing -> Boolean
True ; List a
_ -> Boolean
False }

instance Substructure Root List where
	type Substructural Root List = Maybe
	substructure :: Lens ((<:.>) (Tagged 'Root) List a) (Substructural 'Root List a)
substructure = ((<:.>) (Tagged 'Root) List a
 -> Store (Maybe a) ((<:.>) (Tagged 'Root) List a))
-> PQ_ (->) Store ((<:.>) (Tagged 'Root) List a) (Maybe a)
forall k k k (p :: k -> k -> *) (q :: k -> k -> k) (a :: k)
       (b :: k).
p a (q b a) -> PQ_ p q a b
PQ_ (((<:.>) (Tagged 'Root) List a
  -> Store (Maybe a) ((<:.>) (Tagged 'Root) List a))
 -> PQ_ (->) Store ((<:.>) (Tagged 'Root) List a) (Maybe a))
-> ((<:.>) (Tagged 'Root) List a
    -> Store (Maybe a) ((<:.>) (Tagged 'Root) List a))
-> PQ_ (->) Store ((<:.>) (Tagged 'Root) List a) (Maybe a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>) (Tagged 'Root) List a
zipper -> case TU Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (TU Covariant Covariant Maybe (Construction Maybe) a
 -> (Maybe :. Construction Maybe) := a)
-> TU 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
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Lowerable t, Covariant u) =>
t u ~> u
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 -> Product s a
:*: TU Covariant Covariant Maybe (Construction Maybe) a
-> (<:.>) (Tagged 'Root) List a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (TU Covariant Covariant Maybe (Construction Maybe) a
 -> (<:.>) (Tagged 'Root) List a)
-> (Maybe a -> TU Covariant Covariant Maybe (Construction Maybe) a)
-> Maybe a
-> (<:.>) (Tagged 'Root) List a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (a -> TU Covariant Covariant Maybe (Construction Maybe) a)
-> TU Covariant Covariant Maybe (Construction Maybe) a
-> Maybe a
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve (Construction Maybe a
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Maybe a
 -> TU Covariant Covariant Maybe (Construction Maybe) a)
-> (a -> Construction Maybe a)
-> a
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (a -> ((Maybe :. Construction Maybe) := a) -> 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)) TU Covariant Covariant Maybe (Construction Maybe) a
forall (t :: * -> *) a. Avoidable t => t a
empty
		(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 -> Product s a
:*: TU Covariant Covariant Maybe (Construction Maybe) a
-> (<:.>) (Tagged 'Root) List a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (TU Covariant Covariant Maybe (Construction Maybe) a
 -> (<:.>) (Tagged 'Root) List a)
-> (Maybe a -> TU Covariant Covariant Maybe (Construction Maybe) a)
-> Maybe a
-> (<:.>) (Tagged 'Root) List a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (a -> TU Covariant Covariant Maybe (Construction Maybe) a)
-> TU Covariant Covariant Maybe (Construction Maybe) a
-> Maybe a
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve (Construction Maybe a
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Maybe a
 -> TU Covariant Covariant Maybe (Construction Maybe) a)
-> (a -> Construction Maybe a)
-> a
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (a -> ((Maybe :. Construction Maybe) := a) -> 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
forall (t :: * -> *) a. Avoidable t => t a
empty)) TU Covariant Covariant Maybe (Construction Maybe) a
forall (t :: * -> *) a. Avoidable t => t a
empty

instance Substructure Tail List where
	type Substructural Tail List = List
	substructure :: Lens ((<:.>) (Tagged 'Tail) List a) (Substructural 'Tail List a)
substructure = ((<:.>) (Tagged 'Tail) List a
 -> Store
      (TU Covariant Covariant Maybe (Construction Maybe) a)
      ((<:.>) (Tagged 'Tail) List a))
-> PQ_
     (->)
     Store
     ((<:.>) (Tagged 'Tail) List a)
     (TU Covariant Covariant Maybe (Construction Maybe) a)
forall k k k (p :: k -> k -> *) (q :: k -> k -> k) (a :: k)
       (b :: k).
p a (q b a) -> PQ_ p q a b
PQ_ (((<:.>) (Tagged 'Tail) List a
  -> Store
       (TU Covariant Covariant Maybe (Construction Maybe) a)
       ((<:.>) (Tagged 'Tail) List a))
 -> PQ_
      (->)
      Store
      ((<:.>) (Tagged 'Tail) List a)
      (TU Covariant Covariant Maybe (Construction Maybe) a))
-> ((<:.>) (Tagged 'Tail) List a
    -> Store
         (TU Covariant Covariant Maybe (Construction Maybe) a)
         ((<:.>) (Tagged 'Tail) List a))
-> PQ_
     (->)
     Store
     ((<:.>) (Tagged 'Tail) List a)
     (TU Covariant Covariant Maybe (Construction Maybe) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>) (Tagged 'Tail) List a
x -> case TU Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (TU Covariant Covariant Maybe (Construction Maybe) a
 -> (Maybe :. Construction Maybe) := a)
-> ((<:.>) (Tagged 'Tail) List a
    -> TU Covariant Covariant Maybe (Construction Maybe) a)
-> (<:.>) (Tagged 'Tail) List a
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction Maybe) a
<:= Tagged 'Tail
forall (t :: * -> *) a. Extractable t => a <:= t
extract (TU Covariant Covariant Maybe (Construction Maybe) a
 <:= Tagged 'Tail)
-> ((<:.>) (Tagged 'Tail) List a
    -> Tagged
         'Tail (TU Covariant Covariant Maybe (Construction Maybe) a))
-> (<:.>) (Tagged 'Tail) List a
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Tail) List a
-> Tagged
     'Tail (TU Covariant Covariant Maybe (Construction Maybe) a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run ((<:.>) (Tagged 'Tail) List a
 -> (Maybe :. Construction Maybe) := a)
-> (<:.>) (Tagged 'Tail) List a
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ (<:.>) (Tagged 'Tail) List a
x of
		Just Construction Maybe a
ns -> TU Covariant Covariant Maybe (Construction Maybe) a
-> (<:.>) (Tagged 'Tail) List a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (TU Covariant Covariant Maybe (Construction Maybe) a
 -> (<:.>) (Tagged 'Tail) List a)
-> (Construction Maybe a
    -> TU Covariant Covariant Maybe (Construction Maybe) a)
-> Construction Maybe a
-> (<:.>) (Tagged 'Tail) List a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Maybe a
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Maybe a -> (<:.>) (Tagged 'Tail) List a)
-> Store
     (TU Covariant Covariant Maybe (Construction Maybe) a)
     (Construction Maybe a)
-> Store
     (TU Covariant Covariant Maybe (Construction Maybe) a)
     ((<:.>) (Tagged 'Tail) List a)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> PQ_
  (->)
  Store
  (Construction Maybe a)
  (TU Covariant Covariant Maybe (Construction Maybe) a)
-> Construction Maybe a
-> Store
     (TU Covariant Covariant Maybe (Construction Maybe) a)
     (Construction Maybe a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (forall k (f :: k) (t :: * -> *).
(Substructure f t, Covariant t) =>
t :~. Substructural f t
forall (t :: * -> *).
(Substructure 'Tail t, Covariant t) =>
t :~. Substructural 'Tail t
sub @Tail) Construction Maybe a
ns
		(Maybe :. Construction Maybe) := a
Nothing -> (((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
  :. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
 := (<:.>) (Tagged 'Tail) List a)
-> Store
     (TU Covariant Covariant Maybe (Construction Maybe) a)
     ((<:.>) (Tagged 'Tail) List a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
   :. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
  := (<:.>) (Tagged 'Tail) List a)
 -> Store
      (TU Covariant Covariant Maybe (Construction Maybe) a)
      ((<:.>) (Tagged 'Tail) List a))
-> (((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
     :. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
    := (<:.>) (Tagged 'Tail) List a)
-> Store
     (TU Covariant Covariant Maybe (Construction Maybe) a)
     ((<:.>) (Tagged 'Tail) List a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ TU Covariant Covariant Maybe (Construction Maybe) a
forall (t :: * -> *) a. Avoidable t => t a
empty TU Covariant Covariant Maybe (Construction Maybe) a
-> (TU Covariant Covariant Maybe (Construction Maybe) a
    -> (<:.>) (Tagged 'Tail) List a)
-> ((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
    :. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
   := (<:.>) (Tagged 'Tail) List a
forall s a. s -> a -> Product s a
:*: TU Covariant Covariant Maybe (Construction Maybe) a
-> (<:.>) (Tagged 'Tail) List a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (TU Covariant Covariant Maybe (Construction Maybe) a
 -> (<:.>) (Tagged 'Tail) List a)
-> (TU Covariant Covariant Maybe (Construction Maybe) a
    -> TU Covariant Covariant Maybe (Construction Maybe) a)
-> TU Covariant Covariant Maybe (Construction Maybe) a
-> (<:.>) (Tagged 'Tail) List a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction Maybe) a
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) a. Category m => m a a
identity

-- | Transform any traversable structure into a stack
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) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (((Maybe :. Construction Maybe) := a) -> List a)
-> (t a -> (Maybe :. Construction Maybe) := a) -> t a -> List a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. ((Maybe :. Construction Maybe) := a)
<:= Product ((Maybe :. Construction Maybe) := a)
forall (t :: * -> *) a. Extractable t => a <:= t
extract (((Maybe :. Construction Maybe) := a)
 <:= Product ((Maybe :. Construction Maybe) := a))
-> (t a
    -> Product
         ((Maybe :. Construction Maybe) := a)
         ((Maybe :. Construction Maybe) := a))
-> t a
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (forall a.
Interpreted (State ((Maybe :. Nonempty List) := a)) =>
State ((Maybe :. Nonempty List) := a) a
-> Primary (State ((Maybe :. Nonempty List) := a)) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run @(State (Maybe :. Nonempty List := a)) (State
   ((Maybe :. Construction Maybe) := a)
   ((Maybe :. Construction Maybe) := a)
 -> ((Maybe :. Construction Maybe) := a)
 -> Product
      ((Maybe :. Construction Maybe) := a)
      ((Maybe :. Construction Maybe) := a))
-> ((Maybe :. Construction Maybe) := a)
-> State
     ((Maybe :. Construction Maybe) := a)
     ((Maybe :. Construction Maybe) := a)
-> Product
     ((Maybe :. Construction Maybe) := a)
     ((Maybe :. Construction Maybe) := a)
forall a b c. (a -> b -> c) -> b -> a -> c
% (Maybe :. Construction Maybe) := a
forall a. Maybe a
Nothing) (State
   ((Maybe :. Construction Maybe) := a)
   ((Maybe :. Construction Maybe) := a)
 -> Product
      ((Maybe :. Construction Maybe) := a)
      ((Maybe :. Construction Maybe) := a))
-> (t a
    -> State
         ((Maybe :. Construction Maybe) := a)
         ((Maybe :. Construction Maybe) := a))
-> t a
-> Product
     ((Maybe :. Construction Maybe) := a)
     ((Maybe :. Construction Maybe) := a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (a
 -> ((Maybe :. Construction Maybe) := a)
 -> (Maybe :. Construction Maybe) := a)
-> t a
-> State
     ((Maybe :. Construction Maybe) := a)
     ((Maybe :. Construction Maybe) := a)
forall (t :: * -> *) s (u :: * -> *) a.
(Traversable t, Memorable s u) =>
(a -> s -> s) -> t a -> u s
fold (Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall a. a -> Maybe a
Just (Construction Maybe a -> (Maybe :. Construction Maybe) := a)
-> (((->) a :. (->) ((Maybe :. Construction Maybe) := a))
    := Construction Maybe a)
-> a
-> ((Maybe :. Construction Maybe) := a)
-> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) (v :: * -> * -> *) a c d b.
(Covariant t, t ~ v a, Category v) =>
v c d -> ((v a :. v b) := c) -> (v a :. v b) := d
.#.. ((->) a :. (->) ((Maybe :. Construction Maybe) := a))
:= Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct)

----------------------------------------- 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.
Category m =>
m b c -> m a b -> m a c
. Construction Maybe a -> Maybe (Construction Maybe a)
forall a. a -> Maybe a
Just (Construction Maybe a -> Construction Maybe a)
-> Construction Maybe a -> Construction Maybe a
forall (m :: * -> * -> *) a b. Category m => m (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 -> a -> Boolean
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run Predicate a
p a
x Boolean -> Maybe a -> Maybe a -> Maybe a
forall a. Boolean -> a -> a -> a
? 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)
$ (Maybe :. Construction Maybe) := a
xs ((Maybe :. Construction Maybe) := a)
-> (Construction Maybe a -> Maybe a) -> Maybe a
forall (t :: * -> *) a b. Bindable t => t a -> (a -> t b) -> t 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

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
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Maybe a
 -> TU Covariant Covariant Maybe (Construction Maybe) a)
-> ((<:.>) (Tagged ('Into List)) (Construction Maybe) a
    -> Construction Maybe a)
-> (<:.>) (Tagged ('Into List)) (Construction Maybe) a
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged ('Into List)) (Construction Maybe) a
-> Construction Maybe a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph

instance Morphable Push (Construction Maybe) where
	type Morphing Push (Construction Maybe) = Identity <:.:> 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) = (Identity a -> Construction Maybe a)
-> T_U Covariant Covariant (->) Identity (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 ((Identity a -> Construction Maybe a)
 -> T_U Covariant Covariant (->) Identity (Construction Maybe) a)
-> (Identity a -> Construction Maybe a)
-> T_U Covariant Covariant (->) Identity (Construction Maybe) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(Identity 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 Measurable Length (Construction Maybe) where
	type Measural Length (Construction Maybe) a = Denumerator
	measurement :: Tagged 'Length (Construction Maybe a)
-> Measural 'Length (Construction Maybe) a
measurement (Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct (Construction Maybe a -> (Maybe :. Construction Maybe) := a)
-> (Tagged 'Length (Construction Maybe a) -> Construction Maybe a)
-> Tagged 'Length (Construction Maybe a)
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged 'Length (Construction Maybe a) -> Construction Maybe a
forall (t :: * -> *) a. Extractable t => a <:= t
extract -> (Maybe :. Construction Maybe) := a
Nothing) = Denumerator
Measural 'Length (Construction Maybe) a
One
	measurement (Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct (Construction Maybe a -> (Maybe :. Construction Maybe) := a)
-> (Tagged 'Length (Construction Maybe a) -> Construction Maybe a)
-> Tagged 'Length (Construction Maybe a)
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged 'Length (Construction Maybe a) -> Construction Maybe a
forall (t :: * -> *) a. Extractable t => a <:= t
extract -> Just Construction Maybe a
xs) = Denumerator
One Denumerator -> Denumerator -> Denumerator
forall a. Semigroup a => a -> a -> a
+ Construction Maybe a -> Measural 'Length (Construction Maybe) a
forall k (f :: k) (t :: * -> *) a.
Measurable f t =>
t a -> Measural f t a
measure @Length Construction Maybe a
xs

instance Substructure Root (Construction Maybe) where
	type Substructural Root (Construction Maybe) = Identity
	substructure :: Lens
  ((<:.>) (Tagged 'Root) (Construction Maybe) a)
  (Substructural 'Root (Construction Maybe) a)
substructure = ((<:.>) (Tagged 'Root) (Construction Maybe) a
 -> Store
      (Identity a) ((<:.>) (Tagged 'Root) (Construction Maybe) a))
-> PQ_
     (->)
     Store
     ((<:.>) (Tagged 'Root) (Construction Maybe) a)
     (Identity a)
forall k k k (p :: k -> k -> *) (q :: k -> k -> k) (a :: k)
       (b :: k).
p a (q b a) -> PQ_ p q a b
PQ_ (((<:.>) (Tagged 'Root) (Construction Maybe) a
  -> Store
       (Identity a) ((<:.>) (Tagged 'Root) (Construction Maybe) a))
 -> PQ_
      (->)
      Store
      ((<:.>) (Tagged 'Root) (Construction Maybe) a)
      (Identity a))
-> ((<:.>) (Tagged 'Root) (Construction Maybe) a
    -> Store
         (Identity a) ((<:.>) (Tagged 'Root) (Construction Maybe) a))
-> PQ_
     (->)
     Store
     ((<:.>) (Tagged 'Root) (Construction Maybe) a)
     (Identity a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>) (Tagged 'Root) (Construction Maybe) a
zipper -> case (<:.>) (Tagged 'Root) (Construction Maybe) a
-> Construction Maybe a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Lowerable t, Covariant u) =>
t u ~> u
lower (<:.>) (Tagged 'Root) (Construction Maybe) a
zipper of
		Construct a
x (Maybe :. Construction Maybe) := a
xs -> (((:*:) (Identity a) :. (->) (Identity a))
 := (<:.>) (Tagged 'Root) (Construction Maybe) a)
-> Store
     (Identity a) ((<:.>) (Tagged 'Root) (Construction Maybe) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity a) :. (->) (Identity a))
  := (<:.>) (Tagged 'Root) (Construction Maybe) a)
 -> Store
      (Identity a) ((<:.>) (Tagged 'Root) (Construction Maybe) a))
-> (((:*:) (Identity a) :. (->) (Identity a))
    := (<:.>) (Tagged 'Root) (Construction Maybe) a)
-> Store
     (Identity a) ((<:.>) (Tagged 'Root) (Construction Maybe) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a -> Identity a
forall a. a -> Identity a
Identity a
x Identity a
-> (Identity a -> (<:.>) (Tagged 'Root) (Construction Maybe) a)
-> ((:*:) (Identity a) :. (->) (Identity a))
   := (<:.>) (Tagged 'Root) (Construction Maybe) a
forall s a. s -> a -> Product s a
:*: Construction Maybe a
-> (<:.>) (Tagged 'Root) (Construction Maybe) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Maybe a
 -> (<:.>) (Tagged 'Root) (Construction Maybe) a)
-> (Identity a -> Construction Maybe a)
-> Identity a
-> (<:.>) (Tagged 'Root) (Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a)
-> ((Maybe :. Construction Maybe) := a)
-> a
-> Construction Maybe a
forall a b c. (a -> b -> c) -> b -> a -> c
% (Maybe :. Construction Maybe) := a
xs) (a -> Construction Maybe a)
-> (Identity a -> a) -> Identity a -> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Identity a -> a
forall (t :: * -> *) a. Extractable t => a <:= t
extract

instance Substructure Tail (Construction Maybe) where
	type Substructural Tail (Construction Maybe) = List
	substructure :: Lens
  ((<:.>) (Tagged 'Tail) (Construction Maybe) a)
  (Substructural 'Tail (Construction Maybe) a)
substructure = ((<:.>) (Tagged 'Tail) (Construction Maybe) a
 -> Store
      (TU Covariant Covariant Maybe (Construction Maybe) a)
      ((<:.>) (Tagged 'Tail) (Construction Maybe) a))
-> PQ_
     (->)
     Store
     ((<:.>) (Tagged 'Tail) (Construction Maybe) a)
     (TU Covariant Covariant Maybe (Construction Maybe) a)
forall k k k (p :: k -> k -> *) (q :: k -> k -> k) (a :: k)
       (b :: k).
p a (q b a) -> PQ_ p q a b
PQ_ (((<:.>) (Tagged 'Tail) (Construction Maybe) a
  -> Store
       (TU Covariant Covariant Maybe (Construction Maybe) a)
       ((<:.>) (Tagged 'Tail) (Construction Maybe) a))
 -> PQ_
      (->)
      Store
      ((<:.>) (Tagged 'Tail) (Construction Maybe) a)
      (TU Covariant Covariant Maybe (Construction Maybe) a))
-> ((<:.>) (Tagged 'Tail) (Construction Maybe) a
    -> Store
         (TU Covariant Covariant Maybe (Construction Maybe) a)
         ((<:.>) (Tagged 'Tail) (Construction Maybe) a))
-> PQ_
     (->)
     Store
     ((<:.>) (Tagged 'Tail) (Construction Maybe) a)
     (TU Covariant Covariant Maybe (Construction Maybe) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>) (Tagged 'Tail) (Construction Maybe) a
stack -> case Construction Maybe a <:= Tagged 'Tail
forall (t :: * -> *) a. Extractable t => a <:= t
extract (Construction Maybe a <:= Tagged 'Tail)
-> Construction Maybe a <:= Tagged 'Tail
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ (<:.>) (Tagged 'Tail) (Construction Maybe) a
-> Primary (Tagged 'Tail <:.> Construction Maybe) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (<:.>) (Tagged 'Tail) (Construction Maybe) a
stack of
		Construct a
x (Maybe :. Construction Maybe) := a
xs -> (((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
  :. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
 := (<:.>) (Tagged 'Tail) (Construction Maybe) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Maybe) a)
     ((<:.>) (Tagged 'Tail) (Construction Maybe) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
   :. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
  := (<:.>) (Tagged 'Tail) (Construction Maybe) a)
 -> Store
      (TU Covariant Covariant Maybe (Construction Maybe) a)
      ((<:.>) (Tagged 'Tail) (Construction Maybe) a))
-> (((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
     :. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
    := (<:.>) (Tagged 'Tail) (Construction Maybe) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Maybe) a)
     ((<:.>) (Tagged 'Tail) (Construction Maybe) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ ((Maybe :. Construction Maybe) := a)
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (Maybe :. Construction Maybe) := a
xs TU Covariant Covariant Maybe (Construction Maybe) a
-> (TU Covariant Covariant Maybe (Construction Maybe) a
    -> (<:.>) (Tagged 'Tail) (Construction Maybe) a)
-> ((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
    :. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
   := (<:.>) (Tagged 'Tail) (Construction Maybe) a
forall s a. s -> a -> Product s a
:*: Construction Maybe a
-> (<:.>) (Tagged 'Tail) (Construction Maybe) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Maybe a
 -> (<:.>) (Tagged 'Tail) (Construction Maybe) a)
-> (TU Covariant Covariant Maybe (Construction Maybe) a
    -> Construction Maybe a)
-> TU Covariant Covariant Maybe (Construction Maybe) a
-> (<:.>) (Tagged 'Tail) (Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (((Maybe :. Construction Maybe) := a) -> Construction Maybe a)
-> (TU Covariant Covariant Maybe (Construction Maybe) a
    -> (Maybe :. Construction Maybe) := a)
-> TU Covariant Covariant Maybe (Construction Maybe) a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run

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

type instance Combinative List = Comprehension Maybe

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

type instance Zipper List = Tap (List <:.:> List := (:*:))

instance {-# OVERLAPS #-} Applicative (Tap (List <:.:> List := (:*:))) where
	Tap a -> b
f (T_U (List (a -> b)
lfs :*: List (a -> b)
rfs)) <*> :: Tap ((List <:.:> List) := (:*:)) (a -> b)
-> Tap ((List <:.:> List) := (:*:)) a
-> Tap ((List <:.:> List) := (:*:)) b
<*> Tap a
x (T_U (List a
ls :*: List a
rs)) = b
-> (:=) (List <:.:> List) (:*:) b
-> Tap ((List <:.:> List) := (:*:)) b
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (b
 -> (:=) (List <:.:> List) (:*:) b
 -> Tap ((List <:.:> List) := (:*:)) b)
-> b
-> (:=) (List <:.:> List) (:*:) b
-> Tap ((List <:.:> List) := (:*:)) b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# a -> b
f a
x ((:=) (List <:.:> List) (:*:) b
 -> Tap ((List <:.:> List) := (:*:)) b)
-> (:=) (List <:.:> List) (:*:) b
-> Tap ((List <:.:> List) := (:*:)) b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Product
  (TU Covariant Covariant Maybe (Construction Maybe) b)
  (TU Covariant Covariant Maybe (Construction Maybe) b)
-> (:=) (List <:.:> List) (:*:) b
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 (List (a -> b)
lfs List (a -> b)
-> List a -> TU Covariant Covariant Maybe (Construction Maybe) b
forall (t :: * -> *) a b. Applicative t => t (a -> b) -> t a -> t b
<*> List a
ls TU Covariant Covariant Maybe (Construction Maybe) b
-> TU Covariant Covariant Maybe (Construction Maybe) b
-> Product
     (TU Covariant Covariant Maybe (Construction Maybe) b)
     (TU Covariant Covariant Maybe (Construction Maybe) b)
forall s a. s -> a -> Product s a
:*: List (a -> b)
rfs List (a -> b)
-> List a -> TU Covariant Covariant Maybe (Construction Maybe) b
forall (t :: * -> *) a b. Applicative t => t (a -> b) -> t a -> t b
<*> List a
rs)

instance {-# OVERLAPS #-} Traversable (Tap (List <:.:> List := (:*:))) where
	Tap a
x (T_U (List a
future :*: List a
past)) ->> :: Tap ((List <:.:> List) := (:*:)) a
-> (a -> u b) -> (u :. Tap ((List <:.:> List) := (:*:))) := b
->> a -> u b
f = (\Reverse List b
past' b
x' TU Covariant Covariant Maybe (Construction Maybe) b
future' -> b
-> (:=) (List <:.:> List) (:*:) b
-> Tap ((List <:.:> List) := (:*:)) b
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap b
x' ((:=) (List <:.:> List) (:*:) b
 -> Tap ((List <:.:> List) := (:*:)) b)
-> (:=) (List <:.:> List) (:*:) b
-> Tap ((List <:.:> List) := (:*:)) b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ TU Covariant Covariant Maybe (Construction Maybe) b
-> TU Covariant Covariant Maybe (Construction Maybe) b
-> (:=) (List <:.:> List) (:*:) b
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (TU Covariant Covariant Maybe (Construction Maybe) b
 -> TU Covariant Covariant Maybe (Construction Maybe) b
 -> (:=) (List <:.:> List) (:*:) b)
-> TU Covariant Covariant Maybe (Construction Maybe) b
-> TU Covariant Covariant Maybe (Construction Maybe) b
-> (:=) (List <:.:> List) (:*:) b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# TU Covariant Covariant Maybe (Construction Maybe) b
future' (TU Covariant Covariant Maybe (Construction Maybe) b
 -> (:=) (List <:.:> List) (:*:) b)
-> TU Covariant Covariant Maybe (Construction Maybe) b
-> (:=) (List <:.:> List) (:*:) b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Reverse List b -> Primary (Reverse List) b
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run Reverse List b
past')
		(Reverse List b
 -> b
 -> TU Covariant Covariant Maybe (Construction Maybe) b
 -> Tap ((List <:.:> List) := (:*:)) b)
-> u (Reverse List b)
-> u (b
      -> TU Covariant Covariant Maybe (Construction Maybe) b
      -> Tap ((List <:.:> List) := (:*:)) b)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> List a -> Reverse List a
forall k (t :: k -> *) (a :: k). t a -> Reverse t a
Reverse List a
past Reverse List a -> (a -> u b) -> u (Reverse List b)
forall (t :: * -> *) (u :: * -> *) a b.
(Traversable t, Pointable u, Applicative u) =>
t a -> (a -> u b) -> (u :. t) := b
->> a -> u b
f u (b
   -> TU Covariant Covariant Maybe (Construction Maybe) b
   -> Tap ((List <:.:> List) := (:*:)) b)
-> u b
-> u (TU Covariant Covariant Maybe (Construction Maybe) b
      -> Tap ((List <:.:> List) := (:*:)) b)
forall (t :: * -> *) a b. Applicative t => t (a -> b) -> t a -> t b
<*> a -> u b
f a
x u (TU Covariant Covariant Maybe (Construction Maybe) b
   -> Tap ((List <:.:> List) := (:*:)) b)
-> u (TU Covariant Covariant Maybe (Construction Maybe) b)
-> (u :. Tap ((List <:.:> List) := (:*:))) := b
forall (t :: * -> *) a b. Applicative t => t (a -> b) -> t a -> t b
<*> List a
future List a
-> (a -> u b)
-> u (TU Covariant Covariant Maybe (Construction Maybe) b)
forall (t :: * -> *) (u :: * -> *) a b.
(Traversable t, Pointable u, Applicative u) =>
t a -> (a -> u b) -> (u :. t) := b
->> a -> u b
f

instance {-# OVERLAPS #-} Extendable (Tap (List <:.:> List := (:*:))) where
	Tap ((List <:.:> List) := (:*:)) a
z =>> :: Tap ((List <:.:> List) := (:*:)) a
-> (Tap ((List <:.:> List) := (:*:)) a -> b)
-> Tap ((List <:.:> List) := (:*:)) b
=>> Tap ((List <:.:> List) := (:*:)) a -> b
f = let move :: (Tap ((List <:.:> List) := (:*:)) a
 -> (<:.>) Maybe (Tap ((List <:.:> List) := (:*:))) a)
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Tap ((List <:.:> List) := (:*:)) a)
move Tap ((List <:.:> List) := (:*:)) a
-> (<:.>) Maybe (Tap ((List <:.:> List) := (:*:))) a
rtt = ((Maybe :. Construction Maybe)
 := Tap ((List <:.:> List) := (:*:)) a)
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Tap ((List <:.:> List) := (:*:)) a)
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (((Maybe :. Construction Maybe)
  := Tap ((List <:.:> List) := (:*:)) a)
 -> TU
      Covariant
      Covariant
      Maybe
      (Construction Maybe)
      (Tap ((List <:.:> List) := (:*:)) a))
-> (Construction Maybe (Tap ((List <:.:> List) := (:*:)) a)
    -> (Maybe :. Construction Maybe)
       := Tap ((List <:.:> List) := (:*:)) a)
-> Construction Maybe (Tap ((List <:.:> List) := (:*:)) a)
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Tap ((List <:.:> List) := (:*:)) a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Maybe (Tap ((List <:.:> List) := (:*:)) a)
-> (Maybe :. Construction Maybe)
   := Tap ((List <:.:> List) := (:*:)) a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct (Construction Maybe (Tap ((List <:.:> List) := (:*:)) a)
 -> TU
      Covariant
      Covariant
      Maybe
      (Construction Maybe)
      (Tap ((List <:.:> List) := (:*:)) a))
-> Construction Maybe (Tap ((List <:.:> List) := (:*:)) a)
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Tap ((List <:.:> List) := (:*:)) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ (<:.>) Maybe (Tap ((List <:.:> List) := (:*:))) a
-> Maybe (Tap ((List <:.:> List) := (:*:)) a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run ((<:.>) Maybe (Tap ((List <:.:> List) := (:*:))) a
 -> Maybe (Tap ((List <:.:> List) := (:*:)) a))
-> (Tap ((List <:.:> List) := (:*:)) a
    -> (<:.>) Maybe (Tap ((List <:.:> List) := (:*:))) a)
-> Tap ((List <:.:> List) := (:*:)) a
-> Maybe (Tap ((List <:.:> List) := (:*:)) a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tap ((List <:.:> List) := (:*:)) a
-> (<:.>) Maybe (Tap ((List <:.:> List) := (:*:))) a
rtt (Tap ((List <:.:> List) := (:*:)) a
 -> Maybe (Tap ((List <:.:> List) := (:*:)) a))
-> Tap ((List <:.:> List) := (:*:)) a :=> Construction Maybe
forall (t :: * -> *) a.
Covariant t =>
(a :=> t) -> a :=> Construction t
.-+ Tap ((List <:.:> List) := (:*:)) a
z in
		b
-> (:=) (List <:.:> List) (:*:) b
-> Tap ((List <:.:> List) := (:*:)) b
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (b
 -> (:=) (List <:.:> List) (:*:) b
 -> Tap ((List <:.:> List) := (:*:)) b)
-> b
-> (:=) (List <:.:> List) (:*:) b
-> Tap ((List <:.:> List) := (:*:)) b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Tap ((List <:.:> List) := (:*:)) a -> b
f Tap ((List <:.:> List) := (:*:)) a
z ((:=) (List <:.:> List) (:*:) b
 -> Tap ((List <:.:> List) := (:*:)) b)
-> (:=) (List <:.:> List) (:*:) b
-> Tap ((List <:.:> List) := (:*:)) b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ List b -> List b -> (:=) (List <:.:> List) (:*:) b
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (List b -> List b -> (:=) (List <:.:> List) (:*:) b)
-> List b -> List b -> (:=) (List <:.:> List) (:*:) b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Tap ((List <:.:> List) := (:*:)) a -> b
f (Tap ((List <:.:> List) := (:*:)) a -> b)
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Tap ((List <:.:> List) := (:*:)) a)
-> List b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> (Tap ((List <:.:> List) := (:*:)) a
 -> (<:.>) Maybe (Tap ((List <:.:> List) := (:*:))) a)
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Tap ((List <:.:> List) := (:*:)) a)
move (forall a (mod :: a) (struct :: * -> *).
Morphable ('Rotate mod) struct =>
struct ~> Morphing ('Rotate mod) struct
forall (struct :: * -> *).
Morphable ('Rotate 'Left) struct =>
struct ~> Morphing ('Rotate 'Left) struct
rotate @Left) (List b -> (:=) (List <:.:> List) (:*:) b)
-> List b -> (:=) (List <:.:> List) (:*:) b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Tap ((List <:.:> List) := (:*:)) a -> b
f (Tap ((List <:.:> List) := (:*:)) a -> b)
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Tap ((List <:.:> List) := (:*:)) a)
-> List b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> (Tap ((List <:.:> List) := (:*:)) a
 -> (<:.>) Maybe (Tap ((List <:.:> List) := (:*:))) a)
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Tap ((List <:.:> List) := (:*:)) a)
move (forall a (mod :: a) (struct :: * -> *).
Morphable ('Rotate mod) struct =>
struct ~> Morphing ('Rotate mod) struct
forall (struct :: * -> *).
Morphable ('Rotate 'Right) struct =>
struct ~> Morphing ('Rotate 'Right) struct
rotate @Right)

instance Morphable (Rotate Left) (Tap (List <:.:> List := (:*:))) where
	type Morphing (Rotate Left) (Tap (List <:.:> List := (:*:))) = Maybe <:.> Zipper List
	morphing :: (<:.>)
  (Tagged ('Rotate 'Left)) (Tap ((List <:.:> List) := (:*:))) a
-> Morphing ('Rotate 'Left) (Tap ((List <:.:> List) := (:*:))) a
morphing ((<:.>)
  (Tagged ('Rotate 'Left)) (Tap ((List <:.:> List) := (:*:))) a
-> Tap ((List <:.:> List) := (:*:)) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Tap a
x (T_U (List a
future :*: List a
past))) = ((Maybe :. Tap ((List <:.:> List) := (:*:))) := a)
-> TU
     Covariant Covariant Maybe (Tap ((List <:.:> List) := (:*:))) a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU
		(((Maybe :. Tap ((List <:.:> List) := (:*:))) := a)
 -> TU
      Covariant Covariant Maybe (Tap ((List <:.:> List) := (:*:))) a)
-> ((Maybe :. Tap ((List <:.:> List) := (:*:))) := a)
-> TU
     Covariant Covariant Maybe (Tap ((List <:.:> List) := (:*:))) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a
-> T_U Covariant Covariant (:*:) List List a
-> Tap ((List <:.:> List) := (:*:)) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (a
 -> T_U Covariant Covariant (:*:) List List a
 -> Tap ((List <:.:> List) := (:*:)) a)
-> T_U Covariant Covariant (:*:) List List a
-> a
-> Tap ((List <:.:> List) := (:*:)) a
forall a b c. (a -> b -> c) -> b -> a -> c
% List a -> List a -> T_U Covariant Covariant (:*:) List List a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Lens (List a) (List a) -> List a -> List a
forall src tgt. Lens src tgt -> src -> tgt
view (forall k (f :: k) (t :: * -> *).
(Substructure f t, Covariant t) =>
t :~. Substructural f t
forall (t :: * -> *).
(Substructure 'Tail t, Covariant t) =>
t :~. Substructural 'Tail t
sub @Tail) List a
future) (a :=:=> List
forall k (mod :: k) (struct :: * -> *) a.
Morphed mod struct ((Identity <:.:> struct) := (->)) =>
a :=:=> struct
item @Push a
x List a
past) (a -> Tap ((List <:.:> List) := (:*:)) a)
-> Maybe a -> (Maybe :. Tap ((List <:.:> List) := (:*:))) := a
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> Lens (List a) (Maybe a) -> List a -> Maybe a
forall src tgt. Lens src tgt -> src -> tgt
view (forall k (f :: k) (t :: * -> *).
(Substructure f t, Covariant t) =>
t :~. Substructural f t
forall (t :: * -> *).
(Substructure 'Root t, Covariant t) =>
t :~. Substructural 'Root t
sub @Root) List a
future

instance Morphable (Rotate Right) (Tap (List <:.:> List := (:*:))) where
	type Morphing (Rotate Right) (Tap (List <:.:> List := (:*:))) = Maybe <:.> Zipper List
	morphing :: (<:.>)
  (Tagged ('Rotate 'Right)) (Tap ((List <:.:> List) := (:*:))) a
-> Morphing ('Rotate 'Right) (Tap ((List <:.:> List) := (:*:))) a
morphing ((<:.>)
  (Tagged ('Rotate 'Right)) (Tap ((List <:.:> List) := (:*:))) a
-> Tap ((List <:.:> List) := (:*:)) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Tap a
x (T_U (List a
future :*: List a
past))) = ((Maybe :. Tap ((List <:.:> List) := (:*:))) := a)
-> TU
     Covariant Covariant Maybe (Tap ((List <:.:> List) := (:*:))) a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU
		(((Maybe :. Tap ((List <:.:> List) := (:*:))) := a)
 -> TU
      Covariant Covariant Maybe (Tap ((List <:.:> List) := (:*:))) a)
-> ((Maybe :. Tap ((List <:.:> List) := (:*:))) := a)
-> TU
     Covariant Covariant Maybe (Tap ((List <:.:> List) := (:*:))) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a
-> T_U Covariant Covariant (:*:) List List a
-> Tap ((List <:.:> List) := (:*:)) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (a
 -> T_U Covariant Covariant (:*:) List List a
 -> Tap ((List <:.:> List) := (:*:)) a)
-> T_U Covariant Covariant (:*:) List List a
-> a
-> Tap ((List <:.:> List) := (:*:)) a
forall a b c. (a -> b -> c) -> b -> a -> c
% List a -> List a -> T_U Covariant Covariant (:*:) List List a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (a :=:=> List
forall k (mod :: k) (struct :: * -> *) a.
Morphed mod struct ((Identity <:.:> struct) := (->)) =>
a :=:=> struct
item @Push a
x List a
future) (Lens (List a) (List a) -> List a -> List a
forall src tgt. Lens src tgt -> src -> tgt
view (forall k (f :: k) (t :: * -> *).
(Substructure f t, Covariant t) =>
t :~. Substructural f t
forall (t :: * -> *).
(Substructure 'Tail t, Covariant t) =>
t :~. Substructural 'Tail t
sub @Tail) List a
past) (a -> Tap ((List <:.:> List) := (:*:)) a)
-> Maybe a -> (Maybe :. Tap ((List <:.:> List) := (:*:))) := a
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> Lens (List a) (Maybe a) -> List a -> Maybe a
forall src tgt. Lens src tgt -> src -> tgt
view (forall k (f :: k) (t :: * -> *).
(Substructure f t, Covariant t) =>
t :~. Substructural f t
forall (t :: * -> *).
(Substructure 'Root t, Covariant t) =>
t :~. Substructural 'Root t
sub @Root) List a
past

instance Morphable (Into (Tap (List <:.:> List := (:*:)))) List where
	type Morphing (Into (Tap (List <:.:> List := (:*:)))) List = Maybe <:.> Zipper List
	morphing :: (<:.>) (Tagged ('Into (Tap ((List <:.:> List) := (:*:))))) List a
-> Morphing ('Into (Tap ((List <:.:> List) := (:*:)))) List a
morphing ((<:.>) (Tagged ('Into (Tap ((List <:.:> 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 -> Tap ((List <:.:> List) := (:*:)) a)
-> Maybe (Construction Maybe a)
-> Maybe (Tap ((List <:.:> List) := (:*:)) a)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$>) (Primary List a
 -> Primary
      (TU Covariant Covariant Maybe (Tap ((List <:.:> List) := (:*:))))
      a)
-> List a
-> TU
     Covariant Covariant Maybe (Tap ((List <:.:> List) := (:*:))) a
forall (t :: * -> *) (u :: * -> *) a b.
(Interpreted t, Interpreted u) =>
(Primary t a -> Primary u b) -> t a -> u b
||= List a
list

instance Morphable (Into List) (Tap (List <:.:> List := (:*:))) where
	type Morphing (Into List) (Tap (List <:.:> List := (:*:))) = List
	morphing :: (<:.>) (Tagged ('Into List)) (Tap ((List <:.:> List) := (:*:))) a
-> Morphing ('Into List) (Tap ((List <:.:> List) := (:*:))) a
morphing ((<:.>) (Tagged ('Into List)) (Tap ((List <:.:> List) := (:*:))) a
-> Tap ((List <:.:> List) := (:*:)) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Tap a
x (T_U (List a
future :*: List a
past))) = (List a
 :*: TU Covariant Covariant Maybe (Construction Maybe) (List a))
-> List a
forall a b. (a :*: b) -> a
attached ((List a
  :*: TU Covariant Covariant Maybe (Construction Maybe) (List a))
 -> List a)
-> (List a
    :*: TU 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 (t :: * -> *) a. Interpreted t => t a -> Primary t a
run @(State _)
		# past ->> modify . item @Push @List
		# item @Push x future

instance Morphable (Into (Comprehension Maybe)) (Tap (List <:.:> List := (:*:))) where
	type Morphing (Into (Comprehension Maybe)) (Tap (List <:.:> List := (:*:))) = Comprehension Maybe
	morphing :: (<:.>)
  (Tagged ('Into (Comprehension Maybe)))
  (Tap ((List <:.:> List) := (:*:)))
  a
-> Morphing
     ('Into (Comprehension Maybe)) (Tap ((List <:.:> List) := (:*:))) a
morphing ((<:.>)
  (Tagged ('Into (Comprehension Maybe)))
  (Tap ((List <:.:> List) := (:*:)))
  a
-> Tap ((List <:.:> List) := (:*:)) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Tap a
x (T_U (List a
future :*: List a
past))) = (Comprehension Maybe a
 :*: TU
       Covariant
       Covariant
       Maybe
       (Construction Maybe)
       (Comprehension Maybe a))
-> Comprehension Maybe a
forall a b. (a :*: b) -> a
attached ((Comprehension Maybe a
  :*: TU
        Covariant
        Covariant
        Maybe
        (Construction Maybe)
        (Comprehension Maybe a))
 -> Comprehension Maybe a)
-> (Comprehension Maybe a
    :*: TU
          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 (t :: * -> *) a. Interpreted t => t a -> Primary t a
run @(State _)
		# past ->> modify . item @Push @(Comprehension Maybe)
		# item @Push x (Comprehension future)

instance Substructure Root (Tap (List<:.:> List:= (:*:))) where
	type Substructural Root (Tap (List<:.:> List:= (:*:))) = Identity
	substructure :: Lens
  ((<:.>) (Tagged 'Root) (Tap ((List <:.:> List) := (:*:))) a)
  (Substructural 'Root (Tap ((List <:.:> List) := (:*:))) a)
substructure = ((<:.>) (Tagged 'Root) (Tap ((List <:.:> List) := (:*:))) a
 -> Store
      (Identity a)
      ((<:.>) (Tagged 'Root) (Tap ((List <:.:> List) := (:*:))) a))
-> PQ_
     (->)
     Store
     ((<:.>) (Tagged 'Root) (Tap ((List <:.:> List) := (:*:))) a)
     (Identity a)
forall k k k (p :: k -> k -> *) (q :: k -> k -> k) (a :: k)
       (b :: k).
p a (q b a) -> PQ_ p q a b
PQ_ (((<:.>) (Tagged 'Root) (Tap ((List <:.:> List) := (:*:))) a
  -> Store
       (Identity a)
       ((<:.>) (Tagged 'Root) (Tap ((List <:.:> List) := (:*:))) a))
 -> PQ_
      (->)
      Store
      ((<:.>) (Tagged 'Root) (Tap ((List <:.:> List) := (:*:))) a)
      (Identity a))
-> ((<:.>) (Tagged 'Root) (Tap ((List <:.:> List) := (:*:))) a
    -> Store
         (Identity a)
         ((<:.>) (Tagged 'Root) (Tap ((List <:.:> List) := (:*:))) a))
-> PQ_
     (->)
     Store
     ((<:.>) (Tagged 'Root) (Tap ((List <:.:> List) := (:*:))) a)
     (Identity a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>) (Tagged 'Root) (Tap ((List <:.:> List) := (:*:))) a
zipper -> case (<:.>) (Tagged 'Root) (Tap ((List <:.:> List) := (:*:))) a
-> Tap ((List <:.:> List) := (:*:)) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Lowerable t, Covariant u) =>
t u ~> u
lower (<:.>) (Tagged 'Root) (Tap ((List <:.:> List) := (:*:))) a
zipper of
		Tap a
x (:=) (List <:.:> List) (:*:) a
xs -> (((:*:) (Identity a) :. (->) (Identity a))
 := (<:.>) (Tagged 'Root) (Tap ((List <:.:> List) := (:*:))) a)
-> Store
     (Identity a)
     ((<:.>) (Tagged 'Root) (Tap ((List <:.:> List) := (:*:))) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity a) :. (->) (Identity a))
  := (<:.>) (Tagged 'Root) (Tap ((List <:.:> List) := (:*:))) a)
 -> Store
      (Identity a)
      ((<:.>) (Tagged 'Root) (Tap ((List <:.:> List) := (:*:))) a))
-> (((:*:) (Identity a) :. (->) (Identity a))
    := (<:.>) (Tagged 'Root) (Tap ((List <:.:> List) := (:*:))) a)
-> Store
     (Identity a)
     ((<:.>) (Tagged 'Root) (Tap ((List <:.:> List) := (:*:))) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a -> Identity a
forall a. a -> Identity a
Identity a
x Identity a
-> (Identity a
    -> (<:.>) (Tagged 'Root) (Tap ((List <:.:> List) := (:*:))) a)
-> ((:*:) (Identity a) :. (->) (Identity a))
   := (<:.>) (Tagged 'Root) (Tap ((List <:.:> List) := (:*:))) a
forall s a. s -> a -> Product s a
:*: Tap ((List <:.:> List) := (:*:)) a
-> (<:.>) (Tagged 'Root) (Tap ((List <:.:> List) := (:*:))) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Tap ((List <:.:> List) := (:*:)) a
 -> (<:.>) (Tagged 'Root) (Tap ((List <:.:> List) := (:*:))) a)
-> (Identity a -> Tap ((List <:.:> List) := (:*:)) a)
-> Identity a
-> (<:.>) (Tagged 'Root) (Tap ((List <:.:> List) := (:*:))) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (a
-> (:=) (List <:.:> List) (:*:) a
-> Tap ((List <:.:> List) := (:*:)) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (a
 -> (:=) (List <:.:> List) (:*:) a
 -> Tap ((List <:.:> List) := (:*:)) a)
-> (:=) (List <:.:> List) (:*:) a
-> a
-> Tap ((List <:.:> List) := (:*:)) a
forall a b c. (a -> b -> c) -> b -> a -> c
% (:=) (List <:.:> List) (:*:) a
xs) (a -> Tap ((List <:.:> List) := (:*:)) a)
-> (Identity a -> a)
-> Identity a
-> Tap ((List <:.:> List) := (:*:)) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Identity a -> a
forall (t :: * -> *) a. Extractable t => a <:= t
extract

instance Substructure Left (Tap (List <:.:> List := (:*:))) where
	type Substructural Left (Tap (List <:.:> List := (:*:))) = List
	substructure :: Lens
  ((<:.>) (Tagged 'Left) (Tap ((List <:.:> List) := (:*:))) a)
  (Substructural 'Left (Tap ((List <:.:> List) := (:*:))) a)
substructure = ((<:.>) (Tagged 'Left) (Tap ((List <:.:> List) := (:*:))) a
 -> Store
      (TU Covariant Covariant Maybe (Construction Maybe) a)
      ((<:.>) (Tagged 'Left) (Tap ((List <:.:> List) := (:*:))) a))
-> PQ_
     (->)
     Store
     ((<:.>) (Tagged 'Left) (Tap ((List <:.:> List) := (:*:))) a)
     (TU Covariant Covariant Maybe (Construction Maybe) a)
forall k k k (p :: k -> k -> *) (q :: k -> k -> k) (a :: k)
       (b :: k).
p a (q b a) -> PQ_ p q a b
PQ_ (((<:.>) (Tagged 'Left) (Tap ((List <:.:> List) := (:*:))) a
  -> Store
       (TU Covariant Covariant Maybe (Construction Maybe) a)
       ((<:.>) (Tagged 'Left) (Tap ((List <:.:> List) := (:*:))) a))
 -> PQ_
      (->)
      Store
      ((<:.>) (Tagged 'Left) (Tap ((List <:.:> List) := (:*:))) a)
      (TU Covariant Covariant Maybe (Construction Maybe) a))
-> ((<:.>) (Tagged 'Left) (Tap ((List <:.:> List) := (:*:))) a
    -> Store
         (TU Covariant Covariant Maybe (Construction Maybe) a)
         ((<:.>) (Tagged 'Left) (Tap ((List <:.:> List) := (:*:))) a))
-> PQ_
     (->)
     Store
     ((<:.>) (Tagged 'Left) (Tap ((List <:.:> List) := (:*:))) a)
     (TU Covariant Covariant Maybe (Construction Maybe) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>) (Tagged 'Left) (Tap ((List <:.:> List) := (:*:))) a
zipper -> case (<:.>) (Tagged 'Left) (Tap ((List <:.:> List) := (:*:))) a
-> Tap ((List <:.:> List) := (:*:)) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Lowerable t, Covariant u) =>
t u ~> u
lower (<:.>) (Tagged 'Left) (Tap ((List <:.:> List) := (:*:))) a
zipper of
		Tap a
x (T_U (TU Covariant Covariant Maybe (Construction Maybe) a
future :*: TU Covariant Covariant Maybe (Construction Maybe) a
past)) -> (((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
  :. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
 := (<:.>) (Tagged 'Left) (Tap ((List <:.:> List) := (:*:))) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Maybe) a)
     ((<:.>) (Tagged 'Left) (Tap ((List <:.:> List) := (:*:))) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
   :. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
  := (<:.>) (Tagged 'Left) (Tap ((List <:.:> List) := (:*:))) a)
 -> Store
      (TU Covariant Covariant Maybe (Construction Maybe) a)
      ((<:.>) (Tagged 'Left) (Tap ((List <:.:> List) := (:*:))) a))
-> (((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
     :. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
    := (<:.>) (Tagged 'Left) (Tap ((List <:.:> List) := (:*:))) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Maybe) a)
     ((<:.>) (Tagged 'Left) (Tap ((List <:.:> List) := (:*:))) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ TU Covariant Covariant Maybe (Construction Maybe) a
future TU Covariant Covariant Maybe (Construction Maybe) a
-> (TU Covariant Covariant Maybe (Construction Maybe) a
    -> (<:.>) (Tagged 'Left) (Tap ((List <:.:> List) := (:*:))) a)
-> ((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
    :. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
   := (<:.>) (Tagged 'Left) (Tap ((List <:.:> List) := (:*:))) a
forall s a. s -> a -> Product s a
:*: Tap ((List <:.:> List) := (:*:)) a
-> (<:.>) (Tagged 'Left) (Tap ((List <:.:> List) := (:*:))) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Tap ((List <:.:> List) := (:*:)) a
 -> (<:.>) (Tagged 'Left) (Tap ((List <:.:> List) := (:*:))) a)
-> (TU Covariant Covariant Maybe (Construction Maybe) a
    -> Tap ((List <:.:> List) := (:*:)) a)
-> TU Covariant Covariant Maybe (Construction Maybe) a
-> (<:.>) (Tagged 'Left) (Tap ((List <:.:> List) := (:*:))) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a
-> T_U Covariant Covariant (:*:) List List a
-> Tap ((List <:.:> List) := (:*:)) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap a
x (T_U Covariant Covariant (:*:) List List a
 -> Tap ((List <:.:> List) := (:*:)) a)
-> (TU Covariant Covariant Maybe (Construction Maybe) a
    -> T_U Covariant Covariant (:*:) List List a)
-> TU Covariant Covariant Maybe (Construction Maybe) a
-> Tap ((List <:.:> List) := (:*:)) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Product
  (TU Covariant Covariant Maybe (Construction Maybe) a)
  (TU Covariant Covariant Maybe (Construction Maybe) a)
-> T_U Covariant Covariant (:*:) List 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 (Product
   (TU Covariant Covariant Maybe (Construction Maybe) a)
   (TU Covariant Covariant Maybe (Construction Maybe) a)
 -> T_U Covariant Covariant (:*:) List List a)
-> (TU Covariant Covariant Maybe (Construction Maybe) a
    -> Product
         (TU Covariant Covariant Maybe (Construction Maybe) a)
         (TU Covariant Covariant Maybe (Construction Maybe) a))
-> TU Covariant Covariant Maybe (Construction Maybe) a
-> T_U Covariant Covariant (:*:) List List a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (TU Covariant Covariant Maybe (Construction Maybe) a
-> TU Covariant Covariant Maybe (Construction Maybe) a
-> Product
     (TU Covariant Covariant Maybe (Construction Maybe) a)
     (TU Covariant Covariant Maybe (Construction Maybe) a)
forall s a. s -> a -> Product s a
:*: TU Covariant Covariant Maybe (Construction Maybe) a
past)

instance Substructure Right (Tap (List <:.:> List := (:*:))) where
	type Substructural Right (Tap (List <:.:> List := (:*:))) = List
	substructure :: Lens
  ((<:.>) (Tagged 'Right) (Tap ((List <:.:> List) := (:*:))) a)
  (Substructural 'Right (Tap ((List <:.:> List) := (:*:))) a)
substructure = ((<:.>) (Tagged 'Right) (Tap ((List <:.:> List) := (:*:))) a
 -> Store
      (TU Covariant Covariant Maybe (Construction Maybe) a)
      ((<:.>) (Tagged 'Right) (Tap ((List <:.:> List) := (:*:))) a))
-> PQ_
     (->)
     Store
     ((<:.>) (Tagged 'Right) (Tap ((List <:.:> List) := (:*:))) a)
     (TU Covariant Covariant Maybe (Construction Maybe) a)
forall k k k (p :: k -> k -> *) (q :: k -> k -> k) (a :: k)
       (b :: k).
p a (q b a) -> PQ_ p q a b
PQ_ (((<:.>) (Tagged 'Right) (Tap ((List <:.:> List) := (:*:))) a
  -> Store
       (TU Covariant Covariant Maybe (Construction Maybe) a)
       ((<:.>) (Tagged 'Right) (Tap ((List <:.:> List) := (:*:))) a))
 -> PQ_
      (->)
      Store
      ((<:.>) (Tagged 'Right) (Tap ((List <:.:> List) := (:*:))) a)
      (TU Covariant Covariant Maybe (Construction Maybe) a))
-> ((<:.>) (Tagged 'Right) (Tap ((List <:.:> List) := (:*:))) a
    -> Store
         (TU Covariant Covariant Maybe (Construction Maybe) a)
         ((<:.>) (Tagged 'Right) (Tap ((List <:.:> List) := (:*:))) a))
-> PQ_
     (->)
     Store
     ((<:.>) (Tagged 'Right) (Tap ((List <:.:> List) := (:*:))) a)
     (TU Covariant Covariant Maybe (Construction Maybe) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>) (Tagged 'Right) (Tap ((List <:.:> List) := (:*:))) a
zipper -> case (<:.>) (Tagged 'Right) (Tap ((List <:.:> List) := (:*:))) a
-> Tap ((List <:.:> List) := (:*:)) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Lowerable t, Covariant u) =>
t u ~> u
lower (<:.>) (Tagged 'Right) (Tap ((List <:.:> List) := (:*:))) a
zipper of
		Tap a
x (T_U (TU Covariant Covariant Maybe (Construction Maybe) a
future :*: TU Covariant Covariant Maybe (Construction Maybe) a
past)) -> (((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
  :. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
 := (<:.>) (Tagged 'Right) (Tap ((List <:.:> List) := (:*:))) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Maybe) a)
     ((<:.>) (Tagged 'Right) (Tap ((List <:.:> List) := (:*:))) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
   :. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
  := (<:.>) (Tagged 'Right) (Tap ((List <:.:> List) := (:*:))) a)
 -> Store
      (TU Covariant Covariant Maybe (Construction Maybe) a)
      ((<:.>) (Tagged 'Right) (Tap ((List <:.:> List) := (:*:))) a))
-> (((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
     :. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
    := (<:.>) (Tagged 'Right) (Tap ((List <:.:> List) := (:*:))) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Maybe) a)
     ((<:.>) (Tagged 'Right) (Tap ((List <:.:> List) := (:*:))) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ TU Covariant Covariant Maybe (Construction Maybe) a
past TU Covariant Covariant Maybe (Construction Maybe) a
-> (TU Covariant Covariant Maybe (Construction Maybe) a
    -> (<:.>) (Tagged 'Right) (Tap ((List <:.:> List) := (:*:))) a)
-> ((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
    :. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
   := (<:.>) (Tagged 'Right) (Tap ((List <:.:> List) := (:*:))) a
forall s a. s -> a -> Product s a
:*: Tap ((List <:.:> List) := (:*:)) a
-> (<:.>) (Tagged 'Right) (Tap ((List <:.:> List) := (:*:))) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Tap ((List <:.:> List) := (:*:)) a
 -> (<:.>) (Tagged 'Right) (Tap ((List <:.:> List) := (:*:))) a)
-> (TU Covariant Covariant Maybe (Construction Maybe) a
    -> Tap ((List <:.:> List) := (:*:)) a)
-> TU Covariant Covariant Maybe (Construction Maybe) a
-> (<:.>) (Tagged 'Right) (Tap ((List <:.:> List) := (:*:))) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a
-> T_U Covariant Covariant (:*:) List List a
-> Tap ((List <:.:> List) := (:*:)) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap a
x (T_U Covariant Covariant (:*:) List List a
 -> Tap ((List <:.:> List) := (:*:)) a)
-> (TU Covariant Covariant Maybe (Construction Maybe) a
    -> T_U Covariant Covariant (:*:) List List a)
-> TU Covariant Covariant Maybe (Construction Maybe) a
-> Tap ((List <:.:> List) := (:*:)) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Product
  (TU Covariant Covariant Maybe (Construction Maybe) a)
  (TU Covariant Covariant Maybe (Construction Maybe) a)
-> T_U Covariant Covariant (:*:) List 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 (Product
   (TU Covariant Covariant Maybe (Construction Maybe) a)
   (TU Covariant Covariant Maybe (Construction Maybe) a)
 -> T_U Covariant Covariant (:*:) List List a)
-> (TU Covariant Covariant Maybe (Construction Maybe) a
    -> Product
         (TU Covariant Covariant Maybe (Construction Maybe) a)
         (TU Covariant Covariant Maybe (Construction Maybe) a))
-> TU Covariant Covariant Maybe (Construction Maybe) a
-> T_U Covariant Covariant (:*:) List List a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (TU Covariant Covariant Maybe (Construction Maybe) a
future TU Covariant Covariant Maybe (Construction Maybe) a
-> TU Covariant Covariant Maybe (Construction Maybe) a
-> Product
     (TU Covariant Covariant Maybe (Construction Maybe) a)
     (TU Covariant Covariant Maybe (Construction Maybe) a)
forall s a. s -> a -> Product s a
:*:)

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

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

instance {-# OVERLAPS #-} Applicative (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) where
	Tap a -> b
f (T_U (Construction Maybe (a -> b)
lfs :*: Construction Maybe (a -> b)
rfs)) <*> :: Tap
  ((Construction Maybe <:.:> Construction Maybe) := (:*:)) (a -> b)
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) b
<*> Tap a
x (T_U (Construction Maybe a
ls :*: Construction Maybe a
rs)) = b
-> (:=) (Construction Maybe <:.:> Construction Maybe) (:*:) b
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) b
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (b
 -> (:=) (Construction Maybe <:.:> Construction Maybe) (:*:) b
 -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) b)
-> b
-> (:=) (Construction Maybe <:.:> Construction Maybe) (:*:) b
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# a -> b
f a
x ((:=) (Construction Maybe <:.:> Construction Maybe) (:*:) b
 -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) b)
-> (:=) (Construction Maybe <:.:> Construction Maybe) (:*:) b
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Product (Construction Maybe b) (Construction Maybe b)
-> (:=) (Construction Maybe <:.:> Construction Maybe) (:*:) b
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 (Construction Maybe (a -> b)
lfs Construction Maybe (a -> b)
-> Construction Maybe a -> Construction Maybe b
forall (t :: * -> *) a b. Applicative t => t (a -> b) -> t a -> t b
<*> Construction Maybe a
ls Construction Maybe b
-> Construction Maybe b
-> Product (Construction Maybe b) (Construction Maybe b)
forall s a. s -> a -> Product s a
:*: Construction Maybe (a -> b)
rfs Construction Maybe (a -> b)
-> Construction Maybe a -> Construction Maybe b
forall (t :: * -> *) a b. Applicative t => t (a -> b) -> t a -> t b
<*> Construction Maybe a
rs)

instance {-# OVERLAPS #-} Traversable (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) where
	Tap a
x (T_U (Construction Maybe a
future :*: Construction Maybe a
past)) ->> :: Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
-> (a -> u b)
-> (u
    :. Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
   := b
->> a -> u b
f = (\Reverse (Construction Maybe) b
past' b
x' Construction Maybe b
future' -> b
-> (:=) (Construction Maybe <:.:> Construction Maybe) (:*:) b
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) b
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap b
x' ((:=) (Construction Maybe <:.:> Construction Maybe) (:*:) b
 -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) b)
-> (:=) (Construction Maybe <:.:> Construction Maybe) (:*:) b
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Construction Maybe b
-> Construction Maybe b
-> (:=) (Construction Maybe <:.:> Construction Maybe) (:*:) b
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Construction Maybe b
 -> Construction Maybe b
 -> (:=) (Construction Maybe <:.:> Construction Maybe) (:*:) b)
-> Construction Maybe b
-> Construction Maybe b
-> (:=) (Construction Maybe <:.:> Construction Maybe) (:*:) b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Construction Maybe b
future' (Construction Maybe b
 -> (:=) (Construction Maybe <:.:> Construction Maybe) (:*:) b)
-> Construction Maybe b
-> (:=) (Construction Maybe <:.:> Construction Maybe) (:*:) b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Reverse (Construction Maybe) b
-> Primary (Reverse (Construction Maybe)) b
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run Reverse (Construction Maybe) b
past')
		(Reverse (Construction Maybe) b
 -> b
 -> Construction Maybe b
 -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) b)
-> u (Reverse (Construction Maybe) b)
-> u (b
      -> Construction Maybe b
      -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) b)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> Construction Maybe a -> Reverse (Construction Maybe) a
forall k (t :: k -> *) (a :: k). t a -> Reverse t a
Reverse Construction Maybe a
past Reverse (Construction Maybe) a
-> (a -> u b) -> u (Reverse (Construction Maybe) b)
forall (t :: * -> *) (u :: * -> *) a b.
(Traversable t, Pointable u, Applicative u) =>
t a -> (a -> u b) -> (u :. t) := b
->> a -> u b
f u (b
   -> Construction Maybe b
   -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) b)
-> u b
-> u (Construction Maybe b
      -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) b)
forall (t :: * -> *) a b. Applicative t => t (a -> b) -> t a -> t b
<*> a -> u b
f a
x u (Construction Maybe b
   -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) b)
-> u (Construction Maybe b)
-> (u
    :. Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
   := b
forall (t :: * -> *) a b. Applicative t => t (a -> b) -> t a -> t b
<*> Construction Maybe a
future Construction Maybe a -> (a -> u b) -> u (Construction Maybe b)
forall (t :: * -> *) (u :: * -> *) a b.
(Traversable t, Pointable u, Applicative u) =>
t a -> (a -> u b) -> (u :. t) := b
->> a -> u b
f

instance Morphable (Rotate Left) (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) where
	type Morphing (Rotate Left) (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) = Maybe <:.> Zipper (Construction Maybe)
	morphing :: (<:.>)
  (Tagged ('Rotate 'Left))
  (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  a
-> Morphing
     ('Rotate 'Left)
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
     a
morphing ((<:.>)
  (Tagged ('Rotate 'Left))
  (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  a
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Tap a
x (T_U (Construction Maybe a
future :*: Construction Maybe a
past))) = ((Maybe
  :. Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
 := a)
-> TU
     Covariant
     Covariant
     Maybe
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
     a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (((Maybe
   :. Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  := a)
 -> TU
      Covariant
      Covariant
      Maybe
      (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
      a)
-> ((Maybe
     :. Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
    := a)
-> TU
     Covariant
     Covariant
     Maybe
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Construction Maybe)
     (Construction Maybe)
     a
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (a <:= Construction Maybe
forall (t :: * -> *) a. Extractable t => a <:= t
extract Construction Maybe a
future) (T_U
   Covariant
   Covariant
   (:*:)
   (Construction Maybe)
   (Construction Maybe)
   a
 -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a)
-> (Construction Maybe a
    -> T_U
         Covariant
         Covariant
         (:*:)
         (Construction Maybe)
         (Construction Maybe)
         a)
-> Construction Maybe a
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Maybe a
-> Construction Maybe a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Construction Maybe)
     (Construction Maybe)
     a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Construction Maybe a
 -> Construction Maybe a
 -> T_U
      Covariant
      Covariant
      (:*:)
      (Construction Maybe)
      (Construction Maybe)
      a)
-> Construction Maybe a
-> Construction Maybe a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Construction Maybe)
     (Construction Maybe)
     a
forall a b c. (a -> b -> c) -> b -> a -> c
% a :=:=> Construction Maybe
forall k (mod :: k) (struct :: * -> *) a.
Morphed mod struct ((Identity <:.:> struct) := (->)) =>
a :=:=> struct
item @Push a
x Construction Maybe a
past (Construction Maybe a
 -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a)
-> Maybe (Construction Maybe a)
-> (Maybe
    :. Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
   := a
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> Construction Maybe a -> Maybe (Construction Maybe a)
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct Construction Maybe a
future

instance Morphable (Rotate Right) (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) where
	type Morphing (Rotate Right) (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) = Maybe <:.> Zipper (Construction Maybe)
	morphing :: (<:.>)
  (Tagged ('Rotate 'Right))
  (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  a
-> Morphing
     ('Rotate 'Right)
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
     a
morphing ((<:.>)
  (Tagged ('Rotate 'Right))
  (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  a
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Tap a
x (T_U (Construction Maybe a
future :*: Construction Maybe a
past))) = ((Maybe
  :. Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
 := a)
-> TU
     Covariant
     Covariant
     Maybe
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
     a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (((Maybe
   :. Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  := a)
 -> TU
      Covariant
      Covariant
      Maybe
      (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
      a)
-> ((Maybe
     :. Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
    := a)
-> TU
     Covariant
     Covariant
     Maybe
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Construction Maybe)
     (Construction Maybe)
     a
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (a <:= Construction Maybe
forall (t :: * -> *) a. Extractable t => a <:= t
extract Construction Maybe a
past) (T_U
   Covariant
   Covariant
   (:*:)
   (Construction Maybe)
   (Construction Maybe)
   a
 -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a)
-> (Construction Maybe a
    -> T_U
         Covariant
         Covariant
         (:*:)
         (Construction Maybe)
         (Construction Maybe)
         a)
-> Construction Maybe a
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Maybe a
-> Construction Maybe a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Construction Maybe)
     (Construction Maybe)
     a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (a :=:=> Construction Maybe
forall k (mod :: k) (struct :: * -> *) a.
Morphed mod struct ((Identity <:.:> struct) := (->)) =>
a :=:=> struct
item @Push a
x Construction Maybe a
future) (Construction Maybe a
 -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a)
-> Maybe (Construction Maybe a)
-> (Maybe
    :. Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
   := a
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> Construction Maybe a -> Maybe (Construction Maybe a)
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct Construction Maybe a
past

instance Morphable (Into (Tap (List <:.:> List := (:*:)))) (Construction Maybe) where
	type Morphing (Into (Tap (List <:.:> List := (:*:)))) (Construction Maybe) = Zipper List
	morphing :: (<:.>)
  (Tagged ('Into (Tap ((List <:.:> List) := (:*:)))))
  (Construction Maybe)
  a
-> Morphing
     ('Into (Tap ((List <:.:> List) := (:*:)))) (Construction Maybe) a
morphing ((<:.>)
  (Tagged ('Into (Tap ((List <:.:> List) := (:*:)))))
  (Construction Maybe)
  a
-> Construction Maybe a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construction Maybe a
ne) = a
-> T_U Covariant Covariant (:*:) List List a
-> Tap ((List <:.:> List) := (:*:)) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (a
 -> T_U Covariant Covariant (:*:) List List a
 -> Tap ((List <:.:> List) := (:*:)) a)
-> a
-> T_U Covariant Covariant (:*:) List List a
-> Tap ((List <:.:> List) := (:*:)) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# a <:= Construction Maybe
forall (t :: * -> *) a. Extractable t => a <:= t
extract Construction Maybe a
ne (T_U Covariant Covariant (:*:) List List a
 -> Tap ((List <:.:> List) := (:*:)) a)
-> T_U Covariant Covariant (:*:) List List a
-> Tap ((List <:.:> List) := (:*:)) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ List a -> List a -> T_U Covariant Covariant (:*:) List List a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (List a -> List a -> T_U Covariant Covariant (:*:) List List a)
-> List a -> List a -> T_U Covariant Covariant (:*:) List List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Lens (Construction Maybe a) (List a)
-> Construction Maybe a -> List a
forall src tgt. Lens src tgt -> src -> tgt
view (forall k (f :: k) (t :: * -> *).
(Substructure f t, Covariant t) =>
t :~. Substructural f t
forall (t :: * -> *).
(Substructure 'Tail t, Covariant t) =>
t :~. Substructural 'Tail t
sub @Tail) Construction Maybe a
ne (List a -> T_U Covariant Covariant (:*:) List List a)
-> List a -> T_U Covariant Covariant (:*:) List List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# List a
forall (t :: * -> *) a. Avoidable t => t a
empty

instance Morphable (Into (Tap (List <:.:> List := (:*:)))) (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) where
	type Morphing (Into (Tap (List <:.:> List := (:*:)))) (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) = Zipper List
	morphing :: (<:.>)
  (Tagged ('Into (Tap ((List <:.:> List) := (:*:)))))
  (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  a
-> Morphing
     ('Into (Tap ((List <:.:> List) := (:*:))))
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
     a
morphing ((<:.>)
  (Tagged ('Into (Tap ((List <:.:> List) := (:*:)))))
  (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  a
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
zipper) = a
-> (:=) (List <:.:> List) (:*:) a
-> Tap ((List <:.:> List) := (:*:)) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (a
 -> (:=) (List <:.:> List) (:*:) a
 -> Tap ((List <:.:> List) := (:*:)) a)
-> a
-> (:=) (List <:.:> List) (:*:) a
-> Tap ((List <:.:> List) := (:*:)) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# a <:= Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:))
forall (t :: * -> *) a. Extractable t => a <:= t
extract Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
zipper ((:=) (List <:.:> List) (:*:) a
 -> Tap ((List <:.:> List) := (:*:)) a)
-> (:=) (List <:.:> List) (:*:) a
-> Tap ((List <:.:> List) := (:*:)) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Construction Maybe a
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Maybe a
 -> TU Covariant Covariant Maybe (Construction Maybe) a)
-> (Construction Maybe a
    -> TU Covariant Covariant Maybe (Construction Maybe) a)
-> Product (Construction Maybe a) (Construction Maybe a)
-> Product
     (TU Covariant Covariant Maybe (Construction Maybe) a)
     (TU Covariant Covariant Maybe (Construction Maybe) a)
forall (v :: * -> * -> *) a b c d.
(Bivariant v, forall i. Covariant (v i)) =>
(a -> b) -> (c -> d) -> v a c -> v b d
<-> Construction Maybe a
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Primary ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
 -> Primary ((List <:.:> List) := (:*:)) a)
-> (:=) (Construction Maybe <:.:> Construction Maybe) (:*:) a
-> (:=) (List <:.:> List) (:*:) a
forall (t :: * -> *) (u :: * -> *) a b.
(Interpreted t, Interpreted u) =>
(Primary t a -> Primary u b) -> t a -> u b
||= Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
-> (:=) (Construction Maybe <:.:> Construction Maybe) (:*:) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Lowerable t, Covariant u) =>
t u ~> u
lower Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
zipper

instance Morphable (Into (Tap (Construction Maybe <:.:> Construction Maybe := (:*:)))) (Tap (List <:.:> List := (:*:))) where
	type Morphing (Into (Tap (Construction Maybe <:.:> Construction Maybe := (:*:)))) (Tap (List <:.:> List := (:*:))) = Maybe <:.> Zipper (Construction Maybe)
	morphing :: (<:.>)
  (Tagged
     ('Into
        (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))))
  (Tap ((List <:.:> List) := (:*:)))
  a
-> Morphing
     ('Into
        (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:))))
     (Tap ((List <:.:> List) := (:*:)))
     a
morphing ((<:.>)
  (Tagged
     ('Into
        (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))))
  (Tap ((List <:.:> List) := (:*:)))
  a
-> Tap ((List <:.:> List) := (:*:)) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Tap ((List <:.:> List) := (:*:)) a
zipper) = let spread :: t s -> t a -> t (Product s a)
spread t s
x t a
y = s -> a -> Product s a
forall s a. s -> a -> Product s a
(:*:) (s -> a -> Product s a) -> t s -> t (a -> Product s a)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> t s
x t (a -> Product s a) -> t a -> t (Product s a)
forall (t :: * -> *) a b. Applicative t => t (a -> b) -> t a -> t b
<*> t a
y in ((Maybe
  :. Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
 := a)
-> TU
     Covariant
     Covariant
     Maybe
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
     a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (((Maybe
   :. Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  := a)
 -> TU
      Covariant
      Covariant
      Maybe
      (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
      a)
-> ((Maybe
     :. Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
    := a)
-> TU
     Covariant
     Covariant
     Maybe
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$
		a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Construction Maybe)
     (Construction Maybe)
     a
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (a <:= Tap ((List <:.:> List) := (:*:))
forall (t :: * -> *) a. Extractable t => a <:= t
extract Tap ((List <:.:> List) := (:*:)) a
zipper) (T_U
   Covariant
   Covariant
   (:*:)
   (Construction Maybe)
   (Construction Maybe)
   a
 -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a)
-> (Product (Construction Maybe a) (Construction Maybe a)
    -> T_U
         Covariant
         Covariant
         (:*:)
         (Construction Maybe)
         (Construction Maybe)
         a)
-> Product (Construction Maybe a) (Construction Maybe a)
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Product (Construction Maybe a) (Construction Maybe a)
-> T_U
     Covariant
     Covariant
     (:*:)
     (Construction Maybe)
     (Construction Maybe)
     a
forall k k k k k (ct :: k) (cu :: k) (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 (Product (Construction Maybe a) (Construction Maybe a)
 -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a)
-> Maybe (Product (Construction Maybe a) (Construction Maybe a))
-> (Maybe
    :. Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
   := a
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> ((Product
  ((Maybe :. Construction Maybe) := a)
  ((Maybe :. Construction Maybe) := a)
-> (((Maybe :. Construction Maybe) := a)
    -> ((Maybe :. Construction Maybe) := a)
    -> Maybe (Product (Construction Maybe a) (Construction Maybe a)))
-> Maybe (Product (Construction Maybe a) (Construction Maybe a))
forall (t :: * -> *) (u :: * -> *) a b.
Adjoint t u =>
t a -> (a -> u b) -> b
|- ((Maybe :. Construction Maybe) := a)
-> ((Maybe :. Construction Maybe) := a)
-> Maybe (Product (Construction Maybe a) (Construction Maybe a))
forall (t :: * -> *) s a.
Applicative t =>
t s -> t a -> t (Product s a)
spread) (Product
   ((Maybe :. Construction Maybe) := a)
   ((Maybe :. Construction Maybe) := a)
 -> Maybe (Product (Construction Maybe a) (Construction Maybe a)))
-> ((:=) (List <:.:> List) (:*:) a
    -> Product
         ((Maybe :. Construction Maybe) := a)
         ((Maybe :. Construction Maybe) := a))
-> (:=) (List <:.:> List) (:*:) a
-> Maybe (Product (Construction Maybe a) (Construction Maybe a))
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (TU Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (TU Covariant Covariant Maybe (Construction Maybe) a
 -> (Maybe :. Construction Maybe) := a)
-> (TU Covariant Covariant Maybe (Construction Maybe) a
    -> (Maybe :. Construction Maybe) := a)
-> Product
     (TU Covariant Covariant Maybe (Construction Maybe) a)
     (TU Covariant Covariant Maybe (Construction Maybe) a)
-> Product
     ((Maybe :. Construction Maybe) := a)
     ((Maybe :. Construction Maybe) := a)
forall (v :: * -> * -> *) a b c d.
(Bivariant v, forall i. Covariant (v i)) =>
(a -> b) -> (c -> d) -> v a c -> v b d
<-> TU Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run) (Product
   (TU Covariant Covariant Maybe (Construction Maybe) a)
   (TU Covariant Covariant Maybe (Construction Maybe) a)
 -> Product
      ((Maybe :. Construction Maybe) := a)
      ((Maybe :. Construction Maybe) := a))
-> ((:=) (List <:.:> List) (:*:) a
    -> Product
         (TU Covariant Covariant Maybe (Construction Maybe) a)
         (TU Covariant Covariant Maybe (Construction Maybe) a))
-> (:=) (List <:.:> List) (:*:) a
-> Product
     ((Maybe :. Construction Maybe) := a)
     ((Maybe :. Construction Maybe) := a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (:=) (List <:.:> List) (:*:) a
-> Product
     (TU Covariant Covariant Maybe (Construction Maybe) a)
     (TU Covariant Covariant Maybe (Construction Maybe) a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run ((:=) (List <:.:> List) (:*:) a
 -> Maybe (Product (Construction Maybe a) (Construction Maybe a)))
-> (:=) (List <:.:> List) (:*:) a
-> Maybe (Product (Construction Maybe a) (Construction Maybe a))
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Tap ((List <:.:> List) := (:*:)) a
-> (:=) (List <:.:> List) (:*:) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Lowerable t, Covariant u) =>
t u ~> u
lower Tap ((List <:.:> List) := (:*:)) a
zipper)

instance Morphable (Into (Construction Maybe)) (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) where
	type Morphing (Into (Construction Maybe)) (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) = Construction Maybe
	morphing :: (<:.>)
  (Tagged ('Into (Construction Maybe)))
  (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  a
-> Morphing
     ('Into (Construction Maybe))
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
     a
morphing ((<:.>)
  (Tagged ('Into (Construction Maybe)))
  (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  a
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Tap a
x (T_U (Construction Maybe a
future :*: Construction Maybe a
past))) = (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 (t :: * -> *) a. Interpreted t => t a -> Primary t a
run @(State _)
		# past ->> modify . item @Push @(Nonempty List)
		# item @Push x future

instance Morphable (Into List) (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) where
	type Morphing (Into List) (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) = List
	morphing :: (<:.>)
  (Tagged ('Into List))
  (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  a
-> Morphing
     ('Into List)
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
     a
morphing ((<:.>)
  (Tagged ('Into List))
  (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  a
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Tap a
x (T_U (Construction Maybe a
future :*: Construction Maybe a
past))) = (TU Covariant Covariant Maybe (Construction Maybe) a
 :*: Construction
       Maybe (TU Covariant Covariant Maybe (Construction Maybe) a))
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall a b. (a :*: b) -> a
attached ((TU Covariant Covariant Maybe (Construction Maybe) a
  :*: Construction
        Maybe (TU Covariant Covariant Maybe (Construction Maybe) a))
 -> TU Covariant Covariant Maybe (Construction Maybe) a)
-> (TU Covariant Covariant Maybe (Construction Maybe) a
    :*: Construction
          Maybe (TU Covariant Covariant Maybe (Construction Maybe) a))
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ forall a.
Interpreted
  (State (TU Covariant Covariant Maybe (Construction Maybe) a)) =>
State (TU Covariant Covariant Maybe (Construction Maybe) a) a
-> Primary
     (State (TU Covariant Covariant Maybe (Construction Maybe) a)) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run @(State _)
		# past ->> modify . item @Push @List
		# item @Push x (lift future)

instance Substructure Root (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) where
	type Substructural Root (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) = Identity
	substructure :: Lens
  ((<:.>)
     (Tagged 'Root)
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
     a)
  (Substructural
     'Root
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
     a)
substructure = ((<:.>)
   (Tagged 'Root)
   (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
   a
 -> Store
      (Identity a)
      ((<:.>)
         (Tagged 'Root)
         (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
         a))
-> PQ_
     (->)
     Store
     ((<:.>)
        (Tagged 'Root)
        (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
        a)
     (Identity a)
forall k k k (p :: k -> k -> *) (q :: k -> k -> k) (a :: k)
       (b :: k).
p a (q b a) -> PQ_ p q a b
PQ_ (((<:.>)
    (Tagged 'Root)
    (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
    a
  -> Store
       (Identity a)
       ((<:.>)
          (Tagged 'Root)
          (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
          a))
 -> PQ_
      (->)
      Store
      ((<:.>)
         (Tagged 'Root)
         (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
         a)
      (Identity a))
-> ((<:.>)
      (Tagged 'Root)
      (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
      a
    -> Store
         (Identity a)
         ((<:.>)
            (Tagged 'Root)
            (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
            a))
-> PQ_
     (->)
     Store
     ((<:.>)
        (Tagged 'Root)
        (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
        a)
     (Identity a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>)
  (Tagged 'Root)
  (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  a
zipper -> case (<:.>)
  (Tagged 'Root)
  (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  a
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Lowerable t, Covariant u) =>
t u ~> u
lower (<:.>)
  (Tagged 'Root)
  (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  a
zipper of
		Tap a
x (:=) (Construction Maybe <:.:> Construction Maybe) (:*:) a
xs -> (((:*:) (Identity a) :. (->) (Identity a))
 := (<:.>)
      (Tagged 'Root)
      (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
      a)
-> Store
     (Identity a)
     ((<:.>)
        (Tagged 'Root)
        (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
        a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity a) :. (->) (Identity a))
  := (<:.>)
       (Tagged 'Root)
       (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
       a)
 -> Store
      (Identity a)
      ((<:.>)
         (Tagged 'Root)
         (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
         a))
-> (((:*:) (Identity a) :. (->) (Identity a))
    := (<:.>)
         (Tagged 'Root)
         (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
         a)
-> Store
     (Identity a)
     ((<:.>)
        (Tagged 'Root)
        (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
        a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a -> Identity a
forall a. a -> Identity a
Identity a
x Identity a
-> (Identity a
    -> (<:.>)
         (Tagged 'Root)
         (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
         a)
-> ((:*:) (Identity a) :. (->) (Identity a))
   := (<:.>)
        (Tagged 'Root)
        (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
        a
forall s a. s -> a -> Product s a
:*: Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
-> (<:.>)
     (Tagged 'Root)
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
     a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
 -> (<:.>)
      (Tagged 'Root)
      (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
      a)
-> (Identity a
    -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a)
-> Identity a
-> (<:.>)
     (Tagged 'Root)
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (a
-> (:=) (Construction Maybe <:.:> Construction Maybe) (:*:) a
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (a
 -> (:=) (Construction Maybe <:.:> Construction Maybe) (:*:) a
 -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a)
-> (:=) (Construction Maybe <:.:> Construction Maybe) (:*:) a
-> a
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
forall a b c. (a -> b -> c) -> b -> a -> c
% (:=) (Construction Maybe <:.:> Construction Maybe) (:*:) a
xs) (a
 -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a)
-> (Identity a -> a)
-> Identity a
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Identity a -> a
forall (t :: * -> *) a. Extractable t => a <:= t
extract

instance Substructure Left (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) where
	type Substructural Left (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) = Construction Maybe
	substructure :: Lens
  ((<:.>)
     (Tagged 'Left)
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
     a)
  (Substructural
     'Left
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
     a)
substructure = ((<:.>)
   (Tagged 'Left)
   (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
   a
 -> Store
      (Construction Maybe a)
      ((<:.>)
         (Tagged 'Left)
         (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
         a))
-> PQ_
     (->)
     Store
     ((<:.>)
        (Tagged 'Left)
        (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
        a)
     (Construction Maybe a)
forall k k k (p :: k -> k -> *) (q :: k -> k -> k) (a :: k)
       (b :: k).
p a (q b a) -> PQ_ p q a b
PQ_ (((<:.>)
    (Tagged 'Left)
    (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
    a
  -> Store
       (Construction Maybe a)
       ((<:.>)
          (Tagged 'Left)
          (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
          a))
 -> PQ_
      (->)
      Store
      ((<:.>)
         (Tagged 'Left)
         (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
         a)
      (Construction Maybe a))
-> ((<:.>)
      (Tagged 'Left)
      (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
      a
    -> Store
         (Construction Maybe a)
         ((<:.>)
            (Tagged 'Left)
            (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
            a))
-> PQ_
     (->)
     Store
     ((<:.>)
        (Tagged 'Left)
        (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
        a)
     (Construction Maybe a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>)
  (Tagged 'Left)
  (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  a
zipper -> case (<:.>)
  (Tagged 'Left)
  (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  a
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Lowerable t, Covariant u) =>
t u ~> u
lower (<:.>)
  (Tagged 'Left)
  (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  a
zipper of
		Tap a
x (T_U (Construction Maybe a
future :*: Construction Maybe a
past)) -> (((:*:) (Construction Maybe a) :. (->) (Construction Maybe a))
 := (<:.>)
      (Tagged 'Left)
      (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
      a)
-> Store
     (Construction Maybe a)
     ((<:.>)
        (Tagged 'Left)
        (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
        a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Construction Maybe a) :. (->) (Construction Maybe a))
  := (<:.>)
       (Tagged 'Left)
       (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
       a)
 -> Store
      (Construction Maybe a)
      ((<:.>)
         (Tagged 'Left)
         (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
         a))
-> (((:*:) (Construction Maybe a) :. (->) (Construction Maybe a))
    := (<:.>)
         (Tagged 'Left)
         (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
         a)
-> Store
     (Construction Maybe a)
     ((<:.>)
        (Tagged 'Left)
        (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
        a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Construction Maybe a
future Construction Maybe a
-> (Construction Maybe a
    -> (<:.>)
         (Tagged 'Left)
         (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
         a)
-> ((:*:) (Construction Maybe a) :. (->) (Construction Maybe a))
   := (<:.>)
        (Tagged 'Left)
        (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
        a
forall s a. s -> a -> Product s a
:*: Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
-> (<:.>)
     (Tagged 'Left)
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
     a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
 -> (<:.>)
      (Tagged 'Left)
      (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
      a)
-> (Construction Maybe a
    -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a)
-> Construction Maybe a
-> (<:.>)
     (Tagged 'Left)
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Construction Maybe)
     (Construction Maybe)
     a
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap a
x (T_U
   Covariant
   Covariant
   (:*:)
   (Construction Maybe)
   (Construction Maybe)
   a
 -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a)
-> (Construction Maybe a
    -> T_U
         Covariant
         Covariant
         (:*:)
         (Construction Maybe)
         (Construction Maybe)
         a)
-> Construction Maybe a
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Product (Construction Maybe a) (Construction Maybe a)
-> T_U
     Covariant
     Covariant
     (:*:)
     (Construction Maybe)
     (Construction Maybe)
     a
forall k k k k k (ct :: k) (cu :: k) (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 (Product (Construction Maybe a) (Construction Maybe a)
 -> T_U
      Covariant
      Covariant
      (:*:)
      (Construction Maybe)
      (Construction Maybe)
      a)
-> (Construction Maybe a
    -> Product (Construction Maybe a) (Construction Maybe a))
-> Construction Maybe a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Construction Maybe)
     (Construction Maybe)
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (Construction Maybe a
-> Construction Maybe a
-> Product (Construction Maybe a) (Construction Maybe a)
forall s a. s -> a -> Product s a
:*: Construction Maybe a
past)

instance Substructure Right (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) where
	type Substructural Right (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) = Construction Maybe
	substructure :: Lens
  ((<:.>)
     (Tagged 'Right)
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
     a)
  (Substructural
     'Right
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
     a)
substructure = ((<:.>)
   (Tagged 'Right)
   (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
   a
 -> Store
      (Construction Maybe a)
      ((<:.>)
         (Tagged 'Right)
         (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
         a))
-> PQ_
     (->)
     Store
     ((<:.>)
        (Tagged 'Right)
        (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
        a)
     (Construction Maybe a)
forall k k k (p :: k -> k -> *) (q :: k -> k -> k) (a :: k)
       (b :: k).
p a (q b a) -> PQ_ p q a b
PQ_ (((<:.>)
    (Tagged 'Right)
    (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
    a
  -> Store
       (Construction Maybe a)
       ((<:.>)
          (Tagged 'Right)
          (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
          a))
 -> PQ_
      (->)
      Store
      ((<:.>)
         (Tagged 'Right)
         (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
         a)
      (Construction Maybe a))
-> ((<:.>)
      (Tagged 'Right)
      (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
      a
    -> Store
         (Construction Maybe a)
         ((<:.>)
            (Tagged 'Right)
            (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
            a))
-> PQ_
     (->)
     Store
     ((<:.>)
        (Tagged 'Right)
        (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
        a)
     (Construction Maybe a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>)
  (Tagged 'Right)
  (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  a
zipper -> case (<:.>)
  (Tagged 'Right)
  (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  a
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Lowerable t, Covariant u) =>
t u ~> u
lower (<:.>)
  (Tagged 'Right)
  (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  a
zipper of
		Tap a
x (T_U (Construction Maybe a
future :*: Construction Maybe a
past)) -> (((:*:) (Construction Maybe a) :. (->) (Construction Maybe a))
 := (<:.>)
      (Tagged 'Right)
      (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
      a)
-> Store
     (Construction Maybe a)
     ((<:.>)
        (Tagged 'Right)
        (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
        a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Construction Maybe a) :. (->) (Construction Maybe a))
  := (<:.>)
       (Tagged 'Right)
       (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
       a)
 -> Store
      (Construction Maybe a)
      ((<:.>)
         (Tagged 'Right)
         (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
         a))
-> (((:*:) (Construction Maybe a) :. (->) (Construction Maybe a))
    := (<:.>)
         (Tagged 'Right)
         (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
         a)
-> Store
     (Construction Maybe a)
     ((<:.>)
        (Tagged 'Right)
        (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
        a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Construction Maybe a
past Construction Maybe a
-> (Construction Maybe a
    -> (<:.>)
         (Tagged 'Right)
         (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
         a)
-> ((:*:) (Construction Maybe a) :. (->) (Construction Maybe a))
   := (<:.>)
        (Tagged 'Right)
        (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
        a
forall s a. s -> a -> Product s a
:*: Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
-> (<:.>)
     (Tagged 'Right)
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
     a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
 -> (<:.>)
      (Tagged 'Right)
      (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
      a)
-> (Construction Maybe a
    -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a)
-> Construction Maybe a
-> (<:.>)
     (Tagged 'Right)
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Construction Maybe)
     (Construction Maybe)
     a
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap a
x (T_U
   Covariant
   Covariant
   (:*:)
   (Construction Maybe)
   (Construction Maybe)
   a
 -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a)
-> (Construction Maybe a
    -> T_U
         Covariant
         Covariant
         (:*:)
         (Construction Maybe)
         (Construction Maybe)
         a)
-> Construction Maybe a
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Product (Construction Maybe a) (Construction Maybe a)
-> T_U
     Covariant
     Covariant
     (:*:)
     (Construction Maybe)
     (Construction Maybe)
     a
forall k k k k k (ct :: k) (cu :: k) (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 (Product (Construction Maybe a) (Construction Maybe a)
 -> T_U
      Covariant
      Covariant
      (:*:)
      (Construction Maybe)
      (Construction Maybe)
      a)
-> (Construction Maybe a
    -> Product (Construction Maybe a) (Construction Maybe a))
-> Construction Maybe a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Construction Maybe)
     (Construction Maybe)
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (Construction Maybe a
future Construction Maybe a
-> Construction Maybe a
-> Product (Construction Maybe a) (Construction Maybe a)
forall s a. s -> a -> Product s a
:*:)

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

type instance Zipper (Comprehension Maybe) = Tap (Comprehension Maybe <:.:> Comprehension Maybe := (:*:))

instance {-# OVERLAPS #-} Applicative (Tap (Comprehension Maybe <:.:> Comprehension Maybe := (:*:))) where
	Tap a -> b
f (T_U (Comprehension Maybe (a -> b)
lfs :*: Comprehension Maybe (a -> b)
rfs)) <*> :: Tap
  ((Comprehension Maybe <:.:> Comprehension Maybe) := (:*:)) (a -> b)
-> Tap ((Comprehension Maybe <:.:> Comprehension Maybe) := (:*:)) a
-> Tap ((Comprehension Maybe <:.:> Comprehension Maybe) := (:*:)) b
<*> Tap a
x (T_U (Comprehension Maybe a
ls :*: Comprehension Maybe a
rs)) = b
-> (:=) (Comprehension Maybe <:.:> Comprehension Maybe) (:*:) b
-> Tap ((Comprehension Maybe <:.:> Comprehension Maybe) := (:*:)) b
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (b
 -> (:=) (Comprehension Maybe <:.:> Comprehension Maybe) (:*:) b
 -> Tap
      ((Comprehension Maybe <:.:> Comprehension Maybe) := (:*:)) b)
-> b
-> (:=) (Comprehension Maybe <:.:> Comprehension Maybe) (:*:) b
-> Tap ((Comprehension Maybe <:.:> Comprehension Maybe) := (:*:)) b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# a -> b
f a
x ((:=) (Comprehension Maybe <:.:> Comprehension Maybe) (:*:) b
 -> Tap
      ((Comprehension Maybe <:.:> Comprehension Maybe) := (:*:)) b)
-> (:=) (Comprehension Maybe <:.:> Comprehension Maybe) (:*:) b
-> Tap ((Comprehension Maybe <:.:> Comprehension Maybe) := (:*:)) b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Product (Comprehension Maybe b) (Comprehension Maybe b)
-> (:=) (Comprehension Maybe <:.:> Comprehension Maybe) (:*:) b
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 (Comprehension Maybe (a -> b)
lfs Comprehension Maybe (a -> b)
-> Comprehension Maybe a -> Comprehension Maybe b
forall (t :: * -> *) a b. Applicative t => t (a -> b) -> t a -> t b
<*> Comprehension Maybe a
ls Comprehension Maybe b
-> Comprehension Maybe b
-> Product (Comprehension Maybe b) (Comprehension Maybe b)
forall s a. s -> a -> Product s a
:*: Comprehension Maybe (a -> b)
rfs Comprehension Maybe (a -> b)
-> Comprehension Maybe a -> Comprehension Maybe b
forall (t :: * -> *) a b. Applicative t => t (a -> b) -> t a -> t b
<*> Comprehension Maybe a
rs)

----------------------------------------- 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
-> TU
     Covariant Covariant Maybe (Construction Maybe) (Product key a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Prefixed List key a
 -> TU
      Covariant Covariant Maybe (Construction Maybe) (Product key a))
-> ((<:.>) (Tagged ('Lookup 'Key)) (Prefixed List key) a
    -> Prefixed List key a)
-> (<:.>) (Tagged ('Lookup 'Key)) (Prefixed List key) a
-> TU
     Covariant Covariant Maybe (Construction Maybe) (Product key a)
forall (m :: * -> * -> *) b c a.
Category 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 -> TU Covariant Covariant Maybe (Construction Maybe) (Product key a)
list) = (((->) key :. Maybe) := a)
-> TU Covariant Covariant ((->) key) Maybe a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU ((((->) key :. Maybe) := a)
 -> TU Covariant Covariant ((->) key) Maybe a)
-> (((->) key :. Maybe) := a)
-> TU Covariant Covariant ((->) key) Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \key
key -> ((Construction Maybe :. Product key) := a)
-> Prefixed (Construction Maybe) key a
forall (t :: * -> *) k a. ((t :. Product k) := a) -> Prefixed t k a
Prefixed (((Construction Maybe :. Product key) := a)
 -> Prefixed (Construction Maybe) key a)
-> Maybe ((Construction Maybe :. Product key) := a)
-> Maybe (Prefixed (Construction Maybe) key a)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> TU Covariant Covariant Maybe (Construction Maybe) (Product key a)
-> Primary List (Product key a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run TU Covariant Covariant Maybe (Construction Maybe) (Product key a)
list Maybe (Prefixed (Construction Maybe) key a)
-> (Prefixed (Construction Maybe) key a -> Maybe a) -> Maybe a
forall (t :: * -> *) a b. Bindable t => t a -> (a -> t b) -> t b
>>= 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 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 (t :: * -> *) a. Interpreted t => 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.
Category 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)
-> TU Covariant Covariant ((->) key) Maybe a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU ((((->) key :. Maybe) := a)
 -> TU Covariant Covariant ((->) key) Maybe a)
-> (((->) key :. Maybe) := a)
-> TU Covariant Covariant ((->) key) Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \key
key -> a <:= Product key
forall (t :: * -> *) a. Extractable t => a <:= t
extract (a <:= Product key) -> Maybe (key :*: a) -> Maybe a
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> key -> Maybe (key :*: a)
search key
key where
		search :: key -> Maybe (key :*: a)
search key
key = key
key key -> key -> Boolean
forall a. Setoid a => a -> a -> Boolean
== (key :*: a) -> key
forall a b. (a :*: b) -> a
attached key :*: a
x Boolean
-> Maybe (key :*: a) -> Maybe (key :*: a) -> Maybe (key :*: a)
forall a. Boolean -> a -> a -> a
? (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)
$ (Maybe :. Construction Maybe) := (key :*: a)
xs ((Maybe :. Construction Maybe) := (key :*: a))
-> (Construction Maybe (key :*: a) -> Maybe (key :*: a))
-> Maybe (key :*: a)
forall (t :: * -> *) a b. Bindable t => t a -> (a -> t b) -> t 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
key key -> key -> Boolean
forall a. Setoid a => a -> a -> Boolean
==) (key -> Boolean) -> ((key :*: a) -> key) -> (key :*: a) -> Boolean
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (key :*: a) -> key
forall a b. (a :*: b) -> a
attached)