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

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

import Hcompta.LCC.IO (FromFile, PathFile(..))
import Hcompta.LCC.Compta (LCC)
import Hcompta.LCC.Read ()
import Hcompta.LCC.Sym.FileSystem (tyPathFile)
import Hcompta.LCC.Sym.IO (fromFile, Sym_FromFile)
import Hcompta.LCC.Write
import Hcompta.LCC.Balance
import qualified Hcompta as H

import Language.Symantic
import qualified Language.Symantic.Document as Doc
import Language.Symantic.Lib (tyIO)

-- * Class 'Sym_LCC'
type instance Sym (LCC sou) = Sym_LCC
class Sym_FromFile term => Sym_LCC term where
	lcc :: LCC sou -> term (LCC sou)
	default lcc :: Sym_LCC (UnT term) => Trans term => LCC sou -> term (LCC sou)
	lcc = trans . lcc

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

instance Typeable sou => NameTyOf (LCC sou) where
	nameTyOf _c = ["LCC"] `Mod` "LCC"
instance NameTyOf Context_Write where
	nameTyOf _c = ["LCC"] `Mod` "Context_Write"
instance NameTyOf Doc.ANSI_IO where
	nameTyOf _c = ["Doc"] `Mod` "ANSIO_IO"
instance (Typeable sou, Eq sou, Show sou) => ClassInstancesFor (LCC sou) where
	proveConstraintFor _ (w:@(f:@cw:@d):@a)
	 | Just HRefl <- proj_ConstKiTy @(K (LCC sou)) @(LCC sou) a
	 = case () of
		 _ | Just HRefl <- proj_ConstKiTy @(K Writeable) @Writeable w
		   , Just HRefl <- proj_ConstKiTy @(K (->)) @(->) f
		   , Just HRefl <- proj_ConstKiTy @(K Context_Write) @Context_Write cw
		   -> case () of
			 _ | Just HRefl <- proj_ConstKiTy @(K Doc.ANSI_IO) @Doc.ANSI_IO d -> Just Dict
			   | Just HRefl <- proj_ConstKiTy @(K Doc.ANSI)    @Doc.ANSI    d -> Just Dict
			   | Just HRefl <- proj_ConstKiTy @(K Doc.Plain)   @Doc.Plain   d -> Just Dict
			   | Just HRefl <- proj_ConstKiTy @(K Doc.PlainIO) @Doc.PlainIO d -> Just Dict
			 _ -> Nothing
		 _ -> Nothing
	proveConstraintFor _ (q:@b:@a)
	 | Just HRefl <- proj_ConstKiTy @(K H.Sumable) @H.Sumable q
	 , Just HRefl <- proj_ConstKiTy @(K Balance) @Balance b
	 , Just HRefl <- proj_ConstKiTy @(K (LCC sou)) @(LCC sou) a
	 = Just Dict
	proveConstraintFor _ (q:@a)
	 | Just HRefl <- proj_ConstKiTy @(K (LCC sou)) @(LCC sou) a
	 = case () of
		 _ | Just Refl <- proj_ConstTy @Eq   q -> Just Dict
		   | Just Refl <- proj_ConstTy @Show q -> Just Dict
		 _ -> Nothing
	proveConstraintFor _c _q = 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 @_ @LCC 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 @_ @LCC 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
	-}
instance TypeInstancesFor (LCC sou)

instance Gram_Term_AtomsFor src ss g (LCC sou)
instance
 ( Source src
 , Typeable sou
 , Eq sou
 , Show sou
 , Typeable ss
 , FromFile (LCC sou)
 , SymInj           ss (LCC sou)
 ) => ModuleFor src ss (LCC sou) where
	moduleFor = ["LCC"] `moduleWhere`
	 [ "readLCC" := teLCC_readLCC @sou
	 ]

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

teLCC_readLCC ::
 forall sou src ss ts.
 Eq sou =>
 Show sou =>
 Typeable sou =>
 Typeable ss =>
 FromFile (LCC sou) =>
 SymInj ss (LCC sou) =>
 Source src =>
 Term src ss ts '[] (() #> (PathFile -> IO (LCC sou)))
teLCC_readLCC = Term noConstraint
                     (tyPathFile ~> tyIO tyLCC) $
                     teSym @(LCC sou) $ lam1 fromFile

{-
teLCC_readLCC ::
 forall src ss ts.
 Typeable src =>
 Typeable ss =>
 Comptable src ss =>
 Source src =>
 Term src ss ts '[] (() #> (PathFile -> IO LCC))
teLCC_readLCC = Term noConstraint (tyPathFile ~> tyIO tyLCC) $ teSym @LCC $ 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
-}