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
14 import Data.Proxy (Proxy(..))
15 import Data.Type.Equality ((:~:)(Refl))
16 import qualified System.IO as IO
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
25 -- * Class 'Sym_IO_Lam'
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)
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 (Sym_IO r1, Sym_IO r2) => Sym_IO (Repr_Dup r1 r2) where
42 io_hClose (h1 `Repr_Dup` h2) =
43 io_hClose h1 `Repr_Dup` io_hClose h2
44 io_openFile (f1 `Repr_Dup` f2) (m1 `Repr_Dup` m2) =
45 io_openFile f1 m1 `Repr_Dup` io_openFile f2 m2
49 data Expr_IO (root:: *)
50 type instance Root_of_Expr (Expr_IO root) = root
51 type instance Type_of_Expr (Expr_IO root) = Type_IO
52 type instance Sym_of_Expr (Expr_IO root) repr = (Sym_IO repr)
53 type instance Error_of_Expr ast (Expr_IO root) = No_Error_Expr
55 -- | Parsing utility to check that the given type is a 'Type_IO'
56 -- or raise 'Error_Expr_Type_mismatch'.
58 :: forall ast ex root ty h ret.
59 ( root ~ Root_of_Expr ex
60 , ty ~ Type_Root_of_Expr ex
61 , Type0_Lift Type_IO (Type_of_Expr root)
62 , Type0_Unlift Type_IO (Type_of_Expr root)
63 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
64 (Error_of_Expr ast root)
66 => Proxy ex -> ast -> ty h
67 -> (Type_IO ty h -> Either (Error_of_Expr ast root) ret)
68 -> Either (Error_of_Expr ast root) ret
69 check_type_io ex ast ty k =
70 case type0_unlift $ unType_Root ty of
74 Error_Expr_Type_mismatch ast
75 (Exists_Type0 (type_io $ type_var0 SZero
79 -- | Parse 'io_hClose'.
81 :: forall root ty ast hs ret.
82 ( ty ~ Type_Root_of_Expr (Expr_IO root)
85 , Type0_Lift Type_Unit (Type_of_Expr root)
86 , Type0_Lift Type_IO_Handle (Type_of_Expr root)
87 , Type0_Lift Type_IO (Type_of_Expr root)
88 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
89 (Error_of_Expr ast root)
90 , Root_of_Expr root ~ root
92 -> ExprFrom ast (Expr_IO root) hs ret
93 io_hclose_from ast_h ex ast ctx k =
94 expr_from (Proxy::Proxy root) ast_h ctx $
95 \(ty_h::ty h_h) (Forall_Repr_with_Context h) ->
96 check_type0_eq ex ast type_io_handle ty_h $ \Refl ->
97 k (type_io type_unit) $ Forall_Repr_with_Context $
100 -- | Parse 'io_openFile'.
102 :: forall root ty ast hs ret.
103 ( ty ~ Type_Root_of_Expr (Expr_IO root)
106 , Type0_Lift Type_IO_FilePath (Type_of_Expr root)
107 , Type0_Lift Type_IO_Handle (Type_of_Expr root)
108 , Type0_Lift Type_IO_Mode (Type_of_Expr root)
109 , Type0_Lift Type_IO (Type_of_Expr root)
110 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
111 (Error_of_Expr ast root)
112 , Root_of_Expr root ~ root
114 -> ExprFrom ast (Expr_IO root) hs ret
115 io_openfile_from ast_file ast_mode ex ast ctx k =
116 expr_from (Proxy::Proxy root) ast_file ctx $
117 \(ty_file::ty h_file) (Forall_Repr_with_Context file) ->
118 expr_from (Proxy::Proxy root) ast_mode ctx $
119 \(ty_mode::ty h_mode) (Forall_Repr_with_Context mode) ->
120 check_type0_eq ex ast type_io_filepath ty_file $ \Refl ->
121 check_type0_eq ex ast type_io_mode ty_mode $ \Refl ->
122 k (type_io type_io_handle) $ Forall_Repr_with_Context $
123 \c -> io_openFile (file c) (mode c)