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)