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

import Data.Eq (Eq)
import Data.Function (($))
import Data.Maybe (Maybe(..))
import Text.Show (Show(..))

import Hcompta.LCC.Account
import Hcompta.LCC.Amount
import Hcompta.LCC.Posting (Posting)
import qualified Hcompta.LCC.Posting as LCC

import Hcompta.LCC.Sym.Account (tyAccount)
import Hcompta.LCC.Sym.Amount (tyAmounts)

import Language.Symantic

-- * Class 'Sym_Posting'
type instance Sym Posting = Sym_Posting
class Sym_Posting term where
	posting_account :: term Posting -> term Account
	posting_amounts :: term Posting -> term Amounts
	default posting_account :: Sym_Posting (UnT term) => Trans term => term Posting -> term Account
	default posting_amounts :: Sym_Posting (UnT term) => Trans term => term Posting -> term Amounts
	posting_account = trans1 posting_account
	posting_amounts = trans1 posting_amounts

instance Sym_Posting Eval where
	posting_account = eval1 LCC.posting_account
	posting_amounts = eval1 LCC.posting_amounts
instance Sym_Posting View where
	posting_account = view1 "Posting.account"
	posting_amounts = view1 "Posting.amounts"
instance (Sym_Posting r1, Sym_Posting r2) => Sym_Posting (Dup r1 r2) where
	posting_account = dup1 @Sym_Posting posting_account
	posting_amounts = dup1 @Sym_Posting posting_amounts
instance (Sym_Posting term, Sym_Lambda term) => Sym_Posting (BetaT term)

instance ClassInstancesFor Posting where
	proveConstraintFor _ (TyApp _ (TyConst _ _ q) c)
	 | Just HRefl <- proj_ConstKiTy @(K Posting) @Posting c
	 = case () of
		 _ | Just Refl <- proj_Const @Eq q   -> Just Dict
		   | Just Refl <- proj_Const @Show q -> Just Dict
		 _ -> Nothing
	proveConstraintFor _c _q = Nothing
instance TypeInstancesFor Posting where

instance Gram_Term_AtomsFor src ss g Posting
instance (Source src, Inj_Sym ss Posting) => ModuleFor src ss Posting where
	moduleFor = ["Posting"] `moduleWhere`
	 [ "account" := tePosting_account
	 , "amounts" := tePosting_amounts
	 ]

tyPosting :: Source src => Inj_Len vs => Type src vs Posting
tyPosting = tyConst @(K Posting) @Posting

tePosting_account :: TermDef Posting '[] (() #> (Posting -> Account))
tePosting_account = Term noConstraint (tyPosting ~> tyAccount) $ teSym @Posting $ lam1 posting_account

tePosting_amounts :: TermDef Posting '[] (() #> (Posting -> Amounts))
tePosting_amounts = Term noConstraint (tyPosting ~> tyAmounts) $ teSym @Posting $ lam1 posting_amounts