{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE OverloadedStrings      #-}
{-# LANGUAGE PolyKinds              #-}
{-# LANGUAGE RankNTypes             #-}
{-# LANGUAGE Safe                   #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE TypeOperators          #-}

-- NB: UndecidableInstances needed for nested type family application. :-/
{-# LANGUAGE UndecidableInstances   #-}

module Data.InvertibleGrammar.Generic
  ( with
  , match
  , Coproduct (..)
  ) where

import Prelude hiding ((.), id)

import Control.Applicative
import Control.Category ((.))

import Data.Functor.Identity
import Data.InvertibleGrammar.Base
import Data.Kind (Type)
import Data.Monoid (First(..))
import Data.Profunctor (Choice(..))
import Data.Profunctor.Unsafe
import Data.Tagged
import Data.Text (pack)


import GHC.Generics

-- | Provide a data constructor/stack isomorphism to a grammar working on
-- stacks. Works for types with one data constructor. For sum types use 'match'
-- and 'Coproduct'.
with
  :: forall a b s t c d f p.
     ( Generic a
     , MkPrismList (Rep a)
     , MkStackPrism f
     , Rep a ~ M1 D d (M1 C c f)
     , StackPrismLhs f t ~ b
     , Constructor c
     ) =>
     (Grammar p b (a :- t) -> Grammar p s (a :- t))
  -> Grammar p s (a :- t)
with :: forall a b s t (c :: Meta) (d :: Meta) (f :: * -> *) p.
(Generic a, MkPrismList (Rep a), MkStackPrism f,
 Rep a ~ M1 D d (M1 C c f), StackPrismLhs f t ~ b, Constructor c) =>
(Grammar p b (a :- t) -> Grammar p s (a :- t))
-> Grammar p s (a :- t)
with Grammar p b (a :- t) -> Grammar p s (a :- t)
g =
  let PrismList (P forall t. StackPrism (StackPrismLhs f t) (a :- t)
prism) = forall a. (Generic a, MkPrismList (Rep a)) => StackPrisms a
mkRevPrismList
      name :: [Char]
name = forall {k} (c :: k) k1 (t :: k -> (k1 -> *) -> k1 -> *)
       (f :: k1 -> *) (a :: k1).
Constructor c =>
t c f a -> [Char]
conName (forall a. HasCallStack => a
undefined :: m c f e)
  in Grammar p b (a :- t) -> Grammar p s (a :- t)
g (forall a b p. (a -> b) -> (b -> Either Mismatch a) -> Grammar p a b
PartialIso
         (forall a b. StackPrism a b -> a -> b
fwd forall t. StackPrism (StackPrismLhs f t) (a :- t)
prism)
         (forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Text -> Mismatch
expected (Text
"constructor " forall a. Semigroup a => a -> a -> a
<> [Char] -> Text
pack [Char]
name)) forall a b. b -> Either a b
Right forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. StackPrism a b -> b -> Maybe a
bkwd forall t. StackPrism (StackPrismLhs f t) (a :- t)
prism))

-- | Combine all grammars provided in 'Coproduct' list into a single grammar.
match
  :: ( Generic a
     , MkPrismList (Rep a)
     , Match (Rep a) bs t
     , bs ~ Coll (Rep a) t
     ) =>
     Coproduct p s bs a t
  -> Grammar p s (a :- t)
match :: forall a (bs :: [*]) t p s.
(Generic a, MkPrismList (Rep a), Match (Rep a) bs t,
 bs ~ Coll (Rep a) t) =>
Coproduct p s bs a t -> Grammar p s (a :- t)
match = forall a b. (a, b) -> a
fst forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (f :: * -> *) (bs :: [*]) t a p s.
Match f bs t =>
PrismList f a
-> Coproduct p s bs a t
-> (Grammar p s (a :- t), Coproduct p s (Trav f bs) a t)
match' forall a. (Generic a, MkPrismList (Rep a)) => StackPrisms a
mkRevPrismList

-- | Heterogenous list of grammars, each one matches a data constructor of type
-- @a@. 'With' is used to provide a data constructor/stack isomorphism to a
-- grammar working on stacks. 'End' ends the list of matches.
data Coproduct p s bs a t where

  With
    :: (Grammar p b (a :- t) -> Grammar p s (a :- t))
    -> Coproduct p s bs a t
    -> Coproduct p s (b ': bs) a t

  End :: Coproduct p s '[] a t

----------------------------------------------------------------------
-- Machinery

type family (:++) (as :: [k]) (bs :: [k]) :: [k] where
  (:++) (a ': as) bs = a ': (as :++ bs)
  (:++) '[] bs = bs

type family Coll (f :: Type -> Type) (t :: Type) :: [Type] where
  Coll (f :+: g)  t = Coll f t :++ Coll g t
  Coll (M1 D c f) t = Coll f t
  Coll (M1 C c f) t = '[StackPrismLhs f t]

type family Trav (t :: Type -> Type) (l :: [Type]) :: [Type] where
  Trav (f :+: g) lst = Trav g (Trav f lst)
  Trav (M1 D c f) lst = Trav f lst
  Trav (M1 C c f) (l ': ls) = ls

class Match (f :: Type -> Type) bs t where
  match' :: PrismList f a
         -> Coproduct p s bs a t
         -> ( Grammar p s (a :- t)
            , Coproduct p s (Trav f bs) a t
            )

instance (Match f bs t, Trav f bs ~ '[]) => Match (M1 D c f) bs t where
  match' :: forall a p s.
PrismList (M1 D c f) a
-> Coproduct p s bs a t
-> (Grammar p s (a :- t), Coproduct p s (Trav (M1 D c f) bs) a t)
match' (PrismList PrismList f a
p) = forall (f :: * -> *) (bs :: [*]) t a p s.
Match f bs t =>
PrismList f a
-> Coproduct p s bs a t
-> (Grammar p s (a :- t), Coproduct p s (Trav f bs) a t)
match' PrismList f a
p

instance
  ( Match f bs t
  , Match g (Trav f bs) t
  ) => Match (f :+: g) bs t where
  match' :: forall a p s.
PrismList (f :+: g) a
-> Coproduct p s bs a t
-> (Grammar p s (a :- t), Coproduct p s (Trav (f :+: g) bs) a t)
match' (PrismList f a
p :& PrismList g a
q) Coproduct p s bs a t
lst =
    let (Grammar p s (a :- t)
gp, Coproduct p s (Trav f bs) a t
rest)  = forall (f :: * -> *) (bs :: [*]) t a p s.
Match f bs t =>
PrismList f a
-> Coproduct p s bs a t
-> (Grammar p s (a :- t), Coproduct p s (Trav f bs) a t)
match' PrismList f a
p Coproduct p s bs a t
lst
        (Grammar p s (a :- t)
qp, Coproduct p s (Trav g (Trav f bs)) a t
rest') = forall (f :: * -> *) (bs :: [*]) t a p s.
Match f bs t =>
PrismList f a
-> Coproduct p s bs a t
-> (Grammar p s (a :- t), Coproduct p s (Trav f bs) a t)
match' PrismList g a
q Coproduct p s (Trav f bs) a t
rest
    in (Grammar p s (a :- t)
gp forall a. Semigroup a => a -> a -> a
<> Grammar p s (a :- t)
qp, Coproduct p s (Trav g (Trav f bs)) a t
rest')

instance (StackPrismLhs f t ~ b, Constructor c) => Match (M1 C c f) (b ': bs) t where
  match' :: forall a p s.
PrismList (M1 C c f) a
-> Coproduct p s (b : bs) a t
-> (Grammar p s (a :- t),
    Coproduct p s (Trav (M1 C c f) (b : bs)) a t)
match' (P forall t. StackPrism (StackPrismLhs f t) (a :- t)
prism) (With Grammar p b (a :- t) -> Grammar p s (a :- t)
g Coproduct p s bs a t
rest) =
    let name :: [Char]
name = forall {k} (c :: k) k1 (t :: k -> (k1 -> *) -> k1 -> *)
       (f :: k1 -> *) (a :: k1).
Constructor c =>
t c f a -> [Char]
conName (forall a. HasCallStack => a
undefined :: m c f e)
        p :: b -> a :- t
p = forall a b. StackPrism a b -> a -> b
fwd forall t. StackPrism (StackPrismLhs f t) (a :- t)
prism
        q :: (a :- t) -> Either Mismatch b
q = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Text -> Mismatch
expected (Text
"constructor " forall a. Semigroup a => a -> a -> a
<> [Char] -> Text
pack [Char]
name)) forall a b. b -> Either a b
Right forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. StackPrism a b -> b -> Maybe a
bkwd forall t. StackPrism (StackPrismLhs f t) (a :- t)
prism
    in (Grammar p b (a :- t) -> Grammar p s (a :- t)
g forall a b. (a -> b) -> a -> b
$ forall a b p. (a -> b) -> (b -> Either Mismatch a) -> Grammar p a b
PartialIso b -> a :- t
p (a :- t) -> Either Mismatch b
q, Coproduct p s bs a t
rest)

-- NB. The following machinery is heavily based on
-- https://github.com/MedeaMelana/stack-prism/blob/master/Data/StackPrism/Generic.hs

-- | Derive a list of stack prisms. For more information on the shape of a
-- 'PrismList', please see the documentation below.
mkRevPrismList :: (Generic a, MkPrismList (Rep a)) => StackPrisms a
mkRevPrismList :: forall a. (Generic a, MkPrismList (Rep a)) => StackPrisms a
mkRevPrismList = forall (f :: * -> *) p a q.
MkPrismList f =>
(f p -> a) -> (a -> Maybe (f q)) -> PrismList f a
mkPrismList' forall a x. Generic a => Rep a x -> a
to (forall a. a -> Maybe a
Just forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a x. Generic a => a -> Rep a x
from)

type StackPrism a b = forall p f. (Choice p, Applicative f) => p a (f a) -> p b (f b)

-- | Construct a prism.
stackPrism :: (a -> b) -> (b -> Maybe a) -> StackPrism a b
stackPrism :: forall a b. (a -> b) -> (b -> Maybe a) -> StackPrism a b
stackPrism a -> b
f b -> Maybe a
g = forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap (\b
b -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a b. a -> Either a b
Left b
b) forall a b. b -> Either a b
Right (b -> Maybe a
g b
b)) (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f)) forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (p :: * -> * -> *) a b c.
Choice p =>
p a b -> p (Either c a) (Either c b)
right'

-- | Apply a prism in forward direction.
fwd :: StackPrism a b -> a -> b
fwd :: forall a b. StackPrism a b -> a -> b
fwd StackPrism a b
l = forall a. Identity a -> a
runIdentity forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible c b) =>
q b c -> p a b -> p a c
#. forall {k} (s :: k) b. Tagged s b -> b
unTagged forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible c b) =>
q b c -> p a b -> p a c
#. StackPrism a b
l forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible b a) =>
p b c -> q a b -> p a c
.# forall {k} (s :: k) b. b -> Tagged s b
Tagged forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible b a) =>
p b c -> q a b -> p a c
.# forall a. a -> Identity a
Identity

-- | Apply a prism in backward direction.
bkwd :: StackPrism a b -> b -> Maybe a
bkwd :: forall a b. StackPrism a b -> b -> Maybe a
bkwd StackPrism a b
l = forall a. First a -> Maybe a
getFirst forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible c b) =>
q b c -> p a b -> p a c
#. forall {k} a (b :: k). Const a b -> a
getConst forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible c b) =>
q b c -> p a b -> p a c
#. StackPrism a b
l (forall {k} a (b :: k). a -> Const a b
Const forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible c b) =>
q b c -> p a b -> p a c
#. forall a. Maybe a -> First a
First forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible c b) =>
q b c -> p a b -> p a c
#. forall a. a -> Maybe a
Just)

