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

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

import Language.Symantic

-- * Class 'Sym_Negable'
class Sym_Negable term where
	neg :: Negable n => term n -> term n
	default neg :: (Trans t term, Negable n) => t term n -> t term n
	neg = trans_map1 neg

type instance Sym_of_Iface (Proxy Negable) = Sym_Negable
type instance TyConsts_of_Iface (Proxy Negable) = Proxy Negable ': TyConsts_imported_by (Proxy Negable)
type instance TyConsts_imported_by (Proxy Negable) = '[]

instance Sym_Negable HostI where
	neg = liftM quantity_neg
instance Sym_Negable TextI where
	neg = textI1 "-"
instance (Sym_Negable r1, Sym_Negable r2) => Sym_Negable (DupI r1 r2) where
	neg = dupI1 @Sym_Negable neg

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

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

instance -- CompileI
 ( Inj_TyConst cs Negable
 , Proj_TyCon  cs
 , Compile cs is
 ) => CompileI cs is (Proxy Negable) where
	compileI tok ctx k =
		case tok of
		 Token_Term_Negable_neg tok_a -> op1_from tok_a neg
		where
		op1_from tok_a
		 (op::forall term a. (Sym_Negable term, Negable a)
			 => term a -> term a) =
		 -- neg :: Negable a => a -> a
			compileO tok_a ctx $ \ty_a (TermO x) ->
			check_TyCon (At (Just tok_a) (ty @Negable :$ ty_a)) $ \TyCon ->
			k ty_a $ TermO $
			 \c -> op (x c)
instance -- TokenizeT
 Inj_Token meta ts Negable =>
 TokenizeT meta ts (Proxy Negable) where
	tokenizeT _t = mempty
	 { tokenizers_prefix = tokenizeTMod []
		 [ tokenize1 "-" (Prefix 10) Token_Term_Negable_neg
		 ]
	 }
instance Gram_Term_AtomsT meta ts (Proxy Negable) g