{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Expression for 'Monad'.
module Language.Symantic.Expr.Monad where

import Control.Monad (Monad)
import qualified Control.Monad as Monad
import qualified Data.Function as Fun
import Data.Proxy (Proxy(..))
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding ((<$>), Monad(..))

import Language.Symantic.Type
import Language.Symantic.Repr
import Language.Symantic.Expr.Root
import Language.Symantic.Expr.Error
import Language.Symantic.Expr.From
import Language.Symantic.Expr.Lambda
import Language.Symantic.Expr.Functor
import Language.Symantic.Trans.Common

-- * Class 'Sym_Monad'
-- | Symantic.
class Sym_Functor repr => Sym_Monad repr where
	return :: Monad m => repr a -> repr (m a)
	(>>=)  :: Monad m => repr (m a) -> repr (a -> m b) -> repr (m b)
	
	default return :: (Trans t repr, Monad m)
	 => t repr a -> t repr (m a)
	default (>>=) :: (Trans t repr, Monad m)
	 => t repr (m a) -> t repr (a -> m b) -> t repr (m b)
	
	return = trans_map1 return
	(>>=)  = trans_map2 (>>=)
infixl 1 >>=
instance Sym_Monad Repr_Host where
	return = Monad.liftM Monad.return
	(>>=)  = Monad.liftM2 (Monad.>>=)
instance Sym_Monad Repr_Text where
	return = repr_text_app1 "return"
	(>>=)  = repr_text_infix ">>=" (Precedence 1)
instance (Sym_Monad r1, Sym_Monad r2) => Sym_Monad (Repr_Dup r1 r2) where
	return = repr_dup1 sym_Monad return
	(>>=)  = repr_dup2 sym_Monad (>>=)

sym_Monad :: Proxy Sym_Monad
sym_Monad = Proxy

-- * Type 'Expr_Monad'
-- | Expression.
data Expr_Monad (root:: *)
type instance Root_of_Expr      (Expr_Monad root)      = root
type instance Type_of_Expr      (Expr_Monad root)      = No_Type
type instance Sym_of_Expr       (Expr_Monad root) repr = (Sym_Monad repr)
type instance Error_of_Expr ast (Expr_Monad root)      = No_Error_Expr

return_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Monad root)
 , Type0_Eq ty
 , Type1_From ast ty
 , Type1_Constraint Monad ty
 , Expr_From ast root
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast -> ast
 -> ExprFrom ast (Expr_Monad root) hs ret
return_from ast_f ast_a ex ast ctx k =
 -- return :: Monad f => a -> f a
	either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) Fun.id $
	type1_from (Proxy::Proxy ty) ast_f $ \_f ty_f -> Right $
		expr_from (Proxy::Proxy root) ast_a ctx $
		 \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
		let ty_fa = ty_f ty_a in
		check_type1_constraint ex (Proxy::Proxy Monad) ast ty_fa $ \Dict ->
		k ty_fa $ Forall_Repr_with_Context $
		 \c -> return (a c)

bind_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Monad root)
 , Type0_Eq ty
 , Type1_Eq ty
 , Expr_From ast root
 , Type0_Lift   Type_Fun (Type_of_Expr root)
 , Type0_Unlift Type_Fun (Type_of_Expr root)
 , Type1_Unlift (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 , Type1_Constraint Monad ty
 ) => ast -> ast
 -> ExprFrom ast (Expr_Monad root) hs ret
bind_from ast_ma ast_f ex ast ctx k =
 -- (>>=) :: Monad m => m a -> (a -> m b) -> m b
	expr_from (Proxy::Proxy root) ast_ma ctx $
	 \(ty_ma::ty h_ma) (Forall_Repr_with_Context ma) ->
	expr_from (Proxy::Proxy root) ast_f ctx $
	 \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
	check_type1 ex ast ty_ma $ \(Type1 m ty_m_a, Type1_Lift ty_m) ->
	check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_a ty_f_mb) ->
	check_type0_eq ex ast ty_m_a ty_f_a $ \Refl ->
	check_type1 ex ast ty_f_mb $ \(Type1 _ ty_f_m_b, _) ->
	check_type1_eq ex ast ty_ma ty_f_mb $ \Refl ->
	check_type1_constraint ex (Proxy::Proxy Monad) ast ty_ma $ \Dict ->
	k (Type_Root $ ty_m $ Type1 m ty_f_m_b) $ Forall_Repr_with_Context $
	 \c -> (>>=) (ma c) (f c)