git.iko.soy/rel8
on b86f445 help sign in
rel8/src/Rel8/Table/ADT.hs
217 lines 6.0 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 UndecidableInstances #-}
12{-# language UndecidableSuperClasses #-}
14module Rel8.Table.ADT
15 ( ADT( ADT )
16 , ADTable, fromADT, toADT
17 , BuildableADT
18 , BuildADT, buildADT
19 , InsertADT, insertADT
20 , ConstructableADT
21 , ConstructADT, constructADT
22 , DeconstructADT, deconstructADT
23 , NameADT, nameADT
24 , AggregateADT, aggregateADT
25 , ADTRep
26 )
27where
29-- base
30import Data.Kind ( Constraint, Type )
31import Data.Proxy ( Proxy( Proxy ) )
32import Data.Type.Equality ( (:~:)( Refl ) )
33import GHC.Generics ( Generic, Rep, from, to )
34import GHC.TypeLits ( Symbol )
35import Prelude
37-- rel8
38import Rel8.Aggregate ( Aggregate )
39import Rel8.Expr ( Expr )
40import Rel8.FCF ( Eval, Exp )
41import Rel8.Generic.Construction
42 ( GGBuildable
43 , GGBuild, ggbuild
44 , GGInsert, gginsert
45 , GGConstructable
46 , GGConstruct, ggconstruct
47 , GGDeconstruct, ggdeconstruct
48 , GGName, ggname
49 , GGAggregate, ggaggregate
50 )
51import Rel8.Generic.Map ( GMappable, GMap, gmap, gunmap )
52import Rel8.Generic.Record ( GRecordable, GRecord, grecord, gunrecord )
53import Rel8.Generic.Rel8able
54 ( Rel8able
55 , GRep, GColumns, gfromColumns, gtoColumns
56 , greify, gunreify
57 )
58import qualified Rel8.Generic.Table.ADT as G
59import qualified Rel8.Kind.Algebra as K
60import Rel8.Schema.Context ( Col )
61import Rel8.Schema.HTable ( HTable )
62import Rel8.Schema.Insert ( Insert )
63import qualified Rel8.Schema.Kind as K
64import Rel8.Schema.Name ( Name )
65import Rel8.Schema.Reify ( Col( Reify ), Reify, hreify, hunreify )
66import Rel8.Schema.Result ( Result )
67import Rel8.Table
68 ( Table
69 , fromColumns, toColumns, reify, unreify
70 , TTable, TColumns, TUnreify
71 )
74type ADT :: K.Rel8able -> K.Rel8able
75newtype ADT t context = ADT (GColumnsADT t (Col context))
78instance ADTable t => Rel8able (ADT t) where
79 type GColumns (ADT t) = GColumnsADT t
81 gfromColumns = ADT
82 gtoColumns (ADT a) = a
84 greify (ADT a) = ADT (hreify a)
85 gunreify (ADT a) = ADT (hunreify a)
88instance (ADTable t, context ~ Result) => Generic (ADT t context) where
89 type Rep (ADT t context) = Rep (t context)
91 from =
92 gmap @(TTable (Reify Result)) (Proxy @TUnreify) (unreify Refl) .
93 gunrecord @(Rep (t (Reify Result))) .
94 G.gfromColumnsADT
95 @(TTable (Reify Result))
96 @TColumns
97 (\(Reify a) -> a)
98 Reify
99 fromColumns .
100 hreify .
101 (\(ADT a) -> a)
103 to =
104 ADT .
105 hunreify .
106 G.gtoColumnsADT
107 @(TTable (Reify Result))
108 @TColumns
109 (\(Reify a) -> a)
110 Reify
111 toColumns .
112 grecord @(Rep (t (Reify Result))) .
113 gunmap @(TTable (Reify Result)) (Proxy @TUnreify) (reify Refl)
116fromADT :: ADTable t => ADT t Result -> t Result
117fromADT = to . from
120toADT :: ADTable t => t Result -> ADT t Result
121toADT = to . from
124type ADTable :: K.Rel8able -> Constraint
125class
126 ( Generic (t Result)
127 , HTable (GColumnsADT t)
128 , G.GTableADT (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRecord (Rep (t (Reify Result))))
129 , GRecordable (Rep (t (Reify Result)))
130 , GMappable (TTable (Reify Result)) (Rep (t (Reify Result)))
131 , GMap TUnreify (Rep (t (Reify Result))) ~ Rep (t Result)
132 )
133 => ADTable t
134instance
135 ( Generic (t Result)
136 , HTable (GColumnsADT t)
137 , G.GTableADT (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRecord (Rep (t (Reify Result))))
138 , GRecordable (Rep (t (Reify Result)))
139 , GMappable (TTable (Reify Result)) (Rep (t (Reify Result)))
140 , GMap TUnreify (Rep (t (Reify Result))) ~ Rep (t Result)
141 )
142 => ADTable t
145type BuildableADT :: K.Rel8able -> Symbol -> Constraint
146class GGBuildable 'K.Sum name (ADTRep t) => BuildableADT t name
147instance GGBuildable 'K.Sum name (ADTRep t) => BuildableADT t name
150type BuildADT :: K.Rel8able -> Symbol -> Type
151type BuildADT t name = GGBuild 'K.Sum name (ADTRep t) (ADT t Expr)
154buildADT :: forall t name. BuildableADT t name => BuildADT t name
155buildADT =
156 ggbuild @'K.Sum @name @(ADTRep t) @(ADT t Expr) ADT
159type InsertADT :: K.Rel8able -> Symbol -> Type
160type InsertADT t name = GGInsert 'K.Sum name (ADTRep t) (ADT t Insert)
163insertADT :: forall t name. BuildableADT t name => InsertADT t name
164insertADT =
165 gginsert @'K.Sum @name @(ADTRep t) @(ADT t Insert) ADT
168type ConstructableADT :: K.Rel8able -> Constraint
169class GGConstructable 'K.Sum (ADTRep t) => ConstructableADT t
170instance GGConstructable 'K.Sum (ADTRep t) => ConstructableADT t
173type ConstructADT :: K.Rel8able -> Type
174type ConstructADT t = forall r. GGConstruct 'K.Sum (ADTRep t) r
177constructADT :: forall t. ConstructableADT t => ConstructADT t -> ADT t Expr
178constructADT f =
179 ggconstruct @'K.Sum @(ADTRep t) @(ADT t Expr) ADT
180 (f @(ADT t Expr))
183type DeconstructADT :: K.Rel8able -> Type -> Type
184type DeconstructADT t r = GGDeconstruct 'K.Sum (ADTRep t) (ADT t Expr) r
187deconstructADT :: forall t r. (ConstructableADT t, Table Expr r)
188 => DeconstructADT t r
189deconstructADT =
190 ggdeconstruct @'K.Sum @(ADTRep t) @(ADT t Expr) @r (\(ADT a) -> a)
193type NameADT :: K.Rel8able -> Type
194type NameADT t = GGName 'K.Sum (ADTRep t) (ADT t Name)
197nameADT :: forall t. ConstructableADT t => NameADT t
198nameADT = ggname @'K.Sum @(ADTRep t) @(ADT t Name) ADT
201type AggregateADT :: K.Rel8able -> Type
202type AggregateADT t = forall r. GGAggregate 'K.Sum (ADTRep t) r
205aggregateADT :: forall t. ConstructableADT t
206 => AggregateADT t -> ADT t Expr -> Aggregate (ADT t Expr)
207aggregateADT f =
208 ggaggregate @'K.Sum @(ADTRep t) @(ADT t Expr) ADT (\(ADT a) -> a)
209 (f @(Aggregate (ADT t Expr)))
212data ADTRep :: K.Rel8able -> K.Context -> Exp (Type -> Type)
213type instance Eval (ADTRep t context) = GRep t context
216type GColumnsADT :: K.Rel8able -> K.HTable
217type GColumnsADT t = G.GColumnsADT TColumns (GRep t (Reify Result))