{-# 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 NameTyOf Show where
        nameTyOf _c = ["Show"] `Mod` "Show"
instance FixityOf Show
instance ClassInstancesFor Show
instance TypeInstancesFor Show

-- Compiling
instance Gram_Term_AtomsFor src ss g Show
instance (Source src, SymInj 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 => LenInj 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