]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Compiling/IO.hs
Use GHC-8.0.1's TypeInType to handle kinds better, and migrate Compiling.
[haskell/symantic.git] / Language / Symantic / Compiling / IO.hs
1 {-# LANGUAGE DataKinds #-}
2 {-# LANGUAGE DefaultSignatures #-}
3 {-# LANGUAGE FlexibleContexts #-}
4 {-# LANGUAGE FlexibleInstances #-}
5 {-# LANGUAGE MultiParamTypeClasses #-}
6 {-# LANGUAGE OverloadedStrings #-}
7 {-# LANGUAGE Rank2Types #-}
8 {-# LANGUAGE ScopedTypeVariables #-}
9 {-# LANGUAGE TypeFamilies #-}
10 {-# LANGUAGE TypeOperators #-}
11 {-# LANGUAGE UndecidableInstances #-}
12 {-# OPTIONS_GHC -fno-warn-orphans #-}
13 {-# OPTIONS_GHC -fconstraint-solver-iterations=5 #-}
14 -- | Symantic for 'IO'.
15 module Language.Symantic.Compiling.IO where
16
17 import Control.Monad (liftM, liftM2)
18 import Data.Proxy
19 import Data.String (IsString)
20 import Data.Text (Text)
21 import Data.Type.Equality ((:~:)(Refl))
22 import qualified System.IO as IO
23
24 import Language.Symantic.Typing
25 import Language.Symantic.Compiling.Term
26 import Language.Symantic.Interpreting
27 import Language.Symantic.Transforming.Trans
28
29 -- * Class 'Sym_IO'
30 class Sym_IO term where
31 io_hClose :: term IO.Handle -> term (IO ())
32 io_openFile :: term IO.FilePath -> term IO.IOMode -> term (IO IO.Handle)
33
34 default io_hClose :: Trans t term => t term IO.Handle -> t term (IO ())
35 default io_openFile :: Trans t term => t term IO.FilePath -> t term IO.IOMode -> t term (IO IO.Handle)
36
37 io_hClose = trans_map1 io_hClose
38 io_openFile = trans_map2 io_openFile
39
40 type instance Sym_of_Iface (Proxy IO) = Sym_IO
41 type instance Consts_of_Iface (Proxy IO) = Proxy IO ': Consts_imported_by IO
42 type instance Consts_imported_by IO =
43 [ Proxy IO.Handle
44 , Proxy IO.IOMode
45 , Proxy IO.FilePath
46 , Proxy Applicative
47 , Proxy Functor
48 , Proxy Monad
49 ]
50 type instance Consts_imported_by IO.Handle =
51 '[ Proxy Eq
52 ]
53 type instance Consts_imported_by IO.IOMode =
54 [ Proxy Enum
55 , Proxy Eq
56 , Proxy Ord
57 ]
58
59 instance Sym_IO HostI where
60 io_hClose = liftM IO.hClose
61 io_openFile = liftM2 IO.openFile
62 instance Sym_IO TextI where
63 io_hClose = textI_app1 "IO.hClose"
64 io_openFile = textI_app2 "IO.openFile"
65 instance (Sym_IO r1, Sym_IO r2) => Sym_IO (DupI r1 r2) where
66 io_hClose = dupI1 sym_IO io_hClose
67 io_openFile = dupI2 sym_IO io_openFile
68
69 instance Const_from Text cs => Const_from Text (Proxy IO ': cs) where
70 const_from "IO" k = k (ConstZ kind)
71 const_from s k = const_from s $ k . ConstS
72 instance Const_from Text cs => Const_from Text (Proxy IO.Handle ': cs) where
73 const_from "IO.Handle" k = k (ConstZ kind)
74 const_from s k = const_from s $ k . ConstS
75 instance Const_from Text cs => Const_from Text (Proxy IO.IOMode ': cs) where
76 const_from "IO.IOMode" k = k (ConstZ kind)
77 const_from s k = const_from s $ k . ConstS
78
79 instance Show_Const cs => Show_Const (Proxy IO ': cs) where
80 show_const ConstZ{} = "IO"
81 show_const (ConstS c) = show_const c
82 instance Show_Const cs => Show_Const (Proxy IO.Handle ': cs) where
83 show_const ConstZ{} = "IO.Handle"
84 show_const (ConstS c) = show_const c
85 instance Show_Const cs => Show_Const (Proxy IO.IOMode ': cs) where
86 show_const ConstZ{} = "IO.IOMode"
87 show_const (ConstS c) = show_const c
88
89 instance -- Proj_ConC IO
90 ( Proj_Const cs IO
91 , Proj_Consts cs (Consts_imported_by IO)
92 ) => Proj_ConC cs (Proxy IO) where
93 proj_conC _ (TyConst q :$ TyConst c)
94 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
95 , Just Refl <- proj_const c (Proxy::Proxy IO)
96 = Just $ case () of
97 _ | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
98 | Just Refl <- proj_const q (Proxy::Proxy Functor) -> Just Con
99 | Just Refl <- proj_const q (Proxy::Proxy Monad) -> Just Con
100 _ -> Nothing
101 proj_conC _c _q = Nothing
102 instance -- Proj_ConC IO.Handle
103 ( Proj_Const cs IO.Handle
104 , Proj_Consts cs (Consts_imported_by IO.Handle)
105 ) => Proj_ConC cs (Proxy IO.Handle) where
106 proj_conC _ (TyConst q :$ TyConst c)
107 | Just Refl <- eq_skind (kind_of_const c) SKiType
108 , Just Refl <- proj_const c (Proxy::Proxy IO.Handle)
109 = Just $ case () of
110 _ | Just Refl <- proj_const q (Proxy::Proxy Eq) -> Just Con
111 _ -> Nothing
112 proj_conC _c _q = Nothing
113 instance -- Proj_ConC IO.IOMode
114 ( Proj_Const cs IO.IOMode
115 , Proj_Consts cs (Consts_imported_by IO.IOMode)
116 ) => Proj_ConC cs (Proxy IO.IOMode) where
117 proj_conC _ (TyConst q :$ TyConst c)
118 | Just Refl <- eq_skind (kind_of_const c) SKiType
119 , Just Refl <- proj_const c (Proxy::Proxy IO.IOMode)
120 = Just $ case () of
121 _ | Just Refl <- proj_const q (Proxy::Proxy Enum) -> Just Con
122 | Just Refl <- proj_const q (Proxy::Proxy Eq) -> Just Con
123 | Just Refl <- proj_const q (Proxy::Proxy Ord) -> Just Con
124 _ -> Nothing
125 proj_conC _c _q = Nothing
126 instance -- Term_fromI
127 ( AST ast
128 , Lexem ast ~ LamVarName
129 , Inj_Const (Consts_of_Ifaces is) IO
130 , Inj_Const (Consts_of_Ifaces is) IO.Handle
131 , Inj_Const (Consts_of_Ifaces is) IO.FilePath
132 , Inj_Const (Consts_of_Ifaces is) IO.IOMode
133 , Inj_Const (Consts_of_Ifaces is) (->)
134 , Inj_Const (Consts_of_Ifaces is) ()
135 , Term_from is ast
136 ) => Term_fromI is (Proxy IO) ast where
137 term_fromI ast ctx k =
138 case ast_lexem ast of
139 "IO.hClose" -> io_hClose_from
140 "IO.openFile" -> io_openFile_from
141 _ -> Left $ Error_Term_unsupported
142 where
143 io_hClose_from =
144 -- hClose :: Handle -> IO ()
145 case ast_nodes ast of
146 [] -> Left $ Error_Term_Syntax $
147 Error_Syntax_more_arguments_needed $ At (Just ast) 1
148 [ast_h] ->
149 term_from ast_h ctx $ \ty_h (TermLC h) ->
150 check_type (At Nothing tyIO_Handle) (At (Just ast_h) ty_h) $ \Refl ->
151 k (tyIO :$ tyUnit) $ TermLC $
152 io_hClose . h
153 _ -> Left $ Error_Term_Syntax $
154 Error_Syntax_too_many_arguments $ At (Just ast) 1
155 io_openFile_from =
156 -- openFile :: FilePath -> IOMode -> IO Handle
157 case ast_nodes ast of
158 [] -> Left $ Error_Term_Syntax $
159 Error_Syntax_more_arguments_needed $ At (Just ast) 1
160 [ast_fp] ->
161 term_from ast_fp ctx $ \ty_fp (TermLC fp) ->
162 check_type (At Nothing tyIO_FilePath) (At (Just ast_fp) ty_fp) $ \Refl ->
163 k (tyIO_IOMode ~> tyIO :$ tyIO_Handle) $ TermLC $
164 \c -> lam $ io_openFile (fp c)
165 [ast_fp, ast_m] ->
166 term_from ast_fp ctx $ \ty_fp (TermLC fp) ->
167 term_from ast_m ctx $ \ty_m (TermLC m) ->
168 check_type (At Nothing tyIO_FilePath) (At (Just ast_fp) ty_fp) $ \Refl ->
169 check_type (At Nothing tyIO_IOMode) (At (Just ast_m) ty_m) $ \Refl ->
170 k (tyIO :$ tyIO_Handle) $ TermLC $
171 \c -> io_openFile (fp c) (m c)
172 _ -> Left $ Error_Term_Syntax $
173 Error_Syntax_too_many_arguments $ At (Just ast) 2
174
175 -- | The 'IO' 'Type'
176 tyIO :: Inj_Const cs IO => Type cs IO
177 tyIO = TyConst inj_const
178
179 -- | The 'IO.Handle' 'Type'
180 tyIO_Handle :: Inj_Const cs IO.Handle => Type cs IO.Handle
181 tyIO_Handle = TyConst inj_const
182
183 -- | The 'IO.IOMode' 'Type'
184 tyIO_IOMode :: Inj_Const cs IO.IOMode => Type cs IO.IOMode
185 tyIO_IOMode = TyConst inj_const
186
187 -- | The 'IO.FilePath' 'Type'
188 tyIO_FilePath :: Inj_Const cs IO.FilePath => Type cs IO.FilePath
189 tyIO_FilePath = TyConst inj_const
190
191 sym_IO :: Proxy Sym_IO
192 sym_IO = Proxy
193
194 syIO :: IsString a => [Syntax a] -> Syntax a
195 syIO = Syntax "IO"