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