]> Git — Sourcephile - comptalang.git/blob - lcc/Hcompta/LCC/Sym/Zeroable.hs
Commit old WIP.
[comptalang.git] / lcc / Hcompta / LCC / Sym / Zeroable.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 -- | Symantic for 'Zeroable'.
4 module Hcompta.LCC.Sym.Zeroable where
5
6 import Language.Symantic
7 import Language.Symantic.Lib (a0)
8
9 import Hcompta.Quantity as H hiding (zero)
10 import qualified Hcompta.Quantity as H
11
12 -- * Class 'Sym_Zeroable'
13 type instance Sym Zeroable = Sym_Zeroable
14 class Sym_Zeroable term where
15 zero :: Zeroable a => term a
16 default zero :: Sym_Zeroable (UnT term) => Trans term => Zeroable a => term a
17 zero = trans zero
18
19 instance Sym_Zeroable Eval where
20 zero = Eval H.zero
21 instance Sym_Zeroable View where
22 zero = view0 "zero"
23 instance (Sym_Zeroable r1, Sym_Zeroable r2) => Sym_Zeroable (Dup r1 r2) where
24 zero = dup0 @Sym_Zeroable zero
25 instance (Sym_Zeroable term, Sym_Lambda term) => Sym_Zeroable (BetaT term)
26
27 instance NameTyOf Zeroable where
28 nameTyOf _c = ["Zeroable"] `Mod` "Zeroable"
29 instance FixityOf Zeroable
30 instance ClassInstancesFor Zeroable
31 instance TypeInstancesFor Zeroable
32 instance Gram_Term_AtomsFor src ss g Zeroable
33 instance (Source src, SymInj ss Zeroable) => ModuleFor src ss Zeroable where
34 moduleFor = ["Zeroable"] `moduleWhere`
35 [ "zero" := teZeroable_zero
36 ]
37
38 tyZeroable :: Source src => Type src vs a -> Type src vs (Zeroable a)
39 tyZeroable a = tyConstLen @(K Zeroable) @Zeroable (lenVars a) `tyApp` a
40
41 teZeroable_zero :: TermDef Zeroable '[Proxy a] (Zeroable a #> a)
42 teZeroable_zero = Term (tyZeroable a0) a0 (teSym @Zeroable zero)