git.iko.soy/rel8
on db40580 help sign in
rel8/src/Rel8/Generic/Construction.hs
528 lines 20 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 ( GGBuildable
18 , GGBuild, ggbuild
19 , GGInsert, gginsert
20 , GGConstructable
21 , GGConstruct, ggconstruct
22 , GGDeconstruct, ggdeconstruct
23 , GGName, ggname
24 , GGAggregate, ggaggregate
25 , GGAggregate', ggaggregate'
26 )
27where
29-- base
30import Data.Bifunctor ( first )
31import Data.Kind ( Constraint, Type )
32import Data.List.NonEmpty ( NonEmpty( (:|) ) )
33import Data.Type.Equality ( (:~:)( Refl ) )
34import GHC.TypeLits ( Symbol )
35import Prelude
37-- rel8
38import Rel8.Aggregate ( Col( A ), Aggregate )
39import Rel8.Expr ( Col( E ), Expr )
40import Rel8.Expr.Aggregate ( groupByExpr )
41import Rel8.Expr.Eq ( (==.) )
42import Rel8.Expr.Null ( nullify, snull, unsafeUnnullify )
43import Rel8.Expr.Serialize ( litExpr )
44import Rel8.FCF ( Compose, Eval, Exp )
45import Rel8.Generic.Construction.ADT
46 ( GConstructorADT, GMakeableADT, gmakeADT
47 , GConstructableADT
48 , GBuildADT, gbuildADT, gunbuildADT
49 , GConstructADT, gconstructADT, gdeconstructADT
50 , RepresentableConstructors, GConstructors, gcindex, gctabulate
51 , RepresentableFields, gfindex, gftabulate, gftraverse
52 )
53import Rel8.Generic.Construction.Record
54 ( GConstructor
55 , GConstructable, GConstruct, gconstruct, gdeconstruct
56 , Representable, gindex, gtabulate, gtraverse
57 )
58import Rel8.Generic.Table ( GGColumns )
59import Rel8.Kind.Algebra
60 ( SAlgebra( SProduct, SSum )
61 , KnownAlgebra, algebraSing
62 )
63import qualified Rel8.Kind.Algebra as K
64import Rel8.Schema.Context.Nullify ( runTag )
65import Rel8.Schema.HTable ( HTable )
66import Rel8.Schema.HTable.Identity ( HIdentity( HType ) )
67import Rel8.Schema.Insert ( Col( I ), Create(..), Insert )
68import qualified Rel8.Schema.Kind as K
69import Rel8.Schema.Name ( Col( N ), Name( Name ) )
70import Rel8.Schema.Null ( Nullity( Null, NotNull ) )
71import Rel8.Schema.Spec ( SSpec( SSpec, nullity, info ) )
72import Rel8.Schema.Reify ( Col( Reify ), Reify, hreify, hunreify )
73import Rel8.Schema.Result ( Result )
74import Rel8.Table
75 ( TTable, TColumns, TUnreify
76 , Table, fromColumns, toColumns, reify, unreify
77 )
78import Rel8.Table.Bool ( case_ )
79import Rel8.Type.Tag ( Tag )
81-- semigroupoids
82import Data.Functor.Apply ( Apply, MaybeApply( MaybeApply ), liftF2 )
85type GGBuildable :: K.Algebra -> Symbol -> (K.Context -> Exp (Type -> Type)) -> Constraint
86type GGBuildable algebra name rep =
87 ( KnownAlgebra algebra
88 , Eval (GGColumns algebra TColumns (Eval (rep (Reify Aggregate)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
89 , Eval (GGColumns algebra TColumns (Eval (rep (Reify Expr)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
90 , Eval (GGColumns algebra TColumns (Eval (rep (Reify Insert)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
91 , Eval (GGColumns algebra TColumns (Eval (rep (Reify Name)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
92 , HTable (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))))
93 , GGBuildable' algebra name rep
94 )
97type GGBuildable' :: K.Algebra -> Symbol -> (K.Context -> Exp (Type -> Type)) -> Constraint
98type family GGBuildable' algebra name rep where
99 GGBuildable' 'K.Product name rep =
100 ( name ~ GConstructor (Eval (rep (Reify Expr)))
101 , name ~ GConstructor (Eval (rep (Reify Insert)))
102 , Representable TUnreify (Eval (rep (Reify Expr)))
103 , Representable TUnreify (Eval (rep (Reify Insert)))
104 , GConstructable (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr)) (Eval (rep (Reify Expr)))
105 , GConstructable (TTable (Reify Insert)) TColumns TUnreify (Col (Reify Insert)) (Eval (rep (Reify Insert)))
106 )
107 GGBuildable' 'K.Sum name rep =
108 ( Representable TUnreify (GConstructorADT name (Eval (rep (Reify Expr))))
109 , Representable TUnreify (GConstructorADT name (Eval (rep (Reify Insert))))
110 , GMakeableADT (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr)) name (Eval (rep (Reify Expr)))
111 , GMakeableADT (TTable (Reify Insert)) TColumns TUnreify (Col (Reify Insert)) name (Eval (rep (Reify Insert)))
112 )
115type GGBuild :: K.Algebra -> Symbol -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
116type family GGBuild algebra name rep r where
117 GGBuild 'K.Product _name rep r =
118 GConstruct TUnreify (Eval (rep (Reify Expr))) r
119 GGBuild 'K.Sum name rep r =
120 GConstruct TUnreify (GConstructorADT name (Eval (rep (Reify Expr)))) r
123ggbuild :: forall algebra name rep a. GGBuildable algebra name rep
124 => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr) -> a)
125 -> GGBuild algebra name rep a
126ggbuild gfromColumns = case algebraSing @algebra of
127 SProduct ->
128 gtabulate @TUnreify @(Eval (rep (Reify Expr))) @a $
129 gfromColumns .
130 hunreify .
131 gconstruct
132 @(TTable (Reify Expr))
133 @TColumns
134 @TUnreify
135 @(Col (Reify Expr))
136 @(Eval (rep (Reify Expr)))
137 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
138 SSum ->
139 gtabulate @TUnreify @(GConstructorADT name (Eval (rep (Reify Expr)))) @a $
140 gfromColumns .
141 hunreify .
142 gmakeADT
143 @(TTable (Reify Expr))
144 @TColumns
145 @TUnreify
146 @(Col (Reify Expr))
147 @name
148 @(Eval (rep (Reify Expr)))
149 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
150 (\SSpec {info} -> Reify (E (snull info)))
151 (\SSpec {nullity} -> case nullity of
152 Null -> id
153 NotNull -> \(Reify (E a)) -> Reify (E (nullify a)))
154 (HType . Reify . E . litExpr)
157type GGInsert :: K.Algebra -> Symbol -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
158type family GGInsert algebra name rep r where
159 GGInsert 'K.Product _name rep r =
160 GConstruct TUnreify (Eval (rep (Reify Insert))) r
161 GGInsert 'K.Sum name rep r =
162 GConstruct TUnreify (GConstructorADT name (Eval (rep (Reify Insert)))) r
165gginsert :: forall algebra name rep a. GGBuildable algebra name rep
166 => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Insert) -> a)
167 -> GGInsert algebra name rep a
168gginsert gfromColumns = case algebraSing @algebra of
169 SProduct ->
170 gtabulate @TUnreify @(Eval (rep (Reify Insert))) @a $
171 gfromColumns .
172 hunreify .
173 gconstruct
174 @(TTable (Reify Insert))
175 @TColumns
176 @TUnreify
177 @(Col (Reify Insert))
178 @(Eval (rep (Reify Insert)))
179 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
180 SSum ->
181 gtabulate @TUnreify @(GConstructorADT name (Eval (rep (Reify Insert)))) @a $
182 gfromColumns .
183 hunreify .
184 gmakeADT
185 @(TTable (Reify Insert))
186 @TColumns
187 @TUnreify
188 @(Col (Reify Insert))
189 @name
190 @(Eval (rep (Reify Insert)))
191 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
192 (\SSpec {info} -> Reify $ I (Value (snull info)))
193 (\SSpec {nullity} -> case nullity of
194 Null -> id
195 NotNull -> \case
196 Reify (I Default) -> Reify (I Default)
197 Reify (I (Value a)) -> Reify (I (Value (nullify a))))
198 (HType . Reify . I . Value . litExpr)
201type GGConstructable :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Constraint
202type GGConstructable algebra rep =
203 ( KnownAlgebra algebra
204 , Eval (GGColumns algebra TColumns (Eval (rep (Reify Aggregate)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
205 , Eval (GGColumns algebra TColumns (Eval (rep (Reify Expr)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
206 , Eval (GGColumns algebra TColumns (Eval (rep (Reify Insert)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
207 , Eval (GGColumns algebra TColumns (Eval (rep (Reify Name)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
208 , HTable (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))))
209 , GGConstructable' algebra rep
210 )
213type GGConstructable' :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Constraint
214type family GGConstructable' algebra rep where
215 GGConstructable' 'K.Product rep =
216 ( Representable (Compose Aggregate TUnreify) (Eval (rep (Reify Expr)))
217 , Representable TUnreify (Eval (rep (Reify Aggregate)))
218 , Representable TUnreify (Eval (rep (Reify Expr)))
219 , Representable TUnreify (Eval (rep (Reify Insert)))
220 , Representable TUnreify (Eval (rep (Reify Name)))
221 , GConstructable (TTable (Reify Aggregate)) TColumns TUnreify (Col (Reify Aggregate)) (Eval (rep (Reify Aggregate)))
222 , GConstructable (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr)) (Eval (rep (Reify Expr)))
223 , GConstructable (TTable (Reify Insert)) TColumns TUnreify (Col (Reify Insert)) (Eval (rep (Reify Insert)))
224 , GConstructable (TTable (Reify Name)) TColumns TUnreify (Col (Reify Name)) (Eval (rep (Reify Name)))
225 )
226 GGConstructable' 'K.Sum rep =
227 ( RepresentableConstructors TUnreify (Eval (rep (Reify Expr)))
228 , RepresentableConstructors TUnreify (Eval (rep (Reify Insert)))
229 , RepresentableFields (Compose Aggregate TUnreify) (Eval (rep (Reify Expr)))
230 , RepresentableFields TUnreify (Eval (rep (Reify Aggregate)))
231 , RepresentableFields TUnreify (Eval (rep (Reify Expr)))
232 , RepresentableFields TUnreify (Eval (rep (Reify Name)))
233 , Functor (GConstructors TUnreify (Eval (rep (Reify Expr))))
234 , Functor (GConstructors TUnreify (Eval (rep (Reify Insert))))
235 , GConstructableADT (TTable (Reify Aggregate)) TColumns TUnreify (Col (Reify Aggregate)) (Eval (rep (Reify Aggregate)))
236 , GConstructableADT (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr)) (Eval (rep (Reify Expr)))
237 , GConstructableADT (TTable (Reify Insert)) TColumns TUnreify (Col (Reify Insert)) (Eval (rep (Reify Insert)))
238 , GConstructableADT (TTable (Reify Name)) TColumns TUnreify (Col (Reify Name)) (Eval (rep (Reify Name)))
239 )
242type GGConstruct :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
243type family GGConstruct algebra rep r where
244 GGConstruct 'K.Product rep r =
245 GConstruct TUnreify (Eval (rep (Reify Expr))) r -> r
246 GGConstruct 'K.Sum rep r =
247 GConstructADT TUnreify (Eval (rep (Reify Expr))) r r
250ggconstruct :: forall algebra rep a. GGConstructable algebra rep
251 => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr) -> a)
252 -> GGConstruct algebra rep a -> a
253ggconstruct gfromColumns f = case algebraSing @algebra of
254 SProduct ->
255 f $
256 gtabulate @TUnreify @(Eval (rep (Reify Expr))) @a $
257 gfromColumns .
258 hunreify .
259 gconstruct
260 @(TTable (Reify Expr))
261 @TColumns
262 @TUnreify
263 @(Col (Reify Expr))
264 @(Eval (rep (Reify Expr)))
265 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
266 SSum ->
267 gcindex @TUnreify @(Eval (rep (Reify Expr))) @a f $
268 fmap (gfromColumns . hunreify) $
269 gconstructADT
270 @(TTable (Reify Expr))
271 @TColumns
272 @TUnreify
273 @(Col (Reify Expr))
274 @(Eval (rep (Reify Expr)))
275 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
276 (\SSpec {info} -> Reify (E (snull info)))
277 (\SSpec {nullity} -> case nullity of
278 Null -> id
279 NotNull -> \(Reify (E a)) -> Reify (E (nullify a)))
280 (HType . Reify . E . litExpr)
283type GGDeconstruct :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type -> Type
284type family GGDeconstruct algebra rep a r where
285 GGDeconstruct 'K.Product rep a r =
286 GConstruct TUnreify (Eval (rep (Reify Expr))) r -> a -> r
287 GGDeconstruct 'K.Sum rep a r =
288 GConstructADT TUnreify (Eval (rep (Reify Expr))) r (a -> r)
291ggdeconstruct :: forall algebra rep a r. (GGConstructable algebra rep, Table Expr r)
292 => (a -> Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr))
293 -> GGDeconstruct algebra rep a r
294ggdeconstruct gtoColumns = case algebraSing @algebra of
295 SProduct -> \build ->
296 gindex @TUnreify @(Eval (rep (Reify Expr))) @r build .
297 gdeconstruct
298 @(TTable (Reify Expr))
299 @TColumns
300 @TUnreify
301 @(Col (Reify Expr))
302 @(Eval (rep (Reify Expr)))
303 (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns) .
304 hreify .
305 gtoColumns
306 SSum ->
307 gctabulate @TUnreify @(Eval (rep (Reify Expr))) @r @(a -> r) $ \constructors as ->
308 let
309 (HType (Reify (E tag)), cases) =
310 gdeconstructADT
311 @(TTable (Reify Expr))
312 @TColumns
313 @TUnreify
314 @(Col (Reify Expr))
315 @(Eval (rep (Reify Expr)))
316 (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns)
317 (\SSpec {nullity} -> case nullity of
318 Null -> id
319 NotNull -> \(Reify (E a)) -> Reify (E (unsafeUnnullify a)))
320 constructors $
321 hreify $
322 gtoColumns as
323 in
324 case cases of
325 ((_, r) :| (map (first ((tag ==.) . litExpr)) -> cases')) ->
326 case_ cases' r
329type GGName :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
330type family GGName algebra rep a where
331 GGName 'K.Product rep a = GConstruct TUnreify (Eval (rep (Reify Name))) a
332 GGName 'K.Sum rep a = Name Tag -> GBuildADT TUnreify (Eval (rep (Reify Name))) a
335ggname :: forall algebra rep a. GGConstructable algebra rep
336 => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Name) -> a)
337 -> GGName algebra rep a
338ggname gfromColumns = case algebraSing @algebra of
339 SProduct ->
340 gtabulate @TUnreify @(Eval (rep (Reify Name))) @a $
341 gfromColumns .
342 hunreify .
343 gconstruct
344 @(TTable (Reify Name))
345 @TColumns
346 @TUnreify
347 @(Col (Reify Name))
348 @(Eval (rep (Reify Name)))
349 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
350 SSum -> \tag ->
351 gftabulate @TUnreify @(Eval (rep (Reify Name))) @a $
352 gfromColumns .
353 hunreify .
354 gbuildADT
355 @(TTable (Reify Name))
356 @TColumns
357 @TUnreify
358 @(Col (Reify Name))
359 @(Eval (rep (Reify Name)))
360 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
361 (\_ _ (Reify (N (Name a))) -> Reify (N (Name a)))
362 (HType (Reify (N tag)))
365type GGAggregate :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
366type family GGAggregate algebra rep r where
367 GGAggregate 'K.Product rep r =
368 GConstruct (Compose Aggregate TUnreify) (Eval (rep (Reify Expr))) r ->
369 GConstruct TUnreify (Eval (rep (Reify Expr))) r
370 GGAggregate 'K.Sum rep r =
371 GBuildADT (Compose Aggregate TUnreify) (Eval (rep (Reify Expr))) r ->
372 GBuildADT TUnreify (Eval (rep (Reify Expr))) r
375ggaggregate :: forall algebra rep a. GGConstructable algebra rep
376 => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr) -> a)
377 -> (a -> Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr))
378 -> GGAggregate algebra rep (Aggregate a) -> a -> Aggregate a
379ggaggregate gfromColumns gtoColumns agg es = case algebraSing @algebra of
380 SProduct -> flip f exprs $
381 fmap
382 ( gfromColumns
383 . hunreify
384 . gconstruct
385 @(TTable (Reify Expr))
386 @TColumns
387 @TUnreify
388 @(Col (Reify Expr))
389 @(Eval (rep (Reify Expr)))
390 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
391 ) .
392 liftF½ .
393 gtraverse @TUnreify @(Eval (rep (Reify Expr))) @_ @Aggregate (MaybeApply . Left)
394 where
395 f =
396 gindex @TUnreify @(Eval (rep (Reify Expr))) @(Aggregate a) .
397 agg .
398 gtabulate @(Compose Aggregate TUnreify) @(Eval (rep (Reify Expr))) @(Aggregate a)
399 exprs =
400 gdeconstruct
401 @(TTable (Reify Expr))
402 @TColumns
403 @TUnreify
404 @(Col (Reify Expr))
405 @(Eval (rep (Reify Expr)))
406 (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns) $
407 hreify $
408 gtoColumns es
409 SSum -> flip f exprs $
410 liftF1½
411 (\tag' ->
412 gfromColumns .
413 hunreify .
414 gbuildADT
415 @(TTable (Reify Expr))
416 @TColumns
417 @TUnreify
418 @(Col (Reify Expr))
419 @(Eval (rep (Reify Expr)))
420 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
421 (\tag'' SSpec {nullity} (Reify (E a)) ->
422 Reify $ E $ runTag nullity (tag ==. litExpr tag'') a)
423 (HType (Reify (E tag'))))
424 (groupByExpr tag) .
425 gftraverse @TUnreify @(Eval (rep (Reify Expr))) @_ @Aggregate (MaybeApply . Left)
426 where
427 f =
428 gfindex @TUnreify @(Eval (rep (Reify Expr))) @(Aggregate a) .
429 agg .
430 gftabulate @(Compose Aggregate TUnreify) @(Eval (rep (Reify Expr))) @(Aggregate a)
431 (HType (Reify (E tag)), exprs) =
432 gunbuildADT
433 @(TTable (Reify Expr))
434 @TColumns
435 @TUnreify
436 @(Col (Reify Expr))
437 @(Eval (rep (Reify Expr)))
438 (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns)
439 (\SSpec {nullity} -> case nullity of
440 Null -> id
441 NotNull -> \(Reify (E a)) -> Reify (E (unsafeUnnullify a))) $
442 hreify $
443 gtoColumns es
446type GGAggregate' :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
447type family GGAggregate' algebra rep r where
448 GGAggregate' 'K.Product rep r =
449 GConstruct TUnreify (Eval (rep (Reify Aggregate))) r ->
450 GConstruct TUnreify (Eval (rep (Reify Expr))) r
451 GGAggregate' 'K.Sum rep r =
452 GBuildADT TUnreify (Eval (rep (Reify Aggregate))) r ->
453 GBuildADT TUnreify (Eval (rep (Reify Expr))) r
456ggaggregate' :: forall algebra rep exprs agg. GGConstructable algebra rep
457 => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Aggregate) -> agg)
458 -> (exprs -> Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr))
459 -> GGAggregate' algebra rep agg -> exprs -> agg
460ggaggregate' gfromColumns gtoColumns agg es = case algebraSing @algebra of
461 SProduct -> flip f exprs $
462 gfromColumns .
463 hunreify .
464 gconstruct
465 @(TTable (Reify Aggregate))
466 @TColumns
467 @TUnreify
468 @(Col (Reify Aggregate))
469 @(Eval (rep (Reify Aggregate)))
470 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
471 where
472 f =
473 gindex @TUnreify @(Eval (rep (Reify Expr))) @agg .
474 agg .
475 gtabulate @TUnreify @(Eval (rep (Reify Aggregate))) @agg
476 exprs =
477 gdeconstruct
478 @(TTable (Reify Expr))
479 @TColumns
480 @TUnreify
481 @(Col (Reify Expr))
482 @(Eval (rep (Reify Expr)))
483 (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns) $
484 hreify $
485 gtoColumns es
486 SSum -> flip f exprs $
487 gfromColumns .
488 hunreify .
489 gbuildADT
490 @(TTable (Reify Aggregate))
491 @TColumns
492 @TUnreify
493 @(Col (Reify Aggregate))
494 @(Eval (rep (Reify Aggregate)))
495 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
496 (\tag' SSpec {nullity} (Reify (A a)) ->
497 Reify $ A $ runTag nullity (tag ==. litExpr tag') <$> a)
498 (HType (Reify (A (groupByExpr tag))))
499 where
500 f =
501 gfindex @TUnreify @(Eval (rep (Reify Expr))) @agg .
502 agg .
503 gftabulate @TUnreify @(Eval (rep (Reify Aggregate))) @agg
504 (HType (Reify (E tag)), exprs) =
505 gunbuildADT
506 @(TTable (Reify Expr))
507 @TColumns
508 @TUnreify
509 @(Col (Reify Expr))
510 @(Eval (rep (Reify Expr)))
511 (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns)
512 (\SSpec {nullity} -> case nullity of
513 Null -> id
514 NotNull -> \(Reify (E a)) -> Reify (E (unsafeUnnullify a))) $
515 hreify $
516 gtoColumns es
519liftF½ :: MaybeApply Aggregate a -> Aggregate a
520liftF½ (MaybeApply ma) = case ma of
521 Left a -> a
522 Right a -> a <$ groupByExpr (litExpr False)
525liftF1½ :: Apply v => (a -> b -> c) -> v a -> MaybeApply v b -> v c
526liftF1½ f a (MaybeApply eb) = case eb of
527 Left b -> liftF2 f a b
528 Right b -> fmap (`f` b) a