{-# LANGUAGE RankNTypes #-}

module Text.Cassette.Lead where

import Control.Lens qualified as Lens
import Text.Cassette.Internal.Tr (Tr(..))
import Text.Cassette.Prim

-- | Nullary leads. Synonym to 'PP'.
type NullL s = forall r. K7 Tr r (s -> r)

-- | Unary leads. A lead of type @'UnL' s a@ projects/injects a component @a@
-- from/into outer type @s@.
type UnL s a = forall r. K7 Tr (a -> r) (s -> r)

-- | Binary leads. A lead of type @'BinL' s a b@ projects/injects components
-- @a@, @b@ from/into outer type @s@.
type BinL s a b = forall r. K7 Tr (a -> b -> r) (s -> r)

-- | Ternary leads. A lead of type @'TernL' s a b c@ projects/injects components
-- @a@, @b@, @c@ from/into outer type @s@.
type TernL s a b c = forall r. K7 Tr (a -> b -> c -> r) (s -> r)

-- | Quaternary leads. A lead of type @'QuaternL' s a b c d@ projects/injects
-- components @a@, @b@, @c@, @d@ from/into outer type @s@.
type QuaternL s a b c d = forall r. K7 Tr (a -> b -> c -> d -> r) (s -> r)

-- | Lift an isomorphism (see the
-- [lens](https://hackage.haskell.org/package/lens) library) to a lead.
isoL :: forall s a. Lens.Iso s s a a -> UnL s a
isoL :: forall s a. Iso s s a a -> UnL s a
isoL Iso s s a a
l = Tr (a -> r) (s -> r)
-> (forall t. Tr ((a -> r) -> t) ((s -> r) -> t))
-> K7 Tr (a -> r) (s -> r)
forall (p :: * -> * -> *) a b.
p a b -> (forall t. p (a -> t) (b -> t)) -> K7 p a b
K7 ((C (a -> r) -> C (s -> r)) -> Tr (a -> r) (s -> r)
forall r r'. (C r -> C r') -> Tr r r'
Tr C (a -> r) -> C (s -> r)
forall {t} {p} {t} {t} {t}.
((t -> p -> t) -> t -> a -> t) -> (t -> s -> t) -> t -> s -> t
leadin) ((C ((a -> r) -> t) -> C ((s -> r) -> t))
-> Tr ((a -> r) -> t) ((s -> r) -> t)
forall r r'. (C r -> C r') -> Tr r r'
Tr C ((a -> r) -> t) -> C ((s -> r) -> t)
forall {t} {p} {t} {t} {t} {t}.
((t -> p -> t) -> t -> (a -> t) -> t)
-> (t -> (s -> t) -> t) -> t -> (s -> t) -> t
leadout)
  where
    leadin :: ((t -> p -> t) -> t -> a -> t) -> (t -> s -> t) -> t -> s -> t
leadin (t -> p -> t) -> t -> a -> t
k t -> s -> t
k' t
s s
t = (t -> p -> t) -> t -> a -> t
k (\t
s p
_ -> t -> s -> t
k' t
s s
t) t
s (Lens s s a a -> s -> a
forall s t a b. Lens s t a b -> s -> a
Lens.view (a -> f a) -> s -> f s
Lens s s a a
Iso s s a a
l s
t)
    leadout :: ((t -> p -> t) -> t -> (a -> t) -> t)
-> (t -> (s -> t) -> t) -> t -> (s -> t) -> t
leadout (t -> p -> t) -> t -> (a -> t) -> t
k t -> (s -> t) -> t
k' t
s s -> t
u = (t -> p -> t) -> t -> (a -> t) -> t
k (\t
s p
_ -> t -> (s -> t) -> t
k' t
s s -> t
u) t
s (\a
x -> s -> t
u (Lens a a s s -> a -> s
forall s t a b. Lens s t a b -> s -> a
Lens.view (Iso s s a a -> Iso a a s s
forall s t a b. Iso s t a b -> Iso b a t s
Lens.from p a (f a) -> p s (f s)
Iso s s a a
l) a
x))

-- | Lift a prism (see [lens](https://hackage.haskell.org/package/lens) library)
-- to a lead.
prismL :: Lens.Prism s s a a -> UnL s a
prismL :: forall s a. Prism s s a a -> UnL s a
prismL Prism s s a a
l = Tr (a -> r) (s -> r)
-> (forall t. Tr ((a -> r) -> t) ((s -> r) -> t))
-> K7 Tr (a -> r) (s -> r)
forall (p :: * -> * -> *) a b.
p a b -> (forall t. p (a -> t) (b -> t)) -> K7 p a b
K7 ((C (a -> r) -> C (s -> r)) -> Tr (a -> r) (s -> r)
forall r r'. (C r -> C r') -> Tr r r'
Tr C (a -> r) -> C (s -> r)
forall {t} {p} {t}.
((t -> p -> t) -> t -> a -> t) -> (t -> s -> t) -> t -> s -> t
leadin) ((C ((a -> r) -> t) -> C ((s -> r) -> t))
-> Tr ((a -> r) -> t) ((s -> r) -> t)
forall r r'. (C r -> C r') -> Tr r r'
Tr C ((a -> r) -> t) -> C ((s -> r) -> t)
forall {t} {p} {t} {t} {t} {t}.
((t -> p -> t) -> t -> (a -> t) -> t)
-> (t -> (s -> t) -> t) -> t -> (s -> t) -> t
leadout)
  where
    leadin :: ((t -> p -> t) -> t -> a -> t) -> (t -> s -> t) -> t -> s -> t
leadin (t -> p -> t) -> t -> a -> t
k t -> s -> t
k' t
s s
t = case Prism s s a a -> s -> Maybe a
forall s t a b. Prism s t a b -> s -> Maybe a
Lens.preview p a (f a) -> p s (f s)
Prism s s a a
l s
t of
      Maybe a
Nothing -> t -> s -> t
k' t
s s
t
      Just a
x -> (t -> p -> t) -> t -> a -> t
k (\t
s p
_ -> t -> s -> t
k' t
s s
t) t
s a
x
    leadout :: ((t -> p -> t) -> t -> (a -> t) -> t)
-> (t -> (s -> t) -> t) -> t -> (s -> t) -> t
leadout (t -> p -> t) -> t -> (a -> t) -> t
k t -> (s -> t) -> t
k' t
s s -> t
u = (t -> p -> t) -> t -> (a -> t) -> t
k (\t
s p
_ -> t -> (s -> t) -> t
k' t
s s -> t
u) t
s (\a
x -> s -> t
u (Prism s s a a -> a -> s
forall s t a b. Prism s t a b -> b -> t
Lens.review p a (f a) -> p s (f s)
Prism s s a a
l a
x))

-- | Iterates a one step construction function (resp. deconstruction) function,
-- i.e. a lead, thus obtaining a right fold (resp. unfold). The resulting lead
-- is a catamorphism on one side and an anamorpism on the other, hence the name.
-- The type of this function is the same as that of 'foldr', lifted to
-- cassettes.
catanar :: BinL b a b -> BinL b b [a]
catanar :: forall b a. BinL b a b -> BinL b b [a]
catanar BinL b a b
_ = [Char] -> K7 Tr (b -> [a] -> r) (b -> r)
forall a. HasCallStack => [Char] -> a
error [Char]
"unimplemented"
-- catanar (K7 (Tr f) (Tr f')) = K7 (Tr g) (Tr g')
--   where
--     g k k' s xs@[]      z = k (\s _ -> k' s xs z) s z
--     g k k' s xs@(x:xs') z =
--       g (\k' s z -> f k (\s _ _ -> k' s z) s z x) (\s _ _ -> k' s xs z) s xs' z
--     g' k k' s z =
--       f' (\k' s z x -> g' (\k' s xs' z -> k k' s (x:xs') z) (\s _ -> k' s z x) s z) (\s _ -> k (\s _ _ -> k' s z) s [] z) s z

-- | Iterates a one step construction function (resp. deconstruction) function,
-- i.e. a lead, thus obtaining a left fold (resp. unfold). The resulting lead is
-- a catamorphism on one side and an anamorpism on the other, hence the name.
-- The type of this function is the same as that of 'foldl', lifted to
-- cassettes.
catanal :: BinL a a b -> BinL a a [b]
catanal :: forall a b. BinL a a b -> BinL a a [b]
catanal BinL a a b
_ = [Char] -> K7 Tr (a -> [b] -> r) (a -> r)
forall a. HasCallStack => [Char] -> a
error [Char]
"unimplemented"
-- catanal (K7 (Tr f) (Tr f')) = K7 (Tr g) (Tr (g' []))
--   where
--     g k k' s xs@[]      z = k (\s _ -> k' s xs z) s z
--     g k k' s xs@(x:xs') z =
--       f (\k' s z -> g k (\s _ _ -> k' s z) s xs' z) (\s _ _ -> k' s xs z) s x z
--     g' xs' k k' s z =
--       f' (\k' s x z -> g' (x:xs') k (\s _ -> k' s x z) s z) (\s _ -> k (\s _ _ -> k' s z) s xs' z) s z

