{-# language DataKinds #-}
{-# language LambdaCase #-}
{-# language MultiParamTypeClasses #-}
{-# language StandaloneKindSignatures #-}
{-# language TypeFamilies #-}
{-# language UndecidableInstances #-}

module Rel8.Column.ADT
  ( HADT, AHADT(..)
  )
where

-- base
import Data.Kind ( Type )
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 )
import Rel8.Table
  ( Table, Columns, Context, fromColumns, toColumns
  , Unreify, reify, unreify
  )
import Rel8.Table.ADT ( ADT( ADT ), ADTable, fromADT, toADT )
import Rel8.Table.Recontextualize ( Recontextualize )


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 :: Columns (AHADT context t) (Col (Reify context)) -> AHADT context t
fromColumns = SContext context
-> GColumns (ADT t) (Col (Reify context)) -> AHADT context t
forall (t :: Rel8able) (context :: Context).
ADTable t =>
SContext context
-> GColumns (ADT t) (Col (Reify context)) -> AHADT context t
sfromColumnsADT SContext context
forall (context :: Context). Reifiable context => SContext context
contextSing
  toColumns :: AHADT context t -> Columns (AHADT context t) (Col (Reify context))
toColumns = SContext context
-> AHADT context t -> GColumns (ADT t) (Col (Reify context))
forall (t :: Rel8able) (context :: Context).
ADTable t =>
SContext context
-> AHADT context t -> GColumns (ADT t) (Col (Reify context))
stoColumnsADT SContext context
forall (context :: Context). Reifiable context => SContext context
contextSing
  reify :: (Reify context :~: Reify ctx)
-> Unreify (AHADT context t) -> AHADT context t
reify Reify context :~: Reify ctx
_ = Unreify (AHADT context t) -> AHADT context t
forall (context :: Context) (t :: Rel8able).
HADT context t -> AHADT context t
AHADT
  unreify :: (Reify context :~: Reify ctx)
-> AHADT context t -> Unreify (AHADT context t)
unreify Reify context :~: Reify ctx
_ (AHADT HADT context t
a) = Unreify (AHADT context t)
HADT context t
a


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 :: SContext context
-> GColumns (ADT t) (Col (Reify context)) -> AHADT context t
sfromColumnsADT = \case
  SContext context
SAggregate -> ADT t Aggregate -> AHADT context t
forall (context :: Context) (t :: Rel8able).
HADT context t -> AHADT context t
AHADT (ADT t Aggregate -> AHADT context t)
-> (GColumnsADT
      TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Aggregate))
    -> ADT t Aggregate)
-> GColumnsADT
     TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Aggregate))
-> AHADT context t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GColumnsADT
  TColumns (GRecord (Rep (t (Reify Result)))) (Col Aggregate)
-> ADT t Aggregate
forall (t :: Rel8able) (context :: Context).
GColumnsADT t (Col context) -> ADT t context
ADT (GColumnsADT
   TColumns (GRecord (Rep (t (Reify Result)))) (Col Aggregate)
 -> ADT t Aggregate)
-> (GColumnsADT
      TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Aggregate))
    -> GColumnsADT
         TColumns (GRecord (Rep (t (Reify Result)))) (Col Aggregate))
-> GColumnsADT
     TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Aggregate))
-> ADT t Aggregate
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GColumnsADT
  TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Aggregate))
-> GColumnsADT
     TColumns (GRecord (Rep (t (Reify Result)))) (Col Aggregate)
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col (Reify context)) -> t (Col context)
hunreify
  SContext context
SExpr -> ADT t Expr -> AHADT context t
forall (context :: Context) (t :: Rel8able).
HADT context t -> AHADT context t
AHADT (ADT t Expr -> AHADT context t)
-> (GColumnsADT
      TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Expr))
    -> ADT t Expr)
-> GColumnsADT
     TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Expr))
-> AHADT context t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GColumnsADT TColumns (GRecord (Rep (t (Reify Result)))) (Col Expr)
-> ADT t Expr
forall (t :: Rel8able) (context :: Context).
GColumnsADT t (Col context) -> ADT t context
ADT (GColumnsADT TColumns (GRecord (Rep (t (Reify Result)))) (Col Expr)
 -> ADT t Expr)
-> (GColumnsADT
      TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Expr))
    -> GColumnsADT
         TColumns (GRecord (Rep (t (Reify Result)))) (Col Expr))
