Language/Symantic/Compiling/IO.hs

   1 {-# LANGUAGE DataKinds #-}
   2 {-# LANGUAGE DefaultSignatures #-}
   3 {-# LANGUAGE FlexibleContexts #-}
   4 {-# LANGUAGE FlexibleInstances #-}
   5 {-# LANGUAGE MultiParamTypeClasses #-}
   6 {-# LANGUAGE OverloadedStrings #-}
   7 {-# LANGUAGE Rank2Types #-}
   8 {-# LANGUAGE ScopedTypeVariables #-}
   9 {-# LANGUAGE TypeFamilies #-}
  10 {-# LANGUAGE TypeOperators #-}
  11 {-# LANGUAGE UndecidableInstances #-}
  12 {-# OPTIONS_GHC -fno-warn-orphans #-}
  13 {-# OPTIONS_GHC -fconstraint-solver-iterations=5 #-}
  14 -- | Symantic for 'IO'.
  15 module Language.Symantic.Compiling.IO where
  16
  17 import Control.Monad (liftM, liftM2)
  18 import Data.Proxy
  19 import Data.String (IsString)
  20 import Data.Text (Text)
  21 import Data.Type.Equality ((:~:)(Refl))
  22 import qualified System.IO as IO
  23
  24 import Language.Symantic.Typing
  25 import Language.Symantic.Compiling.Term
  26 import Language.Symantic.Interpreting
  27 import Language.Symantic.Transforming.Trans
  28
  29 -- * Class 'Sym_IO'
  30 class Sym_IO term where
  31         io_hClose   :: term IO.Handle -> term (IO ())
  32         io_openFile :: term IO.FilePath -> term IO.IOMode -> term (IO IO.Handle)
  33
  34         default io_hClose   :: Trans t term => t term IO.Handle -> t term (IO ())
  35         default io_openFile :: Trans t term => t term IO.FilePath -> t term IO.IOMode -> t term (IO IO.Handle)
  36
  37         io_hClose   = trans_map1 io_hClose
  38         io_openFile = trans_map2 io_openFile
  39
  40 type instance Sym_of_Iface (Proxy IO) = Sym_IO
  41 type instance Consts_of_Iface (Proxy IO) = Proxy IO ': Consts_imported_by IO
  42 type instance Consts_imported_by IO =
  43  [ Proxy IO.Handle
  44  , Proxy IO.IOMode
  45  , Proxy IO.FilePath
  46  , Proxy Applicative
  47  , Proxy Functor
  48  , Proxy Monad
  49  ]
  50 type instance Consts_imported_by IO.Handle =
  51  '[ Proxy Eq
  52  ]
  53 type instance Consts_imported_by IO.IOMode =
  54  [ Proxy Enum
  55  , Proxy Eq
  56  , Proxy Ord
  57  ]
  58
  59 instance Sym_IO HostI where
  60         io_hClose   = liftM IO.hClose
  61         io_openFile = liftM2 IO.openFile
  62 instance Sym_IO TextI where
  63         io_hClose   = textI_app1 "IO.hClose"
  64         io_openFile = textI_app2 "IO.openFile"
  65 instance (Sym_IO r1, Sym_IO r2) => Sym_IO (DupI r1 r2) where
  66         io_hClose   = dupI1 sym_IO io_hClose
  67         io_openFile = dupI2 sym_IO io_openFile
  68
  69 instance Const_from Text cs => Const_from Text (Proxy IO ': cs) where
  70         const_from "IO" k = k (ConstZ kind)
  71         const_from s k = const_from s $ k . ConstS
  72 instance Const_from Text cs => Const_from Text (Proxy IO.Handle ': cs) where
  73         const_from "IO.Handle" k = k (ConstZ kind)
  74         const_from s k = const_from s $ k . ConstS
  75 instance Const_from Text cs => Const_from Text (Proxy IO.IOMode ': cs) where
  76         const_from "IO.IOMode" k = k (ConstZ kind)
  77         const_from s k = const_from s $ k . ConstS
  78
  79 instance Show_Const cs => Show_Const (Proxy IO ': cs) where
  80         show_const ConstZ{} = "IO"
  81         show_const (ConstS c) = show_const c
  82 instance Show_Const cs => Show_Const (Proxy IO.Handle ': cs) where
  83         show_const ConstZ{} = "IO.Handle"
  84         show_const (ConstS c) = show_const c
  85 instance Show_Const cs => Show_Const (Proxy IO.IOMode ': cs) where
  86         show_const ConstZ{} = "IO.IOMode"
  87         show_const (ConstS c) = show_const c
  88
  89 instance -- Proj_ConC IO
  90  ( Proj_Const cs IO
  91  , Proj_Consts cs (Consts_imported_by IO)
  92  ) => Proj_ConC cs (Proxy IO) where
  93         proj_conC _ (TyConst q :$ TyConst c)
  94          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
  95          , Just Refl <- proj_const c (Proxy::Proxy IO)
  96          = Just $ case () of
  97                  _ | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
  98                    | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
  99                    | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
 100                  _ -> Nothing
 101         proj_conC _c _q = Nothing
 102 instance -- Proj_ConC IO.Handle
 103  ( Proj_Const cs IO.Handle
 104  , Proj_Consts cs (Consts_imported_by IO.Handle)
 105  ) => Proj_ConC cs (Proxy IO.Handle) where
 106         proj_conC _ (TyConst q :$ TyConst c)
 107          | Just Refl <- eq_skind (kind_of_const c) SKiType
 108          , Just Refl <- proj_const c (Proxy::Proxy IO.Handle)
 109          = Just $ case () of
 110                  _ | Just Refl <- proj_const q (Proxy::Proxy Eq) -> Just Con
 111                  _ -> Nothing
 112         proj_conC _c _q = Nothing
 113 instance -- Proj_ConC IO.IOMode
 114  ( Proj_Const cs IO.IOMode
 115  , Proj_Consts cs (Consts_imported_by IO.IOMode)
 116  ) => Proj_ConC cs (Proxy IO.IOMode) where
 117         proj_conC _ (TyConst q :$ TyConst c)
 118          | Just Refl <- eq_skind (kind_of_const c) SKiType
 119          , Just Refl <- proj_const c (Proxy::Proxy IO.IOMode)
 120          = Just $ case () of
 121                  _ | Just Refl <- proj_const q (Proxy::Proxy Enum) -> Just Con
 122                    | Just Refl <- proj_const q (Proxy::Proxy Eq)   -> Just Con
 123                    | Just Refl <- proj_const q (Proxy::Proxy Ord)  -> Just Con
 124                  _ -> Nothing
 125         proj_conC _c _q = Nothing
 126 instance -- Term_fromI
 127  ( AST ast
 128  , Lexem ast ~ LamVarName
 129  , Inj_Const (Consts_of_Ifaces is) IO
 130  , Inj_Const (Consts_of_Ifaces is) IO.Handle
 131  , Inj_Const (Consts_of_Ifaces is) IO.FilePath
 132  , Inj_Const (Consts_of_Ifaces is) IO.IOMode
 133  , Inj_Const (Consts_of_Ifaces is) (->)
 134  , Inj_Const (Consts_of_Ifaces is) ()
 135  , Term_from is ast
 136  ) => Term_fromI is (Proxy IO) ast where
 137         term_fromI ast ctx k =
 138                 case ast_lexem ast of
 139                  "IO.hClose"   -> io_hClose_from
 140                  "IO.openFile" -> io_openFile_from
 141                  _ -> Left $ Error_Term_unsupported
 142                 where
 143                 io_hClose_from =
 144                  -- hClose :: Handle -> IO ()
 145                         case ast_nodes ast of
 146                          [] -> Left $ Error_Term_Syntax $
 147                                 Error_Syntax_more_arguments_needed $ At (Just ast) 1
 148                          [ast_h] ->
 149                                 term_from ast_h ctx $ \ty_h (TermLC h) ->
 150                                 check_type (At Nothing tyIO_Handle) (At (Just ast_h) ty_h) $ \Refl ->
 151                                 k (tyIO :$ tyUnit) $ TermLC $
 152                                 io_hClose . h
 153                          _ -> Left $ Error_Term_Syntax $
 154                                 Error_Syntax_too_many_arguments $ At (Just ast) 1
 155                 io_openFile_from =
 156                  -- openFile :: FilePath -> IOMode -> IO Handle
 157                         case ast_nodes ast of
 158                          [] -> Left $ Error_Term_Syntax $
 159                                 Error_Syntax_more_arguments_needed $ At (Just ast) 1
 160                          [ast_fp] ->
 161                                 term_from ast_fp ctx $ \ty_fp (TermLC fp) ->
 162                                 check_type (At Nothing tyIO_FilePath) (At (Just ast_fp) ty_fp) $ \Refl ->
 163                                 k (tyIO_IOMode ~> tyIO :$ tyIO_Handle) $ TermLC $
 164                                  \c -> lam $ io_openFile (fp c)
 165                          [ast_fp, ast_m] ->
 166                                 term_from ast_fp ctx $ \ty_fp (TermLC fp) ->
 167                                 term_from ast_m  ctx $ \ty_m  (TermLC m) ->
 168                                 check_type (At Nothing tyIO_FilePath) (At (Just ast_fp) ty_fp) $ \Refl ->
 169                                 check_type (At Nothing tyIO_IOMode) (At (Just ast_m) ty_m) $ \Refl ->
 170                                 k (tyIO :$ tyIO_Handle) $ TermLC $
 171                                  \c -> io_openFile (fp c) (m c)
 172                          _ -> Left $ Error_Term_Syntax $
 173                                 Error_Syntax_too_many_arguments $ At (Just ast) 2
 174
 175 -- | The 'IO' 'Type'
 176 tyIO :: Inj_Const cs IO => Type cs IO
 177 tyIO = TyConst inj_const
 178
 179 -- | The 'IO.Handle' 'Type'
 180 tyIO_Handle :: Inj_Const cs IO.Handle => Type cs IO.Handle
 181 tyIO_Handle = TyConst inj_const
 182
 183 -- | The 'IO.IOMode' 'Type'
 184 tyIO_IOMode :: Inj_Const cs IO.IOMode => Type cs IO.IOMode
 185 tyIO_IOMode = TyConst inj_const
 186
 187 -- | The 'IO.FilePath' 'Type'
 188 tyIO_FilePath :: Inj_Const cs IO.FilePath => Type cs IO.FilePath
 189 tyIO_FilePath = TyConst inj_const
 190
 191 sym_IO :: Proxy Sym_IO
 192 sym_IO = Proxy
 193
 194 syIO :: IsString a => [Syntax a] -> Syntax a
 195 syIO = Syntax "IO"