{-# language AllowAmbiguousTypes #-}
{-# language BlockArguments #-}
{-# language ConstraintKinds #-}
{-# language DataKinds #-}
{-# language FlexibleInstances #-}
{-# language GADTs #-}
{-# language InstanceSigs #-}
{-# language MultiParamTypeClasses #-}
{-# language RankNTypes #-}
{-# language ScopedTypeVariables #-}
{-# language StandaloneKindSignatures #-}
{-# language TypeApplications #-}
{-# language TypeFamilies #-}
{-# language UndecidableInstances #-}
{-# language UndecidableSuperClasses #-}

module Rel8.Schema.HTable.MapTable
  ( HMapTable(..)
  , MapSpec(..)
  , Precompose(..)
  , HMapTableField(..)
  , hproject
  )
where

-- base
import Data.Kind ( Constraint, Type )
import Prelude

-- rel8
import Rel8.FCF ( Exp, Eval )
import Rel8.Schema.HTable
  ( HTable, HConstrainTable, HField
  , hfield, htabulate, htraverse, hdicts, hspecs
  )
import Rel8.Schema.Spec ( Spec )
import qualified Rel8.Schema.Kind as K
import Rel8.Schema.Dict ( Dict( Dict ) )


type HMapTable :: (Type -> Exp Type) -> K.HTable -> K.HTable
newtype HMapTable f t context = HMapTable
  { HMapTable f t context -> t (Precompose f context)
unHMapTable :: t (Precompose f context)
  }


type Precompose :: (Type -> Exp Type) -> K.Context -> K.Context
newtype Precompose f g x = Precompose
  { Precompose f g x -> g (Eval (f x))
precomposed :: g (Eval (f x))
  }


type HMapTableField :: (Type -> Exp Type) -> K.HTable -> K.Context
data HMapTableField f t x where
  HMapTableField :: HField t a -> HMapTableField f t (Eval (f a))


instance (HTable t, MapSpec f) => HTable (HMapTable f t) where
  type HField (HMapTable f t) = 
    HMapTableField f t

  type HConstrainTable (HMapTable f t) c =
    HConstrainTable t (ComposeConstraint f c)

  hfield :: HMapTable f t context -> HField (HMapTable f t) a -> context a
hfield (HMapTable t (Precompose f context)
x) (HMapTableField i) = 
    Precompose f context a -> context (Eval (f a))
forall (f :: * -> Context) (g :: Context) x.
Precompose f g x -> g (Eval (f x))
precomposed (t (Precompose f context) -> HField t a -> Precompose f context a
forall (t :: HTable) (context :: Context) a.
HTable t =>
t context -> HField t a -> context a
hfield t (Precompose f context)
x HField t a
i) 

  htabulate :: (forall a. HField (HMapTable f t) a -> context a)
-> HMapTable f t context
htabulate forall a. HField (HMapTable f t) a -> context a
f = 
    t (Precompose f context) -> HMapTable f t context
forall (f :: * -> Context) (t :: HTable) (context :: Context).
t (Precompose f context) -> HMapTable f t context
HMapTable (t (Precompose f context) -> HMapTable f t context)
-> t (Precompose f context) -> HMapTable f t context
forall a b. (a -> b) -> a -> b
$ (forall a. HField t a -> Precompose f context a)
-> t (Precompose f context)
forall (t :: HTable) (context :: Context).
HTable t =>
(forall a. HField t a -> context a) -> t context
htabulate (context (Eval (f a)) -> Precompose f context a
forall (f :: * -> Context) (g :: Context) x.
g (Eval (f x)) -> Precompose f g x
Precompose (context (Eval (f a)) -> Precompose f context a)
-> (HField t a -> context (Eval (f a)))
-> HField t a
-> Precompose f context a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HMapTableField f t (Eval (f a)) -> context (Eval (f a))
forall a. HField (HMapTable f t) a -> context a
f (HMapTableField f t (Eval (f a)) -> context (Eval (f a)))
-> (HField t a -> HMapTableField f t (Eval (f a)))
-> HField t a
-> context (Eval (f a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HField t a -> HMapTableField f t (Eval (f a))
forall (t :: HTable) a (f :: * -> Context).
HField t a -> HMapTableField f t (Eval (f a))
HMapTableField)

  htraverse :: (forall a. f a -> m (g a))
-> HMapTable f t f -> m (HMapTable f t g)
htraverse forall a. f a -> m (g a)
f (HMapTable t (Precompose f f)
x) = 
    t (Precompose f g) -> HMapTable f t g
forall (f :: * -> Context) (t :: HTable) (context :: Context).
t (Precompose f context) -> HMapTable f t context
HMapTable (t (Precompose f g) -> HMapTable f t g)
-> m (t (Precompose f g)) -> m (HMapTable f t g)
forall (f :: Context) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. Precompose f f a -> m (Precompose f g a))
-> t (Precompose f f) -> m (t (Precompose f g))
forall (t :: HTable) (m :: Context) (f :: Context) (g :: Context).
(HTable t, Apply m) =>
(forall a. f a -> m (g a)) -> t f -> m (t g)
htraverse ((g (Eval (f a)) -> Precompose f g a)
-> m (g (Eval (f a))) -> m (Precompose f g a)
forall (f :: Context) a b. Functor f => (a -> b) -> f a -> f b
fmap g (Eval (f a)) -> Precompose f g a
forall (f :: * -> Context) (g :: Context) x.
g (Eval (f x)) -> Precompose f g x
Precompose (m (g (Eval (f a))) -> m (Precompose f g a))
-> (Precompose f f a -> m (g (Eval (f a))))
-> Precompose f f a
-> m (Precompose f g a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Eval (f a)) -> m (g (Eval (f a)))
forall a. f a -> m (g a)
f (f (Eval (f a)) -> m (g (Eval (f a))))
-> (Precompose f f a -> f (Eval (f a)))
-> Precompose f f a
-> m (g (Eval (f a)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Precompose f f a -> f (Eval (f a))
forall (f :: * -> Context) (g :: Context) x.
Precompose f g x -> g (Eval (f x))
precomposed) t (Precompose f f)
x
  {-# INLINABLE htraverse #-}

  hdicts :: forall c. HConstrainTable (HMapTable f t) c => HMapTable f t (Dict c)
  hdicts :: HMapTable f t (Dict c)
hdicts = 
    (forall a. HField (HMapTable f t) a -> Dict c a)
-> HMapTable f t (Dict c)
forall (t :: HTable) (context :: Context).
HTable t =>
(forall a. HField t a -> context a) -> t context
htabulate \(HMapTableField j) ->
      case t (Dict (ComposeConstraint f c))
-> HField t a -> Dict (ComposeConstraint f c) a
forall (t :: HTable) (context :: Context) a.
HTable t =>
t context -> HField t a -> context a
hfield (HConstrainTable t (ComposeConstraint f c) =>
t (Dict (ComposeConstraint f c))
forall (t :: HTable) (c :: * -> Constraint).
(HTable t, HConstrainTable t c) =>
t (Dict c)
hdicts @_ @(ComposeConstraint f c)) HField t a
j of
        Dict (ComposeConstraint f c) a
Dict -> Dict c a
forall a (c :: a -> Constraint) (a :: a). c a => Dict c a
Dict

  hspecs :: HMapTable f t Spec
hspecs = 
    t (Precompose f Spec) -> HMapTable f t Spec
forall (f :: * -> Context) (t :: HTable) (context :: Context).
t (Precompose f context) -> HMapTable f t context
HMapTable (t (Precompose f Spec) -> HMapTable f t Spec)
-> t (Precompose f Spec) -> HMapTable f t Spec
forall a b. (a -> b) -> a -> b
$ (forall a. HField t a -> Precompose f Spec a)
-> t (Precompose f Spec)
forall (t :: HTable) (context :: Context).
HTable t =>
(forall a. HField t a -> context a) -> t context
htabulate ((forall a. HField t a -> Precompose f Spec a)
 -> t (Precompose f Spec))
-> (forall a. HField t a -> Precompose f Spec a)
-> t (Precompose f Spec)
forall a b. (a -> b) -> a -> b
$ Spec (Eval (f a)) -> Precompose f Spec a
forall (f :: * -> Context) (g :: Context) x.
g (Eval (f x)) -> Precompose f g x
Precompose (Spec (Eval (f a)) -> Precompose f Spec a)
-> (HField t a -> Spec (Eval (f a)))
-> HField t a
-> Precompose f Spec a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x. MapSpec f => Spec x -> Spec (Eval (f x))
forall (f :: * -> Context) x.
MapSpec f =>
Spec x -> Spec (Eval (f x))
mapInfo @f (Spec a -> Spec (Eval (f a)))
-> (HField t a -> Spec a) -> HField t a -> Spec (Eval (f a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t Spec -> HField t a -> Spec a
forall (t :: HTable) (context :: Context) a.
HTable t =>
t context -> HField t a -> context a
hfield t Spec
forall (t :: HTable). HTable t => t Spec
hspecs
  {-# INLINABLE hspecs #-}


type MapSpec :: (Type -> Exp Type) -> Constraint
class MapSpec f where
  mapInfo :: Spec x -> Spec (Eval (f x))


type ComposeConstraint :: (Type -> Exp Type) -> (Type -> Constraint) -> Type -> Constraint
class c (Eval (f a)) => ComposeConstraint f c a
instance c (Eval (f a)) => ComposeConstraint f c a


hproject :: ()
  => (forall ctx. t ctx -> t' ctx)
  -> HMapTable f t context -> HMapTable f t' context
hproject :: (forall (ctx :: Context). t ctx -> t' ctx)
-> HMapTable f t context -> HMapTable f t' context
hproject forall (ctx :: Context). t ctx -> t' ctx
f (HMapTable t (Precompose f context)
a) = t' (Precompose f context) -> HMapTable f t' context
forall (f :: * -> Context) (t :: HTable) (context :: Context).
t (Precompose f context) -> HMapTable f t context
HMapTable (t (Precompose f context) -> t' (Precompose f context)
forall (ctx :: Context). t ctx -> t' ctx
f t (Precompose f context)
a)