]> Git — Sourcephile - comptalang.git/blob - lcc/Hcompta/LCC/Sym/Unit.hs
Commit old WIP.
[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.Type.Equality ((:~:)(Refl))
11 import Text.Show (Show(..))
12 import qualified Language.Symantic.Typing as Sym
13
14 import Language.Symantic
15
16 import Hcompta.LCC.Amount
17
18 -- * Class 'Sym_Unit'
19 type instance Sym Unit = Sym_Unit
20 class Sym_Unit term where
21 unit :: Unit -> term Unit
22 default unit :: Sym_Unit (UnT term) => Trans term => Unit -> term Unit
23 unit = trans . unit
24
25 instance Sym_Unit Eval where
26 unit = Eval
27 instance Sym_Unit View where
28 unit (Unit u) = View $ \_p _v -> u
29 instance (Sym_Unit r1, Sym_Unit r2) => Sym_Unit (Dup r1 r2) where
30 unit x = unit x `Dup` unit x
31 instance (Sym_Unit term, Sym_Lambda term) => Sym_Unit (BetaT term)
32
33 instance NameTyOf Unit where
34 nameTyOf _c = ["Unit"] `Mod` "Unit"
35 instance ClassInstancesFor Unit where
36 proveConstraintFor _c (TyConst _ _ q :$ c)
37 | Just HRefl <- proj_ConstKiTy @(K Unit) @Unit c
38 = case () of
39 _ | Just Refl <- proj_Const @Eq q -> Just Dict
40 | Just Refl <- proj_Const @Ord q -> Just Dict
41 | Just Refl <- proj_Const @Show q -> Just Dict
42 _ -> Nothing
43 proveConstraintFor _c _q = Nothing
44 instance TypeInstancesFor Unit
45 instance Gram_Term_AtomsFor src ss g Unit
46 instance (Source src, SymInj ss Unit) => ModuleFor src ss Unit where
47 moduleFor = ["Unit"] `moduleWhere`
48 [
49 ]
50
51 tyUnit :: Source src => LenInj vs => Type src vs Unit
52 tyUnit = tyConst @(K Unit) @Unit
53
54 teUnit :: Source src => SymInj ss Unit => Unit -> Term src ss ts '[] (() #> Unit)
55 teUnit a = Term noConstraint tyUnit $ teSym @Unit $ unit a