-- | Convenient shorthand for a 'PrismList' indexed by a type and its generic
-- representation.
type StackPrisms a = PrismList (Rep a) a

-- | A data family that is indexed on the building blocks from representation
-- types from @GHC.Generics@. It builds up to a list of prisms, one for each
-- constructor in the generic representation. The list is wrapped in the unary
-- constructor @PrismList@. Within that constructor, the prisms are separated by
-- the right-associative binary infix constructor @:&@. Finally, the individual
-- prisms are wrapped in the unary constructor @P@.
--
-- As an example, here is how to define the prisms @nil@ and @cons@ for @[a]@,
-- which is an instance of @Generic@:
--
-- > nil  :: StackPrism              t  ([a] :- t)
-- > cons :: StackPrism (a :- [a] :- t) ([a] :- t)
-- > PrismList (P nil :& P cons) = mkPrismList :: StackPrisms [a]
data family PrismList (f :: Type -> Type) (a :: Type)

class MkPrismList (f :: Type -> Type) where
  mkPrismList' :: (f p -> a) -> (a -> Maybe (f q)) -> PrismList f a

data instance PrismList (M1 D c f) a = PrismList (PrismList f a)

instance MkPrismList f => MkPrismList (M1 D c f) where
  mkPrismList' :: forall p a q.
