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

import Data.Eq (Eq)
import Data.Function (($), (.))
import Data.Maybe (Maybe(..))
import Text.Show (Show(..))
import qualified Prelude ()
import Data.Typeable (Typeable)
import Data.Map.Strict (Map)
import System.IO (IO)

import Hcompta.LCC.Balance (Balance)
import Hcompta.LCC.Chart (Chart(..))
import Hcompta.LCC.Compta (Compta)
import Hcompta.LCC.IO (PathFile(..), FromFile)
import Hcompta.LCC.Journal (Journal)
import Hcompta.LCC.Posting (Date)
import Hcompta.LCC.Read (ComptaT, Comptable)
import Hcompta.LCC.Transaction (Transaction)
import Hcompta.LCC.Sym.Chart (tyChart)
import Hcompta.LCC.Sym.Date (tyDate)
import Hcompta.LCC.Sym.FileSystem (tyPathFile)
import Hcompta.LCC.Sym.IO (tyFromFile, fromFile, Sym_FromFile)
import Hcompta.LCC.Sym.Transaction (tyTransaction)
import qualified Hcompta as H
import qualified Hcompta.LCC.Journal as LCC
import qualified Hcompta.LCC.Compta  as LCC

import Language.Symantic
import Language.Symantic.Grammar
import Language.Symantic.Lib (a0, tyMap, tyList, tyIO)

-- * Class 'Sym_Compta'
type instance Sym (Compta src ss) = Sym_Compta
class Sym_FromFile term => Sym_Compta term where
	compta       :: Compta src ss j -> term (Compta src ss j)
	compta_chart :: term (Compta src ss j) -> term Chart
	default compta       :: Sym_Compta (UnT term) => Trans term => Compta src ss j -> term (Compta src ss j)
	default compta_chart :: Sym_Compta (UnT term) => Trans term => term (Compta src ss j) -> term Chart
	compta       = trans . compta
	compta_chart = trans1 compta_chart

instance Sym_Compta Eval where
	compta       = Eval
	compta_chart = eval1 LCC.compta_chart
instance Sym_Compta View where
	compta _     = View $ \_v _p -> "Compta.compta"
	compta_chart = view1 "Chart.compta_chart"
instance (Sym_Compta r1, Sym_Compta r2) => Sym_Compta (Dup r1 r2) where
	compta j     = compta j `Dup` compta j
	compta_chart = dup1 @Sym_Compta compta_chart
instance (Sym_Compta term, Sym_Lambda term) => Sym_Compta (BetaT term)

instance (Typeable src, Typeable ss) => NameTyOf (Compta src ss) where
	nameTyOf _c = ["Compta"] `Mod` "Compta"
instance FixityOf (Compta src ss)
instance Comptable src ss =>
         ClassInstancesFor (Compta src ss) where
	proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ c j))
	 | Just HRefl <- proj_ConstKiTy @(K (Compta src ss)) @(Compta src ss) c
	 = case () of
		 _ | Just Refl <- proj_Const @Eq q
		   , Just Dict <- proveConstraint (tq `tyApp` j) -> Just Dict
		   | Just Refl <- proj_Const @Show q
		   , Just Dict <- proveConstraint (tq `tyApp` j) -> Just Dict
		 _ -> Nothing
	proveConstraintFor _ (TyApp _ (TyApp _ tq@(TyConst _ _ q) b) (TyApp _ c a))
	 -- Sumable Balance (Compta src ss a)
	 | Just HRefl <- proj_ConstKi @_ @H.Sumable q
	 , Just HRefl <- proj_ConstKiTy @_ @Balance b
	 , Just HRefl <- proj_ConstKiTy @_ @(Compta src ss) c
	 , Just Dict <- proveConstraint (tq `tyApp` b `tyApp` a)
	 = Just Dict
	proveConstraintFor _ (TyApp _ (TyConst _ _ q) (TyApp _ c a))
	 -- FromFile (Compta src ss a)
	 | Just HRefl <- proj_ConstKi @_ @FromFile q
	 , Just HRefl <- proj_ConstKiTy @_ @(Compta src ss) c
	 = case a of
		 -- 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 (Compta src ss)

instance Gram_Term_AtomsFor src (Proxy (Compta src ss) ': ss) g (Compta src ss)
instance
 ( Source src
 , Typeable src
 , Typeable ss
 , Comptable src ss
 , SymInj           (Proxy (Compta src ss) ': ss) (Compta src ss)
 ) => ModuleFor src (Proxy (Compta src ss) ': ss) (Compta src ss) where
	moduleFor = ["Compta"] `moduleWhere`
	 [ "chart"      := teCompta_chart
	 , "readCompta" := teCompta_readCompta
	 ]

tyCompta :: forall src ss vs a.
 Typeable src =>
 Typeable ss =>
 Comptable src ss =>
 Source src => LenInj vs => Type src vs a ->  Type src vs (Compta src ss a)
tyCompta a = tyConstLen @(K (Compta src ss)) @(Compta src ss) (lenVars a) `tyApp` a

teCompta_chart ::
 forall src ss ts a.
 Typeable src =>
 Typeable ss =>
 Comptable src ss =>
 Source src =>
 Term src (Proxy (Compta src ss) ': ss) ts '[Proxy a] (() #> ((Compta src ss) a -> Chart))
teCompta_chart = Term noConstraint (tyCompta @src @ss a0 ~> tyChart) $ teSym @(Compta src ss) $ lam1 compta_chart

teCompta_readCompta ::
 forall src ss ts.
 Typeable src =>
 Typeable ss =>
 Comptable src ss =>
 Source src =>
 Term src (Proxy (Compta src ss) ': ss) ts '[] (() #> (PathFile -> IO (Compta src ss (Map Date [Transaction]))))
teCompta_readCompta = Term noConstraint (tyPathFile ~> tyIO (tyCompta @src @ss (tyMap tyDate (tyList tyTransaction)))) $ teSym @(Compta src ss) $ lam1 fromFile

{-
tyJournal :: Source src => LenInj vs => Type src vs a ->  Type src vs (Journal a)
tyJournal a = tyConstLen @(K Journal) @Journal (lenVars a) `tyApp` a

teJournal :: Source src => SymInj ss Journal => Journal a -> Term src ss ts '[Proxy a] (() #> Journal a)
teJournal j = Term noConstraint (tyJournal a0) $ teSym @Journal $ journal j

teJournal_file :: Source src => SymInj ss Journal => Term src ss ts '[Proxy a] (() #> (Journal a -> PathFile))
teJournal_file = Term noConstraint (tyJournal a0 ~> tyPathFile) $ teSym @Journal $ lam1 journal_file

teJournal_last_read_time :: Source src => SymInj ss Journal => Term src ss ts '[Proxy a] (() #> (Journal a -> Date))
teJournal_last_read_time = Term noConstraint (tyJournal a0 ~> tyDate) $ teSym @Journal $ lam1 journal_last_read_time

teJournal_content :: Source src => SymInj ss Journal => Term src ss ts '[Proxy a] (() #> (Journal a -> a))
teJournal_content = Term noConstraint (tyJournal a0 ~> a0) $ teSym @Journal $ lam1 journal_content
-}