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

import Control.Monad
import Data.Proxy (Proxy(..))
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (Show(..))
import Text.Show (Show)
import qualified Text.Show as Show

import Language.Symantic.Parsing
import Language.Symantic.Typing
import Language.Symantic.Compiling
import Language.Symantic.Interpreting
import Language.Symantic.Transforming
import Language.Symantic.Lib.Lambda

-- * Class 'Sym_Show'
class Sym_Show term where
	showsPrec :: Show a => term Int -> term a -> term ShowS
	show      :: Show a => term a -> term String
	showList  :: Show a => term [a] -> term ShowS
	
	default showsPrec :: (Trans t term, Show a) => t term Int -> t term a -> t term ShowS
	default show      :: (Trans t term, Show a) => t term a -> t term String
	default showList  :: (Trans t term, Show a) => t term [a] -> t term ShowS
	
	showsPrec = trans_map2 showsPrec
	show      = trans_map1 show
	showList  = trans_map1 showList

type instance Sym_of_Iface (Proxy Show) = Sym_Show
type instance TyConsts_of_Iface (Proxy Show) = Proxy Show ': TyConsts_imported_by (Proxy Show)
type instance TyConsts_imported_by (Proxy Show) =
 [ Proxy []
 , Proxy Char
 , Proxy Int
 ]

instance Sym_Show HostI where
	showsPrec = liftM2 Show.showsPrec
	show      = liftM  Show.show
	showList  = liftM  Show.showList
instance Sym_Show TextI where
	showsPrec = textI2 "showsPrec"
	show      = textI1 "show"
	showList  = textI1 "showList"
instance (Sym_Show r1, Sym_Show r2) => Sym_Show (DupI r1 r2) where
	showsPrec = dupI2 @Sym_Show showsPrec
	show      = dupI1 @Sym_Show show
	showList  = dupI1 @Sym_Show showList

instance
 ( Read_TyNameR TyName cs rs
 , Inj_TyConst cs Show
 ) => Read_TyNameR TyName cs (Proxy Show ': rs) where
	read_TyNameR _cs (TyName "Show") k = k (ty @Show)
	read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
instance Show_TyConst cs => Show_TyConst (Proxy Show ': cs) where
	show_TyConst TyConstZ{} = "Show"
	show_TyConst (TyConstS c) = show_TyConst c

instance Proj_TyConC cs (Proxy Show)
data instance TokenT meta (ts::[*]) (Proxy Show)
 = Token_Term_Show_showsPrec (EToken meta ts) (EToken meta ts)
 | Token_Term_Show_show      (EToken meta ts)
 | Token_Term_Show_showList  (EToken meta ts)
deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Show))
deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Show))

instance -- CompileI
 ( Inj_TyConst cs Show
 , Inj_TyConst cs (->)
 , Inj_TyConsts cs (TyConsts_imported_by (Proxy Show))
 , Proj_TyCon cs
 , Compile cs is
 ) => CompileI cs is (Proxy Show) where
	compileI tok ctx k =
		case tok of
		 Token_Term_Show_showsPrec tok_p tok_a ->
			compileO tok_p ctx $ \ty_p (TermO p) ->
			compileO tok_a ctx $ \ty_a (TermO a) ->
			check_TyEq (At Nothing (ty @Int)) (At (Just tok_p) ty_p) $ \Refl ->
			check_TyCon (At (Just tok_a) (ty @Show :$ ty_a)) $ \TyCon ->
			k tyShowS $ TermO $
			 \c -> showsPrec (p c) (a c)
		 Token_Term_Show_show      tok_a ->
			compileO tok_a ctx $ \ty_a (TermO a) ->
			check_TyCon (At (Just tok_a) (ty @Show :$ ty_a)) $ \TyCon ->
			k tyString $ TermO $
			 \c -> show (a c)
		 Token_Term_Show_showList tok_as ->
			compileO tok_as ctx $ \ty_as (TermO as) ->
			check_TyEq1 (ty @[]) (At (Just tok_as) ty_as) $ \Refl ty_a ->
			check_TyCon (At (Just tok_as) (ty @Show :$ ty_a)) $ \TyCon ->
			k tyShowS $ TermO $
			 \c -> showList (as c)
		where
		tyString = ty @[] :$ ty @Char
		tyShowS  = tyString ~> tyString
instance -- TokenizeT
 Inj_Token meta ts Show =>
 TokenizeT meta ts (Proxy Show) where
	tokenizeT _t = mempty
	 { tokenizers_infix = tokenizeTMod []
		 [ tokenize2 "showsPrec" infixN5 Token_Term_Show_showsPrec
		 , tokenize1 "show"      infixN5 Token_Term_Show_show
		 , tokenize1 "showList"  infixN5 Token_Term_Show_showList
		 ]
	 }
instance Gram_Term_AtomsT meta ts (Proxy Show) g