git.iko.soy/rel8
on db148ff help sign in
rel8/src/Rel8/Generic/Table.hs
188 lines 5.5 kB history raw
1{-# language AllowAmbiguousTypes #-}
2{-# language DataKinds #-}
3{-# language FlexibleContexts #-}
4{-# language FlexibleInstances #-}
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
15 ( GGTable, GGColumns, GGContext, ggfromColumns, ggtoColumns, ggtable
16 , GGToExprs, ggfromResult, ggtoResult
17 , GAlgebra
18 )
19where
21-- base
22import Data.Kind ( Constraint, Type )
23import GHC.Generics ( (:+:), (:*:), K1, M1, U1, V1 )
24import Prelude ()
26-- rel8
27import Rel8.FCF ( Eval, Exp )
28import Rel8.Generic.Table.ADT
29 ( GTableADT, GColumnsADT, gfromColumnsADT, gtoColumnsADT, gtableADT
30 , GToExprsADT, gtoResultADT, gfromResultADT
31 )
32import Rel8.Generic.Table.Record
33 ( GTable, GColumns, GContext, gfromColumns, gtoColumns, gtable
34 , GToExprs, gtoResult, gfromResult
35 )
36import Rel8.Kind.Algebra
37 ( Algebra( Product, Sum )
38 , SAlgebra( SProduct, SSum )
39 , KnownAlgebra, algebraSing
40 )
41import Rel8.Schema.Context ( Col )
42import qualified Rel8.Schema.Kind as K
43import Rel8.Schema.Null ( Nullify )
44import Rel8.Schema.Spec ( Spec( Spec ), SSpec )
45import Rel8.Schema.Result ( Result )
48data GGTable
49 :: Algebra
50 -> (Type -> Exp Constraint)
51 -> (Type -> Exp K.HTable)
52 -> K.HContext
53 -> (Type -> Type)
54 -> Exp Constraint
57type instance Eval (GGTable 'Product _Table _Columns context rep) =
58 GTable _Table _Columns context rep
61type instance Eval (GGTable 'Sum _Table _Columns context rep) =
62 GTableADT _Table _Columns context rep
65data GGToExprs
66 :: Algebra
67 -> (Type -> Type -> Exp Constraint)
68 -> (Type -> Exp K.HTable)
69 -> (Type -> Type)
70 -> (Type -> Type)
71 -> Exp Constraint
74type instance Eval (GGToExprs 'Product _ToExprs _Columns exprs rep) =
75 GToExprs _ToExprs _Columns exprs rep
78type instance Eval (GGToExprs 'Sum _ToExprs _Columns exprs rep) =
79 GToExprsADT _ToExprs _Columns exprs rep
82data GGColumns
83 :: Algebra
84 -> (Type -> Exp K.HTable)
85 -> (Type -> Type)
86 -> Exp K.HTable
89type instance Eval (GGColumns 'Product _Columns rep) = GColumns _Columns rep
92type instance Eval (GGColumns 'Sum _Columns rep) = GColumnsADT _Columns rep
95data GGContext
96 :: Algebra
97 -> (Type -> Exp K.Context)
98 -> (Type -> Type)
99 -> Exp K.Context
102type instance Eval (GGContext 'Product _Context rep) = GContext _Context rep
105type instance Eval (GGContext 'Sum _Context _rep) = Result
108type GAlgebra :: (Type -> Type) -> Algebra
109type family GAlgebra rep where
110 GAlgebra (M1 _ _ rep) = GAlgebra rep
111 GAlgebra V1 = 'Sum
112 GAlgebra (_ :+: _) = 'Sum
113 GAlgebra U1 = 'Sum
114 GAlgebra (_ :*: _) = 'Product
115 GAlgebra (K1 _ _) = 'Product
118ggfromColumns :: forall algebra _Table _Columns rep context x.
119 ( KnownAlgebra algebra
120 , Eval (GGTable algebra _Table _Columns context rep)
121 )
122 => (forall spec. algebra ~ 'Sum => context spec -> Col Result spec)
123 -> (forall spec. algebra ~ 'Sum => Col Result spec -> context spec)
124 -> (forall a. Eval (_Table a) => Eval (_Columns a) context -> a)
125 -> Eval (GGColumns algebra _Columns rep) context
126 -> rep x
127ggfromColumns = case algebraSing @algebra of
128 SProduct -> \_ _ -> gfromColumns @_Table @_Columns
129 SSum -> gfromColumnsADT @_Table @_Columns
132ggtoColumns :: forall algebra _Table _Columns rep context x.
133 ( KnownAlgebra algebra
134 , Eval (GGTable algebra _Table _Columns context rep)
135 )
136 => (forall spec. algebra ~ 'Sum => context spec -> Col Result spec)
137 -> (forall spec. algebra ~ 'Sum => Col Result spec -> context spec)
138 -> (forall a. Eval (_Table a) => a -> Eval (_Columns a) context)
139 -> rep x
140 -> Eval (GGColumns algebra _Columns rep) context
141ggtoColumns = case algebraSing @algebra of
142 SProduct -> \_ _ -> gtoColumns @_Table @_Columns
143 SSum -> gtoColumnsADT @_Table @_Columns
146ggtable :: forall algebra _Table _Columns rep context.
147 ( KnownAlgebra algebra
148 , Eval (GGTable algebra _Table _Columns context rep)
149 )
150 => (forall a proxy. Eval (_Table a) => proxy a -> Eval (_Columns a) context)
151 -> (forall a labels necessity. ()
152 => SSpec ('Spec labels necessity a)
153 -> context ('Spec labels necessity a)
154 -> context ('Spec labels necessity (Nullify a)))
155 -> Eval (GGColumns algebra _Columns rep) context
156ggtable = case algebraSing @algebra of
157 SProduct -> \table _ -> gtable @_Table @_Columns @_ @rep table
158 SSum -> gtableADT @_Table @_Columns @_ @rep
161ggfromResult :: forall algebra _ToExprs _Columns exprs rep x.
162 ( KnownAlgebra algebra
163 , Eval (GGToExprs algebra _ToExprs _Columns exprs rep)
164 )
165 => (forall expr a proxy. Eval (_ToExprs expr a)
166 => proxy expr
167 -> Eval (_Columns expr) (Col Result)
168 -> a)
169 -> Eval (GGColumns algebra _Columns exprs) (Col Result)
170 -> rep x
171ggfromResult = case algebraSing @algebra of
172 SProduct -> gfromResult @_ToExprs @_Columns @exprs
173 SSum -> gfromResultADT @_ToExprs @_Columns @exprs
176ggtoResult :: forall algebra _ToExprs _Columns exprs rep x.
177 ( KnownAlgebra algebra
178 , Eval (GGToExprs algebra _ToExprs _Columns exprs rep)
179 )
180 => (forall expr a proxy. Eval (_ToExprs expr a)
181 => proxy expr
182 -> a
183 -> Eval (_Columns expr) (Col Result))
184 -> rep x
185 -> Eval (GGColumns algebra _Columns exprs) (Col Result)
186ggtoResult = case algebraSing @algebra of
187 SProduct -> gtoResult @_ToExprs @_Columns @exprs
188 SSum -> gtoResultADT @_ToExprs @_Columns @exprs