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

import Control.Monad (liftM)
import Data.Eq (Eq)
import Data.Either (Either)
import Data.Function (($))
import Data.Maybe (Maybe(..))
import Data.Monoid (Monoid(..))
import Data.Proxy
import Data.Type.Equality ((:~:)(Refl))
import Text.Show (Show(..))
import qualified Prelude ()

import Hcompta.LCC.Account
import Hcompta.LCC.Amount
import Hcompta.LCC.Posting (Posting)
import qualified Hcompta.LCC.Posting as LCC
import Language.Symantic
import qualified Language.Symantic.Lib as Sym
import Language.Symantic.Lib ((~>))

-- * Class 'Sym_Posting'
class Sym_Posting term where
	posting_account :: term Posting -> term Account
	posting_amounts :: term Posting -> term Amounts
	default posting_account :: Trans t term => t term Posting -> t term Account
	default posting_amounts :: Trans t term => t term Posting -> t term Amounts
	posting_account = trans_map1 posting_account
	posting_amounts = trans_map1 posting_amounts

type instance Sym_of_Iface (Proxy Posting) = Sym_Posting
type instance TyConsts_of_Iface (Proxy Posting) = Proxy Posting ': TyConsts_imported_by (Proxy Posting)
type instance TyConsts_imported_by (Proxy Posting) =
 [ Proxy Eq
 , Proxy Show
 ]

instance Sym_Posting HostI where
	posting_account = liftM LCC.posting_account
	posting_amounts = liftM LCC.posting_amounts
instance Sym_Posting TextI where
	posting_account = textI1 "posting_account"
	posting_amounts = textI1 "posting_amounts"
instance (Sym_Posting r1, Sym_Posting r2) => Sym_Posting (DupI r1 r2) where
	posting_account = dupI1 @Sym_Posting posting_account
	posting_amounts = dupI1 @Sym_Posting posting_amounts

instance
 ( Read_TyNameR TyName cs rs
 , Inj_TyConst cs Posting
 ) => Read_TyNameR TyName cs (Proxy Posting ': rs) where
	read_TyNameR _cs (TyName "Posting") k = k (ty @Posting)
	read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
instance Show_TyConst cs => Show_TyConst (Proxy Posting ': cs) where
	show_TyConst TyConstZ{} = "Posting"
	show_TyConst (TyConstS c) = show_TyConst c

instance Proj_TyFamC cs Sym.TyFam_MonoElement Posting

instance -- Proj_TyConC
 ( Proj_TyConst cs Posting
 , Proj_TyConsts cs (TyConsts_imported_by (Proxy Posting))
 ) => Proj_TyConC cs (Proxy Posting) where
	proj_TyConC _ (TyConst q :$ TyConst c)
	 | Just Refl <- eq_skind (kind_of_TyConst c) SKiType
	 , Just Refl <- proj_TyConst c (Proxy @Posting)
	 = case () of
		 _ | Just Refl <- proj_TyConst q (Proxy @Eq)   -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Show) -> Just TyCon
		 _ -> Nothing
	proj_TyConC _c _q = Nothing
data instance TokenT meta (ts::[*]) (Proxy Posting)
 = Token_Term_Posting_account
 | Token_Term_Posting_amounts
deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Posting))
deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Posting))

instance -- CompileI
 ( Inj_TyConst cs Posting
 , Inj_TyConst cs (->)
 , Inj_TyConst cs Account
 , Inj_TyConst cs Amounts
 , Proj_TyCon  cs
 , Compile cs is
 ) => CompileI cs is (Proxy Posting) where
	compileI
	 :: forall meta ctx ret ls rs.
	 TokenT meta is (Proxy Posting)
	 -> CompileT meta ctx ret cs is ls (Proxy Posting ': rs)
	compileI tok _ctx k =
		case tok of
		 Token_Term_Posting_account -> get (ty @Account) posting_account
		 Token_Term_Posting_amounts -> get (ty @Amounts) posting_amounts
		where
		get
		 :: forall a. Type cs a
		 -> (forall term. Sym_Posting term => term Posting -> term a)
		 -> Either (Error_Term meta cs is) ret
		get ty_a op =
			k (ty @Posting ~> ty_a) $ TermO $
			 \_c -> Sym.lam op
instance -- TokenizeT
 Inj_Token meta ts Posting =>
 TokenizeT meta ts (Proxy Posting) where
	tokenizeT _t = mempty
	 { tokenizers_infix = tokenizeTMod []
		 [ tokenize0 "posting_account" infixN5 Token_Term_Posting_account
		 , tokenize0 "posting_amounts" infixN5 Token_Term_Posting_amounts
		 ]
	 }
instance -- Gram_Term_AtomsT
 ( Alt g
 , Gram_Rule g
 , Gram_Lexer g
 , Gram_Meta meta g
 , Inj_Token meta ts Posting
 ) => Gram_Term_AtomsT meta ts (Proxy Posting) g where