{-# language AllowAmbiguousTypes #-}
{-# language DataKinds #-}
{-# language FlexibleContexts #-}
{-# language FlexibleInstances #-}
{-# language MultiParamTypeClasses #-}
{-# language RankNTypes #-}
{-# language ScopedTypeVariables #-}
{-# language StandaloneKindSignatures #-}
{-# language TypeApplications #-}
{-# language TypeFamilyDependencies #-}
{-# language UndecidableInstances #-}
{-# language UndecidableSuperClasses #-}

module Rel8.Table.ADT
  ( ADT( ADT )
  , ADTable
  , BuildableADT
  , BuildADT, buildADT
  , ConstructableADT
  , ConstructADT, constructADT
  , DeconstructADT, deconstructADT
  , NameADT, nameADT
  , AggregateADT, aggregateADT
  , ADTRep
  )
where

-- base
import Data.Kind ( Constraint, Type )
import GHC.Generics ( Generic, from, to )
import GHC.TypeLits ( Symbol )
import Prelude

-- rel8
import Rel8.Aggregate ( Aggregate )
import Rel8.Expr ( Expr )
import Rel8.FCF ( Eval, Exp )
import Rel8.Generic.Construction
  ( GGBuildable
  , GGBuild, ggbuild
  , GGConstructable
  , GGConstruct, ggconstruct
  , GGDeconstruct, ggdeconstruct
  , GGName, ggname
  , GGAggregate, ggaggregate
  )
import Rel8.Generic.Record ( Record( Record ), unrecord )
import Rel8.Generic.Rel8able
  ( Rel8able
  , GRep, GColumns, gfromColumns, gtoColumns
  , GFromExprs, gfromResult, gtoResult
  , TSerialize, deserialize, serialize
  )
import qualified Rel8.Generic.Table.ADT as G
import qualified Rel8.Kind.Algebra as K
import Rel8.Schema.HTable ( HTable )
import qualified Rel8.Schema.Kind as K
import Rel8.Schema.Name ( Name )
import Rel8.Schema.Result ( Result )
import Rel8.Table ( Table, TColumns )


type ADT :: K.Rel8able -> K.Rel8able
newtype ADT t context = ADT (GColumnsADT t context)


instance ADTable t => Rel8able (ADT t) where
  type GColumns (ADT t) = GColumnsADT t
  type GFromExprs (ADT t) = t Result

  gfromColumns :: SContext context -> GColumns (ADT t) context -> ADT t context
gfromColumns SContext context
_ = GColumns (ADT t) context -> ADT t context
forall (t :: Rel8able) (context :: Context).
GColumnsADT t context -> ADT t context
ADT
  gtoColumns :: SContext context -> ADT t context -> GColumns (ADT t) context
gtoColumns SContext context
_ (ADT GColumnsADT t context
a) = GColumnsADT t context
GColumns (ADT t) context
a

  gfromResult :: GColumns (ADT t) Result -> GFromExprs (ADT t)
gfromResult =
    Record (t Result) -> t Result
forall a. Record a -> a
unrecord (Record (t Result) -> t Result)
-> (GColumnsADT TColumns (GRecord (Rep (t Expr))) Result
    -> Record (t Result))
-> GColumnsADT TColumns (GRecord (Rep (t Expr))) Result
-> t Result
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    GRecord (Rep (t Result)) Any -> Record (t Result)
forall a x. Generic a => Rep a x -> a
to (GRecord (Rep (t Result)) Any -> Record (t Result))
-> (GColumnsADT TColumns (GRecord (Rep (t Expr))) Result
    -> GRecord (Rep (t Result)) Any)
-> GColumnsADT TColumns (GRecord (Rep (t Expr))) Result
-> Record (t Result)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    (forall expr a (proxy :: Context).
 Eval (TSerialize expr a) =>
 proxy expr -> Eval (TColumns expr) Result -> a)
-> GColumnsADT TColumns (Eval (ADTRep t Expr)) Result
-> Eval (ADTRep t Result) Any
forall (_Serialize :: * -> * -> Exp Constraint)
       (_Columns :: * -> Exp Rel8able) (exprs :: Context) (rep :: Context)
       x.
GSerializeADT _Serialize _Columns exprs rep =>
(forall expr a (proxy :: Context).
 Eval (_Serialize expr a) =>
 proxy expr -> Eval (_Columns expr) Result -> a)
-> GColumnsADT _Columns exprs Result -> rep x
G.gfromResultADT
      @TSerialize
      @TColumns
      @(Eval (ADTRep t Expr))
      @(Eval (ADTRep t Result))
      (\(proxy expr
_ :: proxy x) -> forall (transposition :: Bool) expr a.
Serialize transposition expr a =>
Columns expr Result -> a
forall a.
Serialize (a == Transpose Result expr) expr a =>
Columns expr Result -> a
deserialize @_ @x)

  gtoResult :: GFromExprs (ADT t) -> GColumns (ADT t) Result
gtoResult =
    (forall expr a (proxy :: Context).
 Eval (TSerialize expr a) =>
 proxy expr -> a -> Eval (TColumns expr) Result)
-> Eval (ADTRep t Result) Any
-> GColumnsADT TColumns (Eval (ADTRep t Expr)) Result
forall (_Serialize :: * -> * -> Exp Constraint)
       (_Columns :: * -> Exp Rel8able) (exprs :: Context) (rep :: Context)
       x.
GSerializeADT _Serialize _Columns exprs rep =>
(forall expr a (proxy :: Context).
 Eval (_Serialize expr a) =>
 proxy expr -> a -> Eval (_Columns expr) Result)
-> rep x -> GColumnsADT _Columns exprs Result
G.gtoResultADT
      @TSerialize
      @TColumns
      @(Eval (ADTRep t Expr))
      @(Eval (ADTRep t Result))
      (\(proxy expr
_ :: proxy x) -> forall (transposition :: Bool) expr a.
Serialize transposition expr a =>
a -> Columns expr Result
forall a.
Serialize (a == Transpose Result expr) expr a =>
a -> Columns expr Result
serialize @_ @x) (GRecord (Rep (t Result)) Any
 -> GColumnsADT TColumns (GRecord (Rep (t Expr))) Result)
-> (t Result -> GRecord (Rep (t Result)) Any)
-> t Result
-> GColumnsADT TColumns (GRecord (Rep (t Expr))) Result
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Record (t Result) -> GRecord (Rep (t Result)) Any
forall a x. Generic a => a -> Rep a x
from (Record (t Result) -> GRecord (Rep (t Result)) Any)
-> (t Result -> Record (t Result))
-> t Result
-> GRecord (Rep (t Result)) Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    t Result -> Record (t Result)
forall a. a -> Record a
Record


type ADTable :: K.Rel8able -> Constraint
class
  ( Generic (Record (t Result))
  , HTable (GColumnsADT t)
  , G.GSerializeADT TSerialize TColumns (Eval (ADTRep t Expr)) (Eval (ADTRep t Result))
  )
  => ADTable t
instance
  ( Generic (Record (t Result))
  , HTable (GColumnsADT t)
  , G.GSerializeADT TSerialize TColumns (Eval (ADTRep t Expr)) (Eval (ADTRep t Result))
  )
  => ADTable t


type BuildableADT :: K.Rel8able -> Symbol -> Constraint
class GGBuildable 'K.Sum name (ADTRep t) => BuildableADT t name
instance GGBuildable 'K.Sum name (ADTRep t) => BuildableADT t name


type BuildADT :: K.Rel8able -> Symbol -> Type
type BuildADT t name = GGBuild 'K.Sum name (ADTRep t) (ADT t Expr)


buildADT :: forall t name. BuildableADT t name => BuildADT t name
buildADT :: BuildADT t name
buildADT =
  (Eval (GGColumns 'Sum TColumns (Eval (ADTRep t Expr))) Expr
 -> ADT t Expr)
-> BuildADT t name
forall (algebra :: Algebra) (name :: Symbol)
       (rep :: Context -> Rel8able) a.
GGBuildable algebra name rep =>
(Eval (GGColumns algebra TColumns (Eval (rep Expr))) Expr -> a)
-> GGBuild algebra name rep a
ggbuild @'K.Sum @name @(ADTRep t) @(ADT t Expr) Eval (GGColumns 'Sum TColumns (Eval (ADTRep t Expr))) Expr
-> ADT t Expr
forall (t :: Rel8able) (context :: Context).
GColumnsADT t context -> ADT t context
ADT


type ConstructableADT :: K.Rel8able -> Constraint
class GGConstructable 'K.Sum (ADTRep t) => ConstructableADT t
instance GGConstructable 'K.Sum (ADTRep t) => ConstructableADT t


type ConstructADT :: K.Rel8able -> Type
type ConstructADT t = forall r. GGConstruct 'K.Sum (ADTRep t) r


constructADT :: forall t. ConstructableADT t => ConstructADT t -> ADT t Expr
constructADT :: ConstructADT t -> ADT t Expr
constructADT ConstructADT t
f =
  (Eval (GGColumns 'Sum TColumns (Eval (ADTRep t Expr))) Expr
 -> ADT t Expr)
-> GGConstruct 'Sum (ADTRep t) (ADT t Expr) -> ADT t Expr
forall (algebra :: Algebra) (rep :: Context -> Rel8able) a.
GGConstructable algebra rep =>
(Eval (GGColumns algebra TColumns (Eval (rep Expr))) Expr -> a)
-> GGConstruct algebra rep a -> a
ggconstruct @'K.Sum @(ADTRep t) @(ADT t Expr) Eval (GGColumns 'Sum TColumns (Eval (ADTRep t Expr))) Expr
-> ADT t Expr
forall (t :: Rel8able) (context :: Context).
GColumnsADT t context -> ADT t context
ADT
    (GGConstruct 'Sum (ADTRep t) (ADT t Expr)
ConstructADT t
f @(ADT t Expr))


type DeconstructADT :: K.Rel8able -> Type -> Type
type DeconstructADT t r = GGDeconstruct 'K.Sum (ADTRep t) (ADT t Expr) r


deconstructADT :: forall t r. (ConstructableADT t, Table Expr r)
  => DeconstructADT t r
deconstructADT :: DeconstructADT t r
deconstructADT =
  (ADT t Expr
 -> Eval (GGColumns 'Sum TColumns (Eval (ADTRep t Expr))) Expr)
-> DeconstructADT t r
forall (algebra :: Algebra) (rep :: Context -> Rel8able) a r.
(GGConstructable algebra rep, Table Expr r) =>
(a -> Eval (GGColumns algebra TColumns (Eval (rep Expr))) Expr)
-> GGDeconstruct algebra rep a r
ggdeconstruct @'K.Sum @(ADTRep t) @(ADT t Expr) @r (\(ADT GColumnsADT t Expr
a) -> Eval (GGColumns 'Sum TColumns (Eval (ADTRep t Expr))) Expr
GColumnsADT t Expr
a)


type NameADT :: K.Rel8able -> Type
type NameADT t = GGName 'K.Sum (ADTRep t) (ADT t Name)


nameADT :: forall t. ConstructableADT t => NameADT t
nameADT :: NameADT t
nameADT = (Eval (GGColumns 'Sum TColumns (Eval (ADTRep t Expr))) Name
 -> ADT t Name)
-> NameADT t
forall (algebra :: Algebra) (rep :: Context -> Rel8able) a.
GGConstructable algebra rep =>
(Eval (GGColumns algebra TColumns (Eval (rep Expr))) Name -> a)
-> GGName algebra rep a
ggname @'K.Sum @(ADTRep t) @(ADT t Name) Eval (GGColumns 'Sum TColumns (Eval (ADTRep t Expr))) Name
-> ADT t Name
forall (t :: Rel8able) (context :: Context).
GColumnsADT t context -> ADT t context
ADT


type AggregateADT :: K.Rel8able -> Type
type AggregateADT t = forall r. GGAggregate 'K.Sum (ADTRep t) r


aggregateADT :: forall t. ConstructableADT t
  => AggregateADT t -> ADT t Expr -> ADT t Aggregate
aggregateADT :: AggregateADT t -> ADT t Expr -> ADT t Aggregate
aggregateADT AggregateADT t
f =
  (Eval (GGColumns 'Sum TColumns (Eval (ADTRep t Expr))) Aggregate
 -> ADT t Aggregate)
-> (ADT t Expr
    -> Eval (GGColumns 'Sum TColumns (Eval (ADTRep t Expr))) Expr)
-> GGAggregate 'Sum (ADTRep t) (ADT t Aggregate)
-> ADT t Expr
-> ADT t Aggregate
forall (algebra :: Algebra) (rep :: Context -> Rel8able) exprs agg.
GGConstructable algebra rep =>
(Eval (GGColumns algebra TColumns (Eval (rep Expr))) Aggregate
 -> agg)
-> (exprs
    -> Eval (GGColumns algebra TColumns (Eval (rep Expr))) Expr)
-> GGAggregate algebra rep agg
-> exprs
-> agg
ggaggregate @'K.Sum @(ADTRep t) @(ADT t Expr) @(ADT t Aggregate) Eval (GGColumns 'Sum TColumns (Eval (ADTRep t Expr))) Aggregate
-> ADT t Aggregate
forall (t :: Rel8able) (context :: Context).
GColumnsADT t context -> ADT t context
ADT (\(ADT GColumnsADT t Expr
a) -> Eval (GGColumns 'Sum TColumns (Eval (ADTRep t Expr))) Expr
GColumnsADT t Expr
a)
    (GGAggregate 'Sum (ADTRep t) (ADT t Aggregate)
AggregateADT t
f @(ADT t Aggregate))


data ADTRep :: K.Rel8able -> K.Context -> Exp (Type -> Type)
type instance Eval (ADTRep t context) = GRep t context


type GColumnsADT :: K.Rel8able -> K.HTable
type GColumnsADT t = G.GColumnsADT TColumns (GRep t Expr)