git.iko.soy/rel8
on c6ffdab help sign in
rel8/src/Rel8/Generic/Table/ADT.hs
360 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.HTable ( HTable, hmap )
41import Rel8.Schema.HTable.Identity ( HIdentity( HType ), HType )
42import Rel8.Schema.HTable.Label ( HLabel, hlabel, hunlabel )
43import Rel8.Schema.HTable.Nullify ( HNullify, hnulls, hnullify, hunnullify )
44import Rel8.Schema.HTable.Product ( HProduct( HProduct ) )
45import qualified Rel8.Schema.Kind as K
46import Rel8.Schema.Null ( Nullify )
47import Rel8.Schema.Spec ( Spec( Spec ), SSpec )
48import Rel8.Schema.Result
49 ( Col( R ), Result
50 , null, nullifier, unnullifier
51 )
52import Rel8.Type.Tag ( Tag( Tag ) )
54-- text
55import Data.Text ( pack )
58type GColumnsADT
59 :: (Type -> Exp K.HTable)
60 -> (Type -> Type) -> K.HTable
61type family GColumnsADT _Columns rep where
62 GColumnsADT _Columns (M1 D _ rep) =
63 GColumnsADT' _Columns (HLabel "tag" (HType Tag)) rep
66type GColumnsADT'
67 :: (Type -> Exp K.HTable)
68 -> K.HTable -> (Type -> Type) -> K.HTable
69type family GColumnsADT' _Columns htable rep where
70 GColumnsADT' _Columns htable (a :+: b) =
71 GColumnsADT' _Columns (GColumnsADT' _Columns htable a) b
72 GColumnsADT' _Columns htable (M1 C ('MetaCons _ _ _) U1) = htable
73 GColumnsADT' _Columns htable (M1 C ('MetaCons label _ _) rep) =
74 HProduct htable (HLabel label (HNullify (GColumns _Columns rep)))
77type GTableADT
78 :: (Type -> Exp Constraint)
79 -> (Type -> Exp K.HTable)
80 -> K.HContext -> (Type -> Type) -> Constraint
81class GTableADT _Table _Columns context rep where
82 gfromColumnsADT :: ()
83 => (forall spec. context spec -> Col Result spec)
84 -> (forall spec. Col Result spec -> context spec)
85 -> (forall a. Eval (_Table a) => Eval (_Columns a) context -> a)
86 -> GColumnsADT _Columns rep context
87 -> rep x
89 gtoColumnsADT :: ()
90 => (forall spec. context spec -> Col Result spec)
91 -> (forall spec. Col Result spec -> context spec)
92 -> (forall a. Eval (_Table a) => a -> Eval (_Columns a) context)
93 -> rep x
94 -> GColumnsADT _Columns rep context
96 gtableADT :: ()
97 => (forall a proxy. Eval (_Table a) => proxy a -> Eval (_Columns a) context)
98 -> (forall a. ()
99 => SSpec ('Spec a)
100 -> context ('Spec a)
101 -> context ('Spec (Nullify a)))
102 -> GColumnsADT _Columns rep context
105instance
106 ( htable ~ HLabel "tag" (HType Tag)
107 , HTable (GColumnsADT _Columns (M1 D meta rep))
108 , Eval (_Table (htable context))
109 , Eval (_Columns (htable context)) ~ htable
110 , GTableADT' _Table _Columns htable context rep
111 , GToExprsADT' (Const _Table) _Columns htable rep rep
112 )
113 => GTableADT _Table _Columns context (M1 D meta rep)
114 where
115 gfromColumnsADT fromContext toContext fromColumns =
116 gfromResultADT @(Const _Table) @_Columns @(M1 D meta rep) @(M1 D meta rep)
117 (const (fromColumns . hmap toContext)) .
118 hmap fromContext
120 gtoColumnsADT fromContext toContext toColumns =
121 hmap toContext .
122 gtoResultADT @(Const _Table) @_Columns @(M1 D meta rep) @(M1 D meta rep)
123 (const (hmap fromContext . toColumns))
125 gtableADT table hnullifier =
126 gtableADT' @_Table @_Columns @htable @context @rep table hnullifier htable
127 where
128 htable = table (Proxy @(htable context))
131type GTableADT'
132 :: (Type -> Exp Constraint)
133 -> (Type -> Exp K.HTable)
134 -> K.HTable -> K.HContext -> (Type -> Type) -> Constraint
135class GTableADT' _Table _Columns htable context rep where
136 gtableADT' :: ()
137 => (forall a proxy. Eval (_Table a) => proxy a -> Eval (_Columns a) context)
138 -> (forall a. ()
139 => SSpec ('Spec a)
140 -> context ('Spec a)
141 -> context ('Spec (Nullify a)))
142 -> htable context
143 -> GColumnsADT' _Columns htable rep context
146instance
147 ( htable' ~ GColumnsADT' _Columns htable a
148 , GTableADT' _Table _Columns htable context a
149 , GTableADT' _Table _Columns htable' context b
150 )
151 => GTableADT' _Table _Columns htable context (a :+: b)
152 where
153 gtableADT' table hnullifier =
154 gtableADT' @_Table @_Columns @_ @_ @b table hnullifier .
155 gtableADT' @_Table @_Columns @_ @_ @a table hnullifier
158instance meta ~ 'MetaCons label _fixity _isRecord =>
159 GTableADT' _Table _Columns htable context (M1 C meta U1)
160 where
161 gtableADT' _ _ = id
164instance {-# OVERLAPPABLE #-}
165 ( HTable (GColumns _Columns rep)
166 , GTable _Table _Columns context rep
167 , meta ~ 'MetaCons label _fixity _isRecord
168 , GColumnsADT' _Columns htable (M1 C ('MetaCons label _fixity _isRecord) rep) ~
169 HProduct htable (HLabel label (HNullify (GColumns _Columns rep)))
170 )
171 => GTableADT' _Table _Columns htable context (M1 C meta rep)
172 where
173 gtableADT' table hnullifier htable =
174 HProduct htable $
175 hlabel $
176 hnullify hnullifier $
177 gtable @_Table @_Columns @_ @rep table
180type GToExprsADT
181 :: (Type -> Type -> Exp Constraint)
182 -> (Type -> Exp K.HTable)
183 -> (Type -> Type) -> (Type -> Type) -> Constraint
184class GToExprsADT _ToExprs _Columns exprs rep where
185 gfromResultADT :: ()
186 => (forall expr a proxy.
187 ( Eval (_ToExprs expr a)
188 , HTable (Eval (_Columns expr))
189 )
190 => proxy expr
191 -> Eval (_Columns expr) (Col Result)
192 -> a)
193 -> GColumnsADT _Columns exprs (Col Result)
194 -> rep x
196 gtoResultADT :: ()
197 => (forall expr a proxy.
198 ( Eval (_ToExprs expr a)
199 , HTable (Eval (_Columns expr))
200 )
201 => proxy expr
202 -> a
203 -> Eval (_Columns expr) (Col Result))
204 -> rep x
205 -> GColumnsADT _Columns exprs (Col Result)
208instance
209 ( htable ~ HLabel "tag" (HType Tag)
210 , GToExprsADT' _ToExprs _Columns htable exprs rep
211 )
212 => GToExprsADT _ToExprs _Columns (M1 D meta exprs) (M1 D meta rep)
213 where
214 gfromResultADT fromResult columns =
215 case gfromResultADT' @_ToExprs @_Columns @_ @exprs fromResult tag columns of
216 Just rep -> M1 rep
217 _ -> error "ADT.fromColumns: mismatch between tag and data"
218 where
219 tag = (\(HType (R a)) -> a) . hunlabel @"tag"
221 gtoResultADT toResult (M1 rep) =
222 gtoResultADT' @_ToExprs @_Columns @_ @exprs toResult tag (Just rep)
223 where
224 tag = hlabel @"tag" . HType . R
227type GToExprsADT'
228 :: (Type -> Type -> Exp Constraint)
229 -> (Type -> Exp K.HTable)
230 -> K.HTable -> (Type -> Type) -> (Type -> Type) -> Constraint
231class GToExprsADT' _ToExprs _Columns htable exprs rep where
232 gfromResultADT' :: ()
233 => (forall expr a proxy.
234 ( Eval (_ToExprs expr a)
235 , HTable (Eval (_Columns expr))
236 )
237 => proxy expr
238 -> Eval (_Columns expr) (Col Result)
239 -> a)
240 -> (htable (Col Result) -> Tag)
241 -> GColumnsADT' _Columns htable exprs (Col Result)
242 -> Maybe (rep x)
244 gtoResultADT' :: ()
245 => (forall expr a proxy.
246 ( Eval (_ToExprs expr a)
247 , HTable (Eval (_Columns expr))
248 )
249 => proxy expr
250 -> a
251 -> Eval (_Columns expr) (Col Result))
252 -> (Tag -> htable (Col Result))
253 -> Maybe (rep x)
254 -> GColumnsADT' _Columns htable exprs (Col Result)
256 extract :: GColumnsADT' _Columns htable exprs context -> htable context
259instance
260 ( htable' ~ GColumnsADT' _Columns htable a
261 , GToExprsADT' _ToExprs _Columns htable a rep1
262 , GToExprsADT' _ToExprs _Columns htable' b rep2
263 )
264 => GToExprsADT' _ToExprs _Columns htable (a :+: b) (rep1 :+: rep2)
265 where
266 gfromResultADT' fromResult f columns =
267 case ma of
268 Just a -> Just (L1 a)
269 Nothing -> R1 <$>
270 gfromResultADT' @_ToExprs @_Columns @_ @b @rep2
271 fromResult
272 (f . extract @_ToExprs @_Columns @_ @a @rep1)
273 columns
274 where
275 ma =
276 gfromResultADT' @_ToExprs @_Columns @_ @a @rep1
277 fromResult
278 f
279 (extract @_ToExprs @_Columns @_ @b @rep2 columns)
281 gtoResultADT' toResult tag = \case
282 Just (L1 a) ->
283 gtoResultADT' @_ToExprs @_Columns @_ @b @rep2
284 toResult
285 (\_ -> gtoResultADT' @_ToExprs @_Columns @_ @a @rep1
286 toResult
287 tag
288 (Just a))
289 Nothing
290 Just (R1 b) ->
291 gtoResultADT' @_ToExprs @_Columns @_ @b @rep2
292 toResult
293 (\tag' ->
294 gtoResultADT' @_ToExprs @_Columns @_ @a @rep1
295 toResult
296 (\_ -> tag tag')
297 Nothing)
298 (Just b)
299 Nothing ->
300 gtoResultADT' @_ToExprs @_Columns @_ @b @rep2
301 toResult
302 (\_ -> gtoResultADT' @_ToExprs @_Columns @_ @a @rep1 toResult tag Nothing)
303 Nothing
305 extract =
306 extract @_ToExprs @_Columns @_ @a @rep1 .
307 extract @_ToExprs @_Columns @_ @b @rep2
310instance
311 ( meta ~ 'MetaCons label _fixity _isRecord
312 , KnownSymbol label
313 )
314 => GToExprsADT' _ToExprs _Columns htable (M1 C meta U1) (M1 C meta U1)
315 where
316 gfromResultADT' _ tag columns
317 | tag columns == tag' = Just (M1 U1)
318 | otherwise = Nothing
319 where
320 tag' = Tag $ pack $ symbolVal (Proxy @label)
322 gtoResultADT' _ tag _ = tag tag'
323 where
324 tag' = Tag $ pack $ symbolVal (Proxy @label)
326 extract = id
329instance {-# OVERLAPPABLE #-}
330 ( HTable (GColumns _Columns exprs)
331 , GToExprs _ToExprs _Columns exprs rep
332 , meta ~ 'MetaCons label _fixity _isRecord
333 , KnownSymbol label
334 , GColumnsADT' _Columns htable (M1 C meta exprs) ~
335 HProduct htable (HLabel label (HNullify (GColumns _Columns exprs)))
336 )
337 => GToExprsADT' _ToExprs _Columns htable (M1 C meta exprs) (M1 C meta rep)
338 where
339 gfromResultADT' fromResult tag (HProduct a b)
340 | tag a == tag' =
341 M1 . gfromResult @_ToExprs @_Columns @exprs fromResult <$>
342 hunnullify unnullifier (hunlabel b)
343 | otherwise = Nothing
344 where
345 tag' = Tag $ pack $ symbolVal (Proxy @label)
347 gtoResultADT' toResult tag = \case
348 Nothing -> HProduct (tag tag') (hlabel (hnulls (const null)))
349 Just (M1 rep) -> HProduct (tag tag') $
350 hlabel $
351 hnullify nullifier $
352 gtoResult @_ToExprs @_Columns @exprs toResult rep
353 where
354 tag' = Tag $ pack $ symbolVal (Proxy @label)
356 extract (HProduct a _) = a
359data Const :: (a -> Exp Constraint) -> a -> a -> Exp Constraint
360type instance Eval (Const f x a) = (Eval (f a), x ~ a)