{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# 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 Data.Proxy (Proxy(..))
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding ((<$>), Monad(..))

import Language.Symantic.Type
import Language.Symantic.Trans.Common
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

-- * Class 'Sym_Monad'
-- | Symantic.
class
 ( Sym_Monad_Lam (Lambda_from_Repr repr) repr
 ) => Sym_Monad repr where
	return :: Monad f => repr a -> repr (f a)
	default return :: (Trans t repr, Monad f) => t repr a -> t repr (f a)
	return = trans_map1 return

-- * Class 'Sym_Monad_Lam'
-- | Symantic requiring a 'Lambda'.
class Sym_Functor lam repr => Sym_Monad_Lam lam repr where
	(>>=) :: Monad m => repr (m a) -> repr (Lambda lam a (m b)) -> repr (m b)
	default (>>=) :: (Trans t repr, Monad m)
	 => t repr (m a) -> t repr (Lambda lam a (m b)) -> t repr (m b)
	(>>=) = trans_map2 (>>=)
infixl 1 >>=

-- * Type 'Expr_Monad'
-- | Expression.
data Expr_Monad (lam:: * -> *) (root:: *)
type instance Root_of_Expr      (Expr_Monad lam root)      = root
type instance Type_of_Expr      (Expr_Monad lam root)      = No_Type
type instance Sym_of_Expr       (Expr_Monad lam root) repr = (Sym_Monad repr, Sym_Monad_Lam lam repr)
type instance Error_of_Expr ast (Expr_Monad lam root)      = No_Error_Expr
instance Constraint_Type1 Monad (Type_Type0 px root)
instance Constraint_Type1 Monad (Type_Var1 root)

return_from
 :: forall root ty lam ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Monad lam root)
 , Eq_Type ty
 , Type1_from ast ty
 , Expr_from ast root
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 , Constraint_Type1 Monad ty
 ) => ast -> ast
 -> Expr_From ast (Expr_Monad lam 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) 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_constraint_type1 ex (Proxy::Proxy Monad) ast ty_fa $ \Dict ->
		k ty_fa $ Forall_Repr_with_Context $
		 \c -> return (a c)

bind_from
 :: forall root ty lam ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Monad lam root)
 , Eq_Type ty
 , Eq_Type1 ty
 , Expr_from ast root
 , Lift_Type   (Type_Fun lam) (Type_of_Expr root)
 , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
 , Unlift_Type1 (Type_of_Expr root)
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 , Constraint_Type1 Monad ty
 ) => ast -> ast
 -> Expr_From ast (Expr_Monad lam 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 $ \(Type_Type1 m ty_m_a, Lift_Type1 ty_m) ->
	check_type_fun ex ast ty_f $ \(Type_Type2 Proxy ty_f_a ty_f_mb
	 :: Type_Fun lam ty h_f) ->
	check_eq_type ex ast ty_m_a ty_f_a $ \Refl ->
	check_type1 ex ast ty_f_mb $ \(Type_Type1 _ ty_f_m_b, _) ->
	check_eq_type1 ex ast ty_ma ty_f_mb $ \Refl ->
	check_constraint_type1 ex (Proxy::Proxy Monad) ast ty_ma $ \Dict ->
	k (Type_Root $ ty_m $ Type_Type1 m ty_f_m_b) $ Forall_Repr_with_Context $
	 \c -> (>>=) (ma c) (f c)