]> Git — Sourcephile - comptalang.git/blob - lcc/Hcompta/LCC/Sym/Chart.hs
Commit old WIP.
[comptalang.git] / lcc / Hcompta / LCC / Sym / Chart.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 -- | Symantic for 'Chart'.
4 module Hcompta.LCC.Sym.Chart where
5
6 import Data.Eq (Eq)
7 import Data.Maybe (Maybe(..))
8 import Text.Show (Show(..))
9
10 import Hcompta.LCC.Chart (Chart)
11 import Language.Symantic
12
13 -- * Class 'Sym_Chart'
14 type instance Sym Chart = Sym_Chart
15 class Sym_Chart (term:: * -> *) where
16
17 instance Sym_Chart Eval where
18 instance Sym_Chart View where
19 instance (Sym_Chart r1, Sym_Chart r2) => Sym_Chart (Dup r1 r2) where
20 instance (Sym_Chart term, Sym_Lambda term) => Sym_Chart (BetaT term)
21
22 instance NameTyOf Chart where
23 nameTyOf _c = ["Chart"] `Mod` "Chart"
24 instance ClassInstancesFor Chart where
25 proveConstraintFor _ (TyConst _ _ q :$ a)
26 | Just HRefl <- proj_ConstKiTy @(K Chart) @Chart a
27 = case () of
28 _ | Just Refl <- proj_Const @Eq q -> Just Dict
29 | Just Refl <- proj_Const @Show q -> Just Dict
30 _ -> Nothing
31 proveConstraintFor _c _q = Nothing
32 instance TypeInstancesFor Chart where
33
34 instance Gram_Term_AtomsFor src ss g Chart
35 instance (Source src, SymInj ss Chart) => ModuleFor src ss Chart where
36 moduleFor = ["Chart"] `moduleWhere`
37 [
38 ]
39
40 tyChart :: Source src => LenInj vs => Type src vs Chart
41 tyChart = tyConst @(K Chart) @Chart