{-# OPTIONS_GHC -fno-warn-orphans #-}
module Pandora.Paradigm.Structure.Some.List where
import Pandora.Core.Functor (type (:.), type (:=))
import Pandora.Pattern ((.|..))
import Pandora.Pattern.Category ((.), ($), identity)
import Pandora.Pattern.Functor.Covariant (Covariant ((<$>)))
import Pandora.Pattern.Functor.Extractable (extract)
import Pandora.Pattern.Functor.Avoidable (empty)
import Pandora.Pattern.Functor.Traversable (Traversable)
import Pandora.Pattern.Functor.Extendable (Extendable ((=>>)))
import Pandora.Pattern.Transformer.Liftable (lift)
import Pandora.Pattern.Object.Setoid (Setoid ((==)))
import Pandora.Pattern.Object.Semigroup (Semigroup ((+)))
import Pandora.Pattern.Object.Monoid (Monoid (zero))
import Pandora.Paradigm.Primary.Object.Boolean (Boolean (True, False), (?))
import Pandora.Paradigm.Primary.Object.Numerator (Numerator (Numerator))
import Pandora.Paradigm.Primary.Object.Denumerator (Denumerator (One))
import Pandora.Paradigm.Primary.Functor.Function ((%), (&))
import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Just, Nothing))
import Pandora.Paradigm.Primary.Functor.Identity (Identity (Identity))
import Pandora.Paradigm.Primary.Functor.Predicate (Predicate (Predicate))
import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)), type (:*:), twosome)
import Pandora.Paradigm.Primary.Functor.Tagged (Tagged (Tag))
import Pandora.Paradigm.Primary.Functor.Wye (Wye (Left, Right))
import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct), deconstruct, (.-+))
import Pandora.Paradigm.Primary.Transformer.Tap (Tap (Tap))
import Pandora.Paradigm.Inventory.State (State, fold)
import Pandora.Paradigm.Inventory.Store (Store (Store))
import Pandora.Paradigm.Inventory.Optics (view)
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run, (||=))
import Pandora.Paradigm.Schemes.TU (TU (TU), type (<:.>))
import Pandora.Paradigm.Schemes.T_U (T_U (T_U), type (<:.:>))
import Pandora.Paradigm.Structure.Ability.Nonempty (Nonempty)
import Pandora.Paradigm.Structure.Ability.Nullable (Nullable (null))
import Pandora.Paradigm.Structure.Ability.Zipper (Zipper)
import Pandora.Paradigm.Structure.Ability.Focusable (Focusable (Focusing, focusing), Location (Head), focus)
import Pandora.Paradigm.Structure.Ability.Deletable (Deletable ((-=)))
import Pandora.Paradigm.Structure.Ability.Measurable (Measurable (Measural, measurement), Scale (Length), measure)
import Pandora.Paradigm.Structure.Ability.Monotonic (Monotonic (reduce, resolve))
import Pandora.Paradigm.Structure.Ability.Morphable (Morphable (Morphing, morphing), Morph (Rotate, Into, Push, Pop), premorph, rotate, item)
import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Substructural, substructure), Segment (Tail), sub, subview)
import Pandora.Paradigm.Structure.Interface.Stack (Stack)
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 :: * -> * -> *). Category m => m ~~> m
$ 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 (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
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 :: * -> * -> *). Category m => m ~~> m
$ \(Identity a
x) -> 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 :: * -> * -> *). Category m => m ~~> m
$ List a
xs
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 (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
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 :: * -> *) a b.
Interpreted t =>
(Primary t a -> Primary t b) -> t a -> t b
||= List a
xs
instance Stack List where
instance Focusable Head List where
type Focusing Head List a = Maybe a
focusing :: Tagged 'Head (List a) :-. Focusing 'Head List a
focusing (List a <:= Tagged 'Head
forall (t :: * -> *) a. Extractable t => a <:= t
extract -> List a
stack) = (((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Head (List a))
-> Store (Maybe a) (Tagged 'Head (List a))
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Head (List a))
-> Store (Maybe a) (Tagged 'Head (List a)))
-> (((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Head (List a))
-> Store (Maybe a) (Tagged 'Head (List a))
forall (m :: * -> * -> *). Category m => m ~~> m
$ a <:= Construction Maybe
forall (t :: * -> *) a. Extractable t => a <:= t
extract (a <:= Construction Maybe)
-> Maybe (Construction Maybe a) -> Maybe a
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> List a -> Primary List a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run List a
stack Maybe a
-> (Maybe a -> Tagged 'Head (List a))
-> ((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Head (List a)
forall s a. s -> a -> Product s a
:*: \case
Just a
x -> List a
stack List a -> (List a -> List a) -> List a
forall a b. a -> (a -> b) -> b
& forall k (f :: k) (t :: * -> *).
Substructure f t =>
t ~> Substructural f t
forall (t :: * -> *).
Substructure 'Tail t =>
t ~> Substructural 'Tail t
subview @Tail List a -> (List a -> List a) -> List a
forall a b. a -> (a -> b) -> b
& a :=:=> List
forall k (f :: k) (t :: * -> *) a.
(Morphable f t, Morphing f t ~ ((Identity <:.:> t) := (->))) =>
a :=:=> t
item @Push a
x List a
-> (List a -> Tagged 'Head (List a)) -> Tagged 'Head (List a)
forall a b. a -> (a -> b) -> b
& List a -> Tagged 'Head (List a)
forall k (tag :: k) a. a -> Tagged tag a
Tag
Maybe a
Nothing -> List a
stack List a -> (List a -> List a) -> List a
forall a b. a -> (a -> b) -> b
& forall k (f :: k) (t :: * -> *).
Substructure f t =>
t ~> Substructural f t
forall (t :: * -> *).
Substructure 'Tail t =>
t ~> Substructural 'Tail t
subview @Tail List a
-> (List a -> Tagged 'Head (List a)) -> Tagged 'Head (List a)
forall a b. a -> (a -> b) -> b
& List a -> Tagged 'Head (List a)
forall k (tag :: k) a. a -> Tagged tag a
Tag
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 :: * -> * -> *). Category m => m ~~> m
$ Construction Maybe a -> Measural 'Length (Construction Maybe) a
forall k (f :: k) (t :: * -> *) a.
Measurable f t =>
t a -> Measural f t a
measure @Length Construction Maybe a
xs
instance Nullable 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 :: * -> * -> *). Category m => m ~~> m
$ \case { TU Maybe (Construction Maybe a)
Nothing -> Boolean
True ; List a
_ -> Boolean
False }
instance Substructure Tail List where
type Substructural Tail List = List
substructure :: Lens ((<:.>) (Tagged 'Tail) List a) (Substructural 'Tail List a)
substructure (TU Covariant Covariant Maybe (Construction Maybe) a
-> Maybe (Construction Maybe a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (TU Covariant Covariant Maybe (Construction Maybe) a
-> Maybe (Construction Maybe a))
-> ((<:.>) (Tagged 'Tail) 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 -> 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
<$> Lens
(Construction Maybe a) (Substructural 'Tail (Construction Maybe) a)
forall k (f :: k) (t :: * -> *).
Substructure f t =>
t :~. Substructural f t
sub @Tail Construction Maybe a
ns
substructure (TU Covariant Covariant Maybe (Construction Maybe) a
-> Maybe (Construction Maybe a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (TU Covariant Covariant Maybe (Construction Maybe) a
-> Maybe (Construction Maybe a))
-> ((<:.>) (Tagged 'Tail) 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 -> 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 :: * -> * -> *). Category m => m ~~> m
$ TU Covariant Covariant Maybe (Construction Maybe) a
forall (t :: * -> *) a. Avoidable t => t a
empty TU Covariant Covariant Maybe (Construction Maybe) a
-> (TU Covariant Covariant Maybe (Construction Maybe) a
-> (<:.>) (Tagged 'Tail) 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
instance Deletable List where
a
_ -= :: a :=:=> List
-= TU Maybe (Construction Maybe a)
Nothing = 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)
forall a. Maybe a
Nothing
a
x -= TU (Just (Construct a
y Maybe (Construction Maybe a)
ys)) = a
x a -> a -> Boolean
forall a. Setoid a => a -> a -> Boolean
== a
y Boolean
-> TU Covariant Covariant Maybe (Construction Maybe) a
-> TU Covariant Covariant Maybe (Construction Maybe) a
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall a. Boolean -> a -> a -> a
? 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)
ys
(TU Covariant Covariant Maybe (Construction Maybe) a
-> TU Covariant Covariant Maybe (Construction Maybe) a)
-> TU Covariant Covariant Maybe (Construction Maybe) a
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *). Category m => m ~~> m
$ 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)
-> (TU Covariant Covariant Maybe (Construction Maybe) a
-> Construction Maybe a)
-> TU Covariant Covariant Maybe (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
. a -> Maybe (Construction Maybe a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
y (Maybe (Construction Maybe a) -> Construction Maybe a)
-> (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 (TU Covariant Covariant Maybe (Construction Maybe) a
-> Maybe (Construction Maybe a))
-> (TU Covariant Covariant Maybe (Construction Maybe) a
-> TU Covariant Covariant Maybe (Construction Maybe) a)
-> TU Covariant Covariant 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 :=:=> List
forall (t :: * -> *) a. (Deletable t, Setoid a) => a :=:=> t
(-=) @List a
x (TU Covariant Covariant Maybe (Construction Maybe) a
-> TU Covariant Covariant Maybe (Construction Maybe) a)
-> TU Covariant Covariant Maybe (Construction Maybe) a
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *). Category m => m ~~> m
$ Maybe (Construction Maybe a)
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
(a :: k).
((t :. u) := a) -> TU ct cu t u a
TU Maybe (Construction Maybe a)
ys
filter :: forall a . Predicate a -> List a -> List a
filter :: Predicate a -> List a -> List a
filter (Predicate a -> Boolean
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) -> List a)
-> (List a -> (Maybe :. Construction Maybe) := a)
-> List 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))
-> (List a
-> Product
((Maybe :. Construction Maybe) := a)
((Maybe :. Construction Maybe) := a))
-> List 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))
-> (List a
-> State
((Maybe :. Construction Maybe) := a)
((Maybe :. Construction Maybe) := a))
-> 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
. (a
-> ((Maybe :. Construction Maybe) := a)
-> (Maybe :. Construction Maybe) := a)
-> List a
-> State
((Maybe :. Construction Maybe) := a)
((Maybe :. Construction Maybe) := a)
forall (t :: * -> *) s (u :: * -> *) a.
(Traversable t, Memorable s u) =>
(a -> s -> s) -> t a -> u s
fold (\a
now (Maybe :. Construction Maybe) := a
new -> a -> Boolean
p a
now Boolean
-> ((Maybe :. Construction Maybe) := a)
-> ((Maybe :. Construction Maybe) := a)
-> (Maybe :. Construction Maybe) := a
forall a. Boolean -> a -> a -> a
? Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall a. a -> Maybe a
Just (a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
now (Maybe :. Construction Maybe) := a
new) (((Maybe :. Construction Maybe) := a)
-> (Maybe :. Construction Maybe) := a)
-> ((Maybe :. Construction Maybe) := a)
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *). Category m => m ~~> m
$ (Maybe :. Construction Maybe) := a
new)
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 (v :: * -> * -> *) a c d b.
(Category v, Covariant (v a)) =>
v c d -> ((v a :. v b) := c) -> (v a :. v b) := d
.|.. ((->) a :. (->) ((Maybe :. Construction Maybe) := a))
:= Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct)
type instance Nonempty 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 :: * -> * -> *). Category m => m ~~> m
$ Construction Maybe a -> Maybe (Construction Maybe a)
forall a. a -> Maybe a
Just Construction Maybe a
ys
Construct a
x (Just Construction Maybe a
xs) + Construction Maybe a
ys = a -> Maybe (Construction Maybe a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Maybe (Construction Maybe a) -> Construction Maybe a)
-> (Construction Maybe a -> Maybe (Construction Maybe a))
-> Construction Maybe a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Maybe a -> Maybe (Construction Maybe a)
forall a. a -> Maybe a
Just (Construction Maybe a -> Construction Maybe a)
-> Construction Maybe a -> Construction Maybe a
forall (m :: * -> * -> *). Category m => m ~~> m
$ Construction Maybe a
xs Construction Maybe a
-> Construction Maybe a -> Construction Maybe a
forall a. Semigroup a => a -> a -> a
+ Construction Maybe a
ys
instance Morphable (Into 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 (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph
instance Focusable Head (Construction Maybe) where
type Focusing Head (Construction Maybe) a = a
focusing :: Tagged 'Head (Construction Maybe a)
:-. Focusing 'Head (Construction Maybe) a
focusing (Construction Maybe a <:= Tagged 'Head
forall (t :: * -> *) a. Extractable t => a <:= t
extract -> Construction Maybe a
stack) = (((:*:) a :. (->) a) := Tagged 'Head (Construction Maybe a))
-> Store a (Tagged 'Head (Construction Maybe a))
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) a :. (->) a) := Tagged 'Head (Construction Maybe a))
-> Store a (Tagged 'Head (Construction Maybe a)))
-> (((:*:) a :. (->) a) := Tagged 'Head (Construction Maybe a))
-> Store a (Tagged 'Head (Construction Maybe a))
forall (m :: * -> * -> *). Category m => m ~~> m
$ a <:= Construction Maybe
forall (t :: * -> *) a. Extractable t => a <:= t
extract Construction Maybe a
stack a
-> (a -> Tagged 'Head (Construction Maybe a))
-> ((:*:) a :. (->) a) := Tagged 'Head (Construction Maybe a)
forall s a. s -> a -> Product s a
:*: Construction Maybe a -> Tagged 'Head (Construction Maybe a)
forall k (tag :: k) a. a -> Tagged tag a
Tag (Construction Maybe a -> Tagged 'Head (Construction Maybe a))
-> (a -> Construction Maybe a)
-> a
-> Tagged 'Head (Construction Maybe a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a)
-> ((Maybe :. Construction Maybe) := a)
-> a
-> Construction Maybe a
forall a b c. (a -> b -> c) -> b -> a -> c
% Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct Construction Maybe a
stack
instance 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 (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
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 :: * -> * -> *). Category m => m ~~> m
$ \(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 :: * -> * -> *). Category m => m ~~> m
$ 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 Monotonic a (Construction Maybe a) where
reduce :: (a -> r -> r) -> r -> Construction Maybe a -> r
reduce a -> r -> r
f r
r ~(Construct a
x (Maybe :. Construction Maybe) := a
xs) = a -> r -> r
f a
x (r -> r) -> r -> r
forall (m :: * -> * -> *). Category m => m ~~> m
$ (a -> r -> r) -> r -> ((Maybe :. Construction Maybe) := a) -> r
forall a e r. Monotonic a e => (a -> r -> r) -> r -> e -> r
reduce a -> r -> r
f r
r (Maybe :. Construction Maybe) := a
xs
instance Substructure Tail (Construction Maybe) where
type Substructural Tail (Construction Maybe) = List
substructure :: Lens
((<:.>) (Tagged 'Tail) (Construction Maybe) a)
(Substructural 'Tail (Construction Maybe) a)
substructure (Construction Maybe a <:= Tagged 'Tail
forall (t :: * -> *) a. Extractable t => a <:= t
extract (Construction Maybe a <:= Tagged 'Tail)
-> ((<:.>) (Tagged 'Tail) (Construction Maybe) a
-> Tagged 'Tail (Construction Maybe a))
-> (<:.>) (Tagged 'Tail) (Construction Maybe) a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Tail) (Construction Maybe) a
-> Tagged 'Tail (Construction Maybe a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Construct a
x (Maybe :. Construction Maybe) := a
xs) =
(((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
:. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
:= (<:.>) (Tagged 'Tail) (Construction Maybe) a)
-> Store
(TU Covariant Covariant Maybe (Construction Maybe) a)
((<:.>) (Tagged 'Tail) (Construction Maybe) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
:. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
:= (<:.>) (Tagged 'Tail) (Construction Maybe) a)
-> Store
(TU Covariant Covariant Maybe (Construction Maybe) a)
((<:.>) (Tagged 'Tail) (Construction Maybe) a))
-> (((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
:. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
:= (<:.>) (Tagged 'Tail) (Construction Maybe) a)
-> Store
(TU Covariant Covariant Maybe (Construction Maybe) a)
((<:.>) (Tagged 'Tail) (Construction Maybe) a)
forall (m :: * -> * -> *). Category m => m ~~> m
$ ((Maybe :. Construction Maybe) := a)
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
(a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (Maybe :. Construction Maybe) := a
xs TU Covariant Covariant Maybe (Construction Maybe) a
-> (TU Covariant Covariant Maybe (Construction Maybe) a
-> (<:.>) (Tagged 'Tail) (Construction Maybe) a)
-> ((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
:. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
:= (<:.>) (Tagged 'Tail) (Construction Maybe) a
forall s a. s -> a -> Product s a
:*: Construction Maybe a
-> (<:.>) (Tagged 'Tail) (Construction Maybe) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Maybe a
-> (<:.>) (Tagged 'Tail) (Construction Maybe) a)
-> (TU Covariant Covariant Maybe (Construction Maybe) a
-> Construction Maybe a)
-> TU Covariant Covariant Maybe (Construction Maybe) a
-> (<:.>) (Tagged 'Tail) (Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (((Maybe :. Construction Maybe) := a) -> Construction Maybe a)
-> (TU Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a)
-> TU Covariant Covariant Maybe (Construction Maybe) a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run
type instance Zipper List = Tap (List <:.:> List := (:*:))
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)
-> TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap ((List <:.:> List) := (:*:)) a)
move Tap ((List <:.:> List) := (:*:)) a :=> Maybe
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 :: * -> * -> *). Category m => m ~~> m
$ Tap ((List <:.:> List) := (:*:)) a :=> Maybe
rtt (Tap ((List <:.:> List) := (:*:)) a :=> Maybe)
-> Tap ((List <:.:> List) := (:*:)) a :=> Construction Maybe
forall (t :: * -> *) a.
Covariant t =>
(a :=> t) -> a :=> Construction t
.-+ Tap ((List <:.:> List) := (:*:)) a
z
in Tap ((List <:.:> List) := (:*:)) a -> b
f (Tap ((List <:.:> List) := (:*:)) a -> b)
-> Tap
((List <:.:> List) := (:*:)) (Tap ((List <:.:> List) := (:*:)) a)
-> Tap ((List <:.:> List) := (:*:)) b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> Tap ((List <:.:> List) := (:*:)) a
-> T_U
Covariant
Covariant
(:*:)
List
List
(Tap ((List <:.:> List) := (:*:)) a)
-> Tap
((List <:.:> List) := (:*:)) (Tap ((List <:.:> List) := (:*:)) a)
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap Tap ((List <:.:> List) := (:*:)) a
z (TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap ((List <:.:> List) := (:*:)) a)
-> TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap ((List <:.:> List) := (:*:)) a)
-> T_U
Covariant
Covariant
(:*:)
List
List
(Tap ((List <:.:> List) := (:*:)) a)
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome ((Tap ((List <:.:> List) := (:*:)) a :=> Maybe)
-> TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap ((List <:.:> List) := (:*:)) a)
move ((Tap ((List <:.:> List) := (:*:)) a :=> Maybe)
-> TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap ((List <:.:> List) := (:*:)) a))
-> (Tap ((List <:.:> List) := (:*:)) a :=> Maybe)
-> TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap ((List <:.:> List) := (:*:)) a)
forall (m :: * -> * -> *). Category m => m ~~> m
$ (<:.>) 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
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. forall a (f :: a) (t :: * -> *).
Morphable ('Rotate f) t =>
t ~> Morphing ('Rotate f) t
forall (t :: * -> *).
Morphable ('Rotate 'Left) t =>
t ~> Morphing ('Rotate 'Left) t
rotate @Left) ((Tap ((List <:.:> List) := (:*:)) a :=> Maybe)
-> TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap ((List <:.:> List) := (:*:)) a)
move ((Tap ((List <:.:> List) := (:*:)) a :=> Maybe)
-> TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap ((List <:.:> List) := (:*:)) a))
-> (Tap ((List <:.:> List) := (:*:)) a :=> Maybe)
-> TU
Covariant
Covariant
Maybe
(Construction Maybe)
(Tap ((List <:.:> List) := (:*:)) a)
forall (m :: * -> * -> *). Category m => m ~~> m
$ (<:.>) 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
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. forall a (f :: a) (t :: * -> *).
Morphable ('Rotate f) t =>
t ~> Morphing ('Rotate f) t
forall (t :: * -> *).
Morphable ('Rotate 'Right) t =>
t ~> Morphing ('Rotate 'Right) t
rotate @Right))
instance Morphable (Rotate Left) (Tap (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 (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> Tap a
x (T_U (List a
bs :*: List a
fs))) = ((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 :: * -> * -> *). Category m => m ~~> m
$ 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 (List a -> Substructural 'Tail List a
forall k (f :: k) (t :: * -> *).
Substructure f t =>
t ~> Substructural f t
subview @Tail List a
bs) (a :=:=> List
forall k (f :: k) (t :: * -> *) a.
(Morphable f t, Morphing f t ~ ((Identity <:.:> t) := (->))) =>
a :=:=> t
item @Push a
x List a
fs) (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 :: * -> *) a.
Focusable f t =>
t a :-. Focusing f t a
forall (t :: * -> *) a.
Focusable 'Head t =>
t a :-. Focusing 'Head t a
focus @Head) List a
bs
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 (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> Tap a
x (T_U (List a
bs :*: List a
fs))) = ((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 :: * -> * -> *). Category m => m ~~> m
$ 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 (f :: k) (t :: * -> *) a.
(Morphable f t, Morphing f t ~ ((Identity <:.:> t) := (->))) =>
a :=:=> t
item @Push a
x List a
bs) (List a -> Substructural 'Tail List a
forall k (f :: k) (t :: * -> *).
Substructure f t =>
t ~> Substructural f t
subview @Tail List a
fs) (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 :: * -> *) a.
Focusable f t =>
t a :-. Focusing f t a
forall (t :: * -> *) a.
Focusable 'Head t =>
t a :-. Focusing 'Head t a
focus @Head) List a
fs
type instance Zipper (Construction Maybe) = Tap (Construction Maybe <:.:> Construction Maybe := (:*:))
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 (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> Tap a
x (T_U (Construction Maybe a
bs :*: Construction Maybe a
fs))) = ((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 :: * -> * -> *). Category m => m ~~> m
$ 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
bs) (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 (f :: k) (t :: * -> *) a.
(Morphable f t, Morphing f t ~ ((Identity <:.:> t) := (->))) =>
a :=:=> t
item @Push a
x Construction Maybe a
fs) (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
bs
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 (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> Tap a
x (T_U (Construction Maybe a
bs :*: Construction Maybe a
fs))) = ((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 :: * -> * -> *). Category m => m ~~> m
$ 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
fs) (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 (f :: k) (t :: * -> *) a.
(Morphable f t, Morphing f t ~ ((Identity <:.:> t) := (->))) =>
a :=:=> t
item @Push a
x Construction Maybe a
bs) (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
fs
instance Monotonic a (Maybe <:.> Construction Maybe := a) where
reduce :: (a -> r -> r) -> r -> (List := a) -> r
reduce a -> r -> r
f r
r = (a -> r -> r) -> r -> ((Maybe :. Construction Maybe) := a) -> r
forall a e r. Monotonic a e => (a -> r -> r) -> r -> e -> r
reduce a -> r -> r
f r
r (((Maybe :. Construction Maybe) := a) -> r)
-> ((List := a) -> (Maybe :. Construction Maybe) := a)
-> (List := a)
-> r
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