{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for 'Addable'.
module Hcompta.LCC.Sym.Addable where

import Control.Monad (liftM2)
import Data.Eq (Eq)
import Data.Function (($))
import Data.Maybe (Maybe(..))
import Data.Monoid (Monoid(..))
import Data.Proxy
import Text.Show (Show)
import qualified Prelude ()

import Hcompta.Quantity
import Language.Symantic
import Language.Symantic.Lib.Lambda

-- * Class 'Sym_Addable'
class Sym_Addable term where
	(+) :: Addable n => term n -> term n -> term n; infixl 6 +
	default (+) :: (Trans t term, Addable n) => t term n -> t term n -> t term n
	(+) = trans_map2 (+)

type instance Sym_of_Iface (Proxy Addable) = Sym_Addable
type instance TyConsts_of_Iface (Proxy Addable) = Proxy Addable ': TyConsts_imported_by (Proxy Addable)
type instance TyConsts_imported_by (Proxy Addable) = '[]

instance Sym_Addable HostI where
	(+) = liftM2 quantity_add
instance Sym_Addable TextI where
	(+) = textI_infix "+" (infixB L 6)
instance (Sym_Addable r1, Sym_Addable r2) => Sym_Addable (DupI r1 r2) where
	(+) = dupI2 @Sym_Addable (+)

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

instance Proj_TyConC cs (Proxy Addable)
data instance TokenT meta (ts::[*]) (Proxy Addable)
 = Token_Term_Addable_add (EToken meta ts)
deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Addable))
deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Addable))

instance -- CompileI
 ( Inj_TyConst cs Addable
 , Inj_TyConst cs (->)
 , Proj_TyCon  cs
 , Compile cs is
 ) => CompileI cs is (Proxy Addable) where
	compileI tok ctx k =
		case tok of
		 Token_Term_Addable_add tok_a -> op2_from tok_a (+)
		where
		op2_from tok_a
		 (op::forall term a. (Sym_Addable term, Addable a)
			 => term a -> term a -> term a) =
		 -- (+) :: Addable a => a -> a -> a
			compileO tok_a ctx $ \ty_a (TermO x) ->
			check_TyCon (At (Just tok_a) (ty @Addable :$ ty_a)) $ \TyCon ->
			k (ty_a ~> ty_a) $ TermO $
			 \c -> lam $ \y -> op (x c) y
instance -- TokenizeT
 Inj_Token meta ts Addable =>
 TokenizeT meta ts (Proxy Addable) where
	tokenizeT _t = mempty
	 { tokenizers_infix = tokenizeTMod []
		 [ tokenize1 "+" (infixB L 6) Token_Term_Addable_add
		 ]
	 }
instance Gram_Term_AtomsT meta ts (Proxy Addable) g