-- | '(:)' lead.
consL :: BinL [a] a [a]
consL :: forall a r. K7 Tr (a -> [a] -> r) ([a] -> r)
consL = Tr (a -> [a] -> r) ([a] -> r)
-> (forall t. Tr ((a -> [a] -> r) -> t) (([a] -> r) -> t))
-> K7 Tr (a -> [a] -> r) ([a] -> r)
forall (p :: * -> * -> *) a b.
p a b -> (forall t. p (a -> t) (b -> t)) -> K7 p a b
K7 ((C (a -> [a] -> r) -> C ([a] -> r))
-> Tr (a -> [a] -> r) ([a] -> r)
forall r r'. (C r -> C r') -> Tr r r'
Tr C (a -> [a] -> r) -> C ([a] -> r)
forall {t} {p} {p} {t} {t}.
((t -> p -> p -> t) -> t -> t -> [t] -> t)
-> (t -> [t] -> t) -> t -> [t] -> t
leadin) ((C ((a -> [a] -> r) -> t) -> C (([a] -> r) -> t))
-> Tr ((a -> [a] -> r) -> t) (([a] -> r) -> t)
forall r r'. (C r -> C r') -> Tr r r'
Tr C ((a -> [a] -> r) -> t) -> C (([a] -> r) -> t)
forall {t} {p} {t} {t} {a} {t} {t}.
((t -> p -> t) -> t -> (a -> [a] -> t) -> t)
-> (t -> ([a] -> t) -> t) -> t -> ([a] -> t) -> t
leadout)
  where
    leadin :: ((t -> p -> p -> t) -> t -> t -> [t] -> t)
