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

import Control.Monad (liftM)
import Data.Proxy
import Data.Type.Equality ((:~:)(Refl))
import qualified Data.Char as Char
import qualified Data.Text as Text

import Language.Symantic.Parsing hiding (char)
import qualified Language.Symantic.Grammar as Gram
import Language.Symantic.Typing
import Language.Symantic.Compiling
import Language.Symantic.Interpreting
import Language.Symantic.Transforming
import Language.Symantic.Lib.Lambda
import Language.Symantic.Lib.MonoFunctor (TyFam_MonoElement(..))

-- * Class '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 :: Trans t term => Char -> t term Char
	default char_toUpper :: Trans t term => t term Char -> t term Char
	default char_toLower :: Trans t term => t term Char -> t term Char
	
	char = trans_lift . char
	char_toUpper = trans_map1 char_toUpper
	char_toLower = trans_map1 char_toLower

type instance Sym_of_Iface (Proxy Char) = Sym_Char
type instance TyConsts_of_Iface (Proxy Char) = Proxy Char ': TyConsts_imported_by (Proxy Char)
type instance TyConsts_imported_by (Proxy Char) =
 [ Proxy Bounded
 , Proxy Enum
 , Proxy Eq
 , Proxy Ord
 , Proxy Show
 ]

instance Sym_Char HostI where
	char = HostI
	char_toUpper = liftM Char.toUpper
	char_toLower = liftM Char.toLower
instance Sym_Char TextI where
	char a = TextI $ \_p _v ->
		Text.pack (show a)
	char_toUpper = textI1 "Char.toUpper"
	char_toLower = textI1 "Char.toLower"
instance (Sym_Char r1, Sym_Char r2) => Sym_Char (DupI r1 r2) where
	char x = char x `DupI` char x
	char_toUpper = dupI1 @Sym_Char char_toUpper
	char_toLower = dupI1 @Sym_Char char_toLower

instance
 ( Read_TyNameR TyName cs rs
 , Inj_TyConst cs Char
 ) => Read_TyNameR TyName cs (Proxy Char ': rs) where
	read_TyNameR _cs (TyName "Char") k = k (ty @Char)
	read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
instance Show_TyConst cs => Show_TyConst (Proxy Char ': cs) where
	show_TyConst TyConstZ{} = "Char"
	show_TyConst (TyConstS c) = show_TyConst c

instance Proj_TyFamC cs TyFam_MonoElement Char

instance -- Proj_TyConC
 ( Proj_TyConst cs Char
 , Proj_TyConsts cs (TyConsts_imported_by (Proxy Char))
 ) => Proj_TyConC cs (Proxy Char) where
	proj_TyConC _ (TyConst q :$ TyConst c)
	 | Just Refl <- eq_skind (kind_of_TyConst c) SKiType
	 , Just Refl <- proj_TyConst c (Proxy @Char)
	 = case () of
		 _ | Just Refl <- proj_TyConst q (Proxy @Bounded) -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Enum)    -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Eq)      -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Ord)     -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Show)    -> Just TyCon
		 _ -> Nothing
	proj_TyConC _c _q = Nothing
data instance TokenT meta (ts::[*]) (Proxy Char)
 = Token_Term_Char Char
 | Token_Term_Char_toUpper
 | Token_Term_Char_toLower
deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Char))
deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Char))

instance -- CompileI
 ( Inj_TyConst cs Char
 , Inj_TyConst cs (->)
 ) => CompileI cs is (Proxy Char) where
	compileI tok _ctx k =
		case tok of
		 Token_Term_Char c -> k (ty @Char) $ Term $ \_c -> char c
		 Token_Term_Char_toUpper -> from_op char_toUpper
		 Token_Term_Char_toLower -> from_op char_toLower
		where
		from_op (op::forall term. Sym_Char term => term Char -> term Char) =
			k (ty @Char ~> ty @Char) $ Term $ \_c -> lam op
instance -- TokenizeT
 Inj_Token meta ts Char =>
 TokenizeT meta ts (Proxy Char) where
	tokenizeT _t = mempty
	 { tokenizers_infix = tokenizeTMod [Mod_Name "Char"]
		 [ tokenize0 "toLower" infixN5 Token_Term_Char_toLower
		 , tokenize0 "toUpper" infixN5 Token_Term_Char_toUpper
		 ]
	 }
instance -- Gram_Term_AtomsT
 ( Alt g
 , Gram_Rule g
 , Gram_Lexer g
 , Gram_Meta meta g
 , Inj_Token meta ts Char
 ) => Gram_Term_AtomsT meta ts (Proxy Char) g where
	gs_term_atomsT _t =
	 [ rule "term_char" $
		lexeme $ metaG $
		(\c meta -> ProTok $ inj_EToken meta $ Token_Term_Char c)
		 <$> Gram.between tickG tickG (
			Gram.cf_of_Terminal (Gram.any `Gram.but` tickG) Gram.<+>
			'\'' <$ Gram.string "\\'"
		 )
	 ]
		where
		tickG :: Gram_Terminal g' => g' Char
		tickG = Gram.char '\''