{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for 'Char'.
module Language.Symantic.Lib.Char where

import qualified Data.Char as Char
import qualified Data.Text as Text

import Language.Symantic.Grammar hiding (char, any)
import qualified Language.Symantic.Grammar as Gram
import Language.Symantic
import Language.Symantic.Lib.List (tyList)

-- * Class 'Sym_Char'
type instance Sym (Proxy Char) = Sym_Char
class Sym_Char term where
	char :: Char -> term Char
	char_toUpper :: term Char -> term Char
	char_toLower :: term Char -> term Char
	
	default char         :: Sym_Char (UnT term) => Trans term => Char -> term Char
	default char_toUpper :: Sym_Char (UnT term) => Trans term => term Char -> term Char
	default char_toLower :: Sym_Char (UnT term) => Trans term => term Char -> term Char
	
	char         = trans . char
	char_toUpper = trans1 char_toUpper
	char_toLower = trans1 char_toLower

-- Interpreting
instance Sym_Char Eval where
	char         = Eval
	char_toUpper = eval1 Char.toUpper
	char_toLower = eval1 Char.toLower
instance Sym_Char View where
	char a = View $ \_p _v ->
		Text.pack (show a)
	char_toUpper = view1 "Char.toUpper"
	char_toLower = view1 "Char.toLower"
instance (Sym_Char r1, Sym_Char r2) => Sym_Char (Dup r1 r2) where
	char x       = char x `Dup` char x
	char_toUpper = dup1 @Sym_Char char_toUpper
	char_toLower = dup1 @Sym_Char char_toLower

-- Transforming
instance (Sym_Char term, Sym_Lambda term) => Sym_Char (BetaT term)

-- Typing
instance ClassInstancesFor Char where
	proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
	 | Just HRefl <- proj_ConstKiTy @_ @Char z
	 = case () of
		 _ | Just Refl <- proj_Const @Bounded q -> Just Dict
		   | Just Refl <- proj_Const @Enum    q -> Just Dict
		   | Just Refl <- proj_Const @Eq      q -> Just Dict
		   | Just Refl <- proj_Const @Ord     q -> Just Dict
		   | Just Refl <- proj_Const @Show    q -> Just Dict
		 _ -> Nothing
	proveConstraintFor _c _q = Nothing
instance TypeInstancesFor Char

-- Compiling
instance
 ( Gram_Source src g
 , Gram_Alt g
 , Gram_Rule g
 , Gram_Comment g
 , Inj_Sym ss Char
 ) => Gram_Term_AtomsFor src ss g Char where
	g_term_atomsFor _t =
	 [ rule "teChar" $
		lexeme $ g_source $
		(\c src -> BinTree0 $ Token_Term $ TermVT_CF $ (`setSource` src) $ teChar c)
		 <$> between tickG tickG (
			cf_of_Terminal (Gram.any `but` tickG) <+>
			'\'' <$ string "\\'"
		 )
	 ]
		where
		tickG :: Gram_Terminal g' => g' Char
		tickG = Gram.char '\''
instance (Source src, Inj_Sym ss Char) => ModuleFor src ss Char where
	moduleFor _s = ["Char"] `moduleWhere`
	 [ "toLower" := teChar_toLower
	 , "toUpper" := teChar_toUpper
	 ]

-- ** 'Type's
tyChar :: Source src => Inj_Len vs => Type src vs Char
tyChar = tyConst @(K Char) @Char

tyString :: Source src => Inj_Len vs => Type src vs String
tyString = tyList tyChar

-- ** 'Term's
teChar :: Source src => Inj_Sym ss Char => Char -> Term src ss ts '[] Char
teChar b = Term noConstraint tyChar $ teSym @Char $ char b

teChar_toUpper, teChar_toLower :: TermDef Char '[] (Char -> Char)
teChar_toUpper = Term noConstraint (tyChar ~> tyChar) $ teSym @Char $ lam1 char_toUpper
teChar_toLower = Term noConstraint (tyChar ~> tyChar) $ teSym @Char $ lam1 char_toLower