-> (t -> [t] -> t) -> t -> [t] -> t
leadin (t -> p -> p -> t) -> t -> t -> [t] -> t
k t -> [t] -> t
k' t
s xs :: [t]
xs@(t
x:[t]
xs') = (t -> p -> p -> t) -> t -> t -> [t] -> t
k (\t
s p
_ p
_ -> t -> [t] -> t
k' t
s [t]
xs) t
s t
x [t]
xs'
    leadin (t -> p -> p -> t) -> t -> t -> [t] -> t
_ t -> [t] -> t
k' t
s [t]
xs = t -> [t] -> t
k' t
s [t]
xs
    leadout :: ((t -> p -> t) -> t -> (a -> [a] -> t) -> t)
-> (t -> ([a] -> t) -> t) -> t -> ([a] -> t) -> t
leadout (t -> p -> t) -> t -> (a -> [a] -> t) -> t
k t -> ([a] -> t) -> t
k' t
s [a] -> t
u = (t -> p -> t) -> t -> (a -> [a] -> t) -> t
k (\t
s p
_ -> t -> ([a] -> t) -> t
k' t
s [a] -> t
u) t
s (\a
x [a]
xs' -> [a] -> t
u (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
xs'))

-- | '[]' lead.
nilL :: NullL [a]
nilL :: forall a r. K7 Tr r ([a] -> r)
nilL = Tr r ([a] -> r)
-> (forall t. Tr (r -> t) (([a] -> r) -> t)) -> K7 Tr r ([a] -> r)
forall (p :: * -> * -> *) a b.
p a b -> (forall t. p (a -> t) (b -> t)) -> K7 p a b
K7 ((C r -> C ([a] -> r)) -> Tr r ([a] -> r)
forall r r'. (C r -> C r') -> Tr r r'
Tr C r -> C ([a] -> r)
forall {t} {t} {a}.
((t -> t) -> t -> t) -> (t -> [a] -> t) -> t -> [a] -> t
leadin) ((C (r -> t) -> C (([a] -> r) -> t))
-> Tr (r -> t) (([a] -> r) -> t)
forall r r'. (C r -> C r') -> Tr r r'
Tr C (r -> t) -> C (([a] -> r) -> t)
forall {t} {p} {t} {t} {t} {t} {a}.
((t -> p -> t) -> t -> t -> t)
-> (t -> ([a] -> t) -> t) -> t -> ([a] -> t) -> t
leadout)
  where
    leadin :: ((t -> t) -> t -> t) -> (t -> [a] -> t) -> t -> [a] -> t
leadin (t -> t) -> t -> t
k t -> [a] -> t
k' t
s xs :: [a]
xs@[] = (t -> t) -> t -> t
k (\t
s -> t -> [a] -> t
k' t
s [a]
xs) t
s
    leadin (t -> t) -> t -> t
_ t -> [a] -> t
k' t
s [a]
xs = t -> [a] -> t
k' t
s [a]
xs
    leadout :: ((t -> p -> t) -> t -> t -> t)
-> (t -> ([a] -> t) -> t) -> t -> ([a] -> t) -> t
leadout (t -> p -> t) -> t -> t -> t
k t -> ([a] -> t) -> t
k' t
s [a] -> t
u = (t -> p -> t) -> t -> t -> t
k (\t
s p
_ -> t -> ([a] -> t) -> t
k' t
s [a] -> t
u) t
s ([a] -> t
u [])

-- | 'Just' lead.
justL :: UnL (Maybe a) a 
justL :: forall a r. K7 Tr (a -> r) (Maybe a -> r)
justL = Tr (a -> r) (Maybe a -> r)
-> (forall t. Tr ((a -> r) -> t) ((Maybe a -> r) -> t))
-> K7 Tr (a -> r) (Maybe a -> r)
forall (p :: * -> * -> *) a b.
p a b -> (forall t. p (a -> t) (b -> t)) -> K7 p a b
K7 ((C (a -> r) -> C (Maybe a -> r)) -> Tr (a -> r) (Maybe a -> r)
forall r r'. (C r -> C r') -> Tr r r'
Tr C (a -> r) -> C (Maybe a -> r)
forall {t} {p} {t} {t}.
((t -> p -> t) -> t -> t -> t)
-> (t -> Maybe t -> t) -> t -> Maybe t -> t
leadin) ((C ((a -> r) -> t) -> C ((Maybe a -> r) -> t))
-> Tr ((a -> r) -> t) ((Maybe a -> r) -> t)
forall r r'. (C r -> C r') -> Tr r r'
Tr C ((a -> r) -> t) -> C ((Maybe a -> r) -> t)
forall {t} {p} {t} {t} {a} {t} {t}.
((t -> p -> t) -> t -> (a -> t) -> t)
-> (t -> (Maybe a -> t) -> t) -> t -> (Maybe a -> t) -> t
leadout)
  where
    leadin :: ((t -> p -> t) -> t -> t -> t)
