lcc/Hcompta/LCC/Sym/Date.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Date'.
   4 module Hcompta.LCC.Sym.Date where
   5
   6 import Data.Eq (Eq)
   7 import Data.Maybe (Maybe(..))
   8 import Text.Show (Show)
   9 import qualified Prelude ()
  10
  11 import Hcompta.LCC.Posting (Date)
  12 import Language.Symantic
  13
  14 -- * Class 'Sym_Date'
  15 type instance Sym Date = Sym_Date
  16 class Sym_Date (term:: * -> *) where
  17
  18 instance Sym_Date Eval where
  19 instance Sym_Date View where
  20 instance (Sym_Date r1, Sym_Date r2) => Sym_Date (Dup r1 r2) where
  21 instance (Sym_Date term, Sym_Lambda term) => Sym_Date (BetaT term)
  22
  23 instance NameTyOf Date where
  24         nameTyOf _c = ["LCC"] `Mod` "Date"
  25 instance ClassInstancesFor Date where
  26         proveConstraintFor _ (TyApp _ (TyConst _ _ q) a)
  27          | Just HRefl <- proj_ConstKiTy @(K Date) @Date a
  28          = case () of
  29                  _ | Just Refl <- proj_Const @Eq   q -> Just Dict
  30                    | Just Refl <- proj_Const @Show q -> Just Dict
  31                  _ -> Nothing
  32         proveConstraintFor _c _q = Nothing
  33 instance TypeInstancesFor Date
  34 instance (Source src, SymInj ss Date) => ModuleFor src ss Date
  35 instance Gram_Term_AtomsFor src ss g Date
  36
  37 tyDate :: Source src => LenInj vs => Type src vs Date
  38 tyDate = tyConst @(K Date) @Date