on b86acbd help sign in
rel8/src/Rel8/Column/NonEmpty.hs
145 lines 4.7 kB history raw
1{-# language DataKinds #-}
2{-# language FlexibleContexts #-}
3{-# language LambdaCase #-}
4{-# language MultiParamTypeClasses #-}
5{-# language StandaloneKindSignatures #-}
6{-# language TypeFamilies #-}
7{-# language UndecidableInstances #-}
9module Rel8.Column.NonEmpty
10 ( HNonEmpty, AHNonEmpty(..)
11 )
12where
14-- base
15import Data.Kind ( Type )
16import Data.List.NonEmpty ( NonEmpty )
17import Data.Type.Equality ( (:~:)( Refl ) )
18import Prelude
20-- rel8
21import Rel8.Aggregate ( Aggregate )
22import Rel8.Expr ( Expr )
23import Rel8.Kind.Context ( SContext(..), Reifiable( contextSing ) )
24import Rel8.Schema.Context ( Col )
25import Rel8.Schema.HTable.NonEmpty ( HNonEmptyTable )
26import qualified Rel8.Schema.Kind as K
27import Rel8.Schema.Name ( Name )
28import Rel8.Schema.Reify ( Reify, hreify, hunreify )
29import Rel8.Schema.Result ( Result )
30import Rel8.Table
31 ( Table, Columns, Congruent, Context, fromColumns, toColumns
32 , Unreify, reify, unreify
33 )
34import Rel8.Table.NonEmpty ( NonEmptyTable( NonEmptyTable ) )
35import Rel8.Table.Recontextualize ( Recontextualize )
36import Rel8.Table.Unreify ( Unreifiability(..), Unreifiable, unreifiability )
39type HNonEmpty :: K.Context -> Type -> Type
40type family HNonEmpty context where
41 HNonEmpty (Reify context) = AHNonEmpty context
42 HNonEmpty Aggregate = NonEmptyTable
43 HNonEmpty Expr = NonEmptyTable
44 HNonEmpty Name = NonEmptyTable
45 HNonEmpty Result = NonEmpty
48type AHNonEmpty :: K.Context -> Type -> Type
49newtype AHNonEmpty context a = AHNonEmpty (HNonEmpty context a)
52instance (Reifiable context, Unreifiable a, Table (Reify context) a) =>
53 Table (Reify context) (AHNonEmpty context a)
54 where
55 type Context (AHNonEmpty context a) = Reify context
56 type Columns (AHNonEmpty context a) = HNonEmptyTable (Columns a)
57 type Unreify (AHNonEmpty context a) = HNonEmpty context (Unreify a)
59 fromColumns = sfromColumnsNonEmpty contextSing
60 toColumns = stoColumnsNonEmpty contextSing
62 reify _ = sreifyNonEmpty (unreifiability contextSing)
63 unreify _ = sunreifyNonEmpty (unreifiability contextSing)
66instance
67 ( Reifiable context, Reifiable context'
68 , Unreifiable a, Unreifiable a'
69 , Recontextualize (Reify context) (Reify context') a a'
70 )
71 => Recontextualize
72 (Reify context)
73 (Reify context')
74 (AHNonEmpty context a)
75 (AHNonEmpty context' a')
78smapNonEmpty :: Congruent a b
79 => SContext context
80 -> (a -> b)
81 -> (HNonEmptyTable (Columns a) (Col (Context a)) -> HNonEmptyTable (Columns b) (Col (Context b)))
82 -> AHNonEmpty context a
83 -> AHNonEmpty context b
84smapNonEmpty = \case
85 SAggregate -> \_ f (AHNonEmpty (NonEmptyTable a)) -> AHNonEmpty (NonEmptyTable (f a))
86 SExpr -> \_ f (AHNonEmpty (NonEmptyTable a)) -> AHNonEmpty (NonEmptyTable (f a))
87 SResult -> \f _ (AHNonEmpty as) -> AHNonEmpty (fmap f as)
88 SName -> \_ f (AHNonEmpty (NonEmptyTable a)) -> AHNonEmpty (NonEmptyTable (f a))
89 SReify context -> \f g (AHNonEmpty as) -> AHNonEmpty (smapNonEmpty context f g as)
92sfromColumnsNonEmpty :: Table (Reify context) a
93 => SContext context
94 -> HNonEmptyTable (Columns a) (Col (Reify context))
95 -> AHNonEmpty context a
96sfromColumnsNonEmpty = \case
97 SAggregate -> AHNonEmpty . NonEmptyTable
98 SExpr -> AHNonEmpty . NonEmptyTable
99 SResult ->
100 AHNonEmpty . fmap (fromColumns . hreify) . fromColumns . hunreify
101 SName -> AHNonEmpty . NonEmptyTable
102 SReify context ->
103 AHNonEmpty .
104 smapNonEmpty context (fromColumns . hreify) hreify .
105 sfromColumnsNonEmpty context .
106 hunreify
109stoColumnsNonEmpty :: Table (Reify context) a
110 => SContext context
111 -> AHNonEmpty context a
112 -> HNonEmptyTable (Columns a) (Col (Reify context))
113stoColumnsNonEmpty = \case
114 SAggregate -> \(AHNonEmpty (NonEmptyTable a)) -> a
115 SExpr -> \(AHNonEmpty (NonEmptyTable a)) -> a
116 SResult ->
117 hreify . toColumns . fmap (hunreify . toColumns) . (\(AHNonEmpty a) -> a)
118 SName -> \(AHNonEmpty (NonEmptyTable a)) -> a
119 SReify context ->
120 hreify .
121 stoColumnsNonEmpty context .
122 smapNonEmpty context (hunreify . toColumns) hunreify .
123 (\(AHNonEmpty a) -> a)
126sreifyNonEmpty :: Table (Reify context) a
127 => Unreifiability context a
128 -> HNonEmpty context (Unreify a)
129 -> AHNonEmpty context a
130sreifyNonEmpty = \case
131 UResult -> AHNonEmpty . fmap (reify Refl)
132 Unreifiability context ->
133 smapNonEmpty context (reify Refl) hreify .
134 AHNonEmpty
137sunreifyNonEmpty :: Table (Reify context) a
138 => Unreifiability context a
139 -> AHNonEmpty context a
140 -> HNonEmpty context (Unreify a)
141sunreifyNonEmpty = \case
142 UResult -> fmap (unreify Refl) . (\(AHNonEmpty a) -> a)
143 Unreifiability context ->
144 (\(AHNonEmpty a) -> a) .
145 smapNonEmpty context (unreify Refl) hunreify