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

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

import Language.Symantic
import Language.Symantic.Lib.Function (a0, b1)

-- * Class 'Sym_Functor'
type instance Sym Functor = Sym_Functor
class Sym_Functor term where
	fmap :: Functor f => term (a -> b) -> term (f a) -> term (f b)
	default fmap :: Sym_Functor (UnT term) => Trans term => Functor f => term (a -> b) -> term (f a) -> term (f b)
	fmap = trans2 fmap
	
	(<$>) :: (Sym_Functor term, Functor f) => term (a -> b) -> term (f a) -> term (f b); infixl 4 <$>
	(<$>) = fmap
	
	(<$) :: Functor f => term a -> term (f b) -> term (f a); infixl 4 <$
	default (<$) :: Sym_Lambda term => Functor f => term a -> term (f b) -> term (f a)
	(<$) x = fmap (lam (Fun.const x))

-- Interpreting
instance Sym_Functor Eval where
	fmap  = eval2 Functor.fmap
	(<$)  = eval2 (Functor.<$)
instance Sym_Functor View where
	fmap  = view2 "fmap"
	(<$>) = viewInfix "<$>" (infixL 4)
	(<$)  = viewInfix "<$"  (infixL 4)
instance (Sym_Functor r1, Sym_Functor r2) => Sym_Functor (Dup r1 r2) where
	fmap = dup2 @Sym_Functor fmap
	(<$) = dup2 @Sym_Functor (<$)

-- Transforming
instance (Sym_Functor term, Sym_Lambda term) => Sym_Functor (BetaT term) where
	(<$>) = trans2 (<$>)
	(<$)  = trans2 (<$)

-- Typing
instance NameTyOf Functor where
	nameTyOf _c = ["Functor"] `Mod` "Functor"
instance FixityOf Functor
instance ClassInstancesFor Functor
instance TypeInstancesFor Functor

-- Compiling
instance Gram_Term_AtomsFor src ss g Functor
instance (Source src, SymInj ss Functor) => ModuleFor src ss Functor where
	moduleFor = ["Functor"] `moduleWhere`
	 [ "fmap" := teFunctor_fmap
	 , "<$"  `withInfixL` 4 := teFunctor_const
	 , "<$>" `withInfixL` 4 := teFunctor_fmap_infix
	 ]

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

f1 :: Source src => LenInj vs => KindInj (K f) =>
      Type src (a ': Proxy f ': vs) f
f1 = tyVar "f" $ VarS varZ

f2 :: Source src => LenInj vs => KindInj (K f) =>
      Type src (a ': b ': Proxy f ': vs) f
f2 = tyVar "f" $ VarS $ VarS varZ

-- ** 'Term's
teFunctor_fmap, teFunctor_fmap_infix :: TermDef Functor '[Proxy a, Proxy b, Proxy f] (Functor f #> ((a -> b) -> f a -> f b))
teFunctor_fmap = Term (tyFunctor f2) ((a0 ~> b1) ~> f2 `tyApp` a0 ~> f2 `tyApp` b1) $ teSym @Functor $ lam2 fmap
teFunctor_fmap_infix = Term (tyFunctor f2) ((a0 ~> b1) ~> f2 `tyApp` a0 ~> f2 `tyApp` b1) $ teSym @Functor $ lam2 (<$>)

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