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 (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
  46
  47 -- * Type 'Expr_IO'
  48 -- | Expression.
  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
  54
  55 -- | Parsing utility to check that the given type is a 'Type_IO'
  56 -- or raise 'Error_Expr_Type_mismatch'.
  57 check_type_io
  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)
  65  )
  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
  71          Just ty_l -> k ty_l
  72          Nothing -> Left $
  73                 error_expr ex $
  74                 Error_Expr_Type_mismatch ast
  75                  (Exists_Type0 (type_io $ type_var0 SZero
  76                  :: ty (IO Var0)))
  77                  (Exists_Type0 ty)
  78
  79 -- | Parse 'io_hClose'.
  80 io_hclose_from
  81  :: forall root ty ast hs ret.
  82  ( ty ~ Type_Root_of_Expr (Expr_IO root)
  83  , Type0_Eq ty
  84  , Expr_From ast 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
  91  ) => ast
  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 $
  98                 \c -> io_hClose (h c)
  99
 100 -- | Parse 'io_openFile'.
 101 io_openfile_from
 102  :: forall root ty ast hs ret.
 103  ( ty ~ Type_Root_of_Expr (Expr_IO root)
 104  , Type0_Eq ty
 105  , Expr_From ast 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
 113  ) => ast -> ast
 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)