git.iko.soy/rel8
on 08dea9f help sign in
rel8/src/Rel8/Generic/Table/ADT.hs
363 lines 11 kB history raw
1{-# language AllowAmbiguousTypes #-}
2{-# language DataKinds #-}
3{-# language FlexibleContexts #-}
4{-# language FlexibleInstances #-}
5{-# language LambdaCase #-}
6{-# language MultiParamTypeClasses #-}
7{-# language PolyKinds #-}
8{-# language RankNTypes #-}
9{-# language ScopedTypeVariables #-}
10{-# language StandaloneKindSignatures #-}
11{-# language TypeApplications #-}
12{-# language TypeFamilies #-}
13{-# language TypeOperators #-}
14{-# language UndecidableInstances #-}
16module Rel8.Generic.Table.ADT
17 ( GTableADT, GColumnsADT, gfromColumnsADT, gtoColumnsADT, gtableADT
18 , GTableADT', GColumnsADT'
19 , GToExprsADT, gfromResultADT, gtoResultADT
20 )
21where
23-- base
24import Data.Kind ( Constraint, Type )
25import Data.Proxy ( Proxy( Proxy ) )
26import GHC.Generics
27 ( (:+:)( L1, R1 ), M1( M1 ), U1( U1 )
28 , C, D
29 , Meta( MetaCons )
30 )
31import GHC.TypeLits ( KnownSymbol, symbolVal )
32import Prelude hiding ( null )
34-- rel8
35import Rel8.FCF ( Eval, Exp )
36import Rel8.Generic.Table.Record
37 ( GTable, GColumns, gtable
38 , GToExprs, gfromResult, gtoResult
39 )
40import Rel8.Schema.Context.Label ( HLabelable, hlabeler, labeler, unlabeler )
41import Rel8.Schema.HTable ( HTable, hmap )
42import Rel8.Schema.HTable.Identity ( HIdentity( HType ), HType )
43import Rel8.Schema.HTable.Label ( HLabel, hlabel, hunlabel )
44import Rel8.Schema.HTable.Nullify ( HNullify, hnulls, hnullify, hunnullify )
45import Rel8.Schema.HTable.Product ( HProduct( HProduct ) )
46import qualified Rel8.Schema.Kind as K
47import Rel8.Schema.Null ( Nullify )
48import Rel8.Schema.Spec ( Spec( Spec ), SSpec )
49import Rel8.Schema.Result
50 ( Col( Result ), Result
51 , null, nullifier, unnullifier
52 )
53import Rel8.Type.Tag ( Tag( Tag ) )
55-- text
56import Data.Text ( pack )
59type GColumnsADT
60 :: (Type -> Exp K.HTable)
61 -> (Type -> Type) -> K.HTable
62type family GColumnsADT _Columns rep where
63 GColumnsADT _Columns (M1 D _ rep) =
64 GColumnsADT' _Columns (HLabel "tag" (HType Tag)) rep
67type GColumnsADT'
68 :: (Type -> Exp K.HTable)
69 -> K.HTable -> (Type -> Type) -> K.HTable
70type family GColumnsADT' _Columns htable rep where
71 GColumnsADT' _Columns htable (a :+: b) =
72 GColumnsADT' _Columns (GColumnsADT' _Columns htable a) b
73 GColumnsADT' _Columns htable (M1 C ('MetaCons _ _ _) U1) = htable
74 GColumnsADT' _Columns htable (M1 C ('MetaCons label _ _) rep) =
75 HProduct htable (HLabel label (HNullify (GColumns _Columns rep)))
78type GTableADT
79 :: (Type -> Exp Constraint)
80 -> (Type -> Exp K.HTable)
81 -> K.HContext -> (Type -> Type) -> Constraint
82class GTableADT _Table _Columns context rep where
83 gfromColumnsADT :: ()
84 => (forall spec. context spec -> Col Result spec)
85 -> (forall spec. Col Result spec -> context spec)
86 -> (forall a. Eval (_Table a) => Eval (_Columns a) context -> a)
87 -> GColumnsADT _Columns rep context
88 -> rep x
90 gtoColumnsADT :: ()
91 => (forall spec. context spec -> Col Result spec)
92 -> (forall spec. Col Result spec -> context spec)
93 -> (forall a. Eval (_Table a) => a -> Eval (_Columns a) context)
94 -> rep x
95 -> GColumnsADT _Columns rep context
97 gtableADT :: ()
98 => (forall a proxy. Eval (_Table a) => proxy a -> Eval (_Columns a) context)
99 -> (forall a labels necessity. ()
100 => SSpec ('Spec labels necessity a)
101 -> context ('Spec labels necessity a)
102 -> context ('Spec labels necessity (Nullify a)))
103 -> GColumnsADT _Columns rep context
106instance
107 ( htable ~ HLabel "tag" (HType Tag)
108 , HTable (GColumnsADT _Columns (M1 D meta rep))
109 , Eval (_Table (htable context))
110 , Eval (_Columns (htable context)) ~ htable
111 , GTableADT' _Table _Columns htable context rep
112 , GToExprsADT' (Const _Table) _Columns htable rep rep
113 )
114 => GTableADT _Table _Columns context (M1 D meta rep)
115 where
116 gfromColumnsADT fromContext toContext fromColumns =
117 gfromResultADT @(Const _Table) @_Columns @(M1 D meta rep) @(M1 D meta rep)
118 (const (fromColumns . hmap toContext)) .
119 hmap fromContext
121 gtoColumnsADT fromContext toContext toColumns =
122 hmap toContext .
123 gtoResultADT @(Const _Table) @_Columns @(M1 D meta rep) @(M1 D meta rep)
124 (const (hmap fromContext . toColumns))
126 gtableADT table hnullifier =
127 gtableADT' @_Table @_Columns @htable @context @rep table hnullifier htable
128 where
129 htable = table (Proxy @(htable context))
132type GTableADT'
133 :: (Type -> Exp Constraint)
134 -> (Type -> Exp K.HTable)
135 -> K.HTable -> K.HContext -> (Type -> Type) -> Constraint
136class GTableADT' _Table _Columns htable context rep where
137 gtableADT' :: ()
138 => (forall a proxy. Eval (_Table a) => proxy a -> Eval (_Columns a) context)
139 -> (forall a labels necessity. ()
140 => SSpec ('Spec labels necessity a)
141 -> context ('Spec labels necessity a)
142 -> context ('Spec labels necessity (Nullify a)))
143 -> htable context
144 -> GColumnsADT' _Columns htable rep context
147instance
148 ( htable' ~ GColumnsADT' _Columns htable a
149 , GTableADT' _Table _Columns htable context a
150 , GTableADT' _Table _Columns htable' context b
151 )
152 => GTableADT' _Table _Columns htable context (a :+: b)
153 where
154 gtableADT' table hnullifier =
155 gtableADT' @_Table @_Columns @_ @_ @b table hnullifier .
156 gtableADT' @_Table @_Columns @_ @_ @a table hnullifier
159instance meta ~ 'MetaCons label _fixity _isRecord =>
160 GTableADT' _Table _Columns htable context (M1 C meta U1)
161 where
162 gtableADT' _ _ = id
165instance {-# OVERLAPPABLE #-}
166 ( HTable (GColumns _Columns rep)
167 , GTable _Table _Columns context rep
168 , HLabelable context
169 , meta ~ 'MetaCons label _fixity _isRecord
170 , KnownSymbol label
171 , GColumnsADT' _Columns htable (M1 C ('MetaCons label _fixity _isRecord) rep) ~
172 HProduct htable (HLabel label (HNullify (GColumns _Columns rep)))
173 )
174 => GTableADT' _Table _Columns htable context (M1 C meta rep)
175 where
176 gtableADT' table hnullifier htable =
177 HProduct htable $
178 hlabel hlabeler $
179 hnullify hnullifier $
180 gtable @_Table @_Columns @_ @rep table
183type GToExprsADT
184 :: (Type -> Type -> Exp Constraint)
185 -> (Type -> Exp K.HTable)
186 -> (Type -> Type) -> (Type -> Type) -> Constraint
187class GToExprsADT _ToExprs _Columns exprs rep where
188 gfromResultADT :: ()
189 => (forall expr a proxy.
190 ( Eval (_ToExprs expr a)
191 , HTable (Eval (_Columns expr))
192 )
193 => proxy expr
194 -> Eval (_Columns expr) (Col Result)
195 -> a)
196 -> GColumnsADT _Columns exprs (Col Result)
197 -> rep x
199 gtoResultADT :: ()
200 => (forall expr a proxy.
201 ( Eval (_ToExprs expr a)
202 , HTable (Eval (_Columns expr))
203 )
204 => proxy expr
205 -> a
206 -> Eval (_Columns expr) (Col Result))
207 -> rep x
208 -> GColumnsADT _Columns exprs (Col Result)
211instance
212 ( htable ~ HLabel "tag" (HType Tag)
213 , GToExprsADT' _ToExprs _Columns htable exprs rep
214 )
215 => GToExprsADT _ToExprs _Columns (M1 D meta exprs) (M1 D meta rep)
216 where
217 gfromResultADT fromResult columns =
218 case gfromResultADT' @_ToExprs @_Columns @_ @exprs fromResult tag columns of
219 Just rep -> M1 rep
220 _ -> error "ADT.fromColumns: mismatch between tag and data"
221 where
222 tag = (\(HType (Result a)) -> a) . hunlabel @_ @"tag" unlabeler
224 gtoResultADT toResult (M1 rep) =
225 gtoResultADT' @_ToExprs @_Columns @_ @exprs toResult tag (Just rep)
226 where
227 tag = hlabel @_ @"tag" labeler . HType . Result
230type GToExprsADT'
231 :: (Type -> Type -> Exp Constraint)
232 -> (Type -> Exp K.HTable)
233 -> K.HTable -> (Type -> Type) -> (Type -> Type) -> Constraint
234class GToExprsADT' _ToExprs _Columns htable exprs rep where
235 gfromResultADT' :: ()
236 => (forall expr a proxy.
237 ( Eval (_ToExprs expr a)
238 , HTable (Eval (_Columns expr))
239 )
240 => proxy expr
241 -> Eval (_Columns expr) (Col Result)
242 -> a)
243 -> (htable (Col Result) -> Tag)
244 -> GColumnsADT' _Columns htable exprs (Col Result)
245 -> Maybe (rep x)
247 gtoResultADT' :: ()
248 => (forall expr a proxy.
249 ( Eval (_ToExprs expr a)
250 , HTable (Eval (_Columns expr))
251 )
252 => proxy expr
253 -> a
254 -> Eval (_Columns expr) (Col Result))
255 -> (Tag -> htable (Col Result))
256 -> Maybe (rep x)
257 -> GColumnsADT' _Columns htable exprs (Col Result)
259 extract :: GColumnsADT' _Columns htable exprs context -> htable context
262instance
263 ( htable' ~ GColumnsADT' _Columns htable a
264 , GToExprsADT' _ToExprs _Columns htable a rep1
265 , GToExprsADT' _ToExprs _Columns htable' b rep2
266 )
267 => GToExprsADT' _ToExprs _Columns htable (a :+: b) (rep1 :+: rep2)
268 where
269 gfromResultADT' fromResult f columns =
270 case ma of
271 Just a -> Just (L1 a)
272 Nothing -> R1 <$>
273 gfromResultADT' @_ToExprs @_Columns @_ @b @rep2
274 fromResult
275 (f . extract @_ToExprs @_Columns @_ @a @rep1)
276 columns
277 where
278 ma =
279 gfromResultADT' @_ToExprs @_Columns @_ @a @rep1
280 fromResult
281 f
282 (extract @_ToExprs @_Columns @_ @b @rep2 columns)
284 gtoResultADT' toResult tag = \case
285 Just (L1 a) ->
286 gtoResultADT' @_ToExprs @_Columns @_ @b @rep2
287 toResult
288 (\_ -> gtoResultADT' @_ToExprs @_Columns @_ @a @rep1
289 toResult
290 tag
291 (Just a))
292 Nothing
293 Just (R1 b) ->
294 gtoResultADT' @_ToExprs @_Columns @_ @b @rep2
295 toResult
296 (\tag' ->
297 gtoResultADT' @_ToExprs @_Columns @_ @a @rep1
298 toResult
299 (\_ -> tag tag')
300 Nothing)
301 (Just b)
302 Nothing ->
303 gtoResultADT' @_ToExprs @_Columns @_ @b @rep2
304 toResult
305 (\_ -> gtoResultADT' @_ToExprs @_Columns @_ @a @rep1 toResult tag Nothing)
306 Nothing
308 extract =
309 extract @_ToExprs @_Columns @_ @a @rep1 .
310 extract @_ToExprs @_Columns @_ @b @rep2
313instance
314 ( meta ~ 'MetaCons label _fixity _isRecord
315 , KnownSymbol label
316 )
317 => GToExprsADT' _ToExprs _Columns htable (M1 C meta U1) (M1 C meta U1)
318 where
319 gfromResultADT' _ tag columns
320 | tag columns == tag' = Just (M1 U1)
321 | otherwise = Nothing
322 where
323 tag' = Tag $ pack $ symbolVal (Proxy @label)
325 gtoResultADT' _ tag _ = tag tag'
326 where
327 tag' = Tag $ pack $ symbolVal (Proxy @label)
329 extract = id
332instance {-# OVERLAPPABLE #-}
333 ( HTable (GColumns _Columns exprs)
334 , GToExprs _ToExprs _Columns exprs rep
335 , meta ~ 'MetaCons label _fixity _isRecord
336 , KnownSymbol label
337 , GColumnsADT' _Columns htable (M1 C meta exprs) ~
338 HProduct htable (HLabel label (HNullify (GColumns _Columns exprs)))
339 )
340 => GToExprsADT' _ToExprs _Columns htable (M1 C meta exprs) (M1 C meta rep)
341 where
342 gfromResultADT' fromResult tag (HProduct a b)
343 | tag a == tag' =
344 M1 . gfromResult @_ToExprs @_Columns @exprs fromResult <$>
345 hunnullify unnullifier (hunlabel unlabeler b)
346 | otherwise = Nothing
347 where
348 tag' = Tag $ pack $ symbolVal (Proxy @label)
350 gtoResultADT' toResult tag = \case
351 Nothing -> HProduct (tag tag') (hlabel labeler (hnulls (const null)))
352 Just (M1 rep) -> HProduct (tag tag') $
353 hlabel labeler $
354 hnullify nullifier $
355 gtoResult @_ToExprs @_Columns @exprs toResult rep
356 where
357 tag' = Tag $ pack $ symbolVal (Proxy @label)
359 extract (HProduct a _) = a
362data Const :: (a -> Exp Constraint) -> a -> a -> Exp Constraint
363type instance Eval (Const f x a) = (Eval (f a), x ~ a)