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

import Control.Monad
import Data.Proxy (Proxy(..))
import Data.Text (Text)
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.Term
import Language.Symantic.Interpreting
import Language.Symantic.Transforming.Trans

-- * 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 Consts_of_Iface (Proxy Show) = Proxy Show ': Consts_imported_by Show
type instance Consts_imported_by Show =
 [ Proxy []
 , 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 (Proxy @Sym_Show) showsPrec
	show      = dupI1 (Proxy @Sym_Show) show
	showList  = dupI1 (Proxy @Sym_Show) showList

instance
 ( Read_TypeNameR Text cs rs
 , Inj_Const cs Show
 ) => Read_TypeNameR Text cs (Proxy Show ': rs) where
	read_typenameR _cs "Show" k = k (ty @Show)
	read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy Show ': cs) where
	show_const ConstZ{} = "Show"
	show_const (ConstS c) = show_const c

instance Proj_ConC 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_Const (Consts_of_Ifaces is) (->)
 , Inj_Const (Consts_of_Ifaces is) Char
 , Inj_Const (Consts_of_Ifaces is) Int
 , Inj_Const (Consts_of_Ifaces is) Show
 , Inj_Const (Consts_of_Ifaces is) []
 , Proj_Con (Consts_of_Ifaces is)
 , Compile is
 ) => CompileI 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_type (At Nothing (ty @Int)) (At (Just tok_p) ty_p) $ \Refl ->
			check_con (At (Just tok_a) (ty @Show :$ ty_a)) $ \Con ->
			k tyShowS $ TermO $
			 \c -> showsPrec (p c) (a c)
		 Token_Term_Show_show      tok_a ->
			compileO tok_a ctx $ \ty_a (TermO a) ->
			check_con (At (Just tok_a) (ty @Show :$ ty_a)) $ \Con ->
			k tyString $ TermO $
			 \c -> show (a c)
		 Token_Term_Show_showList tok_as ->
			compileO tok_as ctx $ \ty_as (TermO as) ->
			check_type1 (ty @[]) (At (Just tok_as) ty_as) $ \Refl ty_a ->
			check_con (At (Just tok_as) (ty @Show :$ ty_a)) $ \Con ->
			k tyShowS $ TermO $
			 \c -> showList (as c)
		where
		tyString = ty @[] :$ ty @Char
		tyShowS  = tyString ~> tyString