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

import Data.Eq (Eq)
import Data.Function (($), (.))
import Data.Map.Strict (Map)
import Data.Maybe (Maybe(..))
import Data.Type.Equality ((:~:)(Refl))
import Text.Show (Show(..))

import Language.Symantic
import Language.Symantic.Lib (tyMap, tyList)

import Hcompta.LCC.Account
import Hcompta.LCC.Balance (Balance)
import Hcompta.LCC.Posting (Posting, Date, unPostings)
import Hcompta.LCC.Sym.Account (tyAccount)
import Hcompta.LCC.Sym.Date    (tyDate)
import Hcompta.LCC.Sym.Posting (tyPosting)
import Hcompta.LCC.Transaction (Transaction)
import qualified Hcompta as H
import qualified Hcompta.LCC.Transaction as LCC

-- * Type 'Postings'
type Postings = Map Account [Posting]

tyPostings :: Source src => LenInj vs => Type src vs Postings
tyPostings = tyMap tyAccount (tyList tyPosting)

-- * Class 'Sym_Transaction'
type instance Sym Transaction = Sym_Transaction
class Sym_Transaction term where
	transaction_date     :: term Transaction -> term Date
	transaction_postings :: term Transaction -> term Postings
	default transaction_date     :: Sym_Transaction (UnT term) => Trans term => term Transaction -> term Date
	default transaction_postings :: Sym_Transaction (UnT term) => Trans term => term Transaction -> term Postings
	transaction_date     = trans1 transaction_date
	transaction_postings = trans1 transaction_postings

instance Sym_Transaction Eval where
	transaction_date     = eval1 LCC.transaction_date
	transaction_postings = eval1 $ unPostings . LCC.transaction_postings
instance Sym_Transaction View where
	transaction_date     = view1 "Transaction.date"
	transaction_postings = view1 "Transaction.postings"
instance (Sym_Transaction r1, Sym_Transaction r2) => Sym_Transaction (Dup r1 r2) where
	transaction_date     = dup1 @Sym_Transaction transaction_date
	transaction_postings = dup1 @Sym_Transaction transaction_postings
instance (Sym_Transaction term, Sym_Lambda term) => Sym_Transaction (BetaT term)

instance NameTyOf Transaction where
	nameTyOf _c = ["LCC"] `Mod` "Transaction"
instance ClassInstancesFor Transaction where
	proveConstraintFor _ (TyApp _ (TyConst _ _ q) c)
	 | Just HRefl <- proj_ConstKiTy @(K Transaction) @Transaction c
	 = case () of
		 _ | Just Refl <- proj_Const @Eq   q -> Just Dict
		   | Just Refl <- proj_Const @Show q -> Just Dict
		 _ -> Nothing
	proveConstraintFor _ (TyApp _ (TyApp _ (TyConst _ _ q) b) a)
	 -- Sumable Balance a
	 | Just HRefl <- proj_ConstKi   @_ @H.Sumable q
	 , Just HRefl <- proj_ConstKiTy @_ @Balance b
	 = case a of
		 TyApp _ l t
		  -- [Transaction]
		  | Just HRefl <- proj_ConstKiTy @_ @[] l
		  , Just HRefl <- proj_ConstKiTy @_ @Transaction t
		  -> Just Dict
		 -- Map Date [Transaction]
		 TyApp _ (TyApp _ m d) (TyApp _ l t)
		  | Just HRefl <- proj_ConstKiTy @_ @Map m
		  , Just HRefl <- proj_ConstKiTy @_ @Date d
		  , Just HRefl <- proj_ConstKiTy @_ @[] l
		  , Just HRefl <- proj_ConstKiTy @_ @Transaction t
		  -> Just Dict
		 _ -> Nothing
	proveConstraintFor _c _q = Nothing
instance TypeInstancesFor Transaction

instance Gram_Term_AtomsFor src ss g Transaction
instance (Source src, SymInj ss Transaction) => ModuleFor src ss Transaction where
	moduleFor = ["LCC"] `moduleWhere`
	 [ "date"     := teTransaction_date
	 , "postings" := teTransaction_postings
	 ]

tyTransaction :: Source src => LenInj vs => Type src vs Transaction
tyTransaction = tyConst @(K Transaction) @Transaction

teTransaction_date :: TermDef Transaction '[] (() #> (Transaction -> Date))
teTransaction_date = Term noConstraint (tyTransaction ~> tyDate) $ teSym @Transaction $ lam1 transaction_date

teTransaction_postings :: TermDef Transaction '[] (() #> (Transaction -> Postings))
teTransaction_postings = Term noConstraint (tyTransaction ~> tyPostings) $ teSym @Transaction $ lam1 transaction_postings