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

import Control.Monad
import qualified Data.Function as Fun
import Data.Monoid (Monoid)
import qualified Data.Monoid as Monoid
import Data.Proxy
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (Monoid(..))

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_Monoid'
class Sym_Monoid term where
	mempty  :: Monoid a => term a
	mappend :: Monoid a => term a -> term a -> term a
	default mempty  :: (Trans t term, Monoid a) => t term a
	default mappend :: (Trans t term, Monoid a) => t term a -> t term a -> t term a
	mempty  = trans_lift mempty
	mappend = trans_map2 mappend

type instance Sym_of_Iface (Proxy Monoid) = Sym_Monoid
type instance TyConsts_of_Iface (Proxy Monoid) = Proxy Monoid ': TyConsts_imported_by Monoid
type instance TyConsts_imported_by Monoid = '[]

instance Sym_Monoid HostI where
	mempty  = HostI Monoid.mempty
	mappend = liftM2 Monoid.mappend
instance Sym_Monoid TextI where
	mempty  = textI0 "mempty"
	mappend = textI2 "mappend"
instance (Sym_Monoid r1, Sym_Monoid r2) => Sym_Monoid (DupI r1 r2) where
	mempty  = dupI0 @Sym_Monoid mempty
	mappend = dupI2 @Sym_Monoid mappend

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

instance Proj_TyConC cs (Proxy Monoid)
data instance TokenT meta (ts::[*]) (Proxy Monoid)
 = Token_Term_Monoid_mempty  (EToken meta '[Proxy Token_Type])
 | Token_Term_Monoid_mappend (EToken meta ts)
deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Monoid))
deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Monoid))
instance -- CompileI
 ( Read_TyName TyName cs
 , Inj_TyConst        cs Monoid
 , Inj_TyConst        cs (->)
 , Proj_TyCon         cs
 , Compile cs is
 ) => CompileI cs is (Proxy Monoid) where
	compileI tok ctx k =
		case tok of
		 Token_Term_Monoid_mempty tok_ty_a ->
			-- mempty :: Monoid a => a
			compile_Type tok_ty_a $ \(ty_a::Type cs a) ->
			check_Kind
			 (At Nothing SKiType)
			 (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
			check_TyCon (At (Just tok_ty_a) (ty @Monoid :$ ty_a)) $ \TyCon ->
			k ty_a $ TermO $ Fun.const mempty
		 Token_Term_Monoid_mappend tok_a ->
			-- mappend :: Monoid a => a -> a -> a
			compileO tok_a ctx $ \ty_a (TermO x) ->
			check_TyCon (At (Just tok_a) (ty @Monoid :$ ty_a)) $ \TyCon ->
			k (ty_a ~> ty_a) $ TermO $
			 \c -> lam $ \y -> mappend (x c) y
instance -- TokenizeT
 Inj_Token meta ts Monoid =>
 TokenizeT meta ts (Proxy Monoid) where
	tokenizeT _t = Monoid.mempty
	 { tokenizers_infix = tokenizeTMod []
		 [ (Term_Name "mempty",) Term_ProTok
			 { term_protok = \meta -> ProTokPi $ \a ->
				ProTok $ inj_EToken meta $ Token_Term_Monoid_mempty a
			 , term_fixity = infixN5
			 }
		 , tokenize1 "mappend" infixN5 Token_Term_Monoid_mappend
		 ]
	 }
instance Gram_Term_AtomsT meta ts (Proxy Monoid) g