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.Chart (Chart(..))
  14 import Hcompta.LCC.Compta (Compta)
  15 import Hcompta.LCC.Journal (Journal, PathFile(..))
  16 import Hcompta.LCC.Sym.Date (tyDate)
  17 import Hcompta.LCC.Sym.FileSystem (tyPathFile)
  18 import Hcompta.LCC.Sym.Chart (tyChart)
  19 import qualified Hcompta.LCC.Journal as LCC
  20 import qualified Hcompta.LCC.Compta  as LCC
  21
  22 import Language.Symantic
  23 import Language.Symantic.Lib (a0)
  24
  25 -- * Class 'Sym_Compta'
  26 type instance Sym (Compta src ss) = Sym_Compta
  27 class Sym_Compta term where
  28         compta       :: Compta src ss j -> term (Compta src ss j)
  29         compta_chart :: term (Compta src ss j) -> term Chart
  30         default compta       :: Sym_Compta (UnT term) => Trans term => Compta src ss j -> term (Compta src ss j)
  31         default compta_chart :: Sym_Compta (UnT term) => Trans term => term (Compta src ss j) -> term Chart
  32         compta       = trans . compta
  33         compta_chart = trans1 compta_chart
  34
  35 instance Sym_Compta Eval where
  36         compta       = Eval
  37         compta_chart = eval1 LCC.compta_chart
  38 instance Sym_Compta View where
  39         compta _     = View $ \_v _p -> "Compta.compta"
  40         compta_chart = view1 "Chart.compta_chart"
  41 instance (Sym_Compta r1, Sym_Compta r2) => Sym_Compta (Dup r1 r2) where
  42         compta j     = compta j `Dup` compta j
  43         compta_chart = dup1 @Sym_Compta compta_chart
  44 instance (Sym_Compta term, Sym_Lambda term) => Sym_Compta (BetaT term)
  45
  46 instance FixityOf (Compta src ss)
  47 instance (Typeable src, Typeable ss, Source src) => ClassInstancesFor (Compta src ss) where
  48         proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ c j))
  49          | Just HRefl <- proj_ConstKiTy @(K (Compta src ss)) @(Compta src ss) c
  50          = case () of
  51                  _ | Just Refl <- proj_Const @Eq q
  52                    , Just Dict <- proveConstraint (tq `tyApp` j) -> Just Dict
  53                    | Just Refl <- proj_Const @Show q
  54                    , Just Dict <- proveConstraint (tq `tyApp` j) -> Just Dict
  55                  _ -> Nothing
  56         proveConstraintFor _c _q = Nothing
  57 instance TypeInstancesFor (Compta src ss)
  58
  59 instance Gram_Term_AtomsFor src (Proxy (Compta src ss) ': ss) g (Compta src ss)
  60 instance
  61  ( Source src
  62  , Typeable src
  63  , Typeable ss
  64  , SymInj           (Proxy (Compta src ss) ': ss) (Compta src ss)
  65  ) => ModuleFor src (Proxy (Compta src ss) ': ss) (Compta src ss) where
  66         moduleFor = ["Compta"] `moduleWhere`
  67          [ "chart" := teCompta_chart
  68          ]
  69
  70 tyCompta :: forall src ss vs a.
  71  Typeable src =>
  72  Typeable ss =>
  73  Source src => LenInj vs => Type src vs a ->  Type src vs (Compta src ss a)
  74 tyCompta a = tyConstLen @(K (Compta src ss)) @(Compta src ss) (lenVars a) `tyApp` a
  75
  76 teCompta_chart ::
  77  forall src ss ts a.
  78  Typeable src =>
  79  Typeable ss =>
  80  Source src =>
  81  Term src (Proxy (Compta src ss) ': ss) ts '[Proxy a] (() #> ((Compta src ss) a -> Chart))
  82 teCompta_chart = Term noConstraint (tyCompta @src @ss a0 ~> tyChart) $ teSym @(Compta src ss) $ lam1 compta_chart
  83
  84 {-
  85 tyJournal :: Source src => LenInj vs => Type src vs a ->  Type src vs (Journal a)
  86 tyJournal a = tyConstLen @(K Journal) @Journal (lenVars a) `tyApp` a
  87
  88 teJournal :: Source src => SymInj ss Journal => Journal a -> Term src ss ts '[Proxy a] (() #> Journal a)
  89 teJournal j = Term noConstraint (tyJournal a0) $ teSym @Journal $ journal j
  90
  91 teJournal_file :: Source src => SymInj ss Journal => Term src ss ts '[Proxy a] (() #> (Journal a -> PathFile))
  92 teJournal_file = Term noConstraint (tyJournal a0 ~> tyPathFile) $ teSym @Journal $ lam1 journal_file
  93
  94 teJournal_last_read_time :: Source src => SymInj ss Journal => Term src ss ts '[Proxy a] (() #> (Journal a -> Date))
  95 teJournal_last_read_time = Term noConstraint (tyJournal a0 ~> tyDate) $ teSym @Journal $ lam1 journal_last_read_time
  96
  97 teJournal_content :: Source src => SymInj ss Journal => Term src ss ts '[Proxy a] (() #> (Journal a -> a))
  98 teJournal_content = Term noConstraint (tyJournal a0 ~> a0) $ teSym @Journal $ lam1 journal_content
  99 -}