TrackedBuffers.hs

{-# LANGUAGE AllowAmbiguousTypes      #-}
{-# LANGUAGE BlockArguments           #-}
{-# LANGUAGE DataKinds                #-}
{-# LANGUAGE ExplicitForAll           #-}
{-# LANGUAGE FlexibleContexts         #-}
{-# LANGUAGE FlexibleInstances        #-}
{-# LANGUAGE FunctionalDependencies   #-}
{-# LANGUAGE GADTs                    #-}
{-# LANGUAGE PolyKinds                #-}
{-# LANGUAGE ScopedTypeVariables      #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications         #-}
{-# LANGUAGE TypeFamilies             #-}
{-# LANGUAGE TypeOperators            #-}
{-# LANGUAGE UndecidableInstances     #-}

module BufferResource where

-- base
import Data.Kind
  ( Type, Constraint )
import Data.Type.Bool
  ( If )
import Data.Type.Equality
  ( type (==) )
import GHC.TypeLits
  ( Symbol, CmpSymbol
  , TypeError, ErrorMessage(..)
  )

-- indexed
import Control.Monad.Indexed
  ( IxPointed(..), IxApplicative(..), IxMonad(..) )
import Data.Functor.Indexed
  ( IxFunctor(..) )

-- singletons
import Data.Singletons
  ( demote )
import Data.Singletons.Prelude.Ord
  ( POrd ( Compare ) )

-- transformers
import Control.Monad.IO.Class
  ( MonadIO )

-------------------------------------------------------------------------------

-- Type-level sorted lists of symbols, with insertion/deletion.

type     Insertion :: p -> [ p ] -> [ p ] -> Constraint
class    Insertion k as bs | k as -> bs, k bs -> as
instance Insertion k '[] '[k]
instance ( POrd p
         , cmp ~ ( k `Compare` a0 ), cmp ~ If ( k == b0 ) LT GT
         , InsertionWithCmp cmp k ( a0 ': as ) ( b0 ': b1 ': bs )
         )
      => Insertion k ( a0 ': as ) ( b0 ': b1 ': bs )

type     InsertionWithCmp :: Ordering -> p -> [ p ] -> [ p ] -> Constraint
class    InsertionWithCmp cmp k as bs | cmp k as -> bs, cmp k bs -> as
instance ( TypeError ( Text "'Insertion': Duplicate element " :<>: ShowType k :<>: Text " in type level list." )
         , as ~ bs, bs ~ as -- to satisfy the coverage condition (irrelevant given that a type error is thrown)
         )
      => InsertionWithCmp EQ k as bs
instance ( a ~ b, as ~ bs )           => InsertionWithCmp LT k ( a ': as ) ( k ': b ': bs )
instance ( a ~ b, Insertion k as bs ) => InsertionWithCmp GT k ( a ': as ) ( b ': bs )

-------------------------------------------------------------------------------
-- Indexed monad keeping track of bound buffers.

-- A buffer is given by a buffer target and a buffer name/index.
data Buffer = Buffer GL.BufferTarget Nat
-- derive a 'POrd' instance using singletons library Template Haskell

type BoundBuffers = [ Buffer ]

type  IxMonadTrack :: ( BoundBuffers -> BoundBuffers -> Type -> Type ) -> Constraint
class IxMonad m => IxMonadTrack m where
  bindBuffer
    :: forall tgt name buffers buffers'
    .  Insertion ( 'Buffer tgt name ) buffers buffers'
    => m buffers buffers' ()
  unbindBuffer
    :: forall tgt name buffers buffers'
    .  Insertion ( 'Buffer tgt name ) buffers' buffers
    => m buffers buffers' ()

type    TrackT :: ( Type -> Type ) -> BoundBuffers -> BoundBuffers -> Type -> Type
newtype TrackT m i j a = TrackT { runTrackT :: m a }
instance Functor m => IxFunctor     ( TrackT m ) where
  -- ...
instance Functor m => IxPointed     ( TrackT m ) where
  -- ...
instance Functor m => IxApplicative ( TrackT m ) where
  -- ...
instance Monad   m => IxMonad       ( TrackT m ) where
  -- ...
instance MonadIO m => IxMonadTrack  ( TrackT m ) where

  bindBuffer
    :: forall tgt name buffers buffers'
    .  Insertion ( 'Buffer tgt name ) buffers buffers'
    => TrackT m buffers buffers' ()
  bindBuffer   ( Buffer bufferTarget ) = TrackT ( GL.Raw.bindBuffer ( demote @tgt ) ( demote @name ) )

  unbindBuffer
    :: forall tgt name buffers buffers'
    .  Insertion ( 'Buffer tgt name ) buffers' buffers
    => TrackT m buffers buffers' ()
  unbindBuffer ( Buffer bufferTarget ) = TrackT ( GL.Raw.bindBuffer ( demote @tgt ) 0 )