{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for 'Applicative'.
module Language.Symantic.Lib.Applicative where

import Control.Applicative (Applicative)
import Prelude hiding (Functor(..), (<$>), Applicative(..), id, const)
import qualified Control.Applicative as Applicative
import qualified Data.Function as Fun

import Language.Symantic
import Language.Symantic.Lib.Function (a0, b1)
import Language.Symantic.Lib.Functor (Sym_Functor(..), (<$>), f1, f2)

-- * Class 'Sym_Applicative'
type instance Sym (Proxy Applicative) = 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 <*>
	(*>)  :: 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 <*
	
	default pure  :: Sym_Applicative (UnT term) => Trans term => Applicative f => term a -> term (f a)
	default (<*>) :: Sym_Applicative (UnT term) => Trans term => Applicative f => term (f (a -> b)) -> term (f a) -> term (f b)
	default (*>)  :: Sym_Lambda term => Applicative f => term (f a) -> term (f b) -> term (f b)
	default (<*)  :: Sym_Lambda term => Applicative f => term (f a) -> term (f b) -> term (f a)
	
	pure   = trans1 pure
	(<*>)  = trans2 (<*>)
	x *> y = lam1 Fun.id    <$  x <*> y
	x <* y = lam2 Fun.const <$> x <*> y

-- Interpreting
instance Sym_Applicative Eval where
	pure  = eval1 Applicative.pure
	(<*>) = eval2 (Applicative.<*>)
instance Sym_Applicative View where
	pure  = view1 "pure"
	(<*>) = viewInfix "<*>" (infixL 4)
	(<* ) = viewInfix "<*"  (infixL 4)
	( *>) = viewInfix "*>"  (infixL 4)
instance (Sym_Applicative r1, Sym_Applicative r2, Sym_Lambda r1, Sym_Lambda r2) => Sym_Applicative (Dup r1 r2) where
	pure  = dup1 @Sym_Applicative pure
	(<*>) = dup2 @Sym_Applicative (<*>)

-- Transforming
instance (Sym_Lambda term, Sym_Applicative term) => Sym_Applicative (BetaT term) where
	(<*) = trans2 (<*)
	(*>) = trans2 (*>)

-- Typing
instance FixityOf Applicative
instance ClassInstancesFor Applicative
instance TypeInstancesFor Applicative

-- Compiling
instance Gram_Term_AtomsFor src ss g Applicative
instance (Source src, Inj_Sym ss Applicative) => ModuleFor src ss Applicative where
	moduleFor = ["Applicative"] `moduleWhere`
	 [ "<*>" `withInfixL` 4 := teApplicative_app
	 , "<*"  `withInfixL` 4 := teApplicative_const
	 , "*>"  `withInfixL` 4 := teApplicative_tsnoc
	 ]

-- ** 'Type's
tyApplicative :: Source src => Type src vs a -> Type src vs (Applicative a)
tyApplicative a = tyConstLen @(K Applicative) @Applicative (lenVars a) `tyApp` a

-- ** 'Term's
teApplicative_pure :: TermDef Applicative '[Proxy a, Proxy f] (Applicative f #> (a -> f a))
teApplicative_pure = Term (tyApplicative f1) (a0 ~> f1 `tyApp` a0) $ teSym @Applicative $ lam1 pure

teApplicative_app :: TermDef Applicative '[Proxy a, Proxy b, Proxy f] (Applicative f #> (f (a -> b) -> f a -> f b))
teApplicative_app = Term (tyApplicative f2) (f2 `tyApp` (a0 ~> b1) ~> f2 `tyApp` a0 ~> f2 `tyApp` b1) $ teSym @Applicative $ lam2 (<*>)

teApplicative_const :: TermDef Applicative '[Proxy a, Proxy b1, Proxy f] (Applicative f #> (f a -> f b1 -> f a))
teApplicative_const = Term (tyApplicative f2) (f2 `tyApp` a0 ~> f2 `tyApp` b1 ~> f2 `tyApp` a0) $ teSym @Applicative $ lam2 (<*)

teApplicative_tsnoc :: TermDef Applicative '[Proxy a, Proxy b, Proxy f] (Applicative f #> (f a -> f b -> f b))
teApplicative_tsnoc = Term (tyApplicative f2) (f2 `tyApp` a0 ~> f2 `tyApp` b1 ~> f2 `tyApp` b1) $ teSym @Applicative $ lam2 (*>)