on add7e77 help sign in
rel8/src/Rel8/Table/ADT.hs
173 lines 4.6 kB history raw
1{-# language AllowAmbiguousTypes #-}
2{-# language DataKinds #-}
3{-# language FlexibleContexts #-}
4{-# language FlexibleInstances #-}
5{-# language MultiParamTypeClasses #-}
6{-# language RankNTypes #-}
7{-# language ScopedTypeVariables #-}
8{-# language StandaloneKindSignatures #-}
9{-# language TypeApplications #-}
10{-# language TypeFamilyDependencies #-}
11{-# language UndecidableInstances #-}
12{-# language UndecidableSuperClasses #-}
14module Rel8.Table.ADT
15 ( ADT( ADT )
16 , ADTable
17 , BuildableADT
18 , BuildADT, buildADT
19 , ConstructableADT
20 , ConstructADT, constructADT
21 , DeconstructADT, deconstructADT
22 , NameADT, nameADT
23 , AggregateADT, aggregateADT
24 , ADTRep
25 )
26where
28-- base
29import Data.Kind ( Constraint, Type )
30import GHC.Generics ( Generic, from, to )
31import GHC.TypeLits ( Symbol )
32import Prelude
34-- rel8
35import Rel8.Aggregate ( Aggregate )
36import Rel8.Expr ( Expr )
37import Rel8.FCF ( Eval, Exp )
38import Rel8.Generic.Construction
39 ( GGBuildable
40 , GGBuild, ggbuild
41 , GGConstructable
42 , GGConstruct, ggconstruct
43 , GGDeconstruct, ggdeconstruct
44 , GGName, ggname
45 , GGAggregate, ggaggregate
46 )
47import Rel8.Generic.Record ( Record( Record ), unrecord )
48import Rel8.Generic.Rel8able
49 ( Rel8able
50 , GRep, GColumns, gfromColumns, gtoColumns
51 , GFromExprs, gfromResult, gtoResult
52 , TSerialize, deserialize, serialize
53 )
54import qualified Rel8.Generic.Table.ADT as G
55import qualified Rel8.Kind.Algebra as K
56import Rel8.Schema.HTable ( HTable )
57import qualified Rel8.Schema.Kind as K
58import Rel8.Schema.Name ( Name )
59import Rel8.Schema.Result ( Result )
60import Rel8.Table ( Table, TColumns )
63type ADT :: K.Rel8able -> K.Rel8able
64newtype ADT t context = ADT (GColumnsADT t context)
67instance ADTable t => Rel8able (ADT t) where
68 type GColumns (ADT t) = GColumnsADT t
69 type GFromExprs (ADT t) = t Result
71 gfromColumns _ = ADT
72 gtoColumns _ (ADT a) = a
74 gfromResult =
75 unrecord .
76 to .
77 G.gfromResultADT
78 @TSerialize
79 @TColumns
80 @(Eval (ADTRep t Expr))
81 @(Eval (ADTRep t Result))
82 (\(_ :: proxy x) -> deserialize @_ @x)
84 gtoResult =
85 G.gtoResultADT
86 @TSerialize
87 @TColumns
88 @(Eval (ADTRep t Expr))
89 @(Eval (ADTRep t Result))
90 (\(_ :: proxy x) -> serialize @_ @x) .
91 from .
92 Record
95type ADTable :: K.Rel8able -> Constraint
96class
97 ( Generic (Record (t Result))
98 , HTable (GColumnsADT t)
99 , G.GSerializeADT TSerialize TColumns (Eval (ADTRep t Expr)) (Eval (ADTRep t Result))
100 )
101 => ADTable t
102instance
103 ( Generic (Record (t Result))
104 , HTable (GColumnsADT t)
105 , G.GSerializeADT TSerialize TColumns (Eval (ADTRep t Expr)) (Eval (ADTRep t Result))
106 )
107 => ADTable t
110type BuildableADT :: K.Rel8able -> Symbol -> Constraint
111class GGBuildable 'K.Sum name (ADTRep t) => BuildableADT t name
112instance GGBuildable 'K.Sum name (ADTRep t) => BuildableADT t name
115type BuildADT :: K.Rel8able -> Symbol -> Type
116type BuildADT t name = GGBuild 'K.Sum name (ADTRep t) (ADT t Expr)
119buildADT :: forall t name. BuildableADT t name => BuildADT t name
120buildADT =
121 ggbuild @'K.Sum @name @(ADTRep t) @(ADT t Expr) ADT
124type ConstructableADT :: K.Rel8able -> Constraint
125class GGConstructable 'K.Sum (ADTRep t) => ConstructableADT t
126instance GGConstructable 'K.Sum (ADTRep t) => ConstructableADT t
129type ConstructADT :: K.Rel8able -> Type
130type ConstructADT t = forall r. GGConstruct 'K.Sum (ADTRep t) r
133constructADT :: forall t. ConstructableADT t => ConstructADT t -> ADT t Expr
134constructADT f =
135 ggconstruct @'K.Sum @(ADTRep t) @(ADT t Expr) ADT
136 (f @(ADT t Expr))
139type DeconstructADT :: K.Rel8able -> Type -> Type
140type DeconstructADT t r = GGDeconstruct 'K.Sum (ADTRep t) (ADT t Expr) r
143deconstructADT :: forall t r. (ConstructableADT t, Table Expr r)
144 => DeconstructADT t r
145deconstructADT =
146 ggdeconstruct @'K.Sum @(ADTRep t) @(ADT t Expr) @r (\(ADT a) -> a)
149type NameADT :: K.Rel8able -> Type
150type NameADT t = GGName 'K.Sum (ADTRep t) (ADT t Name)
153nameADT :: forall t. ConstructableADT t => NameADT t
154nameADT = ggname @'K.Sum @(ADTRep t) @(ADT t Name) ADT
157type AggregateADT :: K.Rel8able -> Type
158type AggregateADT t = forall r. GGAggregate 'K.Sum (ADTRep t) r
161aggregateADT :: forall t. ConstructableADT t
162 => AggregateADT t -> ADT t Expr -> ADT t Aggregate
163aggregateADT f =
164 ggaggregate @'K.Sum @(ADTRep t) @(ADT t Expr) @(ADT t Aggregate) ADT (\(ADT a) -> a)
165 (f @(ADT t Aggregate))
168data ADTRep :: K.Rel8able -> K.Context -> Exp (Type -> Type)
169type instance Eval (ADTRep t context) = GRep t context
172type GColumnsADT :: K.Rel8able -> K.HTable
173type GColumnsADT t = G.GColumnsADT TColumns (GRep t Expr)