]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Expr/IO.hs
polish names
[haskell/symantic.git] / Language / Symantic / Expr / IO.hs
1 {-# LANGUAGE DefaultSignatures #-}
2 {-# LANGUAGE FlexibleContexts #-}
3 {-# LANGUAGE FlexibleInstances #-}
4 {-# LANGUAGE MultiParamTypeClasses #-}
5 {-# LANGUAGE OverloadedStrings #-}
6 {-# LANGUAGE ScopedTypeVariables #-}
7 {-# LANGUAGE TypeFamilies #-}
8 {-# LANGUAGE TypeOperators #-}
9 {-# OPTIONS_GHC -fno-warn-orphans #-}
10 -- | Expression for 'IO'.
11 module Language.Symantic.Expr.IO where
12
13 import Control.Monad
14 import Data.Proxy (Proxy(..))
15 import Data.Type.Equality ((:~:)(Refl))
16 import qualified System.IO as IO
17
18 import Language.Symantic.Type
19 import Language.Symantic.Repr
20 import Language.Symantic.Expr.Root
21 import Language.Symantic.Expr.Error
22 import Language.Symantic.Expr.From
23 import Language.Symantic.Trans.Common
24
25 -- * Class 'Sym_IO_Lam'
26 -- | Symantic.
27 class Sym_IO repr where
28 io_hClose :: repr IO.Handle -> repr (IO ())
29 io_openFile :: repr IO.FilePath -> repr IO.IOMode -> repr (IO IO.Handle)
30
31 default io_hClose :: Trans t repr => t repr IO.Handle -> t repr (IO ())
32 default io_openFile :: Trans t repr => t repr IO.FilePath -> t repr IO.IOMode -> t repr (IO IO.Handle)
33 io_hClose = trans_map1 io_hClose
34 io_openFile = trans_map2 io_openFile
35 instance Sym_IO Repr_Host where
36 io_hClose = liftM IO.hClose
37 io_openFile = liftM2 IO.openFile
38 instance Sym_IO Repr_Text where
39 io_hClose = repr_text_app1 "io_hClose"
40 io_openFile = repr_text_app2 "io_openFile"
41 instance
42 ( Sym_IO r1
43 , Sym_IO r2
44 ) => Sym_IO (Dup r1 r2) where
45 io_hClose (h1 `Dup` h2) =
46 io_hClose h1 `Dup` io_hClose h2
47 io_openFile (f1 `Dup` f2) (m1 `Dup` m2) =
48 io_openFile f1 m1 `Dup` io_openFile f2 m2
49
50 -- * Type 'Expr_IO'
51 -- | Expression.
52 data Expr_IO (root:: *)
53 type instance Root_of_Expr (Expr_IO root) = root
54 type instance Type_of_Expr (Expr_IO root) = Type_IO
55 type instance Sym_of_Expr (Expr_IO root) repr = (Sym_IO repr)
56 type instance Error_of_Expr ast (Expr_IO root) = No_Error_Expr
57
58 -- | Parsing utility to check that the given type is a 'Type_IO'
59 -- or raise 'Error_Expr_Type_mismatch'.
60 check_type_io
61 :: forall ast ex root ty h ret.
62 ( root ~ Root_of_Expr ex
63 , ty ~ Type_Root_of_Expr ex
64 , Type0_Lift Type_IO (Type_of_Expr root)
65 , Type0_Unlift Type_IO (Type_of_Expr root)
66 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
67 (Error_of_Expr ast root)
68 )
69 => Proxy ex -> ast -> ty h
70 -> (Type_IO ty h -> Either (Error_of_Expr ast root) ret)
71 -> Either (Error_of_Expr ast root) ret
72 check_type_io ex ast ty k =
73 case type0_unlift $ unType_Root ty of
74 Just ty_l -> k ty_l
75 Nothing -> Left $
76 error_expr ex $
77 Error_Expr_Type_mismatch ast
78 (Exists_Type0 (type_io $ type_var0 SZero
79 :: ty (IO Var0)))
80 (Exists_Type0 ty)
81
82 -- | Parse 'io_hClose'.
83 io_hclose_from
84 :: forall root ty ast hs ret.
85 ( ty ~ Type_Root_of_Expr (Expr_IO root)
86 , Type0_Eq ty
87 , Expr_From ast root
88 , Type0_Lift Type_Unit (Type_of_Expr root)
89 , Type0_Lift Type_IO_Handle (Type_of_Expr root)
90 , Type0_Lift Type_IO (Type_of_Expr root)
91 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
92 (Error_of_Expr ast root)
93 , Root_of_Expr root ~ root
94 ) => ast
95 -> ExprFrom ast (Expr_IO root) hs ret
96 io_hclose_from ast_h ex ast ctx k =
97 expr_from (Proxy::Proxy root) ast_h ctx $
98 \(ty_h::ty h_h) (Forall_Repr_with_Context h) ->
99 check_type0_eq ex ast type_io_handle ty_h $ \Refl ->
100 k (type_io type_unit) $ Forall_Repr_with_Context $
101 \c -> io_hClose (h c)
102
103 -- | Parse 'io_openFile'.
104 io_openfile_from
105 :: forall root ty ast hs ret.
106 ( ty ~ Type_Root_of_Expr (Expr_IO root)
107 , Type0_Eq ty
108 , Expr_From ast root
109 , Type0_Lift Type_IO_FilePath (Type_of_Expr root)
110 , Type0_Lift Type_IO_Handle (Type_of_Expr root)
111 , Type0_Lift Type_IO_Mode (Type_of_Expr root)
112 , Type0_Lift Type_IO (Type_of_Expr root)
113 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
114 (Error_of_Expr ast root)
115 , Root_of_Expr root ~ root
116 ) => ast -> ast
117 -> ExprFrom ast (Expr_IO root) hs ret
118 io_openfile_from ast_file ast_mode ex ast ctx k =
119 expr_from (Proxy::Proxy root) ast_file ctx $
120 \(ty_file::ty h_file) (Forall_Repr_with_Context file) ->
121 expr_from (Proxy::Proxy root) ast_mode ctx $
122 \(ty_mode::ty h_mode) (Forall_Repr_with_Context mode) ->
123 check_type0_eq ex ast type_io_filepath ty_file $ \Refl ->
124 check_type0_eq ex ast type_io_mode ty_mode $ \Refl ->
125 k (type_io type_io_handle) $ Forall_Repr_with_Context $
126 \c -> io_openFile (file c) (mode c)