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