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