{-# language AllowAmbiguousTypes #-}
{-# language DataKinds #-}
{-# language EmptyCase #-}
{-# language FlexibleInstances #-}
{-# language LambdaCase #-}
{-# language MultiParamTypeClasses #-}
{-# language RankNTypes #-}
{-# language ScopedTypeVariables #-}
{-# language StandaloneKindSignatures #-}
{-# language TypeApplications #-}
{-# language TypeFamilies #-}
{-# language TypeOperators #-}
{-# language UndecidableInstances #-}

module Rel8.Generic.Map
  ( GMap, GMappable (gmap, gunmap)
  )
where

-- base
import Data.Kind ( Constraint, Type )
import GHC.Generics
  ( (:+:)( L1, R1 ), (:*:)( (:*:) ), K1( K1 ), M1( M1 ), U1( U1 ), V1
  )
import Prelude ()

-- rel8
import Rel8.FCF ( Eval, Exp )


type GMap :: (Type -> Exp Type) -> (Type -> Type) -> Type -> Type
type family GMap f rep where
  GMap f (M1 i c rep) = M1 i c (GMap f rep)
  GMap _ V1 = V1
  GMap f (rep1 :+: rep2) = GMap f rep1 :+: GMap f rep2
  GMap _ U1 = U1
  GMap f (rep1 :*: rep2) = GMap f rep1 :*: GMap f rep2
  GMap f (K1 i a) = K1 i (Eval (f a))


type GMappable :: (Type -> Exp Constraint) -> (Type -> Type) -> Constraint
class GMappable constraint rep where
  gmap :: ()
    => proxy f
    -> (forall a. Eval (constraint a) => a -> Eval (f a))
    -> rep x
    -> GMap f rep x

  gunmap :: ()
    => proxy f
    -> (forall a. Eval (constraint a) => Eval (f a) -> a)
    -> GMap f rep x
    -> rep x


instance GMappable constraint rep => GMappable constraint (M1 i c rep) where
  gmap :: proxy f
-> (forall a. Eval (constraint a) => a -> Eval (f a))
-> M1 i c rep x
-> GMap f (M1 i c rep) x
gmap proxy f
proxy forall a. Eval (constraint a) => a -> Eval (f a)
f (M1 rep x
a) = GMap f rep x -> M1 i c (GMap f rep) x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (proxy f
-> (forall a. Eval (constraint a) => a -> Eval (f a))
-> rep x
-> GMap f rep x
forall (constraint :: * -> Exp Constraint) (rep :: Exp *)
       (proxy :: (* -> Exp *) -> *) (f :: * -> Exp *) x.
GMappable constraint rep =>
proxy f
-> (forall a. Eval (constraint a) => a -> Eval (f a))
-> rep x
-> GMap f rep x
gmap @constraint proxy f
proxy forall a. Eval (constraint a) => a -> Eval (f a)
f rep x
a)
  gunmap :: proxy f
-> (forall a. Eval (constraint a) => Eval (f a) -> a)
-> GMap f (M1 i c rep) x
-> M1 i c rep x
gunmap proxy f
proxy forall a. Eval (constraint a) => Eval (f a) -> a
f (M1 a) = rep x -> M1 i c rep x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (proxy f
-> (forall a. Eval (constraint a) => Eval (f a) -> a)
-> GMap f rep x
-> rep x
forall (constraint :: * -> Exp Constraint) (rep :: Exp *)
       (proxy :: (* -> Exp *) -> *) (f :: * -> Exp *) x.
GMappable constraint rep =>
proxy f
-> (forall a. Eval (constraint a) => Eval (f a) -> a)
-> GMap f rep x
-> rep x
gunmap @constraint proxy f
proxy forall a. Eval (constraint a) => Eval (f a) -> a
f GMap f rep x
a)


instance GMappable constraint V1 where
  gmap :: proxy f
-> (forall a. Eval (constraint a) => a -> Eval (f a))
-> V1 x
-> GMap f V1 x
gmap proxy f
_ forall a. Eval (constraint a) => a -> Eval (f a)
_ = V1 x -> GMap f V1 x
\case
  gunmap :: proxy f
-> (forall a. Eval (constraint a) => Eval (f a) -> a)
-> GMap f V1 x
-> V1 x
gunmap proxy f
_ forall a. Eval (constraint a) => Eval (f a) -> a
_ = GMap f V1 x -> V1 x
\case


instance (GMappable constraint rep1, GMappable constraint rep2) =>
  GMappable constraint (rep1 :+: rep2)
 where
  gmap :: proxy f
-> (forall a. Eval (constraint a) => a -> Eval (f a))
-> (:+:) rep1 rep2 x
-> GMap f (rep1 :+: rep2) x
gmap proxy f
proxy forall a. Eval (constraint a) => a -> Eval (f a)
f = \case
    L1 rep1 x
a -> GMap f rep1 x -> (:+:) (GMap f rep1) (GMap f rep2) x
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (proxy f
-> (forall a. Eval (constraint a) => a -> Eval (f a))
-> rep1 x
-> GMap f rep1 x
forall (constraint :: * -> Exp Constraint) (rep :: Exp *)
       (proxy :: (* -> Exp *) -> *) (f :: * -> Exp *) x.
GMappable constraint rep =>
proxy f
-> (forall a. Eval (constraint a) => a -> Eval (f a))
-> rep x
-> GMap f rep x
gmap @constraint proxy f
proxy forall a. Eval (constraint a) => a -> Eval (f a)
f rep1 x
a)
    R1 rep2 x
a -> GMap f rep2 x -> (:+:) (GMap f rep1) (GMap f rep2) x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (proxy f
-> (forall a. Eval (constraint a) => a -> Eval (f a))
-> rep2 x
-> GMap f rep2 x
forall (constraint :: * -> Exp Constraint) (rep :: Exp *)
       (proxy :: (* -> Exp *) -> *) (f :: * -> Exp *) x.
GMappable constraint rep =>
proxy f
-> (forall a. Eval (constraint a) => a -> Eval (f a))
-> rep x
-> GMap f rep x
gmap @constraint proxy f
proxy forall a. Eval (constraint a) => a -> Eval (f a)
f rep2 x
a)
  gunmap :: proxy f
-> (forall a. Eval (constraint a) => Eval (f a) -> a)
-> GMap f (rep1 :+: rep2) x
-> (:+:) rep1 rep2 x
gunmap proxy f
proxy forall a. Eval (constraint a) => Eval (f a) -> a
f = \case
    L1 a -> rep1 x -> (:+:) rep1 rep2 x
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (proxy f
-> (forall a. Eval (constraint a) => Eval (f a) -> a)
-> GMap f rep1 x
-> rep1 x
forall (constraint :: * -> Exp Constraint) (rep :: Exp *)
       (proxy :: (* -> Exp *) -> *) (f :: * -> Exp *) x.
GMappable constraint rep =>
proxy f
-> (forall a. Eval (constraint a) => Eval (f a) -> a)
-> GMap f rep x
-> rep x
gunmap @constraint proxy f
proxy forall a. Eval (constraint a) => Eval (f a) -> a
f GMap f rep1 x
a)
    R1 a -> rep2 x -> (:+:) rep1 rep2 x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (proxy f
-> (forall a. Eval (constraint a) => Eval (f a) -> a)
-> GMap f rep2 x
-> rep2 x
forall (constraint :: * -> Exp Constraint) (rep :: Exp *)
       (proxy :: (* -> Exp *) -> *) (f :: * -> Exp *) x.
GMappable constraint rep =>
proxy f
-> (forall a. Eval (constraint a) => Eval (f a) -> a)
-> GMap f rep x
-> rep x
gunmap @constraint proxy f
proxy forall a. Eval (constraint a) => Eval (f a) -> a
f GMap f rep2 x
a)


instance GMappable constraint U1 where
  gmap :: proxy f
-> (forall a. Eval (constraint a) => a -> Eval (f a))
-> U1 x
-> GMap f U1 x
gmap proxy f
_ forall a. Eval (constraint a) => a -> Eval (f a)
_ U1 x
U1 = GMap f U1 x
forall k (p :: k). U1 p
U1
  gunmap :: proxy f
-> (forall a. Eval (constraint a) => Eval (f a) -> a)
-> GMap f U1 x
-> U1 x
gunmap proxy f
_ forall a. Eval (constraint a) => Eval (f a) -> a
_ GMap f U1 x
U1 = U1 x
forall k (p :: k). U1 p
U1


instance (GMappable constraint rep1, GMappable constraint rep2) =>
  GMappable constraint (rep1 :*: rep2)
 where
  gmap :: proxy f
-> (forall a. Eval (constraint a) => a -> Eval (f a))
-> (:*:) rep1 rep2 x
-> GMap f (rep1 :*: rep2) x
gmap proxy f
proxy forall a. Eval (constraint a) => a -> Eval (f a)
f (rep1 x
a :*: rep2 x
b) =
    proxy f
-> (forall a. Eval (constraint a) => a -> Eval (f a))
-> rep1 x
-> GMap f rep1 x
forall (constraint :: * -> Exp Constraint) (rep :: Exp *)
       (proxy :: (* -> Exp *) -> *) (f :: * -> Exp *) x.
GMappable constraint rep =>
proxy f
-> (forall a. Eval (constraint a) => a -> Eval (f a))
-> rep x
-> GMap f rep x
gmap @constraint proxy f
proxy forall a. Eval (constraint a) => a -> Eval (f a)
f rep1 x
a GMap f rep1 x
-> GMap f rep2 x -> (:*:) (GMap f rep1) (GMap f rep2) x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: proxy f
-> (forall a. Eval (constraint a) => a -> Eval (f a))
-> rep2 x
-> GMap f rep2 x
forall (constraint :: * -> Exp Constraint) (rep :: Exp *)
       (proxy :: (* -> Exp *) -> *) (f :: * -> Exp *) x.
GMappable constraint rep =>
proxy f
-> (forall a. Eval (constraint a) => a -> Eval (f a))
-> rep x
-> GMap f rep x
gmap @constraint proxy f
proxy forall a. Eval (constraint a) => a -> Eval (f a)
f rep2 x
b
  gunmap :: proxy f
-> (forall a. Eval (constraint a) => Eval (f a) -> a)
-> GMap f (rep1 :*: rep2) x
-> (:*:) rep1 rep2 x
gunmap proxy f
proxy forall a. Eval (constraint a) => Eval (f a) -> a
f (a :*: b) =
    proxy f
-> (forall a. Eval (constraint a) => Eval (f a) -> a)
-> GMap f rep1 x
-> rep1 x
forall (constraint :: * -> Exp Constraint) (rep :: Exp *)
       (proxy :: (* -> Exp *) -> *) (f :: * -> Exp *) x.
GMappable constraint rep =>
proxy f
-> (forall a. Eval (constraint a) => Eval (f a) -> a)
-> GMap f rep x
-> rep x
gunmap @constraint proxy f
proxy forall a. Eval (constraint a) => Eval (f a) -> a
f GMap f rep1 x
a rep1 x -> rep2 x -> (:*:) rep1 rep2 x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: proxy f
-> (forall a. Eval (constraint a) => Eval (f a) -> a)
-> GMap f rep2 x
-> rep2 x
forall (constraint :: * -> Exp Constraint) (rep :: Exp *)
       (proxy :: (* -> Exp *) -> *) (f :: * -> Exp *) x.
GMappable constraint rep =>
proxy f
-> (forall a. Eval (constraint a) => Eval (f a) -> a)
-> GMap f rep x
-> rep x
gunmap @constraint proxy f
proxy forall a. Eval (constraint a) => Eval (f a) -> a
f GMap f rep2 x
b


instance Eval (constraint a) => GMappable constraint (K1 i a) where
  gmap :: proxy f
-> (forall a. Eval (constraint a) => a -> Eval (f a))
-> K1 i a x
-> GMap f (K1 i a) x
gmap proxy f
_ forall a. Eval (constraint a) => a -> Eval (f a)
f (K1 a
a) = Eval (f a) -> K1 i (Eval (f a)) x
forall k i c (p :: k). c -> K1 i c p
K1 (a -> Eval (f a)
forall a. Eval (constraint a) => a -> Eval (f a)
f a
a)
  gunmap :: proxy f
-> (forall a. Eval (constraint a) => Eval (f a) -> a)
-> GMap f (K1 i a) x
-> K1 i a x
gunmap proxy f
_ forall a. Eval (constraint a) => Eval (f a) -> a
f (K1 a) = a -> K1 i a x
forall k i c (p :: k). c -> K1 i c p
K1 (Eval (f a) -> a
forall a. Eval (constraint a) => Eval (f a) -> a
f Eval (f a)
a)