{-# OPTIONS_GHC -fno-warn-orphans #-}
module Pandora.Paradigm.Structure.Some.List where
import Pandora.Core.Functor (type (:.), type (:=))
import Pandora.Core.Impliable (imply)
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category ((#), identity)
import Pandora.Pattern.Functor.Covariant (Covariant, Covariant ((<-|-)))
import Pandora.Pattern.Functor.Traversable (Traversable ((<<-)))
import Pandora.Pattern.Functor.Extendable (Extendable ((<<=)))
import Pandora.Pattern.Functor.Bindable (Bindable ((=<<)))
import Pandora.Pattern.Functor.Adjoint (Adjoint ((|-)))
import Pandora.Pattern.Transformer.Liftable (lift)
import Pandora.Pattern.Transformer.Lowerable (lower)
import Pandora.Pattern.Object.Setoid (Setoid ((==)))
import Pandora.Pattern.Object.Semigroup (Semigroup ((+)))
import Pandora.Pattern.Object.Monoid (Monoid (zero))
import Pandora.Paradigm.Primary.Object.Boolean (Boolean (True, False))
import Pandora.Paradigm.Primary.Algebraic ((<-*-), (.-+-), (-.#..-), extract, point, empty, void)
import Pandora.Paradigm.Primary.Algebraic.Product ((:*:) ((:*:)), attached)
import Pandora.Paradigm.Primary.Algebraic.Exponential ((%))
import Pandora.Paradigm.Primary.Algebraic ((<-|-<-|-))
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.Wye (Wye (Left, Right))
import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct), deconstruct, (.-+))
import Pandora.Paradigm.Primary.Transformer.Reverse (Reverse (Reverse))
import Pandora.Paradigm.Primary (twosome)
import Pandora.Paradigm.Inventory.Ability.Gettable (get)
import Pandora.Paradigm.Inventory.Ability.Modifiable (Modifiable (Modification, modify))
import Pandora.Paradigm.Inventory.Some.State (State, fold)
import Pandora.Paradigm.Inventory.Some.Store (Store (Store))
import Pandora.Paradigm.Inventory.Some.Optics (Convex, Obscure, Lens)
import Pandora.Paradigm.Controlflow.Effect.Conditional (Conditional ((?)))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run, (!), (||=))
import Pandora.Paradigm.Schemes.TT (TT (TT), type (<::>))
import Pandora.Paradigm.Schemes.T_U (T_U (T_U), type (<:.:>))
import Pandora.Paradigm.Schemes.P_Q_T (P_Q_T (P_Q_T))
import Pandora.Paradigm.Structure.Ability.Nonempty (Nonempty)
import Pandora.Paradigm.Structure.Ability.Nullable (Nullable (null))
import Pandora.Paradigm.Structure.Ability.Zipper (Zippable (Breadcrumbs), Zipper, Tape)
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 (Available, Substance, 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))
import Pandora.Paradigm.Structure.Modification.Turnover (Turnover (Turnover))
type List = Maybe <::> Construction Maybe
instance Setoid a => Setoid (List a) where
TT (Maybe :. Construction Maybe) := a
ls == :: List a -> List a -> Boolean
== TT (Maybe :. Construction Maybe) := a
rs = (Maybe :. Construction Maybe) := a
ls ((Maybe :. Construction Maybe) := a)
-> ((Maybe :. Construction Maybe) := a) -> Boolean
forall a. Setoid a => a -> a -> Boolean
== (Maybe :. Construction Maybe) := a
rs
instance Semigroup (List a) where
TT Maybe (Construction Maybe a)
Nothing + :: List a -> List a -> List a
+ TT Maybe (Construction Maybe a)
ys = Maybe (Construction Maybe a) -> List a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
(a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT Maybe (Construction Maybe a)
ys
TT (Just (Construct a
x Maybe (Construction Maybe a)
xs)) + TT Maybe (Construction Maybe a)
ys = Construction Maybe a -> List a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Maybe a -> List a)
-> (List a -> Construction Maybe a) -> List a -> List a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> Maybe (Construction Maybe a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Maybe (Construction Maybe a) -> Construction Maybe a)
-> (List a -> Maybe (Construction Maybe a))
-> List a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. List a -> Maybe (Construction Maybe a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run
(List a -> List a) -> List a -> List a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Maybe (Construction Maybe a) -> List a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
(a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT @Covariant @Covariant Maybe (Construction Maybe a)
xs List a -> List a -> List a
forall a. Semigroup a => a -> a -> a
+ Maybe (Construction Maybe a) -> List a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
(a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT @Covariant @Covariant Maybe (Construction Maybe a)
ys
instance Monoid (List a) where
zero :: List a
zero = List a
forall (t :: * -> *) a. Emptiable t => t a
empty
instance Morphable Push List where
type Morphing Push List = 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Construction Maybe a -> List a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Maybe a -> List a)
-> (Identity a -> Construction Maybe a) -> Identity a -> List a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a)
-> ((Maybe :. Construction Maybe) := a)
-> a
-> Construction Maybe a
forall a b c. (a -> b -> c) -> b -> a -> c
% List a -> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run List a
xs) (a -> Construction Maybe a)
-> (Identity a -> a) -> Identity a -> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract
instance Morphable Pop List where
type Morphing Pop List = List
morphing :: (<::>) (Tagged 'Pop) List a -> Morphing 'Pop List a
morphing ((<::>) (Tagged 'Pop) List a -> List a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> List a
xs) = (Construction Maybe a -> (Maybe :. Construction Maybe) := a)
-> ((Maybe :. Construction Maybe) := a)
-> ((Maybe :. Construction Maybe) := a)
-> (Maybe :. Construction Maybe) := a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct (Maybe :. Construction Maybe) := a
forall a. Maybe a
Nothing (Primary List a -> Primary List a) -> List a -> List a
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
m (Primary t a) (Primary u b) -> m (t a) (u b)
||= List a
xs
instance Morphable (Find Element) List where
type Morphing (Find Element) List = Predicate <:.:> Maybe := (->)
morphing :: (<::>) (Tagged ('Find 'Element)) List a
-> Morphing ('Find 'Element) List a
morphing (<::>) (Tagged ('Find 'Element)) List a
list = case TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<::>) (Tagged ('Find 'Element)) List a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph (<::>) (Tagged ('Find 'Element)) List a
list of
(Maybe :. Construction Maybe) := a
Nothing -> (Predicate a -> Maybe a)
-> T_U Covariant Covariant (->) Predicate Maybe a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
(t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((Predicate a -> Maybe a)
-> T_U Covariant Covariant (->) Predicate Maybe a)
-> (Predicate a -> Maybe a)
-> T_U Covariant Covariant (->) Predicate Maybe a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \Predicate a
_ -> Maybe a
forall a. Maybe a
Nothing
Just (Construct a
x (Maybe :. Construction Maybe) := a
xs) -> (Predicate a -> Maybe a)
-> T_U Covariant Covariant (->) Predicate Maybe a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
(t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((Predicate a -> Maybe a)
-> T_U Covariant Covariant (->) Predicate Maybe a)
-> (Predicate a -> Maybe a)
-> T_U Covariant Covariant (->) Predicate Maybe a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \Predicate a
p -> Predicate a -> a -> Boolean
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run Predicate a
p a
x Boolean -> Maybe a -> Maybe a -> Maybe a
forall clause a. Conditional clause => clause -> a -> a -> a
? a -> Maybe a
forall a. a -> Maybe a
Just a
x
(Maybe a -> Maybe a) -> Maybe a -> Maybe a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! forall a2.
Morphed ('Find 'Element) List ((Predicate <:.:> Maybe) := (->)) =>
Predicate a2 -> List a2 -> Maybe a2
forall a1 (mod :: a1) (struct :: * -> *) (result :: * -> *) a2.
Morphed ('Find mod) struct ((Predicate <:.:> result) := (->)) =>
Predicate a2 -> struct a2 -> result a2
find @Element @List @Maybe (Predicate a
-> TT Covariant Covariant Maybe (Construction Maybe) a -> Maybe a)
-> Predicate a
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Predicate a
p (TT Covariant Covariant Maybe (Construction Maybe) a -> Maybe a)
-> TT Covariant Covariant Maybe (Construction Maybe) a -> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# ((Maybe :. Construction Maybe) := a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
(a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (Maybe :. Construction Maybe) := a
xs
instance Morphable (Delete First) List where
type Morphing (Delete First) List = Predicate <:.:> List := (->)
morphing :: (<::>) (Tagged ('Delete 'First)) List a
-> Morphing ('Delete 'First) List a
morphing (<::>) (Tagged ('Delete 'First)) List a
list = case TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<::>) (Tagged ('Delete 'First)) List a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph (<::>) (Tagged ('Delete 'First)) List a
list of
(Maybe :. Construction Maybe) := a
Nothing -> (Predicate a
-> TT Covariant Covariant Maybe (Construction Maybe) a)
-> T_U Covariant Covariant (->) Predicate List a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
(t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((Predicate a
-> TT Covariant Covariant Maybe (Construction Maybe) a)
-> T_U Covariant Covariant (->) Predicate List a)
-> (Predicate a
-> TT Covariant Covariant Maybe (Construction Maybe) a)
-> T_U Covariant Covariant (->) Predicate List a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \Predicate a
_ -> TT Covariant Covariant Maybe (Construction Maybe) a
forall (t :: * -> *) a. Emptiable t => t a
empty
Just (Construct a
x (Maybe :. Construction Maybe) := a
xs) -> (Predicate a
-> TT Covariant Covariant Maybe (Construction Maybe) a)
-> T_U Covariant Covariant (->) Predicate List a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
(t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((Predicate a
-> TT Covariant Covariant Maybe (Construction Maybe) a)
-> T_U Covariant Covariant (->) Predicate List a)
-> (Predicate a
-> TT Covariant Covariant Maybe (Construction Maybe) a)
-> T_U Covariant Covariant (->) Predicate List a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \Predicate a
p ->
Predicate a -> a -> Boolean
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run Predicate a
p a
x Boolean
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall clause a. Conditional clause => clause -> a -> a -> a
? ((Maybe :. Construction Maybe) := a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
(a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (Maybe :. Construction Maybe) := a
xs (TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Construction Maybe a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Maybe a
-> TT Covariant Covariant Maybe (Construction Maybe) a)
-> (TT Covariant Covariant Maybe (Construction Maybe) a
-> Construction Maybe a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (((Maybe :. Construction Maybe) := a) -> Construction Maybe a)
-> (TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a)
-> (TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Predicate a
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall a1 (mod :: a1) (struct :: * -> *) a2.
Morphed ('Delete mod) struct ((Predicate <:.:> struct) := (->)) =>
Predicate a2 -> struct a2 -> struct a2
filter @First @List Predicate a
p (TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# ((Maybe :. Construction Maybe) := a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
(a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (Maybe :. Construction Maybe) := a
xs
instance Morphable (Delete All) List where
type Morphing (Delete All) List = Predicate <:.:> List := (->)
morphing :: (<::>) (Tagged ('Delete 'All)) List a
-> Morphing ('Delete 'All) List a
morphing (<::>) (Tagged ('Delete 'All)) List a
list = case TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<::>) (Tagged ('Delete 'All)) List a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph (<::>) (Tagged ('Delete 'All)) List a
list of
(Maybe :. Construction Maybe) := a
Nothing -> (Predicate a
-> TT Covariant Covariant Maybe (Construction Maybe) a)
-> T_U Covariant Covariant (->) Predicate List a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
(t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((Predicate a
-> TT Covariant Covariant Maybe (Construction Maybe) a)
-> T_U Covariant Covariant (->) Predicate List a)
-> (Predicate a
-> TT Covariant Covariant Maybe (Construction Maybe) a)
-> T_U Covariant Covariant (->) Predicate List a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \Predicate a
_ -> TT Covariant Covariant Maybe (Construction Maybe) a
forall (t :: * -> *) a. Emptiable t => t a
empty
Just (Construct a
x (Maybe :. Construction Maybe) := a
xs) -> (Predicate a
-> TT Covariant Covariant Maybe (Construction Maybe) a)
-> T_U Covariant Covariant (->) Predicate List a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
(t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((Predicate a
-> TT Covariant Covariant Maybe (Construction Maybe) a)
-> T_U Covariant Covariant (->) Predicate List a)
-> (Predicate a
-> TT Covariant Covariant Maybe (Construction Maybe) a)
-> T_U Covariant Covariant (->) Predicate List a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \Predicate a
p ->
Predicate a -> a -> Boolean
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run Predicate a
p a
x Boolean
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall clause a. Conditional clause => clause -> a -> a -> a
? Predicate a
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall a1 (mod :: a1) (struct :: * -> *) a2.
Morphed ('Delete mod) struct ((Predicate <:.:> struct) := (->)) =>
Predicate a2 -> struct a2 -> struct a2
filter @All @List Predicate a
p (((Maybe :. Construction Maybe) := a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
(a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (Maybe :. Construction Maybe) := a
xs)
(TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Construction Maybe a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Maybe a
-> TT Covariant Covariant Maybe (Construction Maybe) a)
-> (TT Covariant Covariant Maybe (Construction Maybe) a
-> Construction Maybe a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (((Maybe :. Construction Maybe) := a) -> Construction Maybe a)
-> (TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a)
-> (TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Predicate a
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall a1 (mod :: a1) (struct :: * -> *) a2.
Morphed ('Delete mod) struct ((Predicate <:.:> struct) := (->)) =>
Predicate a2 -> struct a2 -> struct a2
filter @All @List Predicate a
p (TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# ((Maybe :. Construction Maybe) := a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
(a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (Maybe :. Construction Maybe) := a
xs
instance Stack List where
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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \case { TT Maybe (Construction Maybe a)
Nothing -> Boolean
True ; List a
_ -> Boolean
False }
instance Substructure Root List where
type Available Root List = Maybe
type Substance Root List = Identity
substructure :: Lens
(Available 'Root List)
((<:.>) (Tagged 'Root) List a)
(Substance 'Root List a)
substructure = ((<:.>) (Tagged 'Root) List a
-> Store (Maybe (Identity a)) ((<:.>) (Tagged 'Root) List a))
-> P_Q_T
(->) Store Maybe ((<:.>) (Tagged 'Root) List a) (Identity a)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Root) List a
-> Store (Maybe (Identity a)) ((<:.>) (Tagged 'Root) List a))
-> P_Q_T
(->) Store Maybe ((<:.>) (Tagged 'Root) List a) (Identity a))
-> ((<:.>) (Tagged 'Root) List a
-> Store (Maybe (Identity a)) ((<:.>) (Tagged 'Root) List a))
-> P_Q_T
(->) Store Maybe ((<:.>) (Tagged 'Root) List a) (Identity a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(<:.>) (Tagged 'Root) List a
zipper -> case List a -> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (List a -> (Maybe :. Construction Maybe) := a)
-> List a -> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<:.>) (Tagged 'Root) List a -> List a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged 'Root) List a
zipper of
Just (Construct a
x (Maybe :. Construction Maybe) := a
xs) -> (((:*:) (Maybe (Identity a)) :. (->) (Maybe (Identity a)))
:= (<:.>) (Tagged 'Root) List a)
-> Store (Maybe (Identity a)) ((<:.>) (Tagged 'Root) List a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Identity a)) :. (->) (Maybe (Identity a)))
:= (<:.>) (Tagged 'Root) List a)
-> Store (Maybe (Identity a)) ((<:.>) (Tagged 'Root) List a))
-> (((:*:) (Maybe (Identity a)) :. (->) (Maybe (Identity a)))
:= (<:.>) (Tagged 'Root) List a)
-> Store (Maybe (Identity a)) ((<:.>) (Tagged 'Root) List a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Identity a -> Maybe (Identity a)
forall a. a -> Maybe a
Just (a -> Identity a
forall a. a -> Identity a
Identity a
x) Maybe (Identity a)
-> (Maybe (Identity a) -> (<:.>) (Tagged 'Root) List a)
-> ((:*:) (Maybe (Identity a)) :. (->) (Maybe (Identity a)))
:= (<:.>) (Tagged 'Root) List a
forall s a. s -> a -> s :*: a
:*: List a -> (<:.>) (Tagged 'Root) List a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (List a -> (<:.>) (Tagged 'Root) List a)
-> (Maybe (Identity a) -> List a)
-> Maybe (Identity a)
-> (<:.>) (Tagged 'Root) List a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Identity a -> List a) -> List a -> Maybe (Identity a) -> List a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve (Construction Maybe a -> List a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Maybe a -> List a)
-> (Identity a -> Construction Maybe a) -> Identity a -> List a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a)
-> ((Maybe :. Construction Maybe) := a)
-> a
-> Construction Maybe a
forall a b c. (a -> b -> c) -> b -> a -> c
% (Maybe :. Construction Maybe) := a
xs) (a -> Construction Maybe a)
-> (Identity a -> a) -> Identity a -> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall a. Extractable Identity => Identity a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract @Identity) List a
forall a. Monoid a => a
zero
(Maybe :. Construction Maybe) := a
Nothing -> (((:*:) (Maybe (Identity a)) :. (->) (Maybe (Identity a)))
:= (<:.>) (Tagged 'Root) List a)
-> Store (Maybe (Identity a)) ((<:.>) (Tagged 'Root) List a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Identity a)) :. (->) (Maybe (Identity a)))
:= (<:.>) (Tagged 'Root) List a)
-> Store (Maybe (Identity a)) ((<:.>) (Tagged 'Root) List a))
-> (((:*:) (Maybe (Identity a)) :. (->) (Maybe (Identity a)))
:= (<:.>) (Tagged 'Root) List a)
-> Store (Maybe (Identity a)) ((<:.>) (Tagged 'Root) List a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Maybe (Identity a)
forall a. Maybe a
Nothing Maybe (Identity a)
-> (Maybe (Identity a) -> (<:.>) (Tagged 'Root) List a)
-> ((:*:) (Maybe (Identity a)) :. (->) (Maybe (Identity a)))
:= (<:.>) (Tagged 'Root) List a
forall s a. s -> a -> s :*: a
:*: List a -> (<:.>) (Tagged 'Root) List a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (List a -> (<:.>) (Tagged 'Root) List a)
-> (Maybe (Identity a) -> List a)
-> Maybe (Identity a)
-> (<:.>) (Tagged 'Root) List a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Identity a -> List a) -> List a -> Maybe (Identity a) -> List a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve (Construction Maybe a -> List a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Maybe a -> List a)
-> (Identity a -> Construction Maybe a) -> Identity a -> List a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a)
-> ((Maybe :. Construction Maybe) := a)
-> a
-> Construction Maybe a
forall a b c. (a -> b -> c) -> b -> a -> c
% (Maybe :. Construction Maybe) := a
forall a. Maybe a
Nothing) (a -> Construction Maybe a)
-> (Identity a -> a) -> Identity a -> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall a. Extractable Identity => Identity a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract @Identity) List a
forall a. Monoid a => a
zero
instance Substructure Tail List where
type Available Tail List = Identity
type Substance Tail List = List
substructure :: Lens
(Available 'Tail List)
((<:.>) (Tagged 'Tail) List a)
(Substance 'Tail List a)
substructure = ((<:.>) (Tagged 'Tail) List a
-> Store
(Identity (TT Covariant Covariant Maybe (Construction Maybe) a))
((<:.>) (Tagged 'Tail) List a))
-> P_Q_T
(->)
Store
Identity
((<:.>) (Tagged 'Tail) List a)
(TT Covariant Covariant Maybe (Construction Maybe) a)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Tail) List a
-> Store
(Identity (TT Covariant Covariant Maybe (Construction Maybe) a))
((<:.>) (Tagged 'Tail) List a))
-> P_Q_T
(->)
Store
Identity
((<:.>) (Tagged 'Tail) List a)
(TT Covariant Covariant Maybe (Construction Maybe) a))
-> ((<:.>) (Tagged 'Tail) List a
-> Store
(Identity (TT Covariant Covariant Maybe (Construction Maybe) a))
((<:.>) (Tagged 'Tail) List a))
-> P_Q_T
(->)
Store
Identity
((<:.>) (Tagged 'Tail) List a)
(TT Covariant Covariant Maybe (Construction Maybe) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(<:.>) (Tagged 'Tail) List a
x -> case TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a)
-> ((<:.>) (Tagged 'Tail) List a
-> TT Covariant Covariant Maybe (Construction Maybe) a)
-> (<:.>) (Tagged 'Tail) List a
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Tagged 'Tail (TT Covariant Covariant Maybe (Construction Maybe) a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Tagged 'Tail (TT Covariant Covariant Maybe (Construction Maybe) a)
-> TT Covariant Covariant Maybe (Construction Maybe) a)
-> ((<:.>) (Tagged 'Tail) List a
-> Tagged
'Tail (TT Covariant Covariant Maybe (Construction Maybe) a))
-> (<:.>) (Tagged 'Tail) List a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Tail) List a
-> Tagged
'Tail (TT Covariant Covariant Maybe (Construction Maybe) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run ((<:.>) (Tagged 'Tail) List a
-> (Maybe :. Construction Maybe) := a)
-> (<:.>) (Tagged 'Tail) List a
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! (<:.>) (Tagged 'Tail) List a
x of
Just Construction Maybe a
ns -> TT Covariant Covariant Maybe (Construction Maybe) a
-> (<:.>) (Tagged 'Tail) List a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (TT Covariant Covariant Maybe (Construction Maybe) a
-> (<:.>) (Tagged 'Tail) List a)
-> (Construction Maybe a
-> TT Covariant Covariant Maybe (Construction Maybe) a)
-> Construction Maybe a
-> (<:.>) (Tagged 'Tail) List a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
forall (t :: (* -> *) -> * -> *) (u :: * -> *) a.
(Liftable (->) t, Covariant (->) (->) u) =>
u a -> t u a
lift @(->) (Construction Maybe a -> (<:.>) (Tagged 'Tail) List a)
-> Store
(Identity (TT Covariant Covariant Maybe (Construction Maybe) a))
(Construction Maybe a)
-> Store
(Identity (TT Covariant Covariant Maybe (Construction Maybe) a))
((<:.>) (Tagged 'Tail) List a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- P_Q_T
(->)
Store
Identity
(Construction Maybe a)
(TT Covariant Covariant Maybe (Construction Maybe) a)
-> Construction Maybe a
-> Store
(Identity (TT Covariant Covariant Maybe (Construction Maybe) a))
(Construction Maybe a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
(structure #=@ Substance segment structure)
:= Available segment structure
forall (structure :: * -> *).
(Substructure 'Tail structure, Covariant (->) (->) structure) =>
(structure #=@ Substance 'Tail structure)
:= Available 'Tail structure
sub @Tail) Construction Maybe a
ns
(Maybe :. Construction Maybe) := a
Nothing -> (((:*:)
(Identity (TT Covariant Covariant Maybe (Construction Maybe) a))
:. (->)
(Identity (TT Covariant Covariant Maybe (Construction Maybe) a)))
:= (<:.>) (Tagged 'Tail) List a)
-> Store
(Identity (TT Covariant Covariant Maybe (Construction Maybe) a))
((<:.>) (Tagged 'Tail) List a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:)
(Identity (TT Covariant Covariant Maybe (Construction Maybe) a))
:. (->)
(Identity (TT Covariant Covariant Maybe (Construction Maybe) a)))
:= (<:.>) (Tagged 'Tail) List a)
-> Store
(Identity (TT Covariant Covariant Maybe (Construction Maybe) a))
((<:.>) (Tagged 'Tail) List a))
-> (((:*:)
(Identity (TT Covariant Covariant Maybe (Construction Maybe) a))
:. (->)
(Identity (TT Covariant Covariant Maybe (Construction Maybe) a)))
:= (<:.>) (Tagged 'Tail) List a)
-> Store
(Identity (TT Covariant Covariant Maybe (Construction Maybe) a))
((<:.>) (Tagged 'Tail) List a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! TT Covariant Covariant Maybe (Construction Maybe) a
-> Identity (TT Covariant Covariant Maybe (Construction Maybe) a)
forall a. a -> Identity a
Identity TT Covariant Covariant Maybe (Construction Maybe) a
forall a. Monoid a => a
zero Identity (TT Covariant Covariant Maybe (Construction Maybe) a)
-> (Identity (TT Covariant Covariant Maybe (Construction Maybe) a)
-> (<:.>) (Tagged 'Tail) List a)
-> ((:*:)
(Identity (TT Covariant Covariant Maybe (Construction Maybe) a))
:. (->)
(Identity (TT Covariant Covariant Maybe (Construction Maybe) a)))
:= (<:.>) (Tagged 'Tail) List a
forall s a. s -> a -> s :*: a
:*: TT Covariant Covariant Maybe (Construction Maybe) a
-> (<:.>) (Tagged 'Tail) List a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (TT Covariant Covariant Maybe (Construction Maybe) a
-> (<:.>) (Tagged 'Tail) List a)
-> (Identity (TT Covariant Covariant Maybe (Construction Maybe) a)
-> TT Covariant Covariant Maybe (Construction Maybe) a)
-> Identity (TT Covariant Covariant Maybe (Construction Maybe) a)
-> (<:.>) (Tagged 'Tail) List a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) a. Category m => m a a
identity (TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a)
-> (Identity (TT Covariant Covariant Maybe (Construction Maybe) a)
-> TT Covariant Covariant Maybe (Construction Maybe) a)
-> Identity (TT Covariant Covariant Maybe (Construction Maybe) a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity (TT Covariant Covariant Maybe (Construction Maybe) a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (t :: * -> *) a. Extractable t => t a -> a
extract
linearize :: forall t a . Traversable (->) (->) t => t a -> List a
linearize :: t a -> List a
linearize = ((Maybe :. Construction Maybe) := a) -> List a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
(a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (((Maybe :. Construction Maybe) := a) -> List a)
-> (t a -> (Maybe :. Construction Maybe) := a) -> t a -> List a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (((Maybe :. Construction Maybe) := a)
:*: ((Maybe :. Construction Maybe) := a))
-> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a. Extractable t => t a -> a
extract ((((Maybe :. Construction Maybe) := a)
:*: ((Maybe :. Construction Maybe) := a))
-> (Maybe :. Construction Maybe) := a)
-> (t a
-> ((Maybe :. Construction Maybe) := a)
:*: ((Maybe :. Construction Maybe) := a))
-> t a
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (forall a.
Interpreted (->) (State ((Maybe :. Nonempty List) := a)) =>
State ((Maybe :. Nonempty List) := a) a
-> Primary (State ((Maybe :. Nonempty List) := a)) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run @(->) @(State (Maybe :. Nonempty List := a)) (State
((Maybe :. Construction Maybe) := a)
((Maybe :. Construction Maybe) := a)
-> ((Maybe :. Construction Maybe) := a)
-> ((Maybe :. Construction Maybe) := a)
:*: ((Maybe :. Construction Maybe) := a))
-> ((Maybe :. Construction Maybe) := a)
-> State
((Maybe :. Construction Maybe) := a)
((Maybe :. Construction Maybe) := a)
-> ((Maybe :. Construction Maybe) := a)
:*: ((Maybe :. Construction Maybe) := a)
forall a b c. (a -> b -> c) -> b -> a -> c
% (Maybe :. Construction Maybe) := a
forall a. Maybe a
Nothing) (State
((Maybe :. Construction Maybe) := a)
((Maybe :. Construction Maybe) := a)
-> ((Maybe :. Construction Maybe) := a)
:*: ((Maybe :. Construction Maybe) := a))
-> (t a
-> State
((Maybe :. Construction Maybe) := a)
((Maybe :. Construction Maybe) := a))
-> t a
-> ((Maybe :. Construction Maybe) := a)
:*: ((Maybe :. Construction Maybe) := a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a
-> ((Maybe :. Construction Maybe) := a)
-> (Maybe :. Construction Maybe) := a)
-> t a
-> State
((Maybe :. Construction Maybe) := a)
((Maybe :. Construction Maybe) := a)
forall (t :: * -> *) s (u :: * -> *) a.
(Traversable (->) (->) t, Memorable s u) =>
(a -> s -> s) -> t a -> u s
fold (Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall a. a -> Maybe a
Just (Construction Maybe a -> (Maybe :. Construction Maybe) := a)
-> (a
-> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a)
-> a
-> ((Maybe :. Construction Maybe) := a)
-> (Maybe :. Construction Maybe) := a
forall (target :: * -> * -> *) (v :: * -> * -> *) a c d b.
(Covariant (->) target (v a), Semigroupoid v) =>
v c d -> target (v a (v b c)) (v a (v b d))
-.#..- a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct)
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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Construction Maybe a -> Maybe (Construction Maybe a)
forall a. a -> Maybe a
Just Construction Maybe a
ys
Construct a
x (Just Construction Maybe a
xs) + Construction Maybe a
ys = a -> Maybe (Construction Maybe a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Maybe (Construction Maybe a) -> Construction Maybe a)
-> (Construction Maybe a -> Maybe (Construction Maybe a))
-> Construction Maybe a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Maybe a -> Maybe (Construction Maybe a)
forall a. a -> Maybe a
Just (Construction Maybe a -> Construction Maybe a)
-> Construction Maybe a -> Construction Maybe a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \Predicate a
p ->
Predicate a -> a -> Boolean
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run Predicate a
p a
x Boolean -> Maybe a -> Maybe a -> Maybe a
forall clause a. Conditional clause => clause -> a -> a -> a
? a -> Maybe a
forall a. a -> Maybe a
Just a
x (Maybe a -> Maybe a) -> Maybe a -> Maybe a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! forall a2.
Morphed
('Find 'Element)
(Nonempty List)
((Predicate <:.:> Maybe) := (->)) =>
Predicate a2 -> Nonempty List a2 -> Maybe a2
forall a1 (mod :: a1) (struct :: * -> *) (result :: * -> *) a2.
Morphed ('Find mod) struct ((Predicate <:.:> result) := (->)) =>
Predicate a2 -> struct a2 -> result a2
find @Element @(Nonempty List) @Maybe (Predicate a -> Construction Maybe a -> Maybe a)
-> Predicate a -> Construction Maybe a -> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Predicate a
p (Construction Maybe a -> Maybe a)
-> ((Maybe :. Construction Maybe) := a) -> Maybe a
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
=<< (Maybe :. Construction Maybe) := a
xs
instance Morphable (Into List) (Construction Maybe) where
type Morphing (Into List) (Construction Maybe) = List
morphing :: (<::>) (Tagged ('Into List)) (Construction Maybe) a
-> Morphing ('Into List) (Construction Maybe) a
morphing = Construction Maybe a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Maybe a
-> TT Covariant Covariant Maybe (Construction Maybe) a)
-> ((<::>) (Tagged ('Into List)) (Construction Maybe) a
-> Construction Maybe a)
-> (<::>) (Tagged ('Into List)) (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>) (Tagged ('Into List)) (Construction Maybe) a
-> Construction Maybe a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph
instance Morphable (Into List) (Construction Maybe <::> Maybe) where
type Morphing (Into List) (Construction Maybe <::> Maybe) = List
morphing :: (<::>) (Tagged ('Into List)) (Construction Maybe <::> Maybe) a
-> Morphing ('Into List) (Construction Maybe <::> Maybe) a
morphing (<::>) (Tagged ('Into List)) (Construction Maybe <::> Maybe) a
nonempty_list_with_maybe_elements = case (<::>) (Construction Maybe) Maybe a
-> (Construction Maybe :. Maybe) := a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run ((<::>) (Construction Maybe) Maybe a
-> (Construction Maybe :. Maybe) := a)
-> ((<::>) (Tagged ('Into List)) (Construction Maybe <::> Maybe) a
-> (<::>) (Construction Maybe) Maybe a)
-> (<::>) (Tagged ('Into List)) (Construction Maybe <::> Maybe) a
-> (Construction Maybe :. Maybe) := a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>) (Tagged ('Into List)) (Construction Maybe <::> Maybe) a
-> (<::>) (Construction Maybe) Maybe a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph ((<::>) (Tagged ('Into List)) (Construction Maybe <::> Maybe) a
-> (Construction Maybe :. Maybe) := a)
-> (<::>) (Tagged ('Into List)) (Construction Maybe <::> Maybe) a
-> (Construction Maybe :. Maybe) := a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<::>) (Tagged ('Into List)) (Construction Maybe <::> Maybe) a
nonempty_list_with_maybe_elements of
Construct (Just a
x) (Just (Construction Maybe :. Maybe) := a
xs) -> a :=:=> List
forall k (mod :: k) (struct :: * -> *) a.
Morphed mod struct ((Identity <:.:> struct) := (->)) =>
a :=:=> struct
item @Push a
x (TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<::>) (Construction Maybe) Maybe a
-> Morphing ('Into List) (Construction Maybe <::> Maybe) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @List (((Construction Maybe :. Maybe) := a)
-> (<::>) (Construction Maybe) Maybe a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
(a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT @Covariant @Covariant (Construction Maybe :. Maybe) := a
xs)
Construct (Just a
x) Maybe ((Construction Maybe :. Maybe) := a)
Nothing -> a -> TT Covariant Covariant Maybe (Construction Maybe) a
forall (t :: * -> *) a. Pointable t => a -> t a
point a
x
Construct Maybe a
Nothing (Just (Construction Maybe :. Maybe) := a
xs) -> (<::>) (Construction Maybe) Maybe a
-> Morphing ('Into List) (Construction Maybe <::> Maybe) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @List (((Construction Maybe :. Maybe) := a)
-> (<::>) (Construction Maybe) Maybe a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
(a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT @Covariant @Covariant (Construction Maybe :. Maybe) := a
xs)
Construct Maybe a
Nothing Maybe ((Construction Maybe :. Maybe) := a)
Nothing -> Morphing ('Into List) (Construction Maybe <::> Maybe) a
forall (t :: * -> *) a. Emptiable t => t a
empty
instance Morphable Push (Construction Maybe) where
type Morphing Push (Construction Maybe) = 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall a. a -> Maybe a
Just Construction Maybe a
xs
instance Substructure Root (Construction Maybe) where
type Available Root (Construction Maybe) = Identity
type Substance Root (Construction Maybe) = Identity
substructure :: Lens
(Available 'Root (Construction Maybe))
((<:.>) (Tagged 'Root) (Construction Maybe) a)
(Substance 'Root (Construction Maybe) a)
substructure = ((<:.>) (Tagged 'Root) (Construction Maybe) a -> Identity a)
-> ((<:.>) (Tagged 'Root) (Construction Maybe) a
-> Identity a -> (<:.>) (Tagged 'Root) (Construction Maybe) a)
-> Lens
Identity
((<:.>) (Tagged 'Root) (Construction Maybe) a)
(Identity a)
forall k (result :: k). Impliable result => Arguments result
imply @(Convex Lens _ _) (a -> Identity a
forall a. a -> Identity a
Identity (a -> Identity a)
-> ((<:.>) (Tagged 'Root) (Construction Maybe) a -> a)
-> (<:.>) (Tagged 'Root) (Construction Maybe) a
-> Identity a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Maybe a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Construction Maybe a -> a)
-> ((<:.>) (Tagged 'Root) (Construction Maybe) a
-> Construction Maybe a)
-> (<:.>) (Tagged 'Root) (Construction Maybe) a
-> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Root) (Construction Maybe) a
-> Construction Maybe a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower)
(\(<:.>) (Tagged 'Root) (Construction Maybe) a
source Identity a
target -> Construction Maybe a
-> (<:.>) (Tagged 'Root) (Construction Maybe) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (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)
-> a
-> ((Maybe :. Construction Maybe) := a)
-> Construction Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Identity a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Identity a
target (((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 (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct ((<:.>) (Tagged 'Root) (Construction Maybe) a
-> Construction Maybe a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged 'Root) (Construction Maybe) a
source)))
instance Substructure Tail (Construction Maybe) where
type Available Tail (Construction Maybe) = Identity
type Substance Tail (Construction Maybe) = List
substructure :: Lens
(Available 'Tail (Construction Maybe))
((<:.>) (Tagged 'Tail) (Construction Maybe) a)
(Substance 'Tail (Construction Maybe) a)
substructure = ((<:.>) (Tagged 'Tail) (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a)
-> ((<:.>) (Tagged 'Tail) (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> (<:.>) (Tagged 'Tail) (Construction Maybe) a)
-> Lens
Identity
((<:.>) (Tagged 'Tail) (Construction Maybe) a)
(TT Covariant Covariant Maybe (Construction Maybe) a)
forall k (result :: k). Impliable result => Arguments result
imply @(Convex Lens _ _) (((Maybe :. Construction Maybe) := a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
(a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (((Maybe :. Construction Maybe) := a)
-> TT Covariant Covariant Maybe (Construction Maybe) a)
-> ((<:.>) (Tagged 'Tail) (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a)
-> (<:.>) (Tagged 'Tail) (Construction Maybe) a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. 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 'Tail) (Construction Maybe) a
-> Construction Maybe a)
-> (<:.>) (Tagged 'Tail) (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Tail) (Construction Maybe) a
-> Construction Maybe a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower)
(\(<:.>) (Tagged 'Tail) (Construction Maybe) a
source TT Covariant Covariant Maybe (Construction Maybe) a
target -> Construction Maybe a
-> (<:.>) (Tagged 'Tail) (Construction Maybe) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (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)
-> a
-> ((Maybe :. Construction Maybe) := a)
-> Construction Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Construction Maybe a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract ((<:.>) (Tagged 'Tail) (Construction Maybe) a
-> Construction Maybe a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged 'Tail) (Construction Maybe) a
source) (((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)
# TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run TT Covariant Covariant Maybe (Construction Maybe) a
target))
type instance Combinative List = Comprehension Maybe
instance Zippable List where
type Breadcrumbs List = (Reverse List <:.:> List := (:*:))
instance {-# OVERLAPS #-} Traversable (->) (->) (Tape List) where
a -> u b
f <<- :: (a -> u b) -> Tape List a -> u (Tape List b)
<<- T_U (Identity a
x :*: T_U (Reverse List a
left :*: List a
right)) = (\Reverse List b
past' b
x' Reverse List b
left' -> Identity b -> (:=) (Reverse List <:.:> List) (:*:) b -> Tape List b
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (b -> Identity b
forall a. a -> Identity a
Identity b
x') ((:=) (Reverse List <:.:> List) (:*:) b -> Tape List b)
-> (:=) (Reverse List <:.:> List) (:*:) b -> Tape List b
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Reverse List b
-> TT Covariant Covariant Maybe (Construction Maybe) b
-> (:=) (Reverse List <:.:> List) (:*:) b
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Reverse List b
-> TT Covariant Covariant Maybe (Construction Maybe) b
-> (:=) (Reverse List <:.:> List) (:*:) b)
-> Reverse List b
-> TT Covariant Covariant Maybe (Construction Maybe) b
-> (:=) (Reverse List <:.:> List) (:*:) b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Reverse List b
left' (TT Covariant Covariant Maybe (Construction Maybe) b
-> (:=) (Reverse List <:.:> List) (:*:) b)
-> TT Covariant Covariant Maybe (Construction Maybe) b
-> (:=) (Reverse List <:.:> List) (:*:) b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Reverse List b
-> TT Covariant Covariant Maybe (Construction Maybe) b
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run Reverse List b
past')
(Reverse List b -> b -> Reverse List b -> Tape List b)
-> u (Reverse List b) -> u (b -> Reverse List b -> Tape List b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- a -> u b
f (a -> u b) -> Reverse List a -> u (Reverse List b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
Monoidal (Straight source) (Straight target) (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<<- List a -> Reverse List a
forall k (t :: k -> *) (a :: k). t a -> Reverse t a
Reverse List a
right u (b -> Reverse List b -> Tape List b)
-> u b -> u (Reverse List b -> Tape List b)
forall (t :: * -> *) a b.
(Covariant (->) (->) t,
Semimonoidal (Straight (->)) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*- a -> u b
f a
x u (Reverse List b -> Tape List b)
-> u (Reverse List b) -> u (Tape List b)
forall (t :: * -> *) a b.
(Covariant (->) (->) t,
Semimonoidal (Straight (->)) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*- a -> u b
f (a -> u b) -> Reverse List a -> u (Reverse List b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
Monoidal (Straight source) (Straight target) (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<<- Reverse List a
left
instance {-# OVERLAPS #-} Extendable (->) (Tape List) where
Tape List a -> b
f <<= :: (Tape List a -> b) -> Tape List a -> Tape List b
<<= Tape List a
z = let move :: (Tape List a -> (<::>) Maybe (Tape List) a) -> List (Tape List a)
move Tape List a -> (<::>) Maybe (Tape List) a
rtt = ((Maybe :. Construction Maybe) := Tape List a)
-> List (Tape List a)
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
(a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (((Maybe :. Construction Maybe) := Tape List a)
-> List (Tape List a))
-> (Construction Maybe (Tape List a)
-> (Maybe :. Construction Maybe) := Tape List a)
-> Construction Maybe (Tape List a)
-> List (Tape List a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Maybe (Tape List a)
-> (Maybe :. Construction Maybe) := Tape List a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct (Construction Maybe (Tape List a) -> List (Tape List a))
-> Construction Maybe (Tape List a) -> List (Tape List a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! (<::>) Maybe (Tape List) a -> Maybe (Tape List a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run ((<::>) Maybe (Tape List) a -> Maybe (Tape List a))
-> (Tape List a -> (<::>) Maybe (Tape List) a)
-> Tape List a
-> Maybe (Tape List a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Tape List a -> (<::>) Maybe (Tape List) a
rtt (Tape List a -> Maybe (Tape List a))
-> Tape List a :=> Construction Maybe
forall (t :: * -> *) a.
Covariant (->) (->) t =>
(a :=> t) -> a :=> Construction t
.-+ Tape List a
z in
Identity b -> (:=) (Reverse List <:.:> List) (:*:) b -> Tape List b
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (b -> Identity b
forall a. a -> Identity a
Identity (b -> Identity b) -> b -> Identity b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Tape List a -> b
f Tape List a
z) ((:=) (Reverse List <:.:> List) (:*:) b -> Tape List b)
-> (:=) (Reverse List <:.:> List) (:*:) b -> Tape List b
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Reverse List b -> List b -> (:=) (Reverse List <:.:> List) (:*:) b
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Reverse List b
-> List b -> (:=) (Reverse List <:.:> List) (:*:) b)
-> Reverse List b
-> List b
-> (:=) (Reverse List <:.:> List) (:*:) b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# List b -> Reverse List b
forall k (t :: k -> *) (a :: k). t a -> Reverse t a
Reverse (Tape List a -> b
f (Tape List a -> b) -> List (Tape List a) -> List b
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- (Tape List a -> (<::>) Maybe (Tape List) a) -> List (Tape 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 -> (:=) (Reverse List <:.:> List) (:*:) b)
-> List b -> (:=) (Reverse List <:.:> List) (:*:) b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Tape List a -> b
f (Tape List a -> b) -> List (Tape List a) -> List b
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- (Tape List a -> (<::>) Maybe (Tape List) a) -> List (Tape 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) (Tape List) where
type Morphing (Rotate Left) (Tape List) = Maybe <::> Tape List
morphing :: (<::>) (Tagged ('Rotate 'Left)) (Tape List) a
-> Morphing ('Rotate 'Left) (Tape List) a
morphing ((<::>) (Tagged ('Rotate 'Left)) (Tape List) a -> Tape List a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> T_U (Identity a
x :*: T_U (Reverse List a
left :*: List a
right))) =
let subtree :: (:=) (Reverse List <:.:> List) (:*:) a
subtree = Reverse List a -> List a -> (:=) (Reverse List <:.:> List) (:*:) a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Reverse List a
-> List a -> (:=) (Reverse List <:.:> List) (:*:) a)
-> Reverse List a
-> List a
-> (:=) (Reverse List <:.:> List) (:*:) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# List a -> Reverse List a
forall k (t :: k -> *) (a :: k). t a -> Reverse t a
Reverse (forall e r. Gettable (Convex Lens) => Getting (Convex Lens) e r
forall k (i :: k) e r. Gettable i => Getting i e r
get @(Convex Lens) (Lens Identity (List a) (List a) -> List a -> List a)
-> Lens Identity (List a) (List a) -> List a -> List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
(structure #=@ Substance segment structure)
:= Available segment structure
forall (structure :: * -> *).
(Substructure 'Tail structure, Covariant (->) (->) structure) =>
(structure #=@ Substance 'Tail structure)
:= Available 'Tail structure
sub @Tail (List a -> List a) -> List a -> List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# List a
left) (List a -> (:=) (Reverse List <:.:> List) (:*:) a)
-> List a -> (:=) (Reverse List <:.:> List) (:*:) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# a :=:=> List
forall k (mod :: k) (struct :: * -> *) a.
Morphed mod struct ((Identity <:.:> struct) := (->)) =>
a :=:=> struct
item @Push a
x List a
right in
((Maybe :. Tape List) := a)
-> TT Covariant Covariant Maybe (Tape List) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
(a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (((Maybe :. Tape List) := a)
-> TT Covariant Covariant Maybe (Tape List) a)
-> ((Maybe :. Tape List) := a)
-> TT Covariant Covariant Maybe (Tape List) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! (Identity a -> (:=) (Reverse List <:.:> List) (:*:) a -> Tape List a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Identity a
-> (:=) (Reverse List <:.:> List) (:*:) a -> Tape List a)
-> (Identity a -> Identity a)
-> Identity a
-> (:=) (Reverse List <:.:> List) (:*:) a
-> Tape List a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> Identity a
forall a. a -> Identity a
Identity (a -> Identity a) -> (Identity a -> a) -> Identity a -> Identity a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract) (Identity a
-> (:=) (Reverse List <:.:> List) (:*:) a -> Tape List a)
-> (:=) (Reverse List <:.:> List) (:*:) a
-> Identity a
-> Tape List a
forall a b c. (a -> b -> c) -> b -> a -> c
% (:=) (Reverse List <:.:> List) (:*:) a
subtree (Identity a -> Tape List a)
-> Maybe (Identity a) -> (Maybe :. Tape List) := a
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- Lens Maybe (List a) (Identity a) -> List a -> Maybe (Identity a)
forall k (i :: k) e r. Gettable i => Getting i e r
get @(Obscure Lens) (forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
(structure #=@ Substance segment structure)
:= Available segment structure
forall (structure :: * -> *).
(Substructure 'Root structure, Covariant (->) (->) structure) =>
(structure #=@ Substance 'Root structure)
:= Available 'Root structure
sub @Root) List a
left
instance Morphable (Rotate Right) (Tape List) where
type Morphing (Rotate Right) (Tape List) = Maybe <::> Tape List
morphing :: (<::>) (Tagged ('Rotate 'Right)) (Tape List) a
-> Morphing ('Rotate 'Right) (Tape List) a
morphing ((<::>) (Tagged ('Rotate 'Right)) (Tape List) a -> Tape List a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> T_U (Identity a
x :*: T_U (Reverse List a
left :*: List a
right))) =
let subtree :: (:=) (Reverse List <:.:> List) (:*:) a
subtree = Reverse List a -> List a -> (:=) (Reverse List <:.:> List) (:*:) a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Reverse List a
-> List a -> (:=) (Reverse List <:.:> List) (:*:) a)
-> Reverse List a
-> List a
-> (:=) (Reverse List <:.:> List) (:*:) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# List a -> Reverse List a
forall k (t :: k -> *) (a :: k). t a -> Reverse t a
Reverse (a :=:=> List
forall k (mod :: k) (struct :: * -> *) a.
Morphed mod struct ((Identity <:.:> struct) := (->)) =>
a :=:=> struct
item @Push a
x List a
left) (List a -> (:=) (Reverse List <:.:> List) (:*:) a)
-> List a -> (:=) (Reverse List <:.:> List) (:*:) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Lens Identity (List a) (List a) -> List a -> List a
forall k (i :: k) e r. Gettable i => Getting i e r
get @(Convex Lens) (forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
(structure #=@ Substance segment structure)
:= Available segment structure
forall (structure :: * -> *).
(Substructure 'Tail structure, Covariant (->) (->) structure) =>
(structure #=@ Substance 'Tail structure)
:= Available 'Tail structure
sub @Tail) List a
right in
((Maybe :. Tape List) := a)
-> TT Covariant Covariant Maybe (Tape List) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
(a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (((Maybe :. Tape List) := a)
-> TT Covariant Covariant Maybe (Tape List) a)
-> ((Maybe :. Tape List) := a)
-> TT Covariant Covariant Maybe (Tape List) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Identity a -> (:=) (Reverse List <:.:> List) (:*:) a -> Tape List a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Identity a
-> (:=) (Reverse List <:.:> List) (:*:) a -> Tape List a)
-> (:=) (Reverse List <:.:> List) (:*:) a
-> Identity a
-> Tape List a
forall a b c. (a -> b -> c) -> b -> a -> c
% (:=) (Reverse List <:.:> List) (:*:) a
subtree (Identity a -> Tape List a)
-> Maybe (Identity a) -> (Maybe :. Tape List) := a
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- Lens Maybe (List a) (Identity a) -> List a -> Maybe (Identity a)
forall k (i :: k) e r. Gettable i => Getting i e r
get @(Obscure Lens) (forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
(structure #=@ Substance segment structure)
:= Available segment structure
forall (structure :: * -> *).
(Substructure 'Root structure, Covariant (->) (->) structure) =>
(structure #=@ Substance 'Root structure)
:= Available 'Root structure
sub @Root) List a
right
instance Morphable (Rotate Left) (Turnover (Tape List)) where
type Morphing (Rotate Left) (Turnover (Tape List)) = Turnover (Tape List)
morphing :: (<::>) (Tagged ('Rotate 'Left)) (Turnover (Tape List)) a
-> Morphing ('Rotate 'Left) (Turnover (Tape List)) a
morphing s :: (<::>) (Tagged ('Rotate 'Left)) (Turnover (Tape List)) a
s@((<::>) (Tagged ('Rotate 'Left)) (Turnover (Tape List)) a
-> Turnover (Tape List) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Turnover (T_U (Identity a
x :*: T_U (Reverse List a
left :*: List a
right)))) =
(T_U
Covariant
Covariant
(:*:)
Identity
((Reverse List <:.:> List) := (:*:))
a
-> Turnover (Tape List) a)
-> Turnover (Tape List) a
-> Maybe
(T_U
Covariant
Covariant
(:*:)
Identity
((Reverse List <:.:> List) := (:*:))
a)
-> Turnover (Tape List) a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve @(Tape List _) T_U
Covariant
Covariant
(:*:)
Identity
((Reverse List <:.:> List) := (:*:))
a
-> Turnover (Tape List) a
forall k (t :: k -> *) (a :: k). t a -> Turnover t a
Turnover (Turnover (Tape List) a
-> Maybe
(T_U
Covariant
Covariant
(:*:)
Identity
((Reverse List <:.:> List) := (:*:))
a)
-> Turnover (Tape List) a)
-> Turnover (Tape List) a
-> Maybe
(T_U
Covariant
Covariant
(:*:)
Identity
((Reverse List <:.:> List) := (:*:))
a)
-> Turnover (Tape List) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<::>) (Tagged ('Rotate 'Left)) (Turnover (Tape List)) a
-> Turnover (Tape List) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph (<::>) (Tagged ('Rotate 'Left)) (Turnover (Tape List)) a
s (Maybe
(T_U
Covariant
Covariant
(:*:)
Identity
((Reverse List <:.:> List) := (:*:))
a)
-> Turnover (Tape List) a)
-> Maybe
(T_U
Covariant
Covariant
(:*:)
Identity
((Reverse List <:.:> List) := (:*:))
a)
-> Turnover (Tape List) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! (a
-> Nonempty List a
-> T_U
Covariant
Covariant
(:*:)
Identity
((Reverse List <:.:> List) := (:*:))
a
forall a. a -> Nonempty List a -> Tape List a
rotate_over a
x (Construction Maybe a
-> T_U
Covariant
Covariant
(:*:)
Identity
((Reverse List <:.:> List) := (:*:))
a)
-> Maybe (Construction Maybe a)
-> Maybe
(T_U
Covariant
Covariant
(:*:)
Identity
((Reverse List <:.:> List) := (:*:))
a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- List a -> Maybe (Construction Maybe a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run List a
right) Maybe
(T_U
Covariant
Covariant
(:*:)
Identity
((Reverse List <:.:> List) := (:*:))
a)
-> Maybe
(T_U
Covariant
Covariant
(:*:)
Identity
((Reverse List <:.:> List) := (:*:))
a)
-> Maybe
(T_U
Covariant
Covariant
(:*:)
Identity
((Reverse List <:.:> List) := (:*:))
a)
forall (t :: * -> *) a.
(Covariant (->) (->) t,
Semimonoidal (Straight (->)) (:*:) (:+:) t) =>
t a -> t a -> t a
.-+- (a
-> List a
-> Nonempty List a
-> T_U
Covariant
Covariant
(:*:)
Identity
((Reverse List <:.:> List) := (:*:))
a
forall a. a -> List a -> Nonempty List a -> Tape List a
rotate_left a
x List a
right (Construction Maybe a
-> T_U
Covariant
Covariant
(:*:)
Identity
((Reverse List <:.:> List) := (:*:))
a)
-> Maybe (Construction Maybe a)
-> Maybe
(T_U
Covariant
Covariant
(:*:)
Identity
((Reverse List <:.:> List) := (:*:))
a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- List a -> Maybe (Construction Maybe a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run List a
left) where
rotate_left :: a -> List a -> Nonempty List a -> Tape List a
rotate_left :: a -> List a -> Nonempty List a -> Tape List a
rotate_left a
focused List a
rs (Construct lx lxs) = Identity a -> (:=) (Reverse List <:.:> List) (:*:) a -> Tape List a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Identity a
-> (:=) (Reverse List <:.:> List) (:*:) a -> Tape List a)
-> Identity a
-> (:=) (Reverse List <:.:> List) (:*:) a
-> Tape List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# a -> Identity a
forall (t :: * -> *) a. Pointable t => a -> t a
point a
lx
((:=) (Reverse List <:.:> List) (:*:) a -> Tape List a)
-> (:=) (Reverse List <:.:> List) (:*:) a -> Tape List a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Reverse List a -> List a -> (:=) (Reverse List <:.:> List) (:*:) a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Reverse List a
-> List a -> (:=) (Reverse List <:.:> List) (:*:) a)
-> Reverse List a
-> List a
-> (:=) (Reverse List <:.:> List) (:*:) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# List a -> Reverse List a
forall k (t :: k -> *) (a :: k). t a -> Reverse t a
Reverse (((Maybe :. Construction Maybe) := a) -> List a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
(a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (Maybe :. Construction Maybe) := a
lxs) (List a -> (:=) (Reverse List <:.:> List) (:*:) a)
-> List a -> (:=) (Reverse List <:.:> List) (:*:) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# a :=:=> List
forall k (mod :: k) (struct :: * -> *) a.
Morphed mod struct ((Identity <:.:> struct) := (->)) =>
a :=:=> struct
item @Push a
focused List a
rs
rotate_over :: a -> Nonempty List a -> Tape List a
rotate_over :: a -> Nonempty List a -> Tape List a
rotate_over a
focused Nonempty List a
rs = let new_left :: Construction Maybe a
new_left = (Construction Maybe a :*: Construction Maybe ())
-> Construction Maybe a
forall a b. (a :*: b) -> a
attached (a -> State (Construction Maybe a) ()
forall a. a -> State (Nonempty List a) ()
put_over (a -> State (Construction Maybe a) ())
-> Construction Maybe a
-> State (Construction Maybe a) (Construction Maybe ())
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
Monoidal (Straight source) (Straight target) (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<<- Nonempty List a
Construction Maybe a
rs State (Construction Maybe a) (Construction Maybe ())
-> ((->) (Construction Maybe a) :. (:*:) (Construction Maybe a))
:= Construction Maybe ()
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! a -> Construction Maybe a
forall (t :: * -> *) a. Pointable t => a -> t a
point a
focused) in
Identity a -> (:=) (Reverse List <:.:> List) (:*:) a -> Tape List a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Identity a
-> (:=) (Reverse List <:.:> List) (:*:) a -> Tape List a)
-> Identity a
-> (:=) (Reverse List <:.:> List) (:*:) a
-> Tape List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# a -> Identity a
forall (t :: * -> *) a. Pointable t => a -> t a
point (Construction Maybe a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Construction Maybe a
new_left) ((:=) (Reverse List <:.:> List) (:*:) a -> Tape List a)
-> (:=) (Reverse List <:.:> List) (:*:) a -> Tape List a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Reverse List a -> List a -> (:=) (Reverse List <:.:> List) (:*:) a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (List a -> Reverse List a
forall k (t :: k -> *) (a :: k). t a -> Reverse t a
Reverse (List a -> Reverse List a)
-> (((Maybe :. Construction Maybe) := a) -> List a)
-> ((Maybe :. Construction Maybe) := a)
-> Reverse List a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((Maybe :. Construction Maybe) := a) -> List a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
(a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (((Maybe :. Construction Maybe) := a) -> Reverse List a)
-> ((Maybe :. Construction Maybe) := a) -> Reverse List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct Construction Maybe a
new_left) List a
forall (t :: * -> *) a. Emptiable t => t a
empty
put_over :: a -> State (Nonempty List a) ()
put_over :: a -> State (Nonempty List a) ()
put_over = State (Construction Maybe a) (Construction Maybe a)
-> State (Construction Maybe a) ()
forall (t :: * -> *) a. Covariant (->) (->) t => t a -> t ()
void (State (Construction Maybe a) (Construction Maybe a)
-> State (Construction Maybe a) ())
-> (a -> State (Construction Maybe a) (Construction Maybe a))
-> a
-> State (Construction Maybe a) ()
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall e r. Modifiable State => Modification State e r
forall k (i :: k) e r. Modifiable i => Modification i e r
modify @State ((Construction Maybe a -> Construction Maybe a)
-> State (Construction Maybe a) (Construction Maybe a))
-> (a -> Construction Maybe a -> Construction Maybe a)
-> a
-> State (Construction Maybe a) (Construction Maybe a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall k (mod :: k) (struct :: * -> *) a.
Morphed mod struct ((Identity <:.:> struct) := (->)) =>
a :=:=> struct
forall (struct :: * -> *) a.
Morphed 'Push struct ((Identity <:.:> struct) := (->)) =>
a :=:=> struct
item @Push
instance Morphable (Rotate Right) (Turnover (Tape List)) where
type Morphing (Rotate Right) (Turnover (Tape List)) = Turnover (Tape List)
morphing :: (<::>) (Tagged ('Rotate 'Right)) (Turnover (Tape List)) a
-> Morphing ('Rotate 'Right) (Turnover (Tape List)) a
morphing s :: (<::>) (Tagged ('Rotate 'Right)) (Turnover (Tape List)) a
s@((<::>) (Tagged ('Rotate 'Right)) (Turnover (Tape List)) a
-> Turnover (Tape List) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Turnover (T_U (Identity a
x :*: T_U (Reverse List a
left :*: List a
right)))) =
(T_U
Covariant
Covariant
(:*:)
Identity
((Reverse List <:.:> List) := (:*:))
a
-> Turnover (Tape List) a)
-> Turnover (Tape List) a
-> Maybe
(T_U
Covariant
Covariant
(:*:)
Identity
((Reverse List <:.:> List) := (:*:))
a)
-> Turnover (Tape List) a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve @(Tape List _) T_U
Covariant
Covariant
(:*:)
Identity
((Reverse List <:.:> List) := (:*:))
a
-> Turnover (Tape List) a
forall k (t :: k -> *) (a :: k). t a -> Turnover t a
Turnover (Turnover (Tape List) a
-> Maybe
(T_U
Covariant
Covariant
(:*:)
Identity
((Reverse List <:.:> List) := (:*:))
a)
-> Turnover (Tape List) a)
-> Turnover (Tape List) a
-> Maybe
(T_U
Covariant
Covariant
(:*:)
Identity
((Reverse List <:.:> List) := (:*:))
a)
-> Turnover (Tape List) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<::>) (Tagged ('Rotate 'Right)) (Turnover (Tape List)) a
-> Turnover (Tape List) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph (<::>) (Tagged ('Rotate 'Right)) (Turnover (Tape List)) a
s (Maybe
(T_U
Covariant
Covariant
(:*:)
Identity
((Reverse List <:.:> List) := (:*:))
a)
-> Turnover (Tape List) a)
-> Maybe
(T_U
Covariant
Covariant
(:*:)
Identity
((Reverse List <:.:> List) := (:*:))
a)
-> Turnover (Tape List) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! (a
-> Nonempty List a
-> T_U
Covariant
Covariant
(:*:)
Identity
((Reverse List <:.:> List) := (:*:))
a
forall a. a -> Nonempty List a -> Tape List a
rotate_over a
x (Construction Maybe a
-> T_U
Covariant
Covariant
(:*:)
Identity
((Reverse List <:.:> List) := (:*:))
a)
-> Maybe (Construction Maybe a)
-> Maybe
(T_U
Covariant
Covariant
(:*:)
Identity
((Reverse List <:.:> List) := (:*:))
a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- List a -> Maybe (Construction Maybe a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run List a
left) Maybe
(T_U
Covariant
Covariant
(:*:)
Identity
((Reverse List <:.:> List) := (:*:))
a)
-> Maybe
(T_U
Covariant
Covariant
(:*:)
Identity
((Reverse List <:.:> List) := (:*:))
a)
-> Maybe
(T_U
Covariant
Covariant
(:*:)
Identity
((Reverse List <:.:> List) := (:*:))
a)
forall (t :: * -> *) a.
(Covariant (->) (->) t,
Semimonoidal (Straight (->)) (:*:) (:+:) t) =>
t a -> t a -> t a
.-+- (a
-> List a
-> Nonempty List a
-> T_U
Covariant
Covariant
(:*:)
Identity
((Reverse List <:.:> List) := (:*:))
a
forall a. a -> List a -> Nonempty List a -> Tape List a
rotate_right a
x List a
left (Construction Maybe a
-> T_U
Covariant
Covariant
(:*:)
Identity
((Reverse List <:.:> List) := (:*:))
a)
-> Maybe (Construction Maybe a)
-> Maybe
(T_U
Covariant
Covariant
(:*:)
Identity
((Reverse List <:.:> List) := (:*:))
a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- List a -> Maybe (Construction Maybe a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run List a
right) where
rotate_right :: a -> List a -> Nonempty List a -> Tape List a
rotate_right :: a -> List a -> Nonempty List a -> Tape List a
rotate_right a
focused List a
ls (Construct rx rxs) = Identity a -> (:=) (Reverse List <:.:> List) (:*:) a -> Tape List a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Identity a
-> (:=) (Reverse List <:.:> List) (:*:) a -> Tape List a)
-> Identity a
-> (:=) (Reverse List <:.:> List) (:*:) a
-> Tape List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# a -> Identity a
forall (t :: * -> *) a. Pointable t => a -> t a
point a
rx
((:=) (Reverse List <:.:> List) (:*:) a -> Tape List a)
-> (:=) (Reverse List <:.:> List) (:*:) a -> Tape List a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Reverse List a -> List a -> (:=) (Reverse List <:.:> List) (:*:) a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Reverse List a
-> List a -> (:=) (Reverse List <:.:> List) (:*:) a)
-> Reverse List a
-> List a
-> (:=) (Reverse List <:.:> List) (:*:) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# List a -> Reverse List a
forall k (t :: k -> *) (a :: k). t a -> Reverse t a
Reverse (a :=:=> List
forall k (mod :: k) (struct :: * -> *) a.
Morphed mod struct ((Identity <:.:> struct) := (->)) =>
a :=:=> struct
item @Push a
focused List a
ls) (List a -> (:=) (Reverse List <:.:> List) (:*:) a)
-> List a -> (:=) (Reverse List <:.:> List) (:*:) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# ((Maybe :. Construction Maybe) := a) -> List a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
(a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (Maybe :. Construction Maybe) := a
rxs
rotate_over :: a -> Nonempty List a -> Tape List a
rotate_over :: a -> Nonempty List a -> Tape List a
rotate_over a
focused Nonempty List a
ls = let new_right :: Construction Maybe a
new_right = (Construction Maybe a :*: Construction Maybe ())
-> Construction Maybe a
forall a b. (a :*: b) -> a
attached (a -> State (Construction Maybe a) ()
forall a. a -> State (Nonempty List a) ()
put_over (a -> State (Construction Maybe a) ())
-> Construction Maybe a
-> State (Construction Maybe a) (Construction Maybe ())
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
Monoidal (Straight source) (Straight target) (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<<- Nonempty List a
Construction Maybe a
ls State (Construction Maybe a) (Construction Maybe ())
-> ((->) (Construction Maybe a) :. (:*:) (Construction Maybe a))
:= Construction Maybe ()
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! a -> Construction Maybe a
forall (t :: * -> *) a. Pointable t => a -> t a
point a
focused) in
Identity a -> (:=) (Reverse List <:.:> List) (:*:) a -> Tape List a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Identity a
-> (:=) (Reverse List <:.:> List) (:*:) a -> Tape List a)
-> Identity a
-> (:=) (Reverse List <:.:> List) (:*:) a
-> Tape List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# a -> Identity a
forall (t :: * -> *) a. Pointable t => a -> t a
point (Construction Maybe a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Construction Maybe a
new_right) ((:=) (Reverse List <:.:> List) (:*:) a -> Tape List a)
-> (:=) (Reverse List <:.:> List) (:*:) a -> Tape List a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Reverse List a
-> TT Covariant Covariant Maybe (Construction Maybe) a
-> (:=) (Reverse List <:.:> List) (:*:) a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (TT Covariant Covariant Maybe (Construction Maybe) a
-> Reverse List a
forall k (t :: k -> *) (a :: k). t a -> Reverse t a
Reverse TT Covariant Covariant Maybe (Construction Maybe) a
forall (t :: * -> *) a. Emptiable t => t a
empty) (((Maybe :. Construction Maybe) := a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
(a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (((Maybe :. Construction Maybe) := a)
-> TT Covariant Covariant Maybe (Construction Maybe) a)
-> ((Maybe :. Construction Maybe) := a)
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct Construction Maybe a
new_right)
put_over :: a -> State (Nonempty List a) ()
put_over :: a -> State (Nonempty List a) ()
put_over = State (Construction Maybe a) (Construction Maybe a)
-> State (Construction Maybe a) ()
forall (t :: * -> *) a. Covariant (->) (->) t => t a -> t ()
void (State (Construction Maybe a) (Construction Maybe a)
-> State (Construction Maybe a) ())
-> (a -> State (Construction Maybe a) (Construction Maybe a))
-> a
-> State (Construction Maybe a) ()
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall e r. Modifiable State => Modification State e r
forall k (i :: k) e r. Modifiable i => Modification i e r
modify @State ((Construction Maybe a -> Construction Maybe a)
-> State (Construction Maybe a) (Construction Maybe a))
-> (a -> Construction Maybe a -> Construction Maybe a)
-> a
-> State (Construction Maybe a) (Construction Maybe a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall k (mod :: k) (struct :: * -> *) a.
Morphed mod struct ((Identity <:.:> struct) := (->)) =>
a :=:=> struct
forall (struct :: * -> *) a.
Morphed 'Push struct ((Identity <:.:> struct) := (->)) =>
a :=:=> struct
item @Push
instance Morphable (Into (Tape List)) List where
type Morphing (Into (Tape List)) List = Maybe <::> Tape List
morphing :: (<::>) (Tagged ('Into (Tape List))) List a
-> Morphing ('Into (Tape List)) List a
morphing ((<::>) (Tagged ('Into (Tape List))) List a -> List a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> List a
list) = (forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
forall (struct :: * -> *).
Morphable ('Into (Zipper List)) struct =>
struct ~> Morphing ('Into (Zipper List)) struct
into @(Zipper List) (Construction Maybe a -> Tape List a)
-> Maybe (Construction Maybe a) -> Maybe (Tape List a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-) (Primary List a
-> Primary (TT Covariant Covariant Maybe (Tape List)) a)
-> List a -> TT Covariant Covariant Maybe (Tape List) a
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
m (Primary t a) (Primary u b) -> m (t a) (u b)
||= List a
list
instance Morphable (Into List) (Tape List) where
type Morphing (Into List) (Tape List) = List
morphing :: (<::>) (Tagged ('Into List)) (Tape List) a
-> Morphing ('Into List) (Tape List) a
morphing ((<::>) (Tagged ('Into List)) (Tape List) a -> Tape List a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> T_U (Identity a
x :*: T_U (Reverse List a
left :*: List a
right))) = (List a
:*: TT Covariant Covariant Maybe (Construction Maybe) (List a))
-> List a
forall a b. (a :*: b) -> a
attached ((List a
:*: TT Covariant Covariant Maybe (Construction Maybe) (List a))
-> List a)
-> (List a
:*: TT Covariant Covariant Maybe (Construction Maybe) (List a))
-> List a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! forall a.
Interpreted (->) (State (List a)) =>
State (List a) a -> Primary (State (List a)) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run @(->) @(State _)
# modify @State . item @Push @List <<- right
# item @Push x left
instance Morphable (Into (Comprehension Maybe)) (Tape List) where
type Morphing (Into (Comprehension Maybe)) (Tape List) = Comprehension Maybe
morphing :: (<::>) (Tagged ('Into (Comprehension Maybe))) (Tape List) a
-> Morphing ('Into (Comprehension Maybe)) (Tape List) a
morphing ((<::>) (Tagged ('Into (Comprehension Maybe))) (Tape List) a
-> Tape List a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> T_U (Identity a
x :*: T_U (Reverse List a
left :*: List a
right))) = (Comprehension Maybe a
:*: TT
Covariant
Covariant
Maybe
(Construction Maybe)
(Comprehension Maybe a))
-> Comprehension Maybe a
forall a b. (a :*: b) -> a
attached ((Comprehension Maybe a
:*: TT
Covariant
Covariant
Maybe
(Construction Maybe)
(Comprehension Maybe a))
-> Comprehension Maybe a)
-> (Comprehension Maybe a
:*: TT
Covariant
Covariant
Maybe
(Construction Maybe)
(Comprehension Maybe a))
-> Comprehension Maybe a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! forall a.
Interpreted (->) (State (Comprehension Maybe a)) =>
State (Comprehension Maybe a) a
-> Primary (State (Comprehension Maybe a)) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run @(->) @(State _)
# modify @State . item @Push @(Comprehension Maybe) <<- right
# item @Push x (Comprehension left)
instance Zippable (Construction Maybe) where
type Breadcrumbs (Construction Maybe) = Reverse (Construction Maybe) <:.:> Construction Maybe := (:*:)
instance Morphable (Rotate Left) (Tape (Construction Maybe)) where
type Morphing (Rotate Left) (Tape (Construction Maybe)) =
Maybe <::> (Tape (Construction Maybe))
morphing :: (<::>) (Tagged ('Rotate 'Left)) (Tape (Construction Maybe)) a
-> Morphing ('Rotate 'Left) (Tape (Construction Maybe)) a
morphing ((<::>) (Tagged ('Rotate 'Left)) (Tape (Construction Maybe)) a
-> Tape (Construction Maybe) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> T_U (Identity a
x :*: T_U (Reverse Construction Maybe a
left :*: Construction Maybe a
right))) =
((Maybe :. Tape (Construction Maybe)) := a)
-> TT Covariant Covariant Maybe (Tape (Construction Maybe)) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
(a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (((Maybe :. Tape (Construction Maybe)) := a)
-> TT Covariant Covariant Maybe (Tape (Construction Maybe)) a)
-> ((Maybe :. Tape (Construction Maybe)) := a)
-> TT Covariant Covariant Maybe (Tape (Construction Maybe)) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! (Identity a
:*: (:=)
(Reverse (Construction Maybe) <:.:> Construction Maybe) (:*:) a)
-> Tape (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
:*: (:=)
(Reverse (Construction Maybe) <:.:> Construction Maybe) (:*:) a)
-> Tape (Construction Maybe) a)
-> (Construction Maybe a
-> Identity a
:*: (:=)
(Reverse (Construction Maybe) <:.:> Construction Maybe) (:*:) a)
-> Construction Maybe a
-> Tape (Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a -> Identity a
forall a. a -> Identity a
Identity (Construction Maybe a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Construction Maybe a
left) Identity a
-> (:=)
(Reverse (Construction Maybe) <:.:> Construction Maybe) (:*:) a
-> Identity a
:*: (:=)
(Reverse (Construction Maybe) <:.:> Construction Maybe) (:*:) a
forall s a. s -> a -> s :*: a
:*:) ((:=)
(Reverse (Construction Maybe) <:.:> Construction Maybe) (:*:) a
-> Identity a
:*: (:=)
(Reverse (Construction Maybe) <:.:> Construction Maybe) (:*:) a)
-> (Construction Maybe a
-> (:=)
(Reverse (Construction Maybe) <:.:> Construction Maybe) (:*:) a)
-> Construction Maybe a
-> Identity a
:*: (:=)
(Reverse (Construction Maybe) <:.:> Construction Maybe) (:*:) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Reverse (Construction Maybe) a
-> Construction Maybe a
-> (:=)
(Reverse (Construction Maybe) <:.:> Construction Maybe) (:*:) a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Reverse (Construction Maybe) a
-> Construction Maybe a
-> (:=)
(Reverse (Construction Maybe) <:.:> Construction Maybe) (:*:) a)
-> Construction Maybe a
-> Reverse (Construction Maybe) a
-> (:=)
(Reverse (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
right) (Reverse (Construction Maybe) a
-> (:=)
(Reverse (Construction Maybe) <:.:> Construction Maybe) (:*:) a)
-> (Construction Maybe a -> Reverse (Construction Maybe) a)
-> Construction Maybe a
-> (:=)
(Reverse (Construction Maybe) <:.:> Construction Maybe) (:*:) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Maybe a -> Reverse (Construction Maybe) a
forall k (t :: k -> *) (a :: k). t a -> Reverse t a
Reverse (Construction Maybe a -> Tape (Construction Maybe) a)
-> Maybe (Construction Maybe a)
-> (Maybe :. Tape (Construction Maybe)) := a
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- Construction Maybe a -> Maybe (Construction Maybe a)
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct Construction Maybe a
left
instance Morphable (Rotate Right) (Tape (Construction Maybe)) where
type Morphing (Rotate Right) (Tape (Construction Maybe)) =
Maybe <::> Tape (Construction Maybe)
morphing :: (<::>) (Tagged ('Rotate 'Right)) (Tape (Construction Maybe)) a
-> Morphing ('Rotate 'Right) (Tape (Construction Maybe)) a
morphing ((<::>) (Tagged ('Rotate 'Right)) (Tape (Construction Maybe)) a
-> Tape (Construction Maybe) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> T_U (Identity a
x :*: T_U (Reverse Construction Maybe a
left :*: Construction Maybe a
right))) =
((Maybe :. Tape (Construction Maybe)) := a)
-> TT Covariant Covariant Maybe (Tape (Construction Maybe)) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
(a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (((Maybe :. Tape (Construction Maybe)) := a)
-> TT Covariant Covariant Maybe (Tape (Construction Maybe)) a)
-> ((Maybe :. Tape (Construction Maybe)) := a)
-> TT Covariant Covariant Maybe (Tape (Construction Maybe)) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! (Identity a
:*: (:=)
(Reverse (Construction Maybe) <:.:> Construction Maybe) (:*:) a)
-> Tape (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
:*: (:=)
(Reverse (Construction Maybe) <:.:> Construction Maybe) (:*:) a)
-> Tape (Construction Maybe) a)
-> (Construction Maybe a
-> Identity a
:*: (:=)
(Reverse (Construction Maybe) <:.:> Construction Maybe) (:*:) a)
-> Construction Maybe a
-> Tape (Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a -> Identity a
forall a. a -> Identity a
Identity (Construction Maybe a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Construction Maybe a
right) Identity a
-> (:=)
(Reverse (Construction Maybe) <:.:> Construction Maybe) (:*:) a
-> Identity a
:*: (:=)
(Reverse (Construction Maybe) <:.:> Construction Maybe) (:*:) a
forall s a. s -> a -> s :*: a
:*:) ((:=)
(Reverse (Construction Maybe) <:.:> Construction Maybe) (:*:) a
-> Identity a
:*: (:=)
(Reverse (Construction Maybe) <:.:> Construction Maybe) (:*:) a)
-> (Construction Maybe a
-> (:=)
(Reverse (Construction Maybe) <:.:> Construction Maybe) (:*:) a)
-> Construction Maybe a
-> Identity a
:*: (:=)
(Reverse (Construction Maybe) <:.:> Construction Maybe) (:*:) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Reverse (Construction Maybe) a
-> Construction Maybe a
-> (:=)
(Reverse (Construction Maybe) <:.:> Construction Maybe) (:*:) a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Construction Maybe a -> Reverse (Construction Maybe) a
forall k (t :: k -> *) (a :: k). t a -> Reverse t a
Reverse (Construction Maybe a -> Reverse (Construction Maybe) a)
-> Construction Maybe a -> Reverse (Construction Maybe) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# a :=:=> Construction Maybe
forall k (mod :: k) (struct :: * -> *) a.
Morphed mod struct ((Identity <:.:> struct) := (->)) =>
a :=:=> struct
item @Push a
x Construction Maybe a
left) (Construction Maybe a -> Tape (Construction Maybe) a)
-> Maybe (Construction Maybe a)
-> (Maybe :. Tape (Construction Maybe)) := a
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- Construction Maybe a -> Maybe (Construction Maybe a)
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct Construction Maybe a
right
instance Morphable (Into (Tape List)) (Construction Maybe) where
type Morphing (Into (Tape List)) (Construction Maybe) = Tape List
morphing :: (<::>) (Tagged ('Into (Tape List))) (Construction Maybe) a
-> Morphing ('Into (Tape List)) (Construction Maybe) a
morphing ((<::>) (Tagged ('Into (Tape List))) (Construction Maybe) a
-> Construction Maybe a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Construction Maybe a
ne) = Identity a
-> (:=) (Reverse List <:.:> List) (:*:) a
-> (<:.:>) Identity ((Reverse List <:.:> List) := (:*:)) (:*:) a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Identity a
-> (:=) (Reverse List <:.:> List) (:*:) a
-> (<:.:>) Identity ((Reverse List <:.:> List) := (:*:)) (:*:) a)
-> Identity a
-> (:=) (Reverse List <:.:> List) (:*:) a
-> (<:.:>) Identity ((Reverse 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 (Construction Maybe a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Construction Maybe a
ne) ((:=) (Reverse List <:.:> List) (:*:) a
-> (<:.:>) Identity ((Reverse List <:.:> List) := (:*:)) (:*:) a)
-> (:=) (Reverse List <:.:> List) (:*:) a
-> (<:.:>) Identity ((Reverse List <:.:> List) := (:*:)) (:*:) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Reverse List a -> List a -> (:=) (Reverse List <:.:> List) (:*:) a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Reverse List a
-> List a -> (:=) (Reverse List <:.:> List) (:*:) a)
-> Reverse List a
-> List a
-> (:=) (Reverse List <:.:> List) (:*:) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# List a -> Reverse List a
forall k (t :: k -> *) (a :: k). t a -> Reverse t a
Reverse List a
forall a. Monoid a => a
zero (List a -> (:=) (Reverse List <:.:> List) (:*:) a)
-> List a -> (:=) (Reverse List <:.:> List) (:*:) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (forall e r. Gettable (Convex Lens) => Getting (Convex Lens) e r
forall k (i :: k) e r. Gettable i => Getting i e r
get @(Convex Lens) (Lens Identity (Construction Maybe a) (List a)
-> Construction Maybe a -> List a)
-> Lens Identity (Construction Maybe a) (List a)
-> Construction Maybe a
-> List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
(structure #=@ Substance segment structure)
:= Available segment structure
forall (structure :: * -> *).
(Substructure 'Tail structure, Covariant (->) (->) structure) =>
(structure #=@ Substance 'Tail structure)
:= Available 'Tail structure
sub @Tail (Construction Maybe a -> List a) -> Construction Maybe a -> List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Construction Maybe a
ne)
instance Morphable (Into (Tape List)) (Tape (Construction Maybe)) where
type Morphing (Into (Tape List)) (Tape (Construction Maybe)) = Tape List
morphing :: (<::>) (Tagged ('Into (Tape List))) (Tape (Construction Maybe)) a
-> Morphing ('Into (Tape List)) (Tape (Construction Maybe)) a
morphing ((<::>) (Tagged ('Into (Tape List))) (Tape (Construction Maybe)) a
-> Tape (Construction Maybe) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Tape (Construction Maybe) a
zipper) = ((((Primary (Reverse (Construction Maybe)) a
-> Primary (Reverse List) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Primary (Reverse (Construction Maybe)) a
-> Primary (Reverse List) a)
-> Reverse (Construction Maybe) a -> Reverse List a
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
m (Primary t a) (Primary u b) -> m (t a) (u b)
||=) (Reverse (Construction Maybe) a -> Reverse List a)
-> (Construction Maybe a
-> TT Covariant Covariant Maybe (Construction Maybe) a)
-> (Reverse (Construction Maybe) a -> Reverse List a)
:*: (Construction Maybe a
-> TT Covariant Covariant Maybe (Construction Maybe) a)
forall s a. s -> a -> s :*: a
:*: Construction Maybe a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift ((Reverse (Construction Maybe) a -> Reverse List a)
:*: (Construction Maybe a
-> TT Covariant Covariant Maybe (Construction Maybe) a))
-> (Reverse (Construction Maybe) a :*: Construction Maybe a)
-> Reverse List a
:*: TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) (p :: * -> * -> *) a b c d.
(Covariant m m (p a), Covariant m m (Flip p d),
Interpreted m (Flip p d)) =>
(m a b :*: m c d) -> m (p a c) (p b d)
<-|-<-|-) (Primary
(T_U
Covariant
Covariant
(:*:)
(Reverse (Construction Maybe))
(Construction Maybe))
a
-> Primary ((Reverse List <:.:> List) := (:*:)) a)
-> T_U
Covariant
Covariant
(:*:)
(Reverse (Construction Maybe))
(Construction Maybe)
a
-> T_U Covariant Covariant (:*:) (Reverse List) List a
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
m (Primary t a) (Primary u b) -> m (t a) (u b)
||=) (T_U
Covariant
Covariant
(:*:)
(Reverse (Construction Maybe))
(Construction Maybe)
a
-> T_U Covariant Covariant (:*:) (Reverse List) List a)
-> (Identity a
:*: T_U
Covariant
Covariant
(:*:)
(Reverse (Construction Maybe))
(Construction Maybe)
a)
-> Identity a
:*: T_U Covariant Covariant (:*:) (Reverse List) List a
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-) (Primary (Tape (Construction Maybe)) a -> Primary (Tape List) a)
-> Tape (Construction Maybe) a
-> T_U
Covariant
Covariant
(:*:)
Identity
((Reverse List <:.:> List) := (:*:))
a
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
m (Primary t a) (Primary u b) -> m (t a) (u b)
||= Tape (Construction Maybe) a
zipper
instance Morphable (Into (Tape (Construction Maybe))) (Tape List) where
type Morphing (Into (Tape (Construction Maybe))) (Tape List) =
Maybe <::> Tape (Construction Maybe)
morphing :: (<::>) (Tagged ('Into (Tape (Construction Maybe)))) (Tape List) a
-> Morphing ('Into (Tape (Construction Maybe))) (Tape List) a
morphing ((<::>) (Tagged ('Into (Tape (Construction Maybe)))) (Tape List) a
-> Tape List a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Tape List a
zipper) = let spread :: t (t a) -> t a -> t (Reverse t a :*: a)
spread t (t a)
x t a
y = (\t a
x' a
y' -> t a -> Reverse t a
forall k (t :: k -> *) (a :: k). t a -> Reverse t a
Reverse t a
x' Reverse t a -> a -> Reverse t a :*: a
forall s a. s -> a -> s :*: a
:*: a
y') (t a -> a -> Reverse t a :*: a)
-> t (t a) -> t (a -> Reverse t a :*: a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- t (t a)
x t (a -> Reverse t a :*: a) -> t a -> t (Reverse t a :*: a)
forall (t :: * -> *) a b.
(Covariant (->) (->) t,
Semimonoidal (Straight (->)) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*- t a
y in
((Maybe :. Tape (Construction Maybe)) := a)
-> TT Covariant Covariant Maybe (Tape (Construction Maybe)) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
(a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (((Maybe :. Tape (Construction Maybe)) := a)
-> TT Covariant Covariant Maybe (Tape (Construction Maybe)) a)
-> ((Maybe :. Tape (Construction Maybe)) := a)
-> TT Covariant Covariant Maybe (Tape (Construction Maybe)) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! (Identity a
:*: T_U
Covariant
Covariant
(:*:)
(Reverse (Construction Maybe))
(Construction Maybe)
a)
-> T_U
Covariant
Covariant
(:*:)
Identity
(T_U
Covariant
Covariant
(:*:)
(Reverse (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 ((Identity a
:*: T_U
Covariant
Covariant
(:*:)
(Reverse (Construction Maybe))
(Construction Maybe)
a)
-> T_U
Covariant
Covariant
(:*:)
Identity
(T_U
Covariant
Covariant
(:*:)
(Reverse (Construction Maybe))
(Construction Maybe))
a)
-> ((Reverse (Construction Maybe) a :*: Construction Maybe a)
-> Identity a
:*: T_U
Covariant
Covariant
(:*:)
(Reverse (Construction Maybe))
(Construction Maybe)
a)
-> (Reverse (Construction Maybe) a :*: Construction Maybe a)
-> T_U
Covariant
Covariant
(:*:)
Identity
(T_U
Covariant
Covariant
(:*:)
(Reverse (Construction Maybe))
(Construction Maybe))
a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a -> Identity a
forall a. a -> Identity a
Identity (Tape List a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Tape List a
zipper) Identity a
-> T_U
Covariant
Covariant
(:*:)
(Reverse (Construction Maybe))
(Construction Maybe)
a
-> Identity a
:*: T_U
Covariant
Covariant
(:*:)
(Reverse (Construction Maybe))
(Construction Maybe)
a
forall s a. s -> a -> s :*: a
:*:) (T_U
Covariant
Covariant
(:*:)
(Reverse (Construction Maybe))
(Construction Maybe)
a
-> Identity a
:*: T_U
Covariant
Covariant
(:*:)
(Reverse (Construction Maybe))
(Construction Maybe)
a)
-> ((Reverse (Construction Maybe) a :*: Construction Maybe a)
-> T_U
Covariant
Covariant
(:*:)
(Reverse (Construction Maybe))
(Construction Maybe)
a)
-> (Reverse (Construction Maybe) a :*: Construction Maybe a)
-> Identity a
:*: T_U
Covariant
Covariant
(:*:)
(Reverse (Construction Maybe))
(Construction Maybe)
a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Reverse (Construction Maybe) a :*: Construction Maybe a)
-> T_U
Covariant
Covariant
(:*:)
(Reverse (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 ((Reverse (Construction Maybe) a :*: Construction Maybe a)
-> T_U
Covariant
Covariant
(:*:)
Identity
(T_U
Covariant
Covariant
(:*:)
(Reverse (Construction Maybe))
(Construction Maybe))
a)
-> Maybe (Reverse (Construction Maybe) a :*: Construction Maybe a)
-> (Maybe :. Tape (Construction Maybe)) := a
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- ((((Maybe :. Construction Maybe) := a)
-> ((Maybe :. Construction Maybe) := a)
-> Maybe (Reverse (Construction Maybe) a :*: Construction Maybe a)
forall k (t :: * -> *) (t :: k -> *) (a :: k) a.
(Covariant (->) (->) t,
Semimonoidal (Straight (->)) (:*:) (:*:) t) =>
t (t a) -> t a -> t (Reverse t a :*: a)
spread (((Maybe :. Construction Maybe) := a)
-> ((Maybe :. Construction Maybe) := a)
-> Maybe (Reverse (Construction Maybe) a :*: Construction Maybe a))
-> (((Maybe :. Construction Maybe) := a)
:*: ((Maybe :. Construction Maybe) := a))
-> Maybe (Reverse (Construction Maybe) a :*: Construction Maybe a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) (u :: * -> *) a b.
Adjoint source target t u =>
target a (u b) -> source (t a) b
|-) ((((Maybe :. Construction Maybe) := a)
:*: ((Maybe :. Construction Maybe) := a))
-> Maybe (Reverse (Construction Maybe) a :*: Construction Maybe a))
-> ((Identity a
:*: T_U Covariant Covariant (:*:) (Reverse List) List a)
-> ((Maybe :. Construction Maybe) := a)
:*: ((Maybe :. Construction Maybe) := a))
-> (Identity a
:*: T_U Covariant Covariant (:*:) (Reverse List) List a)
-> Maybe (Reverse (Construction Maybe) a :*: Construction Maybe a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a)
-> (Reverse List a
-> TT Covariant Covariant Maybe (Construction Maybe) a)
-> Reverse List a
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Reverse List a
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Reverse List a -> (Maybe :. Construction Maybe) := a)
-> (TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a)
-> (Reverse List a -> (Maybe :. Construction Maybe) := a)
:*: (TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a)
forall s a. s -> a -> s :*: a
:*: TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run ((Reverse List a -> (Maybe :. Construction Maybe) := a)
:*: (TT Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a))
-> (Reverse List a
:*: TT Covariant Covariant Maybe (Construction Maybe) a)
-> ((Maybe :. Construction Maybe) := a)
:*: ((Maybe :. Construction Maybe) := a)
forall (m :: * -> * -> *) (p :: * -> * -> *) a b c d.
(Covariant m m (p a), Covariant m m (Flip p d),
Interpreted m (Flip p d)) =>
(m a b :*: m c d) -> m (p a c) (p b d)
<-|-<-|-) ((Reverse List a
:*: TT Covariant Covariant Maybe (Construction Maybe) a)
-> ((Maybe :. Construction Maybe) := a)
:*: ((Maybe :. Construction Maybe) := a))
-> ((Identity a
:*: T_U Covariant Covariant (:*:) (Reverse List) List a)
-> Reverse List a
:*: TT Covariant Covariant Maybe (Construction Maybe) a)
-> (Identity a
:*: T_U Covariant Covariant (:*:) (Reverse List) List a)
-> ((Maybe :. Construction Maybe) := a)
:*: ((Maybe :. Construction Maybe) := a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. T_U Covariant Covariant (:*:) (Reverse List) List a
-> Reverse List a
:*: TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (T_U Covariant Covariant (:*:) (Reverse List) List a
-> Reverse List a
:*: TT Covariant Covariant Maybe (Construction Maybe) a)
-> ((Identity a
:*: T_U Covariant Covariant (:*:) (Reverse List) List a)
-> T_U Covariant Covariant (:*:) (Reverse List) List a)
-> (Identity a
:*: T_U Covariant Covariant (:*:) (Reverse List) List a)
-> Reverse List a
:*: TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Identity a
:*: T_U Covariant Covariant (:*:) (Reverse List) List a)
-> T_U Covariant Covariant (:*:) (Reverse List) List a
forall (t :: * -> *) a. Extractable t => t a -> a
extract ((Identity a
:*: T_U Covariant Covariant (:*:) (Reverse List) List a)
-> Maybe (Reverse (Construction Maybe) a :*: Construction Maybe a))
-> (Identity a
:*: T_U Covariant Covariant (:*:) (Reverse List) List a)
-> Maybe (Reverse (Construction Maybe) a :*: Construction Maybe a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Tape List a
-> Identity a
:*: T_U Covariant Covariant (:*:) (Reverse List) List a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run Tape List a
zipper)
instance Morphable (Into (Construction Maybe)) (Tape (Construction Maybe)) where
type Morphing (Into (Construction Maybe)) (Tape (Construction Maybe)) = Construction Maybe
morphing :: (<::>)
(Tagged ('Into (Construction Maybe))) (Tape (Construction Maybe)) a
-> Morphing
('Into (Construction Maybe)) (Tape (Construction Maybe)) a
morphing ((<::>)
(Tagged ('Into (Construction Maybe))) (Tape (Construction Maybe)) a
-> Tape (Construction Maybe) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> T_U (Identity a
x :*: T_U (Reverse Construction Maybe a
left :*: Construction Maybe a
right))) = (Construction Maybe a
:*: Construction Maybe (Construction Maybe a))
-> Construction Maybe a
forall a b. (a :*: b) -> a
attached ((Construction Maybe a
:*: Construction Maybe (Construction Maybe a))
-> Construction Maybe a)
-> (Construction Maybe a
:*: Construction Maybe (Construction Maybe a))
-> Construction Maybe a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! forall a.
Interpreted (->) (State (Construction Maybe a)) =>
State (Construction Maybe a) a
-> Primary (State (Construction Maybe a)) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run @(->) @(State _)
# modify @State . item @Push @(Nonempty List) <<- right
# item @Push x left
instance Morphable (Into List) (Tape (Construction Maybe)) where
type Morphing (Into List) (Tape (Construction Maybe)) = List
morphing :: (<::>) (Tagged ('Into List)) (Tape (Construction Maybe)) a
-> Morphing ('Into List) (Tape (Construction Maybe)) a
morphing ((<::>) (Tagged ('Into List)) (Tape (Construction Maybe)) a
-> Tape (Construction Maybe) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> T_U (Identity a
x :*: T_U (Reverse Construction Maybe a
left :*: Construction Maybe a
right))) = (TT Covariant Covariant Maybe (Construction Maybe) a
:*: Construction
Maybe (TT Covariant Covariant Maybe (Construction Maybe) a))
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall a b. (a :*: b) -> a
attached ((TT Covariant Covariant Maybe (Construction Maybe) a
:*: Construction
Maybe (TT Covariant Covariant Maybe (Construction Maybe) a))
-> TT Covariant Covariant Maybe (Construction Maybe) a)
-> (TT Covariant Covariant Maybe (Construction Maybe) a
:*: Construction
Maybe (TT Covariant Covariant Maybe (Construction Maybe) a))
-> TT Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! forall a.
Interpreted
(->)
(State (TT Covariant Covariant Maybe (Construction Maybe) a)) =>
State (TT Covariant Covariant Maybe (Construction Maybe) a) a
-> Primary
(State (TT Covariant Covariant Maybe (Construction Maybe) a)) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run @(->) @(State _)
# modify @State . item @Push @List <<- right
# item @Push x (lift left)
instance Zippable (Comprehension Maybe) where
type Breadcrumbs (Comprehension Maybe) = (Comprehension Maybe <:.:> Comprehension Maybe := (:*:))
instance Setoid key => Morphable (Lookup Key) (Prefixed List key) where
type Morphing (Lookup Key) (Prefixed List key) = (->) key <::> Maybe
morphing :: (<::>) (Tagged ('Lookup 'Key)) (Prefixed List key) a
-> Morphing ('Lookup 'Key) (Prefixed List key) a
morphing (Prefixed List key a
-> TT Covariant Covariant Maybe (Construction Maybe) (key :*: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Prefixed List key a
-> TT Covariant Covariant Maybe (Construction Maybe) (key :*: a))
-> ((<::>) (Tagged ('Lookup 'Key)) (Prefixed List key) a
-> Prefixed List key a)
-> (<::>) (Tagged ('Lookup 'Key)) (Prefixed List key) a
-> TT Covariant Covariant Maybe (Construction Maybe) (key :*: a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>) (Tagged ('Lookup 'Key)) (Prefixed List key) a
-> Prefixed List key a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> TT Covariant Covariant Maybe (Construction Maybe) (key :*: a)
list) = (((->) key :. Maybe) := a)
-> TT Covariant Covariant ((->) key) Maybe a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
(a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT ((((->) key :. Maybe) := a)
-> TT Covariant Covariant ((->) key) Maybe a)
-> (((->) key :. Maybe) := a)
-> TT Covariant Covariant ((->) key) Maybe a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \key
key -> key -> Prefixed (Construction Maybe) key a -> Maybe a
forall a1 (mod :: a1) key (struct :: * -> *) a2.
Morphed ('Lookup mod) struct ((->) key <::> Maybe) =>
key -> struct a2 -> Maybe a2
lookup @Key key
key (Prefixed (Construction Maybe) key a -> Maybe a)
-> Maybe (Prefixed (Construction Maybe) key a) -> Maybe a
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
=<< ((Construction Maybe :. (:*:) key) := a)
-> Prefixed (Construction Maybe) key a
forall (t :: * -> *) k a. ((t :. (:*:) k) := a) -> Prefixed t k a
Prefixed (((Construction Maybe :. (:*:) key) := a)
-> Prefixed (Construction Maybe) key a)
-> Maybe ((Construction Maybe :. (:*:) key) := a)
-> Maybe (Prefixed (Construction Maybe) key a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- TT Covariant Covariant Maybe (Construction Maybe) (key :*: a)
-> Maybe ((Construction Maybe :. (:*:) key) := a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run TT Covariant Covariant Maybe (Construction Maybe) (key :*: a)
list
instance Setoid key => Morphable (Lookup Key) (Prefixed (Construction Maybe) key) where
type Morphing (Lookup Key) (Prefixed (Construction Maybe) key) = (->) key <::> Maybe
morphing :: (<::>)
(Tagged ('Lookup 'Key)) (Prefixed (Construction Maybe) key) a
-> Morphing ('Lookup 'Key) (Prefixed (Construction Maybe) key) a
morphing (Prefixed (Construction Maybe) key a
-> Construction Maybe (key :*: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Prefixed (Construction Maybe) key a
-> Construction Maybe (key :*: a))
-> ((<::>)
(Tagged ('Lookup 'Key)) (Prefixed (Construction Maybe) key) a
-> Prefixed (Construction Maybe) key a)
-> (<::>)
(Tagged ('Lookup 'Key)) (Prefixed (Construction Maybe) key) a
-> Construction Maybe (key :*: a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>)
(Tagged ('Lookup 'Key)) (Prefixed (Construction Maybe) key) a
-> Prefixed (Construction Maybe) key a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Construct key :*: a
x (Maybe :. Construction Maybe) := (key :*: a)
xs) = (((->) key :. Maybe) := a)
-> TT Covariant Covariant ((->) key) Maybe a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
(a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT ((((->) key :. Maybe) := a)
-> TT Covariant Covariant ((->) key) Maybe a)
-> (((->) key :. Maybe) := a)
-> TT Covariant Covariant ((->) key) Maybe a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \key
key -> (key :*: a) -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract ((key :*: a) -> a) -> Maybe (key :*: a) -> Maybe a
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- key -> Maybe (key :*: a)
search key
key where
search :: key -> Maybe (key :*: a)
search key
key = key
key key -> key -> 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 clause a. Conditional clause => clause -> 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! 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.
Semigroupoid m =>
m b c -> m a b -> m a c
. (key :*: a) -> key
forall a b. (a :*: b) -> a
attached) (Construction Maybe (key :*: a) -> Maybe (key :*: a))
-> ((Maybe :. Construction Maybe) := (key :*: a))
-> Maybe (key :*: a)
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
=<< (Maybe :. Construction Maybe) := (key :*: a)
xs