{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fconstraint-solver-iterations=6 #-}
-- | Symantic for 'Text'.
module Language.Symantic.Lib.Text where

import Data.Proxy
import Data.Text (Text)
import Data.Type.Equality ((:~:)(Refl))
import qualified Data.MonoTraversable as MT
import qualified Data.Sequences as Seqs
import qualified Data.Text as Text

import Language.Symantic.Parsing
import Language.Symantic.Typing
import Language.Symantic.Compiling
import Language.Symantic.Interpreting
import Language.Symantic.Transforming
import Language.Symantic.Lib.MonoFunctor (TyFam_MonoElement(..))

-- * 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 TyConsts_of_Iface (Proxy Text) = Proxy Text ': TyConsts_imported_by (Proxy Text)
type instance TyConsts_imported_by (Proxy Text) =
 [ Proxy Eq
 , Proxy MT.MonoFoldable
 , Proxy MT.MonoFunctor
 , Proxy Monoid
 , Proxy Ord
 , Proxy Seqs.IsSequence
 , Proxy Seqs.SemiSequence
 , Proxy Show
 ]

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
 ( Read_TyNameR TyName cs rs
 , Inj_TyConst cs Text
 ) => Read_TyNameR TyName cs (Proxy Text ': rs) where
	read_TyNameR _cs (TyName "Text") k = k (ty @Text)
	read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
instance Show_TyConst cs => Show_TyConst (Proxy Text ': cs) where
	show_TyConst TyConstZ{} = "Text"
	show_TyConst (TyConstS c) = show_TyConst c

instance -- Proj_TyFamC TyFam_MonoElement
 ( Proj_TyConst cs Text
 , Inj_TyConst cs (MT.Element Text)
 ) => Proj_TyFamC cs TyFam_MonoElement Text where
	proj_TyFamC _c _fam (TyConst c `TypesS` TypesZ)
	 | Just Refl <- eq_skind (kind_of_TyConst c) SKiType
	 , Just Refl <- proj_TyConst c (Proxy @Text)
	 = Just (TyConst inj_TyConst::Type cs (MT.Element Text))
	proj_TyFamC _c _fam _ty = Nothing

instance -- Proj_TyConC
 ( Proj_TyConst cs Text
 , Proj_TyConsts cs (TyConsts_imported_by (Proxy Text))
 ) => Proj_TyConC cs (Proxy Text) where
	proj_TyConC _ (TyConst q :$ TyConst c)
	 | Just Refl <- eq_skind (kind_of_TyConst c) SKiType
	 , Just Refl <- proj_TyConst c (Proxy @Text)
	 = case () of
		 _ | Just Refl <- proj_TyConst q (Proxy @Eq)                -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @MT.MonoFoldable)   -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @MT.MonoFunctor)    -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Monoid)            -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Ord)               -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Seqs.IsSequence)   -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Seqs.SemiSequence) -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Show)              -> Just TyCon
		 _ -> Nothing
	proj_TyConC _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 -- CompileI
 Inj_TyConst cs Text =>
 CompileI cs is (Proxy Text) where
	compileI tok _ctx k =
		case tok of
		 Token_Term_Text i -> k (ty @Text) $ TermO $ \_c -> text i
instance -- TokenizeT
 -- Inj_Token meta ts Text =>
 TokenizeT meta ts (Proxy Text)
instance Gram_Term_AtomsT meta ts (Proxy Text) g -- TODO