lcc/Hcompta/LCC/Sym/Posting.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Posting'.
   4 module Hcompta.LCC.Sym.Posting where
   5
   6 import Data.Eq (Eq)
   7 import Data.Function (($))
   8 import Data.Maybe (Maybe(..))
   9 import Text.Show (Show(..))
  10
  11 import Hcompta.LCC.Account
  12 import Hcompta.LCC.Amount
  13 import Hcompta.LCC.Posting (Posting)
  14 import qualified Hcompta.LCC.Posting as LCC
  15
  16 import Hcompta.LCC.Sym.Account (tyAccount)
  17 import Hcompta.LCC.Sym.Amount (tyAmounts)
  18
  19 import Language.Symantic
  20
  21 -- * Class 'Sym_Posting'
  22 type instance Sym Posting = Sym_Posting
  23 class Sym_Posting term where
  24         posting_account :: term Posting -> term Account
  25         posting_amounts :: term Posting -> term Amounts
  26         default posting_account :: Sym_Posting (UnT term) => Trans term => term Posting -> term Account
  27         default posting_amounts :: Sym_Posting (UnT term) => Trans term => term Posting -> term Amounts
  28         posting_account = trans1 posting_account
  29         posting_amounts = trans1 posting_amounts
  30
  31 instance Sym_Posting Eval where
  32         posting_account = eval1 LCC.posting_account
  33         posting_amounts = eval1 LCC.posting_amounts
  34 instance Sym_Posting View where
  35         posting_account = view1 "Posting.account"
  36         posting_amounts = view1 "Posting.amounts"
  37 instance (Sym_Posting r1, Sym_Posting r2) => Sym_Posting (Dup r1 r2) where
  38         posting_account = dup1 @Sym_Posting posting_account
  39         posting_amounts = dup1 @Sym_Posting posting_amounts
  40 instance (Sym_Posting term, Sym_Lambda term) => Sym_Posting (BetaT term)
  41
  42 instance NameTyOf Posting where
  43         nameTyOf _c = ["LCC"] `Mod` "Posting"
  44 instance ClassInstancesFor Posting where
  45         proveConstraintFor _ (TyApp _ (TyConst _ _ q) c)
  46          | Just HRefl <- proj_ConstKiTy @(K Posting) @Posting c
  47          = case () of
  48                  _ | Just Refl <- proj_Const @Eq q   -> Just Dict
  49                    | Just Refl <- proj_Const @Show q -> Just Dict
  50                  _ -> Nothing
  51         proveConstraintFor _c _q = Nothing
  52 instance TypeInstancesFor Posting where
  53
  54 instance Gram_Term_AtomsFor src ss g Posting
  55 instance (Source src, SymInj ss Posting) => ModuleFor src ss Posting where
  56         moduleFor = ["LCC", "Posting"] `moduleWhere`
  57          [ "account" := tePosting_account
  58          , "amounts" := tePosting_amounts
  59          ]
  60
  61 tyPosting :: Source src => LenInj vs => Type src vs Posting
  62 tyPosting = tyConst @(K Posting) @Posting
  63
  64 tePosting_account :: TermDef Posting '[] (() #> (Posting -> Account))
  65 tePosting_account = Term noConstraint (tyPosting ~> tyAccount) $ teSym @Posting $ lam1 posting_account
  66
  67 tePosting_amounts :: TermDef Posting '[] (() #> (Posting -> Amounts))
  68 tePosting_amounts = Term noConstraint (tyPosting ~> tyAmounts) $ teSym @Posting $ lam1 posting_amounts