]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Expr/IO.hs
factorizing Type1_From ast Type0
[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 (Sym_IO r1, Sym_IO r2) => Sym_IO (Repr_Dup r1 r2) where
42 io_hClose = repr_dup1 sym_IO io_hClose
43 io_openFile = repr_dup2 sym_IO io_openFile
44
45 sym_IO :: Proxy Sym_IO
46 sym_IO = Proxy
47
48 -- * Type 'Expr_IO'
49 -- | Expression.
50 data Expr_IO (root:: *)
51 type instance Root_of_Expr (Expr_IO root) = root
52 type instance Type_of_Expr (Expr_IO root) = Type_IO
53 type instance Sym_of_Expr (Expr_IO root) repr = Sym_IO repr
54 type instance Error_of_Expr ast (Expr_IO root) = No_Error_Expr
55
56 -- | Parsing utility to check that the given type is a 'Type_IO'
57 -- or raise 'Error_Expr_Type_mismatch'.
58 check_type_io
59 :: forall ast ex root ty h ret.
60 ( root ~ Root_of_Expr ex
61 , ty ~ Type_Root_of_Expr ex
62 , Type0_Lift Type_IO (Type_of_Expr root)
63 , Type0_Unlift Type_IO (Type_of_Expr root)
64 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
65 (Error_of_Expr ast root)
66 )
67 => Proxy ex -> ast -> ty h
68 -> (Type_IO ty h -> Either (Error_of_Expr ast root) ret)
69 -> Either (Error_of_Expr ast root) ret
70 check_type_io ex ast ty k =
71 case type0_unlift $ unType_Root ty of
72 Just ty_l -> k ty_l
73 Nothing -> Left $
74 error_expr ex $
75 Error_Expr_Type_mismatch ast
76 (Exists_Type0 (type_io $ type_var0 SZero
77 :: ty (IO Var0)))
78 (Exists_Type0 ty)
79
80 -- | Parse 'io_hClose'.
81 io_hclose_from
82 :: forall root ty ast hs ret.
83 ( ty ~ Type_Root_of_Expr (Expr_IO root)
84 , Type0_Eq ty
85 , Expr_From ast root
86 , Type0_Lift Type_Unit (Type_of_Expr root)
87 , Type0_Lift Type_IO_Handle (Type_of_Expr root)
88 , Type0_Lift Type_IO (Type_of_Expr root)
89 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
90 (Error_of_Expr ast root)
91 , Root_of_Expr root ~ root
92 ) => ast
93 -> ExprFrom ast (Expr_IO root) hs ret
94 io_hclose_from ast_h ex ast ctx k =
95 expr_from (Proxy::Proxy root) ast_h ctx $
96 \(ty_h::ty h_h) (Forall_Repr_with_Context h) ->
97 check_type0_eq ex ast type_io_handle ty_h $ \Refl ->
98 k (type_io type_unit) $ Forall_Repr_with_Context $
99 \c -> io_hClose (h c)
100
101 -- | Parse 'io_openFile'.
102 io_openfile_from
103 :: forall root ty ast hs ret.
104 ( ty ~ Type_Root_of_Expr (Expr_IO root)
105 , Type0_Eq ty
106 , Expr_From ast root
107 , Type0_Lift Type_IO_FilePath (Type_of_Expr root)
108 , Type0_Lift Type_IO_Handle (Type_of_Expr root)
109 , Type0_Lift Type_IO_Mode (Type_of_Expr root)
110 , Type0_Lift Type_IO (Type_of_Expr root)
111 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
112 (Error_of_Expr ast root)
113 , Root_of_Expr root ~ root
114 ) => ast -> ast
115 -> ExprFrom ast (Expr_IO root) hs ret
116 io_openfile_from ast_file ast_mode ex ast ctx k =
117 expr_from (Proxy::Proxy root) ast_file ctx $
118 \(ty_file::ty h_file) (Forall_Repr_with_Context file) ->
119 expr_from (Proxy::Proxy root) ast_mode ctx $
120 \(ty_mode::ty h_mode) (Forall_Repr_with_Context mode) ->
121 check_type0_eq ex ast type_io_filepath ty_file $ \Refl ->
122 check_type0_eq ex ast type_io_mode ty_mode $ \Refl ->
123 k (type_io type_io_handle) $ Forall_Repr_with_Context $
124 \c -> io_openFile (file c) (mode c)