lcc/Hcompta/LCC/Sym/Sumable.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Sumable'.
   4 module Hcompta.LCC.Sym.Sumable where
   5
   6 import Language.Symantic
   7 import Language.Symantic.Lib (s0)
   8
   9 import Hcompta.Quantity as H hiding ((+=))
  10 import qualified Hcompta.Quantity as H
  11 import Hcompta.LCC.Sym.Writeable (a1)
  12
  13 -- * Class 'Sym_Sumable'
  14 type instance Sym Sumable = Sym_Sumable
  15 class Sym_Sumable term where
  16         (+=) :: Sumable s a => term s -> term a -> term s
  17         default (+=) :: Sym_Sumable (UnT term) => Trans term => Sumable s a => term s -> term a -> term s
  18         (+=) = trans2 (+=)
  19
  20 instance Sym_Sumable Eval where
  21         (+=) = eval2 (H.+=)
  22 instance Sym_Sumable View where
  23         (+=) = viewInfix "+=" (infixN 4)
  24 instance (Sym_Sumable r1, Sym_Sumable r2) => Sym_Sumable (Dup r1 r2) where
  25         (+=) = dup2 @Sym_Sumable (+=)
  26 instance (Sym_Sumable term, Sym_Lambda term) => Sym_Sumable (BetaT term)
  27
  28 instance NameTyOf Sumable where
  29         nameTyOf _c = ["Sumable"] `Mod` "Sumable"
  30 instance FixityOf Sumable
  31 instance ClassInstancesFor Sumable
  32 instance TypeInstancesFor Sumable
  33 instance Gram_Term_AtomsFor src ss g Sumable
  34 instance (Source src, SymInj ss Sumable) => ModuleFor src ss Sumable where
  35         moduleFor = ["Sumable"] `moduleWhere`
  36          [ "+=" `withInfixN` 4 := teSumable_incBy
  37          ]
  38
  39 tySumable :: Source src => Type src vs s -> Type src vs a -> Type src vs (Sumable s a)
  40 tySumable s a = tyConstLen @(K Sumable) @Sumable (lenVars s) `tyApp` s `tyApp` a
  41
  42 teSumable_incBy :: TermDef Sumable '[Proxy s, Proxy a] (Sumable s a #> (s -> a -> s))
  43 teSumable_incBy = Term (tySumable s0 a1) (s0 ~> a1 ~> s0) (teSym @Sumable (lam2 (+=)))