{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for '(->)'.
module Language.Symantic.Lib.Lambda where

import qualified Data.Function as Fun
import qualified Data.Kind as Kind
import Data.Monoid ((<>))
import Data.Proxy (Proxy(..))
import qualified Data.Text as Text
import Data.Type.Equality ((:~:)(..))
import Prelude hiding ((^))

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


-- * Class 'Sym_Lambda'
class Sym_Lambda term where
	-- | /Lambda abstraction/.
	lam :: (term arg -> term res) -> term (arg -> res)
	default lam :: Trans t term => (t term arg -> t term res) -> t term (arg -> res)
	lam f = trans_lift $ lam $ trans_apply . f . trans_lift
	
	-- | /Lambda application/.
	(.$) :: term (arg -> res) -> term arg -> term res
	default (.$) :: Trans t term => t term (arg -> res) -> t term arg -> t term res
	infixr 0 .$
	(.$) f x = trans_lift (trans_apply f .$ trans_apply x)
	
	-- | Convenient 'lam' and '.$' wrapper.
	let_ :: term var -> (term var -> term res) -> term res
	let_ x y = lam y .$ x
	
	id :: term a -> term a
	id a = lam Fun.id .$ a
	
	const :: term a -> term b -> term a
	const a b = (lam (lam . Fun.const) .$ a) .$ b
	
	-- | /Lambda composition/.
	(^) :: term (b -> c) -> term (a -> b) -> term (a -> c)
	(^) f g = lam $ \a -> f .$ (g .$ a)
	infixr 9 ^
	
	flip :: term (a -> b -> c) -> term (b -> a -> c)
	flip f = lam $ \b -> lam $ \a -> (f .$ a) .$ b

type instance Sym_of_Iface (Proxy (->)) = Sym_Lambda
type instance TyConsts_of_Iface (Proxy (->)) = Proxy (->) ': TyConsts_imported_by (->)
type instance TyConsts_imported_by (->) =
 [ Proxy Applicative
 , Proxy Functor
 , Proxy Monad
 , Proxy Monoid
 ]

instance Sym_Lambda HostI where
	lam f = HostI (unHostI . f . HostI)
	(.$)  = (<*>)
instance Sym_Lambda TextI where
	lam f = TextI $ \po v ->
		let x = "x" <> Text.pack (show v) in
		infix_paren po op $
			"\\" <> x <> " -> " <>
			unTextI (f (TextI $ \_po _v -> x)) (op, L) (succ v)
		where op = infixN 1
	-- (.$) = textI_infix "$" (Precedence 0)
	(.$) (TextI a1) (TextI a2) = TextI $ \po v ->
		infix_paren po op $
			a1 (op, L) v <> " " <> a2 (op, R) v
		where op = infixN 10
	let_ e in_ =
		TextI $ \po v ->
			let x = "x" <> Text.pack (show v) in
			infix_paren po op $
			"let" <> " " <> x <> " = "
			 <> unTextI e (infixN 0, L) (succ v) <> " in "
			 <> unTextI (in_ (TextI $ \_po _v -> x)) (op, L) (succ v)
		where op = infixN 2
	(^)   = textI_infix "." (infixR 9)
	id    = textI1 "id"
	const = textI2 "const"
	flip  = textI1 "flip"
instance (Sym_Lambda r1, Sym_Lambda r2) => Sym_Lambda (DupI r1 r2) where
	lam f = dupI_1 lam_f `DupI` dupI_2 lam_f
		where lam_f = lam f
	(.$) = dupI2 @Sym_Lambda (.$)

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

instance -- Proj_TyConC (->)
 ( Proj_TyConst cs (->)
 , Proj_TyConsts cs (TyConsts_imported_by (->))
 , Proj_TyCon cs
 ) => Proj_TyConC cs (Proxy (->)) where
	proj_TyConC _ (TyConst q :$ (TyConst c :$ _r))
	 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_TyConst c (Proxy @(->))
	 = case () of
		 _ | Just Refl <- proj_TyConst q (Proxy @Functor)     -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Applicative) -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Monad)       -> Just TyCon
		 _ -> Nothing
	proj_TyConC _ (t@(TyConst q) :$ (TyConst c :$ _a :$ b))
	 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_TyConst c (Proxy @(->))
	 = case () of
		 _ | Just Refl <- proj_TyConst q (Proxy @Monoid)
		   , Just TyCon  <- proj_TyCon (t :$ b) -> Just TyCon
		 _ -> Nothing
	proj_TyConC _c _q = Nothing
deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy (->)))
deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy (->)))
instance -- CompileI (->)
 ( Inj_TyConst cs (->)
 , Read_TyName TyName cs
 , Compile cs is
 ) => CompileI cs is (Proxy (->)) where
	compileI tok ctx k =
		case tok of
		 Token_Term_Abst name_arg tok_ty_arg tok_body ->
			compile_Type tok_ty_arg $ \(ty_arg::Type cs h) ->
			check_Kind
			 (At Nothing SKiType)
			 (At (Just $ tok_ty_arg) $ kind_of ty_arg) $ \Refl ->
			compileO tok_body
			 (LamCtx_TypeS name_arg ty_arg ctx) $
			 \ty_res (TermO res) ->
			k (ty_arg ~> ty_res) $ TermO $
			 \c -> lam $ \arg ->
				res (arg `LamCtx_TermS` c)
		 Token_Term_App tok_lam tok_arg_actual ->
			compileO tok_lam ctx $ \ty_lam (TermO lam_) ->
			compileO tok_arg_actual ctx $ \ty_arg_actual (TermO arg_actual) ->
			check_TyEq2 (ty @(->)) (At (Just tok_lam) ty_lam) $ \Refl ty_arg ty_res ->
			check_TyEq
			 (At (Just tok_lam) ty_arg)
			 (At (Just tok_arg_actual) ty_arg_actual) $ \Refl ->
			k ty_res $ TermO $
			 \c -> lam_ c .$ arg_actual c
		 Token_Term_Let name tok_bound tok_body ->
			compileO tok_bound ctx $ \ty_bound (TermO bound) ->
			compileO tok_body (LamCtx_TypeS name ty_bound ctx) $
			 \ty_res (TermO res) ->
			k ty_res $ TermO $
			 \c -> let_ (bound c) $ \arg -> res (arg `LamCtx_TermS` c)
		 Token_Term_Var nam -> go nam ctx k
			where
			go :: forall meta lc ret ls rs.
			    TeName
			 -> LamCtx_Type cs is TeName lc
			 -> ( forall h.
			       Type cs (h::Kind.Type)
			    -> TermO lc h is ls rs
			    -> Either (Error_Term meta cs is) ret )
			 -> Either (Error_Term meta cs is) ret
			go name lc k' =
				case lc of
				 LamCtx_TypeZ -> Left $ Error_Term_unbound name
				 LamCtx_TypeS n typ _ | n == name ->
					k' typ $ TermO $ \(te `LamCtx_TermS` _) -> te
				 LamCtx_TypeS _n _ty lc' ->
					go name lc' $ \typ (TermO te::TermO lc' h is '[] is) ->
					k' typ $ TermO $ \(_ `LamCtx_TermS` c) -> te c
		 Token_Term_Compose tok_f tok_g ->
		 -- (.) :: (b -> c) -> (a -> b) -> a -> c
			compileO tok_f ctx $ \ty_f (TermO f) ->
			compileO tok_g ctx $ \ty_g (TermO g) ->
			check_TyEq2 (ty @(->)) (At (Just tok_f) ty_f) $ \Refl ty_f_b ty_c ->
			check_TyEq2 (ty @(->)) (At (Just tok_g) ty_g) $ \Refl ty_a ty_g_b ->
			check_TyEq
			 (At (Just tok_f) ty_f_b)
			 (At (Just tok_g) ty_g_b) $ \Refl ->
			k (ty_a ~> ty_c) $ TermO $
			 \c -> (^) (f c) (g c)
instance
 Inj_Token meta ts (->) =>
 TokenizeT meta ts (Proxy (->)) where
	tokenizeT _t = mempty
	 { tokenizers_infix = tokenizeTMod []
		 [ tokenize2 "." (infixR 9) Token_Term_Compose
		 , tokenize2 "$" (infixR 0) Token_Term_App
		 ]
	 }
instance Gram_Term_AtomsT meta ts (Proxy (->)) g

-- | The function 'Type' @(->)@,
-- with an infix notation more readable.
(~>) :: forall cs a b. Inj_TyConst cs (->)
 => Type cs a -> Type cs b -> Type cs (a -> b)
(~>) a b = ty @(->) :$ a :$ b
infixr 5 ~>