symantic-lib/Language/Symantic/Lib/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.Lib.IO where
   6
   7 import Control.Monad (liftM, liftM2)
   8 import Data.Proxy
   9 import Data.Type.Equality ((:~:)(Refl))
  10 import qualified System.IO as IO
  11
  12 import Language.Symantic.Parsing
  13 import Language.Symantic.Typing
  14 import Language.Symantic.Compiling
  15 import Language.Symantic.Interpreting
  16 import Language.Symantic.Transforming
  17 import Language.Symantic.Lib.Lambda
  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 TyConsts_of_Iface (Proxy IO) = Proxy IO ': TyConsts_imported_by IO
  32 type instance TyConsts_of_Iface (Proxy IO.Handle) = Proxy IO.Handle ': TyConsts_imported_by IO.Handle
  33 type instance TyConsts_of_Iface (Proxy IO.IOMode) = Proxy IO.IOMode ': TyConsts_imported_by IO.IOMode
  34 type instance TyConsts_imported_by IO =
  35  [ Proxy IO.Handle
  36  , Proxy IO.IOMode
  37  , Proxy Applicative
  38  , Proxy Functor
  39  , Proxy Monad
  40  ]
  41 type instance TyConsts_imported_by IO.Handle =
  42  '[ Proxy Eq
  43  ]
  44 type instance TyConsts_imported_by IO.IOMode =
  45  [ Proxy Enum
  46  , Proxy Eq
  47  , Proxy Ord
  48  ]
  49
  50 instance Sym_IO HostI where
  51         io_hClose   = liftM IO.hClose
  52         io_openFile = liftM2 IO.openFile
  53 instance Sym_IO TextI where
  54         io_hClose   = textI1 "IO.hClose"
  55         io_openFile = textI2 "IO.openFile"
  56 instance (Sym_IO r1, Sym_IO r2) => Sym_IO (DupI r1 r2) where
  57         io_hClose   = dupI1 @Sym_IO io_hClose
  58         io_openFile = dupI2 @Sym_IO io_openFile
  59
  60 instance
  61  ( Read_TyNameR TyName cs rs
  62  , Inj_TyConst cs IO
  63  ) => Read_TyNameR TyName cs (Proxy IO ': rs) where
  64         read_TyNameR _cs (TyName "IO") k = k (ty @IO)
  65         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
  66 instance
  67  ( Read_TyNameR TyName cs rs
  68  , Inj_TyConst cs IO.Handle
  69  ) => Read_TyNameR TyName cs (Proxy IO.Handle ': rs) where
  70         read_TyNameR _cs (TyName "IO.Handle") k = k (ty @IO.Handle)
  71         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
  72 instance
  73  ( Read_TyNameR TyName cs rs
  74  , Inj_TyConst cs IO.IOMode
  75  ) => Read_TyNameR TyName cs (Proxy IO.IOMode ': rs) where
  76         read_TyNameR _cs (TyName "IO.Mode") k = k (ty @IO.IOMode)
  77         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
  78
  79 instance Show_TyConst cs => Show_TyConst (Proxy IO ': cs) where
  80         show_TyConst TyConstZ{} = "IO"
  81         show_TyConst (TyConstS c) = show_TyConst c
  82 instance Show_TyConst cs => Show_TyConst (Proxy IO.Handle ': cs) where
  83         show_TyConst TyConstZ{} = "IO.Handle"
  84         show_TyConst (TyConstS c) = show_TyConst c
  85 instance Show_TyConst cs => Show_TyConst (Proxy IO.IOMode ': cs) where
  86         show_TyConst TyConstZ{} = "IO.IOMode"
  87         show_TyConst (TyConstS c) = show_TyConst c
  88
  89 instance -- Proj_TyConC IO
  90  ( Proj_TyConst cs IO
  91  , Proj_TyConsts cs (TyConsts_imported_by IO)
  92  ) => Proj_TyConC cs (Proxy IO) where
  93         proj_TyConC _ (TyConst q :$ TyConst c)
  94          | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
  95          , Just Refl <- proj_TyConst c (Proxy @IO)
  96          = case () of
  97                  _ | Just Refl <- proj_TyConst q (Proxy @Applicative) -> Just TyCon
  98                    | Just Refl <- proj_TyConst q (Proxy @Functor)     -> Just TyCon
  99                    | Just Refl <- proj_TyConst q (Proxy @Monad)       -> Just TyCon
 100                  _ -> Nothing
 101         proj_TyConC _c _q = Nothing
 102 instance -- Proj_TyConC IO.Handle
 103  ( Proj_TyConst cs IO.Handle
 104  , Proj_TyConsts cs (TyConsts_imported_by IO.Handle)
 105  ) => Proj_TyConC cs (Proxy IO.Handle) where
 106         proj_TyConC _ (TyConst q :$ TyConst c)
 107          | Just Refl <- eq_skind (kind_of_TyConst c) SKiType
 108          , Just Refl <- proj_TyConst c (Proxy @IO.Handle)
 109          = case () of
 110                  _ | Just Refl <- proj_TyConst q (Proxy @Eq) -> Just TyCon
 111                  _ -> Nothing
 112         proj_TyConC _c _q = Nothing
 113 instance -- Proj_TyConC IO.IOMode
 114  ( Proj_TyConst cs IO.IOMode
 115  , Proj_TyConsts cs (TyConsts_imported_by IO.IOMode)
 116  ) => Proj_TyConC cs (Proxy IO.IOMode) where
 117         proj_TyConC _ (TyConst q :$ TyConst c)
 118          | Just Refl <- eq_skind (kind_of_TyConst c) SKiType
 119          , Just Refl <- proj_TyConst c (Proxy @IO.IOMode)
 120          = case () of
 121                  _ | Just Refl <- proj_TyConst q (Proxy @Enum) -> Just TyCon
 122                    | Just Refl <- proj_TyConst q (Proxy @Eq)   -> Just TyCon
 123                    | Just Refl <- proj_TyConst q (Proxy @Ord)  -> Just TyCon
 124                  _ -> Nothing
 125         proj_TyConC _c _q = Nothing
 126 data instance TokenT meta (ts::[*]) (Proxy IO)
 127  = Token_Term_IO_hClose   (EToken meta ts)
 128  | Token_Term_IO_openFile (EToken meta ts)
 129 data instance TokenT meta (ts::[*]) (Proxy IO.Handle)
 130 data instance TokenT meta (ts::[*]) (Proxy IO.IOMode)
 131 deriving instance Eq_Token   meta ts => Eq   (TokenT meta ts (Proxy IO))
 132 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy IO))
 133 deriving instance Eq_Token   meta ts => Eq   (TokenT meta ts (Proxy IO.Handle))
 134 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy IO.Handle))
 135 deriving instance Eq_Token   meta ts => Eq   (TokenT meta ts (Proxy IO.IOMode))
 136 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy IO.IOMode))
 137 instance -- CompileI IO
 138  ( Inj_TyConst (TyConsts_of_Ifaces is) IO
 139  , Inj_TyConst (TyConsts_of_Ifaces is) IO.Handle
 140  , Inj_TyConst (TyConsts_of_Ifaces is) []
 141  , Inj_TyConst (TyConsts_of_Ifaces is) Char
 142  , Inj_TyConst (TyConsts_of_Ifaces is) IO.IOMode
 143  , Inj_TyConst (TyConsts_of_Ifaces is) (->)
 144  , Inj_TyConst (TyConsts_of_Ifaces is) ()
 145  , Compile is
 146  ) => CompileI is (Proxy IO) where
 147         compileI tok ctx k =
 148                 case tok of
 149                  Token_Term_IO_hClose tok_h ->
 150                         -- hClose :: Handle -> IO ()
 151                         compileO tok_h ctx $ \ty_h (TermO h) ->
 152                         check_TyEq
 153                          (At Nothing (ty @IO.Handle))
 154                          (At (Just tok_h) ty_h) $ \Refl ->
 155                         k (ty @IO :$ ty @()) $ TermO $
 156                                 io_hClose . h
 157                  Token_Term_IO_openFile tok_fp ->
 158                         -- openFile :: FilePath -> IOMode -> IO Handle
 159                         compileO tok_fp ctx $ \ty_fp (TermO fp) ->
 160                         check_TyEq
 161                          (At Nothing tyFilePath)
 162                          (At (Just tok_fp) ty_fp) $ \Refl ->
 163                         k (ty @IO.IOMode ~> ty @IO :$ ty @IO.Handle) $ TermO $
 164                          \c -> lam $ io_openFile (fp c)
 165                 where tyFilePath = ty @[] :$ ty @Char
 166 instance CompileI is (Proxy IO.Handle) where
 167         compileI tok _ctx _k = case tok of _ -> undefined
 168 instance CompileI is (Proxy IO.IOMode) where
 169         compileI tok _ctx _k = case tok of _ -> undefined
 170 instance -- TokenizeT IO
 171  Inj_Token meta ts IO =>
 172  TokenizeT meta ts (Proxy IO) where
 173         tokenizeT _t = mempty
 174          { tokenizers_infix = tokenizeTMod [Mod_Name "IO"]
 175                  [ tokenize1 "hClose"   infixN5 Token_Term_IO_hClose
 176                  , tokenize1 "openFile" infixN5 Token_Term_IO_openFile
 177                  ]
 178          }
 179 instance TokenizeT meta ts (Proxy IO.Handle)
 180 instance TokenizeT meta ts (Proxy IO.IOMode)
 181 instance Gram_Term_AtomsT meta ts (Proxy IO) g
 182 instance Gram_Term_AtomsT meta ts (Proxy IO.Handle) g
 183 instance Gram_Term_AtomsT meta ts (Proxy IO.IOMode) g