{-# OPTIONS_HADDOCK not-home #-}

{-# LANGUAGE AllowAmbiguousTypes    #-}
{-# LANGUAGE BlockArguments         #-}
{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE PolyKinds              #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE TypeApplications       #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE UndecidableInstances   #-}

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

import Data.Kind (Type)
import Data.Generics.Product.Internal.HList (HList (..))
import Data.Generic.HKD.Types (HKD (..), GHKD_)
import GHC.Generics
import Prelude hiding (uncurry)

class Fill (f :: Type -> Type) (structure :: Type) (types :: [Type])
    | structure f -> types, types -> f where
  fill :: HList types -> HKD structure f

class GFill (f :: Type -> Type) (xs :: [Type]) (ys :: [Type]) (rep :: Type -> Type)
    | xs rep -> ys, ys f rep -> xs, xs -> f where
  gfill :: HList xs -> (HList ys, GHKD_ f rep p)

instance GFill f xs ys inner
    => GFill f xs ys (M1 index meta inner) where
  gfill :: HList xs -> (HList ys, GHKD_ f (M1 index meta inner) p)
gfill = (GHKD_ f inner p -> M1 index meta (GHKD_ f inner) p)
-> (HList ys, GHKD_ f inner p)
-> (HList ys, M1 index meta (GHKD_ f inner) p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap GHKD_ f inner p -> M1 index meta (GHKD_ f inner) p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 ((HList ys, GHKD_ f inner p)
 -> (HList ys, M1 index meta (GHKD_ f inner) p))
-> (HList xs -> (HList ys, GHKD_ f inner p))
-> HList xs
-> (HList ys, M1 index meta (GHKD_ f inner) p)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (xs :: [*]) (ys :: [*]) (rep :: * -> *) p.
GFill f xs ys rep =>
HList xs -> (HList ys, GHKD_ f rep p)
forall (f :: * -> *) (xs :: [*]) (ys :: [*]) (rep :: * -> *) p.
GFill f xs ys rep =>
HList xs -> (HList ys, GHKD_ f rep p)
gfill @f

instance (GFill f xs ys left, GFill f ys zs right)
    => GFill f xs zs (left :*: right) where
  gfill :: HList xs -> (HList zs, GHKD_ f (left :*: right) p)
gfill HList xs
xs = do
    let (HList ys
ys,  GHKD_ f left p
left) = HList xs -> (HList ys, GHKD_ f left p)
forall (f :: * -> *) (xs :: [*]) (ys :: [*]) (rep :: * -> *) p.
GFill f xs ys rep =>
HList xs -> (HList ys, GHKD_ f rep p)
gfill @f HList xs
xs
        (HList zs
zs, GHKD_ f right p
right) = HList ys -> (HList zs, GHKD_ f right p)
forall (f :: * -> *) (xs :: [*]) (ys :: [*]) (rep :: * -> *) p.
GFill f xs ys rep =>
HList xs -> (HList ys, GHKD_ f rep p)
gfill @f HList ys
ys

    (HList zs
zs, GHKD_ f left p
left GHKD_ f left p
-> GHKD_ f right p -> (:*:) (GHKD_ f left) (GHKD_ f right) p
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: GHKD_ f right p
right)

instance GFill f (f x ': xs) xs (Rec0 x) where
  gfill :: HList (f x : xs) -> (HList xs, GHKD_ f (Rec0 x) p)
gfill (a
x :> HList as1
xs) = (HList xs
HList as1
xs, a -> K1 R a p
forall k i c (p :: k). c -> K1 i c p
K1 a
x)

instance (Generic shape, GFill f with '[] (Rep shape))
    => Fill f shape with where
  fill :: HList with -> HKD shape f
fill = GHKD_ f (Rep shape) Void -> HKD shape f
forall structure (f :: * -> *).
HKD_ f structure Void -> HKD structure f
HKD (GHKD_ f (Rep shape) Void -> HKD shape f)
-> (HList with -> GHKD_ f (Rep shape) Void)
-> HList with
-> HKD shape f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HList '[], GHKD_ f (Rep shape) Void) -> GHKD_ f (Rep shape) Void
forall a b. (a, b) -> b
snd ((HList '[], GHKD_ f (Rep shape) Void) -> GHKD_ f (Rep shape) Void)
-> (HList with -> (HList '[], GHKD_ f (Rep shape) Void))
-> HList with
-> GHKD_ f (Rep shape) Void
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rep :: * -> *) p.
GFill f with '[] rep =>
HList with -> (HList '[], GHKD_ f rep p)
forall (f :: * -> *) (xs :: [*]) (ys :: [*]) (rep :: * -> *) p.
GFill f xs ys rep =>
HList xs -> (HList ys, GHKD_ f rep p)
gfill @f @_ @'[]

-- | With many HKD applications, we're working with types like 'Maybe' where it
-- makes sense for us to start with 'mempty' and add values in as we go.
--
-- This isn't always the case, however: if all the component parts of our type
-- are gathered using some 'IO' action, we'd like to construct something like
-- @HKD MyType IO@, and @IO a@ isn't a 'Monoid' for all types @a@. When this
-- happens, we need to pass in our parameters /when/ we build our structure.
--
-- The 'build' function lets us construct our type by passing explicit values
-- for each parameter:
--
-- >>> :set -XDeriveGeneric -XTypeApplications
--
-- >>> :{
-- data User
--   = User { name :: String, age :: Int, likesDogs :: Bool }
--   deriving Generic
-- :}
--
-- >>> :{
-- test :: _
-- test = build @User
-- :}
-- ...
-- ... Found type wildcard ...
-- ... standing for ...f [Char] -> f Int -> f Bool -> HKD User f...
-- ...
--
-- Once we call the 'build' function, and indicate the type we want to build,
-- we are free to pick whichever @f@ we like and get to work!
class Build (structure :: Type) (f :: Type -> Type) (k :: Type)
    | f structure -> k where
  build :: k

class GBuild (f :: Type -> Type) (structure :: Type) (xs :: [Type]) (k :: Type)
    | f structure xs -> k where
  gbuild :: (HList xs -> HKD structure f) -> k

instance GBuild f structure xs k
    => GBuild f structure (x ': xs) (x -> k) where
  gbuild :: (HList (x : xs) -> HKD structure f) -> x -> k
gbuild HList (x : xs) -> HKD structure f
k x
x = (HList xs -> HKD structure f) -> k
forall (f :: * -> *) structure (xs :: [*]) k.
GBuild f structure xs k =>
(HList xs -> HKD structure f) -> k
gbuild @_ @_ @xs \HList xs
xs -> HList (x : xs) -> HKD structure f
k (x
x x -> HList xs -> HList (x : xs)
forall a (as1 :: [*]). a -> HList as1 -> HList (a : as1)
:> HList xs
xs)

instance GBuild f structure '[] (HKD structure f) where
  gbuild :: (HList '[] -> HKD structure f) -> HKD structure f
gbuild HList '[] -> HKD structure f
k = HList '[] -> HKD structure f
k HList '[]
Nil

instance (Fill f structure xs, GBuild f structure xs k)
    => Build structure f k where
  build :: k
build = (HList xs -> HKD structure f) -> k
forall (f :: * -> *) structure (xs :: [*]) k.
GBuild f structure xs k =>
(HList xs -> HKD structure f) -> k
gbuild @f @structure @xs HList xs -> HKD structure f
forall (f :: * -> *) structure (types :: [*]).
Fill f structure types =>
HList types -> HKD structure f
fill