(M1 D c f p -> a)
-> (a -> Maybe (M1 D c f q)) -> PrismList (M1 D c f) a
mkPrismList' M1 D c f p -> a
f' a -> Maybe (M1 D c f q)
g' = forall (c :: Meta) (f :: * -> *) a.
PrismList f a -> PrismList (M1 D c f) a
PrismList (forall (f :: * -> *) p a q.
MkPrismList f =>
(f p -> a) -> (a -> Maybe (f q)) -> PrismList f a
mkPrismList' (M1 D c f p -> a
f' forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1 forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> Maybe (M1 D c f q)
g'))

infixr :&
data instance PrismList (f :+: g) a = PrismList f a :& PrismList g a

instance (MkPrismList f, MkPrismList g) => MkPrismList (f :+: g) where
  mkPrismList' :: forall p a q.
((:+:) f g p -> a)
-> (a -> Maybe ((:+:) f g q)) -> PrismList (f :+: g) a
mkPrismList' (:+:) f g p -> a
f' a -> Maybe ((:+:) f g q)
g' = forall a p q.
((:+:) f g p -> a) -> (a -> Maybe ((:+:) f g q)) -> PrismList f a
f (:+:) f g p -> a
f' a -> Maybe ((:+:) f g q)
g' forall (f :: * -> *) (g :: * -> *) a.
PrismList f a -> PrismList g a -> PrismList (f :+: g) a
:& forall a p q.
((:+:) f g p -> a) -> (a -> Maybe ((:+:) f g q)) -> PrismList g a
g (:+:) f g p -> a
f' a -> Maybe ((:+:) f g q)
g'
    where
      f :: forall a p q. ((f :+: g) p -> a) -> (a -> Maybe ((f :+: g) q)) -> PrismList f a
      f :: forall a p q.
((:+:) f g p -> a) -> (a -> Maybe ((:+:) f g q)) -> PrismList f a
f (:+:) f g p -> a
_f' a -> Maybe ((:+:) f g q)
_g' = forall (f :: * -> *) p a q.
MkPrismList f =>
(f p -> a) -> (a -> Maybe (f q)) -> PrismList f a
mkPrismList' (\f p
fp -> (:+:) f g p -> a
_f' (forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 f p
fp)) (forall a q. (a -> Maybe ((:+:) f g q)) -> a -> Maybe (f q)
matchL a -> Maybe ((:+:) f g q)
_g')
      g :: forall a p q. ((f :+: g) p -> a) -> (a -> Maybe ((f :+: g) q)) -> PrismList g a
      g :: forall a p q.
((:+:) f g p -> a) -> (a -> Maybe ((:+:) f g q)) -> PrismList g a
g (:+:) f g p -> a
_f' a -> Maybe ((:+:) f g q)
_g' = forall (f :: * -> *) p a q.
MkPrismList f =>
(f p -> a) -> (a -> Maybe (f q)) -> PrismList f a
mkPrismList' (\g p
gp -> (:+:) f g p -> a
_f' (forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 g p
gp)) (forall a q. (a -> Maybe ((:+:) f g q)) -> a -> Maybe (g q)
matchR a -> Maybe ((:+:) f g q)
_g')

      matchL :: (a -> Maybe ((f :+: g) q)) -> a -> Maybe (f q)
      matchL :: forall a q. (a -> Maybe ((:+:) f g q)) -> a -> Maybe (f q)
matchL a -> Maybe ((:+:) f g q)
_g' a
a = case a -> Maybe ((:+:) f g q)
_g' a
a of
        Just (L1 f q
f'') -> forall a. a -> Maybe a
Just f q
f''
        Maybe ((:+:) f g q)
_ -> forall a. Maybe a
Nothing

      matchR :: (a -> Maybe ((f :+: g) q)) -> a -> Maybe (g q)
      matchR :: forall a q. (a -> Maybe ((:+:) f g q)) -> a -> Maybe (g q)
matchR a -> Maybe ((:+:) f g q)
_g' a
a = case a -> Maybe ((:+:) f g q)
_g' a
a of
        Just (R1 g q
g'') -> forall a. a -> Maybe a
Just g q
g''
        Maybe ((:+:) f g q)
_ -> forall a. Maybe a
Nothing

data instance PrismList (M1 C c f) a = P (forall t. StackPrism (StackPrismLhs f t) (a :- t))

instance MkStackPrism f => MkPrismList (M1 C c f) where
  mkPrismList' :: forall p a q.
(M1 C c f p -> a)
-> (a -> Maybe (M1 C c f q)) -> PrismList (M1 C c f) a
mkPrismList' M1 C c f p -> a
f' a -> Maybe (M1 C c f q)
g' = forall (c :: Meta) (f :: * -> *) a.
(forall t. StackPrism (StackPrismLhs f t) (a :- t))
-> PrismList (M1 C c f) a
P (forall a b. (a -> b) -> (b -> Maybe a) -> StackPrism a b
stackPrism (forall a p t. (M1 C c f p -> a) -> StackPrismLhs f t -> a :- t
f M1 C c f p -> a
f') (forall a p t.
(a -> Maybe (M1 C c f p)) -> (a :- t) -> Maybe (StackPrismLhs f t)
g a -> Maybe (M1 C c f q)
g'))
    where
      f :: forall a p t. (M1 C c f p -> a) -> StackPrismLhs f t -> a :- t
      f :: forall a p t. (M1 C c f p -> a) -> StackPrismLhs f t -> a :- t
f M1 C c f p -> a
_f' StackPrismLhs f t
lhs = forall a b t. (a -> b) -> (a :- t) -> b :- t
mapHead (M1 C c f p -> a
_f' forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1) (forall (f :: * -> *) p t.
MkStackPrism f =>
StackPrismLhs f t -> f p :- t
mkR StackPrismLhs f t
lhs)
      g :: forall a p t. (a -> Maybe (M1 C c f p)) -> (a :- t) -> Maybe (StackPrismLhs f t)
      g :: forall a p t.
(a -> Maybe (M1 C c f p)) -> (a :- t) -> Maybe (StackPrismLhs f t)
g a -> Maybe (M1 C c f p)
_g' (a
a :- t
t) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) p t.
MkStackPrism f =>
(f p :- t) -> StackPrismLhs f t
mkL forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (forall h t. h -> t -> h :- t
:- t
t) forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1) (a -> Maybe (M1 C c f p)
_g' a
a)

