{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for 'Monad'.
module Language.Symantic.Lib.Monad where

import Control.Monad (Monad)
import qualified Control.Monad as Monad
import Data.Proxy
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (Monad(..))

import Language.Symantic.Parsing
import Language.Symantic.Typing
import Language.Symantic.Compiling
import Language.Symantic.Interpreting
import Language.Symantic.Transforming
import Language.Symantic.Lib.Applicative (Sym_Applicative)

-- * Class 'Sym_Monad'
class Sym_Applicative term => Sym_Monad term where
	return :: Monad m => term a -> term (m a)
	(>>=)  :: Monad m => term (m a) -> term (a -> m b) -> term (m b)
	join   :: Monad m => term (m (m a)) -> term (m a)
	when   :: Applicative f => term Bool -> term (f ()) -> term (f ())
	
	default return :: (Trans t term, Monad m)
	 => t term a -> t term (m a)
	default (>>=) :: (Trans t term, Monad m)
	 => t term (m a) -> t term (a -> m b) -> t term (m b)
	default join :: (Trans t term, Monad m)
	 => t term (m (m a)) -> t term (m a)
	default when :: (Trans t term, Applicative f)
	 => t term Bool -> t term (f ()) -> t term (f ())
	
	return = trans_map1 return
	(>>=)  = trans_map2 (>>=)
	join   = trans_map1 join
	when   = trans_map2 when

infixl 1 >>=

type instance Sym_of_Iface (Proxy Monad) = Sym_Monad
type instance Consts_of_Iface (Proxy Monad) = Proxy Monad ': Consts_imported_by Monad
type instance Consts_imported_by Monad =
 [ Proxy ()
 , Proxy Applicative
 , Proxy Bool
 ]

instance Sym_Monad HostI where
	return = Monad.liftM  Monad.return
	(>>=)  = Monad.liftM2 (Monad.>>=)
	join   = Monad.liftM  Monad.join
	when   = Monad.liftM2 Monad.when
instance Sym_Monad TextI where
	return = textI1 "return"
	(>>=)  = textI_infix ">>=" (infixL 1)
	join   = textI1 "join"
	when   = textI2 "when"
instance (Sym_Monad r1, Sym_Monad r2) => Sym_Monad (DupI r1 r2) where
	return = dupI1 (Proxy @Sym_Monad) return
	(>>=)  = dupI2 (Proxy @Sym_Monad) (>>=)
	join   = dupI1 (Proxy @Sym_Monad) join
	when   = dupI2 (Proxy @Sym_Monad) when

instance
 ( Read_TypeNameR Type_Name cs rs
 , Inj_Const cs Monad
 ) => Read_TypeNameR Type_Name cs (Proxy Monad ': rs) where
	read_typenameR _cs (Type_Name "Monad") k = k (ty @Monad)
	read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy Monad ': cs) where
	show_const ConstZ{} = "Monad"
	show_const (ConstS c) = show_const c

instance Proj_ConC cs (Proxy Monad)
data instance TokenT meta (ts::[*]) (Proxy Monad)
 = Token_Term_Monad_return (EToken meta '[Proxy Token_Type]) (EToken meta ts)
 | Token_Term_Monad_bind   (EToken meta ts) (EToken meta ts)
 | Token_Term_Monad_join   (EToken meta ts)
 | Token_Term_Monad_when   (EToken meta ts) (EToken meta ts)
deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Monad))
deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Monad))
instance -- CompileI
 ( Read_TypeName Type_Name (Consts_of_Ifaces is)
 , Inj_Const (Consts_of_Ifaces is) Monad
 , Inj_Const (Consts_of_Ifaces is) (->)
 , Inj_Const (Consts_of_Ifaces is) ()
 , Inj_Const (Consts_of_Ifaces is) Applicative
 , Inj_Const (Consts_of_Ifaces is) Bool
 , Proj_Con  (Consts_of_Ifaces is)
 , Compile is
 ) => CompileI is (Proxy Monad) where
	compileI tok ctx k =
		case tok of
		 Token_Term_Monad_return tok_ty_m tok_a ->
			-- return :: Monad m => a -> m a
			compile_type tok_ty_m $ \(ty_m::Type (Consts_of_Ifaces is) m) ->
			check_kind
			 (At Nothing (SKiType `SKiArrow` SKiType))
			 (At (Just tok_ty_m) $ kind_of ty_m) $ \Refl ->
			check_con (At (Just tok_ty_m) (ty @Monad :$ ty_m)) $ \Con ->
			compileO tok_a ctx $ \ty_a (TermO a) ->
			k (ty_m :$ ty_a) $ TermO $
			 \c -> return (a c)
		 Token_Term_Monad_bind tok_ma tok_a2mb ->
			-- (>>=) :: Monad m => m a -> (a -> m b) -> m b
			compileO tok_ma   ctx $ \ty_ma   (TermO ma) ->
			compileO tok_a2mb ctx $ \ty_a2mb (TermO a2mb) ->
			check_con1 (ty @Monad) (At (Just tok_ma) ty_ma) $ \Refl Con ty_ma_m ty_ma_a ->
			check_type2 (ty @(->)) (At (Just tok_a2mb) ty_a2mb) $ \Refl ty_a2mb_a ty_a2mb_mb ->
			check_type1 ty_ma_m (At (Just tok_a2mb) ty_a2mb_mb) $ \Refl _ty_a2mb_mb_b ->
			check_type
			 (At (Just tok_a2mb) ty_a2mb_a)
			 (At (Just tok_ma) ty_ma_a) $ \Refl ->
			k ty_a2mb_mb $ TermO $
			 \c -> (>>=) (ma c) (a2mb c)
		 Token_Term_Monad_join tok_mma ->
			-- join :: Monad m => m (m a) -> m a
			compileO tok_mma ctx $ \ty_mma (TermO mma) ->
			check_con1 (ty @Monad) (At (Just tok_mma) ty_mma) $ \Refl Con ty_mma_m ty_mma_ma ->
			check_type1 ty_mma_m (At (Just tok_mma) ty_mma_ma) $ \Refl _ty_mma_ma_a ->
			k ty_mma_ma $ TermO $
			 \c -> join (mma c)
		 Token_Term_Monad_when tok_cond tok_ok ->
			-- when :: Applicative f => Bool -> f () -> f ()
			compileO tok_cond ctx $ \ty_cond (TermO cond) ->
			compileO tok_ok   ctx $ \ty_ok   (TermO ok) ->
			check_con1 (ty @Applicative) (At (Just tok_ok) ty_ok) $ \Refl Con _ty_ok_f ty_ok_u ->
			check_type
			 (At Nothing (ty @Bool))
			 (At (Just tok_cond) ty_cond) $ \Refl ->
			check_type
			 (At Nothing (ty @()))
			 (At (Just tok_ok) ty_ok_u) $ \Refl ->
			k ty_ok $ TermO $
			 \c -> when (cond c) (ok c)
instance -- TokenizeT
 Inj_Token meta ts Monad =>
 TokenizeT meta ts (Proxy Monad) where
	tokenizeT _t = mempty
	 { tokenizers_infix = tokenizeTMod []
		 [ (Term_Name "Nothing",) Term_ProTok
			 { term_protok = \meta -> ProTokPi $ \m -> ProTokLam $ \a ->
				ProTok $ inj_etoken meta $ Token_Term_Monad_return m a
			 , term_fixity = infixN5
			 }
		 , tokenize2 ">>="  (infixL 1) Token_Term_Monad_bind
		 , tokenize1 "join" infixN5    Token_Term_Monad_join
		 , tokenize2 "when" infixN5    Token_Term_Monad_when
		 ]
	 }
instance Gram_Term_AtomsT meta ts (Proxy Monad) g