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 (Typeable src, Typeable ss) => NameTyOf (Compta src ss) where
  47         nameTyOf _c = ["LCC"] `Mod` "Compta"
  48 instance FixityOf (Compta src ss)
  49 instance (Typeable src, Typeable ss, Source src) => ClassInstancesFor (Compta src ss) where
  50         proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ c j))
  51          | Just HRefl <- proj_ConstKiTy @(K (Compta src ss)) @(Compta src ss) c
  52          = case () of
  53                  _ | Just Refl <- proj_Const @Eq q
  54                    , Just Dict <- proveConstraint (tq `tyApp` j) -> Just Dict
  55                    | Just Refl <- proj_Const @Show q
  56                    , Just Dict <- proveConstraint (tq `tyApp` j) -> Just Dict
  57                  _ -> Nothing
  58         proveConstraintFor _c _q = Nothing
  59 instance TypeInstancesFor (Compta src ss)
  60
  61 instance Gram_Term_AtomsFor src (Proxy (Compta src ss) ': ss) g (Compta src ss)
  62 instance
  63  ( Source src
  64  , Typeable src
  65  , Typeable ss
  66  , SymInj           (Proxy (Compta src ss) ': ss) (Compta src ss)
  67  ) => ModuleFor src (Proxy (Compta src ss) ': ss) (Compta src ss) where
  68         moduleFor = ["LCC"] `moduleWhere`
  69          [ "chart" := teCompta_chart
  70          ]
  71
  72 tyCompta :: forall src ss vs a.
  73  Typeable src =>
  74  Typeable ss =>
  75  Source src => LenInj vs => Type src vs a ->  Type src vs (Compta src ss a)
  76 tyCompta a = tyConstLen @(K (Compta src ss)) @(Compta src ss) (lenVars a) `tyApp` a
  77
  78 teCompta_chart ::
  79  forall src ss ts a.
  80  Typeable src =>
  81  Typeable ss =>
  82  Source src =>
  83  Term src (Proxy (Compta src ss) ': ss) ts '[Proxy a] (() #> ((Compta src ss) a -> Chart))
  84 teCompta_chart = Term noConstraint (tyCompta @src @ss a0 ~> tyChart) $ teSym @(Compta src ss) $ lam1 compta_chart
  85
  86 {-
  87 tyJournal :: Source src => LenInj vs => Type src vs a ->  Type src vs (Journal a)
  88 tyJournal a = tyConstLen @(K Journal) @Journal (lenVars a) `tyApp` a
  89
  90 teJournal :: Source src => SymInj ss Journal => Journal a -> Term src ss ts '[Proxy a] (() #> Journal a)
  91 teJournal j = Term noConstraint (tyJournal a0) $ teSym @Journal $ journal j
  92
  93 teJournal_file :: Source src => SymInj ss Journal => Term src ss ts '[Proxy a] (() #> (Journal a -> PathFile))
  94 teJournal_file = Term noConstraint (tyJournal a0 ~> tyPathFile) $ teSym @Journal $ lam1 journal_file
  95
  96 teJournal_last_read_time :: Source src => SymInj ss Journal => Term src ss ts '[Proxy a] (() #> (Journal a -> Date))
  97 teJournal_last_read_time = Term noConstraint (tyJournal a0 ~> tyDate) $ teSym @Journal $ lam1 journal_last_read_time
  98
  99 teJournal_content :: Source src => SymInj ss Journal => Term src ss ts '[Proxy a] (() #> (Journal a -> a))
 100 teJournal_content = Term noConstraint (tyJournal a0 ~> a0) $ teSym @Journal $ lam1 journal_content
 101 -}