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
  12 -- * Class 'Sym_Sumable'
  13 type instance Sym Sumable = Sym_Sumable
  14 class Sym_Sumable term where
  15         (+=) :: Sumable s a => term s -> term a -> term s
  16         default (+=) :: Sym_Sumable (UnT term) => Trans term => Sumable s a => term s -> term a -> term s
  17         (+=) = trans2 (+=)
  18
  19 instance Sym_Sumable Eval where
  20         (+=) = eval2 (H.+=)
  21 instance Sym_Sumable View where
  22         (+=) = viewInfix "+=" (infixN 4)
  23 instance (Sym_Sumable r1, Sym_Sumable r2) => Sym_Sumable (Dup r1 r2) where
  24         (+=) = dup2 @Sym_Sumable (+=)
  25 instance (Sym_Sumable term, Sym_Lambda term) => Sym_Sumable (BetaT term)
  26
  27 instance NameTyOf Sumable where
  28         nameTyOf _c = ["LCC"] `Mod` "Sumable"
  29 instance FixityOf Sumable
  30 instance ClassInstancesFor Sumable
  31 instance TypeInstancesFor Sumable
  32 instance Gram_Term_AtomsFor src ss g Sumable
  33 instance (Source src, SymInj ss Sumable) => ModuleFor src ss Sumable where
  34         moduleFor = ["LCC"] `moduleWhere`
  35          [ "+=" `withInfixN` 4 := teSumable_incBy
  36          ]
  37
  38 tySumable :: Source src => Type src vs s -> Type src vs a -> Type src vs (Sumable s a)
  39 tySumable s a = tyConstLen @(K Sumable) @Sumable (lenVars s) `tyApp` s `tyApp` a
  40
  41 teSumable_incBy :: TermDef Sumable '[Proxy s, Proxy a] (Sumable s a #> (s -> a -> s))
  42 teSumable_incBy = Term (tySumable s0 a1) (s0 ~> a1 ~> s0) (teSym @Sumable (lam2 (+=)))
  43
  44 a1 :: Source src => LenInj vs => KindInj (K a) =>
  45       Type src (a0 ': Proxy a ': vs) a
  46 a1 = tyVar "a" (VarS varZ)