-> (t -> Maybe t -> t) -> t -> Maybe t -> t
leadin (t -> p -> t) -> t -> t -> t
k t -> Maybe t -> t
k' t
s mb :: Maybe t
mb@(Just t
x) = (t -> p -> t) -> t -> t -> t
k (\t
s p
_ -> t -> Maybe t -> t
k' t
s Maybe t
mb) t
s t
x
    leadin (t -> p -> t) -> t -> t -> t
_ t -> Maybe t -> t
k' t
s Maybe t
mb = t -> Maybe t -> t
k' t
s Maybe t
mb
    leadout :: ((t -> p -> t) -> t -> (a -> t) -> t)
-> (t -> (Maybe a -> t) -> t) -> t -> (Maybe a -> t) -> t
leadout (t -> p -> t) -> t -> (a -> t) -> t
k t -> (Maybe a -> t) -> t
k' t
s Maybe a -> t
u = (t -> p -> t) -> t -> (a -> t) -> t
k (\t
s p
_ -> t -> (Maybe a -> t) -> t
k' t
s Maybe a -> t
u) t
s (\a
x -> Maybe a -> t
u (a -> Maybe a
forall a. a -> Maybe a
Just a
x))

-- | 'Nothing' lead.
nothingL :: PP (Maybe a)
nothingL :: forall a r. K7 Tr r (Maybe a -> r)
nothingL = Tr r (Maybe a -> r)
-> (forall t. Tr (r -> t) ((Maybe a -> r) -> t))
-> K7 Tr r (Maybe a -> r)
forall (p :: * -> * -> *) a b.
p a b -> (forall t. p (a -> t) (b -> t)) -> K7 p a b
K7 ((C r -> C (Maybe a -> r)) -> Tr r (Maybe a -> r)
forall r r'. (C r -> C r') -> Tr r r'
Tr C r -> C (Maybe a -> r)
forall {t} {t} {a}.
((t -> t) -> t -> t) -> (t -> Maybe a -> t) -> t -> Maybe a -> t
leadin) ((C (r -> t) -> C ((Maybe a -> r) -> t))
-> Tr (r -> t) ((Maybe a -> r) -> t)
forall r r'. (C r -> C r') -> Tr r r'
Tr C (r -> t) -> C ((Maybe a -> r) -> t)
forall {t} {p} {t} {t} {t} {t} {a}.
((t -> p -> t) -> t -> t -> t)
-> (t -> (Maybe a -> t) -> t) -> t -> (Maybe a -> t) -> t
leadout)
  where
    leadin :: ((t -> t) -> t -> t) -> (t -> Maybe a -> t) -> t -> Maybe a -> t
