{-# language DataKinds #-}
{-# language FlexibleInstances #-}
{-# language FunctionalDependencies #-}
{-# language ScopedTypeVariables #-}
{-# language StandaloneKindSignatures #-}
{-# language TypeApplications #-}
{-# language TypeFamilies #-}
{-# language UndecidableInstances #-}

{-# options_ghc -fno-warn-orphans #-}

module Rel8.Table.Rel8able
  (
  )
where

-- base
import Data.Kind ( Constraint, Type )
import Data.Type.Equality ( (:~:)( Refl ) )
import Prelude

-- rel8
import Rel8.Expr ( Expr )
import qualified Rel8.Kind.Algebra as K
import Rel8.Kind.Context
  ( SContext( SReify )
  , Reifiable, contextSing
  , sLabelable, sReifiable
  )
import Rel8.Generic.Rel8able
  ( Rel8able, Algebra
  , GColumns, gfromColumns, gtoColumns
  , greify, gunreify
  )
import Rel8.Schema.Context ( Col )
import Rel8.Schema.Context.Label ( Labelable )
import Rel8.Schema.Dict ( Dict( Dict ) )
import qualified Rel8.Schema.Kind as K
import Rel8.Schema.HTable ( HConstrainTable, hdicts )
import Rel8.Schema.Reify ( hreify, hunreify, UnwrapReify )
import Rel8.Schema.Result ( Result )
import Rel8.Table
  ( Table, Columns, Context, Congruent, fromColumns, toColumns
  , Unreify, reify, unreify
  )
import Rel8.Schema.Spec.ConstrainDBType ( ConstrainDBType )
import Rel8.Table.ADT ( ADT( ADT ), ADTable, fromADT, toADT )
import Rel8.Table.Eq ( EqTable, eqTable )
import Rel8.Table.HKD ( HKD )
import Rel8.Table.Ord ( OrdTable, ordTable )
import Rel8.Table.Recontextualize ( Recontextualize )
import Rel8.Table.Serialize ( FromExprs, ToExprs, fromResult, toResult )
import Rel8.Type.Eq ( DBEq )
import Rel8.Type.Ord ( DBOrd )


instance (Rel8able t, Labelable context, Reifiable context) =>
  Table context (t context)
 where
  type Columns (t context) = GColumns t
  type Context (t context) = context
  type Unreify (t context) = t (UnwrapReify context)

  fromColumns :: Columns (t context) (Col context) -> t context
fromColumns = t (Reify context) -> t context
forall (t :: Rel8able) (context :: Context).
(Rel8able t, Labelable context, Reifiable context) =>
t (Reify context) -> t context
gunreify (t (Reify context) -> t context)
-> (GColumns t (Col context) -> t (Reify context))
-> GColumns t (Col context)
-> t context
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GColumns t (Col (Reify context)) -> t (Reify context)
forall (t :: Rel8able) (context :: Context).
(Rel8able t, Labelable context, Reifiable context) =>
GColumns t (Col (Reify context)) -> t (Reify context)
gfromColumns (GColumns t (Col (Reify context)) -> t (Reify context))
-> (GColumns t (Col context) -> GColumns t (Col (Reify context)))
-> GColumns t (Col context)
-> t (Reify context)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GColumns t (Col context) -> GColumns t (Col (Reify context))
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col context) -> t (Col (Reify context))
hreify
  toColumns :: t context -> Columns (t context) (Col context)
toColumns = GColumns t (Col (Reify context)) -> GColumns t (Col context)
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col (Reify context)) -> t (Col context)
hunreify (GColumns t (Col (Reify context)) -> GColumns t (Col context))
-> (t context -> GColumns t (Col (Reify context)))
-> t context
-> GColumns t (Col context)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t (Reify context) -> GColumns t (Col (Reify context))
forall (t :: Rel8able) (context :: Context).
(Rel8able t, Labelable context, Reifiable context) =>
t (Reify context) -> GColumns t (Col (Reify context))
gtoColumns (t (Reify context) -> GColumns t (Col (Reify context)))
-> (t context -> t (Reify context))
-> t context
-> GColumns t (Col (Reify context))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t context -> t (Reify context)
forall (t :: Rel8able) (context :: Context).
(Rel8able t, Labelable context, Reifiable context) =>
t context -> t (Reify context)
greify

  reify :: (context :~: Reify ctx) -> Unreify (t context) -> t context
reify context :~: Reify ctx
Refl = case Reifiable context => SContext context
forall (context :: Context). Reifiable context => SContext context
contextSing @context of
    SReify SContext context
context -> case SContext context -> Dict Labelable context
forall (context :: Context).
SContext context -> Dict Labelable context
sLabelable SContext context
context of
      Dict Labelable context
Dict -> case SContext context -> Dict Reifiable context
forall (context :: Context).
SContext context -> Dict Reifiable context
sReifiable SContext context
context of
        Dict Reifiable context
Dict -> Unreify (t context) -> t context
forall (t :: Rel8able) (context :: Context).
(Rel8able t, Labelable context, Reifiable context) =>
t context -> t (Reify context)
greify

  unreify :: (context :~: Reify ctx) -> t context -> Unreify (t context)
unreify context :~: Reify ctx
Refl = case Reifiable context => SContext context
forall (context :: Context). Reifiable context => SContext context
contextSing @context of
    SReify SContext context
context -> case SContext context -> Dict Labelable context
forall (context :: Context).
SContext context -> Dict Labelable context
sLabelable SContext context
context of
      Dict Labelable context
Dict -> case SContext context -> Dict Reifiable context
forall (context :: Context).
SContext context -> Dict Reifiable context
sReifiable SContext context
context of
        Dict Reifiable context
Dict -> t context -> Unreify (t context)
forall (t :: Rel8able) (context :: Context).
(Rel8able t, Labelable context, Reifiable context) =>
t (Reify context) -> t context
gunreify


instance
  ( Rel8able t
  , Labelable from, Reifiable from
  , Labelable to, Reifiable to
  , Congruent (t from) (t to)
  )
  => Recontextualize from to (t from) (t to)


instance
  ( context ~ Expr
  , Rel8able t
  , HConstrainTable (Columns (t context)) (ConstrainDBType DBEq)
  )
  => EqTable (t context)
 where
  eqTable :: Columns (t context) (Dict (ConstrainDBType DBEq))
eqTable = HConstrainTable (Columns (t context)) (ConstrainDBType DBEq) =>
Columns (t context) (Dict (ConstrainDBType DBEq))
forall (t :: HTable) (c :: Spec -> Constraint).
(HTable t, HConstrainTable t c) =>
t (Dict c)
hdicts @(Columns (t context)) @(ConstrainDBType DBEq)


instance
  ( context ~ Expr
  , Rel8able t
  , HConstrainTable (Columns (t context)) (ConstrainDBType DBEq)
  , HConstrainTable (Columns (t context)) (ConstrainDBType DBOrd)
  )
  => OrdTable (t context)
 where
  ordTable :: Columns (t context) (Dict (ConstrainDBType DBOrd))
ordTable = HConstrainTable (Columns (t context)) (ConstrainDBType DBOrd) =>
Columns (t context) (Dict (ConstrainDBType DBOrd))
forall (t :: HTable) (c :: Spec -> Constraint).
(HTable t, HConstrainTable t c) =>
t (Dict c)
hdicts @(Columns (t context)) @(ConstrainDBType DBOrd)


type instance FromExprs (t Expr) = FromExprs' t


instance
  ( x ~ t' Expr
  , result ~ Result
  , ToExprs' (Algebra t) t' t
  )
  => ToExprs x (t result)
 where
  fromResult :: Columns x (Col Result) -> t result
fromResult = forall (algebra :: Algebra) (t' :: Rel8able) (t :: Rel8able).
ToExprs' algebra t' t =>
GColumns t' (Col Result) -> t Result
forall (t :: Rel8able).
ToExprs' (Algebra t) t' t =>
GColumns t' (Col Result) -> t Result
fromResult' @(Algebra t) @t'
  toResult :: t result -> Columns x (Col Result)
toResult = forall (algebra :: Algebra) (t' :: Rel8able) (t :: Rel8able).
ToExprs' algebra t' t =>
t Result -> GColumns t' (Col Result)
forall (t :: Rel8able).
ToExprs' (Algebra t) t' t =>
t Result -> GColumns t' (Col Result)
toResult' @(Algebra t) @t'


type FromExprs' :: K.Rel8able -> Type
type family FromExprs' t where
  FromExprs' (ADT t) = t Result
  FromExprs' (HKD a) = a
  FromExprs' t = t Result


type ToExprs' :: K.Algebra -> K.Rel8able -> K.Rel8able -> Constraint
class (algebra ~ Algebra t, Rel8able t') =>
  ToExprs' algebra t' t | algebra t -> t'
 where
  fromResult' :: GColumns t' (Col Result) -> t Result
  toResult' :: t Result -> GColumns t' (Col Result)


instance (Algebra t ~ 'K.Product, Rel8able t, t ~ t') =>
  ToExprs' 'K.Product t' t
 where
  fromResult' :: GColumns t' (Col Result) -> t Result
fromResult' = GColumns t' (Col Result) -> t Result
forall (context :: Context) a.
Table context a =>
Columns a (Col context) -> a
fromColumns
  toResult' :: t Result -> GColumns t' (Col Result)
toResult' = t Result -> GColumns t' (Col Result)
forall (context :: Context) a.
Table context a =>
a -> Columns a (Col context)
toColumns


instance (Algebra t ~ 'K.Sum, ADTable t, t' ~ ADT t) =>
  ToExprs' 'K.Sum t' t
 where
  fromResult' :: GColumns t' (Col Result) -> t Result
fromResult' = ADT t Result -> t Result
forall (t :: Rel8able). ADTable t => ADT t Result -> t Result
fromADT (ADT t Result -> t Result)
-> (GColumnsADT
      TColumns (GRecord (Rep (t (Reify Result)))) (Col Result)
    -> ADT t Result)
-> GColumnsADT
     TColumns (GRecord (Rep (t (Reify Result)))) (Col Result)
-> t Result
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GColumnsADT
  TColumns (GRecord (Rep (t (Reify Result)))) (Col Result)
-> ADT t Result
forall (t :: Rel8able) (context :: Context).
GColumnsADT t (Col context) -> ADT t context
ADT
  toResult' :: t Result -> GColumns t' (Col Result)
toResult' = (\(ADT GColumnsADT t (Col Result)
a) -> GColumnsADT t (Col Result)
GColumnsADT
  TColumns (GRecord (Rep (t (Reify Result)))) (Col Result)
a) (ADT t Result
 -> GColumnsADT
      TColumns (GRecord (Rep (t (Reify Result)))) (Col Result))
-> (t Result -> ADT t Result)
-> t Result
-> GColumnsADT
     TColumns (GRecord (Rep (t (Reify Result)))) (Col Result)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t Result -> ADT t Result
forall (t :: Rel8able). ADTable t => t Result -> ADT t Result
toADT