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

import Control.Monad (liftM2)
import qualified Data.Function as Fun
import Data.Functor (Functor)
import qualified Data.Functor as Functor
import Data.Proxy (Proxy(..))
import Data.Type.Equality
import Prelude hiding (Functor(..))

import Language.Symantic.Parsing
import Language.Symantic.Typing
import Language.Symantic.Compiling
import Language.Symantic.Interpreting
import Language.Symantic.Transforming
import Language.Symantic.Lib.Lambda

-- * Class 'Sym_Functor'
class Sym_Lambda term => Sym_Functor term where
	fmap :: Functor f => term (a -> b) -> term (f a) -> term (f b)
	default fmap
	 :: (Trans t term, Functor f)
	 => t term (a -> b)
	 -> t term (f a)
	 -> t term (f b)
	fmap = trans_map2 fmap
	
	(<$) :: Functor f => term a -> term (f b) -> term (f a)
	(<$) a = fmap (lam (Fun.const a))

infixl 4 <$

type instance Sym_of_Iface (Proxy Functor) = Sym_Functor
type instance TyConsts_of_Iface (Proxy Functor) = Proxy Functor ': TyConsts_imported_by Functor
type instance TyConsts_imported_by Functor = '[]

instance Sym_Functor HostI where
	fmap = liftM2 Functor.fmap
	(<$) = liftM2 (Functor.<$)
instance Sym_Functor TextI where
	fmap = textI2 "fmap"
	(<$) = textI_infix "<$" (infixL 4)
instance (Sym_Functor r1, Sym_Functor r2) => Sym_Functor (DupI r1 r2) where
	fmap = dupI2 (Proxy @Sym_Functor) fmap
	(<$) = dupI2 (Proxy @Sym_Functor) (<$)

-- | 'fmap' alias.
(<$>) :: (Sym_Functor term, Functor f)
 => term (a -> b) -> term (f a) -> term (f b)
(<$>) = fmap
infixl 4 <$>

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

instance Proj_TyConC cs (Proxy Functor)
data instance TokenT meta (ts::[*]) (Proxy Functor)
 = Token_Term_Functor_fmap   (EToken meta ts) (EToken meta ts)
 | Token_Term_Functor_const (EToken meta ts) (EToken meta ts)
deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Functor))
deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Functor))
instance -- CompileI
 ( Inj_TyConst  (TyConsts_of_Ifaces is) Functor
 , Inj_TyConst  (TyConsts_of_Ifaces is) (->)
 , Proj_TyCon   (TyConsts_of_Ifaces is)
 , Compile is
 ) => CompileI is (Proxy Functor) where
	compileI tok ctx k =
		case tok of
		 Token_Term_Functor_fmap tok_a2b tok_fa ->
			-- fmap :: Functor f => (a -> b) -> f a -> f b
			compileO tok_a2b ctx $ \ty_a2b (TermO a2b) ->
			compileO tok_fa  ctx $ \ty_fa  (TermO fa) ->
			check_TyEq2 (ty @(->))
			 (At (Just tok_a2b) ty_a2b) $ \Refl ty_a2b_a ty_a2b_b ->
			check_TyCon1 (ty @Functor)
			 (At (Just tok_fa) ty_fa) $ \Refl TyCon ty_fa_f ty_fa_a ->
			check_TyEq
			 (At (Just tok_a2b) ty_a2b_a)
			 (At (Just tok_fa) ty_fa_a) $ \Refl ->
			k (ty_fa_f :$ ty_a2b_b) $ TermO $
			 \c -> fmap (a2b c) (fa c)
		 Token_Term_Functor_const tok_a tok_fb ->
			-- (<$) :: Functor f => a -> f b -> f a
			compileO tok_a  ctx $ \ty_a  (TermO a) ->
			compileO tok_fb ctx $ \ty_fb (TermO fb) ->
			check_TyCon1 (ty @Functor)
			 (At (Just tok_fb) ty_fb) $ \Refl TyCon ty_fb_f _ty_fb_b ->
			k (ty_fb_f :$ ty_a) $ TermO $
			 \c -> (<$) (a c) (fb c)
instance -- TokenizeT
 Inj_Token meta ts Functor =>
 TokenizeT meta ts (Proxy Functor) where
	tokenizeT _t = mempty
	 { tokenizers_infix = tokenizeTMod []
		 [ tokenize2 "fmap" infixN5   Token_Term_Functor_fmap
		 , tokenize2 "<$"  (infixL 4) Token_Term_Functor_const
		 , tokenize2 "<$>" (infixL 4) Token_Term_Functor_fmap
		 ]
	 }
instance Gram_Term_AtomsT meta ts (Proxy Functor) g