git.iko.soy/rel8
on fb3d2d9 help sign in
rel8/src/Rel8/Generic/Table/ADT.hs
362 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 , GToExprsADT, gfromResultADT, gtoResultADT
19 )
20where
22-- base
23import Data.Kind ( Constraint, Type )
24import Data.Proxy ( Proxy( Proxy ) )
25import GHC.Generics
26 ( (:+:)( L1, R1 ), M1( M1 ), U1( U1 )
27 , C, D
28 , Meta( MetaCons )
29 )
30import GHC.TypeLits ( KnownSymbol, symbolVal )
31import Prelude hiding ( null )
33-- rel8
34import Rel8.FCF ( Eval, Exp )
35import Rel8.Generic.Table.Record
36 ( GTable, GColumns, gtable
37 , GToExprs, gfromResult, gtoResult
38 )
39import Rel8.Schema.Context.Label ( HLabelable, hlabeler, labeler, unlabeler )
40import Rel8.Schema.HTable ( HTable, hmap )
41import Rel8.Schema.HTable.Label ( HLabel, hlabel, hunlabel )
42import Rel8.Schema.HTable.Nullify ( HNullify, hnulls, hnullify, hunnullify )
43import Rel8.Schema.HTable.Product ( HProduct( HProduct ) )
44import Rel8.Schema.HTable.Type ( HType( HType ) )
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( Result ), 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 labels necessity. ()
99 => SSpec ('Spec labels necessity a)
100 -> context ('Spec labels necessity a)
101 -> context ('Spec labels necessity (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 labels necessity. ()
139 => SSpec ('Spec labels necessity a)
140 -> context ('Spec labels necessity a)
141 -> context ('Spec labels necessity (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 , HLabelable context
168 , meta ~ 'MetaCons label _fixity _isRecord
169 , KnownSymbol label
170 , GColumnsADT' _Columns htable (M1 C ('MetaCons label _fixity _isRecord) rep) ~
171 HProduct htable (HLabel label (HNullify (GColumns _Columns rep)))
172 )
173 => GTableADT' _Table _Columns htable context (M1 C meta rep)
174 where
175 gtableADT' table hnullifier htable =
176 HProduct htable $
177 hlabel hlabeler $
178 hnullify hnullifier $
179 gtable @_Table @_Columns @_ @rep table
182type GToExprsADT
183 :: (Type -> Type -> Exp Constraint)
184 -> (Type -> Exp K.HTable)
185 -> (Type -> Type) -> (Type -> Type) -> Constraint
186class GToExprsADT _ToExprs _Columns exprs rep where
187 gfromResultADT :: ()
188 => (forall expr a proxy.
189 ( Eval (_ToExprs expr a)
190 , HTable (Eval (_Columns expr))
191 )
192 => proxy expr
193 -> Eval (_Columns expr) (Col Result)
194 -> a)
195 -> GColumnsADT _Columns exprs (Col Result)
196 -> rep x
198 gtoResultADT :: ()
199 => (forall expr a proxy.
200 ( Eval (_ToExprs expr a)
201 , HTable (Eval (_Columns expr))
202 )
203 => proxy expr
204 -> a
205 -> Eval (_Columns expr) (Col Result))
206 -> rep x
207 -> GColumnsADT _Columns exprs (Col Result)
210instance
211 ( htable ~ HLabel "tag" (HType Tag)
212 , GToExprsADT' _ToExprs _Columns htable exprs rep
213 )
214 => GToExprsADT _ToExprs _Columns (M1 D meta exprs) (M1 D meta rep)
215 where
216 gfromResultADT fromResult columns =
217 case gfromResultADT' @_ToExprs @_Columns @_ @exprs fromResult tag columns of
218 Just rep -> M1 rep
219 _ -> error "ADT.fromColumns: mismatch between tag and data"
220 where
221 tag = (\(HType (Result a)) -> a) . hunlabel @_ @"tag" unlabeler
223 gtoResultADT toResult (M1 rep) =
224 gtoResultADT' @_ToExprs @_Columns @_ @exprs toResult tag (Just rep)
225 where
226 tag = hlabel @_ @"tag" labeler . HType . Result
229type GToExprsADT'
230 :: (Type -> Type -> Exp Constraint)
231 -> (Type -> Exp K.HTable)
232 -> K.HTable -> (Type -> Type) -> (Type -> Type) -> Constraint
233class GToExprsADT' _ToExprs _Columns htable exprs rep where
234 gfromResultADT' :: ()
235 => (forall expr a proxy.
236 ( Eval (_ToExprs expr a)
237 , HTable (Eval (_Columns expr))
238 )
239 => proxy expr
240 -> Eval (_Columns expr) (Col Result)
241 -> a)
242 -> (htable (Col Result) -> Tag)
243 -> GColumnsADT' _Columns htable exprs (Col Result)
244 -> Maybe (rep x)
246 gtoResultADT' :: ()
247 => (forall expr a proxy.
248 ( Eval (_ToExprs expr a)
249 , HTable (Eval (_Columns expr))
250 )
251 => proxy expr
252 -> a
253 -> Eval (_Columns expr) (Col Result))
254 -> (Tag -> htable (Col Result))
255 -> Maybe (rep x)
256 -> GColumnsADT' _Columns htable exprs (Col Result)
258 extract :: GColumnsADT' _Columns htable exprs context -> htable context
261instance
262 ( htable' ~ GColumnsADT' _Columns htable a
263 , GToExprsADT' _ToExprs _Columns htable a rep1
264 , GToExprsADT' _ToExprs _Columns htable' b rep2
265 )
266 => GToExprsADT' _ToExprs _Columns htable (a :+: b) (rep1 :+: rep2)
267 where
268 gfromResultADT' fromResult f columns =
269 case ma of
270 Just a -> Just (L1 a)
271 Nothing -> R1 <$>
272 gfromResultADT' @_ToExprs @_Columns @_ @b @rep2
273 fromResult
274 (f . extract @_ToExprs @_Columns @_ @a @rep1)
275 columns
276 where
277 ma =
278 gfromResultADT' @_ToExprs @_Columns @_ @a @rep1
279 fromResult
280 f
281 (extract @_ToExprs @_Columns @_ @b @rep2 columns)
283 gtoResultADT' toResult tag = \case
284 Just (L1 a) ->
285 gtoResultADT' @_ToExprs @_Columns @_ @b @rep2
286 toResult
287 (\_ -> gtoResultADT' @_ToExprs @_Columns @_ @a @rep1
288 toResult
289 tag
290 (Just a))
291 Nothing
292 Just (R1 b) ->
293 gtoResultADT' @_ToExprs @_Columns @_ @b @rep2
294 toResult
295 (\tag' ->
296 gtoResultADT' @_ToExprs @_Columns @_ @a @rep1
297 toResult
298 (\_ -> tag tag')
299 Nothing)
300 (Just b)
301 Nothing ->
302 gtoResultADT' @_ToExprs @_Columns @_ @b @rep2
303 toResult
304 (\_ -> gtoResultADT' @_ToExprs @_Columns @_ @a @rep1 toResult tag Nothing)
305 Nothing
307 extract =
308 extract @_ToExprs @_Columns @_ @a @rep1 .
309 extract @_ToExprs @_Columns @_ @b @rep2
312instance
313 ( meta ~ 'MetaCons label _fixity _isRecord
314 , KnownSymbol label
315 )
316 => GToExprsADT' _ToExprs _Columns htable (M1 C meta U1) (M1 C meta U1)
317 where
318 gfromResultADT' _ tag columns
319 | tag columns == tag' = Just (M1 U1)
320 | otherwise = Nothing
321 where
322 tag' = Tag $ pack $ symbolVal (Proxy @label)
324 gtoResultADT' _ tag _ = tag tag'
325 where
326 tag' = Tag $ pack $ symbolVal (Proxy @label)
328 extract = id
331instance {-# OVERLAPPABLE #-}
332 ( HTable (GColumns _Columns exprs)
333 , GToExprs _ToExprs _Columns exprs rep
334 , meta ~ 'MetaCons label _fixity _isRecord
335 , KnownSymbol label
336 , GColumnsADT' _Columns htable (M1 C meta exprs) ~
337 HProduct htable (HLabel label (HNullify (GColumns _Columns exprs)))
338 )
339 => GToExprsADT' _ToExprs _Columns htable (M1 C meta exprs) (M1 C meta rep)
340 where
341 gfromResultADT' fromResult tag (HProduct a b)
342 | tag a == tag' =
343 M1 . gfromResult @_ToExprs @_Columns @exprs fromResult <$>
344 hunnullify unnullifier (hunlabel unlabeler b)
345 | otherwise = Nothing
346 where
347 tag' = Tag $ pack $ symbolVal (Proxy @label)
349 gtoResultADT' toResult tag = \case
350 Nothing -> HProduct (tag tag') (hlabel labeler (hnulls null))
351 Just (M1 rep) -> HProduct (tag tag') $
352 hlabel labeler $
353 hnullify nullifier $
354 gtoResult @_ToExprs @_Columns @exprs toResult rep
355 where
356 tag' = Tag $ pack $ symbolVal (Proxy @label)
358 extract (HProduct a _) = a
361data Const :: (a -> Exp Constraint) -> a -> a -> Exp Constraint
362type instance Eval (Const f x a) = (Eval (f a), x ~ a)