Types.hs-boot

{-# LANGUAGE AllowAmbiguousTypes      #-}
{-# LANGUAGE DataKinds                #-}
{-# LANGUAGE FlexibleInstances        #-}
{-# LANGUAGE GADTs                    #-}
{-# LANGUAGE PolyKinds                #-}
{-# LANGUAGE RoleAnnotations          #-}
{-# LANGUAGE ScopedTypeVariables      #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies             #-}
{-# LANGUAGE TypeOperators            #-}

module FIR.Prim.Types where

-- base
import Data.Kind
  ( Type )
import Data.Typeable
  ( Typeable )

-- text-short
import Data.Text.Short
  ( ShortText )

-- fir
import {-# SOURCE #-} Control.Type.Optic
  ( IndexChain )
import Data.Binary.Class.Put
  ( Put )
import Data.Function.Variadic
  ( ListVariadic )
import Data.Type.Known
  ( Known )
import Data.Type.Map
  ( (:->)((:->)) )
import {-# SOURCE #-} FIR.AST
import FIR.AST.Type
  ( AugType(Val) )
import {-# SOURCE #-} FIR.Prim.Struct
  ( StructFieldKind )
import qualified SPIRV.PrimTy   as SPIRV
import qualified SPIRV.ScalarTy as SPIRV

------------------------------------------------------------
-- singletons for primitive types

data SScalarTy :: Type -> Type where
type role SScalarTy nominal

data SPrimTy :: Type -> Type where
type role SPrimTy nominal

type family HasOpaqueType (a :: Type) :: Bool where ..

class ( Show ty
      , Eq ty, Ord ty, Typeable ty
      , ty ~ ListVariadic '[] ty
      )
    => PrimTy ty where
  type FieldsOfType ty fldTy :: [ IndexChain ]
  primTySing :: SPrimTy ty

class ( PrimTy ty
      , Put ty
      , HasOpaqueType ty ~ False
      )
    => ScalarTy ty where
  scalarTySing :: SScalarTy ty

class (ScalarTy ty, Integral ty) => IntegralTy ty

scalarTy :: forall ty. ScalarTy ty => SPIRV.ScalarTy
primTy   :: forall ty. PrimTy   ty => SPIRV.PrimTy

data SPrimTyMap :: [fld :-> Type] -> Type where
  SNil  :: SPrimTyMap '[]
  SCons :: (StructFieldKind fld, Known fld k, PrimTy a, PrimTyMap as)
        => SPrimTyMap ((k ':-> a) ': as)
type role SPrimTyMap nominal

class    (Typeable as, StructFieldKind fld) => PrimTyMap (as :: [fld :-> Type]) where
  primTyMapSing :: SPrimTyMap as

primTyMap :: forall (fld :: Type) (flds :: [fld :-> Type])
          .  PrimTyMap flds
          => [ (Maybe ShortText, SPIRV.PrimTy) ]

instance StructFieldKind fld => PrimTyMap ('[] :: [fld :-> Type]) where

instance forall ( fld :: Type           )
                ( k   :: fld            )
                ( a   :: Type           )
                ( as  :: [fld :-> Type] )
      . ( StructFieldKind fld
        , Typeable k
        , Known fld k
        , PrimTy a
        , PrimTyMap as
        )
       => PrimTyMap ((k ':-> a) ': as) where


type SPrimFunc :: (Type -> Type) -> Type
data SPrimFunc :: (Type -> Type) -> Type where
type role SPrimFunc nominal

type DistDict :: (Type -> Type) -> Type -> Type
data DistDict f a where
type role DistDict nominal nominal

class ( Applicative f
    --, forall a. (Syntactic a, Internal a ~ Val va, PrimTy va) => Syntactic (f a)
      ) => PrimFunc f where
  primFuncSing :: SPrimFunc f
  distDict     :: ( Syntactic a, Internal a ~ Val va, PrimTy va )
               => DistDict f a

primFuncName :: forall f. PrimFunc f => String