leadin (t -> t) -> t -> t
k t -> Maybe a -> t
k' t
s mb :: Maybe a
mb@Maybe a
Nothing = (t -> t) -> t -> t
k (\t
s -> t -> Maybe a -> t
k' t
s Maybe a
mb) t
s
    leadin (t -> t) -> t -> t
_ t -> Maybe a -> t
k' t
s Maybe a
mb = t -> Maybe a -> t
k' t
s Maybe a
mb
    leadout :: ((t -> p -> t) -> t -> t -> t)
-> (t -> (Maybe a -> t) -> t) -> t -> (Maybe a -> t) -> t
leadout (t -> p -> t) -> t -> t -> t
k t -> (Maybe a -> t) -> t
k' t
s Maybe a -> t
u = (t -> p -> t) -> t -> t -> t
k (\t
s p
_ -> t -> (Maybe a -> t) -> t
k' t
s Maybe a -> t
u) t
s (Maybe a -> t
u Maybe a
forall a. Maybe a
Nothing)

-- | Construct/destruct the unit element.
unitL :: NullL ()
unitL :: NullL ()
unitL = Tr r (() -> r)
-> (forall t. Tr (r -> t) ((() -> r) -> t)) -> K7 Tr r (() -> r)
forall (p :: * -> * -> *) a b.
p a b -> (forall t. p (a -> t) (b -> t)) -> K7 p a b
K7 ((C r -> C (() -> r)) -> Tr r (() -> r)
forall r r'. (C r -> C r') -> Tr r r'
Tr C r -> C (() -> r)
forall {t} {t} {t} {t}.
((t -> t) -> t -> t) -> (t -> () -> t) -> t -> () -> t
leadin) ((C (r -> t) -> C ((() -> r) -> t)) -> Tr (r -> t) ((() -> r) -> t)
forall r r'. (C r -> C r') -> Tr r r'
Tr C (r -> t) -> C ((() -> r) -> t)
forall {t} {p} {t} {t} {t} {t}.
((t -> p -> t) -> t -> t -> t)
-> (t -> (() -> t) -> t) -> t -> (() -> t) -> t
leadout)
  where
    leadin :: ((t -> t) -> t -> t) -> (t -> () -> t) -> t -> () -> t
leadin (t -> t) -> t -> t
k t -> () -> t
k' t
s t :: ()
t@() = (t -> t) -> t -> t
k (\t
s -> t -> () -> t
k' t
s ()
t) t
s
    leadout :: ((t -> p -> t) -> t -> t -> t)
-> (t -> (() -> t) -> t) -> t -> (() -> t) -> t
leadout (t -> p -> t) -> t -> t -> t
k t -> (() -> t) -> t
k' t
s () -> t
u = (t -> p -> t) -> t -> t -> t
k (\t
s p
_ -> t -> (() -> t) -> t
k' t
s () -> t
u) t
s (() -> t
u ())

