-- | Symantic for 'Show'.
module Language.Symantic.Lib.Show where
-import Control.Monad
-import Data.Proxy (Proxy(..))
-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
-import Language.Symantic.Interpreting
-import Language.Symantic.Transforming
-import Language.Symantic.Lib.Lambda
+import Language.Symantic
+import Language.Symantic.Lib.Char (tyString)
+import Language.Symantic.Lib.Function (a0)
+import Language.Symantic.Lib.Int (tyInt)
+import Language.Symantic.Lib.List (tyList)
-- * Class 'Sym_Show'
+type instance Sym Show = 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
+ default showsPrec :: Sym_Show (UnT term) => Trans term => Show a => term Int -> term a -> term ShowS
+ default show :: Sym_Show (UnT term) => Trans term => Show a => term a -> term String
+ default showList :: Sym_Show (UnT term) => Trans term => Show a => term [a] -> term ShowS
- showsPrec = trans_map2 showsPrec
- show = trans_map1 show
- showList = trans_map1 showList
+ showsPrec = trans2 showsPrec
+ show = trans1 show
+ showList = trans1 showList
-type instance Sym_of_Iface (Proxy Show) = Sym_Show
-type instance TyConsts_of_Iface (Proxy Show) = Proxy Show ': TyConsts_imported_by Show
-type instance TyConsts_imported_by Show =
- [ Proxy []
- , Proxy (->)
- , Proxy Char
- , Proxy Int
- ]
+instance Sym_Show Eval where
+ showsPrec = eval2 Show.showsPrec
+ show = eval1 Show.show
+ showList = eval1 Show.showList
+instance Sym_Show View where
+ showsPrec = view2 "showsPrec"
+ show = view1 "show"
+ showList = view1 "showList"
+instance (Sym_Show r1, Sym_Show r2) => Sym_Show (Dup r1 r2) where
+ showsPrec = dup2 @Sym_Show showsPrec
+ show = dup1 @Sym_Show show
+ showList = dup1 @Sym_Show showList
-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
+-- Transforming
+instance (Sym_Show term, Sym_Lambda term) => Sym_Show (BetaT term)
-instance
- ( Read_TyNameR TyName cs rs
- , Inj_TyConst cs Show
- ) => Read_TyNameR TyName cs (Proxy Show ': rs) where
- read_TyNameR _cs (TyName "Show") k = k (ty @Show)
- read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
-instance Show_TyConst cs => Show_TyConst (Proxy Show ': cs) where
- show_TyConst TyConstZ{} = "Show"
- show_TyConst (TyConstS c) = show_TyConst c
+-- Typing
+instance NameTyOf Show where
+ nameTyOf _c = ["Show"] `Mod` "Show"
+instance FixityOf Show
+instance ClassInstancesFor Show
+instance TypeInstancesFor Show
-instance Proj_TyConC 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_TyConst (TyConsts_of_Ifaces is) (->)
- , Inj_TyConst (TyConsts_of_Ifaces is) Char
- , Inj_TyConst (TyConsts_of_Ifaces is) Int
- , Inj_TyConst (TyConsts_of_Ifaces is) Show
- , Inj_TyConst (TyConsts_of_Ifaces is) []
- , Proj_TyCon (TyConsts_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_TyEq (At Nothing (ty @Int)) (At (Just tok_p) ty_p) $ \Refl ->
- check_TyCon (At (Just tok_a) (ty @Show :$ ty_a)) $ \TyCon ->
- k tyShowS $ TermO $
- \c -> showsPrec (p c) (a c)
- Token_Term_Show_show tok_a ->
- compileO tok_a ctx $ \ty_a (TermO a) ->
- check_TyCon (At (Just tok_a) (ty @Show :$ ty_a)) $ \TyCon ->
- k tyString $ TermO $
- \c -> show (a c)
- Token_Term_Show_showList tok_as ->
- compileO tok_as ctx $ \ty_as (TermO as) ->
- check_TyEq1 (ty @[]) (At (Just tok_as) ty_as) $ \Refl ty_a ->
- check_TyCon (At (Just tok_as) (ty @Show :$ ty_a)) $ \TyCon ->
- k tyShowS $ TermO $
- \c -> showList (as c)
- where
- tyString = ty @[] :$ ty @Char
- tyShowS = tyString ~> tyString
-instance -- TokenizeT
- Inj_Token meta ts Show =>
- TokenizeT meta ts (Proxy Show) where
- tokenizeT _t = mempty
- { tokenizers_infix = tokenizeTMod []
- [ tokenize2 "showsPrec" infixN5 Token_Term_Show_showsPrec
- , tokenize1 "show" infixN5 Token_Term_Show_show
- , tokenize1 "showList" infixN5 Token_Term_Show_showList
- ]
- }
-instance Gram_Term_AtomsT meta ts (Proxy Show) g
+-- Compiling
+instance Gram_Term_AtomsFor src ss g Show
+instance (Source src, SymInj ss Show) => ModuleFor src ss Show where
+ moduleFor = ["Show"] `moduleWhere`
+ [ "showsPrec" := teShow_showsPrec
+ , "show" := teShow_show
+ , "showList" := teShow_showList
+ ]
+
+-- ** 'Type's
+tyShow :: Source src => Type src vs a -> Type src vs (Show a)
+tyShow a = tyConstLen @(K Show) @Show (lenVars a) `tyApp` a
+
+tyShowS :: Source src => LenInj vs => Type src vs ShowS
+tyShowS = tyString ~> tyString
+
+-- ** 'Term's
+teShow_showsPrec :: TermDef Show '[Proxy a] (Show a #> (Int -> a -> ShowS))
+teShow_showsPrec = Term (tyShow a0) (tyInt ~> a0 ~> tyShowS) $ teSym @Show $ lam2 showsPrec
+
+teShow_show :: TermDef Show '[Proxy a] (Show a #> (a -> String))
+teShow_show = Term (tyShow a0) (a0 ~> tyString) $ teSym @Show $ lam1 show
+
+teShow_showList :: TermDef Show '[Proxy a] (Show a #> ([a] -> ShowS))
+teShow_showList = Term (tyShow a0) (tyList a0 ~> tyShowS) $ teSym @Show $ lam1 showList
sourcephile / git / haskell / symantic.git / blobdiff