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

import Language.Symantic
import Language.Symantic.Lib (s0)

import Hcompta.Quantity as H hiding ((+=))
import qualified Hcompta.Quantity as H

-- * Class 'Sym_Sumable'
type instance Sym Sumable = Sym_Sumable
class Sym_Sumable term where
	(+=) :: Sumable s a => term s -> term a -> term s
	default (+=) :: Sym_Sumable (UnT term) => Trans term => Sumable s a => term s -> term a -> term s
	(+=) = trans2 (+=)

instance Sym_Sumable Eval where
	(+=) = eval2 (H.+=)
instance Sym_Sumable View where
	(+=) = viewInfix "+=" (infixN 4)
instance (Sym_Sumable r1, Sym_Sumable r2) => Sym_Sumable (Dup r1 r2) where
	(+=) = dup2 @Sym_Sumable (+=)
instance (Sym_Sumable term, Sym_Lambda term) => Sym_Sumable (BetaT term)

instance NameTyOf Sumable where
	nameTyOf _c = ["LCC"] `Mod` "Sumable"
instance FixityOf Sumable
instance ClassInstancesFor Sumable
instance TypeInstancesFor Sumable
instance Gram_Term_AtomsFor src ss g Sumable
instance (Source src, SymInj ss Sumable) => ModuleFor src ss Sumable where
	moduleFor = ["LCC"] `moduleWhere`
	 [ "+=" `withInfixN` 4 := teSumable_incBy
	 ]

tySumable :: Source src => Type src vs s -> Type src vs a -> Type src vs (Sumable s a)
tySumable s a = tyConstLen @(K Sumable) @Sumable (lenVars s) `tyApp` s `tyApp` a

teSumable_incBy :: TermDef Sumable '[Proxy s, Proxy a] (Sumable s a #> (s -> a -> s))
teSumable_incBy = Term (tySumable s0 a1) (s0 ~> a1 ~> s0) (teSym @Sumable (lam2 (+=)))

a1 :: Source src => LenInj vs => KindInj (K a) =>
      Type src (a0 ': Proxy a ': vs) a
a1 = tyVar "a" (VarS varZ)