{-# 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