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

import Data.Monoid (Monoid)
import Prelude hiding (Monoid(..))
import qualified Data.Monoid as Monoid

import Language.Symantic
import Language.Symantic.Lib.Function (a0)

-- * Class 'Sym_Monoid'
type instance Sym Monoid = Sym_Monoid
class Sym_Monoid term where
	mempty  :: Monoid a => term a
	mappend :: Monoid a => term a -> term a -> term a
	default mempty  :: Sym_Monoid (UnT term) => Trans term => Monoid a => term a
	default mappend :: Sym_Monoid (UnT term) => Trans term => Monoid a => term a -> term a -> term a
	mempty  = trans mempty
	mappend = trans2 mappend

-- Interpreting
instance Sym_Monoid Eval where
	mempty  = Eval  Monoid.mempty
	mappend = eval2 Monoid.mappend
instance Sym_Monoid View where
	mempty  = view0 "mempty"
	mappend = view2 "mappend"
instance (Sym_Monoid r1, Sym_Monoid r2) => Sym_Monoid (Dup r1 r2) where
	mempty  = dup0 @Sym_Monoid mempty
	mappend = dup2 @Sym_Monoid mappend

-- Transforming
instance (Sym_Monoid term, Sym_Lambda term) => Sym_Monoid (BetaT term)

-- Typing
instance FixityOf Monoid
instance ClassInstancesFor Monoid
instance TypeInstancesFor Monoid

-- Compiling
instance Gram_Term_AtomsFor src ss g Monoid
instance (Source src, SymInj ss Monoid) => ModuleFor src ss Monoid where
	moduleFor = ["Monoid"] `moduleWhere`
	 [ "mempty"  := teMonoid_mempty
	 , "mappend" := teMonoid_mappend
	 ]

-- ** 'Type's
tyMonoid :: Source src => Type src vs a -> Type src vs (Monoid a)
tyMonoid a = tyConstLen @(K Monoid) @Monoid (lenVars a) `tyApp` a

-- ** 'Term's
teMonoid_mempty :: TermDef Monoid '[Proxy a] (Monoid a #> a)
teMonoid_mempty = Term (tyMonoid a0) a0 $ teSym @Monoid $ mempty

teMonoid_mappend :: TermDef Monoid '[Proxy a] (Monoid a #> (a -> a -> a))
teMonoid_mappend = Term (tyMonoid a0) (a0 ~> a0 ~> a0) $ teSym @Monoid $ lam2 mappend