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

import Control.Monad (Monad)
import qualified Control.Monad as Monad
import qualified Data.Function as Fun
import Data.Monoid ((<>))
import Data.Proxy
import Data.String (IsString)
import Data.Text (Text)
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (Monad(..))

import Language.Symantic.Typing
import Language.Symantic.Compiling.Term
import Language.Symantic.Compiling.Applicative (Sym_Applicative, tyApplicative)
import Language.Symantic.Compiling.Bool (tyBool)
import Language.Symantic.Interpreting
import Language.Symantic.Transforming.Trans

-- * 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)
	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 when :: (Trans t term, Applicative f)
	 => t term Bool -> t term (f ()) -> t term (f ())
	
	return = trans_map1 return
	(>>=)  = trans_map2 (>>=)
	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.>>=)
	when   = Monad.liftM2 Monad.when
instance Sym_Monad TextI where
	return = textI_app1 "return"
	(>>=)  = textI_infix ">>=" (Precedence 1)
	when (TextI cond) (TextI ok) =
		TextI $ \p v ->
			let p' = Precedence 2 in
			paren p p' $
			"when " <> cond p' v <>
			" " <> ok p' v
instance (Sym_Monad r1, Sym_Monad r2) => Sym_Monad (DupI r1 r2) where
	return = dupI1 sym_Monad return
	(>>=)  = dupI2 sym_Monad (>>=)
	when   = dupI2 sym_Monad when

instance Const_from Text cs => Const_from Text (Proxy Monad ': cs) where
	const_from "Monad" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Show_Const cs => Show_Const (Proxy Monad ': cs) where
	show_const ConstZ{} = "Monad"
	show_const (ConstS c) = show_const c

instance -- Proj_ConC
 Proj_ConC cs (Proxy Monad)
instance -- Term_fromI
 ( AST ast
 , Lexem ast ~ LamVarName
 , Const_from (Lexem ast) (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)
 , Term_from is ast
 ) => Term_fromI is (Proxy Monad) ast where
	term_fromI ast ctx k =
		case ast_lexem ast of
		 "return" -> return_from
		 ">>="    -> bind_from
		 "when"   -> when_from
		 _ -> Left $ Error_Term_unsupported
		where
		return_from =
		 -- return :: Monad m => a -> m a
			from_ast2 ast $ \ast_ty_m ast_a ->
			either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
			type_from ast_ty_m $ \ty_m -> Right $
			check_kind ast (SKiType `SKiArrow` SKiType) (At (Just ast_ty_m) ty_m) $ \Refl ->
			check_constraint (At (Just ast_ty_m) (tyMonad :$ ty_m)) $ \Con ->
			term_from ast_a ctx $ \ty_a (TermLC a) ->
			k (ty_m :$ ty_a) $ TermLC $
			 \c -> return (a c)
		bind_from =
		 -- (>>=) :: Monad m => m a -> (a -> m b) -> m b
			from_ast2 ast $ \ast_ma ast_a2mb ->
			term_from ast_ma   ctx $ \ty_ma   (TermLC ma) ->
			term_from ast_a2mb ctx $ \ty_a2mb (TermLC a2mb) ->
			check_constraint1 tyMonad ast_ma ty_ma $ \Refl Con ty_ma_m ty_ma_a ->
			check_type2 tyFun ast_a2mb ty_a2mb $ \Refl ty_a2mb_a ty_a2mb_mb ->
			check_type1 ty_ma_m ast_a2mb ty_a2mb_mb $ \Refl _ty_a2mb_mb_b ->
			check_type (At (Just ast_a2mb) ty_a2mb_a) (At (Just ast_ma) ty_ma_a) $ \Refl ->
			k ty_a2mb_mb $ TermLC $
			 \c -> (>>=) (ma c) (a2mb c)
		when_from =
		 -- when :: Applicative f => Bool -> f () -> f ()
			case ast_nodes ast of
			 [] -> Left $ Error_Term_Syntax $
				Error_Syntax_more_arguments_needed $ At (Just ast) 2
			 [ast_cond, ast_ok] ->
				term_from ast_cond ctx $ \ty_cond (TermLC cond) ->
				term_from ast_ok   ctx $ \ty_ok   (TermLC ok) ->
				check_constraint1 tyApplicative ast_ok ty_ok $ \Refl Con _ty_ok_f ty_ok_u ->
				check_type (At Nothing tyBool) (At (Just ast_cond) ty_cond) $ \Refl ->
				check_type (At Nothing tyUnit) (At (Just ast_ok) ty_ok_u) $ \Refl ->
				k ty_ok $ TermLC $
				 \c -> when (cond c) (ok c)
			 _ -> Left $ Error_Term_Syntax $
				Error_Syntax_too_many_arguments $ At (Just ast) 2

-- | The 'Monad' 'Type'
tyMonad :: Inj_Const cs Monad => Type cs Monad
tyMonad = TyConst inj_const

sym_Monad :: Proxy Sym_Monad
sym_Monad = Proxy

syMonad :: IsString a => [Syntax a] -> Syntax a
syMonad = Syntax "Monad"

syWhen :: IsString a => Syntax a -> Syntax a -> Syntax a
syWhen cond ok = Syntax "when" [cond, ok]