{-# 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 Hcompta.LCC.Compta (Compta(..))
import Hcompta.LCC.Journal (Journal, PathFile(..))
import Hcompta.LCC.Sym.Date (tyDate)
import Hcompta.LCC.Sym.FileSystem (tyPathFile)
import qualified Hcompta.LCC.Journal as LCC

import Language.Symantic
import Language.Symantic.Lib (a0)

-- * Class 'Sym_Compta'
class Sym_Compta term where
	compta :: Compta src ss j -> term (Compta src ss j)
	default compta :: Sym_Compta (UnT term) => Trans term => Compta src ss j -> term (Compta src ss j)
	compta = trans . compta

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

instance FixityOf (Compta src ss)
instance (Typeable src, Typeable ss, Source src) => 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 _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
 , Inj_Sym          (Proxy (Compta src ss) ': ss) (Compta src ss)
 ) => ModuleFor src (Proxy (Compta src ss) ': ss) (Compta src ss) where
	moduleFor = ["Compta"] `moduleWhere`
	 [
	 ]

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

teJournal :: Source src => Inj_Sym 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 => Inj_Sym 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 => Inj_Sym 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 => Inj_Sym ss Journal => Term src ss ts '[Proxy a] (() #> (Journal a -> a))
teJournal_content = Term noConstraint (tyJournal a0 ~> a0) $ teSym @Journal $ lam1 journal_content
-}