git.iko.soy/rel8
on 97d89cf help sign in
rel8/src/Rel8/Generic/Table/ADT.hs
225 lines 7.1 kB history raw
1{-# language AllowAmbiguousTypes #-}
2{-# language DataKinds #-}
3{-# language FlexibleInstances #-}
4{-# language LambdaCase #-}
5{-# language MultiParamTypeClasses #-}
6{-# language RankNTypes #-}
7{-# language ScopedTypeVariables #-}
8{-# language StandaloneKindSignatures #-}
9{-# language TypeApplications #-}
10{-# language TypeFamilies #-}
11{-# language TypeOperators #-}
12{-# language UndecidableInstances #-}
14module Rel8.Generic.Table.ADT
15 ( GTableADT, GColumnsADT, gfromResultADT, gtoResultADT
16 , GTableADT', GColumnsADT'
17 )
18where
20-- base
21import Data.Kind ( Constraint, Type )
22import Data.Proxy ( Proxy( Proxy ) )
23import GHC.Generics
24 ( (:+:)( L1, R1 ), M1( M1 ), U1( U1 )
25 , C, D
26 , Meta( MetaCons )
27 )
28import GHC.TypeLits ( KnownSymbol, symbolVal )
29import Prelude hiding ( null )
31-- rel8
32import Rel8.FCF ( Eval, Exp )
33import Rel8.Generic.Map ( GMap )
34import Rel8.Generic.Table.Record ( GTable, GColumns, gfromResult, gtoResult )
35import Rel8.Schema.HTable ( HTable )
36import Rel8.Schema.HTable.Identity ( HIdentity( HType ), HType )
37import Rel8.Schema.HTable.Label ( HLabel, hlabel, hunlabel )
38import Rel8.Schema.HTable.Nullify ( HNullify, hnulls, hnullify, hunnullify )
39import Rel8.Schema.HTable.Product ( HProduct( HProduct ) )
40import qualified Rel8.Schema.Kind as K
41import Rel8.Schema.Result
42 ( Result( R )
43 , null, nullifier, unnullifier
44 )
45import Rel8.Type.Tag ( Tag( Tag ) )
47-- text
48import Data.Text ( pack )
51type GColumnsADT
52 :: (Type -> Exp K.HTable)
53 -> (Type -> Type) -> K.HTable
54type family GColumnsADT _Columns rep where
55 GColumnsADT _Columns (M1 D _ rep) =
56 GColumnsADT' _Columns (HLabel "tag" (HType Tag)) rep
59type GColumnsADT'
60 :: (Type -> Exp K.HTable)
61 -> K.HTable -> (Type -> Type) -> K.HTable
62type family GColumnsADT' _Columns htable rep where
63 GColumnsADT' _Columns htable (a :+: b) =
64 GColumnsADT' _Columns (GColumnsADT' _Columns htable a) b
65 GColumnsADT' _Columns htable (M1 C ('MetaCons _ _ _) U1) = htable
66 GColumnsADT' _Columns htable (M1 C ('MetaCons label _ _) rep) =
67 HProduct htable (HLabel label (HNullify (GColumns _Columns rep)))
70type GTableADT
71 :: (Type -> Exp Constraint)
72 -> (Type -> Exp K.HTable)
73 -> (Type -> Exp Type)
74 -> (Type -> Type) -> Constraint
75class GTableADT _Table _Columns _FromExprs rep where
76 gfromResultADT :: ()
77 => (forall a proxy. Eval (_Table a)
78 => proxy a -> Eval (_Columns a) Result -> Eval (_FromExprs a))
79 -> GColumnsADT _Columns rep Result
80 -> GMap _FromExprs rep x
82 gtoResultADT :: ()
83 => (forall a proxy. Eval (_Table a)
84 => proxy a -> Eval (_FromExprs a) -> Eval (_Columns a) Result)
85 -> GMap _FromExprs rep x
86 -> GColumnsADT _Columns rep Result
89instance
90 ( htable ~ HLabel "tag" (HType Tag)
91 , GTableADT' _Table _Columns _FromExprs htable rep
92 )
93 => GTableADT _Table _Columns _FromExprs (M1 D meta rep)
94 where
95 gfromResultADT fromResult columns =
96 case gfromResultADT' @_Table @_Columns @_FromExprs @htable @rep fromResult tag columns of
97 Just rep -> M1 rep
98 _ -> error "ADT.fromColumns: mismatch between tag and data"
99 where
100 tag = (\(HType (R a)) -> a) . hunlabel @"tag"
102 gtoResultADT toResult (M1 rep) =
103 gtoResultADT' @_Table @_Columns @_FromExprs @htable @rep toResult tag (Just rep)
104 where
105 tag = hlabel @"tag" . HType . R
108type GTableADT'
109 :: (Type -> Exp Constraint)
110 -> (Type -> Exp K.HTable)
111 -> (Type -> Exp Type)
112 -> K.HTable -> (Type -> Type) -> Constraint
113class GTableADT' _Table _Columns _FromExprs htable rep where
114 gfromResultADT' :: context ~ Result
115 => (forall a proxy. Eval (_Table a)
116 => proxy a -> Eval (_Columns a) context -> Eval (_FromExprs a))
117 -> (htable Result -> Tag)
118 -> GColumnsADT' _Columns htable rep context
119 -> Maybe (GMap _FromExprs rep x)
121 gtoResultADT' :: context ~ Result
122 => (forall a proxy. Eval (_Table a)
123 => proxy a -> Eval (_FromExprs a) -> Eval (_Columns a) context)
124 -> (Tag -> htable Result)
125 -> Maybe (GMap _FromExprs rep x)
126 -> GColumnsADT' _Columns htable rep context
128 extract :: GColumnsADT' _Columns htable rep context -> htable context
131instance
132 ( htable' ~ GColumnsADT' _Columns htable a
133 , GTableADT' _Table _Columns _FromExprs htable a
134 , GTableADT' _Table _Columns _FromExprs htable' b
135 )
136 => GTableADT' _Table _Columns _FromExprs htable (a :+: b)
137 where
138 gfromResultADT' fromResult f columns =
139 case ma of
140 Just a -> Just (L1 a)
141 Nothing -> R1 <$>
142 gfromResultADT' @_Table @_Columns @_FromExprs @_ @b
143 fromResult
144 (f . extract @_Table @_Columns @_FromExprs @_ @a)
145 columns
146 where
147 ma =
148 gfromResultADT' @_Table @_Columns @_FromExprs @_ @a
149 fromResult
150 f
151 (extract @_Table @_Columns @_FromExprs @_ @b columns)
153 gtoResultADT' toResult tag = \case
154 Just (L1 a) ->
155 gtoResultADT' @_Table @_Columns @_FromExprs @_ @b
156 toResult
157 (\_ -> gtoResultADT' @_Table @_Columns @_FromExprs @_ @a
158 toResult
159 tag
160 (Just a))
161 Nothing
162 Just (R1 b) ->
163 gtoResultADT' @_Table @_Columns @_FromExprs @_ @b
164 toResult
165 (\tag' ->
166 gtoResultADT' @_Table @_Columns @_FromExprs @_ @a
167 toResult
168 (\_ -> tag tag')
169 Nothing)
170 (Just b)
171 Nothing ->
172 gtoResultADT' @_Table @_Columns @_FromExprs @_ @b
173 toResult
174 (\_ -> gtoResultADT' @_Table @_Columns @_FromExprs @_ @a toResult tag Nothing)
175 Nothing
177 extract =
178 extract @_Table @_Columns @_FromExprs @_ @a .
179 extract @_Table @_Columns @_FromExprs @_ @b
182instance (meta ~ 'MetaCons label _fixity _isRecord, KnownSymbol label) =>
183 GTableADT' _Table _Columns _FromExprs htable (M1 C meta U1)
184 where
185 gfromResultADT' _ tag columns
186 | tag columns == tag' = Just (M1 U1)
187 | otherwise = Nothing
188 where
189 tag' = Tag $ pack $ symbolVal (Proxy @label)
191 gtoResultADT' _ tag _ = tag tag'
192 where
193 tag' = Tag $ pack $ symbolVal (Proxy @label)
195 extract = id
198instance {-# OVERLAPPABLE #-}
199 ( HTable (GColumns _Columns rep)
200 , GTable _Table _Columns _FromExprs rep
201 , meta ~ 'MetaCons label _fixity _isRecord
202 , KnownSymbol label
203 , GColumnsADT' _Columns htable (M1 C ('MetaCons label _fixity _isRecord) rep) ~
204 HProduct htable (HLabel label (HNullify (GColumns _Columns rep)))
205 )
206 => GTableADT' _Table _Columns _FromExprs htable (M1 C meta rep)
207 where
208 gfromResultADT' fromResult tag (HProduct a b)
209 | tag a == tag' =
210 M1 . gfromResult @_Table @_Columns @_FromExprs @rep fromResult <$>
211 hunnullify unnullifier (hunlabel b)
212 | otherwise = Nothing
213 where
214 tag' = Tag $ pack $ symbolVal (Proxy @label)
216 gtoResultADT' toResult tag = \case
217 Nothing -> HProduct (tag tag') (hlabel (hnulls (const null)))
218 Just (M1 rep) -> HProduct (tag tag') $
219 hlabel $
220 hnullify nullifier $
221 gtoResult @_Table @_Columns @_FromExprs @rep toResult rep
222 where
223 tag' = Tag $ pack $ symbolVal (Proxy @label)
225 extract (HProduct a _) = a