{-# 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.ADT
( ADT( ADT )
, ADTable, fromADT, toADT
, BuildableADT
, BuildADT, buildADT
, InsertADT, insertADT
, ConstructableADT
, ConstructADT, constructADT
, DeconstructADT, deconstructADT
, NameADT, nameADT
, AggregateADT, aggregateADT
, ADTRep
)
where
import Data.Kind ( Constraint, Type )
import Data.Proxy ( Proxy( Proxy ) )
import Data.Type.Equality ( (:~:)( Refl ) )
import GHC.Generics ( Generic, Rep, from, to )
import GHC.TypeLits ( Symbol )
import Prelude
import Rel8.Aggregate ( Aggregate )
import Rel8.Expr ( Expr )
import Rel8.FCF ( Eval, Exp )
import Rel8.Generic.Construction
( GGBuildable
, GGBuild, ggbuild
, GGInsert, gginsert
, GGConstructable
, GGConstruct, ggconstruct
, GGDeconstruct, ggdeconstruct
, GGName, ggname
, GGAggregate, ggaggregate
)
import Rel8.Generic.Map ( GMappable, GMap, gmap, gunmap )
import Rel8.Generic.Record ( GRecordable, GRecord, grecord, gunrecord )
import Rel8.Generic.Rel8able
( Rel8able
, GRep, GColumns, gfromColumns, gtoColumns
, greify, gunreify
)
import qualified Rel8.Generic.Table.ADT as G
import qualified Rel8.Kind.Algebra as K
import Rel8.Schema.Context ( Col )
import Rel8.Schema.HTable ( HTable )
import Rel8.Schema.Insert ( Insert )
import qualified Rel8.Schema.Kind as K
import Rel8.Schema.Name ( Name )
import Rel8.Schema.Reify ( Col( Reify ), Reify, hreify, hunreify )
import Rel8.Schema.Result ( Result )
import Rel8.Table
( Table
, fromColumns, toColumns, reify, unreify
, TTable, TColumns, TUnreify
)
type ADT :: K.Rel8able -> K.Rel8able
newtype ADT t context = ADT (GColumnsADT t (Col context))
instance ADTable t => Rel8able (ADT t) where
type GColumns (ADT t) = GColumnsADT t
gfromColumns :: GColumns (ADT t) (Col (Reify context)) -> ADT t (Reify context)
gfromColumns = GColumns (ADT t) (Col (Reify context)) -> ADT t (Reify context)
forall (t :: Rel8able) (context :: Context).
GColumnsADT t (Col context) -> ADT t context
ADT
gtoColumns :: ADT t (Reify context) -> GColumns (ADT t) (Col (Reify context))
gtoColumns (ADT GColumnsADT t (Col (Reify context))
a) = GColumnsADT t (Col (Reify context))
GColumns (ADT t) (Col (Reify context))
a
greify :: ADT t context -> ADT t (Reify context)
greify (ADT GColumnsADT t (Col context)
a) = GColumnsADT t (Col (Reify context)) -> ADT t (Reify context)
forall (t :: Rel8able) (context :: Context).
GColumnsADT t (Col context) -> ADT t context
ADT (GColumnsADT
TColumns (GRecord (Rep (t (Reify Result)))) (Col context)
-> GColumnsADT
TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify context))
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col context) -> t (Col (Reify context))
hreify GColumnsADT t (Col context)
GColumnsADT
TColumns (GRecord (Rep (t (Reify Result)))) (Col context)
a)
gunreify :: ADT t (Reify context) -> ADT t context
gunreify (ADT GColumnsADT t (Col (Reify context))
a) = GColumnsADT t (Col context) -> ADT t context
forall (t :: Rel8able) (context :: Context).
GColumnsADT t (Col context) -> ADT t context
ADT (GColumnsADT
TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify context))
-> GColumnsADT
TColumns (GRecord (Rep (t (Reify Result)))) (Col context)
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col (Reify context)) -> t (Col context)
hunreify GColumnsADT t (Col (Reify context))
GColumnsADT
TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify context))
a)
instance (ADTable t, context ~ Result) => Generic (ADT t context) where
type Rep (ADT t context) = Rep (t context)
from :: ADT t context -> Rep (ADT t context) x
from =
Proxy TUnreify
-> (forall a.
Eval (TTable (Reify Result) a) =>
a -> Eval (TUnreify a))
-> Rep (t (Reify Result)) x
-> GMap TUnreify (Rep (t (Reify Result))) 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 Result)) (Proxy TUnreify
forall k (t :: k). Proxy t
Proxy @TUnreify) ((Reify Result :~: Reify Result) -> a -> Unreify a
forall (context :: Context) a (ctx :: Context).
Table context a =>
(context :~: Reify ctx) -> a -> Unreify a
unreify Reify Result :~: Reify Result
forall k (a :: k). a :~: a
Refl) (Rep (t (Reify Result)) x -> Rep (t Result) x)
-> (ADT t context -> Rep (t (Reify Result)) x)
-> ADT t context
-> Rep (t Result) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall x.
GRecordable (Rep (t (Reify Result))) =>
GRecord (Rep (t (Reify Result))) x -> Rep (t (Reify Result)) x
forall (rep :: * -> *) x. GRecordable rep => GRecord rep x -> rep x
gunrecord @(Rep (t (Reify Result))) (GRecord (Rep (t (Reify Result))) x -> Rep (t (Reify Result)) x)
-> (ADT t context -> GRecord (Rep (t (Reify Result))) x)
-> ADT t context
-> Rep (t (Reify Result)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
(forall (spec :: Spec). Col (Reify Result) spec -> Col Result spec)
-> (forall (spec :: Spec).
Col Result spec -> Col (Reify Result) spec)
-> (forall a.
Eval (TTable (Reify Result) a) =>
Eval (TColumns a) (Col (Reify Result)) -> a)
-> GColumnsADT
TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Result))
-> GRecord (Rep (t (Reify Result))) x
forall (_Table :: * -> Exp Constraint)
(_Columns :: * -> Exp HTable) (context :: HContext) (rep :: * -> *)
x.
GTableADT _Table _Columns context rep =>
(forall (spec :: Spec). context spec -> Col Result spec)
-> (forall (spec :: Spec). Col Result spec -> context spec)
-> (forall a. Eval (_Table a) => Eval (_Columns a) context -> a)
-> GColumnsADT _Columns rep context
-> rep x
G.gfromColumnsADT
@(TTable (Reify Result))
@TColumns
(\(Reify a) -> Col Result spec
a)
forall (spec :: Spec). Col Result spec -> Col (Reify Result) spec
forall (context :: Context) (spec :: Spec).
Col context spec -> Col (Reify context) spec
Reify
forall a.
Eval (TTable (Reify Result) a) =>
Eval (TColumns a) (Col (Reify Result)) -> a
forall (context :: Context) a.
Table context a =>
Columns a (Col context) -> a
fromColumns (GColumnsADT
TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Result))
-> GRecord (Rep (t (Reify Result))) x)
-> (ADT t context
-> GColumnsADT
TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Result)))
-> ADT t context
-> GRecord (Rep (t (Reify Result))) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
GColumnsADT
TColumns (GRecord (Rep (t (Reify Result)))) (Col Result)
-> GColumnsADT
TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Result))
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col context) -> t (Col (Reify context))
hreify (GColumnsADT
TColumns (GRecord (Rep (t (Reify Result)))) (Col Result)
-> GColumnsADT
TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Result)))
-> (ADT t context
-> GColumnsADT
TColumns (GRecord (Rep (t (Reify Result)))) (Col Result))
-> ADT t context
-> GColumnsADT
TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Result))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
(\(ADT GColumnsADT t (Col context)
a) -> GColumnsADT t (Col context)
GColumnsADT
TColumns (GRecord (Rep (t (Reify Result)))) (Col Result)
a)
to :: Rep (ADT t context) x -> ADT t context
to =
GColumnsADT
TColumns (GRecord (Rep (t (Reify Result)))) (Col Result)
-> ADT t context
forall (t :: Rel8able) (context :: Context).
GColumnsADT t (Col context) -> ADT t context
ADT (GColumnsADT
TColumns (GRecord (Rep (t (Reify Result)))) (Col Result)
-> ADT t context)
-> (Rep (t Result) x
-> GColumnsADT
TColumns (GRecord (Rep (t (Reify Result)))) (Col Result))
-> Rep (t Result) x
-> ADT t context
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
GColumnsADT
TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Result))
-> GColumnsADT
TColumns (GRecord (Rep (t (Reify Result)))) (Col Result)
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col (Reify context)) -> t (Col context)
hunreify (GColumnsADT
TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Result))
-> GColumnsADT
TColumns (GRecord (Rep (t (Reify Result)))) (Col Result))
-> (Rep (t Result) x
-> GColumnsADT
TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Result)))
-> Rep (t Result) x
-> GColumnsADT
TColumns (GRecord (Rep (t (Reify Result)))) (Col Result)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
(forall (spec :: Spec). Col (Reify Result) spec -> Col Result spec)
-> (forall (spec :: Spec).
Col Result spec -> Col (Reify Result) spec)
-> (forall a.
Eval (TTable (Reify Result) a) =>
a -> Eval (TColumns a) (Col (Reify Result)))
-> GRecord (Rep (t (Reify Result))) x
-> GColumnsADT
TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Result))
forall (_Table :: * -> Exp Constraint)
(_Columns :: * -> Exp HTable) (context :: HContext) (rep :: * -> *)
x.
GTableADT _Table _Columns context rep =>
(forall (spec :: Spec). context spec -> Col Result spec)
-> (forall (spec :: Spec). Col Result spec -> context spec)
-> (forall a. Eval (_Table a) => a -> Eval (_Columns a) context)
-> rep x
-> GColumnsADT _Columns rep context
G.gtoColumnsADT
@(TTable (Reify Result))
@TColumns
(\(Reify a) -> Col Result spec
a)
forall (spec :: Spec). Col Result spec -> Col (Reify Result) spec
forall (context :: Context) (spec :: Spec).
Col context spec -> Col (Reify context) spec
Reify
forall a.
Eval (TTable (Reify Result) a) =>
a -> Eval (TColumns a) (Col (Reify Result))
forall (context :: Context) a.
Table context a =>
a -> Columns a (Col context)
toColumns (GRecord (Rep (t (Reify Result))) x
-> GColumnsADT
TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Result)))
-> (Rep (t Result) x -> GRecord (Rep (t (Reify Result))) x)
-> Rep (t Result) x
-> GColumnsADT
TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Result))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall x.
GRecordable (Rep (t (Reify Result))) =>
Rep (t (Reify Result)) x -> GRecord (Rep (t (Reify Result))) x
forall (rep :: * -> *) x. GRecordable rep => rep x -> GRecord rep x
grecord @(Rep (t (Reify Result))) (Rep (t (Reify Result)) x -> GRecord (Rep (t (Reify Result))) x)
-> (Rep (t Result) x -> Rep (t (Reify Result)) x)
-> Rep (t Result) x
-> GRecord (Rep (t (Reify Result))) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
Proxy TUnreify
-> (forall a.
Eval (TTable (Reify Result) a) =>
Eval (TUnreify a) -> a)
-> GMap TUnreify (Rep (t (Reify Result))) x
-> Rep (t (Reify Result)) 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 Result)) (Proxy TUnreify
forall k (t :: k). Proxy t
Proxy @TUnreify) ((Reify Result :~: Reify Result) -> Unreify a -> a
forall (context :: Context) a (ctx :: Context).
Table context a =>
(context :~: Reify ctx) -> Unreify a -> a
reify Reify Result :~: Reify Result
forall k (a :: k). a :~: a
Refl)
fromADT :: ADTable t => ADT t Result -> t Result
fromADT :: ADT t Result -> t Result
fromADT = Rep (t Result) Any -> t Result
forall a x. Generic a => Rep a x -> a
to (Rep (t Result) Any -> t Result)
-> (ADT t Result -> Rep (t Result) Any) -> ADT t Result -> t Result
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ADT t Result -> Rep (t Result) Any
forall a x. Generic a => a -> Rep a x
from
toADT :: ADTable t => t Result -> ADT t Result
toADT :: t Result -> ADT t Result
toADT = Rep (t Result) Any -> ADT t Result
forall a x. Generic a => Rep a x -> a
to (Rep (t Result) Any -> ADT t Result)
-> (t Result -> Rep (t Result) Any) -> t Result -> ADT t Result
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t Result -> Rep (t Result) Any
forall a x. Generic a => a -> Rep a x
from
type ADTable :: K.Rel8able -> Constraint
class
( Generic (t Result)
, HTable (GColumnsADT t)
, G.GTableADT (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRecord (Rep (t (Reify Result))))
, GRecordable (Rep (t (Reify Result)))
, GMappable (TTable (Reify Result)) (Rep (t (Reify Result)))
, GMap TUnreify (Rep (t (Reify Result))) ~ Rep (t Result)
)
=> ADTable t
instance
( Generic (t Result)
, HTable (GColumnsADT t)
, G.GTableADT (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRecord (Rep (t (Reify Result))))
, GRecordable (Rep (t (Reify Result)))
, GMappable (TTable (Reify Result)) (Rep (t (Reify Result)))
, GMap TUnreify (Rep (t (Reify Result))) ~ Rep (t Result)
)
=> ADTable t
type BuildableADT :: K.Rel8able -> Symbol -> Constraint
class GGBuildable 'K.Sum name (ADTRep t) => BuildableADT t name
instance GGBuildable 'K.Sum name (ADTRep t) => BuildableADT t name
type BuildADT :: K.Rel8able -> Symbol -> Type
type BuildADT t name = GGBuild 'K.Sum name (ADTRep t) (ADT t Expr)
buildADT :: forall t name. BuildableADT t name => BuildADT t name
buildADT :: BuildADT t name
buildADT =
(Eval
(GGColumns 'Sum TColumns (Eval (ADTRep t (Reify Result))))
(Col Expr)
-> ADT t Expr)
-> BuildADT t 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 @'K.Sum @name @(ADTRep t) @(ADT t Expr) Eval
(GGColumns 'Sum TColumns (Eval (ADTRep t (Reify Result))))
(Col Expr)
-> ADT t Expr
forall (t :: Rel8able) (context :: Context).
GColumnsADT t (Col context) -> ADT t context
ADT
type InsertADT :: K.Rel8able -> Symbol -> Type
type InsertADT t name = GGInsert 'K.Sum name (ADTRep t) (ADT t Insert)
insertADT :: forall t name. BuildableADT t name => InsertADT t name
insertADT :: InsertADT t name
insertADT =
(Eval
(GGColumns 'Sum TColumns (Eval (ADTRep t (Reify Result))))
(Col Insert)
-> ADT t Insert)
-> InsertADT t name
forall (algebra :: Algebra) (name :: Symbol)
(rep :: Context -> Exp (* -> *)) a.
GGBuildable algebra name rep =>
(Eval
(GGColumns algebra TColumns (Eval (rep (Reify Result))))
(Col Insert)
-> a)
-> GGInsert algebra name rep a
gginsert @'K.Sum @name @(ADTRep t) @(ADT t Insert) Eval
(GGColumns 'Sum TColumns (Eval (ADTRep t (Reify Result))))
(Col Insert)
-> ADT t Insert
forall (t :: Rel8able) (context :: Context).
GColumnsADT t (Col context) -> ADT t context
ADT
type ConstructableADT :: K.Rel8able -> Constraint
class GGConstructable 'K.Sum (ADTRep t) => ConstructableADT t
instance GGConstructable 'K.Sum (ADTRep t) => ConstructableADT t
type ConstructADT :: K.Rel8able -> Type
type ConstructADT t = forall r. GGConstruct 'K.Sum (ADTRep t) r
constructADT :: forall t. ConstructableADT t => ConstructADT t -> ADT t Expr
constructADT :: ConstructADT t -> ADT t Expr
constructADT ConstructADT t
f =
(Eval
(GGColumns 'Sum TColumns (Eval (ADTRep t (Reify Result))))
(Col Expr)
-> ADT t Expr)
-> GGConstruct 'Sum (ADTRep t) (ADT t Expr) -> ADT t 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 @'K.Sum @(ADTRep t) @(ADT t Expr) Eval
(GGColumns 'Sum TColumns (Eval (ADTRep t (Reify Result))))
(Col Expr)
-> ADT t Expr
forall (t :: Rel8able) (context :: Context).
GColumnsADT t (Col context) -> ADT t context
ADT
(GGConstruct 'Sum (ADTRep t) (ADT t Expr)
ConstructADT t
f @(ADT t Expr))
type DeconstructADT :: K.Rel8able -> Type -> Type
type DeconstructADT t r = GGDeconstruct 'K.Sum (ADTRep t) (ADT t Expr) r
deconstructADT :: forall t r. (ConstructableADT t, Table Expr r)
=> DeconstructADT t r
deconstructADT :: DeconstructADT t r
deconstructADT =
(ADT t Expr
-> Eval
(GGColumns 'Sum TColumns (Eval (ADTRep t (Reify Result))))
(Col Expr))
-> DeconstructADT t 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 @'K.Sum @(ADTRep t) @(ADT t Expr) @r (\(ADT GColumnsADT t (Col Expr)
a) -> Eval
(GGColumns 'Sum TColumns (Eval (ADTRep t (Reify Result))))
(Col Expr)
GColumnsADT t (Col Expr)
a)
type NameADT :: K.Rel8able -> Type
type NameADT t = GGName 'K.Sum (ADTRep t) (ADT t Name)
nameADT :: forall t. ConstructableADT t => NameADT t
nameADT :: NameADT t
nameADT = (Eval
(GGColumns 'Sum TColumns (Eval (ADTRep t (Reify Result))))
(Col Name)
-> ADT t Name)
-> NameADT t
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 @'K.Sum @(ADTRep t) @(ADT t Name) Eval
(GGColumns 'Sum TColumns (Eval (ADTRep t (Reify Result))))
(Col Name)
-> ADT t Name
forall (t :: Rel8able) (context :: Context).
GColumnsADT t (Col context) -> ADT t context
ADT
type AggregateADT :: K.Rel8able -> Type
type AggregateADT t = forall r. GGAggregate 'K.Sum (ADTRep t) r
aggregateADT :: forall t. ConstructableADT t
=> AggregateADT t -> ADT t Expr -> ADT t Aggregate
aggregateADT :: AggregateADT t -> ADT t Expr -> ADT t Aggregate
aggregateADT AggregateADT t
f =
(Eval
(GGColumns 'Sum TColumns (Eval (ADTRep t (Reify Result))))
(Col Aggregate)
-> ADT t Aggregate)
-> (ADT t Expr
-> Eval
(GGColumns 'Sum TColumns (Eval (ADTRep t (Reify Result))))
(Col Expr))
-> GGAggregate 'Sum (ADTRep t) (ADT t Aggregate)
-> ADT t Expr
-> ADT t 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 @'K.Sum @(ADTRep t) @(ADT t Expr) @(ADT t Aggregate) Eval
(GGColumns 'Sum TColumns (Eval (ADTRep t (Reify Result))))
(Col Aggregate)
-> ADT t Aggregate
forall (t :: Rel8able) (context :: Context).
GColumnsADT t (Col context) -> ADT t context
ADT (\(ADT GColumnsADT t (Col Expr)
a) -> Eval
(GGColumns 'Sum TColumns (Eval (ADTRep t (Reify Result))))
(Col Expr)
GColumnsADT t (Col Expr)
a)
(GGAggregate 'Sum (ADTRep t) (ADT t Aggregate)
AggregateADT t
f @(ADT t Aggregate))
data ADTRep :: K.Rel8able -> K.Context -> Exp (Type -> Type)
type instance Eval (ADTRep t context) = GRep t context
type GColumnsADT :: K.Rel8able -> K.HTable
type GColumnsADT t = G.GColumnsADT TColumns (GRep t (Reify Result))