lcc/Hcompta/LCC/Sym/Compta.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Compta'.
   4 module Hcompta.LCC.Sym.Compta where
   5
   6 import Data.Eq (Eq)
   7 import Data.Function (($), (.))
   8 import Data.Maybe (Maybe(..))
   9 import Text.Show (Show(..))
  10 import qualified Prelude ()
  11 import Data.Typeable (Typeable)
  12
  13 import Hcompta.LCC.Compta (Compta(..))
  14 import Hcompta.LCC.Journal (Journal, PathFile(..))
  15 import Hcompta.LCC.Sym.Date (tyDate)
  16 import Hcompta.LCC.Sym.FileSystem (tyPathFile)
  17 import qualified Hcompta.LCC.Journal as LCC
  18
  19 import Language.Symantic
  20 import Language.Symantic.Lib (a0)
  21
  22 -- * Class 'Sym_Compta'
  23 class Sym_Compta term where
  24         compta :: Compta src ss j -> term (Compta src ss j)
  25         default compta :: Sym_Compta (UnT term) => Trans term => Compta src ss j -> term (Compta src ss j)
  26         compta = trans . compta
  27
  28 instance Sym_Compta Eval where
  29         compta = Eval
  30 instance Sym_Compta View where
  31         compta _ = View $ \_v _p -> "Compta.compta"
  32 instance (Sym_Compta r1, Sym_Compta r2) => Sym_Compta (Dup r1 r2) where
  33         compta j = compta j `Dup` compta j
  34 instance (Sym_Compta term, Sym_Lambda term) => Sym_Compta (BetaT term)
  35
  36 instance FixityOf (Compta src ss)
  37 instance (Typeable src, Typeable ss, Source src) => ClassInstancesFor (Compta src ss) where
  38         proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ c j))
  39          | Just HRefl <- proj_ConstKiTy @(K (Compta src ss)) @(Compta src ss) c
  40          = case () of
  41                  _ | Just Refl <- proj_Const @Eq q
  42                    , Just Dict <- proveConstraint (tq `tyApp` j) -> Just Dict
  43                    | Just Refl <- proj_Const @Show q
  44                    , Just Dict <- proveConstraint (tq `tyApp` j) -> Just Dict
  45                  _ -> Nothing
  46         proveConstraintFor _c _q = Nothing
  47 instance TypeInstancesFor (Compta src ss)
  48
  49 instance Gram_Term_AtomsFor src (Proxy (Compta src ss) ': ss) g (Compta src ss)
  50 instance
  51  ( Source src
  52  , Inj_Sym          (Proxy (Compta src ss) ': ss) (Compta src ss)
  53  ) => ModuleFor src (Proxy (Compta src ss) ': ss) (Compta src ss) where
  54         moduleFor = ["Compta"] `moduleWhere`
  55          [
  56          ]
  57
  58 {-
  59 tyJournal :: Source src => Inj_Len vs => Type src vs a ->  Type src vs (Journal a)
  60 tyJournal a = tyConstLen @(K Journal) @Journal (lenVars a) `tyApp` a
  61
  62 teJournal :: Source src => Inj_Sym ss Journal => Journal a -> Term src ss ts '[Proxy a] (() #> Journal a)
  63 teJournal j = Term noConstraint (tyJournal a0) $ teSym @Journal $ journal j
  64
  65 teJournal_file :: Source src => Inj_Sym ss Journal => Term src ss ts '[Proxy a] (() #> (Journal a -> PathFile))
  66 teJournal_file = Term noConstraint (tyJournal a0 ~> tyPathFile) $ teSym @Journal $ lam1 journal_file
  67
  68 teJournal_last_read_time :: Source src => Inj_Sym ss Journal => Term src ss ts '[Proxy a] (() #> (Journal a -> Date))
  69 teJournal_last_read_time = Term noConstraint (tyJournal a0 ~> tyDate) $ teSym @Journal $ lam1 journal_last_read_time
  70
  71 teJournal_content :: Source src => Inj_Sym ss Journal => Term src ss ts '[Proxy a] (() #> (Journal a -> a))
  72 teJournal_content = Term noConstraint (tyJournal a0 ~> a0) $ teSym @Journal $ lam1 journal_content
  73 -}