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 -}