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

import Data.Eq (Eq)
import Data.Maybe (Maybe(..))
import Text.Show (Show)
import qualified Prelude ()

import Hcompta.LCC.Posting (Date)
import Language.Symantic

-- * Class 'Sym_Date'
type instance Sym Date = Sym_Date
class Sym_Date (term:: * -> *) where

instance Sym_Date Eval where
instance Sym_Date View where
instance (Sym_Date r1, Sym_Date r2) => Sym_Date (Dup r1 r2) where
instance (Sym_Date term, Sym_Lambda term) => Sym_Date (BetaT term)

instance NameTyOf Date where
	nameTyOf _c = ["Date"] `Mod` "Date"
instance ClassInstancesFor Date where
	proveConstraintFor _ (TyConst _ _ q :$ a)
	 | Just HRefl <- proj_ConstKiTy @(K Date) @Date a
	 = case () of
		 _ | Just Refl <- proj_Const @Eq   q -> Just Dict
		   | Just Refl <- proj_Const @Show q -> Just Dict
		 _ -> Nothing
	proveConstraintFor _c _q = Nothing
instance TypeInstancesFor Date
instance (Source src, SymInj ss Date) => ModuleFor src ss Date
instance Gram_Term_AtomsFor src ss g Date

tyDate :: Source src => LenInj vs => Type src vs Date
tyDate = tyConst @(K Date) @Date