git.iko.soy/rel8
on 97d89cf help sign in
rel8/src/Rel8/Table/ADT.hs
185 lines 5.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 TypeFamilyDependencies #-}
12{-# language UndecidableInstances #-}
13{-# language UndecidableSuperClasses #-}
15module Rel8.Table.ADT
16 ( ADT( ADT )
17 , ADTable
18 , BuildableADT
19 , BuildADT, buildADT
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 GHC.Generics ( Generic, Rep, from, to )
32import GHC.TypeLits ( Symbol )
33import Prelude
35-- rel8
36import Rel8.Aggregate ( Aggregate )
37import Rel8.Expr ( Expr )
38import Rel8.FCF ( Eval, Exp )
39import Rel8.Generic.Construction
40 ( GGBuildable
41 , GGBuild, ggbuild
42 , GGConstructable
43 , GGConstruct, ggconstruct
44 , GGDeconstruct, ggdeconstruct
45 , GGName, ggname
46 , GGAggregate, ggaggregate
47 )
48import Rel8.Generic.Map ( GMap )
49import Rel8.Generic.Record ( Record( Record ), unrecord )
50import Rel8.Generic.Rel8able
51 ( Rel8able
52 , GRep, GColumns, gfromColumns, gtoColumns
53 , GFromExprs, gfromResult, gtoResult
54 )
55import qualified Rel8.Generic.Table.ADT as G
56import qualified Rel8.Kind.Algebra as K
57import Rel8.Schema.Context.Virtual
58import Rel8.Schema.HTable ( HTable )
59import qualified Rel8.Schema.Kind as K
60import Rel8.Schema.Name ( Name )
61import Rel8.Schema.Result ( Result )
62import Rel8.Table
63 ( Table, fromResult, toResult
64 , TTable, TColumns, TFromExprs
65 )
68type ADT :: K.Rel8able -> K.Rel8able
69newtype ADT t context = ADT (GColumnsADT t context)
72instance ADTable t => Rel8able (ADT t) where
73 type GColumns (ADT t) = GColumnsADT t
74 type GFromExprs (ADT t) = t Result
76 gfromColumns VAggregate = ADT
77 gfromColumns VExpr = ADT
78 gfromColumns VName = ADT
80 gtoColumns VAggregate (ADT a) = a
81 gtoColumns VExpr (ADT a) = a
82 gtoColumns VName (ADT a) = a
84 gfromResult =
85 unrecord .
86 to .
87 G.gfromResultADT
88 @(TTable Expr)
89 @TColumns
90 @TFromExprs
91 @(Eval (ADTRep t Expr))
92 (\(_ :: proxy x) -> fromResult @_ @x)
94 gtoResult =
95 G.gtoResultADT
96 @(TTable Expr)
97 @TColumns
98 @TFromExprs
99 @(Eval (ADTRep t Expr))
100 (\(_ :: proxy x) -> toResult @_ @x) .
101 from .
102 Record
105type ADTable :: K.Rel8able -> Constraint
106class
107 ( Generic (Record (t Result))
108 , HTable (GColumnsADT t)
109 , G.GTableADT (TTable Expr) TColumns TFromExprs (Eval (ADTRep t Expr))
110 , GMap TFromExprs (Rep (Record (t Expr))) ~ Rep (Record (t Result))
111 )
112 => ADTable t
113instance
114 ( Generic (Record (t Result))
115 , HTable (GColumnsADT t)
116 , G.GTableADT (TTable Expr) TColumns TFromExprs (Eval (ADTRep t Expr))
117 , GMap TFromExprs (Rep (Record (t Expr))) ~ Rep (Record (t Result))
118 )
119 => ADTable t
122type BuildableADT :: K.Rel8able -> Symbol -> Constraint
123class GGBuildable 'K.Sum name (ADTRep t) => BuildableADT t name
124instance GGBuildable 'K.Sum name (ADTRep t) => BuildableADT t name
127type BuildADT :: K.Rel8able -> Symbol -> Type
128type BuildADT t name = GGBuild 'K.Sum name (ADTRep t) (ADT t Expr)
131buildADT :: forall t name. BuildableADT t name => BuildADT t name
132buildADT =
133 ggbuild @'K.Sum @name @(ADTRep t) @(ADT t Expr) ADT
136type ConstructableADT :: K.Rel8able -> Constraint
137class GGConstructable 'K.Sum (ADTRep t) => ConstructableADT t
138instance GGConstructable 'K.Sum (ADTRep t) => ConstructableADT t
141type ConstructADT :: K.Rel8able -> Type
142type ConstructADT t = forall r. GGConstruct 'K.Sum (ADTRep t) r
145constructADT :: forall t. ConstructableADT t => ConstructADT t -> ADT t Expr
146constructADT f =
147 ggconstruct @'K.Sum @(ADTRep t) @(ADT t Expr) ADT
148 (f @(ADT t Expr))
151type DeconstructADT :: K.Rel8able -> Type -> Type
152type DeconstructADT t r = GGDeconstruct 'K.Sum (ADTRep t) (ADT t Expr) r
155deconstructADT :: forall t r. (ConstructableADT t, Table Expr r)
156 => DeconstructADT t r
157deconstructADT =
158 ggdeconstruct @'K.Sum @(ADTRep t) @(ADT t Expr) @r (\(ADT a) -> a)
161type NameADT :: K.Rel8able -> Type
162type NameADT t = GGName 'K.Sum (ADTRep t) (ADT t Name)
165nameADT :: forall t. ConstructableADT t => NameADT t
166nameADT = ggname @'K.Sum @(ADTRep t) @(ADT t Name) ADT
169type AggregateADT :: K.Rel8able -> Type
170type AggregateADT t = forall r. GGAggregate 'K.Sum (ADTRep t) r
173aggregateADT :: forall t. ConstructableADT t
174 => AggregateADT t -> ADT t Expr -> ADT t Aggregate
175aggregateADT f =
176 ggaggregate @'K.Sum @(ADTRep t) @(ADT t Expr) @(ADT t Aggregate) ADT (\(ADT a) -> a)
177 (f @(ADT t Aggregate))
180data ADTRep :: K.Rel8able -> K.Context -> Exp (Type -> Type)
181type instance Eval (ADTRep t context) = GRep t context
184type GColumnsADT :: K.Rel8able -> K.HTable
185type GColumnsADT t = G.GColumnsADT TColumns (GRep t Expr)