]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/IO.hs
Fix comment typo.
[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / IO.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 {-# OPTIONS_GHC -fconstraint-solver-iterations=5 #-}
4 -- | Symantic for 'IO'.
5 module Language.Symantic.Lib.IO where
6
7 import Control.Monad (liftM, liftM2)
8 import Data.Proxy
9 import Data.Type.Equality ((:~:)(Refl))
10 import qualified System.IO as IO
11
12 import Language.Symantic.Parsing
13 import Language.Symantic.Typing
14 import Language.Symantic.Compiling
15 import Language.Symantic.Interpreting
16 import Language.Symantic.Transforming
17 import Language.Symantic.Lib.Lambda
18
19 -- * Class 'Sym_IO'
20 class Sym_IO term where
21 io_hClose :: term IO.Handle -> term (IO ())
22 io_openFile :: term IO.FilePath -> term IO.IOMode -> term (IO IO.Handle)
23
24 default io_hClose :: Trans t term => t term IO.Handle -> t term (IO ())
25 default io_openFile :: Trans t term => t term IO.FilePath -> t term IO.IOMode -> t term (IO IO.Handle)
26
27 io_hClose = trans_map1 io_hClose
28 io_openFile = trans_map2 io_openFile
29
30 type instance Sym_of_Iface (Proxy IO) = Sym_IO
31 type instance TyConsts_of_Iface (Proxy IO) = Proxy IO ': TyConsts_imported_by IO
32 type instance TyConsts_imported_by IO =
33 [ Proxy IO.Handle
34 , Proxy IO.IOMode
35 , Proxy Applicative
36 , Proxy Functor
37 , Proxy Monad
38 ]
39 type instance TyConsts_imported_by IO.Handle =
40 '[ Proxy Eq
41 ]
42 type instance TyConsts_imported_by IO.IOMode =
43 [ Proxy Enum
44 , Proxy Eq
45 , Proxy Ord
46 ]
47
48 instance Sym_IO HostI where
49 io_hClose = liftM IO.hClose
50 io_openFile = liftM2 IO.openFile
51 instance Sym_IO TextI where
52 io_hClose = textI1 "IO.hClose"
53 io_openFile = textI2 "IO.openFile"
54 instance (Sym_IO r1, Sym_IO r2) => Sym_IO (DupI r1 r2) where
55 io_hClose = dupI1 @Sym_IO io_hClose
56 io_openFile = dupI2 @Sym_IO io_openFile
57
58 instance
59 ( Read_TyNameR TyName cs rs
60 , Inj_TyConst cs IO
61 ) => Read_TyNameR TyName cs (Proxy IO ': rs) where
62 read_TyNameR _cs (TyName "IO") k = k (ty @IO)
63 read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
64 instance
65 ( Read_TyNameR TyName cs rs
66 , Inj_TyConst cs IO.Handle
67 ) => Read_TyNameR TyName cs (Proxy IO.Handle ': rs) where
68 read_TyNameR _cs (TyName "IO.Handle") k = k (ty @IO.Handle)
69 read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
70 instance
71 ( Read_TyNameR TyName cs rs
72 , Inj_TyConst cs IO.IOMode
73 ) => Read_TyNameR TyName cs (Proxy IO.IOMode ': rs) where
74 read_TyNameR _cs (TyName "IO.Mode") k = k (ty @IO.IOMode)
75 read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
76
77 instance Show_TyConst cs => Show_TyConst (Proxy IO ': cs) where
78 show_TyConst TyConstZ{} = "IO"
79 show_TyConst (TyConstS c) = show_TyConst c
80 instance Show_TyConst cs => Show_TyConst (Proxy IO.Handle ': cs) where
81 show_TyConst TyConstZ{} = "IO.Handle"
82 show_TyConst (TyConstS c) = show_TyConst c
83 instance Show_TyConst cs => Show_TyConst (Proxy IO.IOMode ': cs) where
84 show_TyConst TyConstZ{} = "IO.IOMode"
85 show_TyConst (TyConstS c) = show_TyConst c
86
87 instance -- Proj_TyConC IO
88 ( Proj_TyConst cs IO
89 , Proj_TyConsts cs (TyConsts_imported_by IO)
90 ) => Proj_TyConC cs (Proxy IO) where
91 proj_TyConC _ (TyConst q :$ TyConst c)
92 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
93 , Just Refl <- proj_TyConst c (Proxy @IO)
94 = case () of
95 _ | Just Refl <- proj_TyConst q (Proxy @Applicative) -> Just TyCon
96 | Just Refl <- proj_TyConst q (Proxy @Functor) -> Just TyCon
97 | Just Refl <- proj_TyConst q (Proxy @Monad) -> Just TyCon
98 _ -> Nothing
99 proj_TyConC _c _q = Nothing
100 instance -- Proj_TyConC IO.Handle
101 ( Proj_TyConst cs IO.Handle
102 , Proj_TyConsts cs (TyConsts_imported_by IO.Handle)
103 ) => Proj_TyConC cs (Proxy IO.Handle) where
104 proj_TyConC _ (TyConst q :$ TyConst c)
105 | Just Refl <- eq_skind (kind_of_TyConst c) SKiType
106 , Just Refl <- proj_TyConst c (Proxy @IO.Handle)
107 = case () of
108 _ | Just Refl <- proj_TyConst q (Proxy @Eq) -> Just TyCon
109 _ -> Nothing
110 proj_TyConC _c _q = Nothing
111 instance -- Proj_TyConC IO.IOMode
112 ( Proj_TyConst cs IO.IOMode
113 , Proj_TyConsts cs (TyConsts_imported_by IO.IOMode)
114 ) => Proj_TyConC cs (Proxy IO.IOMode) where
115 proj_TyConC _ (TyConst q :$ TyConst c)
116 | Just Refl <- eq_skind (kind_of_TyConst c) SKiType
117 , Just Refl <- proj_TyConst c (Proxy @IO.IOMode)
118 = case () of
119 _ | Just Refl <- proj_TyConst q (Proxy @Enum) -> Just TyCon
120 | Just Refl <- proj_TyConst q (Proxy @Eq) -> Just TyCon
121 | Just Refl <- proj_TyConst q (Proxy @Ord) -> Just TyCon
122 _ -> Nothing
123 proj_TyConC _c _q = Nothing
124 data instance TokenT meta (ts::[*]) (Proxy IO)
125 = Token_Term_IO_hClose (EToken meta ts)
126 | Token_Term_IO_openFile (EToken meta ts)
127 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy IO))
128 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy IO))
129 instance -- CompileI
130 ( Inj_TyConst (TyConsts_of_Ifaces is) IO
131 , Inj_TyConst (TyConsts_of_Ifaces is) IO.Handle
132 , Inj_TyConst (TyConsts_of_Ifaces is) []
133 , Inj_TyConst (TyConsts_of_Ifaces is) Char
134 , Inj_TyConst (TyConsts_of_Ifaces is) IO.IOMode
135 , Inj_TyConst (TyConsts_of_Ifaces is) (->)
136 , Inj_TyConst (TyConsts_of_Ifaces is) ()
137 , Compile is
138 ) => CompileI is (Proxy IO) where
139 compileI tok ctx k =
140 case tok of
141 Token_Term_IO_hClose tok_h ->
142 -- hClose :: Handle -> IO ()
143 compileO tok_h ctx $ \ty_h (TermO h) ->
144 check_TyEq
145 (At Nothing (ty @IO.Handle))
146 (At (Just tok_h) ty_h) $ \Refl ->
147 k (ty @IO :$ ty @()) $ TermO $
148 io_hClose . h
149 Token_Term_IO_openFile tok_fp ->
150 -- openFile :: FilePath -> IOMode -> IO Handle
151 compileO tok_fp ctx $ \ty_fp (TermO fp) ->
152 check_TyEq
153 (At Nothing tyFilePath)
154 (At (Just tok_fp) ty_fp) $ \Refl ->
155 k (ty @IO.IOMode ~> ty @IO :$ ty @IO.Handle) $ TermO $
156 \c -> lam $ io_openFile (fp c)
157 where tyFilePath = ty @[] :$ ty @Char
158 instance -- TokenizeT
159 Inj_Token meta ts IO =>
160 TokenizeT meta ts (Proxy IO) where
161 tokenizeT _t = mempty
162 { tokenizers_infix = tokenizeTMod [Mod_Name "IO"]
163 [ tokenize1 "hClose" infixN5 Token_Term_IO_hClose
164 , tokenize1 "openFile" infixN5 Token_Term_IO_openFile
165 ]
166 }
167 instance Gram_Term_AtomsT meta ts (Proxy IO) g