git.iko.soy/rel8
on 760dcd8 help sign in
rel8/src/Rel8/Generic/Construction.hs
371 lines 14 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 , GGConstructable
20 , GGConstruct, ggconstruct
21 , GGDeconstruct, ggdeconstruct
22 , GGName, ggname
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 GHC.TypeLits ( Symbol )
33import Prelude
35-- rel8
36import Rel8.Aggregate ( Col( A ), Aggregate( Aggregate ) )
37import Rel8.Expr ( Col( E ), Expr )
38import Rel8.Expr.Aggregate ( groupByExpr )
39import Rel8.Expr.Eq ( (==.) )
40import Rel8.Expr.Null ( nullify, snull, unsafeUnnullify )
41import Rel8.Expr.Serialize ( litExpr )
42import Rel8.FCF ( Eval, Exp )
43import Rel8.Generic.Construction.ADT
44 ( GConstructorADT, GMakeableADT, gmakeADT
45 , GConstructableADT
46 , GBuildADT, gbuildADT, gunbuildADT
47 , GConstructADT, gconstructADT, gdeconstructADT
48 , RepresentableConstructors, GConstructors, gcindex, gctabulate
49 , RepresentableFields, gfindex, gftabulate
50 )
51import Rel8.Generic.Construction.Record
52 ( GConstructor
53 , GConstructable, GConstruct, gconstruct, gdeconstruct
54 , Representable, gindex, gtabulate
55 )
56import Rel8.Generic.Table ( GGColumns )
57import Rel8.Kind.Algebra
58 ( SAlgebra( SProduct, SSum )
59 , KnownAlgebra, algebraSing
60 )
61import qualified Rel8.Kind.Algebra as K
62import Rel8.Schema.Context.Nullify ( runTag )
63import Rel8.Schema.HTable ( HTable )
64import Rel8.Schema.HTable.Identity ( HIdentity( HType ) )
65import qualified Rel8.Schema.Kind as K
66import Rel8.Schema.Name ( Col( N ), Name( Name ) )
67import Rel8.Schema.Null ( Nullity( Null, NotNull ) )
68import Rel8.Schema.Spec ( SSpec( SSpec, nullity, info ) )
69import Rel8.Schema.Reify ( Col( Reify ), Reify, hreify, hunreify )
70import Rel8.Schema.Result ( Result )
71import Rel8.Table
72 ( TTable, TColumns, TUnreify
73 , Table, fromColumns, toColumns, reify, unreify
74 )
75import Rel8.Table.Bool ( case_ )
76import Rel8.Type.Tag ( Tag )
79type GGBuildable :: K.Algebra -> Symbol -> (K.Context -> Exp (Type -> Type)) -> Constraint
80type GGBuildable algebra name rep =
81 ( KnownAlgebra algebra
82 , Eval (GGColumns algebra TColumns (Eval (rep (Reify Aggregate)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
83 , Eval (GGColumns algebra TColumns (Eval (rep (Reify Expr)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
84 , Eval (GGColumns algebra TColumns (Eval (rep (Reify Name)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
85 , HTable (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))))
86 , GGBuildable' algebra name rep
87 )
90type GGBuildable' :: K.Algebra -> Symbol -> (K.Context -> Exp (Type -> Type)) -> Constraint
91type family GGBuildable' algebra name rep where
92 GGBuildable' 'K.Product name rep =
93 ( name ~ GConstructor (Eval (rep (Reify Expr)))
94 , Representable TUnreify (Eval (rep (Reify Expr)))
95 , GConstructable (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr)) (Eval (rep (Reify Expr)))
96 )
97 GGBuildable' 'K.Sum name rep =
98 ( Representable TUnreify (GConstructorADT name (Eval (rep (Reify Expr))))
99 , GMakeableADT (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr)) name (Eval (rep (Reify Expr)))
100 )
103type GGBuild :: K.Algebra -> Symbol -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
104type family GGBuild algebra name rep r where
105 GGBuild 'K.Product _name rep r =
106 GConstruct TUnreify (Eval (rep (Reify Expr))) r
107 GGBuild 'K.Sum name rep r =
108 GConstruct TUnreify (GConstructorADT name (Eval (rep (Reify Expr)))) r
111ggbuild :: forall algebra name rep a. GGBuildable algebra name rep
112 => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr) -> a)
113 -> GGBuild algebra name rep a
114ggbuild gfromColumns = case algebraSing @algebra of
115 SProduct ->
116 gtabulate @TUnreify @(Eval (rep (Reify Expr))) @a $
117 gfromColumns .
118 hunreify .
119 gconstruct
120 @(TTable (Reify Expr))
121 @TColumns
122 @TUnreify
123 @(Col (Reify Expr))
124 @(Eval (rep (Reify Expr)))
125 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
126 SSum ->
127 gtabulate @TUnreify @(GConstructorADT name (Eval (rep (Reify Expr)))) @a $
128 gfromColumns .
129 hunreify .
130 gmakeADT
131 @(TTable (Reify Expr))
132 @TColumns
133 @TUnreify
134 @(Col (Reify Expr))
135 @name
136 @(Eval (rep (Reify Expr)))
137 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
138 (\SSpec {info} -> Reify (E (snull info)))
139 (\SSpec {nullity} -> case nullity of
140 Null -> id
141 NotNull -> \(Reify (E a)) -> Reify (E (nullify a)))
142 (HType . Reify . E . litExpr)
145type GGConstructable :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Constraint
146type GGConstructable algebra rep =
147 ( KnownAlgebra algebra
148 , Eval (GGColumns algebra TColumns (Eval (rep (Reify Aggregate)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
149 , Eval (GGColumns algebra TColumns (Eval (rep (Reify Expr)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
150 , Eval (GGColumns algebra TColumns (Eval (rep (Reify Name)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
151 , HTable (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))))
152 , GGConstructable' algebra rep
153 )
156type GGConstructable' :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Constraint
157type family GGConstructable' algebra rep where
158 GGConstructable' 'K.Product rep =
159 ( Representable TUnreify (Eval (rep (Reify Aggregate)))
160 , Representable TUnreify (Eval (rep (Reify Expr)))
161 , Representable TUnreify (Eval (rep (Reify Name)))
162 , GConstructable (TTable (Reify Aggregate)) TColumns TUnreify (Col (Reify Aggregate)) (Eval (rep (Reify Aggregate)))
163 , GConstructable (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr)) (Eval (rep (Reify Expr)))
164 , GConstructable (TTable (Reify Name)) TColumns TUnreify (Col (Reify Name)) (Eval (rep (Reify Name)))
165 )
166 GGConstructable' 'K.Sum rep =
167 ( RepresentableConstructors TUnreify (Eval (rep (Reify Expr)))
168 , RepresentableFields TUnreify (Eval (rep (Reify Aggregate)))
169 , RepresentableFields TUnreify (Eval (rep (Reify Expr)))
170 , RepresentableFields TUnreify (Eval (rep (Reify Name)))
171 , Functor (GConstructors TUnreify (Eval (rep (Reify Expr))))
172 , GConstructableADT (TTable (Reify Aggregate)) TColumns TUnreify (Col (Reify Aggregate)) (Eval (rep (Reify Aggregate)))
173 , GConstructableADT (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr)) (Eval (rep (Reify Expr)))
174 , GConstructableADT (TTable (Reify Name)) TColumns TUnreify (Col (Reify Name)) (Eval (rep (Reify Name)))
175 )
178type GGConstruct :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
179type family GGConstruct algebra rep r where
180 GGConstruct 'K.Product rep r =
181 GConstruct TUnreify (Eval (rep (Reify Expr))) r -> r
182 GGConstruct 'K.Sum rep r =
183 GConstructADT TUnreify (Eval (rep (Reify Expr))) r r
186ggconstruct :: forall algebra rep a. GGConstructable algebra rep
187 => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr) -> a)
188 -> GGConstruct algebra rep a -> a
189ggconstruct gfromColumns f = case algebraSing @algebra of
190 SProduct ->
191 f $
192 gtabulate @TUnreify @(Eval (rep (Reify Expr))) @a $
193 gfromColumns .
194 hunreify .
195 gconstruct
196 @(TTable (Reify Expr))
197 @TColumns
198 @TUnreify
199 @(Col (Reify Expr))
200 @(Eval (rep (Reify Expr)))
201 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
202 SSum ->
203 gcindex @TUnreify @(Eval (rep (Reify Expr))) @a f $
204 fmap (gfromColumns . hunreify) $
205 gconstructADT
206 @(TTable (Reify Expr))
207 @TColumns
208 @TUnreify
209 @(Col (Reify Expr))
210 @(Eval (rep (Reify Expr)))
211 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
212 (\SSpec {info} -> Reify (E (snull info)))
213 (\SSpec {nullity} -> case nullity of
214 Null -> id
215 NotNull -> \(Reify (E a)) -> Reify (E (nullify a)))
216 (HType . Reify . E . litExpr)
219type GGDeconstruct :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type -> Type
220type family GGDeconstruct algebra rep a r where
221 GGDeconstruct 'K.Product rep a r =
222 GConstruct TUnreify (Eval (rep (Reify Expr))) r -> a -> r
223 GGDeconstruct 'K.Sum rep a r =
224 GConstructADT TUnreify (Eval (rep (Reify Expr))) r (a -> r)
227ggdeconstruct :: forall algebra rep a r. (GGConstructable algebra rep, Table Expr r)
228 => (a -> Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr))
229 -> GGDeconstruct algebra rep a r
230ggdeconstruct gtoColumns = case algebraSing @algebra of
231 SProduct -> \build ->
232 gindex @TUnreify @(Eval (rep (Reify Expr))) @r build .
233 gdeconstruct
234 @(TTable (Reify Expr))
235 @TColumns
236 @TUnreify
237 @(Col (Reify Expr))
238 @(Eval (rep (Reify Expr)))
239 (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns) .
240 hreify .
241 gtoColumns
242 SSum ->
243 gctabulate @TUnreify @(Eval (rep (Reify Expr))) @r @(a -> r) $ \constructors as ->
244 let
245 (HType (Reify (E tag)), cases) =
246 gdeconstructADT
247 @(TTable (Reify Expr))
248 @TColumns
249 @TUnreify
250 @(Col (Reify Expr))
251 @(Eval (rep (Reify Expr)))
252 (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns)
253 (\SSpec {nullity} -> case nullity of
254 Null -> id
255 NotNull -> \(Reify (E a)) -> Reify (E (unsafeUnnullify a)))
256 constructors $
257 hreify $
258 gtoColumns as
259 in
260 case cases of
261 ((_, r) :| (map (first ((tag ==.) . litExpr)) -> cases')) ->
262 case_ cases' r
265type GGName :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
266type family GGName algebra rep a where
267 GGName 'K.Product rep a = GConstruct TUnreify (Eval (rep (Reify Name))) a
268 GGName 'K.Sum rep a = Name Tag -> GBuildADT TUnreify (Eval (rep (Reify Name))) a
271ggname :: forall algebra rep a. GGConstructable algebra rep
272 => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Name) -> a)
273 -> GGName algebra rep a
274ggname gfromColumns = case algebraSing @algebra of
275 SProduct ->
276 gtabulate @TUnreify @(Eval (rep (Reify Name))) @a $
277 gfromColumns .
278 hunreify .
279 gconstruct
280 @(TTable (Reify Name))
281 @TColumns
282 @TUnreify
283 @(Col (Reify Name))
284 @(Eval (rep (Reify Name)))
285 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
286 SSum -> \tag ->
287 gftabulate @TUnreify @(Eval (rep (Reify Name))) @a $
288 gfromColumns .
289 hunreify .
290 gbuildADT
291 @(TTable (Reify Name))
292 @TColumns
293 @TUnreify
294 @(Col (Reify Name))
295 @(Eval (rep (Reify Name)))
296 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
297 (\_ _ (Reify (N (Name a))) -> Reify (N (Name a)))
298 (HType (Reify (N tag)))
301type GGAggregate :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
302type family GGAggregate algebra rep r where
303 GGAggregate 'K.Product rep r =
304 GConstruct TUnreify (Eval (rep (Reify Aggregate))) r ->
305 GConstruct TUnreify (Eval (rep (Reify Expr))) r
306 GGAggregate 'K.Sum rep r =
307 GBuildADT TUnreify (Eval (rep (Reify Aggregate))) r ->
308 GBuildADT TUnreify (Eval (rep (Reify Expr))) r
311ggaggregate :: forall algebra rep exprs agg. GGConstructable algebra rep
312 => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Aggregate) -> agg)
313 -> (exprs -> Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr))
314 -> GGAggregate algebra rep agg -> exprs -> agg
315ggaggregate gfromColumns gtoColumns agg es = case algebraSing @algebra of
316 SProduct -> flip f exprs $
317 gfromColumns .
318 hunreify .
319 gconstruct
320 @(TTable (Reify Aggregate))
321 @TColumns
322 @TUnreify
323 @(Col (Reify Aggregate))
324 @(Eval (rep (Reify Aggregate)))
325 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
326 where
327 f =
328 gindex @TUnreify @(Eval (rep (Reify Expr))) @agg .
329 agg .
330 gtabulate @TUnreify @(Eval (rep (Reify Aggregate))) @agg
331 exprs =
332 gdeconstruct
333 @(TTable (Reify Expr))
334 @TColumns
335 @TUnreify
336 @(Col (Reify Expr))
337 @(Eval (rep (Reify Expr)))
338 (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns) $
339 hreify $
340 gtoColumns es
341 SSum -> flip f exprs $
342 gfromColumns .
343 hunreify .
344 gbuildADT
345 @(TTable (Reify Aggregate))
346 @TColumns
347 @TUnreify
348 @(Col (Reify Aggregate))
349 @(Eval (rep (Reify Aggregate)))
350 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
351 (\tag' SSpec {nullity} (Reify (A (Aggregate a))) ->
352 Reify $ A $ Aggregate $ runTag nullity (tag ==. litExpr tag') <$> a)
353 (HType (Reify (A (groupByExpr tag))))
354 where
355 f =
356 gfindex @TUnreify @(Eval (rep (Reify Expr))) @agg .
357 agg .
358 gftabulate @TUnreify @(Eval (rep (Reify Aggregate))) @agg
359 (HType (Reify (E tag)), exprs) =
360 gunbuildADT
361 @(TTable (Reify Expr))
362 @TColumns
363 @TUnreify
364 @(Col (Reify Expr))
365 @(Eval (rep (Reify Expr)))
366 (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns)
367 (\SSpec {nullity} -> case nullity of
368 Null -> id
369 NotNull -> \(Reify (E a)) -> Reify (E (unsafeUnnullify a))) $
370 hreify $
371 gtoColumns es