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

import Data.Char (Char)
import Data.Eq (Eq)
import Data.Function (($), (.))
import Data.Functor ((<$>), (<$))
import Data.Maybe (Maybe(..))
import Data.Ord (Ord)
import Data.String (String)
import Prelude (Bounded, Enum)
import Text.Show (Show(..))
import qualified Data.Char as Char
import qualified Data.Text as Text

import Language.Symantic.Grammar hiding (char)
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 NameTyOf Char where
        nameTyOf _c = ["Char"] `Mod` "Char"
instance ClassInstancesFor Char where
        proveConstraintFor _ (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
 , SymInj 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_Char g' => g' Char
                tickG = G.char '\''
instance (Source src, SymInj ss Char) => ModuleFor src ss Char where
        moduleFor = ["Char"] `moduleWhere`
         [ "toLower" := teChar_toLower
         , "toUpper" := teChar_toUpper
         ]

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

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

-- ** 'Term's
teChar :: Source src => SymInj 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