git.iko.soy/rel8
on db148ff help sign in
rel8/src/Rel8/Table/Rel8able.hs
148 lines 3.9 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, gfromColumns, gtoColumns
33 , greify, gunreify
34 )
35import Rel8.Schema.Context ( Col )
36import Rel8.Schema.Context.Label ( Labelable )
37import Rel8.Schema.Dict ( Dict( Dict ) )
38import qualified Rel8.Schema.Kind as K
39import Rel8.Schema.HTable ( HConstrainTable, hdicts )
40import Rel8.Schema.Reify ( hreify, hunreify, UnwrapReify )
41import Rel8.Schema.Result ( Result )
42import Rel8.Table
43 ( Table, Columns, Context, Congruent, fromColumns, toColumns
44 , Unreify, reify, unreify
45 )
46import Rel8.Schema.Spec.ConstrainDBType ( ConstrainDBType )
47import Rel8.Table.ADT ( ADT( ADT ), ADTable, fromADT, toADT )
48import Rel8.Table.Eq ( EqTable, eqTable )
49import Rel8.Table.HKD ( HKD )
50import Rel8.Table.Ord ( OrdTable, ordTable )
51import Rel8.Table.Recontextualize ( Recontextualize )
52import Rel8.Table.Serialize ( FromExprs, ToExprs, fromResult, toResult )
53import Rel8.Type.Eq ( DBEq )
54import Rel8.Type.Ord ( DBOrd )
57instance (Rel8able t, Labelable context, Reifiable context) =>
58 Table context (t context)
59 where
60 type Columns (t context) = GColumns t
61 type Context (t context) = context
62 type Unreify (t context) = t (UnwrapReify context)
64 fromColumns = gunreify . gfromColumns . hreify
65 toColumns = hunreify . gtoColumns . greify
67 reify Refl = case contextSing @context of
68 SReify context -> case sLabelable context of
69 Dict -> case sReifiable context of
70 Dict -> greify
72 unreify Refl = case contextSing @context of
73 SReify context -> case sLabelable context of
74 Dict -> case sReifiable context of
75 Dict -> gunreify
78instance
79 ( Rel8able t
80 , Labelable from, Reifiable from
81 , Labelable to, Reifiable to
82 , Congruent (t from) (t to)
83 )
84 => Recontextualize from to (t from) (t to)
87instance
88 ( context ~ Expr
89 , Rel8able t
90 , HConstrainTable (Columns (t context)) (ConstrainDBType DBEq)
91 )
92 => EqTable (t context)
93 where
94 eqTable = hdicts @(Columns (t context)) @(ConstrainDBType DBEq)
97instance
98 ( context ~ Expr
99 , Rel8able t
100 , HConstrainTable (Columns (t context)) (ConstrainDBType DBEq)
101 , HConstrainTable (Columns (t context)) (ConstrainDBType DBOrd)
102 )
103 => OrdTable (t context)
104 where
105 ordTable = hdicts @(Columns (t context)) @(ConstrainDBType DBOrd)
108type instance FromExprs (t Expr) = FromExprs' t
111instance
112 ( x ~ t' Expr
113 , result ~ Result
114 , ToExprs' (Algebra t) t' t
115 )
116 => ToExprs x (t result)
117 where
118 fromResult = fromResult' @(Algebra t) @t'
119 toResult = toResult' @(Algebra t) @t'
122type FromExprs' :: K.Rel8able -> Type
123type family FromExprs' t where
124 FromExprs' (ADT t) = t Result
125 FromExprs' (HKD a) = a
126 FromExprs' t = t Result
129type ToExprs' :: K.Algebra -> K.Rel8able -> K.Rel8able -> Constraint
130class (algebra ~ Algebra t, Rel8able t') =>
131 ToExprs' algebra t' t | algebra t -> t'
132 where
133 fromResult' :: GColumns t' (Col Result) -> t Result
134 toResult' :: t Result -> GColumns t' (Col Result)
137instance (Algebra t ~ 'K.Product, Rel8able t, t ~ t') =>
138 ToExprs' 'K.Product t' t
139 where
140 fromResult' = fromColumns
141 toResult' = toColumns
144instance (Algebra t ~ 'K.Sum, ADTable t, t' ~ ADT t) =>
145 ToExprs' 'K.Sum t' t
146 where
147 fromResult' = fromADT . ADT
148 toResult' = (\(ADT a) -> a) . toADT