-> GColumnsADT
     TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Expr))
-> ADT t Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GColumnsADT
  TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Expr))
-> GColumnsADT
     TColumns (GRecord (Rep (t (Reify Result)))) (Col Expr)
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col (Reify context)) -> t (Col context)
hunreify
  SContext context
SName -> ADT t Name -> AHADT context t
forall (context :: Context) (t :: Rel8able).
HADT context t -> AHADT context t
AHADT (ADT t Name -> AHADT context t)
-> (GColumnsADT
      TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Name))
    -> ADT t Name)
-> GColumnsADT
     TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Name))
-> AHADT context t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GColumnsADT TColumns (GRecord (Rep (t (Reify Result)))) (Col Name)
-> ADT t Name
forall (t :: Rel8able) (context :: Context).
GColumnsADT t (Col context) -> ADT t context
ADT (GColumnsADT TColumns (GRecord (Rep (t (Reify Result)))) (Col Name)
 -> ADT t Name)
-> (GColumnsADT
      TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Name))
    -> GColumnsADT
         TColumns (GRecord (Rep (t (Reify Result)))) (Col Name))
-> GColumnsADT
     TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Name))
-> ADT t Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GColumnsADT
  TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Name))
-> GColumnsADT
     TColumns (GRecord (Rep (t (Reify Result)))) (Col Name)
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col (Reify context)) -> t (Col context)
hunreify
  SContext context
SResult -> t Result -> AHADT context t
forall (context :: Context) (t :: Rel8able).
HADT context t -> AHADT context t
AHADT (t Result -> AHADT context t)
-> (GColumnsADT
      TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Result))
    -> t Result)
-> GColumnsADT
     TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Result))
-> AHADT context t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (Reify Result))
    -> ADT t Result)
-> GColumnsADT
     TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify 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 (GColumnsADT
   TColumns (GRecord (Rep (t (Reify Result)))) (Col Result)
 -> ADT t Result)
-> (GColumnsADT
      TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Result))
    -> GColumnsADT
         TColumns (GRecord (Rep (t (Reify Result)))) (Col Result))
-> GColumnsADT
     TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Result))
-> ADT t Result
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GColumnsADT
  TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Result))
-> GColumnsADT
     TColumns (GRecord (Rep (t (Reify Result)))) (Col Result)
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col (Reify context)) -> t (Col context)
hunreify
  SReify SContext context
context -> AHADT context t -> AHADT context t
forall (context :: Context) (t :: Rel8able).
HADT context t -> AHADT context t
AHADT (AHADT context t -> AHADT context t)
-> (GColumnsADT
      TColumns
      (GRecord (Rep (t (Reify Result))))
      (Col (Reify (Reify context)))
    -> AHADT context t)
-> GColumnsADT
     TColumns
     (GRecord (Rep (t (Reify Result))))
     (Col (Reify (Reify context)))
-> AHADT context t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SContext context
-> GColumns (ADT t) (Col (Reify context)) -> AHADT context t
forall (t :: Rel8able) (context :: Context).
ADTable t =>
SContext context
-> GColumns (ADT t) (Col (Reify context)) -> AHADT context t
sfromColumnsADT SContext context
context (GColumnsADT
   TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify context))
 -> AHADT context t)
-> (GColumnsADT
      TColumns
      (GRecord (Rep (t (Reify Result))))
      (Col (Reify (Reify context)))
    -> GColumnsADT
         TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify context)))
-> GColumnsADT
     TColumns
     (GRecord (Rep (t (Reify Result))))
     (Col (Reify (Reify context)))
-> AHADT context t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GColumnsADT
  TColumns
  (GRecord (Rep (t (Reify Result))))
  (Col (Reify (Reify context)))
-> GColumnsADT
     TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify context))
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col (Reify context)) -> t (Col context)
hunreify


stoColumnsADT :: ADTable t
  => SContext context
  -> AHADT context t
  -> GColumns (ADT t) (Col (Reify context))
stoColumnsADT :: SContext context
-> AHADT context t -> GColumns (ADT t) (Col (Reify context))
stoColumnsADT = \case
  SContext context
SAggregate -> GColumnsADT
  TColumns (GRecord (Rep (t (Reify Result)))) (Col Aggregate)
