{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for 'Chart'.
module Hcompta.LCC.Sym.Chart where

import Data.Eq (Eq)
import Data.Maybe (Maybe(..))
import Text.Show (Show(..))

import Hcompta.LCC.Chart (Chart)
import Language.Symantic

-- * Class 'Sym_Chart'
type instance Sym Chart = Sym_Chart
class Sym_Chart (term:: * -> *) where

instance Sym_Chart Eval where
instance Sym_Chart View where
instance (Sym_Chart r1, Sym_Chart r2) => Sym_Chart (Dup r1 r2) where
instance (Sym_Chart term, Sym_Lambda term) => Sym_Chart (BetaT term)

instance NameTyOf Chart where
	nameTyOf _c = ["Chart"] `Mod` "Chart"
instance ClassInstancesFor Chart where
	proveConstraintFor _ (TyConst _ _ q :$ a)
	 | Just HRefl <- proj_ConstKiTy @(K Chart) @Chart a
	 = case () of
		 _ | Just Refl <- proj_Const @Eq   q -> Just Dict
		   | Just Refl <- proj_Const @Show q -> Just Dict
		 _ -> Nothing
	proveConstraintFor _c _q = Nothing
instance TypeInstancesFor Chart where

instance Gram_Term_AtomsFor src ss g Chart
instance (Source src, SymInj ss Chart) => ModuleFor src ss Chart where
	moduleFor = ["Chart"] `moduleWhere`
	 [
	 ]

tyChart :: Source src => LenInj vs => Type src vs Chart
tyChart = tyConst @(K Chart) @Chart