{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for 'Functor'.
module Language.Symantic.Compiling.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.String (IsString)
import Data.Text (Text)
import Data.Type.Equality
import Prelude hiding (Functor(..))

import Language.Symantic.Typing
import Language.Symantic.Compiling.Term
import Language.Symantic.Interpreting
import Language.Symantic.Transforming.Trans

-- * 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 Consts_of_Iface (Proxy Functor) = Proxy Functor ': Consts_imported_by Functor
type instance Consts_imported_by Functor = '[]

instance Sym_Functor HostI where
	fmap = liftM2 Functor.fmap
	(<$) = liftM2 (Functor.<$)
instance Sym_Functor TextI where
	fmap = textI_app2 "fmap"
	(<$) = textI_infix "<$" (Precedence 4)
instance (Sym_Functor r1, Sym_Functor r2) => Sym_Functor (DupI r1 r2) where
	fmap = dupI2 sym_Functor fmap
	(<$) = dupI2 sym_Functor (<$)

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

instance Const_from Text cs => Const_from Text (Proxy Functor ': cs) where
	const_from "Functor" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Show_Const cs => Show_Const (Proxy Functor ': cs) where
	show_const ConstZ{} = "Functor"
	show_const (ConstS c) = show_const c

instance -- Proj_ConC
 Proj_ConC cs (Proxy Functor)
instance -- Term_fromI
 ( AST ast
 , Lexem ast ~ LamVarName
 , Inj_Const  (Consts_of_Ifaces is) Functor
 , Inj_Const  (Consts_of_Ifaces is) (->)
 , Proj_Con   (Consts_of_Ifaces is)
 , Term_from is ast
 ) => Term_fromI is (Proxy Functor) ast where
	term_fromI ast ctx k =
		case ast_lexem ast of
		 "fmap" -> fmap_from
		 "<$>"  -> fmap_from
		 "<$"   -> ltdollar_from
		 _ -> Left $ Error_Term_unsupported
		where
		fmap_from =
		 -- fmap :: Functor f => (a -> b) -> f a -> f b
			from_ast2 ast $ \ast_a2b ast_fa ->
			term_from ast_a2b ctx $ \ty_a2b (TermLC a2b) ->
			term_from ast_fa  ctx $ \ty_fa  (TermLC fa) ->
			check_type2 tyFun ast_a2b ty_a2b $ \Refl ty_a2b_a ty_a2b_b ->
			check_constraint1 tyFunctor ast_fa ty_fa $ \Refl Con ty_fa_f ty_fa_a ->
			check_type (At (Just ast_a2b) ty_a2b_a) (At (Just ast_fa) ty_fa_a) $ \Refl ->
			k (ty_fa_f :$ ty_a2b_b) $ TermLC $
			 \c -> fmap (a2b c) (fa c)
		ltdollar_from =
		 -- (<$) :: Functor f => a -> f b -> f a
			from_ast2 ast $ \ast_a ast_fb ->
			term_from ast_a  ctx $ \ty_a  (TermLC a) ->
			term_from ast_fb ctx $ \ty_fb (TermLC fb) ->
			check_constraint1 tyFunctor ast_fb ty_fb $ \Refl Con ty_fb_f _ty_fb_b ->
			k (ty_fb_f :$ ty_a) $ TermLC $
			 \c -> (<$) (a c) (fb c)

-- | The 'Functor' 'Type'
tyFunctor :: Inj_Const cs Functor => Type cs Functor
tyFunctor = TyConst inj_const

sym_Functor :: Proxy Sym_Functor
sym_Functor = Proxy

syFunctor :: IsString a => [Syntax a] -> Syntax a
syFunctor = Syntax "Functor"