symantic-lib/Language/Symantic/Lib/Show.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Show'.
   4 module Language.Symantic.Lib.Show where
   5
   6 import Control.Monad
   7 import Data.Proxy (Proxy(..))
   8 import Data.Type.Equality ((:~:)(Refl))
   9 import Prelude hiding (Show(..))
  10 import Text.Show (Show)
  11 import qualified Text.Show as Show
  12
  13 import Language.Symantic.Parsing
  14 import Language.Symantic.Typing
  15 import Language.Symantic.Compiling
  16 import Language.Symantic.Interpreting
  17 import Language.Symantic.Transforming
  18 import Language.Symantic.Lib.Lambda
  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 TyConsts_of_Iface (Proxy Show) = Proxy Show ': TyConsts_imported_by (Proxy Show)
  36 type instance TyConsts_imported_by (Proxy Show) =
  37  [ Proxy []
  38  , Proxy Char
  39  , Proxy Int
  40  ]
  41
  42 instance Sym_Show HostI where
  43         showsPrec = liftM2 Show.showsPrec
  44         show      = liftM  Show.show
  45         showList  = liftM  Show.showList
  46 instance Sym_Show TextI where
  47         showsPrec = textI2 "showsPrec"
  48         show      = textI1 "show"
  49         showList  = textI1 "showList"
  50 instance (Sym_Show r1, Sym_Show r2) => Sym_Show (DupI r1 r2) where
  51         showsPrec = dupI2 @Sym_Show showsPrec
  52         show      = dupI1 @Sym_Show show
  53         showList  = dupI1 @Sym_Show showList
  54
  55 instance
  56  ( Read_TyNameR TyName cs rs
  57  , Inj_TyConst cs Show
  58  ) => Read_TyNameR TyName cs (Proxy Show ': rs) where
  59         read_TyNameR _cs (TyName "Show") k = k (ty @Show)
  60         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
  61 instance Show_TyConst cs => Show_TyConst (Proxy Show ': cs) where
  62         show_TyConst TyConstZ{} = "Show"
  63         show_TyConst (TyConstS c) = show_TyConst c
  64
  65 instance Proj_TyConC cs (Proxy Show)
  66 data instance TokenT meta (ts::[*]) (Proxy Show)
  67  = Token_Term_Show_showsPrec (EToken meta ts) (EToken meta ts)
  68  | Token_Term_Show_show      (EToken meta ts)
  69  | Token_Term_Show_showList  (EToken meta ts)
  70 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Show))
  71 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Show))
  72
  73 instance -- CompileI
  74  ( Inj_TyConst cs Show
  75  , Inj_TyConst cs (->)
  76  , Inj_TyConsts cs (TyConsts_imported_by (Proxy Show))
  77  , Proj_TyCon cs
  78  , Compile cs is
  79  ) => CompileI cs is (Proxy Show) where
  80         compileI tok ctx k =
  81                 case tok of
  82                  Token_Term_Show_showsPrec tok_p tok_a ->
  83                         compile tok_p ctx $ \ty_p (Term p) ->
  84                         compile tok_a ctx $ \ty_a (Term a) ->
  85                         check_TyEq (At Nothing (ty @Int)) (At (Just tok_p) ty_p) $ \Refl ->
  86                         check_TyCon (At (Just tok_a) (ty @Show :$ ty_a)) $ \TyCon ->
  87                         k tyShowS $ Term $
  88                          \c -> showsPrec (p c) (a c)
  89                  Token_Term_Show_show      tok_a ->
  90                         compile tok_a ctx $ \ty_a (Term a) ->
  91                         check_TyCon (At (Just tok_a) (ty @Show :$ ty_a)) $ \TyCon ->
  92                         k tyString $ Term $
  93                          \c -> show (a c)
  94                  Token_Term_Show_showList tok_as ->
  95                         compile tok_as ctx $ \ty_as (Term as) ->
  96                         check_TyEq1 (ty @[]) (At (Just tok_as) ty_as) $ \Refl ty_a ->
  97                         check_TyCon (At (Just tok_as) (ty @Show :$ ty_a)) $ \TyCon ->
  98                         k tyShowS $ Term $
  99                          \c -> showList (as c)
 100                 where
 101                 tyString = ty @[] :$ ty @Char
 102                 tyShowS  = tyString ~> tyString
 103 instance -- TokenizeT
 104  Inj_Token meta ts Show =>
 105  TokenizeT meta ts (Proxy Show) where
 106         tokenizeT _t = mempty
 107          { tokenizers_infix = tokenizeTMod []
 108                  [ tokenize2 "showsPrec" infixN5 Token_Term_Show_showsPrec
 109                  , tokenize1 "show"      infixN5 Token_Term_Show_show
 110                  , tokenize1 "showList"  infixN5 Token_Term_Show_showList
 111                  ]
 112          }
 113 instance Gram_Term_AtomsT meta ts (Proxy Show) g