lcc/Hcompta/LCC/Sym/Balance.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Balance'.
   4 module Hcompta.LCC.Sym.Balance where
   5
   6 import Data.Maybe (Maybe(..))
   7 import Text.Show (Show(..))
   8
   9 import Language.Symantic
  10 import Language.Symantic.Lib (a0)
  11
  12 import Hcompta.LCC.Sym.Sumable (tySumable)
  13 import Hcompta.LCC.Balance hiding (balance)
  14 import qualified Hcompta as H ()
  15 import qualified Hcompta.LCC.Balance as LCC
  16
  17 -- * Class 'Sym_Balance'
  18 type instance Sym Balance = Sym_Balance
  19 class Sym_Balance term where
  20         balance :: Balanceable a => term a -> term Balance
  21         default balance :: Sym_Balance (UnT term) => Trans term => Balanceable a => term a -> term Balance
  22         balance = trans1 balance
  23
  24 instance Sym_Balance Eval where
  25         balance = eval1 LCC.balance
  26 instance Sym_Balance View where
  27         balance = view1 "balance"
  28 instance (Sym_Balance r1, Sym_Balance r2) => Sym_Balance (Dup r1 r2) where
  29         balance = dup1 @Sym_Balance balance
  30 instance (Sym_Balance term, Sym_Lambda term) => Sym_Balance (BetaT term)
  31
  32 instance NameTyOf Balance where
  33         nameTyOf _c = ["Balance"] `Mod` "Balance"
  34 -- instance FixityOf Balance
  35 instance ClassInstancesFor Balance where
  36         {-
  37         proveConstraintFor _ (TyConst _ _ c :$ q :@ db :@ b)
  38          | Just HRefl <- proj_ConstKiTy @_ @RunQuery c
  39          , Just HRefl <- proj_ConstKiTy @_ @Query q
  40          , Just HRefl <- proj_ConstKiTy @_ @(LCC.LCC LCC.SourceRead) db
  41          , Just HRefl <- proj_ConstKiTy @_ @Balance b
  42          = Just Dict
  43         -}
  44         proveConstraintFor _ (TyConst _ _ q :$ b)
  45          | Just HRefl <- proj_ConstKiTy @_ @Balance b
  46          = case () of
  47                  _ | Just Refl <- proj_Const @Show q -> Just Dict
  48                  _ -> Nothing
  49         proveConstraintFor _c _q = Nothing
  50 instance TypeInstancesFor Balance
  51 instance Gram_Term_AtomsFor src ss g Balance
  52 instance (Source src, SymInj ss Balance) => ModuleFor src ss Balance where
  53         moduleFor = ["Balance"] `moduleWhere`
  54          [ "balance" := teBalance_balance
  55          ]
  56
  57 tyBalance :: Source src => LenInj vs => Type src vs Balance
  58 tyBalance = tyConst @(K Balance) @Balance
  59
  60 tyBalanceable :: Source src => Type src vs a -> Type src vs (Balanceable a)
  61 tyBalanceable a = tySumable (tyConstLen @(K Balance) @Balance (lenVars a)) a
  62
  63 teBalance_balance :: TermDef Balance '[Proxy a] (Balanceable a #> (a -> Balance))
  64 teBalance_balance = Term (tyBalanceable a0) (a0 ~> tyBalance) (teSym @Balance (lam1 balance))