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 ClassInstancesFor Posting where
  43         proveConstraintFor _ (TyApp _ (TyConst _ _ q) c)
  44          | Just HRefl <- proj_ConstKiTy @(K Posting) @Posting c
  45          = case () of
  46                  _ | Just Refl <- proj_Const @Eq q   -> Just Dict
  47                    | Just Refl <- proj_Const @Show q -> Just Dict
  48                  _ -> Nothing
  49         proveConstraintFor _c _q = Nothing
  50 instance TypeInstancesFor Posting where
  51
  52 instance Gram_Term_AtomsFor src ss g Posting
  53 instance (Source src, SymInj ss Posting) => ModuleFor src ss Posting where
  54         moduleFor = ["Posting"] `moduleWhere`
  55          [ "account" := tePosting_account
  56          , "amounts" := tePosting_amounts
  57          ]
  58
  59 tyPosting :: Source src => LenInj vs => Type src vs Posting
  60 tyPosting = tyConst @(K Posting) @Posting
  61
  62 tePosting_account :: TermDef Posting '[] (() #> (Posting -> Account))
  63 tePosting_account = Term noConstraint (tyPosting ~> tyAccount) $ teSym @Posting $ lam1 posting_account
  64
  65 tePosting_amounts :: TermDef Posting '[] (() #> (Posting -> Amounts))
  66 tePosting_amounts = Term noConstraint (tyPosting ~> tyAmounts) $ teSym @Posting $ lam1 posting_amounts