git.iko.soy/rel8
on da86165 help sign in
rel8/src/Rel8/Table/ADT.hs
205 lines 5.7 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 , ConstructableADT
20 , ConstructADT, constructADT
21 , DeconstructADT, deconstructADT
22 , NameADT, nameADT
23 , AggregateADT, aggregateADT
24 , ADTRep
25 )
26where
28-- base
29import Data.Kind ( Constraint, Type )
30import Data.Proxy ( Proxy( Proxy ) )
31import Data.Type.Equality ( (:~:)( Refl ) )
32import GHC.Generics ( Generic, Rep, from, to )
33import GHC.TypeLits ( Symbol )
34import Prelude
36-- rel8
37import Rel8.Aggregate ( Aggregate )
38import Rel8.Expr ( Expr )
39import Rel8.FCF ( Eval, Exp )
40import Rel8.Generic.Construction
41 ( GGBuildable
42 , GGBuild, ggbuild
43 , GGConstructable
44 , GGConstruct, ggconstruct
45 , GGDeconstruct, ggdeconstruct
46 , GGName, ggname
47 , GGAggregate, ggaggregate
48 )
49import Rel8.Generic.Map ( GMappable, GMap, gmap, gunmap )
50import Rel8.Generic.Record ( GRecordable, GRecord, grecord, gunrecord )
51import Rel8.Generic.Rel8able
52 ( Rel8able
53 , GRep, GColumns, gfromColumns, gtoColumns
54 , greify, gunreify
55 )
56import qualified Rel8.Generic.Table.ADT as G
57import qualified Rel8.Kind.Algebra as K
58import Rel8.Schema.Context ( Col )
59import Rel8.Schema.HTable ( HTable )
60import qualified Rel8.Schema.Kind as K
61import Rel8.Schema.Name ( Name )
62import Rel8.Schema.Reify ( Col( Reify ), Reify, hreify, hunreify )
63import Rel8.Schema.Result ( Result )
64import Rel8.Table
65 ( Table
66 , fromColumns, toColumns, reify, unreify
67 , TTable, TColumns, TUnreify
68 )
71type ADT :: K.Rel8able -> K.Rel8able
72newtype ADT t context = ADT (GColumnsADT t (Col context))
75instance ADTable t => Rel8able (ADT t) where
76 type GColumns (ADT t) = GColumnsADT t
78 gfromColumns = ADT
79 gtoColumns (ADT a) = a
81 greify (ADT a) = ADT (hreify a)
82 gunreify (ADT a) = ADT (hunreify a)
85instance (ADTable t, context ~ Result) => Generic (ADT t context) where
86 type Rep (ADT t context) = Rep (t context)
88 from =
89 gmap @(TTable (Reify Result)) (Proxy @TUnreify) (unreify Refl) .
90 gunrecord @(Rep (t (Reify Result))) .
91 G.gfromColumnsADT
92 @(TTable (Reify Result))
93 @TColumns
94 (\(Reify a) -> a)
95 Reify
96 fromColumns .
97 hreify .
98 (\(ADT a) -> a)
100 to =
101 ADT .
102 hunreify .
103 G.gtoColumnsADT
104 @(TTable (Reify Result))
105 @TColumns
106 (\(Reify a) -> a)
107 Reify
108 toColumns .
109 grecord @(Rep (t (Reify Result))) .
110 gunmap @(TTable (Reify Result)) (Proxy @TUnreify) (reify Refl)
113fromADT :: ADTable t => ADT t Result -> t Result
114fromADT = to . from
117toADT :: ADTable t => t Result -> ADT t Result
118toADT = to . from
121type ADTable :: K.Rel8able -> Constraint
122class
123 ( Generic (t Result)
124 , HTable (GColumnsADT t)
125 , G.GTableADT (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRecord (Rep (t (Reify Result))))
126 , GRecordable (Rep (t (Reify Result)))
127 , GMappable (TTable (Reify Result)) (Rep (t (Reify Result)))
128 , GMap TUnreify (Rep (t (Reify Result))) ~ Rep (t Result)
129 )
130 => ADTable t
131instance
132 ( Generic (t Result)
133 , HTable (GColumnsADT t)
134 , G.GTableADT (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRecord (Rep (t (Reify Result))))
135 , GRecordable (Rep (t (Reify Result)))
136 , GMappable (TTable (Reify Result)) (Rep (t (Reify Result)))
137 , GMap TUnreify (Rep (t (Reify Result))) ~ Rep (t Result)
138 )
139 => ADTable t
142type BuildableADT :: K.Rel8able -> Symbol -> Constraint
143class GGBuildable 'K.Sum name (ADTRep t) => BuildableADT t name
144instance GGBuildable 'K.Sum name (ADTRep t) => BuildableADT t name
147type BuildADT :: K.Rel8able -> Symbol -> Type
148type BuildADT t name = GGBuild 'K.Sum name (ADTRep t) (ADT t Expr)
151buildADT :: forall t name. BuildableADT t name => BuildADT t name
152buildADT =
153 ggbuild @'K.Sum @name @(ADTRep t) @(ADT t Expr) ADT
156type ConstructableADT :: K.Rel8able -> Constraint
157class GGConstructable 'K.Sum (ADTRep t) => ConstructableADT t
158instance GGConstructable 'K.Sum (ADTRep t) => ConstructableADT t
161type ConstructADT :: K.Rel8able -> Type
162type ConstructADT t = forall r. GGConstruct 'K.Sum (ADTRep t) r
165constructADT :: forall t. ConstructableADT t => ConstructADT t -> ADT t Expr
166constructADT f =
167 ggconstruct @'K.Sum @(ADTRep t) @(ADT t Expr) ADT
168 (f @(ADT t Expr))
171type DeconstructADT :: K.Rel8able -> Type -> Type
172type DeconstructADT t r = GGDeconstruct 'K.Sum (ADTRep t) (ADT t Expr) r
175deconstructADT :: forall t r. (ConstructableADT t, Table Expr r)
176 => DeconstructADT t r
177deconstructADT =
178 ggdeconstruct @'K.Sum @(ADTRep t) @(ADT t Expr) @r (\(ADT a) -> a)
181type NameADT :: K.Rel8able -> Type
182type NameADT t = GGName 'K.Sum (ADTRep t) (ADT t Name)
185nameADT :: forall t. ConstructableADT t => NameADT t
186nameADT = ggname @'K.Sum @(ADTRep t) @(ADT t Name) ADT
189type AggregateADT :: K.Rel8able -> Type
190type AggregateADT t = forall r. GGAggregate 'K.Sum (ADTRep t) r
193aggregateADT :: forall t. ConstructableADT t
194 => AggregateADT t -> ADT t Expr -> ADT t Aggregate
195aggregateADT f =
196 ggaggregate @'K.Sum @(ADTRep t) @(ADT t Expr) @(ADT t Aggregate) ADT (\(ADT a) -> a)
197 (f @(ADT t Aggregate))
200data ADTRep :: K.Rel8able -> K.Context -> Exp (Type -> Type)
201type instance Eval (ADTRep t context) = GRep t context
204type GColumnsADT :: K.Rel8able -> K.HTable
205type GColumnsADT t = G.GColumnsADT TColumns (GRep t (Reify Result))