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

import Prelude hiding (Show(..))
import Text.Show (Show)
import qualified Text.Show as Show

import Language.Symantic
import Language.Symantic.Lib.Char (tyString)
import Language.Symantic.Lib.Function (a0)
import Language.Symantic.Lib.Int (tyInt)
import Language.Symantic.Lib.List (tyList)

-- * Class 'Sym_Show'
type instance Sym Show = 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 :: Sym_Show (UnT term) => Trans term => Show a => term Int -> term a -> term ShowS
	default show      :: Sym_Show (UnT term) => Trans term => Show a => term a -> term String
	default showList  :: Sym_Show (UnT term) => Trans term => Show a => term [a] -> term ShowS
	
	showsPrec = trans2 showsPrec
	show      = trans1 show
	showList  = trans1 showList

instance Sym_Show Eval where
	showsPrec = eval2 Show.showsPrec
	show      = eval1 Show.show
	showList  = eval1 Show.showList
instance Sym_Show View where
	showsPrec = view2 "showsPrec"
	show      = view1 "show"
	showList  = view1 "showList"
instance (Sym_Show r1, Sym_Show r2) => Sym_Show (Dup r1 r2) where
	showsPrec = dup2 @Sym_Show showsPrec
	show      = dup1 @Sym_Show show
	showList  = dup1 @Sym_Show showList

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

-- Typing
instance FixityOf Show
instance ClassInstancesFor Show
instance TypeInstancesFor Show

-- Compiling
instance Gram_Term_AtomsFor src ss g Show
instance (Source src, Inj_Sym ss Show) => ModuleFor src ss Show where
	moduleFor = ["Show"] `moduleWhere`
	 [ "showsPrec" := teShow_showsPrec
	 , "show"      := teShow_show
	 , "showList"  := teShow_showList
	 ]

-- ** 'Type's
tyShow :: Source src => Type src vs a -> Type src vs (Show a)
tyShow a = tyConstLen @(K Show) @Show (lenVars a) `tyApp` a

tyShowS :: Source src => Inj_Len vs => Type src vs ShowS
tyShowS = tyString ~> tyString

-- ** 'Term's
teShow_showsPrec :: TermDef Show '[Proxy a] (Show a #> (Int -> a -> ShowS))
teShow_showsPrec = Term (tyShow a0) (tyInt ~> a0 ~> tyShowS) $ teSym @Show $ lam2 showsPrec

teShow_show :: TermDef Show '[Proxy a] (Show a #> (a -> String))
teShow_show = Term (tyShow a0) (a0 ~> tyString) $ teSym @Show $ lam1 show

teShow_showList :: TermDef Show '[Proxy a] (Show a #> ([a] -> ShowS))
teShow_showList = Term (tyShow a0) (tyList a0 ~> tyShowS) $ teSym @Show $ lam1 showList