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

module Rel8.Table.HKD
  ( HKD( HKD )
  , HKDable, fromHKD, toHKD, HKDT(..)
  , BuildableHKD
  , BuildHKD, buildHKD
  , ConstructableHKD
  , ConstructHKD, constructHKD
  , DeconstructHKD, deconstructHKD
  , NameHKD, nameHKD
  , AggregateHKD, aggregateHKD
  , HKDRep
  )
where

-- base
import Data.Kind ( Constraint, Type )
import Data.Proxy ( Proxy( Proxy ) )
import Data.Type.Equality ( (:~:)( Refl ) )
import Data.Void ( Void )
import GHC.Generics ( Generic, Rep, from, to )
import GHC.TypeLits ( Symbol )
import Prelude

-- rel8
import Rel8.Aggregate ( Aggregate )
import Rel8.Column ( TColumn )
import Rel8.Expr ( Expr )
import Rel8.FCF ( Eval, Exp )
import Rel8.Kind.Algebra ( KnownAlgebra )
import Rel8.Generic.Construction
  ( GGBuildable
  , GGBuild, ggbuild
  , GGConstructable
  , GGConstruct, ggconstruct
  , GGDeconstruct, ggdeconstruct
  , GGName, ggname
  , GGAggregate, ggaggregate
  )
import Rel8.Generic.Map ( GMap, GMappable, gmap, gunmap )
import Rel8.Generic.Record ( GRecord, GRecordable, grecord, gunrecord )
import Rel8.Generic.Rel8able
  ( Rel8able
  , GColumns, gfromColumns, gtoColumns
  , greify, gunreify
  , TUnreifyContext
  )
import Rel8.Generic.Table
  ( GGTable, GGColumns, GGContext, ggfromColumns, ggtoColumns
  , GAlgebra
  )
import Rel8.Schema.Context ( Col )
import qualified Rel8.Schema.Kind as K
import Rel8.Schema.HTable ( HTable )
import Rel8.Schema.Name ( Name )
import Rel8.Schema.Reify ( Col( Reify ), Reify, hreify, hunreify, notReify )
import Rel8.Schema.Result ( Result )
import Rel8.Table
  ( Table, Columns, Context, Unreify
  , fromColumns, toColumns, reify, unreify
  , TTable, TColumns, TUnreify
  )
import Rel8.Table.Serialize ( ToExprs, fromResult, toResult )


type GColumnsHKD :: Type -> K.HTable
type GColumnsHKD a =
  Eval (GGColumns (GAlgebra (Rep a)) TColumns (GRecord (GMap (TColumn (Reify Result)) (Rep a))))


type HKD :: Type -> K.Rel8able
newtype HKD a f = HKD (GColumnsHKD a (Col f))


instance HKDable a => Rel8able (HKD a) where
  type GColumns (HKD a) = GColumnsHKD a

  gfromColumns :: GColumns (HKD a) (Col (Reify context)) -> HKD a (Reify context)
gfromColumns = GColumns (HKD a) (Col (Reify context)) -> HKD a (Reify context)
forall a (f :: Context). GColumnsHKD a (Col f) -> HKD a f
HKD
  gtoColumns :: HKD a (Reify context) -> GColumns (HKD a) (Col (Reify context))
gtoColumns (HKD GColumnsHKD a (Col (Reify context))
a) = GColumnsHKD a (Col (Reify context))
GColumns (HKD a) (Col (Reify context))
a

  greify :: HKD a context -> HKD a (Reify context)
greify (HKD GColumnsHKD a (Col context)
a) = GColumnsHKD a (Col (Reify context)) -> HKD a (Reify context)
forall a (f :: Context). GColumnsHKD a (Col f) -> HKD a f
HKD (GColumnsHKD a (Col context) -> GColumnsHKD a (Col (Reify context))
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col context) -> t (Col (Reify context))
hreify GColumnsHKD a (Col context)
a)
  gunreify :: HKD a (Reify context) -> HKD a context
gunreify (HKD GColumnsHKD a (Col (Reify context))
a) = GColumnsHKD a (Col context) -> HKD a context
forall a (f :: Context). GColumnsHKD a (Col f) -> HKD a f
HKD (GColumnsHKD a (Col (Reify context)) -> GColumnsHKD a (Col context)
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col (Reify context)) -> t (Col context)
hunreify GColumnsHKD a (Col (Reify context))
a)


