{-# 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 Data.Typeable (Typeable)

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 sou) = Sym_Posting
class Sym_Posting term where
	posting_account :: term (Posting sou) -> term Account
	posting_amounts :: term (Posting sou) -> term Amounts
	default posting_account :: Sym_Posting (UnT term) => Trans term => term (Posting sou) -> term Account
	default posting_amounts :: Sym_Posting (UnT term) => Trans term => term (Posting sou) -> 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 Typeable sou => NameTyOf (Posting sou) where
	nameTyOf _c = ["Posting"] `Mod` "Posting"
instance (Typeable sou, Eq sou, Show sou) => ClassInstancesFor (Posting sou) where
	proveConstraintFor _ (TyConst _ _ q :$ c)
	 | Just HRefl <- proj_ConstKiTy @(K (Posting sou)) @(Posting sou) 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 sou) where

instance Gram_Term_AtomsFor src ss g (Posting sou)
instance
 ( Typeable sou
 , Eq sou
 , Show sou
 , Source src
 , SymInj ss (Posting sou)
 ) => ModuleFor src ss (Posting sou) where
	moduleFor = ["Posting"] `moduleWhere`
	 [ "account" := tePosting_account @sou
	 , "amounts" := tePosting_amounts @sou
	 ]

tyPosting :: forall sou src vs. Eq sou => Show sou => Typeable sou => Source src => LenInj vs => Type src vs (Posting sou)
tyPosting = tyConst @(K (Posting sou)) @(Posting sou)

tePosting_account :: forall sou src ss ts. Eq sou => Show sou => Typeable sou => Source src => SymInj ss (Posting sou) =>
                     Term src ss ts '[] (() #> (Posting sou -> Account))
tePosting_account = Term noConstraint (tyPosting ~> tyAccount) $ teSym @(Posting sou) $ lam1 posting_account

tePosting_amounts :: forall sou src ss ts. Eq sou => Show sou => Typeable sou => Source src => SymInj ss (Posting sou) =>
                     Term src ss ts '[] (() #> (Posting sou -> Amounts))
tePosting_amounts = Term noConstraint (tyPosting ~> tyAmounts) $ teSym @(Posting sou) $ lam1 posting_amounts