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

import Data.Proxy
import Data.Text (Text)
import qualified Data.Text as Text
import Data.Type.Equality ((:~:)(Refl))

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

-- * Class 'Sym_Text'
class Sym_Text term where
	text :: Text -> term Text
	default text :: Trans t term => Text -> t term Text
	text = trans_lift . text

type instance Sym_of_Iface (Proxy Text) = Sym_Text
type instance Consts_of_Iface (Proxy Text) = Proxy Text ': Consts_imported_by Text
type instance Consts_imported_by Text =
 [ Proxy Eq
 , Proxy Monoid
 , Proxy Ord
 ]

instance Sym_Text HostI where
	text = HostI
instance Sym_Text TextI where
	text a = TextI $ \_p _v ->
		Text.pack (show a)
instance (Sym_Text r1, Sym_Text r2) => Sym_Text (DupI r1 r2) where
	text x = text x `DupI` text x

instance Const_from Text cs => Const_from Text (Proxy Text ': cs) where
	const_from "Text" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Show_Const cs => Show_Const (Proxy Text ': cs) where
	show_const ConstZ{} = "Text"
	show_const (ConstS c) = show_const c

instance -- Proj_ConC
 ( Proj_Const cs Text
 , Proj_Consts cs (Consts_imported_by Text)
 ) => Proj_ConC cs (Proxy Text) where
	proj_conC _ (TyConst q :$ TyConst c)
	 | Just Refl <- eq_skind (kind_of_const c) SKiType
	 , Just Refl <- proj_const c (Proxy::Proxy Text)
	 = case () of
		 _ | Just Refl <- proj_const q (Proxy::Proxy Eq)     -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Monoid) -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Ord)    -> Just Con
		 _ -> Nothing
	proj_conC _c _q = Nothing
data instance TokenT meta (ts::[*]) (Proxy Text)
 = Token_Term_Text Text
deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Text))
deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Text))
instance -- Term_fromI
 Inj_Const (Consts_of_Ifaces is) Text =>
 Term_fromI is (Proxy Text) where
	term_fromI tok _ctx k =
		case tok of
		 Token_Term_Text i -> k tyText $ TermLC $ \_c -> text i

-- | The 'Text' 'Type'
tyText :: Inj_Const cs Text => Type cs Text
tyText = TyConst inj_const

sym_Text :: Proxy Sym_Text
sym_Text = Proxy

{-
syText :: IsString a => Syntax a
syText = Syntax "Text" []
-}