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