{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-} -- NOTE: for CansMonadStateInstance
{-# OPTIONS_GHC -fno-warn-tabs #-}

-- | Collect in a 'Monad' stack, the states of 'MC.MonadState' 'Monad'
-- which are instances of a given type class.
module Language.LOL.Typing.Lib.Control.Monad.Classes.StateInstance where

import Control.Monad
import qualified Control.Monad.Classes as MC
import Control.Monad.Trans.Class
import qualified Control.Monad.Trans.State.Lazy as SL
import qualified Control.Monad.Trans.State.Strict as SS
import Data.Bool (Bool(..))
import GHC.Prim (Proxy#, proxy#, Constraint)

import Language.LOL.Typing.Lib.Control.Monad.Classes.Instance
import Language.LOL.Typing.Lib.Control.Monad.Classes.StateFix

-- * Class 'MonadStateInstance'

-- ** Type family 'CanMonadStateInstance'

-- | A close type family to know whether a 'Monad' @m@
-- support an effect 'eff' whose state is an instance of the type class @cl@.
--
-- NOTE: the closeness enables to define 'Class' instances
-- only for the states of the 'Monad's in a 'Monad' stack
-- which support the effects 'MC.EffState'.
type family CanMonadStateInstance (cl:: * -> Constraint) (m:: * -> *) (eff:: k) :: Bool where
	CanMonadStateInstance cl (SL.StateT s m) (MC.EffState  _s) = Class cl s
	CanMonadStateInstance cl (SS.StateT s m) (MC.EffState  _s) = Class cl s
	-- CanMonadStateInstance cl (SL.StateT s m) (MC.EffReader _s) = Class cl s
	-- CanMonadStateInstance cl (SS.StateT s m) (MC.EffReader _s) = Class cl s
	CanMonadStateInstance cl (StateLazyFixT s m) (MC.EffState  _s) = Class cl (s m)
	CanMonadStateInstance cl s eff = 'False

-- ** Type family 'CansMonadStateInstance'

-- | A close type family to know which 'Monad's in a 'Monad' stack @stack@
-- support an effect 'eff' whose state is an instance of the type class @cl@.
type family CansMonadStateInstance (cl:: * -> Constraint) (eff :: k) (stack :: * -> *) :: [Bool] where
	CansMonadStateInstance cl eff (t m) = CanMonadStateInstance cl (t m) eff ': CansMonadStateInstance cl eff m
	CansMonadStateInstance cl eff m     = CanMonadStateInstance cl m     eff ': '[]

-- | A type synonym to constrain a 'Monad' @m@
-- to support an 'MC.EffState' whose state is an instance of the type class @cl@.
type MonadStateInstance cl m
 =   MonadStateInstanceN cl (CansMonadStateInstance cl (MC.EffState ()) m) m

getInstance :: forall cl m. MonadStateInstance cl m => m [Instance cl]
getInstance = getInstanceN (proxy# :: Proxy# (CansMonadStateInstance cl (MC.EffState ()) m))

-- ** Class 'MonadStateInstanceN'

-- | A type class to recurse over the 'Monad' stack
-- to collect the states which are instance of the type class @cl@.
class Monad m => MonadStateInstanceN cl (cans::[Bool]) m where
	getInstanceN :: Proxy# cans -> m [Instance cl]

-- | Collect the lazy 'SL.StateT', and recurse.
instance (cl s, Monad m, MonadStateInstanceN cl cans m)
 => MonadStateInstanceN cl ('True ': cans) (SL.StateT s m) where
	getInstanceN _ = do
		s <- SL.get
		ss <- lift (getInstanceN (proxy# :: Proxy# cans))
		return (Instance s : ss)

-- | Collect the strict 'SS.StateT', and recurse.
instance (cl s, Monad m, MonadStateInstanceN cl cans m)
 => MonadStateInstanceN cl ('True ': cans) (SS.StateT s m) where
	getInstanceN _ = do
		s <- SS.get
		ss <- lift (getInstanceN (proxy# :: Proxy# cans))
		return (Instance s : ss)

-- | Collect the 'StateLazyFixT', and recurse.
instance (cl (s (StateLazyFixT s m)), Monad m, MonadStateInstanceN cl cans m)
 => MonadStateInstanceN cl ('True ': cans) (StateLazyFixT s m) where
	getInstanceN _ = do
		s <- StateLazyFixT SL.get
		ss <- lift (getInstanceN (proxy# :: Proxy# cans))
		return (Instance s : ss)

-- | Recurse the 'Monad' stack, passing over 'Monad' @t m@
-- such that 'CanMonadStateInstance' @cl@ @t m@ @MC.EffState ()@ @~@ 'False'.
instance
 ( Monad m
 , Monad (t m)
 , MonadTrans t
 , MonadStateInstanceN cl (can ': cans) m
 ) => MonadStateInstanceN cl ('False ': (can ': cans)) (t m) where
	getInstanceN _ = lift (getInstanceN (proxy# :: Proxy# (can ': cans)))

-- | Terminating instance, when the deepest 'Monad' on the stack
-- is such that 'CanMonadStateInstance' @cl@ @t m@ @MC.EffState ()@ @~@ 'False':
-- then there is no need to recurse,
-- and thus no 'MonadStateInstanceN' @cl@ @[]@ @m@ constraint to impose.
instance Monad m => MonadStateInstanceN cl ('False ': '[]) m where
	getInstanceN _ = return []