{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for 'Monoid'.
module Language.Symantic.Compiling.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.Text (Text)
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (Monoid(..))

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

-- * 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  = textI_app0 "mempty"
	mappend = textI_app2 "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.
(<>) ::
 ( Sym_Monoid term
 , Monoid a )
 => term a -> term a -> term a
(<>) = mappend
infixr 6 <>

instance Const_from Text cs => Const_from Text (Proxy Monoid ': cs) where
	const_from "Monoid" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
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 -- Term_fromI
 ( Const_from Name_LamVar (Consts_of_Ifaces is)
 , Inj_Const  (Consts_of_Ifaces is) Monoid
 , Inj_Const  (Consts_of_Ifaces is) (->)
 , Proj_Con   (Consts_of_Ifaces is)
 , Term_from is
 ) => Term_fromI is (Proxy Monoid) where
	term_fromI tok ctx k =
		case tok of
		 Token_Term_Monoid_mempty tok_ty_a ->
			-- mempty :: Monoid a => a
			type_from 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 $ TermLC $ Fun.const mempty
		 Token_Term_Monoid_mappend tok_a ->
			-- mappend :: Monoid a => a -> a -> a
			term_from tok_a ctx $ \ty_a (TermLC x) ->
			check_con (At (Just tok_a) (ty @Monoid :$ ty_a)) $ \Con ->
			k (ty_a ~> ty_a) $ TermLC $
			 \c -> lam $ \y -> mappend (x c) y