on 97d89cf help sign in
rel8/src/Rel8/Generic/Construction.hs
352 lines 11 kB history raw
1{-# language AllowAmbiguousTypes #-}
2{-# language ConstraintKinds #-}
3{-# language DataKinds #-}
4{-# language FlexibleContexts #-}
5{-# language NamedFieldPuns #-}
6{-# language ScopedTypeVariables #-}
7{-# language StandaloneKindSignatures #-}
8{-# language TypeApplications #-}
9{-# language TypeFamilies #-}
10{-# language UndecidableInstances #-}
11{-# language ViewPatterns #-}
13module Rel8.Generic.Construction
14 ( GGBuildable
15 , GGBuild, ggbuild
16 , GGConstructable
17 , GGConstruct, ggconstruct
18 , GGDeconstruct, ggdeconstruct
19 , GGName, ggname
20 , GGAggregate, ggaggregate
21 )
22where
24-- base
25import Data.Bifunctor ( first )
26import Data.Kind ( Constraint, Type )
27import Data.List.NonEmpty ( NonEmpty( (:|) ) )
28import GHC.TypeLits ( Symbol )
29import Prelude
31-- rel8
32import Rel8.Aggregate ( Aggregate( A, Aggregate ) )
33import Rel8.Expr ( Expr( E ) )
34import Rel8.Expr.Aggregate ( groupByExpr )
35import Rel8.Expr.Eq ( (==.) )
36import Rel8.Expr.Null ( nullify, snull, unsafeUnnullify )
37import Rel8.Expr.Serialize ( litExpr )
38import Rel8.FCF ( Eval, Exp, Id )
39import Rel8.Generic.Construction.ADT
40 ( GConstructorADT, GMakeableADT, gmakeADT
41 , GConstructableADT
42 , GBuildADT, gbuildADT, gunbuildADT
43 , GConstructADT, gconstructADT, gdeconstructADT
44 , RepresentableConstructors, GConstructors, gcindex, gctabulate
45 , RepresentableFields, gfindex, gftabulate
46 )
47import Rel8.Generic.Construction.Record
48 ( GConstructor
49 , GConstructable, GConstruct, gconstruct, gdeconstruct
50 , Representable, gindex, gtabulate
51 )
52import Rel8.Generic.Table ( GGColumns )
53import Rel8.Kind.Algebra
54 ( SAlgebra( SProduct, SSum )
55 , KnownAlgebra, algebraSing
56 )
57import qualified Rel8.Kind.Algebra as K
58import Rel8.Schema.Context.Nullify ( sguard, snullify )
59import Rel8.Schema.HTable ( HTable )
60import Rel8.Schema.HTable.Identity ( HIdentity( HType ) )
61import qualified Rel8.Schema.Kind as K
62import Rel8.Schema.Name ( Name( N, Name ) )
63import Rel8.Schema.Null ( Nullity( Null, NotNull ) )
64import Rel8.Schema.Spec ( SSpec( SSpec, nullity, info ) )
65import Rel8.Table
66 ( TTable, TColumns
67 , Table, fromColumns, toColumns
68 )
69import Rel8.Table.Bool ( case_ )
70import Rel8.Type.Tag ( Tag )
73type GGBuildable :: K.Algebra -> Symbol -> (K.Context -> Exp (Type -> Type)) -> Constraint
74type GGBuildable algebra name rep =
75 ( KnownAlgebra algebra
76 , Eval (GGColumns algebra TColumns (Eval (rep Aggregate))) ~ Eval (GGColumns algebra TColumns (Eval (rep Expr)))
77 , Eval (GGColumns algebra TColumns (Eval (rep Expr))) ~ Eval (GGColumns algebra TColumns (Eval (rep Expr)))
78 , Eval (GGColumns algebra TColumns (Eval (rep Name))) ~ Eval (GGColumns algebra TColumns (Eval (rep Expr)))
79 , HTable (Eval (GGColumns algebra TColumns (Eval (rep Expr))))
80 , GGBuildable' algebra name rep
81 )
84type GGBuildable' :: K.Algebra -> Symbol -> (K.Context -> Exp (Type -> Type)) -> Constraint
85type family GGBuildable' algebra name rep where
86 GGBuildable' 'K.Product name rep =
87 ( name ~ GConstructor (Eval (rep Expr))
88 , Representable Id (Eval (rep Expr))
89 , GConstructable (TTable Expr) TColumns Id Expr (Eval (rep Expr))
90 )
91 GGBuildable' 'K.Sum name rep =
92 ( Representable Id (GConstructorADT name (Eval (rep Expr)))
93 , GMakeableADT (TTable Expr) TColumns Id Expr name (Eval (rep Expr))
94 )
97type GGBuild :: K.Algebra -> Symbol -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
98type family GGBuild algebra name rep r where
99 GGBuild 'K.Product _name rep r =
100 GConstruct Id (Eval (rep Expr)) r
101 GGBuild 'K.Sum name rep r =
102 GConstruct Id (GConstructorADT name (Eval (rep Expr))) r
105ggbuild :: forall algebra name rep a. GGBuildable algebra name rep
106 => (Eval (GGColumns algebra TColumns (Eval (rep Expr))) Expr -> a)
107 -> GGBuild algebra name rep a
108ggbuild gfromColumns = case algebraSing @algebra of
109 SProduct ->
110 gtabulate @Id @(Eval (rep Expr)) @a $
111 gfromColumns .
112 gconstruct
113 @(TTable Expr)
114 @TColumns
115 @Id
116 @Expr
117 @(Eval (rep Expr))
118 (const toColumns)
119 SSum ->
120 gtabulate @Id @(GConstructorADT name (Eval (rep Expr))) @a $
121 gfromColumns .
122 gmakeADT
123 @(TTable Expr)
124 @TColumns
125 @Id
126 @Expr
127 @name
128 @(Eval (rep Expr))
129 (const toColumns)
130 (\SSpec {info} -> E (snull info))
131 (\SSpec {nullity} -> case nullity of
132 Null -> id
133 NotNull -> \(E a) -> E (nullify a))
134 (HType . E . litExpr)
137type GGConstructable :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Constraint
138type GGConstructable algebra rep =
139 ( KnownAlgebra algebra
140 , Eval (GGColumns algebra TColumns (Eval (rep Aggregate))) ~ Eval (GGColumns algebra TColumns (Eval (rep Expr)))
141 , Eval (GGColumns algebra TColumns (Eval (rep Expr))) ~ Eval (GGColumns algebra TColumns (Eval (rep Expr)))
142 , Eval (GGColumns algebra TColumns (Eval (rep Name))) ~ Eval (GGColumns algebra TColumns (Eval (rep Expr)))
143 , HTable (Eval (GGColumns algebra TColumns (Eval (rep Expr))))
144 , GGConstructable' algebra rep
145 )
148type GGConstructable' :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Constraint
149type family GGConstructable' algebra rep where
150 GGConstructable' 'K.Product rep =
151 ( Representable Id (Eval (rep Aggregate))
152 , Representable Id (Eval (rep Expr))
153 , Representable Id (Eval (rep Name))
154 , GConstructable (TTable Aggregate) TColumns Id Aggregate (Eval (rep Aggregate))
155 , GConstructable (TTable Expr) TColumns Id Expr (Eval (rep Expr))
156 , GConstructable (TTable Name) TColumns Id Name (Eval (rep Name))
157 )
158 GGConstructable' 'K.Sum rep =
159 ( RepresentableConstructors Id (Eval (rep Expr))
160 , RepresentableFields Id (Eval (rep Aggregate))
161 , RepresentableFields Id (Eval (rep Expr))
162 , RepresentableFields Id (Eval (rep Name))
163 , Functor (GConstructors Id (Eval (rep Expr)))
164 , GConstructableADT (TTable Aggregate) TColumns Id Aggregate (Eval (rep Aggregate))
165 , GConstructableADT (TTable Expr) TColumns Id Expr (Eval (rep Expr))
166 , GConstructableADT (TTable Name) TColumns Id Name (Eval (rep Name))
167 )
170type GGConstruct :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
171type family GGConstruct algebra rep r where
172 GGConstruct 'K.Product rep r = GConstruct Id (Eval (rep Expr)) r -> r
173 GGConstruct 'K.Sum rep r = GConstructADT Id (Eval (rep Expr)) r r
176ggconstruct :: forall algebra rep a. GGConstructable algebra rep
177 => (Eval (GGColumns algebra TColumns (Eval (rep Expr))) Expr -> a)
178 -> GGConstruct algebra rep a -> a
179ggconstruct gfromColumns f = case algebraSing @algebra of
180 SProduct ->
181 f $
182 gtabulate @Id @(Eval (rep Expr)) @a $
183 gfromColumns .
184 gconstruct
185 @(TTable Expr)
186 @TColumns
187 @Id
188 @Expr
189 @(Eval (rep Expr))
190 (const toColumns)
191 SSum ->
192 gcindex @Id @(Eval (rep Expr)) @a f $
193 fmap gfromColumns $
194 gconstructADT
195 @(TTable Expr)
196 @TColumns
197 @Id
198 @Expr
199 @(Eval (rep Expr))
200 (const toColumns)
201 (\SSpec {info} -> E (snull info))
202 (\SSpec {nullity} -> case nullity of
203 Null -> id
204 NotNull -> \(E a) -> E (nullify a))
205 (HType . E . litExpr)
208type GGDeconstruct :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type -> Type
209type family GGDeconstruct algebra rep a r where
210 GGDeconstruct 'K.Product rep a r =
211 GConstruct Id (Eval (rep Expr)) r -> a -> r
212 GGDeconstruct 'K.Sum rep a r =
213 GConstructADT Id (Eval (rep Expr)) r (a -> r)
216ggdeconstruct :: forall algebra rep a r. (GGConstructable algebra rep, Table Expr r)
217 => (a -> Eval (GGColumns algebra TColumns (Eval (rep Expr))) Expr)
218 -> GGDeconstruct algebra rep a r
219ggdeconstruct gtoColumns = case algebraSing @algebra of
220 SProduct -> \build ->
221 gindex @Id @(Eval (rep Expr)) @r build .
222 gdeconstruct
223 @(TTable Expr)
224 @TColumns
225 @Id
226 @Expr
227 @(Eval (rep Expr))
228 (const fromColumns) .
229 gtoColumns
230 SSum ->
231 gctabulate @Id @(Eval (rep Expr)) @r @(a -> r) $ \constructors as ->
232 let
233 (HType (E tag), cases) =
234 gdeconstructADT
235 @(TTable Expr)
236 @TColumns
237 @Id
238 @Expr
239 @(Eval (rep Expr))
240 (const fromColumns)
241 (\SSpec {nullity} -> case nullity of
242 Null -> id
243 NotNull -> \(E a) -> E (unsafeUnnullify a))
244 constructors $
245 gtoColumns as
246 in
247 case cases of
248 ((_, r) :| (map (first ((tag ==.) . litExpr)) -> cases')) ->
249 case_ cases' r
252type GGName :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
253type family GGName algebra rep a where
254 GGName 'K.Product rep a = GConstruct Id (Eval (rep Name)) a
255 GGName 'K.Sum rep a = Name Tag -> GBuildADT Id (Eval (rep Name)) a
258ggname :: forall algebra rep a. GGConstructable algebra rep
259 => (Eval (GGColumns algebra TColumns (Eval (rep Expr))) Name -> a)
260 -> GGName algebra rep a
261ggname gfromColumns = case algebraSing @algebra of
262 SProduct ->
263 gtabulate @Id @(Eval (rep Name)) @a $
264 gfromColumns .
265 gconstruct
266 @(TTable Name)
267 @TColumns
268 @Id
269 @Name
270 @(Eval (rep Name))
271 (const toColumns)
272 SSum -> \tag ->
273 gftabulate @Id @(Eval (rep Name)) @a $
274 gfromColumns .
275 gbuildADT
276 @(TTable Name)
277 @TColumns
278 @Id
279 @Name
280 @(Eval (rep Name))
281 (const toColumns)
282 (\_ _ (N (Name a)) -> N (Name a))
283 (HType (N tag))
286type GGAggregate :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
287type family GGAggregate algebra rep r where
288 GGAggregate 'K.Product rep r =
289 GConstruct Id (Eval (rep Aggregate)) r ->
290 GConstruct Id (Eval (rep Expr)) r
291 GGAggregate 'K.Sum rep r =
292 GBuildADT Id (Eval (rep Aggregate)) r ->
293 GBuildADT Id (Eval (rep Expr)) r
296ggaggregate :: forall algebra rep exprs agg. GGConstructable algebra rep
297 => (Eval (GGColumns algebra TColumns (Eval (rep Expr))) Aggregate -> agg)
298 -> (exprs -> Eval (GGColumns algebra TColumns (Eval (rep Expr))) Expr)
299 -> GGAggregate algebra rep agg -> exprs -> agg
300ggaggregate gfromColumns gtoColumns agg es = case algebraSing @algebra of
301 SProduct -> flip f exprs $
302 gfromColumns .
303 gconstruct
304 @(TTable Aggregate)
305 @TColumns
306 @Id
307 @Aggregate
308 @(Eval (rep Aggregate))
309 (const toColumns)
310 where
311 f =
312 gindex @Id @(Eval (rep Expr)) @agg .
313 agg .
314 gtabulate @Id @(Eval (rep Aggregate)) @agg
315 exprs =
316 gdeconstruct
317 @(TTable Expr)
318 @TColumns
319 @Id
320 @Expr
321 @(Eval (rep Expr))
322 (const fromColumns) $
323 gtoColumns es
324 SSum -> flip f exprs $
325 gfromColumns .
326 gbuildADT
327 @(TTable Aggregate)
328 @TColumns
329 @Id
330 @Aggregate
331 @(Eval (rep Aggregate))
332 (const toColumns)
333 (\tag' SSpec {nullity} (A (Aggregate a)) ->
334 A $ Aggregate $ sguard (tag ==. litExpr tag') . snullify nullity <$> a)
335 (HType (A (groupByExpr tag)))
336 where
337 f =
338 gfindex @Id @(Eval (rep Expr)) @agg .
339 agg .
340 gftabulate @Id @(Eval (rep Aggregate)) @agg
341 (HType (E tag), exprs) =
342 gunbuildADT
343 @(TTable Expr)
344 @TColumns
345 @Id
346 @Expr
347 @(Eval (rep Expr))
348 (const fromColumns)
349 (\SSpec {nullity} -> case nullity of
350 Null -> id
351 NotNull -> \(E a) -> E (unsafeUnnullify a)) $
352 gtoColumns es