Language/Symantic/Expr/IO.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE FlexibleInstances #-}
   4 {-# LANGUAGE MultiParamTypeClasses #-}
   5 {-# LANGUAGE ScopedTypeVariables #-}
   6 {-# LANGUAGE TypeFamilies #-}
   7 {-# LANGUAGE TypeOperators #-}
   8 {-# OPTIONS_GHC -fno-warn-orphans #-}
   9 -- | Expression for 'IO'.
  10 module Language.Symantic.Expr.IO where
  11
  12 import Data.Proxy (Proxy(..))
  13 import Data.Type.Equality ((:~:)(Refl))
  14 import qualified System.IO as IO
  15
  16 import Language.Symantic.Type
  17 import Language.Symantic.Trans.Common
  18 import Language.Symantic.Expr.Root
  19 import Language.Symantic.Expr.Error
  20 import Language.Symantic.Expr.From
  21 -- import Language.Symantic.Expr.Lambda
  22
  23 -- * Class 'Sym_IO_Lam'
  24 -- | Symantic.
  25 class Sym_IO repr where
  26         io_hClose   :: repr IO.Handle -> repr (IO ())
  27         io_openFile :: repr IO.FilePath -> repr IO.IOMode -> repr (IO IO.Handle)
  28
  29         default io_hClose   :: Trans t repr => t repr IO.Handle -> t repr (IO ())
  30         default io_openFile :: Trans t repr => t repr IO.FilePath -> t repr IO.IOMode -> t repr (IO IO.Handle)
  31         io_hClose   = trans_map1 io_hClose
  32         io_openFile = trans_map2 io_openFile
  33
  34 -- * Type 'Expr_IO'
  35 -- | Expression.
  36 data Expr_IO (lam:: * -> *) (root:: *)
  37 type instance Root_of_Expr      (Expr_IO lam root)      = root
  38 type instance Type_of_Expr      (Expr_IO lam root)      = Type_IO
  39 type instance Sym_of_Expr       (Expr_IO lam root) repr = (Sym_IO repr)
  40 type instance Error_of_Expr ast (Expr_IO lam root)      = No_Error_Expr
  41
  42 -- | Parsing utility to check that the given type is a 'Type_IO'
  43 -- or raise 'Error_Expr_Type_mismatch'.
  44 check_type_io
  45  :: forall ast ex root ty h ret.
  46  ( root ~ Root_of_Expr ex
  47  , ty ~ Type_Root_of_Expr ex
  48  , Lift_Type   Type_IO (Type_of_Expr root)
  49  , Unlift_Type Type_IO (Type_of_Expr root)
  50  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  51                    (Error_of_Expr ast root)
  52  )
  53  => Proxy ex -> ast -> ty h
  54  -> (Type_IO ty h -> Either (Error_of_Expr ast root) ret)
  55  -> Either (Error_of_Expr ast root) ret
  56 check_type_io ex ast ty k =
  57         case unlift_type $ unType_Root ty of
  58          Just ty_l -> k ty_l
  59          Nothing -> Left $
  60                 error_expr ex $
  61                 Error_Expr_Type_mismatch ast
  62                  (Exists_Type (type_io $ type_var0 SZero
  63                  :: ty (IO Var0)))
  64                  (Exists_Type ty)
  65
  66 -- | Parse 'io_hClose'.
  67 io_hclose_from
  68  :: forall root lam ty ast hs ret.
  69  ( ty ~ Type_Root_of_Expr (Expr_IO lam root)
  70  , Eq_Type ty
  71  , Expr_from ast root
  72  , Lift_Type   Type_Unit (Type_of_Expr root)
  73  , Lift_Type   Type_IO_Handle (Type_of_Expr root)
  74  , Lift_Type   Type_IO (Type_of_Expr root)
  75  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  76                    (Error_of_Expr ast root)
  77  , Root_of_Expr root ~ root
  78  ) => ast
  79  -> Expr_From ast (Expr_IO lam root) hs ret
  80 io_hclose_from ast_h ex ast ctx k =
  81         expr_from (Proxy::Proxy root) ast_h ctx $
  82          \(ty_h::ty h_h) (Forall_Repr_with_Context h) ->
  83         check_eq_type ex ast type_io_handle ty_h $ \Refl ->
  84         k (type_io type_unit) $ Forall_Repr_with_Context $
  85                 \c -> io_hClose (h c)
  86
  87 -- | Parse 'io_openFile'.
  88 io_openfile_from
  89  :: forall root lam ty ast hs ret.
  90  ( ty ~ Type_Root_of_Expr (Expr_IO lam root)
  91  , Eq_Type ty
  92  , Expr_from ast root
  93  , Lift_Type   Type_IO_FilePath (Type_of_Expr root)
  94  , Lift_Type   Type_IO_Handle   (Type_of_Expr root)
  95  , Lift_Type   Type_IO_Mode     (Type_of_Expr root)
  96  , Lift_Type   Type_IO          (Type_of_Expr root)
  97  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  98                    (Error_of_Expr ast root)
  99  , Root_of_Expr root ~ root
 100  ) => ast -> ast
 101  -> Expr_From ast (Expr_IO lam root) hs ret
 102 io_openfile_from ast_file ast_mode ex ast ctx k =
 103         expr_from (Proxy::Proxy root) ast_file ctx $
 104          \(ty_file::ty h_file) (Forall_Repr_with_Context file) ->
 105         expr_from (Proxy::Proxy root) ast_mode ctx $
 106          \(ty_mode::ty h_mode) (Forall_Repr_with_Context mode) ->
 107         check_eq_type ex ast type_io_filepath ty_file $ \Refl ->
 108         check_eq_type ex ast type_io_mode ty_mode $ \Refl ->
 109         k (type_io type_io_handle) $ Forall_Repr_with_Context $
 110                 \c -> io_openFile (file c) (mode c)