{-# 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 'Applicative'.
module Language.Symantic.Compiling.Applicative where

import Control.Applicative (Applicative)
import qualified Control.Applicative as Applicative
import Control.Monad (liftM, liftM2)
import qualified Data.Function as Fun
import Data.Proxy
import Data.String (IsString)
import Data.Text (Text)
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (Functor(..), (<$>), Applicative(..), id, const, Monoid(..))

import Language.Symantic.Typing
import Language.Symantic.Compiling.Term
import Language.Symantic.Compiling.Functor (Sym_Functor(..), (<$>))
import Language.Symantic.Interpreting
import Language.Symantic.Transforming.Trans

-- * Class 'Sym_Applicative'
class Sym_Functor term => Sym_Applicative term where
	pure  :: Applicative f => term a -> term (f a)
	(<*>) :: Applicative f => term (f (a -> b)) -> term (f a) -> term (f b)
	
	default pure  :: (Trans t term, Applicative f) => t term a -> t term (f a)
	default (<*>) :: (Trans t term, Applicative f)
	 => t term (f (a -> b)) -> t term (f a) -> t term (f b)
	
	pure = trans_map1 pure
	(<*>) = trans_map2 (<*>)
	(*>) :: Applicative f => term (f a) -> term (f b) -> term (f b)
	(<*) :: Applicative f => term (f a) -> term (f b) -> term (f a)
	x *> y = (lam Fun.id <$ x) <*> y
	x <* y = (lam (lam . Fun.const) <$> x) <*> y

infixl 4  *>
infixl 4 <*
infixl 4 <*>

type instance Sym_of_Iface (Proxy Applicative) = Sym_Applicative
type instance Consts_of_Iface (Proxy Applicative) = Proxy Applicative ': Consts_imported_by Applicative
type instance Consts_imported_by Applicative = '[]

instance Sym_Applicative HostI where
	pure  = liftM Applicative.pure
	(<*>) = liftM2 (Applicative.<*>)
instance Sym_Applicative TextI where
	pure  = textI_app1 "pure"
	(<*>) = textI_infix "<*>" (Precedence 4)
	(<* ) = textI_infix "<*"  (Precedence 4)
	( *>) = textI_infix "*>"  (Precedence 4)
instance (Sym_Applicative r1, Sym_Applicative r2) => Sym_Applicative (DupI r1 r2) where
	pure  = dupI1 sym_Applicative pure
	(<*>) = dupI2 sym_Applicative (<*>)

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

instance -- Proj_ConC
 Proj_ConC cs (Proxy Applicative)
instance -- Term_fromI
 ( AST ast
 , Lexem ast ~ LamVarName
 , Const_from (Lexem ast) (Consts_of_Ifaces is)
 , Inj_Const  (Consts_of_Ifaces is) Applicative
 , Inj_Const  (Consts_of_Ifaces is) (->)
 , Proj_Con   (Consts_of_Ifaces is)
 , Term_from is ast
 ) => Term_fromI is (Proxy Applicative) ast where
	term_fromI ast ctx k =
		case ast_lexem ast of
		 "pure" -> pure_from
		 "<*>"  -> ltstargt_from
		 "*>"   -> stargt_from
		 "<*"   -> ltstar_from
		 _ -> Left $ Error_Term_unsupported
		where
		pure_from =
		 -- pure :: Applicative f => a -> f a
			from_ast2 ast $ \ast_ty_f ast_a as ->
			either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
			type_from ast_ty_f $ \ty_f -> Right $
			check_kind ast (SKiType `SKiArrow` SKiType) (At (Just ast_ty_f) ty_f) $ \Refl ->
			check_constraint (At (Just ast_ty_f) (tyApplicative :$ ty_f)) $ \Con ->
			term_from ast_a ctx $ \ty_a (TermLC a) ->
			k as (ty_f :$ ty_a) $ TermLC $
			 \c -> pure (a c)
		ltstargt_from =
		 -- (<*>) :: Applicative f => f (a -> b) -> f a -> f b
			from_ast1 ast $ \ast_fa2b as ->
			term_from ast_fa2b ctx $ \ty_fa2b (TermLC fa2b) ->
			check_constraint1 tyApplicative ast_fa2b ty_fa2b $ \Refl Con ty_fa2b_f ty_fa2b_a2b ->
			check_type2 tyFun ast_fa2b ty_fa2b_a2b $ \Refl ty_fa2b_a ty_fa2b_b ->
			k as (ty_fa2b_f :$ ty_fa2b_a ~> ty_fa2b_f :$ ty_fa2b_b) $ TermLC $
			 \c -> lam $ \fa -> (<*>) (fa2b c) fa
		stargt_from =
		 -- (*>) :: Applicative f => f a -> f b -> f b
			from_ast2 ast $ \ast_fa ast_fb as ->
			term_from ast_fa ctx $ \ty_fa (TermLC fa) ->
			term_from ast_fb ctx $ \ty_fb (TermLC fb) ->
			check_constraint1 tyApplicative ast_fa ty_fa $ \Refl Con ty_fa_f _ty_fa_a ->
			check_type1 ty_fa_f ast_fb ty_fb $ \Refl _ty_fb_b ->
			k as ty_fb $ TermLC $
			 \c -> (*>) (fa c) (fb c)
		ltstar_from =
		 -- (<*) :: Applicative f => f a -> f b -> f a
			from_ast2 ast $ \ast_fa ast_fb as ->
			term_from ast_fa ctx $ \ty_fa (TermLC fa) ->
			term_from ast_fb ctx $ \ty_fb (TermLC fb) ->
			check_constraint1 tyApplicative ast_fa ty_fa $ \Refl Con ty_fa_f _ty_fa_a ->
			check_type1 ty_fa_f ast_fb ty_fb $ \Refl _ty_fb_b ->
			k as ty_fa $ TermLC $
			 \c -> (<*) (fa c) (fb c)

-- | The 'Applicative' 'Type'
tyApplicative :: Inj_Const cs Applicative => Type cs Applicative
tyApplicative = TyConst inj_const

sym_Applicative :: Proxy Sym_Applicative
sym_Applicative = Proxy

syApplicative :: IsString a => [Syntax a] -> Syntax a
syApplicative = Syntax "Applicative"