]> Git — Sourcephile - comptalang.git/blob - lcc/Hcompta/LCC/Sym/Posting.hs
Add Compta to the symantics.
[comptalang.git] / 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, Inj_Sym 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 => Inj_Len 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