]> Git — Sourcephile - comptalang.git/blob - lcc/Hcompta/LCC/Sym/Negable.hs
Remove old Yesod scaffolding.
[comptalang.git] / 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 (Proxy 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, Inj_Sym 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))