instance
  ( KnownAlgebra (GAlgebra (Rep a))
  , HTable (GColumnsHKD a)
  , Eval (GGTable (GAlgebra (Rep a)) (TTable (Reify f)) TColumns (Col (Reify f)) (GRecord (GMap (TColumn (Reify f)) (Rep a))))
  , Eval (GGColumns (GAlgebra (Rep a)) TColumns (GRecord (GMap (TColumn (Reify f)) (Rep a)))) ~ GColumnsHKD a
  , Eval (GGContext (GAlgebra (Rep a)) TUnreifyContext (GRecord (GMap (TColumn (Reify f)) (Rep a)))) ~ f
  , GRecordable (GMap (TColumn (Reify f)) (Rep a))
  , GMappable (TTable (Reify f)) (GMap (TColumn (Reify f)) (Rep a))
  , GMap TUnreify (GMap (TColumn (Reify f)) (Rep a)) ~ GMap (TColumn f) (Rep a)
  )
  => Generic (HKD a f)
 where
  type Rep (HKD a f) = GMap (TColumn f) (Rep a)

  from :: HKD a f -> Rep (HKD a f) x
from =
    Proxy TUnreify
-> (forall a. Eval (TTable (Reify f) a) => a -> Eval (TUnreify a))
-> GMap (TColumn (Reify f)) (Rep a) x
-> GMap TUnreify (GMap (TColumn (Reify f)) (Rep a)) x
forall (constraint :: * -> Exp Constraint) (rep :: * -> *)
       (proxy :: (* -> * -> *) -> *) (f :: * -> * -> *) x.
GMappable constraint rep =>
proxy f
-> (forall a. Eval (constraint a) => a -> Eval (f a))
-> rep x
-> GMap f rep x
gmap @(TTable (Reify f)) (Proxy TUnreify
forall k (t :: k). Proxy t
Proxy @TUnreify) ((Reify f :~: Reify f) -> a -> Unreify a
forall (context :: Context) a (ctx :: Context).
Table context a =>
(context :~: Reify ctx) -> a -> Unreify a
unreify Reify f :~: Reify f
forall k (a :: k). a :~: a
Refl) (GMap (TColumn (Reify f)) (Rep a) x -> GMap (TColumn f) (Rep a) x)
-> (HKD a f -> GMap (TColumn (Reify f)) (Rep a) x)
-> HKD a f
-> GMap (TColumn f) (Rep a) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    forall x.
GRecordable (GMap (TColumn (Reify f)) (Rep a)) =>
GRecord (GMap (TColumn (Reify f)) (Rep a)) x
-> GMap (TColumn (Reify f)) (Rep a) x
forall (rep :: * -> *) x. GRecordable rep => GRecord rep x -> rep x
gunrecord @(GMap (TColumn (Reify f)) (Rep a)) (GRecord (GMap (TColumn (Reify f)) (Rep a)) x
 -> GMap (TColumn (Reify f)) (Rep a) x)
