{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for 'Char'.
module Language.Symantic.Compiling.Char where

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

import Language.Symantic.Typing
import Language.Symantic.Compiling.Term
import Language.Symantic.Interpreting
import Language.Symantic.Transforming.Trans

-- * Class 'Sym_Char'
class Sym_Char term where
	char :: Char -> term Char
	char_toUpper :: 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
	
	char = trans_lift . char
	char_toUpper = trans_map1 char_toUpper

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
 ]

instance Sym_Char HostI where
	char = HostI
	char_toUpper = liftM Char.toUpper
instance Sym_Char TextI where
	char a = TextI $ \_p _v ->
		Text.pack (show a)
	char_toUpper = textI_app1 "char_toUpper"
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

instance Const_from Text cs => Const_from Text (Proxy Char ': cs) where
	const_from "Char" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
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::Proxy Char)
	 = Just $ case () of
		 _ | Just Refl <- proj_const q (Proxy::Proxy Bounded) -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Enum)    -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Eq)      -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Ord)     -> Just Con
		 _ -> Nothing
	proj_conC _c _q = Nothing
instance -- Term_fromI
 ( AST ast
 , Lexem ast ~ LamVarName
 , Inj_Const (Consts_of_Ifaces is) Char
 , Inj_Const (Consts_of_Ifaces is) (->)
 , Show_Const (Consts_of_Ifaces is)
 ) => Term_fromI is (Proxy Char) ast where
	term_fromI ast _ctx k =
		case ast_lexem ast of
		 "char" -> char_from
		 "char_toUpper" -> char_toUpper_from
		 _ -> Left $ Error_Term_unsupported
		where
		char_from =
			let ty = tyChar in
			from_ast1 ast $ \ast_lit as ->
			from_lex (Text.pack $ show_type ty) ast_lit $ \(lit::Char) ->
			k as ty $ TermLC $ Fun.const $ char lit
		char_toUpper_from =
			from_ast0 ast $ \_ as ->
			k as (tyChar ~> tyChar) $ TermLC $
			Fun.const $ lam char_toUpper

-- | The 'Char' 'Type'
tyChar :: Inj_Const cs Char => Type cs Char
tyChar = TyConst inj_const

sym_Char :: Proxy Sym_Char
sym_Char = Proxy

syChar :: IsString a => Syntax a
syChar = Syntax "Char" []