-- Deriving types and conversions for single constructors

type family StackPrismLhs (f :: Type -> Type) (t :: Type) :: Type

class MkStackPrism (f :: Type -> Type) where
  mkR :: forall p t. StackPrismLhs f t -> (f p :- t)
  mkL :: forall p t. (f p :- t) -> StackPrismLhs f t

type instance StackPrismLhs U1 t = t
instance MkStackPrism U1 where
  mkR :: forall p t. StackPrismLhs U1 t -> U1 p :- t
mkR StackPrismLhs U1 t
t         = forall k (p :: k). U1 p
U1 forall h t. h -> t -> h :- t
:- StackPrismLhs U1 t
t
  mkL :: forall p t. (U1 p :- t) -> StackPrismLhs U1 t
mkL (U1 p
U1 :- t
t) = t
t

type instance StackPrismLhs (K1 i a) t = a :- t
instance MkStackPrism (K1 i a) where
  mkR :: forall p t. StackPrismLhs (K1 i a) t -> K1 i a p :- t
mkR (a
h :- t
t) = forall k i c (p :: k). c -> K1 i c p
K1 a
h forall h t. h -> t -> h :- t
:- t
t
  mkL :: forall p t. (K1 i a p :- t) -> StackPrismLhs (K1 i a) t
mkL (K1 a
h :- t
t) = a
h forall h t. h -> t -> h :- t
:- t
t

