Language/Symantic/Compiling/Show.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Show'.
   4 module Language.Symantic.Compiling.Show where
   5
   6 import Control.Monad
   7 import Data.Proxy (Proxy(..))
   8 import Data.Text (Text)
   9 import Data.Type.Equality ((:~:)(Refl))
  10 import Prelude hiding (Show(..))
  11 import Text.Show (Show)
  12 import qualified Text.Show as Show
  13
  14 import Language.Symantic.Parsing
  15 import Language.Symantic.Typing
  16 import Language.Symantic.Compiling.Term
  17 import Language.Symantic.Interpreting
  18 import Language.Symantic.Transforming.Trans
  19
  20 -- * Class 'Sym_Show'
  21 class Sym_Show term where
  22         showsPrec :: Show a => term Int -> term a -> term ShowS
  23         show      :: Show a => term a -> term String
  24         showList  :: Show a => term [a] -> term ShowS
  25
  26         default showsPrec :: (Trans t term, Show a) => t term Int -> t term a -> t term ShowS
  27         default show      :: (Trans t term, Show a) => t term a -> t term String
  28         default showList  :: (Trans t term, Show a) => t term [a] -> t term ShowS
  29
  30         showsPrec = trans_map2 showsPrec
  31         show      = trans_map1 show
  32         showList  = trans_map1 showList
  33
  34 type instance Sym_of_Iface (Proxy Show) = Sym_Show
  35 type instance Consts_of_Iface (Proxy Show) = Proxy Show ': Consts_imported_by Show
  36 type instance Consts_imported_by Show =
  37  [ Proxy []
  38  , Proxy (->)
  39  , Proxy Char
  40  , Proxy Int
  41  ]
  42
  43 instance Sym_Show HostI where
  44         showsPrec = liftM2 Show.showsPrec
  45         show      = liftM  Show.show
  46         showList  = liftM  Show.showList
  47 instance Sym_Show TextI where
  48         showsPrec = textI_app2 "showsPrec"
  49         show      = textI_app1 "show"
  50         showList  = textI_app1 "showList"
  51 instance (Sym_Show r1, Sym_Show r2) => Sym_Show (DupI r1 r2) where
  52         showsPrec = dupI2 (Proxy @Sym_Show) showsPrec
  53         show      = dupI1 (Proxy @Sym_Show) show
  54         showList  = dupI1 (Proxy @Sym_Show) showList
  55
  56 instance Const_from Text cs => Const_from Text (Proxy Show ': cs) where
  57         const_from "Show" k = k (ConstZ kind)
  58         const_from s k = const_from s $ k . ConstS
  59 instance Show_Const cs => Show_Const (Proxy Show ': cs) where
  60         show_const ConstZ{} = "Show"
  61         show_const (ConstS c) = show_const c
  62
  63 instance Proj_ConC cs (Proxy Show)
  64 data instance TokenT meta (ts::[*]) (Proxy Show)
  65  = Token_Term_Show_showsPrec (EToken meta ts) (EToken meta ts)
  66  | Token_Term_Show_show      (EToken meta ts)
  67  | Token_Term_Show_showList  (EToken meta ts)
  68 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Show))
  69 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Show))
  70 instance -- CompileI
  71  ( Inj_Const (Consts_of_Ifaces is) (->)
  72  , Inj_Const (Consts_of_Ifaces is) Char
  73  , Inj_Const (Consts_of_Ifaces is) Int
  74  , Inj_Const (Consts_of_Ifaces is) Show
  75  , Inj_Const (Consts_of_Ifaces is) []
  76  , Proj_Con (Consts_of_Ifaces is)
  77  , Compile is
  78  ) => CompileI is (Proxy Show) where
  79         compileI tok ctx k =
  80                 case tok of
  81                  Token_Term_Show_showsPrec tok_p tok_a ->
  82                         compileO tok_p ctx $ \ty_p (TermO p) ->
  83                         compileO tok_a ctx $ \ty_a (TermO a) ->
  84                         check_type (At Nothing (ty @Int)) (At (Just tok_p) ty_p) $ \Refl ->
  85                         check_con (At (Just tok_a) (ty @Show :$ ty_a)) $ \Con ->
  86                         k tyShowS $ TermO $
  87                          \c -> showsPrec (p c) (a c)
  88                  Token_Term_Show_show      tok_a ->
  89                         compileO tok_a ctx $ \ty_a (TermO a) ->
  90                         check_con (At (Just tok_a) (ty @Show :$ ty_a)) $ \Con ->
  91                         k tyString $ TermO $
  92                          \c -> show (a c)
  93                  Token_Term_Show_showList tok_as ->
  94                         compileO tok_as ctx $ \ty_as (TermO as) ->
  95                         check_type1 (ty @[]) (At (Just tok_as) ty_as) $ \Refl ty_a ->
  96                         check_con (At (Just tok_as) (ty @Show :$ ty_a)) $ \Con ->
  97                         k tyShowS $ TermO $
  98                          \c -> showList (as c)
  99                 where
 100                 tyString = ty @[] :$ ty @Char
 101                 tyShowS  = tyString ~> tyString