{-# language AllowAmbiguousTypes #-}
{-# language BlockArguments #-}
{-# language DataKinds #-}
{-# language FlexibleContexts #-}
{-# language FlexibleInstances #-}
{-# language MultiParamTypeClasses #-}
{-# language RankNTypes #-}
{-# language ScopedTypeVariables #-}
{-# language StandaloneKindSignatures #-}
{-# language TupleSections #-}
{-# language TypeApplications #-}
{-# language TypeFamilies #-}
{-# language TypeOperators #-}
{-# language UndecidableInstances #-}

module Rel8.Generic.Construction.ADT
  ( GConstructableADT
  , GBuildADT, gbuildADT, gunbuildADT
  , GConstructADT, gconstructADT, gdeconstructADT
  , GFields, RepresentableFields, gftabulate, gfindex
  , GConstructors, RepresentableConstructors, gctabulate, gcindex
  , GConstructorADT, GMakeableADT, gmakeADT
  )
where

-- base
import Data.Bifunctor ( first )
import Data.Functor.Identity ( runIdentity )
import Data.Kind ( Constraint, Type )
import Data.List.NonEmpty ( NonEmpty )
import Data.Proxy ( Proxy( Proxy ) )
import GHC.Generics
  ( (:+:), (:*:)( (:*:) ), M1, U1
  , C, D
  , Meta( MetaData, MetaCons )
  )
import GHC.TypeLits
  ( ErrorMessage( (:<>:), Text ), TypeError
  , Symbol, KnownSymbol, symbolVal
  )
import Prelude hiding ( null )

-- rel8
import Rel8.FCF ( Exp )
import Rel8.Generic.Construction.Record
  ( GConstruct, GConstructable, gconstruct, gdeconstruct
  , GFields, Representable, gtabulate, gindex
  , FromColumns, ToColumns
  )
import Rel8.Generic.Table.ADT ( GColumnsADT, GColumnsADT' )
import Rel8.Generic.Table.Record ( GColumns )
import Rel8.Schema.HTable ( HTable )
import Rel8.Schema.HTable.Identity ( HIdentity )
import Rel8.Schema.HTable.Label ( HLabel, hlabel, hunlabel )
import Rel8.Schema.HTable.Nullify ( HNullify, hnulls, hnullify, hunnullify )
import Rel8.Schema.HTable.Product ( HProduct( HProduct ) )
import Rel8.Schema.Null ( Nullify )
import Rel8.Schema.Spec ( Spec )
import qualified Rel8.Schema.Kind as K
import Rel8.Type.Tag ( Tag( Tag ) )

-- text
import Data.Text ( pack )


type Null :: K.Context -> Type
type Null context = forall a. Spec a -> context (Nullify a)


type Nullifier :: K.Context -> Type
type Nullifier context = forall a. Spec a -> context a -> context (Nullify a)


type Unnullifier :: K.Context -> Type
type Unnullifier context = forall a. Spec a -> context (Nullify a) -> context a


type NoConstructor :: Symbol -> Symbol -> ErrorMessage
type NoConstructor datatype constructor =
  ( 'Text "The type `" ':<>:
    'Text datatype ':<>:
    'Text "` has no constructor `" ':<>:
    'Text constructor ':<>:
    'Text "`."
  )


type GConstructorADT :: Symbol -> (Type -> Type) -> Type -> Type
type family GConstructorADT name rep where
  GConstructorADT name (M1 D ('MetaData datatype _ _ _) rep) =
    GConstructorADT' name rep (TypeError (NoConstructor datatype name))


type GConstructorADT' :: Symbol -> (Type -> Type) -> (Type -> Type) -> Type -> Type
type family GConstructorADT' name rep fallback where
  GConstructorADT' name (M1 D _ rep) fallback =
    GConstructorADT' name rep fallback
  GConstructorADT' name (a :+: b) fallback =
    GConstructorADT' name a (GConstructorADT' name b fallback)
  GConstructorADT' name (M1 C ('MetaCons name _ _) rep) _ = rep
  GConstructorADT' _ _ fallback = fallback


type GConstructADT
  :: (Type -> Exp Type)
  -> (Type -> Type) -> Type -> Type -> Type
type family GConstructADT f rep r x where
  GConstructADT f (M1 D _ rep) r x = GConstructADT f rep r x
  GConstructADT f (a :+: b) r x = GConstructADT f a r (GConstructADT f b r x)
  GConstructADT f (M1 C _ rep) r x = GConstruct f rep r -> x


type GConstructors :: (Type -> Exp Type) -> (Type -> Type) -> Type -> Type
type family GConstructors f rep where
  GConstructors f (M1 D _ rep) = GConstructors f rep
  GConstructors f (a :+: b) = GConstructors f a :*: GConstructors f b
  GConstructors f (M1 C _ rep) = (->) (GFields f rep)


type RepresentableConstructors :: (Type -> Exp Type) -> (Type -> Type) -> Constraint
class RepresentableConstructors f rep where
  gctabulate :: (GConstructors f rep r -> a) -> GConstructADT f rep r a
  gcindex :: GConstructADT f rep r a -> GConstructors f rep r -> a


instance RepresentableConstructors f rep => RepresentableConstructors f (M1 D meta rep) where
  gctabulate = gctabulate @f @rep
  gcindex = gcindex @f @rep


instance (RepresentableConstructors f a, RepresentableConstructors f b) =>
  RepresentableConstructors f (a :+: b)
 where
  gctabulate f =
    gctabulate @f @a \a -> gctabulate @f @b \b -> f (a :*: b)
  gcindex f (a :*: b) = gcindex @f @b (gcindex @f @a f a) b


instance Representable f rep => RepresentableConstructors f (M1 C meta rep) where
  gctabulate f = f . gindex @f @rep
  gcindex f = f . gtabulate @f @rep


type GBuildADT :: (Type -> Exp Type) -> (Type -> Type) -> Type -> Type
type family GBuildADT f rep r where
  GBuildADT f (M1 D _ rep) r = GBuildADT f rep r
  GBuildADT f (a :+: b) r = GBuildADT f a (GBuildADT f b r)
  GBuildADT f (M1 C _ rep) r = GConstruct f rep r


type GFieldsADT :: (Type -> Exp Type) -> (Type -> Type) -> Type
type family GFieldsADT f rep where
  GFieldsADT f (M1 D _ rep) = GFieldsADT f rep
  GFieldsADT f (a :+: b) = (GFieldsADT f a, GFieldsADT f b)
  GFieldsADT f (M1 C _ rep) = GFields f rep


type RepresentableFields :: (Type -> Exp Type) -> (Type -> Type) -> Constraint
class RepresentableFields f rep where
  gftabulate :: (GFieldsADT f rep -> a) -> GBuildADT f rep a
  gfindex :: GBuildADT f rep a -> GFieldsADT f rep -> a


instance RepresentableFields f rep => RepresentableFields f (M1 D meta rep) where
  gftabulate = gftabulate @f @rep
  gfindex = gfindex @f @rep


instance (RepresentableFields f a, RepresentableFields f b) => RepresentableFields f (a :+: b) where
  gftabulate f =
    gftabulate @f @a \a -> gftabulate @f @b \b -> f (a, b)
  gfindex f (a, b) = gfindex @f @b (gfindex @f @a f a) b


instance Representable f rep => RepresentableFields f (M1 C meta rep) where
  gftabulate = gtabulate @f @rep
  gfindex = gindex @f @rep


type GConstructableADT
  :: (Type -> Exp Constraint)
  -> (Type -> Exp K.HTable)
  -> (Type -> Exp Type)
  -> K.Context -> (Type -> Type) -> Constraint
class GConstructableADT _Table _Columns f context rep where
  gbuildADT :: ()
    => ToColumns _Table _Columns f context
    -> (Tag -> Nullifier context)
    -> HIdentity Tag context
    -> GFieldsADT f rep
    -> GColumnsADT _Columns rep context

  gunbuildADT :: ()
    => FromColumns _Table _Columns f context
    -> Unnullifier context
    -> GColumnsADT _Columns rep context
    -> (HIdentity Tag context, GFieldsADT f rep)

  gconstructADT :: ()
    => ToColumns _Table _Columns f context
    -> Null context
    -> Nullifier context
    -> (Tag -> HIdentity Tag context)
    -> GConstructors f rep (GColumnsADT _Columns rep context)

  gdeconstructADT :: ()
    => FromColumns _Table _Columns f context
    -> Unnullifier context
    -> GConstructors f rep r
    -> GColumnsADT _Columns rep context
    -> (HIdentity Tag context, NonEmpty (Tag, r))


instance
  ( htable ~ HLabel "tag" (HIdentity Tag)
  , GConstructableADT' _Table _Columns f context htable rep
  )
  => GConstructableADT _Table _Columns f context (M1 D meta rep)
 where
  gbuildADT toColumns nullifier =
    gbuildADT' @_Table @_Columns @f @context @htable @rep toColumns nullifier .
    hlabel

  gunbuildADT fromColumns unnullifier =
    first hunlabel .
    gunbuildADT' @_Table @_Columns @f @context @htable @rep fromColumns unnullifier

  gconstructADT toColumns null nullifier mk =
    gconstructADT' @_Table @_Columns @f @context @htable @rep toColumns null nullifier
      (hlabel . mk)

  gdeconstructADT fromColumns unnullifier cases =
    first hunlabel .
    gdeconstructADT' @_Table @_Columns @f @context @htable @rep fromColumns unnullifier cases


type GConstructableADT'
  :: (Type -> Exp Constraint)
  -> (Type -> Exp K.HTable)
  -> (Type -> Exp Type)
  -> K.Context -> K.HTable -> (Type -> Type) -> Constraint
class GConstructableADT' _Table _Columns f context htable rep where
  gbuildADT' :: ()
    => ToColumns _Table _Columns f context
    -> (Tag -> Nullifier context)
    -> htable context
    -> GFieldsADT f rep
    -> GColumnsADT' _Columns htable rep context

  gunbuildADT' :: ()
    => FromColumns _Table _Columns f context
    -> Unnullifier context
    -> GColumnsADT' _Columns htable rep context
    -> (htable context, GFieldsADT f rep)

  gconstructADT' :: ()
    => ToColumns _Table _Columns f context
    -> Null context
    -> Nullifier context
    -> (Tag -> htable context)
    -> GConstructors f rep (GColumnsADT' _Columns htable rep context)

  gdeconstructADT' :: ()
    => FromColumns _Table _Columns f context
    -> Unnullifier context
    -> GConstructors f rep r
    -> GColumnsADT' _Columns htable rep context
    -> (htable context, NonEmpty (Tag, r))

  gfill :: ()
    => Null context
    -> htable context
    -> GColumnsADT' _Columns htable rep context


instance
  ( htable' ~ GColumnsADT' _Columns htable a
  , Functor (GConstructors f a)
  , GConstructableADT' _Table _Columns f context htable a
  , GConstructableADT' _Table _Columns f context htable' b
  )
  => GConstructableADT' _Table _Columns f context htable (a :+: b)
 where
  gbuildADT' toColumns nullifier htable (a, b) =
    gbuildADT' @_Table @_Columns @f @context @htable' @b toColumns nullifier
      (gbuildADT' @_Table @_Columns @f @context @htable @a toColumns nullifier htable a)
      b

  gunbuildADT' fromColumns unnullifier columns =
    case gunbuildADT' @_Table @_Columns @f @context @htable' @b fromColumns unnullifier columns of
      (htable', b) ->
        case gunbuildADT' @_Table @_Columns @f @context @htable @a fromColumns unnullifier htable' of
          (htable, a) -> (htable, (a, b))

  gconstructADT' toColumns null nullifier mk =
    fmap (gfill @_Table @_Columns @f @context @htable' @b null) (gconstructADT' @_Table @_Columns @f @context @htable @a toColumns null nullifier mk) :*:
    gconstructADT' @_Table @_Columns @f @context @htable' @b toColumns null nullifier (gfill @_Table @_Columns @f @context @htable @a null . mk)

  gdeconstructADT' fromColumns unnullifier (a :*: b) columns =
    case gdeconstructADT' @_Table @_Columns @f @context @htable' @b fromColumns unnullifier b columns of
      (htable', cases) ->
        case gdeconstructADT' @_Table @_Columns @f @context @htable @a fromColumns unnullifier a htable' of
          (htable, cases') -> (htable, cases' <> cases)

  gfill null =
    gfill @_Table @_Columns @f @context @htable' @b null .
    gfill @_Table @_Columns @f @context @htable @a null


instance (meta ~ 'MetaCons label _fixity _isRecord, KnownSymbol label) =>
  GConstructableADT' _Table _Columns f context htable (M1 C meta U1)
 where
  gbuildADT' _ _ = const
  gunbuildADT' _ _ = (, ())
  gconstructADT' _ _ _ f _ = f tag
    where
      tag = Tag $ pack $ symbolVal (Proxy @label)
  gdeconstructADT' _ _ r htable = (htable, pure (tag, r ()))
    where
      tag = Tag $ pack $ symbolVal (Proxy @label)
  gfill _ = id


instance {-# OVERLAPPABLE #-}
  ( HTable (GColumns _Columns rep)
  , KnownSymbol label
  , meta ~ 'MetaCons label _fixity _isRecord
  , GConstructable _Table _Columns f context rep
  , GColumnsADT' _Columns htable (M1 C meta rep) ~
      HProduct htable (HLabel label (HNullify (GColumns _Columns rep)))
  )
  => GConstructableADT' _Table _Columns f context htable (M1 C meta rep)
 where
  gbuildADT' toColumns nullifier htable =
    HProduct htable .
    hlabel .
    hnullify (nullifier tag) .
    gconstruct @_Table @_Columns @f @context @rep toColumns
    where
      tag = Tag $ pack $ symbolVal (Proxy @label)

  gunbuildADT' fromColumns unnullifier (HProduct htable a) =
    ( htable
    , gdeconstruct @_Table @_Columns @f @context @rep fromColumns $
        runIdentity $
        hunnullify (\spec -> pure . unnullifier spec) $
        hunlabel
        a
    )

  gconstructADT' toColumns _ nullifier mk =
    HProduct htable .
    hlabel .
    hnullify nullifier .
    gconstruct @_Table @_Columns @f @context @rep toColumns
    where
      tag = Tag $ pack $ symbolVal (Proxy @label)
      htable = mk tag

  gdeconstructADT' fromColumns unnullifier r (HProduct htable columns) =
    ( htable
    , pure (tag, r a)
    )
    where
      a = gdeconstruct @_Table @_Columns @f @context @rep fromColumns $
        runIdentity $
        hunnullify (\spec -> pure . unnullifier spec) $
        hunlabel
        columns
      tag = Tag $ pack $ symbolVal (Proxy @label)

  gfill null htable = HProduct htable (hlabel (hnulls null))


type GMakeableADT
  :: (Type -> Exp Constraint)
  -> (Type -> Exp K.HTable)
  -> (Type -> Exp Type)
  -> K.Context -> Symbol -> (Type -> Type) -> Constraint
class GMakeableADT _Table _Columns f context name rep where
  gmakeADT :: ()
    => ToColumns _Table _Columns f context
    -> Null context
    -> Nullifier context
    -> (Tag -> HIdentity Tag context)
    -> GFields f (GConstructorADT name rep)
    -> GColumnsADT _Columns rep context


instance
  ( htable ~ HLabel "tag" (HIdentity Tag)
  , meta ~ 'MetaData datatype _module _package _newtype
  , fallback ~ TypeError (NoConstructor datatype name)
  , fields ~ GFields f (GConstructorADT' name rep fallback)
  , GMakeableADT' _Table _Columns f context htable name rep fields
  , KnownSymbol name
  )
  => GMakeableADT _Table _Columns f context name (M1 D meta rep)
 where
  gmakeADT toColumns null nullifier wrap =
    gmakeADT'
      @_Table @_Columns @f @context @htable @name @rep @fields
      toColumns null nullifier htable
    where
      tag = Tag $ pack $ symbolVal (Proxy @name)
      htable = hlabel (wrap tag)


type GMakeableADT'
  :: (Type -> Exp Constraint)
  -> (Type -> Exp K.HTable)
  -> (Type -> Exp Type)
  -> K.Context -> K.HTable -> Symbol -> (Type -> Type) -> Type -> Constraint
class GMakeableADT' _Table _Columns f context htable name rep fields where
  gmakeADT' :: ()
    => ToColumns _Table _Columns f context
    -> Null context
    -> Nullifier context
    -> htable context
    -> fields
    -> GColumnsADT' _Columns htable rep context


instance
  ( htable' ~ GColumnsADT' _Columns htable a
  , GMakeableADT' _Table _Columns f context htable name a fields
  , GMakeableADT' _Table _Columns f context htable' name b fields
  )
  => GMakeableADT' _Table _Columns f context htable name (a :+: b) fields
 where
  gmakeADT' toColumns null nullifier htable x =
    gmakeADT' @_Table @_Columns @f @context @htable' @name @b @fields
      toColumns null nullifier
      (gmakeADT'
         @_Table @_Columns @f @context @htable @name @a @fields toColumns
         null nullifier htable x)
      x


instance {-# OVERLAPPING #-}
  GMakeableADT' _Table _Columns f context htable name (M1 C ('MetaCons name _fixity _isRecord) U1) fields
 where
  gmakeADT' _ _ _ = const


instance {-# OVERLAPS #-}
  GMakeableADT' _Table _Columns f context htable name (M1 C ('MetaCons label _fixity _isRecord) U1) fields
 where
  gmakeADT' _ _ _ = const


instance {-# OVERLAPS #-}
  ( HTable (GColumns _Columns rep)
  , GConstructable _Table _Columns f context rep
  , fields ~ GFields f rep
  , GColumnsADT' _Columns htable (M1 C ('MetaCons name _fixity _isRecord) rep) ~
      HProduct htable (HLabel name (HNullify (GColumns _Columns rep)))
  )
  => GMakeableADT' _Table _Columns f context htable name (M1 C ('MetaCons name _fixity _isRecord) rep) fields
 where
  gmakeADT' toColumns _ nullifier htable =
    HProduct htable .
    hlabel .
    hnullify nullifier .
    gconstruct @_Table @_Columns @f @context @rep toColumns


instance {-# OVERLAPPABLE #-}
  ( HTable (GColumns _Columns rep)
  , GColumnsADT' _Columns htable (M1 C ('MetaCons label _fixity _isRecord) rep) ~
      HProduct htable (HLabel label (HNullify (GColumns _Columns rep)))
  )
  => GMakeableADT' _Table _Columns f context htable name (M1 C ('MetaCons label _fixity _isRecord) rep) fields
 where
  gmakeADT' _ null _ htable _ =
    HProduct htable $
    hlabel $
    hnulls null