{-# LANGUAGE CPP                    #-}
{-# 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.Monoid (First(..))
import Data.Profunctor (Choice(..))
import Data.Profunctor.Unsafe
import Data.Tagged
import Data.Text (pack)
#if !MIN_VERSION_base(4,11,0)
import Data.Semigroup ((<>))
#endif

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 :: * -> *) (t :: *) :: [*] 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 :: * -> *) (l :: [*]) :: [*] 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 :: * -> *) 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 :: * -> *) (a :: *)

class MkPrismList (f :: * -> *) 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 :: * -> *) (t :: *) :: *

class MkStackPrism (f :: * -> *) 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