{-# language AllowAmbiguousTypes #-}
{-# language ConstraintKinds #-}
{-# language DataKinds #-}
{-# language FlexibleContexts #-}
{-# language NamedFieldPuns #-}
{-# language ScopedTypeVariables #-}
{-# language StandaloneKindSignatures #-}
{-# language TypeApplications #-}
{-# language TypeFamilies #-}
{-# language TypeOperators #-}
{-# language UndecidableInstances #-}
{-# language ViewPatterns #-}

module Rel8.Generic.Construction
  ( GGBuildable
  , GGBuild, ggbuild
  , GGConstructable
  , GGConstruct, ggconstruct
  , GGDeconstruct, ggdeconstruct, ggdeconstructA
  , GGName, ggname
  )
where

-- base
import Data.Bifunctor ( first )
import Data.Functor ((<&>))
import Data.Kind ( Constraint, Type )
import Data.List.NonEmpty ( NonEmpty( (:|) ) )
import GHC.TypeLits ( Symbol )
import Prelude

-- rel8
import Rel8.Expr ( Expr )
import Rel8.Expr.Eq ( (==.) )
import Rel8.Expr.Null ( nullify, snull, unsafeUnnullify )
import Rel8.Expr.Serialize ( litExpr )
import Rel8.FCF ( Eval, Exp, Id )
import Rel8.Generic.Construction.ADT
  ( GConstructorADT, GMakeableADT, gmakeADT
  , GConstructableADT
  , GBuildADT, gbuildADT
  , GConstructADT, gconstructADT, gdeconstructADT
  , RepresentableConstructors, GConstructors, gcindex, gctabulate
  , RepresentableFields, gftabulate
  )
import Rel8.Generic.Construction.Record
  ( GConstructor
  , GConstructable, GConstruct, gconstruct, gdeconstruct
  , Representable, gindex, gtabulate
  )
import Rel8.Generic.Table ( GGColumns )
import Rel8.Kind.Algebra
  ( SAlgebra( SProduct, SSum )
  , KnownAlgebra, algebraSing
  )
import qualified Rel8.Kind.Algebra as K
import Rel8.Schema.HTable ( HTable )
import Rel8.Schema.HTable.Identity ( HIdentity( HIdentity ) )
import qualified Rel8.Schema.Kind as K
import Rel8.Schema.Name ( Name( Name ) )
import Rel8.Schema.Null ( Nullity( Null, NotNull ) )
import Rel8.Schema.Spec ( Spec( Spec, nullity, info ) )
import Rel8.Table
  ( TTable, TColumns
  , Table, fromColumns, toColumns
  )
import Rel8.Table.Bool ( case_ )
import Rel8.Type.Tag ( Tag )

-- semigroupoids
import Data.Functor.Apply (Apply)
import Data.Semigroup.Traversable (sequence1, traverse1)


type GGBuildable :: K.Algebra -> Symbol -> (K.Context -> Exp (Type -> Type)) -> Constraint
type GGBuildable algebra name rep =
  ( KnownAlgebra algebra
  , Eval (GGColumns algebra TColumns (Eval (rep Expr))) ~ Eval (GGColumns algebra TColumns (Eval (rep Expr)))
  , Eval (GGColumns algebra TColumns (Eval (rep Name))) ~ Eval (GGColumns algebra TColumns (Eval (rep Expr)))
  , HTable (Eval (GGColumns algebra TColumns (Eval (rep Expr))))
  , GGBuildable' algebra name rep
  )


type GGBuildable' :: K.Algebra -> Symbol -> (K.Context -> Exp (Type -> Type)) -> Constraint
type family GGBuildable' algebra name rep where
  GGBuildable' 'K.Product name rep =
    ( name ~ GConstructor (Eval (rep Expr))
    , Representable Id (Eval (rep Expr))
    , GConstructable (TTable Expr) TColumns Id Expr (Eval (rep Expr))
    )
  GGBuildable' 'K.Sum name rep =
    ( Representable Id (GConstructorADT name (Eval (rep Expr)))
    , GMakeableADT (TTable Expr) TColumns Id Expr name (Eval (rep Expr))
    )


type GGBuild :: K.Algebra -> Symbol -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
type family GGBuild algebra name rep r where
  GGBuild 'K.Product _name rep r =
    GConstruct Id (Eval (rep Expr)) r
  GGBuild 'K.Sum name rep r =
    GConstruct Id (GConstructorADT name (Eval (rep Expr))) r


ggbuild :: forall algebra name rep a. GGBuildable algebra name rep
  => (Eval (GGColumns algebra TColumns (Eval (rep Expr))) Expr -> a)
  -> GGBuild algebra name rep a
ggbuild gfromColumns = case algebraSing @algebra of
  SProduct ->
    gtabulate @Id @(Eval (rep Expr)) @a $
    gfromColumns .
    gconstruct
      @(TTable Expr)
      @TColumns
      @Id
      @Expr
      @(Eval (rep Expr))
      (const toColumns)
  SSum ->
    gtabulate @Id @(GConstructorADT name (Eval (rep Expr))) @a $
    gfromColumns .
    gmakeADT
      @(TTable Expr)
      @TColumns
      @Id
      @Expr
      @name
      @(Eval (rep Expr))
      (const toColumns)
      (\Spec {info} -> snull info)
      (\Spec {nullity} -> case nullity of
        Null -> id
        NotNull -> nullify)
      (HIdentity . litExpr)


type GGConstructable :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Constraint
type GGConstructable algebra rep =
  ( KnownAlgebra algebra
  , Eval (GGColumns algebra TColumns (Eval (rep Expr))) ~ Eval (GGColumns algebra TColumns (Eval (rep Expr)))
  , Eval (GGColumns algebra TColumns (Eval (rep Name))) ~ Eval (GGColumns algebra TColumns (Eval (rep Expr)))
  , HTable (Eval (GGColumns algebra TColumns (Eval (rep Expr))))
  , GGConstructable' algebra rep
  )


type GGConstructable' :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Constraint
type family GGConstructable' algebra rep where
  GGConstructable' 'K.Product rep =
    ( Representable Id (Eval (rep Expr))
    , Representable Id (Eval (rep Name))
    , GConstructable (TTable Expr) TColumns Id Expr (Eval (rep Expr))
    , GConstructable (TTable Name) TColumns Id Name (Eval (rep Name))
    )
  GGConstructable' 'K.Sum rep =
    ( RepresentableConstructors Id (Eval (rep Expr))
    , RepresentableFields Id (Eval (rep Expr))
    , RepresentableFields Id (Eval (rep Name))
    , Functor (GConstructors Id (Eval (rep Expr)))
    , GConstructableADT (TTable Expr) TColumns Id Expr (Eval (rep Expr))
    , GConstructableADT (TTable Name) TColumns Id Name (Eval (rep Name))
    )


type GGConstruct :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
type family GGConstruct algebra rep r where
  GGConstruct 'K.Product rep r = GConstruct Id (Eval (rep Expr)) r -> r
  GGConstruct 'K.Sum rep r = GConstructADT Id (Eval (rep Expr)) r r


ggconstruct :: forall algebra rep a. GGConstructable algebra rep
  => (Eval (GGColumns algebra TColumns (Eval (rep Expr))) Expr -> a)
  -> GGConstruct algebra rep a -> a
ggconstruct gfromColumns f = case algebraSing @algebra of
  SProduct ->
    f $
    gtabulate @Id @(Eval (rep Expr)) @a $
    gfromColumns .
    gconstruct
      @(TTable Expr)
      @TColumns
      @Id
      @Expr
      @(Eval (rep Expr))
      (const toColumns)
  SSum ->
    gcindex @Id @(Eval (rep Expr)) @a f $
    fmap gfromColumns $
    gconstructADT
      @(TTable Expr)
      @TColumns
      @Id
      @Expr
      @(Eval (rep Expr))
      (const toColumns)
      (\Spec {info} -> snull info)
      (\Spec {nullity} -> case nullity of
        Null -> id
        NotNull -> nullify)
      (HIdentity . litExpr)


type GGDeconstruct :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type -> Type
type family GGDeconstruct algebra rep a r where
  GGDeconstruct 'K.Product rep a r =
    GConstruct Id (Eval (rep Expr)) r -> a -> r
  GGDeconstruct 'K.Sum rep a r =
    GConstructADT Id (Eval (rep Expr)) r (a -> r)


ggdeconstruct :: forall algebra rep a r. (GGConstructable algebra rep, Table Expr r)
  => (a -> Eval (GGColumns algebra TColumns (Eval (rep Expr))) Expr)
  -> GGDeconstruct algebra rep a r
ggdeconstruct gtoColumns = case algebraSing @algebra of
  SProduct -> \build ->
    gindex @Id @(Eval (rep Expr)) @r build .
    gdeconstruct
      @(TTable Expr)
      @TColumns
      @Id
      @Expr
      @(Eval (rep Expr))
      (const fromColumns) .
    gtoColumns
  SSum ->
    gctabulate @Id @(Eval (rep Expr)) @r @(a -> r) $ \constructors as ->
      let
        (HIdentity tag, cases) =
          gdeconstructADT
            @(TTable Expr)
            @TColumns
            @Id
            @Expr
            @(Eval (rep Expr))
            (const fromColumns)
            (\Spec {nullity} -> case nullity of
              Null -> id
              NotNull -> unsafeUnnullify)
            constructors $
          gtoColumns as
      in
        case cases of
          ((_, r) :| (map (first ((tag ==.) . litExpr)) -> cases')) ->
            case_ cases' r


ggdeconstructA :: forall algebra rep a f r. (GGConstructable algebra rep, Apply f, Table Expr r)
  => (a -> Eval (GGColumns algebra TColumns (Eval (rep Expr))) Expr)
  -> GGDeconstruct algebra rep a (f r)
ggdeconstructA gtoColumns = case algebraSing @algebra of
  SProduct -> \build ->
    gindex @Id @(Eval (rep Expr)) @(f r) build .
    gdeconstruct
      @(TTable Expr)
      @TColumns
      @Id
      @Expr
      @(Eval (rep Expr))
      (const fromColumns) .
    gtoColumns
  SSum ->
    gctabulate @Id @(Eval (rep Expr)) @(f r) @(a -> f r) $ \constructors as ->
      let
        (HIdentity tag, cases) =
          gdeconstructADT
            @(TTable Expr)
            @TColumns
            @Id
            @Expr
            @(Eval (rep Expr))
            (const fromColumns)
            (\Spec {nullity} -> case nullity of
              Null -> id
              NotNull -> unsafeUnnullify)
            constructors $
          gtoColumns as
        fcases = traverse1 sequence1 cases
      in
        fcases
          <&> \((_, r) :| (map (first ((tag ==.) . litExpr)) -> cases')) ->
            case_ cases' r


type GGName :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
type family GGName algebra rep a where
  GGName 'K.Product rep a = GConstruct Id (Eval (rep Name)) a
  GGName 'K.Sum rep a = Name Tag -> GBuildADT Id (Eval (rep Name)) a


ggname :: forall algebra rep a. GGConstructable algebra rep
  => (Eval (GGColumns algebra TColumns (Eval (rep Expr))) Name -> a)
  -> GGName algebra rep a
ggname gfromColumns = case algebraSing @algebra of
  SProduct ->
    gtabulate @Id @(Eval (rep Name)) @a $
    gfromColumns .
    gconstruct
      @(TTable Name)
      @TColumns
      @Id
      @Name
      @(Eval (rep Name))
      (const toColumns)
  SSum -> \tag ->
    gftabulate @Id @(Eval (rep Name)) @a $
    gfromColumns .
    gbuildADT
      @(TTable Name)
      @TColumns
      @Id
      @Name
      @(Eval (rep Name))
      (const toColumns)
      (\_ _ (Name a) -> Name a)
      (HIdentity tag)