git.iko.soy/rel8
on e48c73e help sign in
rel8/src/Rel8/Table/ADT.hs
193 lines 5.4 kB history raw
1{-# language AllowAmbiguousTypes #-}
2{-# language DataKinds #-}
3{-# language FlexibleContexts #-}
4{-# language FlexibleInstances #-}
5{-# language RankNTypes #-}
6{-# language ScopedTypeVariables #-}
7{-# language StandaloneKindSignatures #-}
8{-# language TypeApplications #-}
9{-# language TypeFamilies #-}
10{-# language UndecidableInstances #-}
11{-# language UndecidableSuperClasses #-}
13module Rel8.Table.ADT
14 ( ADT( ADT )
15 , ADTable, fromADT, toADT
16 , ConstructableADT
17 , ConstructADT, constructADT
18 , DeconstructADT, deconstructADT
19 , InsertADT, insertADT
20 , NameADT, nameADT
21 , AggregateADT, aggregateADT
22 , ADTRep
23 )
24where
26-- base
27import Data.Kind ( Constraint, Type )
28import Data.Proxy ( Proxy( Proxy ) )
29import Data.Type.Equality ( (:~:)( Refl ) )
30import GHC.Generics ( Generic, Rep, from, to )
31import Prelude
33-- rel8
34import Rel8.Aggregate ( Aggregate )
35import Rel8.Expr ( Expr )
36import Rel8.FCF ( Eval, Exp )
37import Rel8.Generic.Construction
38 ( GGConstructable
39 , GGConstruct, ggconstruct
40 , GGDeconstruct, ggdeconstruct
41 , GGInsert, gginsert
42 , GGName, ggname
43 , GGAggregate, ggaggregate
44 )
45import Rel8.Generic.Map ( GMappable, GMap, gmap, gunmap )
46import Rel8.Generic.Record ( GRecordable, GRecord, grecord, gunrecord )
47import Rel8.Generic.Rel8able
48 ( Rel8able
49 , GRep, GColumns, gfromColumns, gtoColumns
50 , greify, gunreify
51 )
52import qualified Rel8.Generic.Table.ADT as G
53import qualified Rel8.Kind.Algebra as K
54import Rel8.Schema.Context ( Col )
55import Rel8.Schema.HTable ( HTable )
56import Rel8.Schema.Insert ( Insert )
57import qualified Rel8.Schema.Kind as K
58import Rel8.Schema.Name ( Name )
59import Rel8.Schema.Reify ( Col( Reify ), Reify, hreify, hunreify )
60import Rel8.Schema.Result ( Result )
61import Rel8.Table
62 ( Table
63 , fromColumns, toColumns, reify, unreify
64 , TTable, TColumns, TUnreify
65 )
68type ADT :: K.Rel8able -> K.Rel8able
69newtype ADT t context = ADT (GColumnsADT t (Col context))
72instance ADTable t => Rel8able (ADT t) where
73 type GColumns (ADT t) = GColumnsADT t
75 gfromColumns = ADT
76 gtoColumns (ADT a) = a
78 greify (ADT a) = ADT (hreify a)
79 gunreify (ADT a) = ADT (hunreify a)
82instance (ADTable t, context ~ Result) => Generic (ADT t context) where
83 type Rep (ADT t context) = Rep (t context)
85 from =
86 gmap @(TTable (Reify Result)) (Proxy @TUnreify) (unreify Refl) .
87 gunrecord @(Rep (t (Reify Result))) .
88 G.gfromColumnsADT
89 @(TTable (Reify Result))
90 @TColumns
91 (\(Reify a) -> a)
92 Reify
93 fromColumns .
94 hreify .
95 (\(ADT a) -> a)
97 to =
98 ADT .
99 hunreify .
100 G.gtoColumnsADT
101 @(TTable (Reify Result))
102 @TColumns
103 (\(Reify a) -> a)
104 Reify
105 toColumns .
106 grecord @(Rep (t (Reify Result))) .
107 gunmap @(TTable (Reify Result)) (Proxy @TUnreify) (reify Refl)
110fromADT :: ADTable t => ADT t Result -> t Result
111fromADT = to . from
114toADT :: ADTable t => t Result -> ADT t Result
115toADT = to . from
118type ADTable :: K.Rel8able -> Constraint
119class
120 ( Generic (t Result)
121 , HTable (GColumnsADT t)
122 , G.GTableADT (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRecord (Rep (t (Reify Result))))
123 , GRecordable (Rep (t (Reify Result)))
124 , GMappable (TTable (Reify Result)) (Rep (t (Reify Result)))
125 , GMap TUnreify (Rep (t (Reify Result))) ~ Rep (t Result)
126 )
127 => ADTable t
128instance
129 ( Generic (t Result)
130 , HTable (GColumnsADT t)
131 , G.GTableADT (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRecord (Rep (t (Reify Result))))
132 , GRecordable (Rep (t (Reify Result)))
133 , GMappable (TTable (Reify Result)) (Rep (t (Reify Result)))
134 , GMap TUnreify (Rep (t (Reify Result))) ~ Rep (t Result)
135 )
136 => ADTable t
139type ConstructableADT :: K.Rel8able -> Constraint
140class GGConstructable 'K.Sum (ADTRep t) => ConstructableADT t
141instance GGConstructable 'K.Sum (ADTRep t) => ConstructableADT t
144type ConstructADT :: K.Rel8able -> Type
145type ConstructADT t = GGConstruct 'K.Sum (ADTRep t) (ADT t Expr)
148constructADT :: forall t. ConstructableADT t => ConstructADT t
149constructADT = ggconstruct @'K.Sum @(ADTRep t) @(ADT t Expr) ADT
152type DeconstructADT :: K.Rel8able -> Type -> Type
153type DeconstructADT t r = GGDeconstruct 'K.Sum (ADTRep t) (ADT t Expr) r
156deconstructADT :: forall t r. (ConstructableADT t, Table Expr r)
157 => DeconstructADT t r
158deconstructADT = ggdeconstruct @'K.Sum @(ADTRep t) @(ADT t Expr) @r (\(ADT a) -> a)
161type InsertADT :: K.Rel8able -> Type
162type InsertADT t = GGInsert 'K.Sum (ADTRep t) (ADT t Insert)
165insertADT :: forall t. ConstructableADT t => InsertADT t
166insertADT = gginsert @'K.Sum @(ADTRep t) @(ADT t Insert) ADT
169type NameADT :: K.Rel8able -> Type
170type NameADT t = GGName 'K.Sum (ADTRep t) (ADT t Name)
173nameADT :: forall t. ConstructableADT t => NameADT t
174nameADT = ggname @'K.Sum @(ADTRep t) @(ADT t Name) ADT
177type AggregateADT :: K.Rel8able -> Type
178type AggregateADT t = forall r. GGAggregate 'K.Sum (ADTRep t) r
181aggregateADT :: forall t. ConstructableADT t
182 => AggregateADT t -> ADT t Expr -> Aggregate (ADT t Expr)
183aggregateADT f =
184 ggaggregate @'K.Sum @(ADTRep t) @(ADT t Expr) ADT (\(ADT a) -> a)
185 (f @(Aggregate (ADT t Expr)))
188data ADTRep :: K.Rel8able -> K.Context -> Exp (Type -> Type)
189type instance Eval (ADTRep t context) = GRep t context
192type GColumnsADT :: K.Rel8able -> K.HTable
193type GColumnsADT t = G.GColumnsADT TColumns (GRep t (Reify Result))