-- | Construct/destruct a pair.
pairL :: BinL (a, b) a b
pairL :: forall a b r. K7 Tr (a -> b -> r) ((a, b) -> r)
pairL = Tr (a -> b -> r) ((a, b) -> r)
-> (forall t. Tr ((a -> b -> r) -> t) (((a, b) -> r) -> t))
-> K7 Tr (a -> b -> r) ((a, b) -> r)
forall (p :: * -> * -> *) a b.
p a b -> (forall t. p (a -> t) (b -> t)) -> K7 p a b
K7 ((C (a -> b -> r) -> C ((a, b) -> r))
-> Tr (a -> b -> r) ((a, b) -> r)
forall r r'. (C r -> C r') -> Tr r r'
Tr C (a -> b -> r) -> C ((a, b) -> r)
forall {t} {p} {p} {t} {t} {t} {t} {t}.
((t -> p -> p -> t) -> t -> t -> t -> t)
-> (t -> (t, t) -> t) -> t -> (t, t) -> t
leadin) ((C ((a -> b -> r) -> t) -> C (((a, b) -> r) -> t))
-> Tr ((a -> b -> r) -> t) (((a, b) -> r) -> t)
forall r r'. (C r -> C r') -> Tr r r'
Tr C ((a -> b -> r) -> t) -> C (((a, b) -> r) -> t)
forall {t} {p} {t} {t} {a} {b} {t} {t}.
((t -> p -> t) -> t -> (a -> b -> t) -> t)
-> (t -> ((a, b) -> t) -> t) -> t -> ((a, b) -> t) -> t
leadout)
  where
    leadin :: ((t -> p -> p -> t) -> t -> t -> t -> t)
-> (t -> (t, t) -> t) -> t -> (t, t) -> t
leadin (t -> p -> p -> t) -> t -> t -> t -> t
k t -> (t, t) -> t
k' t
s t :: (t, t)
t@(t
x1, t
x2) = (t -> p -> p -> t) -> t -> t -> t -> t
k (\t
s p
_ p
_ -> t -> (t, t) -> t
k' t
s (t, t)
t) t
s t
x1 t
x2
    leadout :: ((t -> p -> t) -> t -> (a -> b -> t) -> t)
-> (t -> ((a, b) -> t) -> t) -> t -> ((a, b) -> t) -> t
leadout (t -> p -> t) -> t -> (a -> b -> t) -> t
k t -> ((a, b) -> t) -> t
k' t
s (a, b) -> t
u = (t -> p -> t) -> t -> (a -> b -> t) -> t
k (\t
s p
_ -> t -> ((a, b) -> t) -> t
k' t
s (a, b) -> t
u) t
s (\a
x1 b
x2 -> (a, b) -> t
u (a
x1, b
x2))

-- | Construct/destruct a 3-tuple.
tripleL :: TernL (a, b, c) a b c
tripleL :: forall a b c r. K7 Tr (a -> b -> c -> r) ((a, b, c) -> r)
tripleL = Tr (a -> b -> c -> r) ((a, b, c) -> r)
-> (forall t. Tr ((a -> b -> c -> r) -> t) (((a, b, c) -> r) -> t))
-> K7 Tr (a -> b -> c -> r) ((a, b, c) -> r)
forall (p :: * -> * -> *) a b.
p a b -> (forall t. p (a -> t) (b -> t)) -> K7 p a b
K7 ((C (a -> b -> c -> r) -> C ((a, b, c) -> r))
-> Tr (a -> b -> c -> r) ((a, b, c) -> r)
forall r r'. (C r -> C r') -> Tr r r'
Tr C (a -> b -> c -> r) -> C ((a, b, c) -> r)
forall {t} {p} {p} {p} {t} {t} {t} {t} {t} {t}.
((t -> p -> p -> p -> t) -> t -> t -> t -> t -> t)
-> (t -> (t, t, t) -> t) -> t -> (t, t, t) -> t
leadin) ((C ((a -> b -> c -> r) -> t) -> C (((a, b, c) -> r) -> t))
-> Tr ((a -> b -> c -> r) -> t) (((a, b, c) -> r) -> t)
forall r r'. (C r -> C r') -> Tr r r'
Tr C ((a -> b -> c -> r) -> t) -> C (((a, b, c) -> r) -> t)
forall {t} {p} {t} {t} {a} {b} {c} {t} {t}.
((t -> p -> t) -> t -> (a -> b -> c -> t) -> t)
-> (t -> ((a, b, c) -> t) -> t) -> t -> ((a, b, c) -> t) -> t
leadout)
  where
    leadin :: ((t -> p -> p -> p -> t) -> t -> t -> t -> t -> t)
-> (t -> (t, t, t) -> t) -> t -> (t, t, t) -> t
leadin (t -> p -> p -> p -> t) -> t -> t -> t -> t -> t
k t -> (t, t, t) -> t
k' t
s t :: (t, t, t)
t@(t
x1, t
x2, t
x3) = (t -> p -> p -> p -> t) -> t -> t -> t -> t -> t
k (\t
s p
_ p
_ p
_ -> t -> (t, t, t) -> t
k' t
s (t, t, t)
t) t
s t
x1 t
x2 t
x3
    leadout :: ((t -> p -> t) -> t -> (a -> b -> c -> t) -> t)