-> GColumnsADT
     TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Aggregate))
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col context) -> t (Col (Reify context))
hreify (GColumnsADT
   TColumns (GRecord (Rep (t (Reify Result)))) (Col Aggregate)
 -> GColumnsADT
      TColumns
      (GRecord (Rep (t (Reify Result))))
      (Col (Reify Aggregate)))
-> (AHADT context t
    -> GColumnsADT
         TColumns (GRecord (Rep (t (Reify Result)))) (Col Aggregate))
-> AHADT context t
-> GColumnsADT
     TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Aggregate))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(AHADT (ADT a)) -> GColumnsADT t (Col Aggregate)
GColumnsADT
  TColumns (GRecord (Rep (t (Reify Result)))) (Col Aggregate)
a)
  SContext context
SExpr -> GColumnsADT TColumns (GRecord (Rep (t (Reify Result)))) (Col Expr)
-> GColumnsADT
     TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Expr))
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col context) -> t (Col (Reify context))
hreify (GColumnsADT TColumns (GRecord (Rep (t (Reify Result)))) (Col Expr)
 -> GColumnsADT
      TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Expr)))
-> (AHADT context t
    -> GColumnsADT
         TColumns (GRecord (Rep (t (Reify Result)))) (Col Expr))
-> AHADT context t
-> GColumnsADT
     TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Expr))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(AHADT (ADT a)) -> GColumnsADT t (Col Expr)
GColumnsADT TColumns (GRecord (Rep (t (Reify Result)))) (Col Expr)
a)
  SContext context
SName -> GColumnsADT TColumns (GRecord (Rep (t (Reify Result)))) (Col Name)
-> GColumnsADT
     TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Name))
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col context) -> t (Col (Reify context))
hreify (GColumnsADT TColumns (GRecord (Rep (t (Reify Result)))) (Col Name)
 -> GColumnsADT
      TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Name)))
-> (AHADT context t
    -> GColumnsADT
         TColumns (GRecord (Rep (t (Reify Result)))) (Col Name))
-> AHADT context t
-> GColumnsADT
     TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Name))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(AHADT (ADT a)) -> GColumnsADT t (Col Name)
GColumnsADT TColumns (GRecord (Rep (t (Reify Result)))) (Col Name)
a)
  SContext context
SResult -> GColumnsADT
  TColumns (GRecord (Rep (t (Reify Result)))) (Col Result)
-> GColumnsADT
     TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Result))
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col context) -> t (Col (Reify context))
hreify (GColumnsADT
   TColumns (GRecord (Rep (t (Reify Result)))) (Col Result)
 -> GColumnsADT
      TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Result)))
-> (AHADT context t
    -> GColumnsADT
         TColumns (GRecord (Rep (t (Reify Result)))) (Col Result))
-> AHADT context t
-> GColumnsADT
     TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify Result))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(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))
-> (AHADT context t -> ADT t Result)
-> AHADT context t
-> 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 (t Result -> ADT t Result)
-> (AHADT context t -> t Result) -> AHADT context t -> ADT t Result
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(AHADT HADT context t
a) -> t Result
HADT context t
a)
  SReify SContext context
context -> GColumnsADT
  TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify context))
-> GColumnsADT
     TColumns
     (GRecord (Rep (t (Reify Result))))
     (Col (Reify (Reify context)))
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col context) -> t (Col (Reify context))
hreify (GColumnsADT
   TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify context))
 -> GColumnsADT
      TColumns
      (GRecord (Rep (t (Reify Result))))
      (Col (Reify (Reify context))))
-> (AHADT context t
    -> GColumnsADT
         TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify context)))
-> AHADT context t
-> GColumnsADT
     TColumns
     (GRecord (Rep (t (Reify Result))))
     (Col (Reify (Reify context)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SContext context
-> AHADT context t -> GColumns (ADT t) (Col (Reify context))
forall (t :: Rel8able) (context :: Context).
ADTable t =>
SContext context
-> AHADT context t -> GColumns (ADT t) (Col (Reify context))
stoColumnsADT SContext context
context (AHADT context t
 -> GColumnsADT
      TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify context)))
-> (AHADT context t -> AHADT context t)
-> AHADT context t
-> GColumnsADT
     TColumns (GRecord (Rep (t (Reify Result)))) (Col (Reify context))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(AHADT HADT context t
a) -> AHADT context t
HADT context t
a)