{-# OPTIONS_HADDOCK not-home #-}

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

{-|
Module      : Data.Generic.HKD.Named
Description : Construct an HKD record with named parameters.
Copyright   : (c) Tom Harding, 2019
License     : MIT
Maintainer  : tom.harding@habito.com
Stability   : experimental
-}
module Data.Generic.HKD.Named
  ( Record (..)
  ) where

import Data.Functor.Contravariant (Contravariant (..))
import Data.Generic.HKD.Types (HKD, HKD_)
import Data.Generics.Product.Internal.Subtype (GUpcast (..))
import Data.Kind (Type)
import GHC.Generics
import Named ((:!), NamedF (..))

type family Append (xs :: Type -> Type) (ys :: Type -> Type) :: Type -> Type where
  Append (S1 meta head) tail    = S1 meta head :*: tail
  Append (left :*: right) other = left :*: Append right other

type family Rearrange (i :: Type -> Type) :: Type -> Type where
  Rearrange (S1       m inner) = S1       m (Rearrange inner)
  Rearrange (M1 index m inner) = M1 index m (Rearrange inner)
  Rearrange (left :*: right)   = Append (Rearrange left) (Rearrange right)
  Rearrange (Rec0 inner)       = Rec0 inner

-- | The 'Data.Generic.HKD.record' function lets us supply arguments to a type
-- one by one, but can cause confusion when working with a record. If the
-- record contains two fields of the same type, for example, we've introduced
-- an opportunity for bugs and confusion. The @record@ function uses the
-- wonderful @named@ package to help us:
--
-- >>> :set -XDeriveGeneric -XTypeApplications
--
-- >>> :{
-- data User
--   = User { name :: String, enemy :: String }
--   deriving Generic
-- :}
--
-- >>> :{
-- test :: _
-- test = record @User
-- :}
-- ...
-- ... Found type wildcard ...
-- ... standing for ...("name" :! f [Char])
-- ...   -> ("enemy" :! f [Char]) -> HKD User f...
-- ...
class Record (structure :: Type) (f :: Type -> Type) (k :: Type)
    | f structure -> k where
  record :: k

class GRecord (rep :: Type -> Type) (f :: Type -> Type) (structure :: Type) (k :: Type)
    | f structure rep -> k where
  grecord :: (forall p. rep p -> HKD structure f) -> k

instance GRecord inner f structure k
    => GRecord (D1 meta inner) f structure k where
  grecord :: (forall p. D1 meta inner p -> HKD structure f) -> k
grecord forall p. D1 meta inner p -> HKD structure f
rebuild = (forall p. inner p -> HKD structure f) -> k
forall (rep :: * -> *) (f :: * -> *) structure k.
GRecord rep f structure k =>
(forall p. rep p -> HKD structure f) -> k
grecord (D1 meta inner p -> HKD structure f
forall p. D1 meta inner p -> HKD structure f
rebuild (D1 meta inner p -> HKD structure f)
-> (inner p -> D1 meta inner p) -> inner p -> HKD structure f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. inner p -> D1 meta inner p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1)

instance GRecord inner f structure k
    => GRecord (C1 meta inner) f structure k where
  grecord :: (forall p. C1 meta inner p -> HKD structure f) -> k
grecord forall p. C1 meta inner p -> HKD structure f
rebuild = (forall p. inner p -> HKD structure f) -> k
forall (rep :: * -> *) (f :: * -> *) structure k.
GRecord rep f structure k =>
(forall p. rep p -> HKD structure f) -> k
grecord (C1 meta inner p -> HKD structure f
forall p. C1 meta inner p -> HKD structure f
rebuild (C1 meta inner p -> HKD structure f)
-> (inner p -> C1 meta inner p) -> inner p -> HKD structure f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. inner p -> C1 meta inner p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1)

instance
    ( rec ~ (Rec0 inner)
    , k ~ (name :! inner -> HKD structure f)
    , meta ~ 'MetaSel ('Just name) i d c
    )
    => GRecord (S1 meta rec) f structure k where
  grecord :: (forall p. S1 meta rec p -> HKD structure f) -> k
grecord forall p. S1 meta rec p -> HKD structure f
fill = \(Arg inner
inner) -> S1 meta rec Any -> HKD structure f
forall p. S1 meta rec p -> HKD structure f
fill (K1 R inner Any -> M1 S meta (Rec0 inner) Any
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (inner -> K1 R inner Any
forall k i c (p :: k). c -> K1 i c p
K1 inner
inner))

instance
    ( GRecord right f structure k'
    , rec ~ Rec0 x
    , left ~ S1 ('MetaSel ('Just name) i d c) rec
    , k ~ (name :! x -> k')
    )
    => GRecord (left :*: right) f structure k where
  grecord :: (forall p. (:*:) left right p -> HKD structure f) -> k
grecord forall p. (:*:) left right p -> HKD structure f
fill = \(Arg x
left) -> (forall p. right p -> HKD structure f) -> k'
forall (rep :: * -> *) (f :: * -> *) structure k.
GRecord rep f structure k =>
(forall p. rep p -> HKD structure f) -> k
grecord \right p
right -> (:*:) left right p -> HKD structure f
forall p. (:*:) left right p -> HKD structure f
fill (K1 R x p -> M1 S ('MetaSel ('Just name) i d c) (Rec0 x) p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (x -> K1 R x p
forall k i c (p :: k). c -> K1 i c p
K1 x
left) M1 S ('MetaSel ('Just name) i d c) (Rec0 x) p
-> right p
-> (:*:) (M1 S ('MetaSel ('Just name) i d c) (Rec0 x)) right p
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: right p
right)

instance
    ( Contravariant (HKD_ f structure)
    , Functor (HKD_ f structure)

    , list ~ Rearrange (HKD_ f structure)
    , GUpcast list (HKD_ f structure)
    , GRecord list f structure k
    )
    => Record structure f k where
  record :: k
record = (forall p. list p -> HKD structure f) -> k
forall (rep :: * -> *) (f :: * -> *) structure k.
GRecord rep f structure k =>
(forall p. rep p -> HKD structure f) -> k
grecord @_ @f @structure (GHKD_ f (Rep structure) p -> HKD structure f
forall a x. Generic a => Rep a x -> a
to (GHKD_ f (Rep structure) p -> HKD structure f)
-> (list p -> GHKD_ f (Rep structure) p)
-> list p
-> HKD structure f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p.
GUpcast list (HKD_ f structure) =>
list p -> HKD_ f structure p
forall (sub :: * -> *) (sup :: * -> *) p.
GUpcast sub sup =>
sub p -> sup p
gupcast @list @(HKD_ f structure))