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

import Data.Maybe (Maybe(..))
import Text.Show (Show(..))

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

import Hcompta.LCC.Sym.Sumable (tySumable)
import Hcompta.LCC.Balance hiding (balance)
import qualified Hcompta as H ()
import qualified Hcompta.LCC.Balance as LCC

-- * Class 'Sym_Balance'
type instance Sym Balance = Sym_Balance
class Sym_Balance term where
	balance :: Balanceable a => term a -> term Balance
	default balance :: Sym_Balance (UnT term) => Trans term => Balanceable a => term a -> term Balance
	balance = trans1 balance

instance Sym_Balance Eval where
	balance = eval1 LCC.balance
instance Sym_Balance View where
	balance = view1 "balance"
instance (Sym_Balance r1, Sym_Balance r2) => Sym_Balance (Dup r1 r2) where
	balance = dup1 @Sym_Balance balance
instance (Sym_Balance term, Sym_Lambda term) => Sym_Balance (BetaT term)

instance NameTyOf Balance where
	nameTyOf _c = ["Balance"] `Mod` "Balance"
-- instance FixityOf Balance
instance ClassInstancesFor Balance where
	{-
	proveConstraintFor _ (TyConst _ _ c :$ q :@ db :@ b)
	 | Just HRefl <- proj_ConstKiTy @_ @RunQuery c
	 , Just HRefl <- proj_ConstKiTy @_ @Query q
	 , Just HRefl <- proj_ConstKiTy @_ @(LCC.LCC LCC.SourceRead) db
	 , Just HRefl <- proj_ConstKiTy @_ @Balance b
	 = Just Dict
	-}
	proveConstraintFor _ (TyConst _ _ q :$ b)
	 | Just HRefl <- proj_ConstKiTy @_ @Balance b
	 = case () of
		 _ | Just Refl <- proj_Const @Show q -> Just Dict
		 _ -> Nothing
	proveConstraintFor _c _q = Nothing
instance TypeInstancesFor Balance
instance Gram_Term_AtomsFor src ss g Balance
instance (Source src, SymInj ss Balance) => ModuleFor src ss Balance where
	moduleFor = ["Balance"] `moduleWhere`
	 [ "balance" := teBalance_balance
	 ]

tyBalance :: Source src => LenInj vs => Type src vs Balance
tyBalance = tyConst @(K Balance) @Balance

tyBalanceable :: Source src => Type src vs a -> Type src vs (Balanceable a)
tyBalanceable a = tySumable (tyConstLen @(K Balance) @Balance (lenVars a)) a

teBalance_balance :: TermDef Balance '[Proxy a] (Balanceable a #> (a -> Balance))
teBalance_balance = Term (tyBalanceable a0) (a0 ~> tyBalance) (teSym @Balance (lam1 balance))