lcc/Hcompta/LCC/Sym/Negable.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Negable'.
   4 module Hcompta.LCC.Sym.Negable where
   5
   6 import Language.Symantic
   7 import Language.Symantic.Lib (a0)
   8
   9 import Hcompta.Quantity
  10
  11 -- * Class 'Sym_Negable'
  12 type instance Sym Negable = Sym_Negable
  13 class Sym_Negable term where
  14         neg :: Negable a => term a -> term a
  15         default neg :: Sym_Negable (UnT term) => Trans term => Negable a => term a -> term a
  16         neg = trans1 neg
  17
  18 instance Sym_Negable Eval where
  19         neg = eval1 quantity_neg
  20 instance Sym_Negable View where
  21         neg = view1 "neg"
  22 instance (Sym_Negable r1, Sym_Negable r2) => Sym_Negable (Dup r1 r2) where
  23         neg = dup1 @Sym_Negable neg
  24 instance (Sym_Negable term, Sym_Lambda term) => Sym_Negable (BetaT term)
  25
  26 instance FixityOf Negable
  27 instance ClassInstancesFor Negable
  28 instance TypeInstancesFor Negable
  29 instance Gram_Term_AtomsFor src ss g Negable
  30 instance (Source src, SymInj ss Negable) => ModuleFor src ss Negable where
  31         moduleFor = ["Negable"] `moduleWhere`
  32          [ "-" `withPrefix` 10 := teNegable_neg
  33          ]
  34
  35 tyNegable :: Source src => Type src vs a -> Type src vs (Negable a)
  36 tyNegable a = tyConstLen @(K Negable) @Negable (lenVars a) `tyApp` a
  37
  38 teNegable_neg :: TermDef Negable '[Proxy a] (Negable a #> (a -> a))
  39 teNegable_neg = Term (tyNegable a0) (a0 ~> a0) (teSym @Negable (lam1 neg))