{-# 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 Consts_of_Iface (Proxy Monoid) = Proxy Monoid ': Consts_imported_by Monoid
type instance Consts_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 (Proxy @Sym_Monoid) mempty
	mappend = dupI2 (Proxy @Sym_Monoid) mappend

-- | 'mappend' alias.
--
-- TODO: move to Semigroup
(<>) ::
 ( Sym_Monoid term
 , Monoid a )
 => term a -> term a -> term a
(<>) = mappend
infixr 6 <>

instance
 ( Read_TypeNameR Type_Name cs rs
 , Inj_Const cs Monoid
 ) => Read_TypeNameR Type_Name cs (Proxy Monoid ': rs) where
	read_typenameR _cs (Type_Name "Monoid") k = k (ty @Monoid)
	read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy Monoid ': cs) where
	show_const ConstZ{} = "Monoid"
	show_const (ConstS c) = show_const c

instance Proj_ConC 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_TypeName Type_Name (Consts_of_Ifaces is)
 , Inj_Const  (Consts_of_Ifaces is) Monoid
 , Inj_Const  (Consts_of_Ifaces is) (->)
 , Proj_Con   (Consts_of_Ifaces is)
 , Compile is
 ) => CompileI 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 (Consts_of_Ifaces is) a) ->
			check_kind
			 (At Nothing SKiType)
			 (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
			check_con (At (Just tok_ty_a) (ty @Monoid :$ ty_a)) $ \Con ->
			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_con (At (Just tok_a) (ty @Monoid :$ ty_a)) $ \Con ->
			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
		 , tokenize1 "<>" (infixR 6) Token_Term_Monoid_mappend
		 ]
	 }
instance Gram_Term_AtomsT meta ts (Proxy Monoid) g