{-# language AllowAmbiguousTypes #-}
{-# language DataKinds #-}
{-# language DefaultSignatures #-}
{-# language FlexibleContexts #-}
{-# language FlexibleInstances #-}
{-# language MultiParamTypeClasses #-}
{-# language ScopedTypeVariables #-}
{-# language StandaloneKindSignatures #-}
{-# language TypeApplications #-}
{-# language TypeFamilies #-}
{-# language UndecidableInstances #-}

module Rel8.Generic.Rel8able
  ( KRel8able, Rel8able
  , Algebra
  , GRep
  , GColumns, gfromColumns, gtoColumns
  , greify, gunreify
  , TUnreifyContext
  )
where

-- base
import Data.Kind ( Constraint, Type )
import Data.Proxy ( Proxy( Proxy ) )
import Data.Type.Equality ( (:~:)( Refl ) )
import GHC.Generics ( Generic, Rep, from, to )
import Prelude

-- rel8
import Rel8.Kind.Context ( Reifiable )
import Rel8.FCF ( Eval, Exp )
import Rel8.Generic.Map ( GMap, GMappable, gmap, gunmap )
import Rel8.Generic.Record ( Record(..) )
import Rel8.Generic.Table ( GAlgebra )
import qualified Rel8.Generic.Table.Record as G
import qualified Rel8.Kind.Algebra as K ( Algebra(..) )
import Rel8.Schema.Context ( Col )
import Rel8.Schema.Context.Label ( Labelable )
import Rel8.Schema.HTable ( HTable )
import qualified Rel8.Schema.Kind as K
import Rel8.Schema.Reify ( Reify, UnwrapReify )
import Rel8.Schema.Result ( Result )
import Rel8.Table
  ( fromColumns, toColumns, reify, unreify
  , TTable, TColumns, TContext, TUnreify
  )


type KRel8able :: Type
type KRel8able = K.Rel8able


-- | This type class allows you to define custom 'Table's using higher-kinded
-- data types. Higher-kinded data types are data types of the pattern:
--
-- @
-- data MyType f =
--   MyType { field1 :: Column f T1 OR HK1 f
--          , field2 :: Column f T2 OR HK2 f
--          , ...
--          , fieldN :: Column f Tn OR HKn f
--          }
-- @
-- 
-- where @Tn@ is any Haskell type, and @HKn@ is any higher-kinded type.
-- 
-- That is, higher-kinded data are records where all fields in the record are
-- all either of the type @Column f T@ (for any @T@), or are themselves
-- higher-kinded data:
-- 
-- [Nested]
-- 
-- @
-- data Nested f =
--   Nested { nested1 :: MyType f
--          , nested2 :: MyType f
--          }
-- @
-- 
-- The @Rel8able@ type class is used to give us a special mapping operation
-- that lets us change the type parameter @f@.
-- 
-- [Supplying @Rel8able@ instances]
-- 
-- This type class should be derived generically for all table types in your
-- project. To do this, enable the @DeriveAnyType@ and @DeriveGeneric@ language
-- extensions:
-- 
-- @
-- \{\-\# LANGUAGE DeriveAnyClass, DeriveGeneric #-\}
-- 
-- data MyType f = MyType { fieldA :: Column f T }
--   deriving ( GHC.Generics.Generic, Rel8able )
-- @
type Rel8able :: K.Rel8able -> Constraint
class HTable (GColumns t) => Rel8able t where
  type GColumns t :: K.HTable

  gfromColumns :: (Labelable context, Reifiable context)
    => GColumns t (Col (Reify context)) -> t (Reify context)

  gtoColumns :: (Labelable context, Reifiable context)
    => t (Reify context) -> GColumns t (Col (Reify context))

  greify :: (Labelable context, Reifiable context)
    => t context -> t (Reify context)

  gunreify :: (Labelable context, Reifiable context)
    => t (Reify context) -> t context

  type GColumns t = G.GColumns TColumns (GRep t (Reify Result))

  default gfromColumns :: forall context.
    ( Generic (Record (t (Reify context)))
    , G.GTable (TTable (Reify context)) TColumns (Col (Reify context)) (GRep t (Reify context))
    , G.GColumns TColumns (GRep t (Reify context)) ~ GColumns t
    )
    => GColumns t (Col (Reify context)) -> t (Reify context)
  gfromColumns =
    Record (t (Reify context)) -> t (Reify context)
forall a. Record a -> a
unrecord (Record (t (Reify context)) -> t (Reify context))
-> (GColumns t (Col (Reify context)) -> Record (t (Reify context)))
-> GColumns t (Col (Reify context))
-> t (Reify context)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    GRecord (Rep (t (Reify context))) Any -> Record (t (Reify context))
forall a x. Generic a => Rep a x -> a
to (GRecord (Rep (t (Reify context))) Any
 -> Record (t (Reify context)))
-> (GColumns t (Col (Reify context))
    -> GRecord (Rep (t (Reify context))) Any)
-> GColumns t (Col (Reify context))
-> Record (t (Reify context))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    (forall a.
 Eval (TTable (Reify context) a) =>
 Eval (TColumns a) (Col (Reify context)) -> a)
-> GColumns
     TColumns (GRecord (Rep (t (Reify context)))) (Col (Reify context))
-> GRecord (Rep (t (Reify context))) Any
forall (_Table :: * -> Exp Constraint)
       (_Columns :: * -> Exp HTable) (context :: HContext) (rep :: * -> *)
       x.
GTable _Table _Columns context rep =>
(forall a. Eval (_Table a) => Eval (_Columns a) context -> a)
-> GColumns _Columns rep context -> rep x
G.gfromColumns @(TTable (Reify context)) @TColumns forall a.
Eval (TTable (Reify context) a) =>
Eval (TColumns a) (Col (Reify context)) -> a
forall (context :: Context) a.
Table context a =>
Columns a (Col context) -> a
fromColumns

  default gtoColumns :: forall context.
    ( Generic (Record (t (Reify context)))
    , G.GTable (TTable (Reify context)) TColumns (Col (Reify context)) (GRep t (Reify context))
    , G.GColumns TColumns (GRep t (Reify context)) ~ GColumns t
    )
    => t (Reify context) -> GColumns t (Col (Reify context))
  gtoColumns =
    (forall a.
 Eval (TTable (Reify context) a) =>
 a -> Eval (TColumns a) (Col (Reify context)))
-> GRecord (Rep (t (Reify context))) Any
-> GColumns
     TColumns (GRecord (Rep (t (Reify context)))) (Col (Reify context))
forall (_Table :: * -> Exp Constraint)
       (_Columns :: * -> Exp HTable) (context :: HContext) (rep :: * -> *)
       x.
GTable _Table _Columns context rep =>
(forall a. Eval (_Table a) => a -> Eval (_Columns a) context)
-> rep x -> GColumns _Columns rep context
G.gtoColumns @(TTable (Reify context)) @TColumns forall a.
Eval (TTable (Reify context) a) =>
a -> Eval (TColumns a) (Col (Reify context))
forall (context :: Context) a.
Table context a =>
a -> Columns a (Col context)
toColumns (GRecord (Rep (t (Reify context))) Any
 -> GColumns t (Col (Reify context)))
-> (t (Reify context) -> GRecord (Rep (t (Reify context))) Any)
-> t (Reify context)
-> GColumns t (Col (Reify context))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Record (t (Reify context)) -> GRecord (Rep (t (Reify context))) Any
forall a x. Generic a => a -> Rep a x
from (Record (t (Reify context))
 -> GRecord (Rep (t (Reify context))) Any)
-> (t (Reify context) -> Record (t (Reify context)))
-> t (Reify context)
-> GRecord (Rep (t (Reify context))) Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    t (Reify context) -> Record (t (Reify context))
forall a. a -> Record a
Record

  default greify :: forall context.
    ( Generic (Record (t context))
    , Generic (Record (t (Reify context)))
    , GMappable (TTable (Reify context)) (GRep t (Reify context))
    , GRep t context ~ GMap TUnreify (GRep t (Reify context))
    )
    => t context -> t (Reify context)
  greify =
    Record (t (Reify context)) -> t (Reify context)
forall a. Record a -> a
unrecord (Record (t (Reify context)) -> t (Reify context))
-> (t context -> Record (t (Reify context)))
-> t context
-> t (Reify context)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    GRecord (Rep (t (Reify context))) Any -> Record (t (Reify context))
forall a x. Generic a => Rep a x -> a
to (GRecord (Rep (t (Reify context))) Any
 -> Record (t (Reify context)))
-> (t context -> GRecord (Rep (t (Reify context))) Any)
-> t context
-> Record (t (Reify context))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Proxy TUnreify
-> (forall a.
    Eval (TTable (Reify context) a) =>
    Eval (TUnreify a) -> a)
-> GMap TUnreify (GRecord (Rep (t (Reify context)))) Any
-> GRecord (Rep (t (Reify context))) Any
forall (constraint :: * -> Exp Constraint) (rep :: * -> *)
       (proxy :: (* -> * -> *) -> *) (f :: * -> * -> *) x.
GMappable constraint rep =>
proxy f
-> (forall a. Eval (constraint a) => Eval (f a) -> a)
-> GMap f rep x
-> rep x
gunmap @(TTable (Reify context)) (Proxy TUnreify
forall k (t :: k). Proxy t
Proxy @TUnreify) ((Reify context :~: Reify context) -> Unreify a -> a
forall (context :: Context) a (ctx :: Context).
Table context a =>
(context :~: Reify ctx) -> Unreify a -> a
reify Reify context :~: Reify context
forall k (a :: k). a :~: a
Refl) (GMap TUnreify (GRecord (Rep (t (Reify context)))) Any
 -> GRecord (Rep (t (Reify context))) Any)
-> (t context
    -> GMap TUnreify (GRecord (Rep (t (Reify context)))) Any)
-> t context
-> GRecord (Rep (t (Reify context))) Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Record (t context)
-> GMap TUnreify (GRecord (Rep (t (Reify context)))) Any
forall a x. Generic a => a -> Rep a x
from (Record (t context)
 -> GMap TUnreify (GRecord (Rep (t (Reify context)))) Any)
-> (t context -> Record (t context))
-> t context
-> GMap TUnreify (GRecord (Rep (t (Reify context)))) Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    t context -> Record (t context)
forall a. a -> Record a
Record

  default gunreify :: forall context.
    ( Generic (Record (t context))
    , Generic (Record (t (Reify context)))
    , GMappable (TTable (Reify context)) (GRep t (Reify context))
    , GRep t context ~ GMap TUnreify (GRep t (Reify context))
    )
    => t (Reify context) -> t context
  gunreify =
    Record (t context) -> t context
forall a. Record a -> a
unrecord (Record (t context) -> t context)
-> (t (Reify context) -> Record (t context))
-> t (Reify context)
-> t context
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    GMap TUnreify (GRecord (Rep (t (Reify context)))) Any
-> Record (t context)
forall a x. Generic a => Rep a x -> a
to (GMap TUnreify (GRecord (Rep (t (Reify context)))) Any
 -> Record (t context))
-> (t (Reify context)
    -> GMap TUnreify (GRecord (Rep (t (Reify context)))) Any)
-> t (Reify context)
-> Record (t context)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Proxy TUnreify
-> (forall a.
    Eval (TTable (Reify context) a) =>
    a -> Eval (TUnreify a))
-> GRecord (Rep (t (Reify context))) Any
-> GMap TUnreify (GRecord (Rep (t (Reify context)))) Any
forall (constraint :: * -> Exp Constraint) (rep :: * -> *)
       (proxy :: (* -> * -> *) -> *) (f :: * -> * -> *) x.
GMappable constraint rep =>
proxy f
-> (forall a. Eval (constraint a) => a -> Eval (f a))
-> rep x
-> GMap f rep x
gmap @(TTable (Reify context)) (Proxy TUnreify
forall k (t :: k). Proxy t
Proxy @TUnreify) ((Reify context :~: Reify context) -> a -> Unreify a
forall (context :: Context) a (ctx :: Context).
Table context a =>
(context :~: Reify ctx) -> a -> Unreify a
unreify Reify context :~: Reify context
forall k (a :: k). a :~: a
Refl) (GRecord (Rep (t (Reify context))) Any
 -> GMap TUnreify (GRecord (Rep (t (Reify context)))) Any)
-> (t (Reify context) -> GRecord (Rep (t (Reify context))) Any)
-> t (Reify context)
-> GMap TUnreify (GRecord (Rep (t (Reify context)))) Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Record (t (Reify context)) -> GRecord (Rep (t (Reify context))) Any
forall a x. Generic a => a -> Rep a x
from (Record (t (Reify context))
 -> GRecord (Rep (t (Reify context))) Any)
-> (t (Reify context) -> Record (t (Reify context)))
-> t (Reify context)
-> GRecord (Rep (t (Reify context))) Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    t (Reify context) -> Record (t (Reify context))
forall a. a -> Record a
Record


type Algebra :: K.Rel8able -> K.Algebra
type Algebra t = GAlgebra (GRep t (Reify Result))


type GRep :: K.Rel8able -> K.Context -> Type -> Type
type GRep t context = Rep (Record (t context))


data TUnreifyContext :: Type -> Exp K.Context
type instance Eval (TUnreifyContext a) = UnwrapReify (Eval (TContext a))