git.iko.soy/rel8
on ae2ce41 help sign in
rel8/src/Rel8/Generic/Construction.hs
452 lines 17 kB history raw
1{-# language AllowAmbiguousTypes #-}
2{-# language ConstraintKinds #-}
3{-# language DataKinds #-}
4{-# language FlexibleContexts #-}
5{-# language FlexibleInstances #-}
6{-# language LambdaCase #-}
7{-# language MultiParamTypeClasses #-}
8{-# language NamedFieldPuns #-}
9{-# language ScopedTypeVariables #-}
10{-# language StandaloneKindSignatures #-}
11{-# language TypeApplications #-}
12{-# language TypeFamilies #-}
13{-# language UndecidableInstances #-}
14{-# language ViewPatterns #-}
16module Rel8.Generic.Construction
17 ( GGConstructable
18 , GGConstruct, ggconstruct
19 , GGDeconstruct, ggdeconstruct
20 , GGInsert, gginsert
21 , GGName, ggname
22 , GGAggregate, ggaggregate
23 , GGAggregate', ggaggregate'
24 )
25where
27-- base
28import Data.Bifunctor ( first )
29import Data.Kind ( Constraint, Type )
30import Data.List.NonEmpty ( NonEmpty( (:|) ) )
31import Data.Type.Equality ( (:~:)( Refl ) )
32import Prelude
34-- rel8
35import Rel8.Aggregate ( Col( Aggregation ), Aggregate )
36import Rel8.Expr ( Col( DB ), Expr )
37import Rel8.Expr.Aggregate ( groupByExpr )
38import Rel8.Expr.Eq ( (==.) )
39import Rel8.Expr.Null ( nullify, snull, unsafeUnnullify )
40import Rel8.Expr.Serialize ( litExpr )
41import Rel8.FCF ( Compose, Eval, Exp )
42import Rel8.Generic.Construction.ADT
43 ( GConstructableADT
44 , GBuildADT, gbuildADT, gunbuildADT
45 , GConstructADT, gconstructADT, gdeconstructADT
46 , CorepConstructors, GConstructors, gcindex, gctabulate
47 , CorepFields, gfindex, gftabulate, gftraverse
48 )
49import Rel8.Generic.Construction.Record
50 ( GConstructable, GConstruct, gconstruct, gdeconstruct
51 , Corep, gindex, gtabulate, gtraverse
52 )
53import Rel8.Generic.Table ( GGColumns )
54import Rel8.Kind.Algebra
55 ( SAlgebra( SProduct, SSum )
56 , KnownAlgebra, algebraSing
57 )
58import qualified Rel8.Kind.Algebra as K
59import Rel8.Kind.Necessity ( SNecessity( SOptional, SRequired ) )
60import Rel8.Schema.Context.Nullify ( runTag )
61import Rel8.Schema.HTable ( HTable )
62import Rel8.Schema.HTable.Identity ( HIdentity( HType ) )
63import Rel8.Schema.Insert ( Col( OptionalInsert, RequiredInsert ), Insert )
64import qualified Rel8.Schema.Kind as K
65import Rel8.Schema.Name ( Col( NameCol ), Name( Name ) )
66import Rel8.Schema.Null ( Nullity( Null, NotNull ) )
67import Rel8.Schema.Spec ( SSpec( SSpec, necessity, nullity, info ) )
68import Rel8.Schema.Reify ( Col( Reify ), Reify, hreify, hunreify )
69import Rel8.Schema.Result ( Result )
70import Rel8.Table
71 ( TTable, TColumns, TUnreify
72 , Table, fromColumns, toColumns, reify, unreify
73 )
74import Rel8.Table.Bool ( case_ )
75import Rel8.Type.Tag ( Tag )
77-- semigroupoids
78import Data.Functor.Apply ( Apply, MaybeApply( MaybeApply ), liftF2 )
81type GGConstructable :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Constraint
82type GGConstructable algebra rep =
83 ( KnownAlgebra algebra
84 , Eval (GGColumns algebra TColumns (Eval (rep (Reify Aggregate)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
85 , Eval (GGColumns algebra TColumns (Eval (rep (Reify Expr)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
86 , Eval (GGColumns algebra TColumns (Eval (rep (Reify Insert)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
87 , Eval (GGColumns algebra TColumns (Eval (rep (Reify Name)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
88 , HTable (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))))
89 , GGConstructable' algebra rep
90 )
93type GGConstructable' :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Constraint
94type family GGConstructable' algebra rep where
95 GGConstructable' 'K.Product rep =
96 ( Corep (Compose Aggregate TUnreify) (Eval (rep (Reify Expr)))
97 , Corep TUnreify (Eval (rep (Reify Aggregate)))
98 , Corep TUnreify (Eval (rep (Reify Expr)))
99 , Corep TUnreify (Eval (rep (Reify Insert)))
100 , Corep TUnreify (Eval (rep (Reify Name)))
101 , GConstructable (TTable (Reify Aggregate)) TColumns TUnreify (Col (Reify Aggregate)) (Eval (rep (Reify Aggregate)))
102 , GConstructable (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr)) (Eval (rep (Reify Expr)))
103 , GConstructable (TTable (Reify Insert)) TColumns TUnreify (Col (Reify Insert)) (Eval (rep (Reify Insert)))
104 , GConstructable (TTable (Reify Name)) TColumns TUnreify (Col (Reify Name)) (Eval (rep (Reify Name)))
105 )
106 GGConstructable' 'K.Sum rep =
107 ( CorepConstructors TUnreify (Eval (rep (Reify Expr)))
108 , CorepConstructors TUnreify (Eval (rep (Reify Insert)))
109 , CorepFields (Compose Aggregate TUnreify) (Eval (rep (Reify Expr)))
110 , CorepFields TUnreify (Eval (rep (Reify Aggregate)))
111 , CorepFields TUnreify (Eval (rep (Reify Expr)))
112 , CorepFields TUnreify (Eval (rep (Reify Name)))
113 , Functor (GConstructors TUnreify (Eval (rep (Reify Expr))))
114 , Functor (GConstructors TUnreify (Eval (rep (Reify Insert))))
115 , GConstructableADT (TTable (Reify Aggregate)) TColumns TUnreify (Col (Reify Aggregate)) (Eval (rep (Reify Aggregate)))
116 , GConstructableADT (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr)) (Eval (rep (Reify Expr)))
117 , GConstructableADT (TTable (Reify Insert)) TColumns TUnreify (Col (Reify Insert)) (Eval (rep (Reify Insert)))
118 , GConstructableADT (TTable (Reify Name)) TColumns TUnreify (Col (Reify Name)) (Eval (rep (Reify Name)))
119 )
122type GGConstruct :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
123type family GGConstruct algebra rep r where
124 GGConstruct 'K.Product rep r = GConstruct TUnreify (Eval (rep (Reify Expr))) r -> r
125 GGConstruct 'K.Sum rep r = GConstructADT TUnreify (Eval (rep (Reify Expr))) r r
128ggconstruct :: forall algebra rep a. GGConstructable algebra rep
129 => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr) -> a)
130 -> GGConstruct algebra rep a -> a
131ggconstruct gfromColumns f = case algebraSing @algebra of
132 SProduct ->
133 f $
134 gtabulate @TUnreify @(Eval (rep (Reify Expr))) @a $
135 gfromColumns .
136 hunreify .
137 gconstruct
138 @(TTable (Reify Expr))
139 @TColumns
140 @TUnreify
141 @(Col (Reify Expr))
142 @(Eval (rep (Reify Expr)))
143 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
144 SSum ->
145 gcindex @TUnreify @(Eval (rep (Reify Expr))) @a f $
146 fmap (gfromColumns . hunreify) $
147 gconstructADT
148 @(TTable (Reify Expr))
149 @TColumns
150 @TUnreify
151 @(Col (Reify Expr))
152 @(Eval (rep (Reify Expr)))
153 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
154 (\SSpec {info} -> Reify (DB (snull info)))
155 (\SSpec {nullity} -> case nullity of
156 Null -> id
157 NotNull -> \(Reify (DB a)) -> Reify (DB (nullify a)))
158 (HType . Reify . DB . litExpr)
161type GGDeconstruct :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type -> Type
162type family GGDeconstruct algebra rep a r where
163 GGDeconstruct 'K.Product rep a r =
164 GConstruct TUnreify (Eval (rep (Reify Expr))) r -> a -> r
165 GGDeconstruct 'K.Sum rep a r =
166 GConstructADT TUnreify (Eval (rep (Reify Expr))) r (a -> r)
169ggdeconstruct :: forall algebra rep a r. (GGConstructable algebra rep, Table Expr r)
170 => (a -> Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr))
171 -> GGDeconstruct algebra rep a r
172ggdeconstruct gtoColumns = case algebraSing @algebra of
173 SProduct -> \build ->
174 gindex @TUnreify @(Eval (rep (Reify Expr))) @r build .
175 gdeconstruct
176 @(TTable (Reify Expr))
177 @TColumns
178 @TUnreify
179 @(Col (Reify Expr))
180 @(Eval (rep (Reify Expr)))
181 (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns) .
182 hreify .
183 gtoColumns
184 SSum ->
185 gctabulate @TUnreify @(Eval (rep (Reify Expr))) @r @(a -> r) $ \constructors as ->
186 let
187 (HType (Reify (DB tag)), cases) =
188 gdeconstructADT
189 @(TTable (Reify Expr))
190 @TColumns
191 @TUnreify
192 @(Col (Reify Expr))
193 @(Eval (rep (Reify Expr)))
194 (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns)
195 (\SSpec {nullity} -> case nullity of
196 Null -> id
197 NotNull -> \(Reify (DB a)) -> Reify (DB (unsafeUnnullify a)))
198 constructors $
199 hreify $
200 gtoColumns as
201 in
202 case cases of
203 ((_, r) :| (map (first ((tag ==.) . litExpr)) -> cases')) ->
204 case_ cases' r
207type GGInsert :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
208type family GGInsert algebra rep r where
209 GGInsert 'K.Product rep r =
210 GConstruct TUnreify (Eval (rep (Reify Insert))) r -> r
211 GGInsert 'K.Sum rep r =
212 GConstructADT TUnreify (Eval (rep (Reify Insert))) r r
215gginsert :: forall algebra rep a. GGConstructable algebra rep
216 => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Insert) -> a)
217 -> GGInsert algebra rep a
218 -> a
219gginsert gfromColumns f = case algebraSing @algebra of
220 SProduct ->
221 f $
222 gtabulate @TUnreify @(Eval (rep (Reify Insert))) @a $
223 gfromColumns .
224 hunreify .
225 gconstruct
226 @(TTable (Reify Insert))
227 @TColumns
228 @TUnreify
229 @(Col (Reify Insert))
230 @(Eval (rep (Reify Insert)))
231 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
232 SSum ->
233 gcindex @TUnreify @(Eval (rep (Reify Insert))) @a f $
234 fmap (gfromColumns . hunreify) $
235 gconstructADT
236 @(TTable (Reify Insert))
237 @TColumns
238 @TUnreify
239 @(Col (Reify Insert))
240 @(Eval (rep (Reify Insert)))
241 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
242 (\SSpec {necessity, info} -> Reify $ case necessity of
243 SRequired -> RequiredInsert (snull info)
244 SOptional -> OptionalInsert (Just (snull info)))
245 (\SSpec {nullity} -> case nullity of
246 Null -> id
247 NotNull -> \case
248 Reify (RequiredInsert a) -> Reify (RequiredInsert (nullify a))
249 Reify (OptionalInsert a) -> Reify (OptionalInsert (nullify <$> a)))
250 (HType . Reify . RequiredInsert . litExpr)
253type GGName :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
254type family GGName algebra rep a where
255 GGName 'K.Product rep a = GConstruct TUnreify (Eval (rep (Reify Name))) a
256 GGName 'K.Sum rep a = Name Tag -> GBuildADT TUnreify (Eval (rep (Reify Name))) a
259ggname :: forall algebra rep a. GGConstructable algebra rep
260 => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Name) -> a)
261 -> GGName algebra rep a
262ggname gfromColumns = case algebraSing @algebra of
263 SProduct ->
264 gtabulate @TUnreify @(Eval (rep (Reify Name))) @a $
265 gfromColumns .
266 hunreify .
267 gconstruct
268 @(TTable (Reify Name))
269 @TColumns
270 @TUnreify
271 @(Col (Reify Name))
272 @(Eval (rep (Reify Name)))
273 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
274 SSum -> \tag ->
275 gftabulate @TUnreify @(Eval (rep (Reify Name))) @a $
276 gfromColumns .
277 hunreify .
278 gbuildADT
279 @(TTable (Reify Name))
280 @TColumns
281 @TUnreify
282 @(Col (Reify Name))
283 @(Eval (rep (Reify Name)))
284 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
285 (\_ _ (Reify (NameCol a)) -> Reify (NameCol a))
286 (HType ((\(Name a) -> Reify (NameCol a)) tag))
289type GGAggregate :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
290type family GGAggregate algebra rep r where
291 GGAggregate 'K.Product rep r =
292 GConstruct (Compose Aggregate TUnreify) (Eval (rep (Reify Expr))) r ->
293 GConstruct TUnreify (Eval (rep (Reify Expr))) r
294 GGAggregate 'K.Sum rep r =
295 GBuildADT (Compose Aggregate TUnreify) (Eval (rep (Reify Expr))) r ->
296 GBuildADT TUnreify (Eval (rep (Reify Expr))) r
299ggaggregate :: forall algebra rep a. GGConstructable algebra rep
300 => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr) -> a)
301 -> (a -> Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr))
302 -> GGAggregate algebra rep (Aggregate a) -> a -> Aggregate a
303ggaggregate gfromColumns gtoColumns agg es = case algebraSing @algebra of
304 SProduct -> flip f exprs $
305 fmap
306 ( gfromColumns
307 . hunreify
308 . gconstruct
309 @(TTable (Reify Expr))
310 @TColumns
311 @TUnreify
312 @(Col (Reify Expr))
313 @(Eval (rep (Reify Expr)))
314 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
315 ) .
316 liftF½ .
317 gtraverse @TUnreify @(Eval (rep (Reify Expr))) @_ @Aggregate (MaybeApply . Left)
318 where
319 f =
320 gindex @TUnreify @(Eval (rep (Reify Expr))) @(Aggregate a) .
321 agg .
322 gtabulate @(Compose Aggregate TUnreify) @(Eval (rep (Reify Expr))) @(Aggregate a)
323 exprs =
324 gdeconstruct
325 @(TTable (Reify Expr))
326 @TColumns
327 @TUnreify
328 @(Col (Reify Expr))
329 @(Eval (rep (Reify Expr)))
330 (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns) $
331 hreify $
332 gtoColumns es
333 SSum -> flip f exprs $
334 liftF1½
335 (\tag' ->
336 gfromColumns .
337 hunreify .
338 gbuildADT
339 @(TTable (Reify Expr))
340 @TColumns
341 @TUnreify
342 @(Col (Reify Expr))
343 @(Eval (rep (Reify Expr)))
344 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
345 (\tag'' SSpec {nullity} (Reify (DB a)) ->
346 Reify $ DB $ runTag nullity (tag ==. litExpr tag'') a)
347 (HType (Reify (DB tag'))))
348 (groupByExpr tag) .
349 gftraverse @TUnreify @(Eval (rep (Reify Expr))) @_ @Aggregate (MaybeApply . Left)
350 where
351 f =
352 gfindex @TUnreify @(Eval (rep (Reify Expr))) @(Aggregate a) .
353 agg .
354 gftabulate @(Compose Aggregate TUnreify) @(Eval (rep (Reify Expr))) @(Aggregate a)
355 (HType (Reify (DB tag)), exprs) =
356 gunbuildADT
357 @(TTable (Reify Expr))
358 @TColumns
359 @TUnreify
360 @(Col (Reify Expr))
361 @(Eval (rep (Reify Expr)))
362 (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns)
363 (\SSpec {nullity} -> case nullity of
364 Null -> id
365 NotNull -> \(Reify (DB a)) -> Reify (DB (unsafeUnnullify a))) $
366 hreify $
367 gtoColumns es
370type GGAggregate' :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
371type family GGAggregate' algebra rep r where
372 GGAggregate' 'K.Product rep r =
373 GConstruct TUnreify (Eval (rep (Reify Aggregate))) r ->
374 GConstruct TUnreify (Eval (rep (Reify Expr))) r
375 GGAggregate' 'K.Sum rep r =
376 GBuildADT TUnreify (Eval (rep (Reify Aggregate))) r ->
377 GBuildADT TUnreify (Eval (rep (Reify Expr))) r
380ggaggregate' :: forall algebra rep exprs agg. GGConstructable algebra rep
381 => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Aggregate) -> agg)
382 -> (exprs -> Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr))
383 -> GGAggregate' algebra rep agg -> exprs -> agg
384ggaggregate' gfromColumns gtoColumns agg es = case algebraSing @algebra of
385 SProduct -> flip f exprs $
386 gfromColumns .
387 hunreify .
388 gconstruct
389 @(TTable (Reify Aggregate))
390 @TColumns
391 @TUnreify
392 @(Col (Reify Aggregate))
393 @(Eval (rep (Reify Aggregate)))
394 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
395 where
396 f =
397 gindex @TUnreify @(Eval (rep (Reify Expr))) @agg .
398 agg .
399 gtabulate @TUnreify @(Eval (rep (Reify Aggregate))) @agg
400 exprs =
401 gdeconstruct
402 @(TTable (Reify Expr))
403 @TColumns
404 @TUnreify
405 @(Col (Reify Expr))
406 @(Eval (rep (Reify Expr)))
407 (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns) $
408 hreify $
409 gtoColumns es
410 SSum -> flip f exprs $
411 gfromColumns .
412 hunreify .
413 gbuildADT
414 @(TTable (Reify Aggregate))
415 @TColumns
416 @TUnreify
417 @(Col (Reify Aggregate))
418 @(Eval (rep (Reify Aggregate)))
419 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
420 (\tag' SSpec {nullity} (Reify (Aggregation a)) ->
421 Reify $ Aggregation $ runTag nullity (tag ==. litExpr tag') <$> a)
422 (HType (Reify (Aggregation (groupByExpr tag))))
423 where
424 f =
425 gfindex @TUnreify @(Eval (rep (Reify Expr))) @agg .
426 agg .
427 gftabulate @TUnreify @(Eval (rep (Reify Aggregate))) @agg
428 (HType (Reify (DB tag)), exprs) =
429 gunbuildADT
430 @(TTable (Reify Expr))
431 @TColumns
432 @TUnreify
433 @(Col (Reify Expr))
434 @(Eval (rep (Reify Expr)))
435 (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns)
436 (\SSpec {nullity} -> case nullity of
437 Null -> id
438 NotNull -> \(Reify (DB a)) -> Reify (DB (unsafeUnnullify a))) $
439 hreify $
440 gtoColumns es
443liftF½ :: MaybeApply Aggregate a -> Aggregate a
444liftF½ (MaybeApply ma) = case ma of
445 Left a -> a
446 Right a -> a <$ groupByExpr (litExpr False)
449liftF1½ :: Apply v => (a -> b -> c) -> v a -> MaybeApply v b -> v c
450liftF1½ f a (MaybeApply eb) = case eb of
451 Left b -> liftF2 f a b
452 Right b -> fmap (`f` b) a