{-# 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.Text (Text)
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (Functor(..), (<$>), Applicative(..), id, const, Monoid(..))

import Language.Symantic.Parsing
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 (Proxy @Sym_Applicative) pure
	(<*>) = dupI2 (Proxy @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 cs (Proxy Applicative)
data instance TokenT meta (ts::[*]) (Proxy Applicative)
 = Token_Term_Applicative_pure     (EToken meta '[Proxy Token_Type]) (EToken meta ts)
 | Token_Term_Applicative_ltstargt (EToken meta ts)
 | Token_Term_Applicative_stargt   (EToken meta ts) (EToken meta ts)
 | Token_Term_Applicative_ltstar   (EToken meta ts) (EToken meta ts)
deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Applicative))
deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Applicative))
instance -- CompileI
 ( Const_from Name_LamVar (Consts_of_Ifaces is)
 , Inj_Const  (Consts_of_Ifaces is) Applicative
 , Inj_Const  (Consts_of_Ifaces is) (->)
 , Proj_Con   (Consts_of_Ifaces is)
 , Compile is
 ) => CompileI is (Proxy Applicative) where
	compileI tok ctx k =
		case tok of
		 Token_Term_Applicative_pure tok_ty_f tok_a ->
			-- pure :: Applicative f => a -> f a
			compile_type tok_ty_f $ \(ty_f::Type (Consts_of_Ifaces is) f) ->
			check_kind
			 (At Nothing $ SKiType `SKiArrow` SKiType)
			 (At (Just tok_ty_f) $ kind_of ty_f) $ \Refl ->
			check_con (At (Just tok_ty_f) (ty @Applicative :$ ty_f)) $ \Con ->
			compileO tok_a ctx $ \ty_a (TermO a) ->
			k (ty_f :$ ty_a) $ TermO $
			 \c -> pure (a c)
		 Token_Term_Applicative_ltstargt tok_fa2b ->
			-- (<*>) :: Applicative f => f (a -> b) -> f a -> f b
			compileO tok_fa2b ctx $ \ty_fa2b (TermO fa2b) ->
			check_con1 (ty @Applicative)
			 (At (Just tok_fa2b) ty_fa2b) $ \Refl Con ty_fa2b_f ty_fa2b_a2b ->
			check_type2 (ty @(->)) (At (Just tok_fa2b) ty_fa2b_a2b) $ \Refl ty_fa2b_a ty_fa2b_b ->
			k (ty_fa2b_f :$ ty_fa2b_a ~> ty_fa2b_f :$ ty_fa2b_b) $ TermO $
			 \c -> lam $ \fa -> (<*>) (fa2b c) fa
		 Token_Term_Applicative_ltstar tok_fa tok_fb ->
			-- (<*) :: Applicative f => f a -> f b -> f a
			compileO tok_fa ctx $ \ty_fa (TermO fa) ->
			compileO tok_fb ctx $ \ty_fb (TermO fb) ->
			check_con1 (ty @Applicative)
			 (At (Just tok_fa) ty_fa) $ \Refl Con ty_fa_f _ty_fa_a ->
			check_type1 ty_fa_f (At (Just tok_fb) ty_fb) $ \Refl _ty_fb_b ->
			k ty_fa $ TermO $
			 \c -> (<*) (fa c) (fb c)
		 Token_Term_Applicative_stargt tok_fa tok_fb ->
			-- (*>) :: Applicative f => f a -> f b -> f b
			compileO tok_fa ctx $ \ty_fa (TermO fa) ->
			compileO tok_fb ctx $ \ty_fb (TermO fb) ->
			check_con1 (ty @Applicative)
			 (At (Just tok_fa) ty_fa) $ \Refl Con ty_fa_f _ty_fa_a ->
			check_type1 ty_fa_f (At (Just tok_fb) ty_fb) $ \Refl _ty_fb_b ->
			k ty_fb $ TermO $
			 \c -> (*>) (fa c) (fb c)