{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# 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.String (IsString)
import Data.Text (Text)
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (Monoid(..))

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 sym_Monoid mempty
	mappend = dupI2 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
 Proj_ConC cs (Proxy Monoid)
instance -- Term_fromI
 ( AST ast
 , Lexem ast ~ LamVarName
 , Const_from (Lexem ast) (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 ast
 ) => Term_fromI is (Proxy Monoid) ast where
	term_fromI ast ctx k =
		case ast_lexem ast of
		 "mempty"  -> mempty_from
		 "mappend" -> mappend_from
		 "<>"      -> mappend_from
		 _ -> Left $ Error_Term_unsupported
		where
		mempty_from =
		 -- mempty :: Monoid a => a
			from_ast1 ast $ \ast_ty_x as ->
			either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
			type_from ast_ty_x $ \ty_x -> Right $
			check_kind ast SKiType (At (Just ast_ty_x) ty_x) $ \Refl ->
			check_constraint (At (Just ast_ty_x) (tyMonoid :$ ty_x)) $ \Con ->
			k as ty_x $ TermLC $ Fun.const mempty
		mappend_from =
		 -- mappend :: Monoid a => a -> a -> a
			from_ast1 ast $ \ast_x as ->
			term_from ast_x ctx $ \ty_x (TermLC x) ->
			check_constraint (At (Just ast_x) (tyMonoid :$ ty_x)) $ \Con ->
			k as (ty_x ~> ty_x) $ TermLC $
			 \c -> lam $ \y -> mappend (x c) y

-- | The 'Monoid' 'Type'
tyMonoid :: Inj_Const cs Monoid => Type cs Monoid
tyMonoid = TyConst inj_const

sym_Monoid :: Proxy Sym_Monoid
sym_Monoid = Proxy

syMonoid :: IsString a => [Syntax a] -> Syntax a
syMonoid = Syntax "Monoid"