{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for 'Subable'.
module Hcompta.LCC.Sym.Subable 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_Subable'
class Sym_Subable term where
	(-) :: Subable n => term n -> term n -> term n; infixl 6 -
	default (-) :: (Trans t term, Subable n) => t term n -> t term n -> t term n
	(-) = trans_map2 (-)

type instance Sym_of_Iface (Proxy Subable) = Sym_Subable
type instance TyConsts_of_Iface (Proxy Subable) = Proxy Subable ': TyConsts_imported_by (Proxy Subable)
type instance TyConsts_imported_by (Proxy Subable) = '[]

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

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

instance Proj_TyConC cs (Proxy Subable)
data instance TokenT meta (ts::[*]) (Proxy Subable)
 = Token_Term_Subable_add (EToken meta ts)
deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Subable))
deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Subable))
instance -- CompileI
 ( Inj_TyConst cs Subable
 , Inj_TyConst cs (->)
 , Proj_TyCon  cs
 , Compile cs is
 ) => CompileI cs is (Proxy Subable) where
	compileI tok ctx k =
		case tok of
		 Token_Term_Subable_add tok_a -> op2_from tok_a (-)
		where
		op2_from tok_a
		 (op::forall term a. (Sym_Subable term, Subable a)
			 => term a -> term a -> term a) =
		 -- (-) :: Subable a => a -> a -> a
			compileO tok_a ctx $ \ty_a (TermO a) ->
			check_TyCon (At (Just tok_a) (ty @Subable :$ ty_a)) $ \TyCon ->
			k (ty_a ~> ty_a) $ TermO $
			 \c -> lam $ \y -> op (a c) y
instance -- TokenizeT
 Inj_Token meta ts Subable =>
 TokenizeT meta ts (Proxy Subable) where
	tokenizeT _t = mempty
	 { tokenizers_infix = tokenizeTMod []
		 [ tokenize1 "-" (infixL 6) Token_Term_Subable_add
		 ]
	 }
instance Gram_Term_AtomsT meta ts (Proxy Subable) g