]> Git — Sourcephile - comptalang.git/blob - lcc/Hcompta/LCC/Sym/LCC.hs
Commit old WIP.
[comptalang.git] / lcc / Hcompta / LCC / Sym / LCC.hs
1 {-# LANGUAGE PatternSynonyms #-}
2 {-# LANGUAGE PolyKinds #-}
3 {-# LANGUAGE RankNTypes #-}
4 {-# LANGUAGE UndecidableInstances #-}
5 {-# OPTIONS_GHC -fno-warn-orphans #-}
6 -- | Symantic for 'LCC'.
7 module Hcompta.LCC.Sym.LCC where
8
9 import Data.Eq (Eq)
10 import Data.Function (($), (.))
11 import Data.Maybe (Maybe(..))
12 import Text.Show (Show(..))
13 import qualified Prelude ()
14 import Data.Typeable (Typeable)
15 import System.IO (IO)
16
17 import Hcompta.LCC.IO (FromFile, PathFile(..))
18 import Hcompta.LCC.Compta (LCC)
19 import Hcompta.LCC.Read ()
20 import Hcompta.LCC.Sym.FileSystem (tyPathFile)
21 import Hcompta.LCC.Sym.IO (fromFile, Sym_FromFile)
22 import Hcompta.LCC.Write as Write
23 import Hcompta.LCC.Balance
24 import qualified Hcompta as H
25
26 import Language.Symantic
27 import qualified Language.Symantic.Document.Term as Doc
28 import qualified Language.Symantic.Document.Term.IO as DocIO
29 import Language.Symantic.Lib (tyIO)
30
31 -- * Class 'Sym_LCC'
32 type instance Sym (LCC sou) = Sym_LCC
33 class Sym_FromFile term => Sym_LCC term where
34 lcc :: LCC sou -> term (LCC sou)
35 default lcc :: Sym_LCC (UnT term) => Trans term => LCC sou -> term (LCC sou)
36 lcc = trans . lcc
37
38 instance Sym_LCC Eval where
39 lcc = Eval
40 instance Sym_LCC View where
41 lcc _ = View $ \_v _p -> "LCC.lcc"
42 instance (Sym_LCC r1, Sym_LCC r2) => Sym_LCC (Dup r1 r2) where
43 lcc j = lcc j `Dup` lcc j
44 instance (Sym_LCC term, Sym_Lambda term) => Sym_LCC (BetaT term)
45
46 instance Typeable sou => NameTyOf (LCC sou) where
47 nameTyOf _c = ["LCC"] `Mod` "LCC"
48 instance NameTyOf Write.Reader where
49 nameTyOf _c = ["LCC"] `Mod` "Write.Reader"
50 instance NameTyOf DocIO.TermIO where
51 nameTyOf _c = ["Doc"] `Mod` "TermIO"
52 instance (Typeable sou, Eq sou, Show sou) => ClassInstancesFor (LCC sou) where
53 proveConstraintFor _ (w:@(f:@cw:@d):@a)
54 | Just HRefl <- proj_ConstKiTy @(K (LCC sou)) @(LCC sou) a
55 = case () of
56 _ | Just HRefl <- proj_ConstKiTy @(K Writeable) @Writeable w
57 , Just HRefl <- proj_ConstKiTy @(K (->)) @(->) f
58 , Just HRefl <- proj_ConstKiTy @(K Write.Reader) @Write.Reader cw
59 -> case () of
60 _ | Just HRefl <- proj_ConstKiTy @(K Doc.Term) @Doc.Term d -> Just Dict
61 | Just HRefl <- proj_ConstKiTy @(K DocIO.TermIO) @DocIO.TermIO d -> Just Dict
62 _ -> Nothing
63 _ -> Nothing
64 proveConstraintFor _ (q:@b:@a)
65 | Just HRefl <- proj_ConstKiTy @(K H.Sumable) @H.Sumable q
66 , Just HRefl <- proj_ConstKiTy @(K Balance) @Balance b
67 , Just HRefl <- proj_ConstKiTy @(K (LCC sou)) @(LCC sou) a
68 = Just Dict
69 proveConstraintFor _ (q:@a)
70 | Just HRefl <- proj_ConstKiTy @(K (LCC sou)) @(LCC sou) a
71 = case () of
72 _ | Just Refl <- proj_ConstTy @Eq q -> Just Dict
73 | Just Refl <- proj_ConstTy @Show q -> Just Dict
74 _ -> Nothing
75 proveConstraintFor _c _q = Nothing
76 {-
77 proveConstraintFor _ (TyApp _ (TyApp _ tq@(TyConst _ _ q) b) (TyApp _ c a))
78 -- Sumable Balance (Compta src ss a)
79 | Just HRefl <- proj_ConstKi @_ @H.Sumable q
80 , Just HRefl <- proj_ConstKiTy @_ @Balance b
81 , Just HRefl <- proj_ConstKiTy @_ @LCC c
82 , Just Dict <- proveConstraint (tq `tyApp` b `tyApp` a)
83 = Just Dict
84 proveConstraintFor _ (TyApp _ (TyConst _ _ q) (TyApp _ c a))
85 -- FromFile (Compta src ss a)
86 | Just HRefl <- proj_ConstKi @_ @FromFile q
87 , Just HRefl <- proj_ConstKiTy @_ @LCC c
88 = case a of
89 -- Map Date [Transaction]
90 TyApp _ (TyApp _ m d) (TyApp _ l t)
91 | Just HRefl <- proj_ConstKiTy @_ @Map m
92 , Just HRefl <- proj_ConstKiTy @_ @Date d
93 , Just HRefl <- proj_ConstKiTy @_ @[] l
94 , Just HRefl <- proj_ConstKiTy @_ @Transaction t
95 -> Just Dict
96 _ -> Nothing
97 -}
98 instance TypeInstancesFor (LCC sou)
99
100 instance Gram_Term_AtomsFor src ss g (LCC sou)
101 instance
102 ( Source src
103 , Typeable sou
104 , Eq sou
105 , Show sou
106 , Typeable ss
107 , FromFile (LCC sou)
108 , SymInj ss (LCC sou)
109 ) => ModuleFor src ss (LCC sou) where
110 moduleFor = ["LCC"] `moduleWhere`
111 [ "readLCC" := teLCC_readLCC @sou
112 ]
113
114 tyLCC :: forall sou src vs. Eq sou => Show sou => Typeable sou => Source src => LenInj vs => Type src vs (LCC sou)
115 tyLCC = tyConst @(K (LCC sou)) @(LCC sou)
116
117 teLCC_readLCC ::
118 forall sou src ss ts.
119 Eq sou =>
120 Show sou =>
121 Typeable sou =>
122 Typeable ss =>
123 FromFile (LCC sou) =>
124 SymInj ss (LCC sou) =>
125 Source src =>
126 Term src ss ts '[] (() #> (PathFile -> IO (LCC sou)))
127 teLCC_readLCC = Term noConstraint
128 (tyPathFile ~> tyIO tyLCC) $
129 teSym @(LCC sou) $ lam1 fromFile
130
131 {-
132 teLCC_readLCC ::
133 forall src ss ts.
134 Typeable src =>
135 Typeable ss =>
136 Comptable src ss =>
137 Source src =>
138 Term src ss ts '[] (() #> (PathFile -> IO LCC))
139 teLCC_readLCC = Term noConstraint (tyPathFile ~> tyIO tyLCC) $ teSym @LCC $ lam1 fromFile
140 -}
141 {-
142 tyJournal :: Source src => LenInj vs => Type src vs a -> Type src vs (Journal a)
143 tyJournal a = tyConstLen @(K Journal) @Journal (lenVars a) `tyApp` a
144
145 teJournal :: Source src => SymInj ss Journal => Journal a -> Term src ss ts '[Proxy a] (() #> Journal a)
146 teJournal j = Term noConstraint (tyJournal a0) $ teSym @Journal $ journal j
147
148 teJournal_file :: Source src => SymInj ss Journal => Term src ss ts '[Proxy a] (() #> (Journal a -> PathFile))
149 teJournal_file = Term noConstraint (tyJournal a0 ~> tyPathFile) $ teSym @Journal $ lam1 journal_file
150
151 teJournal_last_read_time :: Source src => SymInj ss Journal => Term src ss ts '[Proxy a] (() #> (Journal a -> Date))
152 teJournal_last_read_time = Term noConstraint (tyJournal a0 ~> tyDate) $ teSym @Journal $ lam1 journal_last_read_time
153
154 teJournal_content :: Source src => SymInj ss Journal => Term src ss ts '[Proxy a] (() #> (Journal a -> a))
155 teJournal_content = Term noConstraint (tyJournal a0 ~> a0) $ teSym @Journal $ lam1 journal_content
156 -}