@@ -0,0 +1,215 @@
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 #-}
13+
14+module Rel8.Generic.Table.ADT
15+ ( GADTTable (fromGADTColumns, toGADTColumns)
16+ , GADTColumns
17+ )
18+where
19+
20+-- base
21+import Data.Kind ( Constraint, Type )
22+import Data.Proxy ( Proxy( Proxy ) )
23+import GHC.Generics
24+ ( (:+:)( L1, R1 ), M1( M1 ), U1( U1 )
25+ , C, D
26+ , Meta( MetaCons )
27+ )
28+import GHC.TypeLits ( KnownSymbol, symbolVal )
29+import Prelude hiding ( null )
30+
31+-- rel8
32+import Rel8.FCF ( Eval, Exp )
33+import Rel8.Generic.Table ( GTable, GColumns, fromGColumns, toGColumns )
34+import Rel8.Schema.Context ( Col( Result ) )
35+import Rel8.Schema.Context.Label ( labeler, unlabeler )
36+import Rel8.Schema.HTable ( HTable )
37+import Rel8.Schema.HTable.Label ( HLabel, hlabel, hunlabel )
38+import Rel8.Schema.HTable.Nullify ( HNullify, hnulls, hnullify, hunnullify )
39+import Rel8.Schema.HTable.Product ( HProduct( HProduct ) )
40+import Rel8.Schema.HTable.Type ( HType( HType ) )
41+import qualified Rel8.Schema.Kind as K
42+import Rel8.Schema.Result ( Result )
43+import Rel8.Table ( null, nullifier, unnullifier )
44+import Rel8.Type.Tag ( Tag( Tag ) )
45+
46+-- text
47+import Data.Text ( pack )
48+
49+
50+type GADTColumns
51+ :: (Type -> Exp K.HTable)
52+ -> (Type -> Type) -> K.HTable
53+type family GADTColumns _Columns rep where
54+ GADTColumns _Columns (M1 D _ rep) =
55+ GADTColumns' _Columns (HLabel "tag" (HType Tag)) rep
56+
57+
58+type GADTColumns'
59+ :: (Type -> Exp K.HTable)
60+ -> K.HTable -> (Type -> Type) -> K.HTable
61+type 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)))
67+
68+
69+type GADTTable
70+ :: (Type -> Exp Constraint)
71+ -> (Type -> Exp K.HTable)
72+ -> (Type -> Type) -> Constraint
73+class 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
78+
79+ toGADTColumns :: ()
80+ => (forall a. Eval (_Table a) => a -> Eval (_Columns a) (Col Result))
81+ -> rep x
82+ -> GADTColumns _Columns rep (Col Result)
83+
84+
85+instance
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
97+
98+ toGADTColumns toColumns (M1 rep) =
99+ toGADTColumns' @_Table @_Columns toColumns tag (Just rep)
100+ where
101+ tag = hlabel @_ @"tag" labeler . HType . Result
102+
103+
104+type GADTTable'
105+ :: (Type -> Exp Constraint)
106+ -> (Type -> Exp K.HTable)
107+ -> K.HTable -> (Type -> Type) -> Constraint
108+class 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)
114+
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)
120+
121+ extract :: GADTColumns' _Columns htable rep context -> htable context
122+
123+
124+instance
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)
145+
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
169+
170+ extract = extract @_Table @_Columns @_ @a . extract @_Table @_Columns @_ @b
171+
172+
173+instance 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)
181+
182+ toGADTColumns' _ tag _ = tag tag'
183+ where
184+ tag' = Tag $ pack $ symbolVal (Proxy @label)
185+
186+ extract = id
187+
188+
189+instance {-# 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)
205+
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)
214+
215+ extract (HProduct a _) = a