{-# 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 G
import Language.Symantic
import Language.Symantic.Lib.List (tyList)

-- * Class 'Sym_Char'
type instance Sym 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 =
	 [ rule "teChar" $
		lexeme $ source $
		(\c src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teChar c)
		 <$> between tickG tickG (
			cfOf (G.any `but` tickG) <+>
			'\'' <$ string "\\'"
		 )
	 ]
		where
		tickG :: Gram_Terminal g' => g' Char
		tickG = G.char '\''
instance (Source src, Inj_Sym ss Char) => ModuleFor src ss Char where
	moduleFor = ["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