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 = ["LCC"] `Mod` "Balance"
  34 -- instance FixityOf Balance
  35 instance ClassInstancesFor Balance where
  36         proveConstraintFor _ (TyApp _ (TyConst _ _ q) b)
  37          | Just HRefl <- proj_ConstKiTy @_ @Balance b
  38          = case () of
  39                  _ | Just Refl <- proj_Const @Show q -> Just Dict
  40                  _ -> Nothing
  41         proveConstraintFor _c _q = Nothing
  42 instance TypeInstancesFor Balance
  43 instance Gram_Term_AtomsFor src ss g Balance
  44 instance (Source src, SymInj ss Balance) => ModuleFor src ss Balance where
  45         moduleFor = ["LCC"] `moduleWhere`
  46          [ "balance" := teBalance_balance
  47          ]
  48
  49 tyBalance :: Source src => LenInj vs => Type src vs Balance
  50 tyBalance = tyConst @(K Balance) @Balance
  51
  52 tyBalanceable :: Source src => Type src vs a -> Type src vs (Balanceable a)
  53 tyBalanceable a = tySumable (tyConstLen @(K Balance) @Balance (lenVars a)) a
  54
  55 teBalance_balance :: TermDef Balance '[Proxy a] (Balanceable a #> (a -> Balance))
  56 teBalance_balance = Term (tyBalanceable a0) (a0 ~> tyBalance) (teSym @Balance (lam1 balance))