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  , Lift_Type   Type_IO (Type_of_Expr root)
  65  , Unlift_Type Type_IO (Type_of_Expr root)
  66  , Lift_Error_Expr (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 unlift_type $ 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_Type (type_io $ type_var0 SZero
  79                  :: ty (IO Var0)))
  80                  (Exists_Type 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  , Eq_Type ty
  87  , Expr_from ast root
  88  , Lift_Type   Type_Unit (Type_of_Expr root)
  89  , Lift_Type   Type_IO_Handle (Type_of_Expr root)
  90  , Lift_Type   Type_IO (Type_of_Expr root)
  91  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  92                    (Error_of_Expr ast root)
  93  , Root_of_Expr root ~ root
  94  ) => ast
  95  -> Expr_From 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_eq_type 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  , Eq_Type ty
 108  , Expr_from ast root
 109  , Lift_Type   Type_IO_FilePath (Type_of_Expr root)
 110  , Lift_Type   Type_IO_Handle   (Type_of_Expr root)
 111  , Lift_Type   Type_IO_Mode     (Type_of_Expr root)
 112  , Lift_Type   Type_IO          (Type_of_Expr root)
 113  , Lift_Error_Expr (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  -> Expr_From 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_eq_type ex ast type_io_filepath ty_file $ \Refl ->
 124         check_eq_type 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)