type instance StackPrismLhs (M1 i c f) t = StackPrismLhs f t
instance MkStackPrism f => MkStackPrism (M1 i c f) where
  mkR :: forall p t. StackPrismLhs (M1 i c f) t -> M1 i c f p :- t
mkR = forall a b t. (a -> b) -> (a :- t) -> b :- t
mapHead forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (f :: * -> *) p t.
MkStackPrism f =>
StackPrismLhs f t -> f p :- t
mkR
  mkL :: forall p t. (M1 i c f p :- t) -> StackPrismLhs (M1 i c f) t
mkL = forall (f :: * -> *) p t.
MkStackPrism f =>
(f p :- t) -> StackPrismLhs f t
mkL forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b t. (a -> b) -> (a :- t) -> b :- t
mapHead forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1

type instance StackPrismLhs (f :*: g) t = StackPrismLhs g (StackPrismLhs f t)
instance (MkStackPrism f, MkStackPrism g) => MkStackPrism (f :*: g) where
  mkR :: forall p t. StackPrismLhs (f :*: g) t -> (:*:) f g p :- t
mkR StackPrismLhs (f :*: g) t
t = (f p
hg forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g p
hf) forall h t. h -> t -> h :- t
:- t
tg
    where
      g p
hf :- StackPrismLhs f t
tf = forall (f :: * -> *) p t.
MkStackPrism f =>
StackPrismLhs f t -> f p :- t
mkR StackPrismLhs (f :*: g) t
t
      f p
hg :- t
tg = forall (f :: * -> *) p t.
MkStackPrism f =>
StackPrismLhs f t -> f p :- t
mkR StackPrismLhs f t
tf
  mkL :: forall p t. ((:*:) f g p :- t) -> StackPrismLhs (f :*: g) t
mkL ((f p
hf :*: g p
hg) :- t
t) = forall (f :: * -> *) p t.
MkStackPrism f =>
(f p :- t) -> StackPrismLhs f t
mkL (g p
hg forall h t. h -> t -> h :- t
:- forall (f :: * -> *) p t.
MkStackPrism f =>
(f p :- t) -> StackPrismLhs f t
mkL (f p
hf forall h t. h -> t -> h :- t
:- t
t))

mapHead :: (a -> b) -> (a :- t) -> (b :- t)
mapHead :: forall a b t. (a -> b) -> (a :- t) -> b :- t
mapHead a -> b
f (a
h :- t
t) = a -> b
f a
h forall h t. h -> t -> h :- t
:- t
t