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

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

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

-- * 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 Consts_of_Iface (Proxy Char) = Proxy Char ': Consts_imported_by Char
type instance Consts_imported_by 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 (Proxy @Sym_Char) char_toUpper
	char_toLower = dupI1 (Proxy @Sym_Char) char_toLower

instance
 ( Read_TypeNameR Type_Name cs rs
 , Inj_Const cs Char
 ) => Read_TypeNameR Type_Name cs (Proxy Char ': rs) where
	read_typenameR _cs (Type_Name "Char") k = k (ty @Char)
	read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy Char ': cs) where
	show_const ConstZ{} = "Char"
	show_const (ConstS c) = show_const c

instance -- Proj_ConC
 ( Proj_Const cs Char
 , Proj_Consts cs (Consts_imported_by Char)
 ) => Proj_ConC cs (Proxy Char) where
	proj_conC _ (TyConst q :$ TyConst c)
	 | Just Refl <- eq_skind (kind_of_const c) SKiType
	 , Just Refl <- proj_const c (Proxy @Char)
	 = case () of
		 _ | Just Refl <- proj_const q (Proxy @Bounded) -> Just Con
		   | Just Refl <- proj_const q (Proxy @Enum)    -> Just Con
		   | Just Refl <- proj_const q (Proxy @Eq)      -> Just Con
		   | Just Refl <- proj_const q (Proxy @Ord)     -> Just Con
		   | Just Refl <- proj_const q (Proxy @Show)    -> Just Con
		 _ -> Nothing
	proj_conC _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_Const (Consts_of_Ifaces is) Char
 , Inj_Const (Consts_of_Ifaces is) (->)
 ) => CompileI is (Proxy Char) where
	compileI tok _ctx k =
		case tok of
		 Token_Term_Char c -> k (ty @Char) $ TermO $ \_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) $ TermO $ \_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
	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_term (Gram.any `Gram.but` tickG) Gram.<+>
			'\'' <$ Gram.string "\\'"
		 )
	 ]
		where
		tickG :: Gram_Terminal g' => g' Char
		tickG = Gram.char '\''