{-# language AllowAmbiguousTypes #-}
{-# language ConstraintKinds #-}
{-# language DataKinds #-}
{-# language FlexibleContexts #-}
{-# language FlexibleInstances #-}
{-# language LambdaCase #-}
{-# language MultiParamTypeClasses #-}
{-# language NamedFieldPuns #-}
{-# language ScopedTypeVariables #-}
{-# language StandaloneKindSignatures #-}
{-# language TypeApplications #-}
{-# language TypeFamilies #-}
{-# language UndecidableInstances #-}
{-# language ViewPatterns #-}

module Rel8.Generic.Construction
  ( GGBuildable
  , GGBuild, ggbuild
  , GGInsert, gginsert
  , GGConstructable
  , GGConstruct, ggconstruct
  , GGDeconstruct, ggdeconstruct
  , GGName, ggname
  , GGAggregate, ggaggregate
  )
where

-- base
import Data.Bifunctor ( first )
import Data.Kind ( Constraint, Type )
import Data.List.NonEmpty ( NonEmpty( (:|) ) )
import Data.Type.Equality ( (:~:)( Refl ) )
import GHC.TypeLits ( Symbol )
import Prelude

-- rel8
import Rel8.Aggregate ( Col( A ), Aggregate( Aggregate ) )
import Rel8.Expr ( Col( E ), Expr )
import Rel8.Expr.Aggregate ( groupByExpr )
import Rel8.Expr.Eq ( (==.) )
import Rel8.Expr.Null ( nullify, snull, unsafeUnnullify )
import Rel8.Expr.Serialize ( litExpr )
import Rel8.FCF ( Eval, Exp )
import Rel8.Generic.Construction.ADT
  ( GConstructorADT, GMakeableADT, gmakeADT
  , GConstructableADT
  , GBuildADT, gbuildADT, gunbuildADT
  , GConstructADT, gconstructADT, gdeconstructADT
  , RepresentableConstructors, GConstructors, gcindex, gctabulate
  , RepresentableFields, gfindex, gftabulate
  )
import Rel8.Generic.Construction.Record
  ( GConstructor
  , GConstructable, GConstruct, gconstruct, gdeconstruct
  , Representable, gindex, gtabulate
  )
import Rel8.Generic.Table ( GGColumns )
import Rel8.Kind.Algebra
  ( SAlgebra( SProduct, SSum )
  , KnownAlgebra, algebraSing
  )
import qualified Rel8.Kind.Algebra as K
import Rel8.Schema.Context.Nullify ( runTag )
import Rel8.Schema.HTable ( HTable )
import Rel8.Schema.HTable.Identity ( HIdentity( HType ) )
import Rel8.Schema.Insert ( Col( I ), Create(..), Insert )
import qualified Rel8.Schema.Kind as K
import Rel8.Schema.Name ( Col( N ), Name( Name ) )
import Rel8.Schema.Null ( Nullity( Null, NotNull ) )
import Rel8.Schema.Spec ( SSpec( SSpec, nullity, info ) )
import Rel8.Schema.Reify ( Col( Reify ), Reify, hreify, hunreify )
import Rel8.Schema.Result ( Result )
import Rel8.Table
  ( TTable, TColumns, TUnreify
  , Table, fromColumns, toColumns, reify, unreify
  )
import Rel8.Table.Bool ( case_ )
import Rel8.Type.Tag ( Tag )


type GGBuildable :: K.Algebra -> Symbol -> (K.Context -> Exp (Type -> Type)) -> Constraint
type GGBuildable algebra name rep =
  ( KnownAlgebra algebra
  , Eval (GGColumns algebra TColumns (Eval (rep (Reify Aggregate)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
  , Eval (GGColumns algebra TColumns (Eval (rep (Reify Expr)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
  , Eval (GGColumns algebra TColumns (Eval (rep (Reify Insert)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
  , Eval (GGColumns algebra TColumns (Eval (rep (Reify Name)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
  , HTable (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))))
  , GGBuildable' algebra name rep
  )


type GGBuildable' :: K.Algebra -> Symbol -> (K.Context -> Exp (Type -> Type)) -> Constraint
type family GGBuildable' algebra name rep where
  GGBuildable' 'K.Product name rep =
    ( name ~ GConstructor (Eval (rep (Reify Expr)))
    , name ~ GConstructor (Eval (rep (Reify Insert)))
    , Representable TUnreify (Eval (rep (Reify Expr)))
    , Representable TUnreify (Eval (rep (Reify Insert)))
    , GConstructable (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr)) (Eval (rep (Reify Expr)))
    , GConstructable (TTable (Reify Insert)) TColumns TUnreify (Col (Reify Insert)) (Eval (rep (Reify Insert)))
    )
  GGBuildable' 'K.Sum name rep =
    ( Representable TUnreify (GConstructorADT name (Eval (rep (Reify Expr))))
    , Representable TUnreify (GConstructorADT name (Eval (rep (Reify Insert))))
    , GMakeableADT (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr)) name (Eval (rep (Reify Expr)))
    , GMakeableADT (TTable (Reify Insert)) TColumns TUnreify (Col (Reify Insert)) name (Eval (rep (Reify Insert)))
    )


type GGBuild :: K.Algebra -> Symbol -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
type family GGBuild algebra name rep r where
  GGBuild 'K.Product _name rep r =
    GConstruct TUnreify (Eval (rep (Reify Expr))) r
  GGBuild 'K.Sum name rep r =
    GConstruct TUnreify (GConstructorADT name (Eval (rep (Reify Expr)))) r


ggbuild :: forall algebra name rep a. GGBuildable algebra name rep
  => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr) -> a)
  -> GGBuild algebra name rep a
ggbuild :: (Eval
   (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
 -> a)
-> GGBuild algebra name rep a
ggbuild Eval
  (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
-> a
gfromColumns = case KnownAlgebra algebra => SAlgebra algebra
forall (algebra :: Algebra).
KnownAlgebra algebra =>
SAlgebra algebra
algebraSing @algebra of
  SAlgebra algebra
SProduct ->
    (GFields TUnreify (Eval (rep (Reify Expr))) -> a)
-> GConstruct TUnreify (Eval (rep (Reify Expr))) a
forall (f :: * -> * -> *) (rep :: * -> *) a.
Representable f rep =>
(GFields f rep -> a) -> GConstruct f rep a
gtabulate @TUnreify @(Eval (rep (Reify Expr))) @a ((GFields TUnreify (Eval (rep (Reify Expr))) -> a)
 -> GConstruct TUnreify (Eval (rep (Reify Expr))) a)
-> (GFields TUnreify (Eval (rep (Reify Expr))) -> a)
-> GConstruct TUnreify (Eval (rep (Reify Expr))) a
forall a b. (a -> b) -> a -> b
$
    Eval
  (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
-> a
gfromColumns (Eval
   (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
 -> a)
-> (GFields TUnreify (Eval (rep (Reify Expr)))
    -> Eval
         (GGColumns algebra TColumns (Eval (rep (Reify Result))))
         (Col Expr))
-> GFields TUnreify (Eval (rep (Reify Expr)))
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Eval
  (GGColumns algebra TColumns (Eval (rep (Reify Result))))
  (Col (Reify Expr))
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col (Reify context)) -> t (Col context)
hunreify (Eval
   (GGColumns algebra TColumns (Eval (rep (Reify Result))))
   (Col (Reify Expr))
 -> Eval
      (GGColumns algebra TColumns (Eval (rep (Reify Result))))
      (Col Expr))
-> (GFields TUnreify (Eval (rep (Reify Expr)))
    -> Eval
         (GGColumns algebra TColumns (Eval (rep (Reify Result))))
         (Col (Reify Expr)))
-> GFields TUnreify (Eval (rep (Reify Expr)))
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    ToColumns
  (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr))
-> GFields TUnreify (Eval (rep (Reify Expr)))
-> GColumns TColumns (Eval (rep (Reify Expr))) (Col (Reify Expr))
forall (_Table :: * -> Exp Constraint)
       (_Columns :: * -> Exp HTable) (f :: * -> * -> *)
       (context :: HContext) (rep :: * -> *).
GConstructable _Table _Columns f context rep =>
ToColumns _Table _Columns f context
-> GFields f rep -> GColumns _Columns rep context
gconstruct
      @(TTable (Reify Expr))
      @TColumns
      @TUnreify
      @(Col (Reify Expr))
      @(Eval (rep (Reify Expr)))
      (\(proxy x
_ :: proxy x) -> x -> Columns x (Col (Reify Expr))
forall (context :: Context) a.
Table context a =>
a -> Columns a (Col context)
toColumns (x -> Columns x (Col (Reify Expr)))
-> (Unreify x -> x) -> Unreify x -> Columns x (Col (Reify Expr))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Reify Expr :~: Reify Expr) -> Unreify x -> x
forall (context :: Context) a (ctx :: Context).
Table context a =>
(context :~: Reify ctx) -> Unreify a -> a
reify @_ @x Reify Expr :~: Reify Expr
forall k (a :: k). a :~: a
Refl)
  SAlgebra algebra
SSum ->
    (GFields TUnreify (GConstructorADT name (Eval (rep (Reify Expr))))
 -> a)
-> GConstruct
     TUnreify (GConstructorADT name (Eval (rep (Reify Expr)))) a
forall (f :: * -> * -> *) (rep :: * -> *) a.
Representable f rep =>
(GFields f rep -> a) -> GConstruct f rep a
gtabulate @TUnreify @(GConstructorADT name (Eval (rep (Reify Expr)))) @a ((GFields TUnreify (GConstructorADT name (Eval (rep (Reify Expr))))
  -> a)
 -> GConstruct
      TUnreify (GConstructorADT name (Eval (rep (Reify Expr)))) a)
-> (GFields
      TUnreify (GConstructorADT name (Eval (rep (Reify Expr))))
    -> a)
-> GConstruct
     TUnreify (GConstructorADT name (Eval (rep (Reify Expr)))) a
forall a b. (a -> b) -> a -> b
$
    Eval
  (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
-> a
gfromColumns (Eval
   (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
 -> a)
-> (GFields
      TUnreify (GConstructorADT name (Eval (rep (Reify Expr))))
    -> Eval
         (GGColumns algebra TColumns (Eval (rep (Reify Result))))
         (Col Expr))
-> GFields
     TUnreify (GConstructorADT name (Eval (rep (Reify Expr))))
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Eval
  (GGColumns algebra TColumns (Eval (rep (Reify Result))))
  (Col (Reify Expr))
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col (Reify context)) -> t (Col context)
hunreify (Eval
   (GGColumns algebra TColumns (Eval (rep (Reify Result))))
   (Col (Reify Expr))
 -> Eval
      (GGColumns algebra TColumns (Eval (rep (Reify Result))))
      (Col Expr))
-> (GFields
      TUnreify (GConstructorADT name (Eval (rep (Reify Expr))))
    -> Eval
         (GGColumns algebra TColumns (Eval (rep (Reify Result))))
         (Col (Reify Expr)))
-> GFields
     TUnreify (GConstructorADT name (Eval (rep (Reify Expr))))
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    ToColumns
  (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr))
-> Null (Col (Reify Expr))
-> Nullifier (Col (Reify Expr))
-> (Tag -> HType Tag (Col (Reify Expr)))
-> GFields
     TUnreify (GConstructorADT name (Eval (rep (Reify Expr))))
-> GColumnsADT
     TColumns (Eval (rep (Reify Expr))) (Col (Reify Expr))
forall (_Table :: * -> Exp Constraint)
       (_Columns :: * -> Exp HTable) (f :: * -> * -> *)
       (context :: HContext) (name :: Symbol) (rep :: * -> *).
GMakeableADT _Table _Columns f context name rep =>
ToColumns _Table _Columns f context
-> Null context
-> Nullifier context
-> (Tag -> HType Tag context)
-> GFields f (GConstructorADT name rep)
-> GColumnsADT _Columns rep context
gmakeADT
      @(TTable (Reify Expr))
      @TColumns
      @TUnreify
      @(Col (Reify Expr))
      @name
      @(Eval (rep (Reify Expr)))
      (\(proxy x
_ :: proxy x) -> x -> Columns x (Col (Reify Expr))
forall (context :: Context) a.
Table context a =>
a -> Columns a (Col context)
toColumns (x -> Columns x (Col (Reify Expr)))
-> (Unreify x -> x) -> Unreify x -> Columns x (Col (Reify Expr))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Reify Expr :~: Reify Expr) -> Unreify x -> x
forall (context :: Context) a (ctx :: Context).
Table context a =>
(context :~: Reify ctx) -> Unreify a -> a
reify @_ @x Reify Expr :~: Reify Expr
forall k (a :: k). a :~: a
Refl)
      (\SSpec {TypeInformation (Unnullify a)
info :: TypeInformation (Unnullify a)
info :: forall (labels :: Labels) (necessity :: Necessity) a.
SSpec ('Spec labels necessity a) -> TypeInformation (Unnullify a)
info} -> Col Expr ('Spec labels necessity (Nullify a))
-> Col (Reify Expr) ('Spec labels necessity (Nullify a))
forall (context :: Context) (spec :: Spec).
Col context spec -> Col (Reify context) spec
Reify (Expr (Nullify a) -> Col Expr ('Spec labels necessity (Nullify a))
forall a (labels :: Labels) (necessity :: Necessity).
Expr a -> Col Expr ('Spec labels necessity a)
E (TypeInformation (Unnullify' (IsMaybe a) a) -> Expr (Nullify a)
forall a. TypeInformation a -> Expr (Maybe a)
snull TypeInformation (Unnullify' (IsMaybe a) a)
TypeInformation (Unnullify a)
info)))
      (\SSpec {Nullity a
nullity :: Nullity a
nullity :: forall (labels :: Labels) (necessity :: Necessity) a.
SSpec ('Spec labels necessity a) -> Nullity a
nullity} -> case Nullity a
nullity of
        Nullity a
Null -> Col (Reify Expr) ('Spec labels necessity a)
-> Col (Reify Expr) ('Spec labels necessity (Nullify a))
forall a. a -> a
id
        Nullity a
NotNull -> \(Reify (E a)) -> Col Expr ('Spec labels necessity (Maybe a))
-> Col (Reify Expr) ('Spec labels necessity (Maybe a))
forall (context :: Context) (spec :: Spec).
Col context spec -> Col (Reify context) spec
Reify (Expr (Maybe a) -> Col Expr ('Spec labels necessity (Maybe a))
forall a (labels :: Labels) (necessity :: Necessity).
Expr a -> Col Expr ('Spec labels necessity a)
E (Expr a -> Expr (Maybe a)
forall a. NotNull a => Expr a -> Expr (Maybe a)
nullify Expr a
a)))
      (Col (Reify Expr) ('Spec '[] 'Required Tag)
-> HType Tag (Col (Reify Expr))
forall (context :: HContext) a.
context ('Spec '[] 'Required a) -> HType a context
HType (Col (Reify Expr) ('Spec '[] 'Required Tag)
 -> HType Tag (Col (Reify Expr)))
-> (Tag -> Col (Reify Expr) ('Spec '[] 'Required Tag))
-> Tag
-> HType Tag (Col (Reify Expr))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Col Expr ('Spec '[] 'Required Tag)
-> Col (Reify Expr) ('Spec '[] 'Required Tag)
forall (context :: Context) (spec :: Spec).
Col context spec -> Col (Reify context) spec
Reify (Col Expr ('Spec '[] 'Required Tag)
 -> Col (Reify Expr) ('Spec '[] 'Required Tag))
-> (Tag -> Col Expr ('Spec '[] 'Required Tag))
-> Tag
-> Col (Reify Expr) ('Spec '[] 'Required Tag)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr Tag -> Col Expr ('Spec '[] 'Required Tag)
forall a (labels :: Labels) (necessity :: Necessity).
Expr a -> Col Expr ('Spec labels necessity a)
E (Expr Tag -> Col Expr ('Spec '[] 'Required Tag))
-> (Tag -> Expr Tag) -> Tag -> Col Expr ('Spec '[] 'Required Tag)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tag -> Expr Tag
forall a. Sql DBType a => a -> Expr a
litExpr)


type GGInsert :: K.Algebra -> Symbol -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
type family GGInsert algebra name rep r where
  GGInsert 'K.Product _name rep r =
    GConstruct TUnreify (Eval (rep (Reify Insert))) r
  GGInsert 'K.Sum name rep r =
    GConstruct TUnreify (GConstructorADT name (Eval (rep (Reify Insert)))) r


gginsert :: forall algebra name rep a. GGBuildable algebra name rep
  => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Insert) -> a)
  -> GGInsert algebra name rep a
gginsert :: (Eval
   (GGColumns algebra TColumns (Eval (rep (Reify Result))))
   (Col Insert)
 -> a)
-> GGInsert algebra name rep a
gginsert Eval
  (GGColumns algebra TColumns (Eval (rep (Reify Result))))
  (Col Insert)
-> a
gfromColumns = case KnownAlgebra algebra => SAlgebra algebra
forall (algebra :: Algebra).
KnownAlgebra algebra =>
SAlgebra algebra
algebraSing @algebra of
  SAlgebra algebra
SProduct ->
    (GFields TUnreify (Eval (rep (Reify Insert))) -> a)
-> GConstruct TUnreify (Eval (rep (Reify Insert))) a
forall (f :: * -> * -> *) (rep :: * -> *) a.
Representable f rep =>
(GFields f rep -> a) -> GConstruct f rep a
gtabulate @TUnreify @(Eval (rep (Reify Insert))) @a ((GFields TUnreify (Eval (rep (Reify Insert))) -> a)
 -> GConstruct TUnreify (Eval (rep (Reify Insert))) a)
-> (GFields TUnreify (Eval (rep (Reify Insert))) -> a)
-> GConstruct TUnreify (Eval (rep (Reify Insert))) a
forall a b. (a -> b) -> a -> b
$
    Eval
  (GGColumns algebra TColumns (Eval (rep (Reify Result))))
  (Col Insert)
-> a
gfromColumns (Eval
   (GGColumns algebra TColumns (Eval (rep (Reify Result))))
   (Col Insert)
 -> a)
-> (GFields TUnreify (Eval (rep (Reify Insert)))
    -> Eval
         (GGColumns algebra TColumns (Eval (rep (Reify Result))))
         (Col Insert))
-> GFields TUnreify (Eval (rep (Reify Insert)))
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Eval
  (GGColumns algebra TColumns (Eval (rep (Reify Result))))
  (Col (Reify Insert))
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result))))
     (Col Insert)
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col (Reify context)) -> t (Col context)
hunreify (Eval
   (GGColumns algebra TColumns (Eval (rep (Reify Result))))
   (Col (Reify Insert))
 -> Eval
      (GGColumns algebra TColumns (Eval (rep (Reify Result))))
      (Col Insert))
-> (GFields TUnreify (Eval (rep (Reify Insert)))
    -> Eval
         (GGColumns algebra TColumns (Eval (rep (Reify Result))))
         (Col (Reify Insert)))
-> GFields TUnreify (Eval (rep (Reify Insert)))
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result))))
     (Col Insert)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    ToColumns
  (TTable (Reify Insert)) TColumns TUnreify (Col (Reify Insert))
-> GFields TUnreify (Eval (rep (Reify Insert)))
-> GColumns
     TColumns (Eval (rep (Reify Insert))) (Col (Reify Insert))
forall (_Table :: * -> Exp Constraint)
       (_Columns :: * -> Exp HTable) (f :: * -> * -> *)
       (context :: HContext) (rep :: * -> *).
GConstructable _Table _Columns f context rep =>
ToColumns _Table _Columns f context
-> GFields f rep -> GColumns _Columns rep context
gconstruct
      @(TTable (Reify Insert))
      @TColumns
      @TUnreify
      @(Col (Reify Insert))
      @(Eval (rep (Reify Insert)))
      (\(proxy x
_ :: proxy x) -> x -> Columns x (Col (Reify Insert))
forall (context :: Context) a.
Table context a =>
a -> Columns a (Col context)
toColumns (x -> Columns x (Col (Reify Insert)))
-> (Unreify x -> x) -> Unreify x -> Columns x (Col (Reify Insert))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Reify Insert :~: Reify Insert) -> Unreify x -> x
forall (context :: Context) a (ctx :: Context).
Table context a =>
(context :~: Reify ctx) -> Unreify a -> a
reify @_ @x Reify Insert :~: Reify Insert
forall k (a :: k). a :~: a
Refl)
  SAlgebra algebra
SSum ->
    (GFields
   TUnreify (GConstructorADT name (Eval (rep (Reify Insert))))
 -> a)
-> GConstruct
     TUnreify (GConstructorADT name (Eval (rep (Reify Insert)))) a
forall (f :: * -> * -> *) (rep :: * -> *) a.
Representable f rep =>
(GFields f rep -> a) -> GConstruct f rep a
gtabulate @TUnreify @(GConstructorADT name (Eval (rep (Reify Insert)))) @a ((GFields
    TUnreify (GConstructorADT name (Eval (rep (Reify Insert))))
  -> a)
 -> GConstruct
      TUnreify (GConstructorADT name (Eval (rep (Reify Insert)))) a)
-> (GFields
      TUnreify (GConstructorADT name (Eval (rep (Reify Insert))))
    -> a)
-> GConstruct
     TUnreify (GConstructorADT name (Eval (rep (Reify Insert)))) a
forall a b. (a -> b) -> a -> b
$
    Eval
  (GGColumns algebra TColumns (Eval (rep (Reify Result))))
  (Col Insert)
-> a
gfromColumns (Eval
   (GGColumns algebra TColumns (Eval (rep (Reify Result))))
   (Col Insert)
 -> a)
-> (GFields
      TUnreify (GConstructorADT name (Eval (rep (Reify Insert))))
    -> Eval
         (GGColumns algebra TColumns (Eval (rep (Reify Result))))
         (Col Insert))
-> GFields
     TUnreify (GConstructorADT name (Eval (rep (Reify Insert))))
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Eval
  (GGColumns algebra TColumns (Eval (rep (Reify Result))))
  (Col (Reify Insert))
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result))))
     (Col Insert)
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col (Reify context)) -> t (Col context)
hunreify (Eval
   (GGColumns algebra TColumns (Eval (rep (Reify Result))))
   (Col (Reify Insert))
 -> Eval
      (GGColumns algebra TColumns (Eval (rep (Reify Result))))
      (Col Insert))
-> (GFields
      TUnreify (GConstructorADT name (Eval (rep (Reify Insert))))
    -> Eval
         (GGColumns algebra TColumns (Eval (rep (Reify Result))))
         (Col (Reify Insert)))
-> GFields
     TUnreify (GConstructorADT name (Eval (rep (Reify Insert))))
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result))))
     (Col Insert)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    ToColumns
  (TTable (Reify Insert)) TColumns TUnreify (Col (Reify Insert))
-> Null (Col (Reify Insert))
-> Nullifier (Col (Reify Insert))
-> (Tag -> HType Tag (Col (Reify Insert)))
-> GFields
     TUnreify (GConstructorADT name (Eval (rep (Reify Insert))))
-> GColumnsADT
     TColumns (Eval (rep (Reify Insert))) (Col (Reify Insert))
forall (_Table :: * -> Exp Constraint)
       (_Columns :: * -> Exp HTable) (f :: * -> * -> *)
       (context :: HContext) (name :: Symbol) (rep :: * -> *).
GMakeableADT _Table _Columns f context name rep =>
ToColumns _Table _Columns f context
-> Null context
-> Nullifier context
-> (Tag -> HType Tag context)
-> GFields f (GConstructorADT name rep)
-> GColumnsADT _Columns rep context
gmakeADT
      @(TTable (Reify Insert))
      @TColumns
      @TUnreify
      @(Col (Reify Insert))
      @name
      @(Eval (rep (Reify Insert)))
      (\(proxy x
_ :: proxy x) -> x -> Columns x (Col (Reify Insert))
forall (context :: Context) a.
Table context a =>
a -> Columns a (Col context)
toColumns (x -> Columns x (Col (Reify Insert)))
-> (Unreify x -> x) -> Unreify x -> Columns x (Col (Reify Insert))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Reify Insert :~: Reify Insert) -> Unreify x -> x
forall (context :: Context) a (ctx :: Context).
Table context a =>
(context :~: Reify ctx) -> Unreify a -> a
reify @_ @x Reify Insert :~: Reify Insert
forall k (a :: k). a :~: a
Refl)
      (\SSpec {TypeInformation (Unnullify a)
info :: TypeInformation (Unnullify a)
info :: forall (labels :: Labels) (necessity :: Necessity) a.
SSpec ('Spec labels necessity a) -> TypeInformation (Unnullify a)
info} -> Col Insert ('Spec labels necessity (Nullify a))
-> Col (Reify Insert) ('Spec labels necessity (Nullify a))
forall (context :: Context) (spec :: Spec).
Col context spec -> Col (Reify context) spec
Reify (Col Insert ('Spec labels necessity (Nullify a))
 -> Col (Reify Insert) ('Spec labels necessity (Nullify a)))
-> Col Insert ('Spec labels necessity (Nullify a))
-> Col (Reify Insert) ('Spec labels necessity (Nullify a))
forall a b. (a -> b) -> a -> b
$ Create necessity (Nullify a)
-> Col Insert ('Spec labels necessity (Nullify a))
forall (necessity :: Necessity) a (labels :: Labels).
Create necessity a -> Col Insert ('Spec labels necessity a)
I (Expr (Nullify a) -> Create necessity (Nullify a)
forall a (necessity :: Necessity). Expr a -> Create necessity a
Value (TypeInformation (Unnullify' (IsMaybe a) a) -> Expr (Nullify a)
forall a. TypeInformation a -> Expr (Maybe a)
snull TypeInformation (Unnullify' (IsMaybe a) a)
TypeInformation (Unnullify a)
info)))
      (\SSpec {Nullity a
nullity :: Nullity a
nullity :: forall (labels :: Labels) (necessity :: Necessity) a.
SSpec ('Spec labels necessity a) -> Nullity a
nullity} -> case Nullity a
nullity of
        Nullity a
Null -> Col (Reify Insert) ('Spec labels necessity a)
-> Col (Reify Insert) ('Spec labels necessity (Nullify a))
forall a. a -> a
id
        Nullity a
NotNull -> \case
          Reify (I Default) -> Col Insert ('Spec labels 'Optional (Maybe a))
-> Col (Reify Insert) ('Spec labels 'Optional (Maybe a))
forall (context :: Context) (spec :: Spec).
Col context spec -> Col (Reify context) spec
Reify (Create 'Optional (Maybe a)
-> Col Insert ('Spec labels 'Optional (Maybe a))
forall (necessity :: Necessity) a (labels :: Labels).
Create necessity a -> Col Insert ('Spec labels necessity a)
I Create 'Optional (Maybe a)
forall a. Create 'Optional a
Default)
          Reify (I (Value a)) -> Col Insert ('Spec labels necessity (Maybe a))
-> Col (Reify Insert) ('Spec labels necessity (Maybe a))
forall (context :: Context) (spec :: Spec).
Col context spec -> Col (Reify context) spec
Reify (Create necessity (Maybe a)
-> Col Insert ('Spec labels necessity (Maybe a))
forall (necessity :: Necessity) a (labels :: Labels).
Create necessity a -> Col Insert ('Spec labels necessity a)
I (Expr (Maybe a) -> Create necessity (Maybe a)
forall a (necessity :: Necessity). Expr a -> Create necessity a
Value (Expr a -> Expr (Maybe a)
forall a. NotNull a => Expr a -> Expr (Maybe a)
nullify Expr a
a))))
      (Col (Reify Insert) ('Spec '[] 'Required Tag)
-> HType Tag (Col (Reify Insert))
forall (context :: HContext) a.
context ('Spec '[] 'Required a) -> HType a context
HType (Col (Reify Insert) ('Spec '[] 'Required Tag)
 -> HType Tag (Col (Reify Insert)))
-> (Tag -> Col (Reify Insert) ('Spec '[] 'Required Tag))
-> Tag
-> HType Tag (Col (Reify Insert))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Col Insert ('Spec '[] 'Required Tag)
-> Col (Reify Insert) ('Spec '[] 'Required Tag)
forall (context :: Context) (spec :: Spec).
Col context spec -> Col (Reify context) spec
Reify (Col Insert ('Spec '[] 'Required Tag)
 -> Col (Reify Insert) ('Spec '[] 'Required Tag))
-> (Tag -> Col Insert ('Spec '[] 'Required Tag))
-> Tag
-> Col (Reify Insert) ('Spec '[] 'Required Tag)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Create 'Required Tag -> Col Insert ('Spec '[] 'Required Tag)
forall (necessity :: Necessity) a (labels :: Labels).
Create necessity a -> Col Insert ('Spec labels necessity a)
I (Create 'Required Tag -> Col Insert ('Spec '[] 'Required Tag))
-> (Tag -> Create 'Required Tag)
-> Tag
-> Col Insert ('Spec '[] 'Required Tag)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr Tag -> Create 'Required Tag
forall a (necessity :: Necessity). Expr a -> Create necessity a
Value (Expr Tag -> Create 'Required Tag)
-> (Tag -> Expr Tag) -> Tag -> Create 'Required Tag
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tag -> Expr Tag
forall a. Sql DBType a => a -> Expr a
litExpr)


type GGConstructable :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Constraint
type GGConstructable algebra rep =
  ( KnownAlgebra algebra
  , Eval (GGColumns algebra TColumns (Eval (rep (Reify Aggregate)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
  , Eval (GGColumns algebra TColumns (Eval (rep (Reify Expr)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
  , Eval (GGColumns algebra TColumns (Eval (rep (Reify Insert)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
  , Eval (GGColumns algebra TColumns (Eval (rep (Reify Name)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
  , HTable (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))))
  , GGConstructable' algebra rep
  )


type GGConstructable' :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Constraint
type family GGConstructable' algebra rep where
  GGConstructable' 'K.Product rep =
    ( Representable TUnreify (Eval (rep (Reify Aggregate)))
    , Representable TUnreify (Eval (rep (Reify Expr)))
    , Representable TUnreify (Eval (rep (Reify Insert)))
    , Representable TUnreify (Eval (rep (Reify Name)))
    , GConstructable (TTable (Reify Aggregate)) TColumns TUnreify (Col (Reify Aggregate)) (Eval (rep (Reify Aggregate)))
    , GConstructable (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr)) (Eval (rep (Reify Expr)))
    , GConstructable (TTable (Reify Insert)) TColumns TUnreify (Col (Reify Insert)) (Eval (rep (Reify Insert)))
    , GConstructable (TTable (Reify Name)) TColumns TUnreify (Col (Reify Name)) (Eval (rep (Reify Name)))
    )
  GGConstructable' 'K.Sum rep =
    ( RepresentableConstructors TUnreify (Eval (rep (Reify Expr)))
    , RepresentableConstructors TUnreify (Eval (rep (Reify Insert)))
    , RepresentableFields TUnreify (Eval (rep (Reify Aggregate)))
    , RepresentableFields TUnreify (Eval (rep (Reify Expr)))
    , RepresentableFields TUnreify (Eval (rep (Reify Name)))
    , Functor (GConstructors TUnreify (Eval (rep (Reify Expr))))
    , Functor (GConstructors TUnreify (Eval (rep (Reify Insert))))
    , GConstructableADT (TTable (Reify Aggregate)) TColumns TUnreify (Col (Reify Aggregate)) (Eval (rep (Reify Aggregate)))
    , GConstructableADT (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr)) (Eval (rep (Reify Expr)))
    , GConstructableADT (TTable (Reify Insert)) TColumns TUnreify (Col (Reify Insert)) (Eval (rep (Reify Insert)))
    , GConstructableADT (TTable (Reify Name)) TColumns TUnreify (Col (Reify Name)) (Eval (rep (Reify Name)))
    )


type GGConstruct :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
type family GGConstruct algebra rep r where
  GGConstruct 'K.Product rep r =
    GConstruct TUnreify (Eval (rep (Reify Expr))) r -> r
  GGConstruct 'K.Sum rep r =
    GConstructADT TUnreify (Eval (rep (Reify Expr))) r r


ggconstruct :: forall algebra rep a. GGConstructable algebra rep
  => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr) -> a)
  -> GGConstruct algebra rep a -> a
ggconstruct :: (Eval
   (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
 -> a)
-> GGConstruct algebra rep a -> a
ggconstruct Eval
  (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
-> a
gfromColumns GGConstruct algebra rep a
f = case KnownAlgebra algebra => SAlgebra algebra
forall (algebra :: Algebra).
KnownAlgebra algebra =>
SAlgebra algebra
algebraSing @algebra of
  SAlgebra algebra
SProduct ->
    GGConstruct algebra rep a
GConstruct TUnreify (Eval (rep (Reify Expr))) a -> a
f (GConstruct TUnreify (Eval (rep (Reify Expr))) a -> a)
-> GConstruct TUnreify (Eval (rep (Reify Expr))) a -> a
forall a b. (a -> b) -> a -> b
$
    (GFields TUnreify (Eval (rep (Reify Expr))) -> a)
-> GConstruct TUnreify (Eval (rep (Reify Expr))) a
forall (f :: * -> * -> *) (rep :: * -> *) a.
Representable f rep =>
(GFields f rep -> a) -> GConstruct f rep a
gtabulate @TUnreify @(Eval (rep (Reify Expr))) @a ((GFields TUnreify (Eval (rep (Reify Expr))) -> a)
 -> GConstruct TUnreify (Eval (rep (Reify Expr))) a)
-> (GFields TUnreify (Eval (rep (Reify Expr))) -> a)
-> GConstruct TUnreify (Eval (rep (Reify Expr))) a
forall a b. (a -> b) -> a -> b
$
    Eval
  (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
-> a
gfromColumns (Eval
   (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
 -> a)
-> (GFields TUnreify (Eval (rep (Reify Expr)))
    -> Eval
         (GGColumns algebra TColumns (Eval (rep (Reify Result))))
         (Col Expr))
-> GFields TUnreify (Eval (rep (Reify Expr)))
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Eval
  (GGColumns algebra TColumns (Eval (rep (Reify Result))))
  (Col (Reify Expr))
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col (Reify context)) -> t (Col context)
hunreify (Eval
   (GGColumns algebra TColumns (Eval (rep (Reify Result))))
   (Col (Reify Expr))
 -> Eval
      (GGColumns algebra TColumns (Eval (rep (Reify Result))))
      (Col Expr))
-> (GFields TUnreify (Eval (rep (Reify Expr)))
    -> Eval
         (GGColumns algebra TColumns (Eval (rep (Reify Result))))
         (Col (Reify Expr)))
-> GFields TUnreify (Eval (rep (Reify Expr)))
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    ToColumns
  (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr))
-> GFields TUnreify (Eval (rep (Reify Expr)))
-> GColumns TColumns (Eval (rep (Reify Expr))) (Col (Reify Expr))
forall (_Table :: * -> Exp Constraint)
       (_Columns :: * -> Exp HTable) (f :: * -> * -> *)
       (context :: HContext) (rep :: * -> *).
GConstructable _Table _Columns f context rep =>
ToColumns _Table _Columns f context
-> GFields f rep -> GColumns _Columns rep context
gconstruct
      @(TTable (Reify Expr))
      @TColumns
      @TUnreify
      @(Col (Reify Expr))
      @(Eval (rep (Reify Expr)))
      (\(proxy x
_ :: proxy x) -> x -> Columns x (Col (Reify Expr))
forall (context :: Context) a.
Table context a =>
a -> Columns a (Col context)
toColumns (x -> Columns x (Col (Reify Expr)))
-> (Unreify x -> x) -> Unreify x -> Columns x (Col (Reify Expr))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Reify Expr :~: Reify Expr) -> Unreify x -> x
forall (context :: Context) a (ctx :: Context).
Table context a =>
(context :~: Reify ctx) -> Unreify a -> a
reify @_ @x Reify Expr :~: Reify Expr
forall k (a :: k). a :~: a
Refl)
  SAlgebra algebra
SSum ->
    GConstructADT TUnreify (Eval (rep (Reify Expr))) a a
-> GConstructors TUnreify (Eval (rep (Reify Expr))) a -> a
forall (f :: * -> * -> *) (rep :: * -> *) r a.
RepresentableConstructors f rep =>
GConstructADT f rep r a -> GConstructors f rep r -> a
gcindex @TUnreify @(Eval (rep (Reify Expr))) @a GConstructADT TUnreify (Eval (rep (Reify Expr))) a a
GGConstruct algebra rep a
f (GConstructors TUnreify (Eval (rep (Reify Expr))) a -> a)
-> GConstructors TUnreify (Eval (rep (Reify Expr))) a -> a
forall a b. (a -> b) -> a -> b
$
    (Eval
   (GGColumns algebra TColumns (Eval (rep (Reify Result))))
   (Col (Reify Expr))
 -> a)
-> GConstructors
     TUnreify
     (Eval (rep (Reify Expr)))
     (Eval
        (GGColumns algebra TColumns (Eval (rep (Reify Result))))
        (Col (Reify Expr)))
-> GConstructors TUnreify (Eval (rep (Reify Expr))) a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Eval
  (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
-> a
gfromColumns (Eval
   (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
 -> a)
-> (Eval
      (GGColumns algebra TColumns (Eval (rep (Reify Result))))
      (Col (Reify Expr))
    -> Eval
         (GGColumns algebra TColumns (Eval (rep (Reify Result))))
         (Col Expr))
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result))))
     (Col (Reify Expr))
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eval
  (GGColumns algebra TColumns (Eval (rep (Reify Result))))
  (Col (Reify Expr))
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col (Reify context)) -> t (Col context)
hunreify) (GConstructors
   TUnreify
   (Eval (rep (Reify Expr)))
   (Eval
      (GGColumns algebra TColumns (Eval (rep (Reify Result))))
      (Col (Reify Expr)))
 -> GConstructors TUnreify (Eval (rep (Reify Expr))) a)
-> GConstructors
     TUnreify
     (Eval (rep (Reify Expr)))
     (Eval
        (GGColumns algebra TColumns (Eval (rep (Reify Result))))
        (Col (Reify Expr)))
-> GConstructors TUnreify (Eval (rep (Reify Expr))) a
forall a b. (a -> b) -> a -> b
$
    ToColumns
  (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr))
-> Null (Col (Reify Expr))
-> Nullifier (Col (Reify Expr))
-> (Tag -> HType Tag (Col (Reify Expr)))
-> GConstructors
     TUnreify
     (Eval (rep (Reify Expr)))
     (GColumnsADT TColumns (Eval (rep (Reify Expr))) (Col (Reify Expr)))
forall (_Table :: * -> Exp Constraint)
       (_Columns :: * -> Exp HTable) (f :: * -> * -> *)
       (context :: HContext) (rep :: * -> *).
GConstructableADT _Table _Columns f context rep =>
ToColumns _Table _Columns f context
-> Null context
-> Nullifier context
-> (Tag -> HType Tag context)
-> GConstructors f rep (GColumnsADT _Columns rep context)
gconstructADT
      @(TTable (Reify Expr))
      @TColumns
      @TUnreify
      @(Col (Reify Expr))
      @(Eval (rep (Reify Expr)))
      (\(proxy x
_ :: proxy x) -> x -> Columns x (Col (Reify Expr))
forall (context :: Context) a.
Table context a =>
a -> Columns a (Col context)
toColumns (x -> Columns x (Col (Reify Expr)))
-> (Unreify x -> x) -> Unreify x -> Columns x (Col (Reify Expr))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Reify Expr :~: Reify Expr) -> Unreify x -> x
forall (context :: Context) a (ctx :: Context).
Table context a =>
(context :~: Reify ctx) -> Unreify a -> a
reify @_ @x Reify Expr :~: Reify Expr
forall k (a :: k). a :~: a
Refl)
      (\SSpec {TypeInformation (Unnullify a)
info :: TypeInformation (Unnullify a)
info :: forall (labels :: Labels) (necessity :: Necessity) a.
SSpec ('Spec labels necessity a) -> TypeInformation (Unnullify a)
info} -> Col Expr ('Spec labels necessity (Nullify a))
-> Col (Reify Expr) ('Spec labels necessity (Nullify a))
forall (context :: Context) (spec :: Spec).
Col context spec -> Col (Reify context) spec
Reify (Expr (Nullify a) -> Col Expr ('Spec labels necessity (Nullify a))
forall a (labels :: Labels) (necessity :: Necessity).
Expr a -> Col Expr ('Spec labels necessity a)
E (TypeInformation (Unnullify' (IsMaybe a) a) -> Expr (Nullify a)
forall a. TypeInformation a -> Expr (Maybe a)
snull TypeInformation (Unnullify' (IsMaybe a) a)
TypeInformation (Unnullify a)
info)))
      (\SSpec {Nullity a
nullity :: Nullity a
nullity :: forall (labels :: Labels) (necessity :: Necessity) a.
SSpec ('Spec labels necessity a) -> Nullity a
nullity} -> case Nullity a
nullity of
        Nullity a
Null -> Col (Reify Expr) ('Spec labels necessity a)
-> Col (Reify Expr) ('Spec labels necessity (Nullify a))
forall a. a -> a
id
        Nullity a
NotNull -> \(Reify (E a)) -> Col Expr ('Spec labels necessity (Maybe a))
-> Col (Reify Expr) ('Spec labels necessity (Maybe a))
forall (context :: Context) (spec :: Spec).
Col context spec -> Col (Reify context) spec
Reify (Expr (Maybe a) -> Col Expr ('Spec labels necessity (Maybe a))
forall a (labels :: Labels) (necessity :: Necessity).
Expr a -> Col Expr ('Spec labels necessity a)
E (Expr a -> Expr (Maybe a)
forall a. NotNull a => Expr a -> Expr (Maybe a)
nullify Expr a
a)))
      (Col (Reify Expr) ('Spec '[] 'Required Tag)
-> HType Tag (Col (Reify Expr))
forall (context :: HContext) a.
context ('Spec '[] 'Required a) -> HType a context
HType (Col (Reify Expr) ('Spec '[] 'Required Tag)
 -> HType Tag (Col (Reify Expr)))
-> (Tag -> Col (Reify Expr) ('Spec '[] 'Required Tag))
-> Tag
-> HType Tag (Col (Reify Expr))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Col Expr ('Spec '[] 'Required Tag)
-> Col (Reify Expr) ('Spec '[] 'Required Tag)
forall (context :: Context) (spec :: Spec).
Col context spec -> Col (Reify context) spec
Reify (Col Expr ('Spec '[] 'Required Tag)
 -> Col (Reify Expr) ('Spec '[] 'Required Tag))
-> (Tag -> Col Expr ('Spec '[] 'Required Tag))
-> Tag
-> Col (Reify Expr) ('Spec '[] 'Required Tag)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr Tag -> Col Expr ('Spec '[] 'Required Tag)
forall a (labels :: Labels) (necessity :: Necessity).
Expr a -> Col Expr ('Spec labels necessity a)
E (Expr Tag -> Col Expr ('Spec '[] 'Required Tag))
-> (Tag -> Expr Tag) -> Tag -> Col Expr ('Spec '[] 'Required Tag)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tag -> Expr Tag
forall a. Sql DBType a => a -> Expr a
litExpr)


type GGDeconstruct :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type -> Type
type family GGDeconstruct algebra rep a r where
  GGDeconstruct 'K.Product rep a r =
    GConstruct TUnreify (Eval (rep (Reify Expr))) r -> a -> r
  GGDeconstruct 'K.Sum rep a r =
    GConstructADT TUnreify (Eval (rep (Reify Expr))) r (a -> r)


ggdeconstruct :: forall algebra rep 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 :: (a
 -> Eval
      (GGColumns algebra TColumns (Eval (rep (Reify Result))))
      (Col Expr))
-> GGDeconstruct algebra rep a r
ggdeconstruct a
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
gtoColumns = case KnownAlgebra algebra => SAlgebra algebra
forall (algebra :: Algebra).
KnownAlgebra algebra =>
SAlgebra algebra
algebraSing @algebra of
  SAlgebra algebra
SProduct -> \GConstruct TUnreify (Eval (rep (Reify Expr))) r
build ->
    GConstruct TUnreify (Eval (rep (Reify Expr))) r
-> GFields TUnreify (Eval (rep (Reify Expr))) -> r
forall (f :: * -> * -> *) (rep :: * -> *) a.
Representable f rep =>
GConstruct f rep a -> GFields f rep -> a
gindex @TUnreify @(Eval (rep (Reify Expr))) @r GConstruct TUnreify (Eval (rep (Reify Expr))) r
build (GFields TUnreify (Eval (rep (Reify Expr))) -> r)
-> (a -> GFields TUnreify (Eval (rep (Reify Expr)))) -> a -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    FromColumns
  (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr))
-> GColumns TColumns (Eval (rep (Reify Expr))) (Col (Reify Expr))
-> GFields TUnreify (Eval (rep (Reify Expr)))
forall (_Table :: * -> Exp Constraint)
       (_Columns :: * -> Exp HTable) (f :: * -> * -> *)
       (context :: HContext) (rep :: * -> *).
GConstructable _Table _Columns f context rep =>
FromColumns _Table _Columns f context
-> GColumns _Columns rep context -> GFields f rep
gdeconstruct
      @(TTable (Reify Expr))
      @TColumns
      @TUnreify
      @(Col (Reify Expr))
      @(Eval (rep (Reify Expr)))
      (\(proxy x
_ :: proxy x) -> (Reify Expr :~: Reify Expr) -> x -> Unreify x
forall (context :: Context) a (ctx :: Context).
Table context a =>
(context :~: Reify ctx) -> a -> Unreify a
unreify @_ @x Reify Expr :~: Reify Expr
forall k (a :: k). a :~: a
Refl (x -> Unreify x)
-> (Columns x (Col (Reify Expr)) -> x)
-> Columns x (Col (Reify Expr))
-> Unreify x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Columns x (Col (Reify Expr)) -> x
forall (context :: Context) a.
Table context a =>
Columns a (Col context) -> a
fromColumns) (Eval
   (GGColumns algebra TColumns (Eval (rep (Reify Result))))
   (Col (Reify Expr))
 -> GFields TUnreify (Eval (rep (Reify Expr))))
-> (a
    -> Eval
         (GGColumns algebra TColumns (Eval (rep (Reify Result))))
         (Col (Reify Expr)))
-> a
-> GFields TUnreify (Eval (rep (Reify Expr)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Eval
  (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result))))
     (Col (Reify Expr))
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col context) -> t (Col (Reify context))
hreify (Eval
   (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
 -> Eval
      (GGColumns algebra TColumns (Eval (rep (Reify Result))))
      (Col (Reify Expr)))
-> (a
    -> Eval
         (GGColumns algebra TColumns (Eval (rep (Reify Result))))
         (Col Expr))
-> a
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result))))
     (Col (Reify Expr))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    a
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
gtoColumns
  SAlgebra algebra
SSum ->
    (GConstructors TUnreify (Eval (rep (Reify Expr))) r -> a -> r)
-> GConstructADT TUnreify (Eval (rep (Reify Expr))) r (a -> r)
forall (f :: * -> * -> *) (rep :: * -> *) r a.
RepresentableConstructors f rep =>
(GConstructors f rep r -> a) -> GConstructADT f rep r a
gctabulate @TUnreify @(Eval (rep (Reify Expr))) @r @(a -> r) ((GConstructors TUnreify (Eval (rep (Reify Expr))) r -> a -> r)
 -> GConstructADT TUnreify (Eval (rep (Reify Expr))) r (a -> r))
-> (GConstructors TUnreify (Eval (rep (Reify Expr))) r -> a -> r)
-> GConstructADT TUnreify (Eval (rep (Reify Expr))) r (a -> r)
forall a b. (a -> b) -> a -> b
$ \GConstructors TUnreify (Eval (rep (Reify Expr))) r
constructors a
as ->
      let
        (HType (Reify (E tag)), NonEmpty (Tag, r)
cases) =
          FromColumns
  (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr))
-> Unnullifier (Col (Reify Expr))
-> GConstructors TUnreify (Eval (rep (Reify Expr))) r
-> GColumnsADT
     TColumns (Eval (rep (Reify Expr))) (Col (Reify Expr))
-> (HType Tag (Col (Reify Expr)), NonEmpty (Tag, r))
forall (_Table :: * -> Exp Constraint)
       (_Columns :: * -> Exp HTable) (f :: * -> * -> *)
       (context :: HContext) (rep :: * -> *) r.
GConstructableADT _Table _Columns f context rep =>
FromColumns _Table _Columns f context
-> Unnullifier context
-> GConstructors f rep r
-> GColumnsADT _Columns rep context
-> (HType Tag context, NonEmpty (Tag, r))
gdeconstructADT
            @(TTable (Reify Expr))
            @TColumns
            @TUnreify
            @(Col (Reify Expr))
            @(Eval (rep (Reify Expr)))
            (\(proxy x
_ :: proxy x) -> (Reify Expr :~: Reify Expr) -> x -> Unreify x
forall (context :: Context) a (ctx :: Context).
Table context a =>
(context :~: Reify ctx) -> a -> Unreify a
unreify @_ @x Reify Expr :~: Reify Expr
forall k (a :: k). a :~: a
Refl (x -> Unreify x)
-> (Columns x (Col (Reify Expr)) -> x)
-> Columns x (Col (Reify Expr))
-> Unreify x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Columns x (Col (Reify Expr)) -> x
forall (context :: Context) a.
Table context a =>
Columns a (Col context) -> a
fromColumns)
            (\SSpec {Nullity a
nullity :: Nullity a
nullity :: forall (labels :: Labels) (necessity :: Necessity) a.
SSpec ('Spec labels necessity a) -> Nullity a
nullity} -> case Nullity a
nullity of
              Nullity a
Null -> Col (Reify Expr) ('Spec labels necessity (Nullify a))
-> Col (Reify Expr) ('Spec labels necessity a)
forall a. a -> a
id
              Nullity a
NotNull -> \(Reify (E a)) -> Col Expr ('Spec labels necessity a)
-> Col (Reify Expr) ('Spec labels necessity a)
forall (context :: Context) (spec :: Spec).
Col context spec -> Col (Reify context) spec
Reify (Expr a -> Col Expr ('Spec labels necessity a)
forall a (labels :: Labels) (necessity :: Necessity).
Expr a -> Col Expr ('Spec labels necessity a)
E (Expr (Maybe a) -> Expr a
forall a. Expr (Maybe a) -> Expr a
unsafeUnnullify Expr a
Expr (Maybe a)
a)))
            GConstructors TUnreify (Eval (rep (Reify Expr))) r
constructors (GColumnsADT TColumns (Eval (rep (Reify Expr))) (Col (Reify Expr))
 -> (HType Tag (Col (Reify Expr)), NonEmpty (Tag, r)))
-> GColumnsADT
     TColumns (Eval (rep (Reify Expr))) (Col (Reify Expr))
-> (HType Tag (Col (Reify Expr)), NonEmpty (Tag, r))
forall a b. (a -> b) -> a -> b
$
          Eval
  (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result))))
     (Col (Reify Expr))
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col context) -> t (Col (Reify context))
hreify (Eval
   (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
 -> Eval
      (GGColumns algebra TColumns (Eval (rep (Reify Result))))
      (Col (Reify Expr)))
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result))))
     (Col (Reify Expr))
forall a b. (a -> b) -> a -> b
$
          a
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
gtoColumns a
as
      in
        case NonEmpty (Tag, r)
cases of
          ((Tag
_, r
r) :| (((Tag, r) -> (Expr Bool, r)) -> [(Tag, r)] -> [(Expr Bool, r)]
forall a b. (a -> b) -> [a] -> [b]
map ((Tag -> Expr Bool) -> (Tag, r) -> (Expr Bool, r)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((Expr Tag
tag Expr Tag -> Expr Tag -> Expr Bool
forall a. Sql DBEq a => Expr a -> Expr a -> Expr Bool
==.) (Expr Tag -> Expr Bool) -> (Tag -> Expr Tag) -> Tag -> Expr Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tag -> Expr Tag
forall a. Sql DBType a => a -> Expr a
litExpr)) -> [(Expr Bool, r)]
cases')) ->
            [(Expr Bool, r)] -> r -> r
forall a. Table Expr a => [(Expr Bool, a)] -> a -> a
case_ [(Expr Bool, r)]
cases' r
r


type GGName :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
type family GGName algebra rep a where
  GGName 'K.Product rep a = GConstruct TUnreify (Eval (rep (Reify Name))) a
  GGName 'K.Sum rep a = Name Tag -> GBuildADT TUnreify (Eval (rep (Reify Name))) a


ggname :: forall algebra rep a. GGConstructable algebra rep
  => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Name) -> a)
  -> GGName algebra rep a
ggname :: (Eval
   (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Name)
 -> a)
-> GGName algebra rep a
ggname Eval
  (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Name)
-> a
gfromColumns = case KnownAlgebra algebra => SAlgebra algebra
forall (algebra :: Algebra).
KnownAlgebra algebra =>
SAlgebra algebra
algebraSing @algebra of
  SAlgebra algebra
SProduct ->
    (GFields TUnreify (Eval (rep (Reify Name))) -> a)
-> GConstruct TUnreify (Eval (rep (Reify Name))) a
forall (f :: * -> * -> *) (rep :: * -> *) a.
Representable f rep =>
(GFields f rep -> a) -> GConstruct f rep a
gtabulate @TUnreify @(Eval (rep (Reify Name))) @a ((GFields TUnreify (Eval (rep (Reify Name))) -> a)
 -> GConstruct TUnreify (Eval (rep (Reify Name))) a)
-> (GFields TUnreify (Eval (rep (Reify Name))) -> a)
-> GConstruct TUnreify (Eval (rep (Reify Name))) a
forall a b. (a -> b) -> a -> b
$
    Eval
  (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Name)
-> a
gfromColumns (Eval
   (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Name)
 -> a)
-> (GFields TUnreify (Eval (rep (Reify Name)))
    -> Eval
         (GGColumns algebra TColumns (Eval (rep (Reify Result))))
         (Col Name))
-> GFields TUnreify (Eval (rep (Reify Name)))
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Eval
  (GGColumns algebra TColumns (Eval (rep (Reify Result))))
  (Col (Reify Name))
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Name)
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col (Reify context)) -> t (Col context)
hunreify (Eval
   (GGColumns algebra TColumns (Eval (rep (Reify Result))))
   (Col (Reify Name))
 -> Eval
      (GGColumns algebra TColumns (Eval (rep (Reify Result))))
      (Col Name))
-> (GFields TUnreify (Eval (rep (Reify Name)))
    -> Eval
         (GGColumns algebra TColumns (Eval (rep (Reify Result))))
         (Col (Reify Name)))
-> GFields TUnreify (Eval (rep (Reify Name)))
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Name)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    ToColumns
  (TTable (Reify Name)) TColumns TUnreify (Col (Reify Name))
-> GFields TUnreify (Eval (rep (Reify Name)))
-> GColumns TColumns (Eval (rep (Reify Name))) (Col (Reify Name))
forall (_Table :: * -> Exp Constraint)
       (_Columns :: * -> Exp HTable) (f :: * -> * -> *)
       (context :: HContext) (rep :: * -> *).
GConstructable _Table _Columns f context rep =>
ToColumns _Table _Columns f context
-> GFields f rep -> GColumns _Columns rep context
gconstruct
      @(TTable (Reify Name))
      @TColumns
      @TUnreify
      @(Col (Reify Name))
      @(Eval (rep (Reify Name)))
      (\(proxy x
_ :: proxy x) -> x -> Columns x (Col (Reify Name))
forall (context :: Context) a.
Table context a =>
a -> Columns a (Col context)
toColumns (x -> Columns x (Col (Reify Name)))
-> (Unreify x -> x) -> Unreify x -> Columns x (Col (Reify Name))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Reify Name :~: Reify Name) -> Unreify x -> x
forall (context :: Context) a (ctx :: Context).
Table context a =>
(context :~: Reify ctx) -> Unreify a -> a
reify @_ @x Reify Name :~: Reify Name
forall k (a :: k). a :~: a
Refl)
  SAlgebra algebra
SSum -> \Name Tag
tag ->
    (GFieldsADT TUnreify (Eval (rep (Reify Name))) -> a)
-> GBuildADT TUnreify (Eval (rep (Reify Name))) a
forall (f :: * -> * -> *) (rep :: * -> *) a.
RepresentableFields f rep =>
(GFieldsADT f rep -> a) -> GBuildADT f rep a
gftabulate @TUnreify @(Eval (rep (Reify Name))) @a ((GFieldsADT TUnreify (Eval (rep (Reify Name))) -> a)
 -> GBuildADT TUnreify (Eval (rep (Reify Name))) a)
-> (GFieldsADT TUnreify (Eval (rep (Reify Name))) -> a)
-> GBuildADT TUnreify (Eval (rep (Reify Name))) a
forall a b. (a -> b) -> a -> b
$
    Eval
  (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Name)
-> a
gfromColumns (Eval
   (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Name)
 -> a)
-> (GFieldsADT TUnreify (Eval (rep (Reify Name)))
    -> Eval
         (GGColumns algebra TColumns (Eval (rep (Reify Result))))
         (Col Name))
-> GFieldsADT TUnreify (Eval (rep (Reify Name)))
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Eval
  (GGColumns algebra TColumns (Eval (rep (Reify Result))))
  (Col (Reify Name))
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Name)
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col (Reify context)) -> t (Col context)
hunreify (Eval
   (GGColumns algebra TColumns (Eval (rep (Reify Result))))
   (Col (Reify Name))
 -> Eval
      (GGColumns algebra TColumns (Eval (rep (Reify Result))))
      (Col Name))
-> (GFieldsADT TUnreify (Eval (rep (Reify Name)))
    -> Eval
         (GGColumns algebra TColumns (Eval (rep (Reify Result))))
         (Col (Reify Name)))
-> GFieldsADT TUnreify (Eval (rep (Reify Name)))
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Name)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    ToColumns
  (TTable (Reify Name)) TColumns TUnreify (Col (Reify Name))
-> (Tag -> Nullifier (Col (Reify Name)))
-> HType Tag (Col (Reify Name))
-> GFieldsADT TUnreify (Eval (rep (Reify Name)))
-> GColumnsADT
     TColumns (Eval (rep (Reify Name))) (Col (Reify Name))
forall (_Table :: * -> Exp Constraint)
       (_Columns :: * -> Exp HTable) (f :: * -> * -> *)
       (context :: HContext) (rep :: * -> *).
GConstructableADT _Table _Columns f context rep =>
ToColumns _Table _Columns f context
-> (Tag -> Nullifier context)
-> HType Tag context
-> GFieldsADT f rep
-> GColumnsADT _Columns rep context
gbuildADT
      @(TTable (Reify Name))
      @TColumns
      @TUnreify
      @(Col (Reify Name))
      @(Eval (rep (Reify Name)))
      (\(proxy x
_ :: proxy x) -> x -> Columns x (Col (Reify Name))
forall (context :: Context) a.
Table context a =>
a -> Columns a (Col context)
toColumns (x -> Columns x (Col (Reify Name)))
-> (Unreify x -> x) -> Unreify x -> Columns x (Col (Reify Name))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Reify Name :~: Reify Name) -> Unreify x -> x
forall (context :: Context) a (ctx :: Context).
Table context a =>
(context :~: Reify ctx) -> Unreify a -> a
reify @_ @x Reify Name :~: Reify Name
forall k (a :: k). a :~: a
Refl)
      (\Tag
_ SSpec ('Spec labels necessity a)
_ (Reify (N (Name a))) -> Col Name ('Spec labels necessity (Nullify a))
-> Col (Reify Name) ('Spec labels necessity (Nullify a))
forall (context :: Context) (spec :: Spec).
Col context spec -> Col (Reify context) spec
Reify (Name (Nullify a) -> Col Name ('Spec labels necessity (Nullify a))
forall a (labels :: Labels) (necessity :: Necessity).
Name a -> Col Name ('Spec labels necessity a)
N (String -> Name (Nullify a)
forall k (a :: k). (k ~ *) => String -> Name a
Name String
a)))
      (Col (Reify Name) ('Spec '[] 'Required Tag)
-> HType Tag (Col (Reify Name))
forall (context :: HContext) a.
context ('Spec '[] 'Required a) -> HType a context
HType (Col Name ('Spec '[] 'Required Tag)
-> Col (Reify Name) ('Spec '[] 'Required Tag)
forall (context :: Context) (spec :: Spec).
Col context spec -> Col (Reify context) spec
Reify (Name Tag -> Col Name ('Spec '[] 'Required Tag)
forall a (labels :: Labels) (necessity :: Necessity).
Name a -> Col Name ('Spec labels necessity a)
N Name Tag
tag)))


type GGAggregate :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
type family GGAggregate algebra rep r where
  GGAggregate 'K.Product rep r =
    GConstruct TUnreify (Eval (rep (Reify Aggregate))) r ->
      GConstruct TUnreify (Eval (rep (Reify Expr))) r
  GGAggregate 'K.Sum rep r =
    GBuildADT TUnreify (Eval (rep (Reify Aggregate))) r ->
      GBuildADT TUnreify (Eval (rep (Reify Expr))) r


ggaggregate :: forall algebra rep 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 :: (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 Eval
  (GGColumns algebra TColumns (Eval (rep (Reify Result))))
  (Col Aggregate)
-> agg
gfromColumns exprs
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
gtoColumns GGAggregate algebra rep agg
agg exprs
es = case KnownAlgebra algebra => SAlgebra algebra
forall (algebra :: Algebra).
KnownAlgebra algebra =>
SAlgebra algebra
algebraSing @algebra of
  SAlgebra algebra
SProduct -> ((GFields TUnreify (Eval (rep (Reify Aggregate))) -> agg)
 -> GFields TUnreify (Eval (rep (Reify Expr))) -> agg)
-> GFields TUnreify (Eval (rep (Reify Expr)))
-> (GFields TUnreify (Eval (rep (Reify Aggregate))) -> agg)
-> agg
forall a b c. (a -> b -> c) -> b -> a -> c
flip (GFields TUnreify (Eval (rep (Reify Aggregate))) -> agg)
-> GFields TUnreify (Eval (rep (Reify Expr))) -> agg
f GFields TUnreify (Eval (rep (Reify Expr)))
exprs ((GFields TUnreify (Eval (rep (Reify Aggregate))) -> agg) -> agg)
-> (GFields TUnreify (Eval (rep (Reify Aggregate))) -> agg) -> agg
forall a b. (a -> b) -> a -> b
$
    Eval
  (GGColumns algebra TColumns (Eval (rep (Reify Result))))
  (Col Aggregate)
-> agg
gfromColumns (Eval
   (GGColumns algebra TColumns (Eval (rep (Reify Result))))
   (Col Aggregate)
 -> agg)
-> (GFields TUnreify (Eval (rep (Reify Aggregate)))
    -> Eval
         (GGColumns algebra TColumns (Eval (rep (Reify Result))))
         (Col Aggregate))
-> GFields TUnreify (Eval (rep (Reify Aggregate)))
-> agg
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Eval
  (GGColumns algebra TColumns (Eval (rep (Reify Result))))
  (Col (Reify Aggregate))
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result))))
     (Col Aggregate)
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col (Reify context)) -> t (Col context)
hunreify (Eval
   (GGColumns algebra TColumns (Eval (rep (Reify Result))))
   (Col (Reify Aggregate))
 -> Eval
      (GGColumns algebra TColumns (Eval (rep (Reify Result))))
      (Col Aggregate))
-> (GFields TUnreify (Eval (rep (Reify Aggregate)))
    -> Eval
         (GGColumns algebra TColumns (Eval (rep (Reify Result))))
         (Col (Reify Aggregate)))
-> GFields TUnreify (Eval (rep (Reify Aggregate)))
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result))))
     (Col Aggregate)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    ToColumns
  (TTable (Reify Aggregate))
  TColumns
  TUnreify
  (Col (Reify Aggregate))
-> GFields TUnreify (Eval (rep (Reify Aggregate)))
-> GColumns
     TColumns (Eval (rep (Reify Aggregate))) (Col (Reify Aggregate))
forall (_Table :: * -> Exp Constraint)
       (_Columns :: * -> Exp HTable) (f :: * -> * -> *)
       (context :: HContext) (rep :: * -> *).
GConstructable _Table _Columns f context rep =>
ToColumns _Table _Columns f context
-> GFields f rep -> GColumns _Columns rep context
gconstruct
      @(TTable (Reify Aggregate))
      @TColumns
      @TUnreify
      @(Col (Reify Aggregate))
      @(Eval (rep (Reify Aggregate)))
      (\(proxy x
_ :: proxy x) -> x -> Columns x (Col (Reify Aggregate))
forall (context :: Context) a.
Table context a =>
a -> Columns a (Col context)
toColumns (x -> Columns x (Col (Reify Aggregate)))
-> (Unreify x -> x)
-> Unreify x
-> Columns x (Col (Reify Aggregate))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Reify Aggregate :~: Reify Aggregate) -> Unreify x -> x
forall (context :: Context) a (ctx :: Context).
Table context a =>
(context :~: Reify ctx) -> Unreify a -> a
reify @_ @x Reify Aggregate :~: Reify Aggregate
forall k (a :: k). a :~: a
Refl)
    where
      f :: (GFields TUnreify (Eval (rep (Reify Aggregate))) -> agg)
-> GFields TUnreify (Eval (rep (Reify Expr))) -> agg
f =
        GConstruct TUnreify (Eval (rep (Reify Expr))) agg
-> GFields TUnreify (Eval (rep (Reify Expr))) -> agg
forall (f :: * -> * -> *) (rep :: * -> *) a.
Representable f rep =>
GConstruct f rep a -> GFields f rep -> a
gindex @TUnreify @(Eval (rep (Reify Expr))) @agg (GConstruct TUnreify (Eval (rep (Reify Expr))) agg
 -> GFields TUnreify (Eval (rep (Reify Expr))) -> agg)
-> ((GFields TUnreify (Eval (rep (Reify Aggregate))) -> agg)
    -> GConstruct TUnreify (Eval (rep (Reify Expr))) agg)
-> (GFields TUnreify (Eval (rep (Reify Aggregate))) -> agg)
-> GFields TUnreify (Eval (rep (Reify Expr)))
-> agg
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        GGAggregate algebra rep agg
GConstruct TUnreify (Eval (rep (Reify Aggregate))) agg
-> GConstruct TUnreify (Eval (rep (Reify Expr))) agg
agg (GConstruct TUnreify (Eval (rep (Reify Aggregate))) agg
 -> GConstruct TUnreify (Eval (rep (Reify Expr))) agg)
-> ((GFields TUnreify (Eval (rep (Reify Aggregate))) -> agg)
    -> GConstruct TUnreify (Eval (rep (Reify Aggregate))) agg)
-> (GFields TUnreify (Eval (rep (Reify Aggregate))) -> agg)
-> GConstruct TUnreify (Eval (rep (Reify Expr))) agg
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        (GFields TUnreify (Eval (rep (Reify Aggregate))) -> agg)
-> GConstruct TUnreify (Eval (rep (Reify Aggregate))) agg
forall (f :: * -> * -> *) (rep :: * -> *) a.
Representable f rep =>
(GFields f rep -> a) -> GConstruct f rep a
gtabulate @TUnreify @(Eval (rep (Reify Aggregate))) @agg
      exprs :: GFields TUnreify (Eval (rep (Reify Expr)))
exprs =
        FromColumns
  (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr))
-> GColumns TColumns (Eval (rep (Reify Expr))) (Col (Reify Expr))
-> GFields TUnreify (Eval (rep (Reify Expr)))
forall (_Table :: * -> Exp Constraint)
       (_Columns :: * -> Exp HTable) (f :: * -> * -> *)
       (context :: HContext) (rep :: * -> *).
GConstructable _Table _Columns f context rep =>
FromColumns _Table _Columns f context
-> GColumns _Columns rep context -> GFields f rep
gdeconstruct
          @(TTable (Reify Expr))
          @TColumns
          @TUnreify
          @(Col (Reify Expr))
          @(Eval (rep (Reify Expr)))
          (\(proxy x
_ :: proxy x) -> (Reify Expr :~: Reify Expr) -> x -> Unreify x
forall (context :: Context) a (ctx :: Context).
Table context a =>
(context :~: Reify ctx) -> a -> Unreify a
unreify @_ @x Reify Expr :~: Reify Expr
forall k (a :: k). a :~: a
Refl (x -> Unreify x)
-> (Columns x (Col (Reify Expr)) -> x)
-> Columns x (Col (Reify Expr))
-> Unreify x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Columns x (Col (Reify Expr)) -> x
forall (context :: Context) a.
Table context a =>
Columns a (Col context) -> a
fromColumns) (GColumns TColumns (Eval (rep (Reify Expr))) (Col (Reify Expr))
 -> GFields TUnreify (Eval (rep (Reify Expr))))
-> GColumns TColumns (Eval (rep (Reify Expr))) (Col (Reify Expr))
-> GFields TUnreify (Eval (rep (Reify Expr)))
forall a b. (a -> b) -> a -> b
$
        Eval
  (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result))))
     (Col (Reify Expr))
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col context) -> t (Col (Reify context))
hreify (Eval
   (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
 -> Eval
      (GGColumns algebra TColumns (Eval (rep (Reify Result))))
      (Col (Reify Expr)))
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result))))
     (Col (Reify Expr))
forall a b. (a -> b) -> a -> b
$
        exprs
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
gtoColumns exprs
es
  SAlgebra algebra
SSum -> ((GFieldsADT TUnreify (Eval (rep (Reify Aggregate))) -> agg)
 -> GFieldsADT TUnreify (Eval (rep (Reify Expr))) -> agg)
-> GFieldsADT TUnreify (Eval (rep (Reify Expr)))
-> (GFieldsADT TUnreify (Eval (rep (Reify Aggregate))) -> agg)
-> agg
forall a b c. (a -> b -> c) -> b -> a -> c
flip (GFieldsADT TUnreify (Eval (rep (Reify Aggregate))) -> agg)
-> GFieldsADT TUnreify (Eval (rep (Reify Expr))) -> agg
f GFieldsADT TUnreify (Eval (rep (Reify Expr)))
exprs ((GFieldsADT TUnreify (Eval (rep (Reify Aggregate))) -> agg)
 -> agg)
-> (GFieldsADT TUnreify (Eval (rep (Reify Aggregate))) -> agg)
-> agg
forall a b. (a -> b) -> a -> b
$
    Eval
  (GGColumns algebra TColumns (Eval (rep (Reify Result))))
  (Col Aggregate)
-> agg
gfromColumns (Eval
   (GGColumns algebra TColumns (Eval (rep (Reify Result))))
   (Col Aggregate)
 -> agg)
-> (GFieldsADT TUnreify (Eval (rep (Reify Aggregate)))
    -> Eval
         (GGColumns algebra TColumns (Eval (rep (Reify Result))))
         (Col Aggregate))
-> GFieldsADT TUnreify (Eval (rep (Reify Aggregate)))
-> agg
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Eval
  (GGColumns algebra TColumns (Eval (rep (Reify Result))))
  (Col (Reify Aggregate))
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result))))
     (Col Aggregate)
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col (Reify context)) -> t (Col context)
hunreify (Eval
   (GGColumns algebra TColumns (Eval (rep (Reify Result))))
   (Col (Reify Aggregate))
 -> Eval
      (GGColumns algebra TColumns (Eval (rep (Reify Result))))
      (Col Aggregate))
-> (GFieldsADT TUnreify (Eval (rep (Reify Aggregate)))
    -> Eval
         (GGColumns algebra TColumns (Eval (rep (Reify Result))))
         (Col (Reify Aggregate)))
-> GFieldsADT TUnreify (Eval (rep (Reify Aggregate)))
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result))))
     (Col Aggregate)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    ToColumns
  (TTable (Reify Aggregate))
  TColumns
  TUnreify
  (Col (Reify Aggregate))
-> (Tag -> Nullifier (Col (Reify Aggregate)))
-> HType Tag (Col (Reify Aggregate))
-> GFieldsADT TUnreify (Eval (rep (Reify Aggregate)))
-> GColumnsADT
     TColumns (Eval (rep (Reify Aggregate))) (Col (Reify Aggregate))
forall (_Table :: * -> Exp Constraint)
       (_Columns :: * -> Exp HTable) (f :: * -> * -> *)
       (context :: HContext) (rep :: * -> *).
GConstructableADT _Table _Columns f context rep =>
ToColumns _Table _Columns f context
-> (Tag -> Nullifier context)
-> HType Tag context
-> GFieldsADT f rep
-> GColumnsADT _Columns rep context
gbuildADT
      @(TTable (Reify Aggregate))
      @TColumns
      @TUnreify
      @(Col (Reify Aggregate))
      @(Eval (rep (Reify Aggregate)))
      (\(proxy x
_ :: proxy x) -> x -> Columns x (Col (Reify Aggregate))
forall (context :: Context) a.
Table context a =>
a -> Columns a (Col context)
toColumns (x -> Columns x (Col (Reify Aggregate)))
-> (Unreify x -> x)
-> Unreify x
-> Columns x (Col (Reify Aggregate))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Reify Aggregate :~: Reify Aggregate) -> Unreify x -> x
forall (context :: Context) a (ctx :: Context).
Table context a =>
(context :~: Reify ctx) -> Unreify a -> a
reify @_ @x Reify Aggregate :~: Reify Aggregate
forall k (a :: k). a :~: a
Refl)
      (\Tag
tag' SSpec {Nullity a
nullity :: Nullity a
nullity :: forall (labels :: Labels) (necessity :: Necessity) a.
SSpec ('Spec labels necessity a) -> Nullity a
nullity} (Reify (A (Aggregate a))) ->
        Col Aggregate ('Spec labels necessity (Nullify a))
-> Col (Reify Aggregate) ('Spec labels necessity (Nullify a))
forall (context :: Context) (spec :: Spec).
Col context spec -> Col (Reify context) spec
Reify (Col Aggregate ('Spec labels necessity (Nullify a))
 -> Col (Reify Aggregate) ('Spec labels necessity (Nullify a)))
-> Col Aggregate ('Spec labels necessity (Nullify a))
-> Col (Reify Aggregate) ('Spec labels necessity (Nullify a))
forall a b. (a -> b) -> a -> b
$ Aggregate (Nullify a)
-> Col Aggregate ('Spec labels necessity (Nullify a))
forall a (labels :: Labels) (necessity :: Necessity).
Aggregate a -> Col Aggregate ('Spec labels necessity a)
A (Aggregate (Nullify a)
 -> Col Aggregate ('Spec labels necessity (Nullify a)))
-> Aggregate (Nullify a)
-> Col Aggregate ('Spec labels necessity (Nullify a))
forall a b. (a -> b) -> a -> b
$ Aggregator () (Expr (Nullify a)) -> Aggregate (Nullify a)
forall k (a :: k). Aggregator () (Expr a) -> Aggregate a
Aggregate (Aggregator () (Expr (Nullify a)) -> Aggregate (Nullify a))
-> Aggregator () (Expr (Nullify a)) -> Aggregate (Nullify a)
forall a b. (a -> b) -> a -> b
$ Nullity a -> Expr Bool -> Expr a -> Expr (Nullify a)
forall a. Nullity a -> Expr Bool -> Expr a -> Expr (Nullify a)
runTag Nullity a
nullity (Expr Tag
tag Expr Tag -> Expr Tag -> Expr Bool
forall a. Sql DBEq a => Expr a -> Expr a -> Expr Bool
==. Tag -> Expr Tag
forall a. Sql DBType a => a -> Expr a
litExpr Tag
tag') (Expr a -> Expr (Nullify a))
-> Aggregator () (Expr a) -> Aggregator () (Expr (Nullify a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Aggregator () (Expr a)
Aggregator () (Expr a)
a)
      (Col (Reify Aggregate) ('Spec '[] 'Required Tag)
-> HType Tag (Col (Reify Aggregate))
forall (context :: HContext) a.
context ('Spec '[] 'Required a) -> HType a context
HType (Col Aggregate ('Spec '[] 'Required Tag)
-> Col (Reify Aggregate) ('Spec '[] 'Required Tag)
forall (context :: Context) (spec :: Spec).
Col context spec -> Col (Reify context) spec
Reify (Aggregate Tag -> Col Aggregate ('Spec '[] 'Required Tag)
forall a (labels :: Labels) (necessity :: Necessity).
Aggregate a -> Col Aggregate ('Spec labels necessity a)
A (Expr Tag -> Aggregate Tag
forall a. Sql DBEq a => Expr a -> Aggregate a
groupByExpr Expr Tag
tag))))
    where
      f :: (GFieldsADT TUnreify (Eval (rep (Reify Aggregate))) -> agg)
-> GFieldsADT TUnreify (Eval (rep (Reify Expr))) -> agg
f =
        GBuildADT TUnreify (Eval (rep (Reify Expr))) agg
-> GFieldsADT TUnreify (Eval (rep (Reify Expr))) -> agg
forall (f :: * -> * -> *) (rep :: * -> *) a.
RepresentableFields f rep =>
GBuildADT f rep a -> GFieldsADT f rep -> a
gfindex @TUnreify @(Eval (rep (Reify Expr))) @agg (GBuildADT TUnreify (Eval (rep (Reify Expr))) agg
 -> GFieldsADT TUnreify (Eval (rep (Reify Expr))) -> agg)
-> ((GFieldsADT TUnreify (Eval (rep (Reify Aggregate))) -> agg)
    -> GBuildADT TUnreify (Eval (rep (Reify Expr))) agg)
-> (GFieldsADT TUnreify (Eval (rep (Reify Aggregate))) -> agg)
-> GFieldsADT TUnreify (Eval (rep (Reify Expr)))
-> agg
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        GGAggregate algebra rep agg
GBuildADT TUnreify (Eval (rep (Reify Aggregate))) agg
-> GBuildADT TUnreify (Eval (rep (Reify Expr))) agg
agg (GBuildADT TUnreify (Eval (rep (Reify Aggregate))) agg
 -> GBuildADT TUnreify (Eval (rep (Reify Expr))) agg)
-> ((GFieldsADT TUnreify (Eval (rep (Reify Aggregate))) -> agg)
    -> GBuildADT TUnreify (Eval (rep (Reify Aggregate))) agg)
-> (GFieldsADT TUnreify (Eval (rep (Reify Aggregate))) -> agg)
-> GBuildADT TUnreify (Eval (rep (Reify Expr))) agg
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        (GFieldsADT TUnreify (Eval (rep (Reify Aggregate))) -> agg)
-> GBuildADT TUnreify (Eval (rep (Reify Aggregate))) agg
forall (f :: * -> * -> *) (rep :: * -> *) a.
RepresentableFields f rep =>
(GFieldsADT f rep -> a) -> GBuildADT f rep a
gftabulate @TUnreify @(Eval (rep (Reify Aggregate))) @agg
      (HType (Reify (E tag)), GFieldsADT TUnreify (Eval (rep (Reify Expr)))
exprs) =
        FromColumns
  (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr))
-> Unnullifier (Col (Reify Expr))
-> GColumnsADT
     TColumns (Eval (rep (Reify Expr))) (Col (Reify Expr))
-> (HType Tag (Col (Reify Expr)),
    GFieldsADT TUnreify (Eval (rep (Reify Expr))))
forall (_Table :: * -> Exp Constraint)
       (_Columns :: * -> Exp HTable) (f :: * -> * -> *)
       (context :: HContext) (rep :: * -> *).
GConstructableADT _Table _Columns f context rep =>
FromColumns _Table _Columns f context
-> Unnullifier context
-> GColumnsADT _Columns rep context
-> (HType Tag context, GFieldsADT f rep)
gunbuildADT
          @(TTable (Reify Expr))
          @TColumns
          @TUnreify
          @(Col (Reify Expr))
          @(Eval (rep (Reify Expr)))
          (\(proxy x
_ :: proxy x) -> (Reify Expr :~: Reify Expr) -> x -> Unreify x
forall (context :: Context) a (ctx :: Context).
Table context a =>
(context :~: Reify ctx) -> a -> Unreify a
unreify @_ @x Reify Expr :~: Reify Expr
forall k (a :: k). a :~: a
Refl (x -> Unreify x)
-> (Columns x (Col (Reify Expr)) -> x)
-> Columns x (Col (Reify Expr))
-> Unreify x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Columns x (Col (Reify Expr)) -> x
forall (context :: Context) a.
Table context a =>
Columns a (Col context) -> a
fromColumns)
          (\SSpec {Nullity a
nullity :: Nullity a
nullity :: forall (labels :: Labels) (necessity :: Necessity) a.
SSpec ('Spec labels necessity a) -> Nullity a
nullity} -> case Nullity a
nullity of
            Nullity a
Null -> Col (Reify Expr) ('Spec labels necessity (Nullify a))
-> Col (Reify Expr) ('Spec labels necessity a)
forall a. a -> a
id
            Nullity a
NotNull -> \(Reify (E a)) -> Col Expr ('Spec labels necessity a)
-> Col (Reify Expr) ('Spec labels necessity a)
forall (context :: Context) (spec :: Spec).
Col context spec -> Col (Reify context) spec
Reify (Expr a -> Col Expr ('Spec labels necessity a)
forall a (labels :: Labels) (necessity :: Necessity).
Expr a -> Col Expr ('Spec labels necessity a)
E (Expr (Maybe a) -> Expr a
forall a. Expr (Maybe a) -> Expr a
unsafeUnnullify Expr a
Expr (Maybe a)
a))) (GColumnsADT TColumns (Eval (rep (Reify Expr))) (Col (Reify Expr))
 -> (HType Tag (Col (Reify Expr)),
     GFieldsADT TUnreify (Eval (rep (Reify Expr)))))
-> GColumnsADT
     TColumns (Eval (rep (Reify Expr))) (Col (Reify Expr))
-> (HType Tag (Col (Reify Expr)),
    GFieldsADT TUnreify (Eval (rep (Reify Expr))))
forall a b. (a -> b) -> a -> b
$
        Eval
  (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result))))
     (Col (Reify Expr))
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col context) -> t (Col (Reify context))
hreify (Eval
   (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
 -> Eval
      (GGColumns algebra TColumns (Eval (rep (Reify Result))))
      (Col (Reify Expr)))
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result))))
     (Col (Reify Expr))
forall a b. (a -> b) -> a -> b
$
        exprs
-> Eval
     (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr)
gtoColumns exprs
es