-
Notifications
You must be signed in to change notification settings - Fork 38
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Move FromExprs into the Table class and get rid of Unreify (#106)
- Loading branch information
1 parent
5a47018
commit 7c5422f
Showing
47 changed files
with
866 additions
and
2,988 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,117 +1,36 @@ | ||
| {-# language DataKinds #-} | ||
| {-# language FlexibleContexts #-} | ||
| {-# language LambdaCase #-} | ||
| {-# language MultiParamTypeClasses #-} | ||
| {-# language ScopedTypeVariables #-} | ||
| {-# language StandaloneKindSignatures #-} | ||
| {-# language TypeApplications #-} | ||
| {-# language TypeFamilies #-} | ||
|
|
||
| module Rel8.Column | ||
| ( Column, AColumn(..) | ||
| ( Column | ||
| , TColumn | ||
| ) | ||
| where | ||
|
|
||
| -- base | ||
| import Data.Kind ( Type ) | ||
| import Data.Type.Equality ( (:~:)( Refl ) ) | ||
| import Prelude | ||
| import Prelude () | ||
|
|
||
| -- rel8 | ||
| import Rel8.Aggregate ( Aggregate, Col( A ) ) | ||
| import Rel8.Expr ( Expr, Col( E ) ) | ||
| import Rel8.Aggregate ( Aggregate ) | ||
| import Rel8.Expr ( Expr ) | ||
| import Rel8.FCF ( Eval, Exp ) | ||
| import Rel8.Kind.Context ( SContext(..), Reifiable( contextSing ) ) | ||
| import Rel8.Schema.HTable.Identity ( HIdentity(..), HType ) | ||
| import qualified Rel8.Schema.Kind as K | ||
| import Rel8.Schema.Name ( Name(..), Col( N ) ) | ||
| import Rel8.Schema.Null ( Sql ) | ||
| import Rel8.Schema.Reify ( Reify, Col(..) ) | ||
| import Rel8.Schema.Result ( Col( R ), Result, absurd ) | ||
| import Rel8.Schema.Spec ( Spec( Spec ) ) | ||
| import Rel8.Table | ||
| ( Table, Columns, Context, fromColumns, toColumns | ||
| , Unreify, reify, unreify, coherence, congruence | ||
| ) | ||
| import Rel8.Table.Recontextualize ( Recontextualize ) | ||
| import Rel8.Type ( DBType ) | ||
| import Rel8.Schema.Name ( Name(..) ) | ||
| import Rel8.Schema.Result ( Result ) | ||
|
|
||
|
|
||
| -- | This type family is used to specify columns in 'Rel8able's. In @Column f | ||
| -- a@, @f@ is the context of the column (which should be left polymorphic in | ||
| -- 'Rel8able' definitions), and @a@ is the type of the column. | ||
| type Column :: K.Context -> Type -> Type | ||
| type family Column context a where | ||
| Column (Reify context) a = AColumn context a | ||
| Column Aggregate a = Aggregate a | ||
| Column Expr a = Expr a | ||
| Column Name a = Name a | ||
| Column Result a = a | ||
|
|
||
|
|
||
| type AColumn :: K.Context -> Type -> Type | ||
| newtype AColumn context a = AColumn (Column context a) | ||
|
|
||
|
|
||
| instance (Reifiable context, Sql DBType a) => | ||
| Table (Reify context) (AColumn context a) | ||
| where | ||
| type Context (AColumn context a) = Reify context | ||
| type Columns (AColumn context a) = HType a | ||
| type Unreify (AColumn context a) = Column context a | ||
|
|
||
| fromColumns (HType (Reify a)) = sfromColumn contextSing a | ||
| toColumns = HType . Reify . stoColumn contextSing | ||
| reify _ = AColumn | ||
| unreify _ (AColumn a) = a | ||
|
|
||
| coherence Refl = case contextSing @context of | ||
| SAggregate -> const Refl | ||
| SExpr -> const Refl | ||
| SName -> const Refl | ||
| SResult -> absurd | ||
| SReify _ -> const Refl | ||
|
|
||
| congruence Refl = case contextSing @context of | ||
| SAggregate -> const Refl | ||
| SExpr -> const Refl | ||
| SName -> const Refl | ||
| SResult -> absurd | ||
| SReify _ -> const Refl | ||
|
|
||
|
|
||
| instance (Reifiable context, Reifiable context', Sql DBType a) => | ||
| Recontextualize | ||
| (Reify context) | ||
| (Reify context') | ||
| (AColumn context a) | ||
| (AColumn context' a) | ||
|
|
||
|
|
||
| sfromColumn :: () | ||
| => SContext context | ||
| -> Col context ('Spec a) | ||
| -> AColumn context a | ||
| sfromColumn = \case | ||
| SAggregate -> \(A a) -> AColumn a | ||
| SExpr -> \(E a) -> AColumn a | ||
| SName -> \(N a) -> AColumn a | ||
| SResult -> \(R a) -> AColumn a | ||
| SReify context -> \(Reify a) -> AColumn (sfromColumn context a) | ||
|
|
||
|
|
||
| stoColumn :: () | ||
| => SContext context | ||
| -> AColumn context a | ||
| -> Col context ('Spec a) | ||
| stoColumn = \case | ||
| SAggregate -> \(AColumn a) -> A a | ||
| SExpr -> \(AColumn a) -> E a | ||
| SName -> \(AColumn a) -> N a | ||
| SResult -> \(AColumn a) -> R a | ||
| SReify context -> \(AColumn a) -> Reify (stoColumn context a) | ||
|
|
||
|
|
||
| data TColumn :: K.Context -> Type -> Exp Type | ||
| type instance Eval (TColumn f a) = Column f a |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,106 +1,23 @@ | ||
| {-# language DataKinds #-} | ||
| {-# language LambdaCase #-} | ||
| {-# language MultiParamTypeClasses #-} | ||
| {-# language ScopedTypeVariables #-} | ||
| {-# language StandaloneKindSignatures #-} | ||
| {-# language TypeApplications #-} | ||
| {-# language TypeFamilies #-} | ||
| {-# language UndecidableInstances #-} | ||
|
|
||
| module Rel8.Column.ADT | ||
| ( HADT, AHADT(..) | ||
| ( HADT | ||
| ) | ||
| where | ||
|
|
||
| -- base | ||
| import Data.Kind ( Type ) | ||
| import Data.Type.Equality ( (:~:)( Refl ) ) | ||
| import Prelude | ||
| import Prelude () | ||
|
|
||
| -- rel8 | ||
| import Rel8.Generic.Rel8able ( GColumns ) | ||
| import Rel8.Kind.Context ( SContext(..), Reifiable, contextSing ) | ||
| import Rel8.Schema.Context ( Col ) | ||
| import qualified Rel8.Schema.Kind as K | ||
| import Rel8.Schema.Reify ( Reify, hreify, hunreify ) | ||
| import Rel8.Schema.Result ( Result, absurd ) | ||
| import Rel8.Table | ||
| ( Table, Columns, Context, fromColumns, toColumns | ||
| , Unreify, reify, unreify, coherence, congruence | ||
| ) | ||
| import Rel8.Table.ADT ( ADT( ADT ), ADTable, fromADT, toADT ) | ||
| import Rel8.Table.Rel8able () | ||
| import Rel8.Table.Recontextualize ( Recontextualize ) | ||
| import Rel8.Schema.Result ( Result ) | ||
| import Rel8.Table.ADT ( ADT ) | ||
|
|
||
|
|
||
| type HADT :: K.Context -> K.Rel8able -> Type | ||
| type family HADT context t where | ||
| HADT (Reify context) t = AHADT context t | ||
| HADT Result t = t Result | ||
| HADT context t = ADT t context | ||
|
|
||
|
|
||
| type AHADT :: K.Context -> K.Rel8able -> Type | ||
| newtype AHADT context t = AHADT (HADT context t) | ||
|
|
||
|
|
||
| instance (ADTable t, Reifiable context) => | ||
| Table (Reify context) (AHADT context t) | ||
| where | ||
| type Context (AHADT context t) = Reify context | ||
| type Columns (AHADT context t) = GColumns (ADT t) | ||
| type Unreify (AHADT context t) = HADT context t | ||
|
|
||
| fromColumns = sfromColumnsADT contextSing | ||
| toColumns = stoColumnsADT contextSing | ||
| reify _ = AHADT | ||
| unreify _ (AHADT a) = a | ||
|
|
||
| coherence = case contextSing @context of | ||
| SAggregate -> \Refl _ -> Refl | ||
| SExpr -> \Refl _ -> Refl | ||
| SName -> \Refl _ -> Refl | ||
| SResult -> \Refl -> absurd | ||
| SReify _ -> \Refl _ -> Refl | ||
|
|
||
| congruence = case contextSing @context of | ||
| SAggregate -> \_ _ -> Refl | ||
| SExpr -> \_ _ -> Refl | ||
| SName -> \_ _ -> Refl | ||
| SResult -> \Refl -> absurd | ||
| SReify _ -> \_ _ -> Refl | ||
|
|
||
|
|
||
| instance | ||
| ( Reifiable context, Reifiable context' | ||
| , ADTable t, t ~ t' | ||
| ) | ||
| => Recontextualize | ||
| (Reify context) | ||
| (Reify context') | ||
| (AHADT context t) | ||
| (AHADT context' t') | ||
|
|
||
|
|
||
| sfromColumnsADT :: ADTable t | ||
| => SContext context | ||
| -> GColumns (ADT t) (Col (Reify context)) | ||
| -> AHADT context t | ||
| sfromColumnsADT = \case | ||
| SAggregate -> AHADT . ADT . hunreify | ||
| SExpr -> AHADT . ADT . hunreify | ||
| SName -> AHADT . ADT . hunreify | ||
| SResult -> AHADT . fromADT . ADT . hunreify | ||
| SReify context -> AHADT . sfromColumnsADT context . hunreify | ||
|
|
||
|
|
||
| stoColumnsADT :: ADTable t | ||
| => SContext context | ||
| -> AHADT context t | ||
| -> GColumns (ADT t) (Col (Reify context)) | ||
| stoColumnsADT = \case | ||
| SAggregate -> hreify . (\(AHADT (ADT a)) -> a) | ||
| SExpr -> hreify . (\(AHADT (ADT a)) -> a) | ||
| SName -> hreify . (\(AHADT (ADT a)) -> a) | ||
| SResult -> hreify . (\(ADT a) -> a) . toADT . (\(AHADT a) -> a) | ||
| SReify context -> hreify . stoColumnsADT context . (\(AHADT a) -> a) |
Oops, something went wrong.