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 as H hiding (neg)
  10 import qualified Hcompta.Quantity as H
  11
  12 -- * Class 'Sym_Negable'
  13 type instance Sym Negable = Sym_Negable
  14 class Sym_Negable term where
  15         neg :: Negable a => term a -> term a
  16         default neg :: Sym_Negable (UnT term) => Trans term => Negable a => term a -> term a
  17         neg = trans1 neg
  18
  19 instance Sym_Negable Eval where
  20         neg = eval1 H.neg
  21 instance Sym_Negable View where
  22         neg = view1 "neg"
  23 instance (Sym_Negable r1, Sym_Negable r2) => Sym_Negable (Dup r1 r2) where
  24         neg = dup1 @Sym_Negable neg
  25 instance (Sym_Negable term, Sym_Lambda term) => Sym_Negable (BetaT term)
  26
  27 instance NameTyOf Negable where
  28         nameTyOf _c = ["LCC"] `Mod` "Negable"
  29 instance FixityOf Negable
  30 instance ClassInstancesFor Negable
  31 instance TypeInstancesFor Negable
  32 instance Gram_Term_AtomsFor src ss g Negable
  33 instance (Source src, SymInj ss Negable) => ModuleFor src ss Negable where
  34         moduleFor = ["LCC"] `moduleWhere`
  35          [ "-" `withPrefix` 10 := teNegable_neg
  36          ]
  37
  38 tyNegable :: Source src => Type src vs a -> Type src vs (Negable a)
  39 tyNegable a = tyConstLen @(K Negable) @Negable (lenVars a) `tyApp` a
  40
  41 teNegable_neg :: TermDef Negable '[Proxy a] (Negable a #> (a -> a))
  42 teNegable_neg = Term (tyNegable a0) (a0 ~> a0) (teSym @Negable (lam1 neg))