-> (t -> ((a, b, c) -> t) -> t) -> t -> ((a, b, c) -> t) -> t
leadout (t -> p -> t) -> t -> (a -> b -> c -> t) -> t
k t -> ((a, b, c) -> t) -> t
k' t
s (a, b, c) -> t
u = (t -> p -> t) -> t -> (a -> b -> c -> t) -> t
k (\t
s p
_ -> t -> ((a, b, c) -> t) -> t
k' t
s (a, b, c) -> t
u) t
s (\a
x1 b
x2 c
x3 -> (a, b, c) -> t
u (a
x1, b
x2, c
x3))

-- | Construct/destruct a 4-tuple.
quadrupleL :: QuaternL (a, b, c, d) a b c d
quadrupleL :: forall a b c d r. K7 Tr (a -> b -> c -> d -> r) ((a, b, c, d) -> r)
quadrupleL = Tr (a -> b -> c -> d -> r) ((a, b, c, d) -> r)
-> (forall t.
    Tr ((a -> b -> c -> d -> r) -> t) (((a, b, c, d) -> r) -> t))
-> K7 Tr (a -> b -> c -> d -> r) ((a, b, c, d) -> r)
forall (p :: * -> * -> *) a b.
p a b -> (forall t. p (a -> t) (b -> t)) -> K7 p a b
K7 ((C (a -> b -> c -> d -> r) -> C ((a, b, c, d) -> r))
-> Tr (a -> b -> c -> d -> r) ((a, b, c, d) -> r)
forall r r'. (C r -> C r') -> Tr r r'
Tr C (a -> b -> c -> d -> r) -> C ((a, b, c, d) -> r)
forall {t} {p} {p} {p} {p} {t} {t} {t} {t} {t} {t} {t}.
((t -> p -> p -> p -> p -> t) -> t -> t -> t -> t -> t -> t)
-> (t -> (t, t, t, t) -> t) -> t -> (t, t, t, t) -> t
leadin) ((C ((a -> b -> c -> d -> r) -> t) -> C (((a, b, c, d) -> r) -> t))
-> Tr ((a -> b -> c -> d -> r) -> t) (((a, b, c, d) -> r) -> t)
forall r r'. (C r -> C r') -> Tr r r'
Tr C ((a -> b -> c -> d -> r) -> t) -> C (((a, b, c, d) -> r) -> t)
forall {t} {p} {t} {t} {a} {b} {c} {d} {t} {t}.
((t -> p -> t) -> t -> (a -> b -> c -> d -> t) -> t)
-> (t -> ((a, b, c, d) -> t) -> t) -> t -> ((a, b, c, d) -> t) -> t
leadout)
  where
    leadin :: ((t -> p -> p -> p -> p -> t) -> t -> t -> t -> t -> t -> t)
-> (t -> (t, t, t, t) -> t) -> t -> (t, t, t, t) -> t
leadin (t -> p -> p -> p -> p -> t) -> t -> t -> t -> t -> t -> t
k t -> (t, t, t, t) -> t
k' t
s t :: (t, t, t, t)
t@(t
x1, t
x2, t
x3, t
x4) = (t -> p -> p -> p -> p -> t) -> t -> t -> t -> t -> t -> t
k (\t
s p
_ p
_ p
_ p
_ -> t -> (t, t, t, t) -> t
k' t
s (t, t, t, t)
t) t
s t
x1 t
x2 t
x3 t
x4
    leadout :: ((t -> p -> t) -> t -> (a -> b -> c -> d -> t) -> t)
-> (t -> ((a, b, c, d) -> t) -> t) -> t -> ((a, b, c, d) -> t) -> t
leadout (t -> p -> t) -> t -> (a -> b -> c -> d -> t) -> t
k t -> ((a, b, c, d) -> t) -> t
k' t
s (a, b, c, d) -> t
u = (t -> p -> t) -> t -> (a -> b -> c -> d -> t) -> t
k (\t
s p
_ -> t -> ((a, b, c, d) -> t) -> t
k' t
s (a, b, c, d) -> t
u) t
s (\a
x1 b
x2 c
x3 d
x4 -> (a, b, c, d) -> t
u (a
x1, b
x2, c
x3, d
x4))