{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for 'Applicative'.
module Language.Symantic.Lib.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.Type.Equality ((:~:)(Refl))
import Prelude hiding (Functor(..), (<$>), Applicative(..), id, const)

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

-- * 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)
	infixl 4 <*>
	
	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); infixl 4 *>
	(<*) :: Applicative f => term (f a) -> term (f b) -> term (f a); infixl 4 <*
	x *> y = (lam Fun.id <$ x) <*> y
	x <* y = (lam (lam . Fun.const) <$> x) <*> y

type instance Sym_of_Iface (Proxy Applicative) = Sym_Applicative
type instance TyConsts_of_Iface (Proxy Applicative) = Proxy Applicative ': TyConsts_imported_by Applicative
type instance TyConsts_imported_by Applicative = '[]

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

instance
 ( Read_TyNameR TyName cs rs
 , Inj_TyConst cs Applicative
 ) => Read_TyNameR TyName cs (Proxy Applicative ': rs) where
	read_TyNameR _cs (TyName "Applicative") k = k (ty @Applicative)
	read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
instance Show_TyConst cs => Show_TyConst (Proxy Applicative ': cs) where
	show_TyConst TyConstZ{} = "Applicative"
	show_TyConst (TyConstS c) = show_TyConst c

instance Proj_TyConC 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_app   (EToken meta ts)
 | Token_Term_Applicative_tsnoc (EToken meta ts) (EToken meta ts)
 | Token_Term_Applicative_const (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
 ( Read_TyName TyName (TyConsts_of_Ifaces is)
 , Inj_TyConst  (TyConsts_of_Ifaces is) Applicative
 , Inj_TyConst  (TyConsts_of_Ifaces is) (->)
 , Proj_TyCon   (TyConsts_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 (TyConsts_of_Ifaces is) f) ->
			check_Kind
			 (At Nothing $ SKiType `SKiArrow` SKiType)
			 (At (Just tok_ty_f) $ kind_of ty_f) $ \Refl ->
			check_TyCon (At (Just tok_ty_f) (ty @Applicative :$ ty_f)) $ \TyCon ->
			compileO tok_a ctx $ \ty_a (TermO a) ->
			k (ty_f :$ ty_a) $ TermO $
			 \c -> pure (a c)
		 Token_Term_Applicative_app tok_fa2b ->
			-- (<*>) :: Applicative f => f (a -> b) -> f a -> f b
			compileO tok_fa2b ctx $ \ty_fa2b (TermO fa2b) ->
			check_TyCon1 (ty @Applicative)
			 (At (Just tok_fa2b) ty_fa2b) $ \Refl TyCon ty_fa2b_f ty_fa2b_a2b ->
			check_TyEq2 (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_const 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_TyCon1 (ty @Applicative)
			 (At (Just tok_fa) ty_fa) $ \Refl TyCon ty_fa_f _ty_fa_a ->
			check_TyEq1 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_tsnoc 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_TyCon1 (ty @Applicative)
			 (At (Just tok_fa) ty_fa) $ \Refl TyCon ty_fa_f _ty_fa_a ->
			check_TyEq1 ty_fa_f (At (Just tok_fb) ty_fb) $ \Refl _ty_fb_b ->
			k ty_fb $ TermO $
			 \c -> (*>) (fa c) (fb c)
instance -- TokenizeT
 Inj_Token meta ts Applicative =>
 TokenizeT meta ts (Proxy Applicative) where
	tokenizeT _t = mempty
	 { tokenizers_infix = tokenizeTMod []
		 [ tokenize1 "<*>" (infixL 4) Token_Term_Applicative_app
		 , tokenize2 "<*"  (infixL 4) Token_Term_Applicative_const
		 , tokenize2 "*>"  (infixL 4) Token_Term_Applicative_tsnoc
		 ]
	 }
instance Gram_Term_AtomsT meta ts (Proxy Applicative) g