git.iko.soy/rel8
on 6c20afa help sign in
rel8/src/Rel8/Generic/Table/ADT.hs
215 lines 6.6 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 ( GADTTable (fromGADTColumns, toGADTColumns)
16 , GADTColumns
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.Table ( GTable, GColumns, fromGColumns, toGColumns )
34import Rel8.Schema.Context ( Col( Result ) )
35import Rel8.Schema.Context.Label ( labeler, unlabeler )
36import Rel8.Schema.HTable ( HTable )
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 Rel8.Schema.HTable.Type ( HType( HType ) )
41import qualified Rel8.Schema.Kind as K
42import Rel8.Schema.Result ( Result )
43import Rel8.Table ( null, nullifier, unnullifier )
44import Rel8.Type.Tag ( Tag( Tag ) )
46-- text
47import Data.Text ( pack )
50type GADTColumns
51 :: (Type -> Exp K.HTable)
52 -> (Type -> Type) -> K.HTable
53type family GADTColumns _Columns rep where
54 GADTColumns _Columns (M1 D _ rep) =
55 GADTColumns' _Columns (HLabel "tag" (HType Tag)) rep
58type GADTColumns'
59 :: (Type -> Exp K.HTable)
60 -> K.HTable -> (Type -> Type) -> K.HTable
61type family GADTColumns' _Columns htable rep where
62 GADTColumns' _Columns htable (a :+: b) =
63 GADTColumns' _Columns (GADTColumns' _Columns htable a) b
64 GADTColumns' _Columns htable (M1 C ('MetaCons _ _ _) U1) = htable
65 GADTColumns' _Columns htable (M1 C ('MetaCons label _ _) rep) =
66 HProduct htable (HLabel label (HNullify (GColumns _Columns rep)))
69type GADTTable
70 :: (Type -> Exp Constraint)
71 -> (Type -> Exp K.HTable)
72 -> (Type -> Type) -> Constraint
73class GADTTable _Table _Columns rep where
74 fromGADTColumns :: ()
75 => (forall a. Eval (_Table a) => Eval (_Columns a) (Col Result) -> a)
76 -> GADTColumns _Columns rep (Col Result)
77 -> rep x
79 toGADTColumns :: ()
80 => (forall a. Eval (_Table a) => a -> Eval (_Columns a) (Col Result))
81 -> rep x
82 -> GADTColumns _Columns rep (Col Result)
85instance
86 ( htable ~ HLabel "tag" (HType Tag)
87 , GADTTable' _Table _Columns htable rep
88 )
89 => GADTTable _Table _Columns (M1 D meta rep)
90 where
91 fromGADTColumns fromColumns columns =
92 case fromGADTColumns' @_Table @_Columns fromColumns tag columns of
93 Just rep -> M1 rep
94 _ -> error "ADT.fromColumns: mismatch between tag and data"
95 where
96 tag = (\(HType (Result a)) -> a) . hunlabel @_ @"tag" unlabeler
98 toGADTColumns toColumns (M1 rep) =
99 toGADTColumns' @_Table @_Columns toColumns tag (Just rep)
100 where
101 tag = hlabel @_ @"tag" labeler . HType . Result
104type GADTTable'
105 :: (Type -> Exp Constraint)
106 -> (Type -> Exp K.HTable)
107 -> K.HTable -> (Type -> Type) -> Constraint
108class GADTTable' _Table _Columns htable rep where
109 fromGADTColumns' :: ()
110 => (forall a. Eval (_Table a) => Eval (_Columns a) (Col Result) -> a)
111 -> (htable (Col Result) -> Tag)
112 -> GADTColumns' _Columns htable rep (Col Result)
113 -> Maybe (rep x)
115 toGADTColumns' :: ()
116 => (forall a. Eval (_Table a) => a -> Eval (_Columns a) (Col Result))
117 -> (Tag -> htable (Col Result))
118 -> Maybe (rep x)
119 -> GADTColumns' _Columns htable rep (Col Result)
121 extract :: GADTColumns' _Columns htable rep context -> htable context
124instance
125 ( htable' ~ GADTColumns' _Columns htable a
126 , GADTTable' _Table _Columns htable a
127 , GADTTable' _Table _Columns htable' b
128 )
129 => GADTTable' _Table _Columns htable (a :+: b)
130 where
131 fromGADTColumns' fromColumns f columns =
132 case ma of
133 Just a -> Just (L1 a)
134 Nothing -> R1 <$>
135 fromGADTColumns' @_Table @_Columns @_ @b
136 fromColumns
137 (f . extract @_Table @_Columns @_ @a)
138 columns
139 where
140 ma =
141 fromGADTColumns' @_Table @_Columns @_ @a
142 fromColumns
143 f
144 (extract @_Table @_Columns @_ @b columns)
146 toGADTColumns' toColumns tag = \case
147 Just (L1 a) ->
148 toGADTColumns' @_Table @_Columns @_ @b
149 toColumns
150 (\_ -> toGADTColumns' @_Table @_Columns @_ @a
151 toColumns
152 tag
153 (Just a))
154 Nothing
155 Just (R1 b) ->
156 toGADTColumns' @_Table @_Columns @_ @b
157 toColumns
158 (\tag' ->
159 toGADTColumns' @_Table @_Columns @_ @a
160 toColumns
161 (\_ -> tag tag')
162 Nothing)
163 (Just b)
164 Nothing ->
165 toGADTColumns' @_Table @_Columns @_ @b
166 toColumns
167 (\_ -> toGADTColumns' @_Table @_Columns @_ @a toColumns tag Nothing)
168 Nothing
170 extract = extract @_Table @_Columns @_ @a . extract @_Table @_Columns @_ @b
173instance KnownSymbol label =>
174 GADTTable' _Table _Columns htable (M1 C ('MetaCons label _fixity _isRecord) U1)
175 where
176 fromGADTColumns' _ tag columns
177 | tag columns == tag' = Just (M1 U1)
178 | otherwise = Nothing
179 where
180 tag' = Tag $ pack $ symbolVal (Proxy @label)
182 toGADTColumns' _ tag _ = tag tag'
183 where
184 tag' = Tag $ pack $ symbolVal (Proxy @label)
186 extract = id
189instance {-# OVERLAPPABLE #-}
190 ( HTable (GColumns _Columns rep)
191 , GTable _Table _Columns (Col Result) rep
192 , KnownSymbol label
193 , GADTColumns' _Columns htable (M1 C ('MetaCons label _fixity _isRecord) rep) ~
194 HProduct htable (HLabel label (HNullify (GColumns _Columns rep)))
195 )
196 => GADTTable' _Table _Columns htable (M1 C ('MetaCons label _fixity _isRecord) rep)
197 where
198 fromGADTColumns' fromColumns tag (HProduct a b)
199 | tag a == tag' =
200 M1 . fromGColumns @_Table @_Columns fromColumns <$>
201 hunnullify unnullifier (hunlabel unlabeler b)
202 | otherwise = Nothing
203 where
204 tag' = Tag $ pack $ symbolVal (Proxy @label)
206 toGADTColumns' toColumns tag = \case
207 Nothing -> HProduct (tag tag') (hlabel labeler (hnulls null))
208 Just (M1 rep) -> HProduct (tag tag') $
209 hlabel labeler $
210 hnullify nullifier $
211 toGColumns @_Table @_Columns toColumns rep
212 where
213 tag' = Tag $ pack $ symbolVal (Proxy @label)
215 extract (HProduct a _) = a