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.Parsing.Grammar
  15 import Language.Symantic.Typing
  16 import Language.Symantic.Compiling
  17 import Language.Symantic.Interpreting
  18 import Language.Symantic.Transforming.Trans
  19 import Language.Symantic.Lib.Lambda
  20
  21 -- * Class 'Sym_Show'
  22 class Sym_Show term where
  23         showsPrec :: Show a => term Int -> term a -> term ShowS
  24         show      :: Show a => term a -> term String
  25         showList  :: Show a => term [a] -> term ShowS
  26
  27         default showsPrec :: (Trans t term, Show a) => t term Int -> t term a -> t term ShowS
  28         default show      :: (Trans t term, Show a) => t term a -> t term String
  29         default showList  :: (Trans t term, Show a) => t term [a] -> t term ShowS
  30
  31         showsPrec = trans_map2 showsPrec
  32         show      = trans_map1 show
  33         showList  = trans_map1 showList
  34
  35 type instance Sym_of_Iface (Proxy Show) = Sym_Show
  36 type instance Consts_of_Iface (Proxy Show) = Proxy Show ': Consts_imported_by Show
  37 type instance Consts_imported_by Show =
  38  [ Proxy []
  39  , Proxy (->)
  40  , Proxy Char
  41  , Proxy Int
  42  ]
  43
  44 instance Sym_Show HostI where
  45         showsPrec = liftM2 Show.showsPrec
  46         show      = liftM  Show.show
  47         showList  = liftM  Show.showList
  48 instance Sym_Show TextI where
  49         showsPrec = textI2 "showsPrec"
  50         show      = textI1 "show"
  51         showList  = textI1 "showList"
  52 instance (Sym_Show r1, Sym_Show r2) => Sym_Show (DupI r1 r2) where
  53         showsPrec = dupI2 (Proxy @Sym_Show) showsPrec
  54         show      = dupI1 (Proxy @Sym_Show) show
  55         showList  = dupI1 (Proxy @Sym_Show) showList
  56
  57 instance
  58  ( Read_TypeNameR Type_Name cs rs
  59  , Inj_Const cs Show
  60  ) => Read_TypeNameR Type_Name cs (Proxy Show ': rs) where
  61         read_typenameR _cs (Type_Name "Show") k = k (ty @Show)
  62         read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
  63 instance Show_Const cs => Show_Const (Proxy Show ': cs) where
  64         show_const ConstZ{} = "Show"
  65         show_const (ConstS c) = show_const c
  66
  67 instance Proj_ConC cs (Proxy Show)
  68 data instance TokenT meta (ts::[*]) (Proxy Show)
  69  = Token_Term_Show_showsPrec (EToken meta ts) (EToken meta ts)
  70  | Token_Term_Show_show      (EToken meta ts)
  71  | Token_Term_Show_showList  (EToken meta ts)
  72 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Show))
  73 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Show))
  74 instance -- CompileI
  75  ( Inj_Const (Consts_of_Ifaces is) (->)
  76  , Inj_Const (Consts_of_Ifaces is) Char
  77  , Inj_Const (Consts_of_Ifaces is) Int
  78  , Inj_Const (Consts_of_Ifaces is) Show
  79  , Inj_Const (Consts_of_Ifaces is) []
  80  , Proj_Con (Consts_of_Ifaces is)
  81  , Compile is
  82  ) => CompileI is (Proxy Show) where
  83         compileI tok ctx k =
  84                 case tok of
  85                  Token_Term_Show_showsPrec tok_p tok_a ->
  86                         compileO tok_p ctx $ \ty_p (TermO p) ->
  87                         compileO tok_a ctx $ \ty_a (TermO a) ->
  88                         check_type (At Nothing (ty @Int)) (At (Just tok_p) ty_p) $ \Refl ->
  89                         check_con (At (Just tok_a) (ty @Show :$ ty_a)) $ \Con ->
  90                         k tyShowS $ TermO $
  91                          \c -> showsPrec (p c) (a c)
  92                  Token_Term_Show_show      tok_a ->
  93                         compileO tok_a ctx $ \ty_a (TermO a) ->
  94                         check_con (At (Just tok_a) (ty @Show :$ ty_a)) $ \Con ->
  95                         k tyString $ TermO $
  96                          \c -> show (a c)
  97                  Token_Term_Show_showList tok_as ->
  98                         compileO tok_as ctx $ \ty_as (TermO as) ->
  99                         check_type1 (ty @[]) (At (Just tok_as) ty_as) $ \Refl ty_a ->
 100                         check_con (At (Just tok_as) (ty @Show :$ ty_a)) $ \Con ->
 101                         k tyShowS $ TermO $
 102                          \c -> showList (as c)
 103                 where
 104                 tyString = ty @[] :$ ty @Char
 105                 tyShowS  = tyString ~> tyString
 106 instance -- TokenizeT
 107  Inj_Token meta ts Show =>
 108  TokenizeT meta ts (Proxy Show) where
 109         tokenizeT _t = mempty
 110          { tokenizers_infix = tokenizeTMod []
 111                  [ tokenize2 "showsPrec" infixN5 Token_Term_Show_showsPrec
 112                  , tokenize1 "show"      infixN5 Token_Term_Show_show
 113                  , tokenize1 "showList"  infixN5 Token_Term_Show_showList
 114                  ]
 115          }
 116 instance Gram_Term_AtomsT meta ts (Proxy Show) g