git.iko.soy/rel8
on 666f0b9 help sign in
rel8/src/Rel8/Table/Rel8able.hs
169 lines 4.2 kB history raw
1{-# language DataKinds #-}
2{-# language FlexibleInstances #-}
3{-# language FunctionalDependencies #-}
4{-# language ScopedTypeVariables #-}
5{-# language StandaloneKindSignatures #-}
6{-# language TypeApplications #-}
7{-# language TypeFamilies #-}
8{-# language UndecidableInstances #-}
10{-# options_ghc -fno-warn-orphans #-}
12module Rel8.Table.Rel8able
13 (
14 )
15where
17-- base
18import Data.Kind ( Constraint, Type )
19import Data.Type.Equality ( (:~:)( Refl ) )
20import Prelude
22-- rel8
23import Rel8.Expr ( Expr )
24import qualified Rel8.Kind.Algebra as K
25import Rel8.Kind.Context
26 ( SContext( SReify )
27 , Reifiable, contextSing
28 , sLabelable, sReifiable
29 )
30import Rel8.Generic.Rel8able
31 ( Rel8able, Algebra
32 , GColumns, GContext, gfromColumns, gtoColumns
33 , gfromColumnsADT, gtoColumnsADT
34 , greify, gunreify
35 )
36import Rel8.Schema.Context ( Col )
37import Rel8.Schema.Context.Label ( Labelable )
38import Rel8.Schema.Dict ( Dict( Dict ) )
39import qualified Rel8.Schema.Kind as K
40import Rel8.Schema.HTable ( HConstrainTable, hdicts )
41import Rel8.Schema.Reify ( hreify, hunreify, UnwrapReify )
42import Rel8.Schema.Result ( Result )
43import Rel8.Table
44 ( Table, Columns, Context, Congruent, fromColumns, toColumns
45 , Unreify, reify, unreify
46 )
47import Rel8.Schema.Spec.ConstrainDBType ( ConstrainDBType )
48import Rel8.Table.ADT ( ADT )
49import Rel8.Table.Eq ( EqTable, eqTable )
50import Rel8.Table.HKD ( HKD )
51import Rel8.Table.Ord ( OrdTable, ordTable )
52import Rel8.Table.Recontextualize ( Recontextualize )
53import Rel8.Table.Serialize ( FromExprs, ToExprs, fromResult, toResult )
54import Rel8.Type.Eq ( DBEq )
55import Rel8.Type.Ord ( DBOrd )
58instance
59 ( Rel8able t
60 , GContext t context ~ context
61 , Labelable context
62 , Reifiable context
63 )
64 => Table context (t context)
65 where
66 type Columns (t context) = GColumns t
67 type Context (t context) = context
68 type Unreify (t context) = t (UnwrapReify context)
70 fromColumns = gunreify . gfromColumns . hreify
71 toColumns = hunreify . gtoColumns . greify
73 reify Refl = case contextSing @context of
74 SReify context -> case sLabelable context of
75 Dict -> case sReifiable context of
76 Dict -> greify
78 unreify Refl = case contextSing @context of
79 SReify context -> case sLabelable context of
80 Dict -> case sReifiable context of
81 Dict -> gunreify
84instance
85 ( Rel8able t
86 , Labelable from, Reifiable from, GContext t from ~ from
87 , Labelable to, Reifiable to, GContext t to ~ to
88 , Congruent (t from) (t to)
89 )
90 => Recontextualize from to (t from) (t to)
93instance
94 ( context ~ Expr
95 , Rel8able t
96 , GContext t context ~ context
97 , HConstrainTable (Columns (t context)) (ConstrainDBType DBEq)
98 )
99 => EqTable (t context)
100 where
101 eqTable = hdicts @(Columns (t context)) @(ConstrainDBType DBEq)
104instance
105 ( context ~ Expr
106 , Rel8able t
107 , GContext t context ~ context
108 , HConstrainTable (Columns (t context)) (ConstrainDBType DBEq)
109 , HConstrainTable (Columns (t context)) (ConstrainDBType DBOrd)
110 )
111 => OrdTable (t context)
112 where
113 ordTable = hdicts @(Columns (t context)) @(ConstrainDBType DBOrd)
116type instance FromExprs (t Expr) = FromExprs' t
119instance
120 ( x ~ t' Expr
121 , result ~ Result
122 , ToExprs' (Algebra t) t' t
123 )
124 => ToExprs x (t result)
125 where
126 fromResult = fromResult' @(Algebra t) @t'
127 toResult = toResult' @(Algebra t) @t'
130type FromExprs' :: K.Rel8able -> Type
131type family FromExprs' t where
132 FromExprs' (ADT t) = t Result
133 FromExprs' (HKD a) = a
134 FromExprs' t = t Result
137type ToExprs' :: K.Algebra -> K.Rel8able -> K.Rel8able -> Constraint
138class
139 ( algebra ~ Algebra t
140 , Rel8able t'
141 , GContext t' Expr ~ Expr
142 )
143 => ToExprs' algebra t' t | algebra t -> t'
144 where
145 fromResult' :: GColumns t' (Col Result) -> t Result
146 toResult' :: t Result -> GColumns t' (Col Result)
149instance
150 ( Algebra t ~ 'K.Product
151 , Rel8able t
152 , GContext t Expr ~ Expr
153 , t ~ t'
154 )
155 => ToExprs' 'K.Product t' t
156 where
157 fromResult' = fromColumns
158 toResult' = toColumns
161instance
162 ( Algebra t ~ 'K.Sum
163 , Rel8able t
164 , t' ~ ADT t
165 )
166 => ToExprs' 'K.Sum t' t
167 where
168 fromResult' = gunreify . gfromColumnsADT . hreify
169 toResult' = hunreify . gtoColumnsADT . greify