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

import Data.Text (Text)
import qualified Data.MonoTraversable as MT
import qualified Data.Sequences as Seqs
import qualified Data.Text as Text

import Language.Symantic.Grammar hiding (text)
import Language.Symantic
import Language.Symantic.Lib.Char ()
import Language.Symantic.Lib.MonoFunctor (Element)

-- * Class 'Sym_Text'
type instance Sym Text = Sym_Text
class Sym_Text term where
	text :: Text -> term Text
	default text :: Sym_Text (UnT term) => Trans term => Text -> term Text
	text = trans . text

-- Interpreting
instance Sym_Text Eval where
	text = Eval
instance Sym_Text View where
	text a = View $ \_p _v ->
		Text.pack (show a)
instance (Sym_Text r1, Sym_Text r2) => Sym_Text (Dup r1 r2) where
	text x = text x `Dup` text x

-- Transforming
instance (Sym_Text term, Sym_Lambda term) => Sym_Text (BetaT term)

-- Typing
instance NameTyOf Text where
	nameTyOf _c = ["Text"] `Mod` "Text"
instance ClassInstancesFor Text where
	proveConstraintFor _ (TyConst _ _ q :$ c)
	 | Just HRefl <- proj_ConstKiTy @_ @Text c
	 = case () of
		 _ | Just Refl <- proj_Const @Eq                q -> Just Dict
		   | Just Refl <- proj_Const @MT.MonoFoldable   q -> Just Dict
		   | Just Refl <- proj_Const @MT.MonoFunctor    q -> Just Dict
		   | Just Refl <- proj_Const @Monoid            q -> Just Dict
		   | Just Refl <- proj_Const @Ord               q -> Just Dict
		   | Just Refl <- proj_Const @Seqs.IsSequence   q -> Just Dict
		   | Just Refl <- proj_Const @Seqs.SemiSequence q -> Just Dict
		   | Just Refl <- proj_Const @Show              q -> Just Dict
		 _ -> Nothing
	proveConstraintFor _c _q = Nothing
instance TypeInstancesFor Text where
	expandFamFor _c len f (c `TypesS` TypesZ)
	 | Just HRefl <- proj_ConstKi @_ @Element f
	 , Just HRefl <- proj_ConstKiTy @_ @Text c
	 = Just $ tyConstLen @(K (MT.Element Text)) @(MT.Element Text) len
	expandFamFor _c _len _fam _as = Nothing

-- Compiling
instance Gram_Term_AtomsFor src ss g Text -- TODO
instance ModuleFor src ss Text

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

-- ** 'Term's
teText :: Source src => SymInj ss Text => Text -> Term src ss ts '[] (() #> Text)
teText t = Term noConstraint tyText $ teSym @Text $ text t