]> Git — Sourcephile - comptalang.git/blob - lcc/Hcompta/LCC/Sym/Unit.hs
Update to new symantic and draft Modules rendition.
[comptalang.git] / lcc / Hcompta / LCC / Sym / Unit.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 -- | Symantic for 'Unit'.
4 module Hcompta.LCC.Sym.Unit where
5
6 import Data.Eq (Eq)
7 import Data.Function (($), (.))
8 import Data.Maybe (Maybe(..))
9 import Data.Ord (Ord)
10 import Data.Proxy
11 import Data.Type.Equality ((:~:)(Refl))
12 import Text.Show (Show(..))
13 import qualified Language.Symantic.Typing as Sym
14
15 import Language.Symantic
16
17 import Hcompta.LCC.Amount
18
19 -- * Class 'Sym_Unit'
20 type instance Sym (Proxy Unit) = Sym_Unit
21 class Sym_Unit term where
22 unit :: Unit -> term Unit
23 default unit :: Sym_Unit (UnT term) => Trans term => Unit -> term Unit
24 unit = trans . unit
25
26 instance Sym_Unit Eval where
27 unit = Eval
28 instance Sym_Unit View where
29 unit (Unit u) = View $ \_p _v -> u
30 instance (Sym_Unit r1, Sym_Unit r2) => Sym_Unit (Dup r1 r2) where
31 unit x = unit x `Dup` unit x
32 instance (Sym_Unit term, Sym_Lambda term) => Sym_Unit (BetaT term)
33
34 instance ClassInstancesFor Unit where
35 proveConstraintFor _c (TyApp _ (TyConst _ _ q) c)
36 | Just HRefl <- proj_ConstKiTy @(K Unit) @Unit c
37 = case () of
38 _ | Just Refl <- proj_Const @Eq q -> Just Dict
39 | Just Refl <- proj_Const @Ord q -> Just Dict
40 | Just Refl <- proj_Const @Show q -> Just Dict
41 _ -> Nothing
42 proveConstraintFor _c _q = Nothing
43 instance TypeInstancesFor Unit
44 instance Gram_Term_AtomsFor src ss g Unit
45 instance (Source src, Inj_Sym ss Unit) => ModuleFor src ss Unit where
46 moduleFor = ["Unit"] `moduleWhere`
47 [
48 ]
49
50 tyUnit :: Source src => Inj_Len vs => Type src vs Unit
51 tyUnit = tyConst @(K Unit) @Unit
52
53 teUnit :: Source src => Inj_Sym ss Unit => Unit -> Term src ss ts '[] (() #> Unit)
54 teUnit a = Term noConstraint tyUnit $ teSym @Unit $ unit a