on 29cdfdb help sign in
220 lines 7.2 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 ( GSerializeADT, GColumnsADT, gfromResultADT, gtoResultADT
16 , GSerializeADT', GColumnsADT'
17 )
18where
20-- base
21import Data.Functor.Identity ( Identity( Identity ) )
22import Data.Kind ( Constraint, Type )
23import Data.Proxy ( Proxy( Proxy ) )
24import GHC.Generics
25 ( (:+:)( L1, R1 ), M1( M1 ), U1( U1 )
26 , C, D
27 , Meta( MetaCons )
28 )
29import GHC.TypeLits ( KnownSymbol, symbolVal )
30import Prelude hiding ( null )
32-- rel8
33import Rel8.FCF ( Eval, Exp )
34import Rel8.Generic.Table.Record ( GSerialize, GColumns, gfromResult, gtoResult )
35import Rel8.Schema.HTable ( HTable )
36import Rel8.Schema.HTable.Identity ( HIdentity( HIdentity ) )
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 ( Result, null, nullifier, unnullifier )
42import Rel8.Type.Tag ( Tag( Tag ) )
44-- text
45import Data.Text ( pack )
48type GColumnsADT
49 :: (Type -> Exp K.HTable)
50 -> (Type -> Type) -> K.HTable
51type family GColumnsADT _Columns rep where
52 GColumnsADT _Columns (M1 D _ rep) =
53 GColumnsADT' _Columns (HLabel "tag" (HIdentity Tag)) rep
56type GColumnsADT'
57 :: (Type -> Exp K.HTable)
58 -> K.HTable -> (Type -> Type) -> K.HTable
59type family GColumnsADT' _Columns htable rep where
60 GColumnsADT' _Columns htable (a :+: b) =
61 GColumnsADT' _Columns (GColumnsADT' _Columns htable a) b
62 GColumnsADT' _Columns htable (M1 C ('MetaCons _ _ _) U1) = htable
63 GColumnsADT' _Columns htable (M1 C ('MetaCons label _ _) rep) =
64 HProduct htable (HLabel label (HNullify (GColumns _Columns rep)))
67type GSerializeADT
68 :: (Type -> Type -> Exp Constraint)
69 -> (Type -> Exp K.HTable)
70 -> (Type -> Type) -> (Type -> Type) -> Constraint
71class GSerializeADT _Serialize _Columns exprs rep where
72 gfromResultADT :: ()
73 => (forall expr a proxy. Eval (_Serialize expr a)
74 => proxy expr -> Eval (_Columns expr) Result -> a)
75 -> GColumnsADT _Columns exprs Result
76 -> rep x
78 gtoResultADT :: ()
79 => (forall expr a proxy. Eval (_Serialize expr a)
80 => proxy expr -> a -> Eval (_Columns expr) Result)
81 -> rep x
82 -> GColumnsADT _Columns exprs Result
85instance
86 ( htable ~ HLabel "tag" (HIdentity Tag)
87 , GSerializeADT' _Serialize _Columns htable exprs rep
88 )
89 => GSerializeADT _Serialize _Columns (M1 D meta exprs) (M1 D meta rep)
90 where
91 gfromResultADT fromResult columns =
92 case gfromResultADT' @_Serialize @_Columns @htable @exprs @rep fromResult tag columns of
93 Just rep -> M1 rep
94 _ -> error "ADT.fromColumns: mismatch between tag and data"
95 where
96 tag = (\(HIdentity (Identity a)) -> a) . hunlabel @"tag"
98 gtoResultADT toResult (M1 rep) =
99 gtoResultADT' @_Serialize @_Columns @htable @exprs @rep toResult tag (Just rep)
100 where
101 tag = hlabel @"tag" . HIdentity . Identity
104type GSerializeADT'
105 :: (Type -> Type -> Exp Constraint)
106 -> (Type -> Exp K.HTable)
107 -> K.HTable -> (Type -> Type) -> (Type -> Type) -> Constraint
108class GSerializeADT' _Serialize _Columns htable exprs rep where
109 gfromResultADT' :: context ~ Result
110 => (forall expr a proxy. Eval (_Serialize expr a)
111 => proxy expr -> Eval (_Columns expr) context -> a)
112 -> (htable Result -> Tag)
113 -> GColumnsADT' _Columns htable exprs context
114 -> Maybe (rep x)
116 gtoResultADT' :: context ~ Result
117 => (forall expr a proxy. Eval (_Serialize expr a)
118 => proxy expr -> a -> Eval (_Columns expr) context)
119 -> (Tag -> htable Result)
120 -> Maybe (rep x)
121 -> GColumnsADT' _Columns htable exprs context
123 extract :: GColumnsADT' _Columns htable exprs context -> htable context
126instance
127 ( htable' ~ GColumnsADT' _Columns htable exprs1
128 , GSerializeADT' _Serialize _Columns htable exprs1 a
129 , GSerializeADT' _Serialize _Columns htable' exprs2 b
130 )
131 => GSerializeADT' _Serialize _Columns htable (exprs1 :+: exprs2) (a :+: b)
132 where
133 gfromResultADT' fromResult f columns =
134 case ma of
135 Just a -> Just (L1 a)
136 Nothing -> R1 <$>
137 gfromResultADT' @_Serialize @_Columns @_ @exprs2 @b
138 fromResult
139 (f . extract @_Serialize @_Columns @_ @exprs1 @a)
140 columns
141 where
142 ma =
143 gfromResultADT' @_Serialize @_Columns @_ @exprs1 @a
144 fromResult
145 f
146 (extract @_Serialize @_Columns @_ @exprs2 @b columns)
148 gtoResultADT' toResult tag = \case
149 Just (L1 a) ->
150 gtoResultADT' @_Serialize @_Columns @_ @exprs2 @b
151 toResult
152 (\_ -> gtoResultADT' @_Serialize @_Columns @_ @exprs1 @a
153 toResult
154 tag
155 (Just a))
156 Nothing
157 Just (R1 b) ->
158 gtoResultADT' @_Serialize @_Columns @_ @exprs2 @b
159 toResult
160 (\tag' ->
161 gtoResultADT' @_Serialize @_Columns @_ @exprs1 @a
162 toResult
163 (\_ -> tag tag')
164 Nothing)
165 (Just b)
166 Nothing ->
167 gtoResultADT' @_Serialize @_Columns @_ @exprs2 @b
168 toResult
169 (\_ -> gtoResultADT' @_Serialize @_Columns @_ @exprs1 @a toResult tag Nothing)
170 Nothing
172 extract =
173 extract @_Serialize @_Columns @_ @exprs1 @a .
174 extract @_Serialize @_Columns @_ @exprs2 @b
177instance (meta ~ 'MetaCons label _fixity _isRecord, KnownSymbol label) =>
178 GSerializeADT' _Serialize _Columns _htable (M1 C meta U1) (M1 C meta U1)
179 where
180 gfromResultADT' _ tag columns
181 | tag columns == tag' = Just (M1 U1)
182 | otherwise = Nothing
183 where
184 tag' = Tag $ pack $ symbolVal (Proxy @label)
186 gtoResultADT' _ tag _ = tag tag'
187 where
188 tag' = Tag $ pack $ symbolVal (Proxy @label)
190 extract = id
193instance {-# OVERLAPPABLE #-}
194 ( HTable (GColumns _Columns exprs)
195 , GSerialize _Serialize _Columns exprs rep
196 , meta ~ 'MetaCons label _fixity _isRecord
197 , KnownSymbol label
198 , GColumnsADT' _Columns htable (M1 C ('MetaCons label _fixity _isRecord) exprs) ~
199 HProduct htable (HLabel label (HNullify (GColumns _Columns exprs)))
200 )
201 => GSerializeADT' _Serialize _Columns htable (M1 C meta exprs) (M1 C meta rep)
202 where
203 gfromResultADT' fromResult tag (HProduct a b)
204 | tag a == tag' =
205 M1 . gfromResult @_Serialize @_Columns @exprs @rep fromResult <$>
206 hunnullify unnullifier (hunlabel b)
207 | otherwise = Nothing
208 where
209 tag' = Tag $ pack $ symbolVal (Proxy @label)
211 gtoResultADT' toResult tag = \case
212 Nothing -> HProduct (tag tag') (hlabel (hnulls (const null)))
213 Just (M1 rep) -> HProduct (tag tag') $
214 hlabel $
215 hnullify nullifier $
216 gtoResult @_Serialize @_Columns @exprs @rep toResult rep
217 where
218 tag' = Tag $ pack $ symbolVal (Proxy @label)
220 extract (HProduct a _) = a