-> (HKD a f -> GRecord (GMap (TColumn (Reify f)) (Rep a)) x)
-> HKD a f
-> GMap (TColumn (Reify f)) (Rep a) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    (forall (spec :: Spec).
 (GAlgebra (Rep a) ~ 'Sum) =>
 Col (Reify f) spec -> Col Result spec)
-> (forall (spec :: Spec).
    (GAlgebra (Rep a) ~ 'Sum) =>
    Col Result spec -> Col (Reify f) spec)
-> (forall a.
    Eval (TTable (Reify f) a) =>
    Eval (TColumns a) (Col (Reify f)) -> a)
-> Eval
     (GGColumns
        (GAlgebra (Rep a))
        TColumns
        (GRecord (GMap (TColumn (Reify f)) (Rep a))))
     (Col (Reify f))
-> GRecord (GMap (TColumn (Reify f)) (Rep a)) x
forall (algebra :: Algebra) (_Table :: * -> Exp Constraint)
       (_Columns :: * -> Exp HTable) (rep :: * -> *) (context :: HContext)
       x.
(KnownAlgebra algebra,
 Eval (GGTable algebra _Table _Columns context rep)) =>
(forall (spec :: Spec).
 (algebra ~ 'Sum) =>
 context spec -> Col Result spec)
-> (forall (spec :: Spec).
    (algebra ~ 'Sum) =>
    Col Result spec -> context spec)
-> (forall a. Eval (_Table a) => Eval (_Columns a) context -> a)
-> Eval (GGColumns algebra _Columns rep) context
-> rep x
ggfromColumns
      @(GAlgebra (Rep a))
      @(TTable (Reify f))
      @TColumns
      (\(Reify a) -> Col Result spec
a)
      forall (spec :: Spec).
(GAlgebra (Rep a) ~ 'Sum) =>
Col Result spec -> Col (Reify f) spec
forall (context :: Context) (spec :: Spec).
Col context spec -> Col (Reify context) spec
Reify
      forall a.
Eval (TTable (Reify f) a) =>
Eval (TColumns a) (Col (Reify f)) -> a
forall (context :: Context) a.
Table context a =>
Columns a (Col context) -> a
fromColumns (Eval
   (GGColumns
      (GAlgebra (Rep a))
      TColumns
      (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
   (Col (Reify f))
 -> GRecord (GMap (TColumn (Reify f)) (Rep a)) x)
-> (HKD a f
    -> Eval
         (GGColumns
            (GAlgebra (Rep a))
            TColumns
            (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
         (Col (Reify f)))
-> HKD a f
-> GRecord (GMap (TColumn (Reify f)) (Rep a)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Eval
  (GGColumns
     (GAlgebra (Rep a))
     TColumns
     (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
  (Col f)
-> Eval
     (GGColumns
        (GAlgebra (Rep a))
        TColumns
        (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
     (Col (Reify f))
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col context) -> t (Col (Reify context))
hreify (Eval
   (GGColumns
      (GAlgebra (Rep a))
      TColumns
      (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
   (Col f)
 -> Eval
      (GGColumns
         (GAlgebra (Rep a))
         TColumns
         (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
      (Col (Reify f)))
-> (HKD a f
    -> Eval
         (GGColumns
            (GAlgebra (Rep a))
            TColumns
            (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
         (Col f))
-> HKD a f
-> Eval
     (GGColumns
        (GAlgebra (Rep a))
        TColumns
        (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
     (Col (Reify f))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    (\(HKD Eval
  (GGColumns
     (GAlgebra (Rep a))
     TColumns
     (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
  (Col f)
a) -> Eval
  (GGColumns
     (GAlgebra (Rep a))
     TColumns
     (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
  (Col f)
a)

  to :: Rep (HKD a f) x -> HKD a f
to =
    Eval
  (GGColumns
     (GAlgebra (Rep a))
     TColumns
     (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
  (Col f)
-> HKD a f
forall a (f :: Context). GColumnsHKD a (Col f) -> HKD a f
HKD (Eval
   (GGColumns
      (GAlgebra (Rep a))
      TColumns
      (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
   (Col f)
 -> HKD a f)
-> (GMap (TColumn f) (Rep a) x
    -> Eval
         (GGColumns
            (GAlgebra (Rep a))
            TColumns
            (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
         (Col f))
-> GMap (TColumn f) (Rep a) x
-> HKD a f
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Eval
  (GGColumns
     (GAlgebra (Rep a))
     TColumns
     (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
  (Col (Reify f))
-> Eval
     (GGColumns
        (GAlgebra (Rep a))
        TColumns
        (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
     (Col f)
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col (Reify context)) -> t (Col context)
hunreify (Eval
   (GGColumns
      (GAlgebra (Rep a))
      TColumns
      (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
   (Col (Reify f))
 -> Eval
      (GGColumns
         (GAlgebra (Rep a))
         TColumns
         (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
      (Col f))
-> (GMap (TColumn f) (Rep a) x
    -> Eval
         (GGColumns
            (GAlgebra (Rep a))
            TColumns
            (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
         (Col (Reify f)))
-> GMap (TColumn f) (Rep a) x
-> Eval
     (GGColumns
        (GAlgebra (Rep a))
        TColumns
        (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
     (Col f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    (forall (spec :: Spec).
 (GAlgebra (Rep a) ~ 'Sum) =>
 Col (Reify f) spec -> Col Result spec)
-> (forall (spec :: Spec).
    (GAlgebra (Rep a) ~ 'Sum) =>
    Col Result spec -> Col (Reify f) spec)
-> (forall a.
    Eval (TTable (Reify f) a) =>
    a -> Eval (TColumns a) (Col (Reify f)))
-> GRecord (GMap (TColumn (Reify f)) (Rep a)) x
-> Eval
     (GGColumns
        (GAlgebra (Rep a))
        TColumns
        (GRecord (GMap (TColumn (Reify f)) (Rep a))))
     (Col (Reify f))
forall (algebra :: Algebra) (_Table :: * -> Exp Constraint)
       (_Columns :: * -> Exp HTable) (rep :: * -> *) (context :: HContext)
       x.
(KnownAlgebra algebra,
 Eval (GGTable algebra _Table _Columns context rep)) =>
(forall (spec :: Spec).
 (algebra ~ 'Sum) =>
 context spec -> Col Result spec)
-> (forall (spec :: Spec).
    (algebra ~ 'Sum) =>
    Col Result spec -> context spec)
-> (forall a. Eval (_Table a) => a -> Eval (_Columns a) context)
-> rep x
-> Eval (GGColumns algebra _Columns rep) context
ggtoColumns
      @(GAlgebra (Rep a))
      @(TTable (Reify f))
      @TColumns
      (\(Reify a) -> Col Result spec
a)
      forall (spec :: Spec).
(GAlgebra (Rep a) ~ 'Sum) =>
Col Result spec -> Col (Reify f) spec
forall (context :: Context) (spec :: Spec).
Col context spec -> Col (Reify context) spec
Reify
      forall a.
Eval (TTable (Reify f) a) =>
a -> Eval (TColumns a) (Col (Reify f))
forall (context :: Context) a.
Table context a =>
a -> Columns a (Col context)
toColumns (GRecord (GMap (TColumn (Reify f)) (Rep a)) x
 -> Eval
      (GGColumns
         (GAlgebra (Rep a))
         TColumns
         (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
      (Col (Reify f)))
-> (GMap (TColumn f) (Rep a) x
    -> GRecord (GMap (TColumn (Reify f)) (Rep a)) x)
-> GMap (TColumn f) (Rep a) x
-> Eval
     (GGColumns
        (GAlgebra (Rep a))
        TColumns
        (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
     (Col (Reify f))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    forall x.
GRecordable (GMap (TColumn (Reify f)) (Rep a)) =>
GMap (TColumn (Reify f)) (Rep a) x
-> GRecord (GMap (TColumn (Reify f)) (Rep a)) x
forall (rep :: * -> *) x. GRecordable rep => rep x -> GRecord rep x
grecord @(GMap (TColumn (Reify f)) (Rep a)) (GMap (TColumn (Reify f)) (Rep a) x
 -> GRecord (GMap (TColumn (Reify f)) (Rep a)) x)
-> (GMap (TColumn f) (Rep a) x
    -> GMap (TColumn (Reify f)) (Rep a) x)
-> GMap (TColumn f) (Rep a) x
-> GRecord (GMap (TColumn (Reify f)) (Rep a)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Proxy TUnreify
-> (forall a. Eval (TTable (Reify f) a) => Eval (TUnreify a) -> a)
-> GMap TUnreify (GMap (TColumn (Reify f)) (Rep a)) x
-> GMap (TColumn (Reify f)) (Rep a) x
forall (constraint :: * -> Exp Constraint) (rep :: * -> *)
       (proxy :: (* -> * -> *) -> *) (f :: * -> * -> *) x.
GMappable constraint rep =>
proxy f
-> (forall a. Eval (constraint a) => Eval (f a) -> a)
-> GMap f rep x
-> rep x
gunmap @(TTable (Reify f)) (Proxy TUnreify
forall k (t :: k). Proxy t
Proxy @TUnreify) ((Reify f :~: Reify f) -> Unreify a -> a
forall (context :: Context) a (ctx :: Context).
Table context a =>
(context :~: Reify ctx) -> Unreify a -> a
reify Reify f :~: Reify f
forall k (a :: k). a :~: a
Refl)


type HKDT :: Type -> Type
newtype HKDT a = HKDT
  { HKDT a -> a
unHKDT :: a
  }


instance HKDable a => Table Result (HKDT a) where
  type Columns (HKDT a) = GColumnsHKD a
  type Context (HKDT a) = Result
  type Unreify (HKDT a) = Void

  fromColumns :: Columns (HKDT a) (Col Result) -> HKDT a
fromColumns = a -> HKDT a
forall a. a -> HKDT a
HKDT (a -> HKDT a)
-> (Eval
      (GGColumns
         (GAlgebra (Rep a))
         TColumns
         (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
      (Col Result)
    -> a)
-> Eval
     (GGColumns
        (GAlgebra (Rep a))
        TColumns
        (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
     (Col Result)
-> HKDT a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HKD a Result -> a
forall a. HKDable a => HKD a Result -> a
fromHKD (HKD a Result -> a)
-> (Eval
      (GGColumns
         (GAlgebra (Rep a))
         TColumns
         (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
      (Col Result)
    -> HKD a Result)
-> Eval
     (GGColumns
        (GAlgebra (Rep a))
        TColumns
        (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
     (Col Result)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eval
  (GGColumns
     (GAlgebra (Rep a))
     TColumns
     (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
  (Col Result)
-> HKD a Result
forall a (f :: Context). GColumnsHKD a (Col f) -> HKD a f
HKD
  toColumns :: HKDT a -> Columns (HKDT a) (Col Result)
toColumns = (\(HKD Eval
  (GGColumns
     (GAlgebra (Rep a))
     TColumns
     (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
  (Col Result)
a) -> Eval
  (GGColumns
     (GAlgebra (Rep a))
     TColumns
     (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
  (Col Result)
a) (HKD a Result
 -> Eval
      (GGColumns
         (GAlgebra (Rep a))
         TColumns
         (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
      (Col Result))
-> (HKDT a -> HKD a Result)
-> HKDT a
-> Eval
     (GGColumns
        (GAlgebra (Rep a))
        TColumns
        (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
     (Col Result)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> HKD a Result
forall a. HKDable a => a -> HKD a Result
toHKD (a -> HKD a Result) -> (HKDT a -> a) -> HKDT a -> HKD a Result
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(HKDT a
a) -> a
a)
  reify :: (Result :~: Reify ctx) -> Unreify (HKDT a) -> HKDT a
reify = (Result :~: Reify ctx) -> Unreify (HKDT a) -> HKDT a
forall (context :: Context) (ctx :: Context) a.
NotReify context =>
(context :~: Reify ctx) -> a
notReify
  unreify :: (Result :~: Reify ctx) -> HKDT a -> Unreify (HKDT a)
unreify = (Result :~: Reify ctx) -> HKDT a -> Unreify (HKDT a)
forall (context :: Context) (ctx :: Context) a.
NotReify context =>
(context :~: Reify ctx) -> a
notReify


instance
  ( Table Expr (HKD a Expr)
  , Columns (HKD a Expr) ~ GColumns (HKD a)
  , HKDable a
  , x ~ HKD a Expr
  )
  => ToExprs x (HKDT a)
 where
  toResult :: HKDT a -> Columns x (Col Result)
toResult = (\(HKD Eval
  (GGColumns
     (GAlgebra (Rep a))
     TColumns
     (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
  (Col Result)
a) -> Eval
  (GGColumns
     (GAlgebra (Rep a))
     TColumns
     (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
  (Col Result)
a) (HKD a Result
 -> Eval
      (GGColumns
         (GAlgebra (Rep a))
         TColumns
         (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
      (Col Result))
-> (HKDT a -> HKD a Result)
-> HKDT a
-> Eval
     (GGColumns
        (GAlgebra (Rep a))
        TColumns
        (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
     (Col Result)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> HKD a Result
forall a. HKDable a => a -> HKD a Result
toHKD (a -> HKD a Result) -> (HKDT a -> a) -> HKDT a -> HKD a Result
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(HKDT a
a) -> a
a)
  fromResult :: Columns x (Col Result) -> HKDT a
fromResult = a -> HKDT a
forall a. a -> HKDT a
HKDT (a -> HKDT a)
-> (Eval
      (GGColumns
         (GAlgebra (Rep a))
         TColumns
         (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
      (Col Result)
    -> a)
-> Eval
     (GGColumns
        (GAlgebra (Rep a))
        TColumns
        (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
     (Col Result)
-> HKDT a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HKD a Result -> a
forall a. HKDable a => HKD a Result -> a
fromHKD (HKD a Result -> a)
-> (Eval
      (GGColumns
         (GAlgebra (Rep a))
         TColumns
         (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
      (Col Result)
    -> HKD a Result)
-> Eval
     (GGColumns
        (GAlgebra (Rep a))
        TColumns
        (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
     (Col Result)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eval
  (GGColumns
     (GAlgebra (Rep a))
     TColumns
     (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
  (Col Result)
-> HKD a Result
forall a (f :: Context). GColumnsHKD a (Col f) -> HKD a f
HKD


fromHKD :: HKDable a => HKD a Result -> a
fromHKD :: HKD a Result -> a
fromHKD = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
to (Rep a Any -> a)
-> (HKD a Result -> Rep a Any) -> HKD a Result -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy (TColumn Result)
-> (forall a. Eval (Top a) => Eval (TColumn Result a) -> a)
-> GMap (TColumn Result) (Rep a) Any
-> Rep a Any
forall (constraint :: * -> Exp Constraint) (rep :: * -> *)
       (proxy :: (* -> * -> *) -> *) (f :: * -> * -> *) x.
GMappable constraint rep =>
proxy f
-> (forall a. Eval (constraint a) => Eval (f a) -> a)
-> GMap f rep x
-> rep x
gunmap @Top (Proxy (TColumn Result)
forall k (t :: k). Proxy t
Proxy @(TColumn Result)) forall a. a -> a
forall a. Eval (Top a) => Eval (TColumn Result a) -> a
id (GMap (TColumn Result) (Rep a) Any -> Rep a Any)
-> (HKD a Result -> GMap (TColumn Result) (Rep a) Any)
-> HKD a Result
-> Rep a Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HKD a Result -> GMap (TColumn Result) (Rep a) Any
forall a x. Generic a => a -> Rep a x
from


toHKD :: HKDable a => a -> HKD a Result
toHKD :: a -> HKD a Result
toHKD = GMap (TColumn Result) (Rep a) Any -> HKD a Result
forall a x. Generic a => Rep a x -> a
to (GMap (TColumn Result) (Rep a) Any -> HKD a Result)
-> (a -> GMap (TColumn Result) (Rep a) Any) -> a -> HKD a Result
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy (TColumn Result)
-> (forall a. Eval (Top a) => a -> Eval (TColumn Result a))
-> Rep a Any
-> GMap (TColumn Result) (Rep a) Any
forall (constraint :: * -> Exp Constraint) (rep :: * -> *)
       (proxy :: (* -> * -> *) -> *) (f :: * -> * -> *) x.
GMappable constraint rep =>
proxy f
-> (forall a. Eval (constraint a) => a -> Eval (f a))
-> rep x
-> GMap f rep x
gmap @Top (Proxy (TColumn Result)
forall k (t :: k). Proxy t
Proxy @(TColumn Result)) forall a. a -> a
forall a. Eval (Top a) => a -> Eval (TColumn Result a)
id (Rep a Any -> GMap (TColumn Result) (Rep a) Any)
-> (a -> Rep a Any) -> a -> GMap (TColumn Result) (Rep a) Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a Any
forall a x. Generic a => a -> Rep a x
from


class Top_
instance Top_
Top_


data Top :: Type -> Exp Constraint
type instance Eval (Top _) = Top_


class
  ( Generic a
  , HTable (GColumns (HKD a))
  , KnownAlgebra (GAlgebra (Rep a))
  , Eval (GGTable (GAlgebra (Rep a)) (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
  , Eval (GGContext (GAlgebra (Rep a)) TUnreifyContext (GRecord (GMap (TColumn (Reify Result)) (Rep a)))) ~ Result
  , GRecordable (GMap (TColumn (Reify Result)) (Rep a))
  , GMappable Top (Rep a)
  , GMappable (TTable (Reify Result)) (GMap (TColumn (Reify Result)) (Rep a))
  , GMap TUnreify (GMap (TColumn (Reify Result)) (Rep a)) ~ GMap (TColumn Result) (Rep a)
  )
  => HKDable a
instance
  ( Generic a
  , HTable (GColumns (HKD a))
  , KnownAlgebra (GAlgebra (Rep a))
  , Eval (GGTable (GAlgebra (Rep a)) (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
  , Eval (GGContext (GAlgebra (Rep a)) TUnreifyContext (GRecord (GMap (TColumn (Reify Result)) (Rep a)))) ~ Result
  , GRecordable (GMap (TColumn (Reify Result)) (Rep a))
  , GMappable Top (Rep a)
  , GMappable (TTable (Reify Result)) (GMap (TColumn (Reify Result)) (Rep a))
  , GMap TUnreify (GMap (TColumn (Reify Result)) (Rep a)) ~ GMap (TColumn Result) (Rep a)
  )
  => HKDable a


type BuildableHKD :: Type -> Symbol -> Constraint
class GGBuildable (GAlgebra (Rep a)) name (HKDRep a) => BuildableHKD a name
instance GGBuildable (GAlgebra (Rep a)) name (HKDRep a) => BuildableHKD a name


type BuildHKD :: Type -> Symbol -> Type
type BuildHKD a name = GGBuild (GAlgebra (Rep a)) name (HKDRep a) (HKD a Expr)


buildHKD :: forall a name. BuildableHKD a name => BuildHKD a name
buildHKD :: BuildHKD a name
buildHKD =
  (Eval
   (GGColumns
      (GAlgebra (Rep a)) TColumns (Eval (HKDRep a (Reify Result))))
   (Col Expr)
 -> HKD a Expr)
-> BuildHKD a name
forall (algebra :: Algebra) (name :: Symbol)
       (rep :: Context -> Exp (* -> *)) a.
GGBuildable algebra name rep =>
(Eval
   (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
 -> a)
-> GGBuild algebra name rep a
ggbuild @(GAlgebra (Rep a)) @name @(HKDRep a) @(HKD a Expr) Eval
  (GGColumns
     (GAlgebra (Rep a)) TColumns (Eval (HKDRep a (Reify Result))))
  (Col Expr)
-> HKD a Expr
forall a (f :: Context). GColumnsHKD a (Col f) -> HKD a f
HKD


type ConstructableHKD :: Type -> Constraint
class GGConstructable (GAlgebra (Rep a)) (HKDRep a) => ConstructableHKD a
instance GGConstructable (GAlgebra (Rep a)) (HKDRep a) => ConstructableHKD a


type ConstructHKD :: Type -> Type
type ConstructHKD a = forall r. GGConstruct (GAlgebra (Rep a)) (HKDRep a) r


constructHKD :: forall a. ConstructableHKD a => ConstructHKD a -> HKD a Expr
constructHKD :: ConstructHKD a -> HKD a Expr
constructHKD ConstructHKD a
f =
  (Eval
   (GGColumns
      (GAlgebra (Rep a)) TColumns (Eval (HKDRep a (Reify Result))))
   (Col Expr)
 -> HKD a Expr)
-> GGConstruct (GAlgebra (Rep a)) (HKDRep a) (HKD a Expr)
-> HKD a Expr
forall (algebra :: Algebra) (rep :: Context -> Exp (* -> *)) a.
GGConstructable algebra rep =>
(Eval
   (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
 -> a)
-> GGConstruct algebra rep a -> a
ggconstruct @(GAlgebra (Rep a)) @(HKDRep a) @(HKD a Expr) Eval
  (GGColumns
     (GAlgebra (Rep a)) TColumns (Eval (HKDRep a (Reify Result))))
  (Col Expr)
-> HKD a Expr
forall a (f :: Context). GColumnsHKD a (Col f) -> HKD a f
HKD
    (GGConstruct (GAlgebra (Rep a)) (HKDRep a) (HKD a Expr)
ConstructHKD a
f @(HKD a Expr))


type DeconstructHKD :: Type -> Type -> Type
type DeconstructHKD a r = GGDeconstruct (GAlgebra (Rep a)) (HKDRep a) (HKD a Expr) r


deconstructHKD :: forall a r. (ConstructableHKD a, Table Expr r)
  => DeconstructHKD a r
deconstructHKD :: DeconstructHKD a r
deconstructHKD = (HKD a Expr
 -> Eval
      (GGColumns
         (GAlgebra (Rep a)) TColumns (Eval (HKDRep a (Reify Result))))
      (Col Expr))
-> DeconstructHKD a r
forall (algebra :: Algebra) (rep :: Context -> Exp (* -> *)) a r.
(GGConstructable algebra rep, Table Expr r) =>
(a
 -> Eval
      (GGColumns algebra TColumns (Eval (rep (Reify Result))))
      (Col Expr))
-> GGDeconstruct algebra rep a r
ggdeconstruct @(GAlgebra (Rep a)) @(HKDRep a) @(HKD a Expr) @r (\(HKD GColumnsHKD a (Col Expr)
a) -> Eval
  (GGColumns
     (GAlgebra (Rep a)) TColumns (Eval (HKDRep a (Reify Result))))
  (Col Expr)
GColumnsHKD a (Col Expr)
a)


type NameHKD :: Type -> Type
type NameHKD a = GGName (GAlgebra (Rep a)) (HKDRep a) (HKD a Name)


nameHKD :: forall a. ConstructableHKD a => NameHKD a
nameHKD :: NameHKD a
nameHKD = (Eval
   (GGColumns
      (GAlgebra (Rep a)) TColumns (Eval (HKDRep a (Reify Result))))
   (Col Name)
 -> HKD a Name)
-> NameHKD a
forall (algebra :: Algebra) (rep :: Context -> Exp (* -> *)) a.
GGConstructable algebra rep =>
(Eval
   (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Name)
 -> a)
-> GGName algebra rep a
ggname @(GAlgebra (Rep a)) @(HKDRep a) @(HKD a Name) Eval
  (GGColumns
     (GAlgebra (Rep a)) TColumns (Eval (HKDRep a (Reify Result))))
  (Col Name)
-> HKD a Name
forall a (f :: Context). GColumnsHKD a (Col f) -> HKD a f
HKD


type AggregateHKD :: Type -> Type
type AggregateHKD a = forall r. GGAggregate (GAlgebra (Rep a)) (HKDRep a) r


aggregateHKD :: forall a. ConstructableHKD a
  => AggregateHKD a -> HKD a Expr -> HKD a Aggregate
aggregateHKD :: AggregateHKD a -> HKD a Expr -> HKD a Aggregate
aggregateHKD AggregateHKD a
f =
  (Eval
   (GGColumns
      (GAlgebra (Rep a)) TColumns (Eval (HKDRep a (Reify Result))))
   (Col Aggregate)
 -> HKD a Aggregate)
-> (HKD a Expr
    -> Eval
         (GGColumns
            (GAlgebra (Rep a)) TColumns (Eval (HKDRep a (Reify Result))))
         (Col Expr))
-> GGAggregate (GAlgebra (Rep a)) (HKDRep a) (HKD a Aggregate)
-> HKD a Expr
-> HKD a Aggregate
forall (algebra :: Algebra) (rep :: Context -> Exp (* -> *)) exprs
       agg.
GGConstructable algebra rep =>
(Eval
   (GGColumns algebra TColumns (Eval (rep (Reify Result))))
   (Col Aggregate)
 -> agg)
-> (exprs
    -> Eval
         (GGColumns algebra TColumns (Eval (rep (Reify Result))))
         (Col Expr))
-> GGAggregate algebra rep agg
-> exprs
-> agg
ggaggregate @(GAlgebra (Rep a)) @(HKDRep a) @(HKD a Expr) @(HKD a Aggregate) Eval
  (GGColumns
     (GAlgebra (Rep a)) TColumns (Eval (HKDRep a (Reify Result))))
  (Col Aggregate)
-> HKD a Aggregate
forall a (f :: Context). GColumnsHKD a (Col f) -> HKD a f
HKD (\(HKD GColumnsHKD a (Col Expr)
a) -> Eval
  (GGColumns
     (GAlgebra (Rep a)) TColumns (Eval (HKDRep a (Reify Result))))
  (Col Expr)
GColumnsHKD a (Col Expr)
a)
    (GGAggregate (GAlgebra (Rep a)) (HKDRep a) (HKD a Aggregate)
AggregateHKD a
f @(HKD a Aggregate))


data HKDRep :: Type -> K.Context -> Exp (Type -> Type)
type instance Eval (HKDRep a context) =
  GRecord (GMap (TColumn context) (Rep a))