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

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

import Hcompta.Quantity

-- * Class 'Sym_Addable'
type instance Sym Addable = Sym_Addable
class Sym_Addable term where
	(+) :: Addable a => term a -> term a -> term a; infixl 6 +
	default (+) :: Sym_Addable (UnT term) => Trans term => Addable a => term a -> term a -> term a
	(+) = trans2 (+)

instance Sym_Addable Eval where
	(+) = eval2 quantity_add
instance Sym_Addable View where
	(+) = viewInfix "+" (infixB SideL 6)
instance (Sym_Addable r1, Sym_Addable r2) => Sym_Addable (Dup r1 r2) where
	(+) = dup2 @Sym_Addable (+)
instance (Sym_Addable term, Sym_Lambda term) => Sym_Addable (BetaT term)

instance FixityOf Addable
instance ClassInstancesFor Addable
instance TypeInstancesFor Addable
instance Gram_Term_AtomsFor src ss g Addable
instance (Source src, SymInj ss Addable) => ModuleFor src ss Addable where
	moduleFor = ["Addable"] `moduleWhere`
	 [ "+" `withInfixB` (SideL, 6) := teAddable_add
	 ]

tyAddable :: Source src => Type src vs a -> Type src vs (Addable a)
tyAddable a = tyConstLen @(K Addable) @Addable (lenVars a) `tyApp` a

teAddable_add :: TermDef Addable '[Proxy a] (Addable a #> (a -> a -> a))
teAddable_add = Term (tyAddable a0) (a0 ~> a0 ~> a0) (teSym @Addable (lam2 (+)))