{-# language DataKinds #-}
{-# language GADTs #-}
{-# language LambdaCase #-}
{-# language StandaloneKindSignatures #-}

module Rel8.Kind.Context
  ( Reifiable( contextSing )
  , SContext(..)
  , sReifiable
  , sLabelable
  )
where

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

-- rel8
import Rel8.Aggregate ( Aggregate )
import Rel8.Expr ( Expr )
import Rel8.Schema.Dict ( Dict( Dict ) )
import Rel8.Schema.Context ( Interpretation )
import Rel8.Schema.Context.Label ( Labelable )
import Rel8.Schema.Insert ( Insert )
import Rel8.Schema.Kind ( Context )
import Rel8.Schema.Name ( Name )
import Rel8.Schema.Reify ( Reify )
import Rel8.Schema.Result ( Result )


type SContext :: Context -> Type
data SContext context where
  SAggregate :: SContext Aggregate
  SExpr :: SContext Expr
  SInsert :: SContext Insert
  SName :: SContext Name
  SResult :: SContext Result
  SReify :: SContext context -> SContext (Reify context)


type Reifiable :: Context -> Constraint
class Interpretation context => Reifiable context where
  contextSing :: SContext context


instance Reifiable Aggregate where
  contextSing :: SContext Aggregate
contextSing = SContext Aggregate
SAggregate


instance Reifiable Expr where
  contextSing :: SContext Expr
contextSing = SContext Expr
SExpr


instance Reifiable Result where
  contextSing :: SContext Result
contextSing = SContext Result
SResult


instance Reifiable Insert where
  contextSing :: SContext Insert
contextSing = SContext Insert
SInsert


instance Reifiable Name where
  contextSing :: SContext Name
contextSing = SContext Name
SName


instance Reifiable context => Reifiable (Reify context) where
  contextSing :: SContext (Reify context)
contextSing = SContext context -> SContext (Reify context)
forall (context :: Context).
SContext context -> SContext (Reify context)
SReify SContext context
forall (context :: Context). Reifiable context => SContext context
contextSing


sReifiable :: SContext context -> Dict Reifiable context
sReifiable :: SContext context -> Dict Reifiable context
sReifiable = \case
  SContext context
SAggregate -> Dict Reifiable context
forall a (c :: a -> Constraint) (a :: a). c a => Dict c a
Dict
  SContext context
SExpr -> Dict Reifiable context
forall a (c :: a -> Constraint) (a :: a). c a => Dict c a
Dict
  SContext context
SInsert -> Dict Reifiable context
forall a (c :: a -> Constraint) (a :: a). c a => Dict c a
Dict
  SContext context
SName -> Dict Reifiable context
forall a (c :: a -> Constraint) (a :: a). c a => Dict c a
Dict
  SContext context
SResult -> Dict Reifiable context
forall a (c :: a -> Constraint) (a :: a). c a => Dict c a
Dict
  SReify SContext context
context -> case SContext context -> Dict Reifiable context
forall (context :: Context).
SContext context -> Dict Reifiable context
sReifiable SContext context
context of
    Dict Reifiable context
Dict -> Dict Reifiable context
forall a (c :: a -> Constraint) (a :: a). c a => Dict c a
Dict


sLabelable :: SContext context -> Dict Labelable context
sLabelable :: SContext context -> Dict Labelable context
sLabelable = \case
  SContext context
SAggregate -> Dict Labelable context
forall a (c :: a -> Constraint) (a :: a). c a => Dict c a
Dict
  SContext context
SExpr -> Dict Labelable context
forall a (c :: a -> Constraint) (a :: a). c a => Dict c a
Dict
  SContext context
SInsert -> Dict Labelable context
forall a (c :: a -> Constraint) (a :: a). c a => Dict c a
Dict
  SContext context
SName -> Dict Labelable context
forall a (c :: a -> Constraint) (a :: a). c a => Dict c a
Dict
  SContext context
SResult -> Dict Labelable context
forall a (c :: a -> Constraint) (a :: a). c a => Dict c a
Dict
  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 -> Dict Labelable context
forall a (c :: a -> Constraint) (a :: a). c a => Dict c a
Dict