Language/Symantic/Compiling/IO.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 {-# OPTIONS_GHC -fconstraint-solver-iterations=5 #-}
   4 -- | Symantic for 'IO'.
   5 module Language.Symantic.Compiling.IO where
   6
   7 import Control.Monad (liftM, liftM2)
   8 import Data.Proxy
   9 import Data.Text (Text)
  10 import Data.Type.Equality ((:~:)(Refl))
  11 import qualified System.IO as IO
  12
  13 import Language.Symantic.Parsing
  14 import Language.Symantic.Typing
  15 import Language.Symantic.Compiling.Term
  16 import Language.Symantic.Interpreting
  17 import Language.Symantic.Transforming.Trans
  18
  19 -- * Class 'Sym_IO'
  20 class Sym_IO term where
  21         io_hClose   :: term IO.Handle -> term (IO ())
  22         io_openFile :: term IO.FilePath -> term IO.IOMode -> term (IO IO.Handle)
  23
  24         default io_hClose   :: Trans t term => t term IO.Handle -> t term (IO ())
  25         default io_openFile :: Trans t term => t term IO.FilePath -> t term IO.IOMode -> t term (IO IO.Handle)
  26
  27         io_hClose   = trans_map1 io_hClose
  28         io_openFile = trans_map2 io_openFile
  29
  30 type instance Sym_of_Iface (Proxy IO) = Sym_IO
  31 type instance Consts_of_Iface (Proxy IO) = Proxy IO ': Consts_imported_by IO
  32 type instance Consts_imported_by IO =
  33  [ Proxy IO.Handle
  34  , Proxy IO.IOMode
  35  , Proxy Applicative
  36  , Proxy Functor
  37  , Proxy Monad
  38  ]
  39 type instance Consts_imported_by IO.Handle =
  40  '[ Proxy Eq
  41  ]
  42 type instance Consts_imported_by IO.IOMode =
  43  [ Proxy Enum
  44  , Proxy Eq
  45  , Proxy Ord
  46  ]
  47
  48 instance Sym_IO HostI where
  49         io_hClose   = liftM IO.hClose
  50         io_openFile = liftM2 IO.openFile
  51 instance Sym_IO TextI where
  52         io_hClose   = textI1 "IO.hClose"
  53         io_openFile = textI2 "IO.openFile"
  54 instance (Sym_IO r1, Sym_IO r2) => Sym_IO (DupI r1 r2) where
  55         io_hClose   = dupI1 (Proxy @Sym_IO) io_hClose
  56         io_openFile = dupI2 (Proxy @Sym_IO) io_openFile
  57
  58 instance Const_from Text cs => Const_from Text (Proxy IO ': cs) where
  59         const_from "IO" k = k (ConstZ kind)
  60         const_from s k = const_from s $ k . ConstS
  61 instance Const_from Text cs => Const_from Text (Proxy IO.Handle ': cs) where
  62         const_from "IO.Handle" k = k (ConstZ kind)
  63         const_from s k = const_from s $ k . ConstS
  64 instance Const_from Text cs => Const_from Text (Proxy IO.IOMode ': cs) where
  65         const_from "IO.IOMode" k = k (ConstZ kind)
  66         const_from s k = const_from s $ k . ConstS
  67
  68 instance Show_Const cs => Show_Const (Proxy IO ': cs) where
  69         show_const ConstZ{} = "IO"
  70         show_const (ConstS c) = show_const c
  71 instance Show_Const cs => Show_Const (Proxy IO.Handle ': cs) where
  72         show_const ConstZ{} = "IO.Handle"
  73         show_const (ConstS c) = show_const c
  74 instance Show_Const cs => Show_Const (Proxy IO.IOMode ': cs) where
  75         show_const ConstZ{} = "IO.IOMode"
  76         show_const (ConstS c) = show_const c
  77
  78 instance -- Proj_ConC IO
  79  ( Proj_Const cs IO
  80  , Proj_Consts cs (Consts_imported_by IO)
  81  ) => Proj_ConC cs (Proxy IO) where
  82         proj_conC _ (TyConst q :$ TyConst c)
  83          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
  84          , Just Refl <- proj_const c (Proxy::Proxy IO)
  85          = case () of
  86                  _ | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
  87                    | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
  88                    | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
  89                  _ -> Nothing
  90         proj_conC _c _q = Nothing
  91 instance -- Proj_ConC IO.Handle
  92  ( Proj_Const cs IO.Handle
  93  , Proj_Consts cs (Consts_imported_by IO.Handle)
  94  ) => Proj_ConC cs (Proxy IO.Handle) where
  95         proj_conC _ (TyConst q :$ TyConst c)
  96          | Just Refl <- eq_skind (kind_of_const c) SKiType
  97          , Just Refl <- proj_const c (Proxy::Proxy IO.Handle)
  98          = case () of
  99                  _ | Just Refl <- proj_const q (Proxy::Proxy Eq) -> Just Con
 100                  _ -> Nothing
 101         proj_conC _c _q = Nothing
 102 instance -- Proj_ConC IO.IOMode
 103  ( Proj_Const cs IO.IOMode
 104  , Proj_Consts cs (Consts_imported_by IO.IOMode)
 105  ) => Proj_ConC cs (Proxy IO.IOMode) 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.IOMode)
 109          = case () of
 110                  _ | Just Refl <- proj_const q (Proxy::Proxy Enum) -> Just Con
 111                    | Just Refl <- proj_const q (Proxy::Proxy Eq)   -> Just Con
 112                    | Just Refl <- proj_const q (Proxy::Proxy Ord)  -> Just Con
 113                  _ -> Nothing
 114         proj_conC _c _q = Nothing
 115 data instance TokenT meta (ts::[*]) (Proxy IO)
 116  = Token_Term_IO_hClose   (EToken meta ts)
 117  | Token_Term_IO_openFile (EToken meta ts)
 118 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy IO))
 119 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy IO))
 120 instance -- CompileI
 121  ( Inj_Const (Consts_of_Ifaces is) IO
 122  , Inj_Const (Consts_of_Ifaces is) IO.Handle
 123  , Inj_Const (Consts_of_Ifaces is) []
 124  , Inj_Const (Consts_of_Ifaces is) Char
 125  , Inj_Const (Consts_of_Ifaces is) IO.IOMode
 126  , Inj_Const (Consts_of_Ifaces is) (->)
 127  , Inj_Const (Consts_of_Ifaces is) ()
 128  , Compile is
 129  ) => CompileI is (Proxy IO) where
 130         compileI tok ctx k =
 131                 case tok of
 132                  Token_Term_IO_hClose tok_h ->
 133                         -- hClose :: Handle -> IO ()
 134                         compileO tok_h ctx $ \ty_h (TermO h) ->
 135                         check_type
 136                          (At Nothing (ty @IO.Handle))
 137                          (At (Just tok_h) ty_h) $ \Refl ->
 138                         k (ty @IO :$ ty @()) $ TermO $
 139                                 io_hClose . h
 140                  Token_Term_IO_openFile tok_fp ->
 141                         -- openFile :: FilePath -> IOMode -> IO Handle
 142                         compileO tok_fp ctx $ \ty_fp (TermO fp) ->
 143                         check_type
 144                          (At Nothing tyFilePath)
 145                          (At (Just tok_fp) ty_fp) $ \Refl ->
 146                         k (ty @IO.IOMode ~> ty @IO :$ ty @IO.Handle) $ TermO $
 147                          \c -> lam $ io_openFile (fp c)
 148                 where tyFilePath = ty @[] :$ ty @Char